Theory Lambda_Term

theory Lambda_Term
imports BNF_Nonuniform_Fixpoint
theory Lambda_Term
  imports "../code/BNF_Nonuniform_Fixpoint"
begin

nonuniform_datatype (fv: 'a) tm =
  Var 'a
  | App "'a tm" "'a tm"
  | Abs "'a option tm"

thm
  tm.map
  tm.pred_inject
  tm.rel_inject
  tm.rel_distinct
  tm.set

consts join :: "'a tm tm ⇒ 'a tm"

axiomatization where
  join_Var[simp]: "join (Var x) = x" and
  join_App[simp]: "join (App s t) = App (join s) (join t)" and
  join_Abs[simp]: "join (Abs u) =
    Abs (join (map_tm (λx. case x of None ⇒ Var None | Some y ⇒ map_tm Some y) u))"

axiomatization where join_transfer[transfer_rule]:
  "bi_unique A ⟹ rel_fun (rel_tm (rel_tm A)) (rel_tm A) join join"

definition subst :: "('a ⇒ 'b tm) ⇒ 'a tm ⇒ 'b tm" where
  "subst σ = join ∘ map_tm σ"

lemma subst_Var[simp]: "subst σ (Var x) = σ x"
  by (simp add: subst_def)

lemma subst_App[simp]: "subst σ (App s t) = App (subst σ s) (subst σ t)"
  by (simp add: subst_def)

lemma subst_Abs[simp]: "subst σ (Abs u) = Abs (subst (case_option (Var None) (map_tm Some ∘ σ)) u)"
  apply (simp add: subst_def tm.map_comp)
  apply (rule arg_cong[of _ _ join])
  apply (rule fun_cong[of _ _ u])
  apply (rule arg_cong[of _ _ map_tm])
  apply (auto split: option.split)
  done

lemma subst_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique B"
  shows "(rel_fun (rel_fun A (rel_tm B)) (rel_fun (rel_tm A) (rel_tm B))) subst subst"
  unfolding subst_def by transfer_prover

lemma subst_map_tm_Some:
  "subst (case_option (Var None) (λx. map_tm Some (σ x))) (map_tm Some s) =
   map_tm Some (subst σ s)"
  using subst_transfer[of "BNF_Def.Grp UNIV Some" "BNF_Def.Grp UNIV Some"]
  unfolding tm.rel_Grp bi_unique_Grp unfolding rel_fun_def Grp_def
  apply auto
  apply (drule spec2)
  apply (drule mp)
   prefer 2
   apply (erule spec)
  apply simp
  done


nonuniform_induct s in
  subst_subst: "∀σ τ :: 'a ⇒ 'a tm. subst τ (subst σ (s :: 'a tm)) = subst (subst τ ∘ σ) s"
  subgoal premises prems[transfer_rule]
    apply transfer_prover_start
            apply transfer_step+
      prefer 3
      apply (rule refl)
    unfolding Rel_def
     apply (rule left_total_All_transfer')
     apply (rule left_total_fun[of R])
    using bi_unique_alt_def prems(1) apply blast
     apply (simp add: prems(2) tm.left_total_rel)
    apply (rule left_total_All_transfer)
    apply (rule left_total_fun[of R])
    using bi_unique_alt_def prems(1) apply blast
    apply (simp add: prems(2) tm.left_total_rel)
    done
    apply auto[2]
  apply clarsimp
proof -
  fix x :: "'a option tm" and σ τ :: "'a ⇒ 'a tm"
  assume subst_x: "∀σ τ :: 'a option ⇒ 'a option tm. subst τ (subst σ x) = subst (subst τ ∘ σ) x"
  show "subst (case_option (Var None) (map_tm Some ∘ τ))
              (subst (case_option (Var None) (map_tm Some ∘ σ)) x) =
             subst (case_option (Var None) (map_tm Some ∘ (subst τ ∘ σ))) x"
    unfolding subst_x[rule_format]
    apply (rule fun_cong[of _ _ x])
    apply (rule arg_cong[of _ _ subst])
    apply (simp add: comp_def)
    apply (rule ext)
    subgoal for y
      apply (cases y)
       apply (auto simp: subst_map_tm_Some)
      done
    done
qed

end