# 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}.
›

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 ― ‹a lie›
| 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 fmember.rep_eq 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

fun extra_assms :: "('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: fmember.rep_eq ffUnion.rep_eq  global_assms_simps[unfolded fmember.rep_eq])
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')"

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 notin_fset 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: fmember.rep_eq ffUnion.rep_eq)

hence "labelAtIn v p |∈| ?Γ" by (simp add: s[symmetric] Hyp fmember.rep_eq)
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 fmember.rep_eq)
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: fmember.rep_eq)

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 notin_fset)
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 = _›
ultimately
show ?thesis
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 simp add: fmember.rep_eq)
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 fmember.rep_eq 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"
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'"
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)"
from this (1,2) valid_nodes
have "Assumption pf ∈ sset nodes" by (auto simp add: fmember.rep_eq)
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')"
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 (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 (subst (asm) (2) forbidden_path.simps)
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, metis (no_types, lifting) image_iff image_subset_iff notin_fset)

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```