Theory Incredible_Correctness
theory Incredible_Correctness
imports
Abstract_Rules_To_Incredible
Natural_Deduction
begin
text ‹
In this theory, we prove that if we have a graph that proves a given abstract task (which is
represented as the context @{term Tasked_Proof_Graph}), then we can prove @{term solved}.
›
context Tasked_Proof_Graph
begin
definition adjacentTo :: "'vertex ⇒ ('form, 'var) in_port ⇒ ('vertex × ('form, 'var) out_port)" where
"adjacentTo v p = (SOME ps. (ps, (v,p)) ∈ edges)"
fun isReg where
"isReg v p = (case p of Hyp h c ⇒ False | Reg c ⇒
(case nodeOf v of
Conclusion a ⇒ False
| Assumption a ⇒ False
| Rule r ⇒ True
| Helper ⇒ True
))"
fun toNatRule where
"toNatRule v p = (case p of Hyp h c ⇒ Axiom | Reg c ⇒
(case nodeOf v of
Conclusion a ⇒ Axiom
| Assumption a ⇒ Axiom
| Rule r ⇒ NatRule (r,c)
| Helper ⇒ Cut
))"
inductive_set global_assms' :: "'var itself ⇒ 'form set" for i where
"v |∈| vertices ⟹ nodeOf v = Assumption p ⟹ labelAtOut v (Reg p) ∈ global_assms' i"
lemma finite_global_assms': "finite (global_assms' i)"
proof-
have "finite (fset vertices)" by (rule finite_fset)
moreover
have "global_assms' i ⊆ (λ v. case nodeOf v of Assumption p ⇒ labelAtOut v (Reg p)) ` fset vertices"
by (force simp add: global_assms'.simps image_iff )
ultimately
show ?thesis by (rule finite_surj)
qed
context includes fset.lifting
begin
lift_definition global_assms :: "'var itself ⇒ 'form fset" is global_assms' by (rule finite_global_assms')
lemmas global_assmsI = global_assms'.intros[Transfer.transferred]
lemmas global_assms_simps = global_assms'.simps[Transfer.transferred]
end
:: "('vertex × ('form, 'var) in_port) ⇒ 'form fset" where
"extra_assms (v, p) = (λ p. labelAtOut v p) |`| hyps_for (nodeOf v) p"
fun hyps_along :: "('vertex, 'form, 'var) edge' list ⇒ 'form fset" where
"hyps_along pth = ffUnion (extra_assms |`| snd |`| fset_from_list pth) |∪| global_assms TYPE('var)"
lemma hyps_alongE[consumes 1, case_names Hyp Assumption]:
assumes "f |∈| hyps_along pth"
obtains v p h where "(v,p) ∈ snd ` set pth" and "f = labelAtOut v h " and "h |∈| hyps_for (nodeOf v) p"
| v pf where "v |∈| vertices" and "nodeOf v = Assumption pf" "f = labelAtOut v (Reg pf)"
using assms
apply (auto simp add: ffUnion.rep_eq global_assms_simps)
apply (metis image_iff snd_conv)
done
text ‹Here we build the natural deduction tree, by walking the graph.›
primcorec tree :: "'vertex ⇒ ('form, 'var) in_port ⇒ ('vertex, 'form, 'var) edge' list ⇒ (('form entailment), ('rule × 'form) NatRule) dtree" where
"root (tree v p pth) =
((hyps_along ((adjacentTo v p,(v,p))#pth) ⊢ labelAtIn v p),
(case adjacentTo v p of (v', p') ⇒ toNatRule v' p'
))"
| "cont (tree v p pth) =
(case adjacentTo v p of (v', p') ⇒
(if isReg v' p' then ((λ p''. tree v' p'' ((adjacentTo v p,(v,p))#pth)) |`| inPorts (nodeOf v')) else {||}
))"
lemma fst_root_tree[simp]: "fst (root (tree v p pth)) = (hyps_along ((adjacentTo v p,(v,p))#pth) ⊢ labelAtIn v p)" by simp
lemma out_port_cases[consumes 1, case_names Assumption Hyp Rule Helper]:
assumes "p |∈| outPorts n"
obtains
a where "n = Assumption a" and "p = Reg a"
| r h c where "n = Rule r" and "p = Hyp h c"
| r f where "n = Rule r" and "p = Reg f"
| "n = Helper" and "p = Reg anyP"
using assms by (atomize_elim, cases p; cases n) auto
lemma hyps_for_fimage: "hyps_for (Rule r) x = (if x |∈| f_antecedent r then (λ f. Hyp f x) |`| (a_hyps x) else {||})"
apply (rule fset_eqI)
apply (rename_tac p')
apply (case_tac p')
apply (auto simp add: split: if_splits out_port.splits)
done
text ‹Now we prove that the thus produced tree is well-formed.›
theorem wf_tree:
assumes "valid_in_port (v,p)"
assumes "terminal_path v t pth"
shows "wf (tree v p pth)"
using assms
proof (coinduction arbitrary: v p pth)
case (wf v p pth)
let ?t = "tree v p pth"
from saturated[OF wf(1)]
obtain v' p'
where e:"((v',p'),(v,p)) ∈ edges" and [simp]: "adjacentTo v p = (v',p')"
by (auto simp add: adjacentTo_def, metis (no_types, lifting) eq_fst_iff tfl_some)
let ?e = "((v',p'),(v,p))"
let ?pth' = "?e#pth"
let ?Γ = "hyps_along ?pth'"
let ?l = "labelAtIn v p"
from e valid_edges have "v' |∈| vertices" and "p' |∈| outPorts (nodeOf v')" by auto
hence "nodeOf v' ∈ sset nodes" using valid_nodes by (meson image_eqI subsetD)
from ‹?e ∈ edges›
have s: "labelAtOut v' p' = labelAtIn v p" by (rule solved)
from ‹p' |∈| outPorts (nodeOf v')›
show ?case
proof (cases rule: out_port_cases)
case (Hyp r h c)
from Hyp ‹p' |∈| outPorts (nodeOf v')›
have "h |∈| a_hyps c" and "c |∈| f_antecedent r" by auto
hence "hyps (nodeOf v') (Hyp h c) = Some c" using Hyp by simp
from well_scoped[OF ‹ _ ∈ edges›[unfolded Hyp] this]
have "(v, p) = (v', c) ∨ v ∈ scope (v', c)".
hence "(v', c) ∈ insert (v, p) (snd ` set pth)"
proof
assume "(v, p) = (v', c)"
thus ?thesis by simp
next
assume "v ∈ scope (v', c)"
from this terminal_path_end_is_terminal[OF wf(2)] terminal_path_is_path[OF wf(2)]
have "(v', c) ∈ snd ` set pth" by (rule scope_find)
thus ?thesis by simp
qed
moreover
from ‹hyps (nodeOf v') (Hyp h c) = Some c›
have "Hyp h c |∈| hyps_for (nodeOf v') c" by simp
hence "labelAtOut v' (Hyp h c) |∈| extra_assms (v',c)" by auto
ultimately
have "labelAtOut v' (Hyp h c) |∈| ?Γ"
by (fastforce simp add: ffUnion.rep_eq)
hence "labelAtIn v p |∈| ?Γ" by (simp add: s[symmetric] Hyp)
thus ?thesis
using Hyp
apply (auto intro: exI[where x = ?t] simp add: eff.simps simp del: hyps_along.simps)
done
next
case (Assumption f)
from ‹v' |∈| vertices› ‹nodeOf v' = Assumption f›
have "labelAtOut v' (Reg f) |∈| global_assms TYPE('var)"
by (rule global_assmsI)
hence "labelAtOut v' (Reg f) |∈| ?Γ" by auto
hence "labelAtIn v p |∈| ?Γ" by (simp add: s[symmetric] Assumption)
thus ?thesis using Assumption
by (auto intro: exI[where x = ?t] simp add: eff.simps)
next
case (Rule r f)
with ‹nodeOf v' ∈ sset nodes›
have "r ∈ sset rules"
by (auto simp add: nodes_def stream.set_map)
from Rule
have "hyps (nodeOf v') p' = None" by simp
with e ‹terminal_path v t pth›
have "terminal_path v' t ?pth'"..
from Rule ‹p' |∈| outPorts (nodeOf v')›
have "f |∈| f_consequent r" by simp
hence "f ∈ set (consequent r)" by (simp add: f_consequent_def)
with ‹r ∈ sset rules›
have "NatRule (r, f) ∈ sset (smap NatRule n_rules)"
by (auto simp add: stream.set_map n_rules_def no_empty_conclusions)
moreover
{
from ‹f |∈| f_consequent r›
have "f ∈ set (consequent r)" by (simp add: f_consequent_def)
hence "natEff_Inst (r, f) f (f_antecedent r)"
by (rule natEff_Inst.intros)
hence "eff (NatRule (r, f)) (?Γ ⊢ subst (inst v') (freshen (vidx v') f))
((λant. ((λp. subst (inst v') (freshen (vidx v') p)) |`| a_hyps ant |∪| ?Γ ⊢ subst (inst v') (freshen (vidx v') (a_conc ant)))) |`| f_antecedent r)"
(is "eff _ _ ?ants")
proof (rule eff.intros)
fix ant f
assume "ant |∈| f_antecedent r"
from ‹v' |∈| vertices› ‹ant |∈| f_antecedent r›
have "valid_in_port (v',ant)" by (simp add: Rule)
assume "f |∈| ?Γ"
thus "freshenLC (vidx v') ` a_fresh ant ∩ lconsts f = {}"
proof(induct rule: hyps_alongE)
case (Hyp v'' p'' h'')
from Hyp(1) snd_set_path_verties[OF terminal_path_is_path[OF ‹terminal_path v' t ?pth'›]]
have "v'' |∈| vertices" by (force simp add:)
from ‹terminal_path v' t ?pth'› Hyp(1)
have "v'' ∉ scope (v', ant)" by (rule hyps_free_path_not_in_scope)
with ‹valid_in_port (v',ant)› ‹v'' |∈| vertices›
have "freshenLC (vidx v') ` local_vars (nodeOf v') ant ∩ subst_lconsts (inst v'') = {}"
by (rule out_of_scope)
moreover
from hyps_free_vertices_distinct'[OF ‹terminal_path v' t ?pth'›] Hyp.hyps(1)
have "v'' ≠ v'" by (metis distinct.simps(2) fst_conv image_eqI list.set_map)
hence "vidx v'' ≠ vidx v'" using ‹v' |∈| vertices› ‹v'' |∈| vertices› by (meson vidx_inj inj_onD)
hence "freshenLC (vidx v') ` a_fresh ant ∩ freshenLC (vidx v'') ` lconsts (labelsOut (nodeOf v'') h'') = {}"by auto
moreover
have "lconsts f ⊆ lconsts (freshen (vidx v'') (labelsOut (nodeOf v'') h'')) ∪ subst_lconsts (inst v'') " using ‹f = _›
by (simp add: labelAtOut_def fv_subst)
ultimately
show ?thesis
by (fastforce simp add: lconsts_freshen)
next
case (Assumption v pf)
hence "f = subst (inst v) (freshen (vidx v) pf)" by (simp add: labelAtOut_def)
moreover
from Assumption have "Assumption pf ∈ sset nodes" using valid_nodes by auto
hence "pf ∈ set assumptions" unfolding nodes_def by (auto simp add: stream.set_map)
hence "closed pf" by (rule assumptions_closed)
ultimately
have "lconsts f = {}" by (simp add: closed_no_lconsts lconsts_freshen subst_closed freshen_closed)
thus ?thesis by simp
qed
next
fix ant
assume "ant |∈| f_antecedent r"
from ‹v' |∈| vertices› ‹ant |∈| f_antecedent r›
have "valid_in_port (v',ant)" by (simp add: Rule)
moreover
note ‹v' |∈| vertices›
moreover
hence "v' ∉ scope (v', ant)" by (rule scopes_not_refl)
ultimately
have "freshenLC (vidx v') ` local_vars (nodeOf v') ant ∩ subst_lconsts (inst v') = {}"
by (rule out_of_scope)
thus "freshenLC (vidx v') ` a_fresh ant ∩ subst_lconsts (inst v') = {}" by simp
qed
also
have "subst (inst v') (freshen (vidx v') f) = labelAtOut v' p'" using Rule by (simp add: labelAtOut_def)
also
note ‹labelAtOut v' p' = labelAtIn v p›
also
have "?ants = ((λx. (extra_assms (v',x) |∪| hyps_along ?pth' ⊢ labelAtIn v' x)) |`| f_antecedent r)"
by (rule fimage_cong[OF refl])
(auto simp add: labelAtIn_def labelAtOut_def Rule hyps_for_fimage ffUnion.rep_eq)
finally
have "eff (NatRule (r, f))
(?Γ, labelAtIn v p)
((λx. extra_assms (v',x) |∪| ?Γ ⊢ labelAtIn v' x) |`| f_antecedent r)".
}
moreover
{ fix x
assume "x |∈| cont ?t"
then obtain a where "x = tree v' a ?pth'" and "a |∈| f_antecedent r"
by (auto simp add: Rule)
note this(1)
moreover
from ‹v' |∈| vertices› ‹a |∈| f_antecedent r›
have "valid_in_port (v',a)" by (simp add: Rule)
moreover
note ‹terminal_path v' t ?pth'›
ultimately
have "∃v p pth. x = tree v p pth ∧ valid_in_port (v,p) ∧ terminal_path v t pth"
by blast
}
ultimately
show ?thesis using Rule
by (auto intro!: exI[where x = ?t] simp add: comp_def funion_assoc)
next
case Helper
from Helper
have "hyps (nodeOf v') p' = None" by simp
with e ‹terminal_path v t pth›
have "terminal_path v' t ?pth'"..
have "labelAtIn v' (plain_ant anyP) = labelAtIn v p"
unfolding s[symmetric]
using Helper by (simp add: labelAtIn_def labelAtOut_def)
moreover
{ fix x
assume "x |∈| cont ?t"
hence "x = tree v' (plain_ant anyP) ?pth'"
by (auto simp add: Helper)
note this(1)
moreover
from ‹v' |∈| vertices›
have "valid_in_port (v',plain_ant anyP)" by (simp add: Helper)
moreover
note ‹terminal_path v' t ?pth'›
ultimately
have "∃v p pth. x = tree v p pth ∧ valid_in_port (v,p) ∧ terminal_path v t pth"
by blast
}
ultimately
show ?thesis using Helper
by (auto intro!: exI[where x = ?t] simp add: comp_def funion_assoc )
qed
qed
lemma global_in_ass: "global_assms TYPE('var) |⊆| ass_forms"
proof
fix x
assume "x |∈| global_assms TYPE('var)"
then obtain v pf where "v |∈| vertices" and "nodeOf v = Assumption pf" and "x = labelAtOut v (Reg pf)"
by (auto simp add: global_assms_simps)
from this (1,2) valid_nodes
have "Assumption pf ∈ sset nodes" by (auto simp add:)
hence "pf ∈ set assumptions" by (auto simp add: nodes_def stream.set_map)
hence "closed pf" by (rule assumptions_closed)
with ‹x = labelAtOut v (Reg pf)›
have "x = pf" by (auto simp add: labelAtOut_def lconsts_freshen closed_no_lconsts freshen_closed subst_closed)
thus "x |∈| ass_forms" using ‹pf ∈ set assumptions› by (auto simp add: ass_forms_def)
qed
primcorec edge_tree :: "'vertex ⇒ ('form, 'var) in_port ⇒ ('vertex, 'form, 'var) edge' tree" where
"root (edge_tree v p) = (adjacentTo v p, (v,p))"
| "cont (edge_tree v p) =
(case adjacentTo v p of (v', p') ⇒
(if isReg v' p' then ((λ p. edge_tree v' p) |`| inPorts (nodeOf v')) else {||}
))"
lemma tfinite_map_tree: "tfinite (map_tree f t) ⟷ tfinite t"
proof
assume "tfinite (map_tree f t)"
thus "tfinite t"
by (induction "map_tree f t" arbitrary: t rule: tfinite.induct)
(fastforce intro: tfinite.intros simp add: tree.map_sel)
next
assume "tfinite t"
thus "tfinite (map_tree f t)"
by (induction t rule: tfinite.induct)
(fastforce intro: tfinite.intros simp add: tree.map_sel)
qed
lemma finite_tree_edge_tree:
"tfinite (tree v p pth) ⟷ tfinite (edge_tree v p)"
proof-
have "map_tree (λ _. ()) (tree v p pth) = map_tree (λ _. ()) (edge_tree v p)"
by(coinduction arbitrary: v p pth)
(fastforce simp add: tree.map_sel rel_fset_def rel_set_def split: prod.split out_port.split graph_node.split option.split)
thus ?thesis by (metis tfinite_map_tree)
qed
coinductive forbidden_path :: "'vertex ⇒ ('vertex, 'form, 'var) edge' stream ⇒ bool" where
forbidden_path: "((v⇩1,p⇩1),(v⇩2,p⇩2)) ∈ edges ⟹ hyps (nodeOf v⇩1) p⇩1 = None ⟹ forbidden_path v⇩1 pth ⟹ forbidden_path v⇩2 (((v⇩1,p⇩1),(v⇩2,p⇩2))##pth)"
lemma path_is_forbidden:
assumes "valid_in_port (v,p)"
assumes "ipath (edge_tree v p) es"
shows "forbidden_path v es"
using assms
proof(coinduction arbitrary: v p es)
case forbidden_path
let ?es' = "stl es"
from forbidden_path(2)
obtain t' where "root (edge_tree v p) = shd es" and "t' |∈| cont (edge_tree v p)" and "ipath t' ?es'"
by rule blast
from ‹root (edge_tree v p) = shd es›
have [simp]: "shd es = (adjacentTo v p, (v,p))" by simp
from saturated[OF ‹valid_in_port (v,p)›]
obtain v' p'
where e:"((v',p'),(v,p)) ∈ edges" and [simp]: "adjacentTo v p = (v',p')"
by (auto simp add: adjacentTo_def, metis (no_types, lifting) eq_fst_iff tfl_some)
let ?e = "((v',p'),(v,p))"
from e have "p' |∈| outPorts (nodeOf v')" using valid_edges by auto
thus ?case
proof(cases rule: out_port_cases)
case Hyp
with ‹t' |∈| cont (edge_tree v p)›
have False by auto
thus ?thesis..
next
case Assumption
with ‹t' |∈| cont (edge_tree v p)›
have False by auto
thus ?thesis..
next
case (Rule r f)
from ‹t' |∈| cont (edge_tree v p)› Rule
obtain a where [simp]: "t' = edge_tree v' a" and "a |∈| f_antecedent r" by auto
have "es = ?e ## ?es'" by (cases es rule: stream.exhaust_sel) simp
moreover
have "?e ∈ edges" using e by simp
moreover
from ‹p' = Reg f› ‹nodeOf v' = Rule r›
have "hyps (nodeOf v') p' = None" by simp
moreover
from e valid_edges have "v' |∈| vertices" by auto
with ‹nodeOf v' = Rule r› ‹a |∈| f_antecedent r›
have "valid_in_port (v', a)" by simp
moreover
have "ipath (edge_tree v' a) ?es'" using ‹ipath t' _› by simp
ultimately
show ?thesis by metis
next
case Helper
from ‹t' |∈| cont (edge_tree v p)› Helper
have [simp]: "t' = edge_tree v' (plain_ant anyP)" by simp
have "es = ?e ## ?es'" by (cases es rule: stream.exhaust_sel) simp
moreover
have "?e ∈ edges" using e by simp
moreover
from ‹p' = Reg anyP› ‹nodeOf v' = Helper›
have "hyps (nodeOf v') p' = None" by simp
moreover
from e valid_edges have "v' |∈| vertices" by auto
with ‹nodeOf v' = Helper›
have "valid_in_port (v', plain_ant anyP)" by simp
moreover
have "ipath (edge_tree v' (plain_ant anyP)) ?es'" using ‹ipath t' _› by simp
ultimately
show ?thesis by metis
qed
qed
lemma forbidden_path_prefix_is_path:
assumes "forbidden_path v es"
obtains v' where "path v' v (rev (stake n es))"
using assms
apply (atomize_elim)
apply (induction n arbitrary: v es)
apply simp
apply (simp add: path_snoc)
apply (subst (asm) (2) forbidden_path.simps)
apply auto
done
lemma forbidden_path_prefix_is_hyp_free:
assumes "forbidden_path v es"
shows "hyps_free (rev (stake n es))"
using assms
apply (induction n arbitrary: v es)
apply (simp add: hyps_free_def)
apply (subst (asm) (2) forbidden_path.simps)
apply (force simp add: hyps_free_def)
done
text ‹And now we prove that the tree is finite, which requires the above notion of a
@{term forbidden_path}, i.e.\@ an infinite path.›
theorem finite_tree:
assumes "valid_in_port (v,p)"
assumes "terminal_vertex v"
shows "tfinite (tree v p pth)"
proof(rule ccontr)
let ?n = "Suc (fcard vertices)"
assume "¬ tfinite (tree v p pth)"
hence "¬ tfinite (edge_tree v p)" unfolding finite_tree_edge_tree.
then obtain es :: "('vertex, 'form, 'var) edge' stream"
where "ipath (edge_tree v p) es" using Konig by blast
with ‹valid_in_port (v,p)›
have "forbidden_path v es" by (rule path_is_forbidden)
from forbidden_path_prefix_is_path[OF this] forbidden_path_prefix_is_hyp_free[OF this]
obtain v' where "path v' v (rev (stake ?n es))" and "hyps_free (rev (stake ?n es))"
by blast
from this ‹terminal_vertex v›
have "terminal_path v' v (rev (stake ?n es))" by (rule terminal_pathI)
hence "length (rev (stake ?n es)) ≤ fcard vertices"
by (rule hyps_free_limited)
thus False by simp
qed
text ‹The main result of this theory.›
theorem solved
unfolding solved_def
proof(intro ballI allI conjI impI)
fix c
assume "c |∈| conc_forms"
hence "c ∈ set conclusions" by (auto simp add: conc_forms_def)
from this(1) conclusions_present
obtain v where "v |∈| vertices" and "nodeOf v = Conclusion c"
by auto
have "valid_in_port (v, (plain_ant c))"
using ‹v |∈| vertices› ‹nodeOf _ = _ › by simp
have "terminal_vertex v" using ‹v |∈| vertices› ‹nodeOf v = Conclusion c› by auto
let ?t = "tree v (plain_ant c) []"
have "fst (root ?t) = (global_assms TYPE('var), c)"
using ‹c ∈ set conclusions› ‹nodeOf _ = _›
by (auto simp add: labelAtIn_def conclusions_closed closed_no_lconsts freshen_def rename_closed subst_closed)
moreover
have "global_assms TYPE('var) |⊆| ass_forms" by (rule global_in_ass)
moreover
from ‹terminal_vertex v›
have "terminal_path v v []" by (rule terminal_path_empty)
with ‹valid_in_port (v, (plain_ant c))›
have "wf ?t" by (rule wf_tree)
moreover
from ‹valid_in_port (v, plain_ant c)› ‹terminal_vertex v›
have "tfinite ?t" by (rule finite_tree)
ultimately
show "∃Γ t. fst (root t) = (Γ ⊢ c) ∧ Γ |⊆| ass_forms ∧ wf t ∧ tfinite t" by blast
qed
end
end