Theory Incredible_Completeness

theory Incredible_Completeness
imports Build_Incredible_Tree
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 v1 p1 v2 p2 p'
  assume assms: "((v1, p1), (v2, p2)) ∈ edges" "hyps (nodeOf v1) p1 = Some p'"
  from assms(1) hyps_correct[OF assms(2)]
  have "valid_out_port (v1, p1)" and "valid_in_port (v2, p2)" and "valid_in_port (v1, p')" and "v2 |∈| vertices"
    using valid_edges by auto

  from assms
  have "∃ i. fst v1 = fst v2 ∧ prefix (snd v1@[i]) (snd v2) ∧ p' = in_port_at v1 i"
    by (cases v1; cases v2; auto elim!: edge_step)
  hence "scope' v1 p' v2"
    unfolding scope_valid_inport[OF `v2 |∈| vertices`].
  hence "v2 ∈ scope (v1, p')"
    unfolding in_scope[OF `valid_in_port (v1, p')`].
  thus "(v2, p2) = (v1, p') ∨ v2 ∈ scope (v1, 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 v1 p1 v2 p2
  assume "((v1, p1), (v2, p2)) ∈ edges"
  thus "labelAtOut v1 p1 = labelAtIn v2 p2"
  proof(cases rule:edges.cases)
    case (regular_edge c "is")
   
    from `((v1, p1), v2, p2) = edge_at c is`
    have "(v1,p1) = edge_from c is" using fst_edge_at by (metis fst_conv)
    hence [simp]: "v1 = (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 v1 p1 = subst (iSubst ?t') (freshen (vidx v1) (iOutPort ?t'))"
        using regular_edge Nil by (simp add: labelAtOut_def edge_at_def edge_from_def)
      also have "vidx v1 = 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 v2 p2"
        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 v1 p1 = subst (iSubst ?t1) (freshen (vidx v1) (iOutPort ?t1))"
        using regular_edge snoc by (simp add: labelAtOut_def edge_at_def edge_from_def)
      also have "vidx v1 = 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 v2 p2"
        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 `((v1, p1), v2, p2) = hyp_edge_at c is n s`
    have "(v1,p1) = hyp_edge_from c is n s" using fst_hyp_edge_at by (metis fst_conv)
    hence [simp]: "v1 = (c, 0 # ?his)" by (simp add: hyp_edge_from_def)


    have "labelAtOut v1 p1 = subst (iSubst ?t1) (freshen (vidx v1) (labelsOut (iNodeOf ?t1) ?h))"
      using hyp_edge by (simp add: hyp_edge_at_def hyp_edge_from_def labelAtOut_def)
    also have "vidx v1 = 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 v2 p2"
        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