# 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 notin_fset 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 notin_fset 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 ∈ _›
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 ∈ _›
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)"
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 notin_fset 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
```