# Theory Build_Incredible_Tree

```theory Build_Incredible_Tree
imports Incredible_Trees Natural_Deduction
begin

text ‹
This theory constructs an incredible tree (with freshness checked only locally) from a natural
deduction tree.
›

lemma image_eq_to_f:
assumes  "f1 ` S1 = f2 ` S2"
obtains f where "⋀ x. x ∈ S2 ⟹ f x ∈ S1 ∧ f1 (f x) = f2 x"
proof (atomize_elim)
from assms
have "∀x. x ∈ S2 ⟶ (∃ y. y ∈ S1 ∧ f1 y = f2 x)" by (metis image_iff)
thus "∃f. ∀x. x ∈ S2 ⟶ f x ∈ S1 ∧ f1 (f x) = f2 x" by metis
qed

context includes fset.lifting
begin
lemma fimage_eq_to_f:
assumes  "f1 |`| S1 = f2 |`| S2"
obtains f where "⋀ x. x |∈| S2 ⟹ f x |∈| S1 ∧ f1 (f x) = f2 x"
using assms apply transfer using image_eq_to_f by metis
end

begin

lemma build_local_iwf:
fixes t :: "('form entailment × ('rule × 'form) NatRule) tree"
assumes "tfinite t"
assumes "wf t"
shows "∃ it. local_iwf it (fst (root t))"
using assms
proof(induction)
case (tfinite t)
from ‹wf t›
have "snd (root t) ∈ R" using wf.simps by blast

from ‹wf t›
have "eff (snd (root t)) (fst (root t)) ((fst ∘ root) |`| cont t)" using wf.simps by blast

from ‹wf t›
have "⋀ t'. t' |∈| cont t ⟹ wf t'" using wf.simps by blast
hence IH: "⋀ Γ' t'. t' |∈| cont t ⟹ (∃it'. local_iwf it' (fst (root t')))" using tfinite(2) by blast
then obtain its where its: "⋀ t'. t' |∈| cont t ⟹ local_iwf (its t') (fst (root t'))" by metis

from ‹eff _ _ _›
show ?case
proof(cases rule: eff.cases[case_names Axiom NatRule Cut])
case (Axiom c Γ)
show ?thesis
proof (cases "c |∈| ass_forms")
case True (* Global assumption *)
then  have "c ∈ set assumptions"  by (auto simp add:  ass_forms_def)

let "?it" = "INode (Assumption c) c undefined undefined [] ::  ('form, 'rule, 'subst, 'var) itree"

from ‹c ∈ set assumptions›
have "local_iwf ?it (Γ ⊢ c)"
by (auto intro!: iwf local_fresh_check.intros)

thus ?thesis unfolding Axiom..
next
case False
obtain s where "subst s anyP = c" by atomize_elim (rule anyP_is_any)
hence [simp]: "subst s (freshen undefined anyP) = c" by (simp add: lconsts_anyP freshen_closed)

let "?it" = "HNode undefined s [] ::  ('form, 'rule, 'subst, 'var) itree"

from  ‹c |∈| Γ› False
have "local_iwf ?it (Γ ⊢ c)" by (auto intro: iwfH)
thus ?thesis unfolding Axiom..
qed
next
case (NatRule rule c ants Γ i s)
from ‹natEff_Inst rule c ants›
have "snd rule = c"  and [simp]: "ants = f_antecedent (fst rule)" and "c ∈ set (consequent (fst rule))"

from ‹(fst ∘ root) |`| cont t = (λant. (λp. subst s (freshen i p)) |`| a_hyps ant |∪| Γ ⊢ subst s (freshen i (a_conc ant))) |`| ants›
obtain to_t where "⋀ ant. ant |∈| ants ⟹ to_t ant |∈| cont t ∧ (fst ∘ root) (to_t ant) = ((λp. subst s (freshen i p)) |`| a_hyps ant |∪| Γ ⊢ subst s (freshen i (a_conc ant)))"
by (rule fimage_eq_to_f) (rule that)
hence to_t_in_cont: "⋀ ant. ant |∈| ants ⟹ to_t ant |∈| cont t"
and to_t_root: "⋀ ant. ant |∈| ants ⟹  fst (root (to_t ant)) = ((λp. subst s (freshen i p)) |`| a_hyps ant |∪| Γ ⊢ subst s (freshen i (a_conc ant)))"
by auto

let ?ants' = "map (λ ant. its (to_t ant)) (antecedent (fst rule))"
let "?it" = "INode (Rule (fst rule)) c i s ?ants' ::  ('form, 'rule, 'subst, 'var) itree"

from ‹snd (root t) ∈ R›
have "fst rule ∈ sset rules"
unfolding NatRule
by (auto simp add: stream.set_map n_rules_def no_empty_conclusions )
moreover
from ‹c ∈ set (consequent (fst rule))›
have "c |∈| f_consequent (fst rule)" by (simp add: f_consequent_def)
moreover
{ fix ant
assume "ant ∈ set (antecedent (fst rule))"
hence "ant |∈| ants" by (simp add: f_antecedent_def)
from its[OF to_t_in_cont[OF this]]
have "local_iwf (its (to_t ant)) (fst (root (to_t ant)))".
also have "fst (root (to_t ant)) =
((λp. subst s (freshen i p)) |`| a_hyps ant |∪| Γ ⊢ subst s (freshen i (a_conc ant)))"
by (rule to_t_root[OF ‹ant |∈| ants›])
also have "… =
((λh. subst s (freshen i (labelsOut (Rule (fst rule)) h))) |`| hyps_for (Rule (fst rule)) ant |∪| Γ
⊢ subst s (freshen i (a_conc ant)))"
using ‹ant |∈| ants›
by auto
finally
have "local_iwf (its (to_t ant))
((λh. subst s (freshen i (labelsOut (Rule (fst rule)) h))) |`| hyps_for (Rule (fst rule)) ant |∪|
Γ  ⊢ subst s (freshen i (a_conc ant)))".
}
moreover
from NatRule(5,6)
have "local_fresh_check (Rule (fst rule)) i s (Γ ⊢ subst s (freshen i c))"
by (fastforce intro!: local_fresh_check.intros simp add: all_local_vars_def fmember.rep_eq)
ultimately
have "local_iwf ?it ((Γ ⊢ subst s (freshen i c)))"
by (intro iwf ) (auto simp add: list_all2_map2 list_all2_same)
thus ?thesis unfolding NatRule..
next
case (Cut Γ con)
obtain s where "subst s anyP = con" by atomize_elim (rule anyP_is_any)
hence  [simp]: "subst s (freshen undefined anyP) = con" by (simp add: lconsts_anyP freshen_closed)

from ‹(fst ∘ root) |`| cont t = {|Γ ⊢ con|}›
obtain t'  where "t' |∈| cont t" and [simp]: "fst (root t') = (Γ ⊢ con)"
by (cases "cont t") auto

from ‹t' |∈| cont t› obtain "it'" where "local_iwf it' (Γ ⊢ con)" using IH by force

let "?it" = "INode Helper anyP undefined s [it'] ::  ('form, 'rule, 'subst, 'var) itree"

from ‹local_iwf it' (Γ ⊢ con)›
have "local_iwf ?it (Γ ⊢ con)" by (auto intro!: iwf local_fresh_check.intros)
thus ?thesis unfolding Cut..
qed
qed

definition to_it :: "('form entailment × ('rule × 'form) NatRule) tree ⇒ ('form,'rule,'subst,'var) itree" where
"to_it t = (SOME it. local_iwf it (fst (root t)))"

lemma iwf_to_it:
assumes "tfinite t" and "wf t"
shows "local_iwf (to_it t) (fst (root t))"
unfolding to_it_def using build_local_iwf[OF assms] by (rule someI2_ex)
end
end
```