Theory Incredible_Deduction

theory Incredible_Deduction
imports
  Main 
  "HOL-Library.FSet"
  "HOL-Library.Stream"
  Incredible_Signatures
  "HOL-Eisbach.Eisbach"
begin

text ‹This theory contains the definition for actual proof graphs, and their various possible
properties.›

text ‹The following locale first defines graphs, without edges.›

locale Vertex_Graph = 
  Port_Graph_Signature nodes inPorts outPorts
    for nodes :: "'node stream"
    and inPorts :: "'node ⇒ 'inPort fset"
    and outPorts :: "'node ⇒ 'outPort fset" +
  fixes vertices :: "'v fset"
  fixes nodeOf :: "'v ⇒ 'node"
begin
  fun valid_out_port where "valid_out_port (v,p) ⟷ v |∈| vertices ∧ p |∈| outPorts (nodeOf v)"
  fun valid_in_port  where "valid_in_port (v,p) ⟷ v |∈| vertices ∧ p |∈| inPorts (nodeOf v)" 

  fun terminal_node where
    "terminal_node n ⟷ outPorts n = {||}"
  fun terminal_vertex where
    "terminal_vertex v ⟷ v |∈| vertices ∧ terminal_node (nodeOf v)"
end

text ‹And now we add the edges. This allows us to define paths and scopes.›

type_synonym ('v, 'outPort, 'inPort) edge = "(('v × 'outPort) × ('v × 'inPort))"

locale Pre_Port_Graph =
  Vertex_Graph nodes inPorts outPorts vertices nodeOf
    for nodes :: "'node stream"
    and inPorts :: "'node ⇒ 'inPort fset"
    and outPorts :: "'node ⇒ 'outPort fset"
    and vertices :: "'v fset"
    and nodeOf :: "'v ⇒ 'node" +
  fixes edges :: "('v, 'outPort, 'inPort) edge set"
begin
  fun edge_begin :: "(('v × 'outPort) × ('v × 'inPort)) ⇒ 'v" where
    "edge_begin ((v1,p1),(v2,p2)) = v1"
  fun edge_end :: "(('v × 'outPort) × ('v × 'inPort)) ⇒ 'v" where
    "edge_end ((v1,p1),(v2,p2)) = v2"

  lemma edge_begin_tup: "edge_begin x = fst (fst x)" by (metis edge_begin.simps prod.collapse)
  lemma edge_end_tup: "edge_end x = fst (snd x)" by (metis edge_end.simps prod.collapse)

  inductive path :: "'v ⇒ 'v ⇒ ('v, 'outPort, 'inPort) edge list ⇒ bool"   where
    path_empty: "path v v []" |
    path_cons: "e ∈ edges ⟹ path (edge_end e) v' pth ⟹ path (edge_begin e) v' (e#pth)"

  inductive_simps path_cons_simp': "path v v' (e#pth)"
  inductive_simps path_empty_simp[simp]: "path v v' []"
  lemma path_cons_simp: "path v v' (e # pth) ⟷ fst (fst e) = v ∧ e ∈ edges ∧ path (fst (snd e)) v' pth"
    by(auto simp add: path_cons_simp', metis prod.collapse)

  lemma path_appendI: "path v v' pth1 ⟹ path v' v'' pth2 ⟹ path v v'' (pth1@pth2)"
    by (induction pth1 arbitrary: v) (auto simp add: path_cons_simp )

  lemma path_split: "path v v' (pth1@[e]@pth2) ⟷ path v (edge_end e) (pth1@[e]) ∧ path (edge_end e) v' pth2"
    by (induction pth1 arbitrary: v) (auto simp add: path_cons_simp edge_end_tup intro: path_empty)

  lemma path_split2: "path v v' (pth1@(e#pth2)) ⟷ path v (edge_begin e) pth1 ∧ path (edge_begin e) v' (e#pth2)"
    by (induction pth1 arbitrary: v) (auto simp add: path_cons_simp edge_begin_tup intro: path_empty)

  lemma path_snoc: "path v v' (pth1@[e]) ⟷ e ∈ edges ∧ path v (edge_begin e) pth1 ∧ edge_end e = v'"
    by (auto simp add: path_split2 path_cons_simp edge_end_tup edge_begin_tup)

  inductive_set scope :: "'v × 'inPort ⇒ 'v set" for ps where
    "v |∈| vertices ⟹ (⋀ pth v'.  path v v' pth ⟹ terminal_vertex v' ⟹ ps ∈ snd ` set pth)
    ⟹ v ∈ scope ps"

  lemma scope_find:
    assumes "v ∈ scope ps"
    assumes "terminal_vertex v'"
    assumes "path v v' pth"
    shows "ps ∈ snd ` set pth"
  using assms by (auto simp add: scope.simps)

  lemma snd_set_split:
    assumes "ps ∈ snd ` set pth"
    obtains pth1 pth2 e  where "pth = pth1@[e]@pth2" and "snd e = ps" and "ps ∉ snd ` set pth1"
    using assms
    proof (atomize_elim, induction pth)
      case Nil thus ?case by simp
    next
      case (Cons e pth)
      show ?case
      proof(cases "snd e = ps")
        case True
        hence "e # pth = [] @ [e] @ pth ∧ snd e = ps ∧ ps ∉ snd ` set []" by auto
        thus ?thesis by (intro exI)
      next
        case False
        with Cons(2)
        have "ps ∈ snd ` set pth" by auto
        from Cons.IH[OF this this] 
        obtain pth1 e' pth2 where "pth = pth1 @ [e'] @ pth2 ∧ snd e' = ps ∧ ps ∉ snd ` set pth1" by auto
        with False
        have "e#pth = (e# pth1) @ [e'] @ pth2 ∧ snd e' = ps ∧ ps ∉ snd ` set (e#pth1)" by auto
        thus ?thesis by blast
      qed
    qed

  lemma scope_split:
    assumes "v ∈ scope ps"
    assumes "path v v' pth"
    assumes "terminal_vertex v'"
    obtains pth1 e pth2
    where "pth = (pth1@[e])@pth2" and "path v (fst ps) (pth1@[e])" and "path (fst ps) v' pth2" and "snd e = ps" and "ps ∉ snd ` set pth1"
  proof-
    from assms
    have "ps ∈ snd ` set pth" by (auto simp add: scope.simps)
    then obtain pth1 pth2 e  where "pth = pth1@[e]@pth2" and "snd e = ps" and "ps ∉ snd ` set pth1" by (rule snd_set_split)
    
    from ‹path _ _ _› and ‹pth = pth1@[e]@pth2›
    have "path v (edge_end e) (pth1@[e])" and "path (edge_end e) v' pth2" by (metis path_split)+
    show thesis
    proof(rule that)
      show "pth = (pth1@[e])@pth2" using ‹pth= _› by simp
      show "path v (fst ps) (pth1@[e])" using ‹path v (edge_end e) (pth1@[e])›  ‹snd e = ps› by (simp add: edge_end_tup)
      show "path (fst ps) v' pth2" using ‹path (edge_end e) v' pth2›  ‹snd e = ps› by (simp add: edge_end_tup)
      show "ps ∉ snd ` set pth1" by fact
      show "snd e = ps" by fact
    qed
  qed  
end

text ‹This adds well-formedness conditions to the edges and vertices.›

locale Port_Graph = Pre_Port_Graph +
  assumes valid_nodes: "nodeOf ` fset vertices  ⊆ sset nodes"
  assumes valid_edges: "∀ (ps1,ps2) ∈ edges. valid_out_port ps1 ∧ valid_in_port ps2"
begin
  lemma snd_set_path_verties: "path v v' pth ⟹ fst ` snd ` set pth ⊆ fset vertices"
    apply (induction rule: path.induct)
    apply auto
    apply (metis valid_in_port.elims(2) edge_end.simps case_prodD valid_edges)
    done

  lemma fst_set_path_verties: "path v v' pth ⟹ fst ` fst ` set pth ⊆ fset vertices"
    apply (induction rule: path.induct)
    apply auto
    apply (metis valid_out_port.elims(2) edge_begin.simps case_prodD valid_edges)
    done
end

text ‹A pruned graph is one where every node has a path to a terminal node (which will be the conclusions).›

locale Pruned_Port_Graph = Port_Graph +
  assumes pruned: "⋀v.  v |∈| vertices ⟹ (∃pth v'. path v v' pth ∧ terminal_vertex v')"
begin
  lemma scopes_not_refl:
    assumes "v |∈| vertices"
    shows "v ∉ scope (v,p)"
  proof(rule notI)
    assume "v ∈ scope (v,p)"

    from pruned[OF assms]
    obtain pth t where "terminal_vertex t" and "path v t pth" and least: "∀ pth'. path v t pth' ⟶ length pth ≤ length pth'"
      by atomize_elim (auto simp del: terminal_vertex.simps elim: ex_has_least_nat)
        
    from scope_split[OF ‹v ∈ scope (v,p)› ‹path v t pth› ‹terminal_vertex t›]
    obtain pth1 e pth2 where "pth = (pth1 @ [e]) @ pth2" "path v t pth2" by (metis fst_conv)

    from this(2) least
    have "length pth ≤ length pth2" by auto
    with ‹pth = _›
    show False by auto
  qed

  text ‹This lemma can be found in \<^cite>‹"incredible"›, but it is otherwise inconsequential.›
  lemma scopes_nest:
    fixes ps1 ps2
    shows "scope ps1 ⊆ scope ps2 ∨ scope ps2 ⊆ scope ps1 ∨ scope ps1 ∩ scope ps2 = {}"
  proof(cases "ps1 = ps2")
    assume "ps1 ≠ ps2"
    {
    fix v
    assume "v ∈ scope ps1 ∩ scope ps2"
    hence "v |∈| vertices" using scope.simps by auto
    then obtain pth t where "path v t pth" and "terminal_vertex t" using pruned by blast
  
    from ‹path v t pth› and ‹terminal_vertex t› and ‹v ∈ scope ps1 ∩ scope ps2›
    obtain pth1a e1 pth1b  where "pth = (pth1a@[e1])@pth1b" and "path v (fst ps1) (pth1a@[e1])" and "snd e1 = ps1" and "ps1 ∉ snd ` set pth1a"
      by (auto elim: scope_split)
  
    from ‹path v t pth› and ‹terminal_vertex t› and ‹v ∈ scope ps1 ∩ scope ps2›
    obtain pth2a e2 pth2b  where "pth = (pth2a@[e2])@pth2b" and "path v (fst ps2) (pth2a@[e2])" and "snd e2 = ps2" and "ps2 ∉ snd ` set pth2a"
      by (auto elim: scope_split)
   
    from ‹pth = (pth1a@[e1])@pth1b› ‹pth = (pth2a@[e2])@pth2b›
    have "set pth1a ⊆ set pth2a ∨ set pth2a ⊆ set pth1a" by (auto simp add: append_eq_append_conv2)
    hence "scope ps1 ⊆ scope ps2 ∨ scope ps2 ⊆ scope ps1"
    proof
      assume "set pth1a ⊆ set pth2a" with ‹ps2 ∉ _›
      have "ps2 ∉ snd ` set (pth1a@[e1])" using ‹ps1 ≠ ps2› ‹snd e1 = ps1› by auto
  
      have "scope ps1 ⊆ scope ps2"
      proof
        fix v'
        assume "v' ∈ scope ps1"
        hence "v' |∈| vertices" using scope.simps by auto
        thus "v' ∈ scope ps2"
        proof(rule scope.intros)
          fix pth' t'
          assume "path v' t' pth'" and "terminal_vertex t'"
          with ‹v' ∈ scope ps1›
          obtain pth3a e3 pth3b where "pth' = (pth3a@[e3])@pth3b" and "path (fst ps1) t' pth3b"
            by (auto elim: scope_split)
  
          have "path v t' ((pth1a@[e1]) @ pth3b)" using ‹path v (fst ps1) (pth1a@[e1])› and ‹path (fst ps1) t' pth3b›
            by (rule path_appendI)
          with ‹terminal_vertex t'› ‹v ∈ scope ps1 ∩ scope ps2›
          have "ps2 ∈ snd ` set ((pth1a@[e1]) @ pth3b)" by (meson IntD2 scope.cases)
          hence "ps2 ∈ snd ` set pth3b" using ‹ps2 ∉ snd ` set (pth1a@[e1])› by auto
          thus "ps2 ∈ snd ` set pth'" using ‹pth'=_› by auto
        qed
      qed
      thus ?thesis by simp
    next
      assume "set pth2a ⊆ set pth1a" with ‹ps1 ∉ _›
      have "ps1 ∉ snd ` set (pth2a@[e2])" using ‹ps1 ≠ ps2› ‹snd e2 = ps2› by auto
  
      have "scope ps2 ⊆ scope ps1"
      proof
        fix v'
        assume "v' ∈ scope ps2"
        hence "v' |∈| vertices" using scope.simps by auto
        thus "v' ∈ scope ps1"
        proof(rule scope.intros)
          fix pth' t'
          assume "path v' t' pth'" and "terminal_vertex t'"
          with ‹v' ∈ scope ps2›
          obtain pth3a e3 pth3b where "pth' = (pth3a@[e3])@pth3b" and "path (fst ps2) t' pth3b" 
            by (auto elim: scope_split)
  
          have "path v t' ((pth2a@[e2]) @ pth3b)" using ‹path v (fst ps2) (pth2a@[e2])› and ‹path (fst ps2) t' pth3b›
            by (rule path_appendI)
          with ‹terminal_vertex t'› ‹v ∈ scope ps1 ∩ scope ps2›
          have "ps1 ∈ snd ` set ((pth2a@[e2]) @ pth3b)" by (meson IntD1 scope.cases)
          hence "ps1 ∈ snd ` set pth3b" using ‹ps1 ∉ snd ` set (pth2a@[e2])› by auto
          thus "ps1 ∈ snd ` set pth'" using ‹pth'=_› by auto
        qed
      qed
      thus ?thesis by simp
    qed
    }
    thus ?thesis by blast
  qed simp
end

text ‹A well-scoped graph is one where a port marked to be a local hypothesis is only connected to
the corresponding input port, either directly or via a path. It must not be, however, that there is
a a path from such a hypothesis to a terminal node that does not pass by the dedicated input port;
this is expressed via scopes.
›

locale Scoped_Graph = Port_Graph + Port_Graph_Signature_Scoped
locale Well_Scoped_Graph = Scoped_Graph +
  assumes well_scoped: "((v⇩1,p⇩1),(v⇩2,p⇩2)) ∈ edges ⟹ hyps (nodeOf v⇩1) p⇩1 = Some p' ⟹ (v⇩2,p⇩2) = (v⇩1,p') ∨ v⇩2 ∈ scope (v⇩1,p')"

context Scoped_Graph
begin

definition hyps_free where
  "hyps_free pth = (∀ v⇩1 p⇩1 v⇩2 p⇩2. ((v⇩1,p⇩1),(v⇩2,p⇩2)) ∈ set pth ⟶ hyps (nodeOf v⇩1) p⇩1 = None)"

lemma hyps_free_Nil[simp]: "hyps_free []" by (simp add: hyps_free_def)

lemma hyps_free_Cons[simp]: "hyps_free (e#pth) ⟷ hyps_free pth ∧ hyps (nodeOf (fst (fst e))) (snd (fst e)) = None"
  by (auto simp add: hyps_free_def) (metis prod.collapse)

lemma path_vertices_shift:
  assumes "path v v' pth"
  shows "map fst (map fst pth)@[v'] = v#map fst (map snd pth)"
using assms by induction auto

inductive terminal_path where
    terminal_path_empty: "terminal_vertex v ⟹ terminal_path v v []" |
    terminal_path_cons: "((v⇩1,p⇩1),(v⇩2,p⇩2)) ∈ edges ⟹ terminal_path v⇩2 v' pth ⟹ hyps (nodeOf v⇩1) p⇩1 = None ⟹ terminal_path v⇩1 v' (((v⇩1,p⇩1),(v⇩2,p⇩2))#pth)"

lemma terminal_path_is_path:
  assumes "terminal_path v v' pth"
  shows "path v v' pth"
using assms by induction (auto simp add: path_cons_simp)

lemma terminal_path_is_hyps_free:
  assumes "terminal_path v v' pth"
  shows "hyps_free pth"
using assms by induction (auto simp add: hyps_free_def)

lemma terminal_path_end_is_terminal:
  assumes "terminal_path v v' pth"
  shows "terminal_vertex v'"
using assms by induction

lemma terminal_pathI:
  assumes "path v v' pth"
  assumes "hyps_free pth"
  assumes "terminal_vertex v'"
  shows "terminal_path v v' pth"
using assms
by induction (auto intro: terminal_path.intros)
end

text ‹An acyclic graph is one where there are no non-trivial cyclic paths (disregarding
edges that are local hypotheses -- these are naturally and benignly cyclic).›

locale Acyclic_Graph = Scoped_Graph +
  assumes hyps_free_acyclic: "path v v pth ⟹ hyps_free pth ⟹ pth = []"
begin
lemma hyps_free_vertices_distinct:
  assumes "terminal_path v v' pth"
  shows "distinct (map fst (map fst pth)@[v'])"
using assms
proof(induction v v' pth)
  case terminal_path_empty
  show ?case by simp
next
  case (terminal_path_cons v⇩1 p⇩1 v⇩2 p⇩2 v' pth)
  note terminal_path_cons.IH
  moreover
  have "v⇩1 ∉ fst ` fst ` set pth"
  proof
    assume "v⇩1 ∈ fst ` fst ` set pth"
    then obtain pth1 e' pth2 where "pth = pth1@[e']@pth2" and "v⇩1 = fst (fst e')"
      apply (atomize_elim)
      apply (induction pth)
      apply (solves simp)
      apply (auto)
      apply (solves ‹rule exI[where x = "[]"]; simp›)
      apply (metis Cons_eq_appendI image_eqI prod.sel(1))
      done
    with terminal_path_is_path[OF ‹terminal_path v⇩2 v' pth›]
    have "path v⇩2 v⇩1 pth1" by (simp add:  path_split2 edge_begin_tup)
    with ‹((v⇩1, p⇩1), (v⇩2, p⇩2)) ∈ _›
    have "path v⇩1 v⇩1 (((v⇩1, p⇩1), (v⇩2, p⇩2)) # pth1)" by (simp add: path_cons_simp)
    moreover
    from terminal_path_is_hyps_free[OF ‹terminal_path v⇩2 v' pth›]
         ‹hyps (nodeOf v⇩1) p⇩1 = None›
         ‹pth = pth1@[e']@pth2›
    have "hyps_free(((v⇩1, p⇩1), (v⇩2, p⇩2)) # pth1)"
      by (auto simp add: hyps_free_def)
    ultimately
    show False  using hyps_free_acyclic by blast
  qed
  moreover
  have "v⇩1 ≠ v'"
    using hyps_free_acyclic path_cons terminal_path_cons.hyps(1) terminal_path_cons.hyps(2) terminal_path_cons.hyps(3) terminal_path_is_hyps_free terminal_path_is_path by fastforce
  ultimately
  show ?case by (auto simp add: comp_def)
qed

lemma hyps_free_vertices_distinct':
  assumes "terminal_path v v' pth"
  shows "distinct (v # map fst (map snd pth))"
  using hyps_free_vertices_distinct[OF assms]
  unfolding path_vertices_shift[OF terminal_path_is_path[OF assms]]
  .

lemma hyps_free_limited:
  assumes "terminal_path v v' pth"
  shows "length pth ≤ fcard vertices"
proof-
  have "length pth = length (map fst (map fst pth))" by simp
  also
  from hyps_free_vertices_distinct[OF assms]
  have "distinct (map fst (map fst pth))" by simp
  hence "length (map fst (map fst pth)) = card (set (map fst (map fst pth)))"
    by (rule distinct_card[symmetric])
  also have "… ≤ card (fset vertices)"
  proof (rule card_mono[OF finite_fset])    
    from assms(1) 
    show "set (map fst (map fst pth)) ⊆ fset vertices"
      by (induction v v' pth) (auto, metis valid_edges case_prodD valid_out_port.simps)
  qed
  also have "… = fcard vertices" by (simp add: fcard.rep_eq)
  finally show ?thesis.
qed

lemma hyps_free_path_not_in_scope:
  assumes "terminal_path v t pth"
  assumes "(v',p') ∈ snd ` set pth"
  shows   "v' ∉ scope (v, p)"
proof
  assume "v' ∈ scope (v,p)"

  from ‹(v',p') ∈ snd ` set pth›
  obtain pth1 pth2 e  where "pth = pth1@[e]@pth2" and "snd e = (v',p')" by (rule snd_set_split)
  from terminal_path_is_path[OF assms(1), unfolded ‹pth = _ ›] ‹snd e = _›
  have "path v v' (pth1@[e])" and "path v' t pth2" unfolding path_split by (auto simp add: edge_end_tup)
  
  from ‹v' ∈ scope (v,p)› terminal_path_end_is_terminal[OF assms(1)] ‹path v' t pth2›
  have "(v,p) ∈ snd ` set pth2" by (rule scope_find)
  then obtain pth2a e' pth2b  where "pth2 = pth2a@[e']@pth2b" and "snd e' = (v,p)"  by (rule snd_set_split)
  from ‹path v' t pth2›[unfolded ‹pth2 = _ ›] ‹snd e' = _›
  have "path v' v (pth2a@[e'])" and "path v t pth2b" unfolding path_split by (auto simp add: edge_end_tup)
  
  from ‹path v v' (pth1@[e])› ‹path v' v (pth2a@[e'])›
  have "path v v ((pth1@[e])@(pth2a@[e']))" by (rule path_appendI)
  moreover
  from terminal_path_is_hyps_free[OF assms(1)] ‹pth = _› ‹pth2 = _›
  have "hyps_free ((pth1@[e])@(pth2a@[e']))" by (auto simp add: hyps_free_def)
  ultimately
  have "((pth1@[e])@(pth2a@[e'])) = []" by (rule hyps_free_acyclic)
  thus False by simp
qed

end

text ‹A saturated graph is one where every input port is incident to an edge.›

locale Saturated_Graph = Port_Graph +
  assumes saturated: "valid_in_port (v,p) ⟹ ∃ e ∈ edges . snd e = (v,p)"

text ‹These four conditions make up a well-shaped graph.›

locale Well_Shaped_Graph =  Well_Scoped_Graph + Acyclic_Graph + Saturated_Graph + Pruned_Port_Graph

text ‹Next we demand an instantiation. This consists of a unique natural number per vertex,
in order to rename the local constants apart, and furthermore a substitution per block
which instantiates the schematic formulas given in @{term Labeled_Signature}.›

locale Instantiation =
  Vertex_Graph nodes _ _ vertices _ +
  Labeled_Signature nodes  _ _ _ labelsIn labelsOut +
  Abstract_Formulas freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP
  for nodes :: "'node stream" and edges :: "('vertex, 'outPort, 'inPort) edge set" and vertices :: "'vertex fset" and labelsIn :: "'node ⇒ 'inPort ⇒ 'form" and labelsOut :: "'node ⇒ 'outPort ⇒ 'form" 
  and  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" +
  fixes vidx :: "'vertex ⇒ nat"
    and inst :: "'vertex ⇒ 'subst"
  assumes vidx_inj: "inj_on vidx (fset vertices)"
begin
  definition labelAtIn :: "'vertex ⇒ 'inPort ⇒ 'form"  where
    "labelAtIn v p = subst (inst v) (freshen (vidx v) (labelsIn (nodeOf v) p))"
  definition labelAtOut :: "'vertex ⇒ 'outPort ⇒ 'form"  where
    "labelAtOut v p = subst (inst v) (freshen (vidx v) (labelsOut (nodeOf v) p))"
end

text ‹A solution is an instantiation where on every edge, both incident ports are labeld with
the same formula.›

locale Solution =
  Instantiation _ _ _ _ _ edges for edges :: "(('vertex × 'outPort) × 'vertex × 'inPort) set" +
  assumes solved: "((v⇩1,p⇩1),(v⇩2,p⇩2)) ∈ edges ⟹ labelAtOut v⇩1 p⇩1 = labelAtIn v⇩2 p⇩2"

locale Proof_Graph =  Well_Shaped_Graph + Solution

text ‹If we have locally scoped constants, we demand that only blocks in the scope of the 
corresponding input port may mention such a locally scoped variable in its substitution.›

locale Well_Scoped_Instantiation =
   Pre_Port_Graph  nodes inPorts outPorts vertices nodeOf edges +
   Instantiation  inPorts outPorts nodeOf hyps nodes edges  vertices labelsIn labelsOut freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP vidx inst +
   Port_Graph_Signature_Scoped_Vars nodes inPorts outPorts freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP local_vars
   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 inPorts :: "'node ⇒ 'inPort fset" 
    and outPorts :: "'node ⇒ 'outPort fset" 
    and nodeOf :: "'vertex ⇒ 'node" 
    and hyps :: "'node ⇒ 'outPort ⇒ 'inPort option" 
    and nodes :: "'node stream" 
    and vertices :: "'vertex fset" 
    and labelsIn :: "'node ⇒ 'inPort ⇒ 'form" 
    and labelsOut :: "'node ⇒ 'outPort ⇒ 'form" 
    and vidx :: "'vertex ⇒ nat" 
    and inst :: "'vertex ⇒ 'subst" 
    and edges :: "('vertex, 'outPort, 'inPort) edge set" 
    and local_vars :: "'node ⇒ 'inPort ⇒ 'var set" +
  assumes well_scoped_inst:
    "valid_in_port (v,p) ⟹
     var ∈ local_vars (nodeOf v) p ⟹
     v' |∈| vertices ⟹
     freshenLC (vidx v) var ∈ subst_lconsts (inst v') ⟹
     v' ∈ scope (v,p)"
begin
  lemma out_of_scope: "valid_in_port (v,p) ⟹ v' |∈| vertices ⟹ v' ∉ scope (v,p) ⟹ freshenLC (vidx v) ` local_vars (nodeOf v) p ∩ subst_lconsts (inst v') = {}"
    using well_scoped_inst by auto
end

text ‹The following locale assembles all these conditions.›
  
locale Scoped_Proof_Graph =
  Instantiation  inPorts outPorts nodeOf hyps nodes edges  vertices labelsIn labelsOut freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP vidx inst +
  Well_Shaped_Graph  nodes inPorts outPorts vertices nodeOf edges hyps  +
  Solution inPorts outPorts nodeOf hyps nodes vertices  labelsIn labelsOut freshenLC renameLCs lconsts closed subst subst_lconsts subst_renameLCs anyP vidx inst edges +
  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
   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 inPorts :: "'node ⇒ 'inPort fset" 
    and outPorts :: "'node ⇒ 'outPort fset" 
    and nodeOf :: "'vertex ⇒ 'node" 
    and hyps :: "'node ⇒ 'outPort ⇒ 'inPort option" 
    and nodes :: "'node stream" 
    and vertices :: "'vertex fset" 
    and labelsIn :: "'node ⇒ 'inPort ⇒ 'form" 
    and labelsOut :: "'node ⇒ 'outPort ⇒ 'form" 
    and vidx :: "'vertex ⇒ nat" 
    and inst :: "'vertex ⇒ 'subst" 
    and edges :: "('vertex, 'outPort, 'inPort) edge  set" 
    and local_vars :: "'node ⇒ 'inPort ⇒ 'var set"

end