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 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)"
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: 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 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 v⇩1 p⇩1 v⇩2 p⇩2 p'
assume assms: "((v⇩1, p⇩1), (v⇩2, p⇩2)) ∈ edges" "hyps (nodeOf v⇩1) p⇩1 = Some p'"
from assms(1) hyps_correct[OF assms(2)]
have "valid_out_port (v⇩1, p⇩1)" and "valid_in_port (v⇩2, p⇩2)" and "valid_in_port (v⇩1, p')" and "v⇩2 |∈| vertices"
using valid_edges by auto
from assms
have "∃ i. fst v⇩1 = fst v⇩2 ∧ prefix (snd v⇩1@[i]) (snd v⇩2) ∧ p' = in_port_at v⇩1 i"
by (cases v⇩1; cases v⇩2; auto elim!: edge_step)
hence "scope' v⇩1 p' v⇩2"
unfolding scope_valid_inport[OF ‹v⇩2 |∈| vertices›].
hence "v⇩2 ∈ scope (v⇩1, p')"
unfolding in_scope[OF ‹valid_in_port (v⇩1, p')›].
thus "(v⇩2, p⇩2) = (v⇩1, p') ∨ v⇩2 ∈ scope (v⇩1, 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 v⇩1 p⇩1 v⇩2 p⇩2
assume "((v⇩1, p⇩1), (v⇩2, p⇩2)) ∈ edges"
thus "labelAtOut v⇩1 p⇩1 = labelAtIn v⇩2 p⇩2"
proof(cases rule:edges.cases)
case (regular_edge c "is")
from ‹((v⇩1, p⇩1), v⇩2, p⇩2) = edge_at c is›
have "(v⇩1,p⇩1) = edge_from c is" using fst_edge_at by (metis fst_conv)
hence [simp]: "v⇩1 = (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 v⇩1 p⇩1 = subst (iSubst ?t') (freshen (vidx v⇩1) (iOutPort ?t'))"
using regular_edge Nil by (simp add: labelAtOut_def edge_at_def edge_from_def)
also have "vidx v⇩1 = 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 v⇩2 p⇩2"
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 v⇩1 p⇩1 = subst (iSubst ?t1) (freshen (vidx v⇩1) (iOutPort ?t1))"
using regular_edge snoc by (simp add: labelAtOut_def edge_at_def edge_from_def)
also have "vidx v⇩1 = 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 v⇩2 p⇩2"
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 ‹((v⇩1, p⇩1), v⇩2, p⇩2) = hyp_edge_at c is n s›
have "(v⇩1,p⇩1) = hyp_edge_from c is n s" using fst_hyp_edge_at by (metis fst_conv)
hence [simp]: "v⇩1 = (c, 0 # ?his)" by (simp add: hyp_edge_from_def)
have "labelAtOut v⇩1 p⇩1 = subst (iSubst ?t1) (freshen (vidx v⇩1) (labelsOut (iNodeOf ?t1) ?h))"
using hyp_edge by (simp add: hyp_edge_at_def hyp_edge_from_def labelAtOut_def)
also have "vidx v⇩1 = 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 v⇩2 p⇩2"
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..
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"
by (rule imageI)
hence "Conclusion c ∈ nodeOf ` fset vertices" by simp
} thus ?thesis by auto
qed
qed
end
end