# Theory Incredible_Completeness

```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'"

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

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 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"

lemma some_vertices[simp]: "(c, i#is) |∈| vertices ⟷ c ∈ set conclusions ∧ i = 0 ∧ is ∈ it_paths (it' c)"

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)"

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)"

lemma edge_to_Snoc[simp]: "edge_to c (is@[i]) = ((c, 0 # is), in_port_at ((c, 0 # is)) i)"

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"
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 []]"

lemma terminal_path_from_Snoc[simp]:
"terminal_path_from c (is @ [i]) = edge_at  c (is@[i]) # terminal_path_from c is"

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"
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"
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"
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"

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: 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 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)"
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)"
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)"
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''))"
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"
by (rule imageI)
hence "Conclusion c ∈ nodeOf ` fset vertices"  by simp
} thus ?thesis by auto
qed
qed

end

end
```