theory Incredible_Completeness imports Natural_Deduction Incredible_Deduction Build_Incredible_Tree begin text ‹ This theory takes the tree produced in @{theory Incredible_Proof_Machine.Build_Incredible_Tree}, globalizes it using @{term globalize}, and then builds the incredible proof graph out of it. › type_synonym 'form vertex = "('form × nat list)" type_synonym ('form, 'var) edge'' = "('form vertex, 'form, 'var) edge'" locale Solved_Task = Abstract_Task freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP antecedent consequent rules assumptions conclusions for freshenLC :: "nat ⇒ 'var ⇒ 'var" and renameLCs :: "('var ⇒ 'var) ⇒ 'form ⇒ 'form" and lconsts :: "'form ⇒ 'var set" and closed :: "'form ⇒ bool" and subst :: "'subst ⇒ 'form ⇒ 'form" and subst_lconsts :: "'subst ⇒ 'var set" and subst_renameLCs :: "('var ⇒ 'var) ⇒ ('subst ⇒ 'subst)" and anyP :: "'form" and antecedent :: "'rule ⇒ ('form, 'var) antecedent list" and consequent :: "'rule ⇒ 'form list" and rules :: "'rule stream" and assumptions :: "'form list" and conclusions :: "'form list" + assumes solved: solved begin text ‹Let us get our hand on concrete trees.› definition ts :: "'form ⇒ (('form entailment) × ('rule × 'form) NatRule) tree" where "ts c = (SOME t. snd (fst (root t)) = c ∧ fst (fst (root t)) |⊆| ass_forms ∧ wf t ∧ tfinite t)" lemma assumes "c |∈| conc_forms" shows ts_conc: "snd (fst (root (ts c))) = c" and ts_context: "fst (fst (root (ts c))) |⊆| ass_forms" and ts_wf: "wf (ts c)" and ts_finite[simp]: "tfinite (ts c)" unfolding atomize_conj conj_assoc ts_def apply (rule someI_ex) using solved assms by (force simp add: solved_def) abbreviation it' where "it' c ≡ globalize [fidx conc_forms c, 0] (freshenLC v_away) (to_it (ts c))" lemma iwf_it: assumes "c ∈ set conclusions" shows "plain_iwf (it' c) (fst (root (ts c)))" using assms apply (auto simp add: ts_conc conclusions_closed intro!: iwf_globalize' iwf_to_it ts_finite ts_wf) by (meson assumptions_closed fset_mp mem_ass_forms mem_conc_forms ts_context) definition vertices :: "'form vertex fset" where "vertices = Abs_fset (Union ( set (map (λ c. insert (c, []) ((λ p. (c, 0 # p)) ` (it_paths (it' c)))) conclusions)))" lemma mem_vertices: "v |∈| vertices ⟷ (fst v ∈ set conclusions ∧ (snd v = [] ∨ snd v ∈ ((#) 0) ` it_paths (it' (fst v))))" unfolding vertices_def fmember.rep_eq ffUnion.rep_eq by (cases v)(auto simp add: Abs_fset_inverse Bex_def ) lemma prefixeq_vertices: "(c,is) |∈| vertices ⟹ prefix is' is ⟹ (c, is') |∈| vertices" by (cases is') (auto simp add: mem_vertices intro!: imageI elim: it_paths_prefix) lemma none_vertices[simp]: "(c, []) |∈| vertices ⟷ c ∈ set conclusions" by (simp add: mem_vertices) lemma some_vertices[simp]: "(c, i#is) |∈| vertices ⟷ c ∈ set conclusions ∧ i = 0 ∧ is ∈ it_paths (it' c)" by (auto simp add: mem_vertices) lemma vertices_cases[consumes 1, case_names None Some]: assumes "v |∈| vertices" obtains c where "c ∈ set conclusions" and "v = (c, [])" | c "is" where "c ∈ set conclusions" and "is ∈ it_paths (it' c)" and "v = (c, 0#is)" using assms by (cases v; rename_tac "is"; case_tac "is"; auto) lemma vertices_induct[consumes 1, case_names None Some]: assumes "v |∈| vertices" assumes "⋀ c. c ∈ set conclusions ⟹ P (c, [])" assumes "⋀ c is . c ∈ set conclusions ⟹ is ∈ it_paths (it' c) ⟹ P (c, 0#is)" shows "P v" using assms by (cases v; rename_tac "is"; case_tac "is"; auto) fun nodeOf :: "'form vertex ⇒ ('form, 'rule) graph_node" where "nodeOf (pf, []) = Conclusion pf" | "nodeOf (pf, i#is) = iNodeOf (tree_at (it' pf) is)" fun inst where "inst (c,[]) = empty_subst" |"inst (c, i#is) = iSubst (tree_at (it' c) is)" lemma terminal_is_nil[simp]: "v |∈| vertices ⟹ outPorts (nodeOf v) = {||} ⟷ snd v = []" by (induction v rule: nodeOf.induct) (auto elim: iNodeOf_outPorts[rotated] iwf_it) sublocale Vertex_Graph nodes inPorts outPorts vertices nodeOf. definition edge_from :: "'form ⇒ nat list => ('form vertex × ('form,'var) out_port)" where "edge_from c is = ((c, 0 # is), Reg (iOutPort (tree_at (it' c) is)))" lemma fst_edge_from[simp]: "fst (edge_from c is) = (c, 0 # is)" by (simp add: edge_from_def) fun in_port_at :: "('form × nat list) ⇒ nat ⇒ ('form,'var) in_port" where "in_port_at (c, []) _ = plain_ant c" | "in_port_at (c, _#is) i = inPorts' (iNodeOf (tree_at (it' c) is)) ! i" definition edge_to :: "'form ⇒ nat list => ('form vertex × ('form,'var) in_port)" where "edge_to c is = (case rev is of [] ⇒ ((c, []), in_port_at (c, []) 0) | i#is ⇒ ((c, 0 # (rev is)), in_port_at (c, (0#rev is)) i))" lemma edge_to_Nil[simp]: "edge_to c [] = ((c, []), plain_ant c)" by (simp add: edge_to_def) lemma edge_to_Snoc[simp]: "edge_to c (is@[i]) = ((c, 0 # is), in_port_at ((c, 0 # is)) i)" by (simp add: edge_to_def) definition edge_at :: "'form ⇒ nat list => ('form, 'var) edge''" where "edge_at c is = (edge_from c is, edge_to c is)" lemma fst_edge_at[simp]: "fst (edge_at c is) = edge_from c is" by (simp add: edge_at_def) lemma snd_edge_at[simp]: "snd (edge_at c is) = edge_to c is" by (simp add: edge_at_def) lemma hyps_exist': assumes "c ∈ set conclusions" assumes "is ∈ it_paths (it' c)" assumes "tree_at (it' c) is = (HNode i s ants)" shows "subst s (freshen i anyP) ∈ hyps_along (it' c) is" proof- from assms(1) have "plain_iwf (it' c) (fst (root (ts c)))" by (rule iwf_it) moreover note assms(2,3) moreover have "fst (fst (root (ts c))) |⊆| ass_forms" by (simp add: assms(1) ts_context) ultimately show ?thesis by (rule iwf_hyps_exist) qed definition hyp_edge_to :: "'form ⇒ nat list => ('form vertex × ('form,'var) in_port)" where "hyp_edge_to c is = ((c, 0 # is), plain_ant anyP)" (* TODO: Replace n and s by "subst s (freshen n anyP)" *) definition hyp_edge_from :: "'form ⇒ nat list => nat ⇒ 'subst ⇒ ('form vertex × ('form,'var) out_port)" where "hyp_edge_from c is n s = ((c, 0 # hyp_port_path_for (it' c) is (subst s (freshen n anyP))), hyp_port_h_for (it' c) is (subst s (freshen n anyP)))" definition hyp_edge_at :: "'form ⇒ nat list => nat ⇒ 'subst ⇒ ('form, 'var) edge''" where "hyp_edge_at c is n s = (hyp_edge_from c is n s, hyp_edge_to c is)" lemma fst_hyp_edge_at[simp]: "fst (hyp_edge_at c is n s) = hyp_edge_from c is n s" by (simp add:hyp_edge_at_def) lemma snd_hyp_edge_at[simp]: "snd (hyp_edge_at c is n s) = hyp_edge_to c is" by (simp add:hyp_edge_at_def) inductive_set edges where regular_edge: "c ∈ set conclusions ⟹ is ∈ it_paths (it' c) ⟹ edge_at c is ∈ edges" | hyp_edge: "c ∈ set conclusions ⟹ is ∈ it_paths (it' c) ⟹ tree_at (it' c) is = HNode n s ants ⟹ hyp_edge_at c is n s ∈ edges" sublocale Pre_Port_Graph nodes inPorts outPorts vertices nodeOf edges. lemma edge_from_valid_out_port: assumes "p ∈ it_paths (it' c)" assumes "c ∈ set conclusions" shows "valid_out_port (edge_from c p)" using assms by (auto simp add: edge_from_def intro: iwf_outPort iwf_it) lemma edge_to_valid_in_port: assumes "p ∈ it_paths (it' c)" assumes "c ∈ set conclusions" shows "valid_in_port (edge_to c p)" using assms apply (auto simp add: edge_to_def inPorts_fset_of split: list.split elim!: it_paths_SnocE) apply (rule nth_mem) apply (drule (1) iwf_length_inPorts[OF iwf_it]) apply auto done lemma hyp_edge_from_valid_out_port: assumes "is ∈ it_paths (it' c)" assumes "c ∈ set conclusions" assumes "tree_at (it' c) is = HNode n s ants" shows "valid_out_port (hyp_edge_from c is n s)" using assms by(auto simp add: hyp_edge_from_def intro: hyp_port_outPort it_paths_strict_prefix hyp_port_strict_prefix hyps_exist') lemma hyp_edge_to_valid_in_port: assumes "is ∈ it_paths (it' c)" assumes "c ∈ set conclusions" assumes "tree_at (it' c) is = HNode n s ants" shows "valid_in_port (hyp_edge_to c is)" using assms by (auto simp add: hyp_edge_to_def) inductive scope' :: "'form vertex ⇒ ('form,'var) in_port ⇒ 'form × nat list ⇒ bool" where "c ∈ set conclusions ⟹ is' ∈ ((#) 0) ` it_paths (it' c) ⟹ prefix (is@[i]) is' ⟹ ip = in_port_at (c,is) i ⟹ scope' (c, is) ip (c, is')" inductive_simps scope_simp: "scope' v i v'" inductive_cases scope_cases: "scope' v i v'" lemma scope_valid: "scope' v i v' ⟹ v' |∈| vertices" by (auto elim: scope_cases) lemma scope_valid_inport: "v' |∈| vertices ⟹ scope' v ip v' ⟷ (∃ i. fst v = fst v' ∧ prefix (snd v@[i]) (snd v') ∧ ip = in_port_at v i)" by (cases v; cases v') (auto simp add: scope'.simps mem_vertices) definition terminal_path_from :: "'form ⇒ nat list => ('form, 'var) edge'' list" where "terminal_path_from c is = map (edge_at c) (rev (prefixes is))" lemma terminal_path_from_Nil[simp]: "terminal_path_from c [] = [edge_at c []]" by (simp add: terminal_path_from_def) lemma terminal_path_from_Snoc[simp]: "terminal_path_from c (is @ [i]) = edge_at c (is@[i]) # terminal_path_from c is" by (simp add: terminal_path_from_def) lemma path_terminal_path_from: "c ∈ set conclusions ⟹ is ∈ it_paths (it' c) ⟹ path (c, 0 # is) (c, []) (terminal_path_from c is)" by (induction "is" rule: rev_induct) (auto simp add: path_cons_simp intro!: regular_edge elim: it_paths_SnocE) lemma edge_step: assumes "(((a, b), ba), ((aa, bb), bc)) ∈ edges" obtains i where "a = aa" and "b = bb@[i]" and "bc = in_port_at (aa,bb) i" and "hyps (nodeOf (a, b)) ba = None" | i where "a = aa" and "prefix (b@[i]) bb" and "hyps (nodeOf (a, b)) ba = Some (in_port_at (a,b) i)" using assms proof(cases rule: edges.cases[consumes 1, case_names Reg Hyp]) case (Reg c "is") then obtain i where "a = aa" and "b = bb@[i]" and "bc = in_port_at (aa,bb) i" and "hyps (nodeOf (a, b)) ba = None" by (auto elim!: edges.cases simp add: edge_at_def edge_from_def edge_to_def split: list.split list.split_asm) thus thesis by (rule that) next case (Hyp c "is" n s) let ?i = "hyp_port_i_for (it' c) is (subst s (freshen n anyP))" from Hyp have "a = aa" and "prefix (b@[?i]) bb" and "hyps (nodeOf (a, b)) ba = Some (in_port_at (a,b) ?i)" by (auto simp add: edge_at_def edge_from_def edge_to_def hyp_edge_at_def hyp_edge_to_def hyp_edge_from_def intro: hyp_port_prefix hyps_exist' hyp_port_hyps) thus thesis by (rule that) qed lemma path_has_prefixes: assumes "path v v' pth" assumes "snd v' = []" assumes "prefix (is' @ [i]) (snd v)" shows "((fst v, is'), (in_port_at (fst v, is') i)) ∈ snd ` set pth" using assms by (induction rule: path.induct)(auto elim!: edge_step dest: prefix_snocD) lemma in_scope: "valid_in_port (v', p') ⟹ v ∈ scope (v', p') ⟷ scope' v' p' v" proof assume "v ∈ scope (v', p')" hence "v |∈| vertices" and "⋀ pth t. path v t pth ⟹ terminal_vertex t ⟹ (v', p') ∈ snd ` set pth" by (auto simp add: scope.simps) from this show "scope' v' p' v" proof (induction rule: vertices_induct) case (None c) from None(2)[of "(c, [])" "[]", simplified, OF None(1)] have False. thus "scope' v' p' (c, [])".. next case (Some c "is") from `c ∈ set conclusions` `is ∈ it_paths (it' c)` have "path (c, 0#is) (c, []) (terminal_path_from c is)" by (rule path_terminal_path_from) moreover from `c ∈ set conclusions` have "terminal_vertex (c, [])" by simp ultimately have "(v', p') ∈ snd ` set (terminal_path_from c is)" by (rule Some(3)) hence "(v',p') ∈ set (map (edge_to c) (prefixes is))" unfolding terminal_path_from_def by auto then obtain is' where "prefix is' is" and "(v',p') = edge_to c is'" by auto show "scope' v' p' (c, 0#is)" proof(cases "is'" rule: rev_cases) case Nil with `(v',p') = edge_to c is'` have "v' = (c, [])" and "p' = plain_ant c" by (auto simp add: edge_to_def) with `c ∈ set conclusions` `is ∈ it_paths (it' c)` show ?thesis by (auto intro!: scope'.intros) next case (snoc is'' i) with `(v',p') = edge_to c is'` have "v' = (c, 0 # is'')" and "p' = in_port_at v' i" by (auto simp add: edge_to_def) with `c ∈ set conclusions` `is ∈ it_paths (it' c)` `prefix is' is`[unfolded snoc] show ?thesis by (auto intro!: scope'.intros) qed qed next assume "valid_in_port (v', p')" assume "scope' v' p' v" then obtain c is' i "is" where "v' = (c, is')" and "v = (c, is)" and "c ∈ set conclusions" and "p' = in_port_at v' i" and "is ∈ (#) 0 ` it_paths (it' c)" and "prefix (is' @ [i]) is" by (auto simp add: scope'.simps) from `scope' v' p' v` have "(c, is) |∈| vertices" unfolding `v = _` by (rule scope_valid) hence "(c, is) ∈ scope ((c, is'), p')" proof(rule scope.intros) fix pth t assume "path (c,is) t pth" assume "terminal_vertex t" hence "snd t = []" by auto from path_has_prefixes[OF `path (c,is) t pth` `snd t = []`, simplified, OF `prefix (is' @ [i]) is`] show "((c, is'), p') ∈ snd ` set pth" unfolding `p' = _ ` `v' = _ `. qed thus "v ∈ scope (v', p')" using `v =_` `v' = _` by simp qed sublocale Port_Graph nodes inPorts outPorts vertices nodeOf edges proof show "nodeOf ` fset vertices ⊆ sset nodes" apply (auto simp add: fmember.rep_eq[symmetric] mem_vertices) apply (auto simp add: stream.set_map dest: iNodeOf_tree_at[OF iwf_it]) done next have "∀ e ∈ edges. valid_out_port (fst e) ∧ valid_in_port (snd e)" by (auto elim!: edges.cases simp add: edge_at_def dest: edge_from_valid_out_port edge_to_valid_in_port dest: hyp_edge_from_valid_out_port hyp_edge_to_valid_in_port) thus "∀(ps1, ps2)∈edges. valid_out_port ps1 ∧ valid_in_port ps2" by auto qed sublocale Scoped_Graph nodes inPorts outPorts vertices nodeOf edges hyps.. lemma hyps_free_path_length: assumes "path v v' pth" assumes "hyps_free pth" shows "length pth + length (snd v') = length (snd v)" using assms by induction (auto elim!: edge_step ) fun vidx :: "'form vertex ⇒ nat" where "vidx (c, []) = isidx [fidx conc_forms c]" |"vidx (c, _#is) = iAnnot (tree_at (it' c) is)" lemma my_vidx_inj: "inj_on vidx (fset vertices)" by (rule inj_onI) (auto simp add: mem_vertices[unfolded fmember.rep_eq] iAnnot_globalize simp del: iAnnot.simps) lemma vidx_not_v_away[simp]: "v |∈| vertices ⟹ vidx v ≠ v_away" by (cases v rule:vidx.cases) (auto simp add: iAnnot_globalize simp del: iAnnot.simps) sublocale Instantiation inPorts outPorts nodeOf hyps nodes edges vertices labelsIn labelsOut freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP vidx inst proof show "inj_on vidx (fset vertices)" by (rule my_vidx_inj) qed sublocale Well_Scoped_Graph nodes inPorts outPorts vertices nodeOf edges hyps proof fix v⇩_{1}p⇩_{1}v⇩_{2}p⇩_{2}p' assume assms: "((v⇩_{1}, p⇩_{1}), (v⇩_{2}, p⇩_{2})) ∈ edges" "hyps (nodeOf v⇩_{1}) p⇩_{1}= Some p'" from assms(1) hyps_correct[OF assms(2)] have "valid_out_port (v⇩_{1}, p⇩_{1})" and "valid_in_port (v⇩_{2}, p⇩_{2})" and "valid_in_port (v⇩_{1}, p')" and "v⇩_{2}|∈| vertices" using valid_edges by auto from assms have "∃ i. fst v⇩_{1}= fst v⇩_{2}∧ prefix (snd v⇩_{1}@[i]) (snd v⇩_{2}) ∧ p' = in_port_at v⇩_{1}i" by (cases v⇩_{1}; cases v⇩_{2}; auto elim!: edge_step) hence "scope' v⇩_{1}p' v⇩_{2}" unfolding scope_valid_inport[OF `v⇩_{2}|∈| vertices`]. hence "v⇩_{2}∈ scope (v⇩_{1}, p')" unfolding in_scope[OF `valid_in_port (v⇩_{1}, p')`]. thus "(v⇩_{2}, p⇩_{2}) = (v⇩_{1}, p') ∨ v⇩_{2}∈ scope (v⇩_{1}, p')" .. qed sublocale Acyclic_Graph nodes inPorts outPorts vertices nodeOf edges hyps proof fix v pth assume "path v v pth" and "hyps_free pth" from hyps_free_path_length[OF this] show "pth = []" by simp qed sublocale Saturated_Graph nodes inPorts outPorts vertices nodeOf edges proof fix v p assume "valid_in_port (v, p)" thus "∃e∈edges. snd e = (v, p)" proof(induction v) fix c cis assume "valid_in_port ((c, cis), p)" hence "c ∈ set conclusions" by (auto simp add: mem_vertices) show "∃e∈edges. snd e = ((c, cis), p)" proof(cases cis) case Nil with `valid_in_port ((c, cis), p)` have [simp]: "p = plain_ant c" by simp have "[] ∈ it_paths (it' c)" by simp with `c ∈ set conclusions` have "edge_at c [] ∈ edges" by (rule regular_edge) moreover have "snd (edge_at c []) = ((c, []), plain_ant c)" by (simp add: edge_to_def) ultimately show ?thesis by (auto simp add: Nil simp del: snd_edge_at) next case (Cons c' "is") with `valid_in_port ((c, cis), p)` have [simp]: "c' = 0" and "is ∈ it_paths (it' c)" and "p |∈| inPorts (iNodeOf (tree_at (it' c) is))" by auto from this(3) obtain i where "i < length (inPorts' (iNodeOf (tree_at (it' c) is)))" and "p = inPorts' (iNodeOf (tree_at (it' c) is)) ! i" by (auto simp add: inPorts_fset_of in_set_conv_nth) show ?thesis proof (cases "tree_at (it' c) is") case [simp]: (RNode r ants) show ?thesis proof(cases r) case I hence "¬ isHNode (tree_at (it' c) is)" by simp from iwf_length_inPorts_not_HNode[OF iwf_it[OF `c ∈ set conclusions`] `is ∈ it_paths (it' c)` this] `i < length (inPorts' (iNodeOf (tree_at (it' c) is)))` have "i < length (children (tree_at (it' c) is))" by simp with `is ∈ it_paths (it' c)` have "is@[i] ∈ it_paths (it' c)" by (rule it_path_SnocI) from `c ∈ set conclusions` this have "edge_at c (is@[i]) ∈ edges" by (rule regular_edge) moreover have "snd (edge_at c (is@[i])) = ((c, 0 # is), inPorts' (iNodeOf (tree_at (it' c) is)) ! i)" by (simp add: edge_to_def) ultimately show ?thesis by (auto simp add: Cons `p = _` simp del: snd_edge_at) next case (H n s) hence "tree_at (it' c) is = HNode n s ants" by simp from `c ∈ set conclusions` `is ∈ it_paths (it' c)` this have "hyp_edge_at c is n s ∈ edges".. moreover from H `p |∈| inPorts (iNodeOf (tree_at (it' c) is))` have [simp]: "p = plain_ant anyP" by simp have "snd (hyp_edge_at c is n s) = ((c, 0 # is), p)" by (simp add: hyp_edge_to_def) ultimately show ?thesis by (auto simp add: Cons simp del: snd_hyp_edge_at) qed qed qed qed qed sublocale Pruned_Port_Graph nodes inPorts outPorts vertices nodeOf edges proof fix v assume "v |∈| vertices" thus "∃pth v'. path v v' pth ∧ terminal_vertex v'" proof(induct rule: vertices_induct) case (None c) hence "terminal_vertex (c,[])" by simp with path.intros(1) show ?case by blast next case (Some c "is") hence "path (c, 0 # is) (c, []) (terminal_path_from c is)" by (rule path_terminal_path_from) moreover have "terminal_vertex (c,[])" using Some(1) by simp ultimately show ?case by blast qed qed sublocale Well_Shaped_Graph nodes inPorts outPorts vertices nodeOf edges hyps.. sublocale sol:Solution inPorts outPorts nodeOf hyps nodes vertices labelsIn labelsOut freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP vidx inst edges proof fix v⇩_{1}p⇩_{1}v⇩_{2}p⇩_{2}assume "((v⇩_{1}, p⇩_{1}), (v⇩_{2}, p⇩_{2})) ∈ edges" thus "labelAtOut v⇩_{1}p⇩_{1}= labelAtIn v⇩_{2}p⇩_{2}" proof(cases rule:edges.cases) case (regular_edge c "is") from `((v⇩_{1}, p⇩_{1}), v⇩_{2}, p⇩_{2}) = edge_at c is` have "(v⇩_{1},p⇩_{1}) = edge_from c is" using fst_edge_at by (metis fst_conv) hence [simp]: "v⇩_{1}= (c, 0 # is)" by (simp add: edge_from_def) show ?thesis proof(cases "is" rule:rev_cases) case Nil let "?t'" = "it' c" have "labelAtOut v⇩_{1}p⇩_{1}= subst (iSubst ?t') (freshen (vidx v⇩_{1}) (iOutPort ?t'))" using regular_edge Nil by (simp add: labelAtOut_def edge_at_def edge_from_def) also have "vidx v⇩_{1}= iAnnot ?t'" by (simp add: Nil) also have "subst (iSubst ?t') (freshen (iAnnot ?t') (iOutPort ?t')) = snd (fst (root (ts c)))" unfolding iwf_subst_freshen_outPort[OF iwf_it[OF `c ∈ set conclusions`]].. also have "… = c" using `c ∈ set conclusions` by (simp add: ts_conc) also have "… = labelAtIn v⇩_{2}p⇩_{2}" using `c ∈ set conclusions` regular_edge Nil by (simp add: labelAtIn_def edge_at_def freshen_closed conclusions_closed closed_no_lconsts) finally show ?thesis. next case (snoc is' i) let "?t1" = "tree_at (it' c) (is'@[i])" let "?t2" = "tree_at (it' c) is'" have "labelAtOut v⇩_{1}p⇩_{1}= subst (iSubst ?t1) (freshen (vidx v⇩_{1}) (iOutPort ?t1))" using regular_edge snoc by (simp add: labelAtOut_def edge_at_def edge_from_def) also have "vidx v⇩_{1}= iAnnot ?t1" using snoc regular_edge(3) by simp also have "subst (iSubst ?t1) (freshen (iAnnot ?t1) (iOutPort ?t1)) = subst (iSubst ?t2) (freshen (iAnnot ?t2) (a_conc (inPorts' (iNodeOf ?t2) ! i)))" by (rule iwf_edge_match[OF iwf_it[OF `c ∈ set conclusions`] `is ∈ it_paths (it' c)`[unfolded snoc]]) also have "iAnnot ?t2 = vidx (c, 0 # is')" by simp also have "subst (iSubst ?t2) (freshen (vidx (c, 0 # is')) (a_conc (inPorts' (iNodeOf ?t2) ! i))) = labelAtIn v⇩_{2}p⇩_{2}" using regular_edge snoc by (simp add: labelAtIn_def edge_at_def) finally show ?thesis. qed next case (hyp_edge c "is" n s ants) let ?f = "subst s (freshen n anyP)" let ?h = "hyp_port_h_for (it' c) is ?f" let ?his = "hyp_port_path_for (it' c) is ?f" let "?t1" = "tree_at (it' c) ?his" let "?t2" = "tree_at (it' c) is" from `c ∈ set conclusions` `is ∈ it_paths (it' c)` `tree_at (it' c) is = HNode n s ants` have "?f ∈ hyps_along (it' c) is" by (rule hyps_exist') from `((v⇩_{1}, p⇩_{1}), v⇩_{2}, p⇩_{2}) = hyp_edge_at c is n s` have "(v⇩_{1},p⇩_{1}) = hyp_edge_from c is n s" using fst_hyp_edge_at by (metis fst_conv) hence [simp]: "v⇩_{1}= (c, 0 # ?his)" by (simp add: hyp_edge_from_def) have "labelAtOut v⇩_{1}p⇩_{1}= subst (iSubst ?t1) (freshen (vidx v⇩_{1}) (labelsOut (iNodeOf ?t1) ?h))" using hyp_edge by (simp add: hyp_edge_at_def hyp_edge_from_def labelAtOut_def) also have "vidx v⇩_{1}= iAnnot ?t1" by simp also have "subst (iSubst ?t1) (freshen (iAnnot ?t1) (labelsOut (iNodeOf ?t1) ?h)) = ?f" using `?f ∈ hyps_along (it' c) is` by (rule local.hyp_port_eq[symmetric]) also have "… = subst (iSubst ?t2) (freshen (iAnnot ?t2) anyP)" using hyp_edge by simp also have "subst (iSubst ?t2) (freshen (iAnnot ?t2) anyP) = labelAtIn v⇩_{2}p⇩_{2}" using hyp_edge by (simp add: labelAtIn_def hyp_edge_at_def hyp_edge_to_def) finally show ?thesis. qed qed lemma node_disjoint_fresh_vars: assumes "n ∈ sset nodes" assumes "i < length (inPorts' n)" assumes "i' < length (inPorts' n)" shows "a_fresh (inPorts' n ! i) ∩ a_fresh (inPorts' n ! i') = {} ∨ i = i'" using assms no_multiple_local_consts by (fastforce simp add: nodes_def stream.set_map) sublocale Well_Scoped_Instantiation freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP inPorts outPorts nodeOf hyps nodes vertices labelsIn labelsOut vidx inst edges local_vars proof fix v p var v' assume "valid_in_port (v, p)" hence "v |∈| vertices" by simp obtain c "is" where "v = (c,is)" by (cases v, auto) from `valid_in_port (v, p)` `v= _` have "(c,is) |∈| vertices" and "p |∈| inPorts (nodeOf (c, is))" by simp_all hence "c ∈ set conclusions" by (simp add: mem_vertices) from `p |∈| _` obtain i where "i < length (inPorts' (nodeOf (c, is)))" and "p = inPorts' (nodeOf (c, is)) ! i" by (auto simp add: inPorts_fset_of in_set_conv_nth) hence "p = in_port_at (c, is) i" by (cases "is") auto assume "v' |∈| vertices" then obtain c' is' where "v' = (c',is')" by (cases v', auto) assume "var ∈ local_vars (nodeOf v) p" hence "var ∈ a_fresh p" by simp assume "freshenLC (vidx v) var ∈ subst_lconsts (inst v')" then obtain is'' where "is' = 0#is''" and "is'' ∈ it_paths (it' c')" using `v' |∈| vertices` by (cases is') (auto simp add: `v'=_`) note `freshenLC (vidx v) var ∈ subst_lconsts (inst v')` also have "subst_lconsts (inst v') = subst_lconsts (iSubst (tree_at (it' c') is''))" by (simp add: `v'=_` `is'=_`) also from `is'' ∈ it_paths (it' c')` have "… ⊆ fresh_at_path (it' c') is'' ∪ range (freshenLC v_away)" by (rule globalize_local_consts) finally have "freshenLC (vidx v) var ∈ fresh_at_path (it' c') is''" using `v |∈| vertices` by auto then obtain is''' where "prefix is''' is''" and "freshenLC (vidx v) var ∈ fresh_at (it' c') is'''" unfolding fresh_at_path_def by auto then obtain i' is'''' where "prefix (is''''@[i']) is''" and "freshenLC (vidx v) var ∈ fresh_at (it' c') (is''''@[i'])" using append_butlast_last_id[where xs = is''', symmetric] apply (cases "is''' = []") apply (auto simp del: fresh_at_snoc append_butlast_last_id) apply metis done from `is'' ∈ it_paths (it' c')` `prefix (is''''@[i']) is''` have "(is''''@[i']) ∈ it_paths (it' c')" by (rule it_paths_prefix) hence "is'''' ∈ it_paths (it' c')" using append_prefixD it_paths_prefix by blast from this `freshenLC (vidx v) var ∈ fresh_at (it' c') (is''''@[i'])` have "c = c' ∧ is = 0 # is'''' ∧ var ∈ a_fresh (inPorts' (iNodeOf (tree_at (it' c') is'''')) ! i')" unfolding fresh_at_def' using `v |∈| vertices` `v' |∈| vertices` apply (cases "is") apply (auto split: if_splits simp add: iAnnot_globalize it_paths_butlast `v=_` `v'=_` `is'=_` simp del: iAnnot.simps) done hence "c' = c" and "is = 0 # is''''" and "var ∈ a_fresh (inPorts' (iNodeOf (tree_at (it' c') is'''')) ! i')" by simp_all from `(is''''@[i']) ∈ it_paths (it' c')` have "i' < length (inPorts' (nodeOf (c, is)))" using iwf_length_inPorts[OF iwf_it[OF `c ∈ set conclusions`]] by (auto elim!: it_paths_SnocE simp add: `is=_` `c' = _` order.strict_trans2) have "nodeOf (c, is) ∈ sset nodes" unfolding `is = _` `c' = _` nodeOf.simps by (rule iNodeOf_tree_at[OF iwf_it[OF `c ∈ set conclusions`] `is'''' ∈ it_paths (it' c')`[unfolded `c' = _`]]) from `var ∈ a_fresh (inPorts' (iNodeOf (tree_at (it' c') is'''')) ! i')` `var ∈ a_fresh p` `p = inPorts' (nodeOf (c, is)) ! i` node_disjoint_fresh_vars[OF `nodeOf (c, is) ∈ sset nodes` `i < length (inPorts' (nodeOf (c, is)))` `i' < length (inPorts' (nodeOf (c, is)))`] have "i' = i" by (auto simp add: `is=_` `c'=c`) from `prefix (is''''@[i']) is''` have "prefix (is @ [i']) is'" by (simp add: `is'=_` `is=_`) from `c ∈ set conclusions` `is'' ∈ it_paths (it' c')` `prefix (is @ [i']) is'` `p = in_port_at (c, is) i` have "scope' v p v'" unfolding `v=_` `v'=_` `c' = _` `is' = _` `i'=_` by (auto intro: scope'.intros) thus "v' ∈ scope (v, p)" using `valid_in_port (v, p)` by (simp add: in_scope) qed sublocale Scoped_Proof_Graph freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP inPorts outPorts nodeOf hyps nodes vertices labelsIn labelsOut vidx inst edges local_vars.. (* interpretation of @{term Tasked_Proof_Graph} has to be named to avoid name clashes in @{term Abstract_Task}. *) sublocale tpg:Tasked_Proof_Graph freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP antecedent consequent rules assumptions conclusions vertices nodeOf edges vidx inst proof show "set (map Conclusion conclusions) ⊆ nodeOf ` fset vertices" proof- { fix c assume "c ∈ set conclusions" hence "(c, []) |∈| vertices" by simp hence "nodeOf (c, []) ∈ nodeOf ` fset vertices" unfolding fmember.rep_eq by (rule imageI) hence "Conclusion c ∈ nodeOf ` fset vertices" by simp } thus ?thesis by auto qed qed end end