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

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