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