```theory Incredible_Predicate_Tasks
imports
Incredible_Completeness
Incredible_Predicate
"HOL-Eisbach.Eisbach"
begin

declare One_nat_def [simp del]

context ND_Rules_Inst begin
lemma eff_NatRuleI:
"nat_rule rule c ants
⟹ entail = (Γ ⊢ subst s (freshen a c))
⟹ hyps = ((λant. ((λp. subst s (freshen a p)) |`| a_hyps ant |∪| Γ ⊢ subst s (freshen a (a_conc ant)))) |`| ants)
⟹ (⋀ ant f. ant |∈| ants ⟹ f |∈| Γ ⟹ freshenLC a ` (a_fresh ant) ∩ lconsts f = {})
⟹ (⋀ ant. ant |∈| ants ⟹ freshenLC a ` (a_fresh ant) ∩ subst_lconsts s = {})
⟹ eff (NatRule rule) entail hyps"
by (drule eff.intros(2)) simp_all
end

lemma  natEff_InstI:
"rule = (r,c)
⟹ c ∈ set (consequent r)
⟹ antec = f_antecedent r
⟹ natEff_Inst rule c antec"
by (metis natEff_Inst.intros)
end

context begin

text ‹A typical task with local constants:: ‹∀x. Q x ⟶ Q x››

"curry to_nat :: nat ⇒ var ⇒ var"
map_lc
lc
"closed"
subst
lc_subst
map_lc_subst
"Var 0 []"
antecedent
consequent
prop_rules
"[]"
"[ForallX (imp (Q x) (Q x))]"
by unfold_locales auto

text ‹Then we show, that this task has a proof within our formalization of natural deduction
by giving a concrete proof tree.›

abbreviation lx :: "nat" where "lx ≡ to_nat (1::nat,0::nat)"

abbreviation base_tree :: "((form fset × form) × (prop_rule × form) NatRule) tree" where
"base_tree ≡ Node ({|Q (LC lx)|} ⊢ Q (LC lx), Axiom) {||}"

abbreviation imp_tree :: "((form fset × form) × (prop_rule × form) NatRule) tree" where
"imp_tree ≡ Node ({||} ⊢ imp (Q (LC lx)) (Q (LC lx)), NatRule (impI, imp X Y)) {|base_tree|}"

abbreviation solution_tree :: "((form fset × form) × (prop_rule × form) NatRule) tree" where
"solution_tree ≡ Node ({||} ⊢ ForallX (imp (Q x) (Q x)), NatRule (allI, ForallX (P x))) {|imp_tree|}"

abbreviation s1 where "s1 ≡ [(12, ([9], imp (Q x) (Q x)))] "
abbreviation s2 where "s2 ≡ [(10, ([], Q (LC lx))), (11, ([], Q (LC lx)))] "

lemma fv_subst_s1[simp]: "fv_subst s1 = {}"

lemma subst1_simps[simp]:
"subst s1 (P (LC n)) = imp (Q (LC n)) (Q (LC n))"
"subst s1 (ForallX (P x)) = ForallX (imp (Q x) (Q x))"
by simp_all

lemma subst2_simps[simp]:
"subst s2 X = Q (LC lx)"
"subst s2 Y = Q (LC lx)"
"subst s2 (imp X Y) = imp (subst s2 X) (subst s2 Y)"
by simp_all

lemma substI1: "ForallX (imp (Q x) (Q x)) = subst s1 (predicate.freshen 1 (ForallX (P x)))"
by (auto simp add: predicate.freshen_def Let_def)

lemma substI2: "imp (Q (LC lx)) (Q (LC lx)) = subst s2 (predicate.freshen 2 (imp X Y))"
by (auto simp add: predicate.freshen_def Let_def)

declare subst.simps[simp del]

apply clarsimp
apply (rule_tac x="{||}" in exI)
apply clarsimp
apply (rule_tac x="solution_tree" in exI)
apply clarsimp
apply (rule conjI)

apply clarsimp
apply clarsimp
apply (rule conjI)
apply (solves ‹simp›)
apply (solves ‹rule substI1›)
apply (subst antecedent.sel(2))
apply (solves ‹simp›)
apply (solves ‹simp›)
apply (solves ‹simp›)
apply simp

apply clarsimp
apply clarsimp
apply (rule conjI)
apply (solves ‹simp›)
apply (solves ‹rule substI2›)
apply (solves ‹simp add: predicate.f_antecedent_def predicate.freshen_def›)
apply (solves ‹simp›)
apply simp

apply (solves ‹(rule tfinite.intros, simp)+›)
done

abbreviation vertices where "vertices ≡ {|0::nat,1,2 |}"
fun nodeOf  where
"nodeOf n = [Conclusion (ForallX (imp (Q x) (Q x))),
Rule allI,
Rule impI] ! n "

fun inst  where
"inst n = [[],s1,s2] ! n"

abbreviation e1 :: "(nat, form, nat) edge'"
where "e1 ≡ ((1,Reg (ForallX (P x))), (0,plain_ant (ForallX (imp (Q x) (Q x)))))"
abbreviation e2  :: "(nat, form, nat) edge'"
where "e2 ≡ ((2,Reg (imp X Y)), (1,allI_input))"
abbreviation e3  :: "(nat, form, nat) edge'"
where "e3 ≡ ((2,Hyp X (impI_input)), (2,impI_input))"
abbreviation task_edges :: "(nat, form, nat) edge' set" where "task_edges ≡ {e1, e2, e3}"

by standard (auto simp add: predicate.f_consequent_def predicate.f_antecedent_def)

nodeOf
vertices
"curry to_nat :: nat ⇒ var ⇒ var"
map_lc
lc
"closed"
subst
lc_subst
map_lc_subst
"Var 0 []"
"id"
"inst"
by unfold_locales simp

text ‹Finally we can also show that there is a proof graph for this task.›

interpretation Well_Scoped_Graph
vertices
nodeOf
by standard (auto split: if_splits)

lemma no_path_01[simp]: "task.path 0 v pth ⟷ (pth = [] ∧ v = 0)"
lemma no_path_12[simp]: "¬ task.path 1 2 pth"

interpretation Acyclic_Graph
vertices
nodeOf
proof
fix v pth
thus "pth = []"
qed

interpretation Saturated_Graph
vertices
nodeOf
by standard

interpretation Pruned_Port_Graph
vertices
nodeOf
proof
fix v
assume "v |∈| vertices"
hence "∃ pth. task.path v 0 pth"
apply auto
done
moreover
ultimately
show "∃pth v'. task.path v v' pth ∧ task.terminal_vertex v'" by blast
qed

interpretation Well_Shaped_Graph
vertices
..

interpretation Solution
nodeOf
vertices
"curry to_nat :: nat ⇒ var ⇒ var"
map_lc
lc
"closed"
subst
lc_subst
map_lc_subst
"Var 0 []"
id
inst
by standard

interpretation Proof_Graph
vertices
nodeOf
"curry to_nat :: nat ⇒ var ⇒ var"
map_lc
lc
"closed"
subst
lc_subst
map_lc_subst
"Var 0 []"
id
inst
..

lemma path_20:
shows "(1, allI_input) ∈ snd ` set pth"
proof-
{ fix v
hence "v = 0 ∨ v = 1 ∨ (1, allI_input) ∈ snd ` set pth"
by (induction v "0::nat" pth rule: task.path.induct) auto
}
from this[OF assms]
show ?thesis by auto
qed

lemma scope_21: "2 ∈ task.scope (1, allI_input)"

interpretation Scoped_Proof_Graph
"curry to_nat :: nat ⇒ var ⇒ var"
map_lc
lc
"closed"
subst
lc_subst
map_lc_subst
"Var 0 []"
nodeOf
vertices
id
inst
by standard (auto simp add: predicate.f_antecedent_def scope_21)

"curry to_nat :: nat ⇒ var ⇒ var"
map_lc
lc
"closed"
subst
lc_subst
map_lc_subst
"Var 0 []"
antecedent
consequent
prop_rules
"[]"
"[ForallX (imp (Q x) (Q x))]"
vertices
nodeOf