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