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