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

context Abstract_Task
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))"
      by (auto simp add: natEff_Inst.simps)  

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