theory LamFunimports "../Nominal2" Quotient_Optionbeginatom_decl namenominal_datatype lam = Var "name"| App "lam" "lam"| Lam x::"name" l::"lam" binds x in lthm lam.distinctthm lam.inductthm lam.exhaustthm lam.fv_defsthm lam.bn_defsthm lam.perm_simpsthm lam.eq_iffthm lam.fv_bn_eqvtthm lam.size_eqvtthm lam.sizethm lam_raw.sizethm lam.freshprimrec match_Var_raw where "match_Var_raw (Var_raw x) = Some x"| "match_Var_raw (App_raw x y) = None"| "match_Var_raw (Lam_raw n t) = None"quotient_definition "match_Var :: lam \<Rightarrow> name option"is match_Var_rawlemma [quot_respect]: "(alpha_lam_raw ===> op =) match_Var_raw match_Var_raw" by (rule, induct_tac a b rule: alpha_lam_raw.induct, simp_all)lemmas match_Var_simps = match_Var_raw.simps[quot_lifted]primrec match_App_raw where "match_App_raw (Var_raw x) = None"| "match_App_raw (App_raw x y) = Some (x, y)"| "match_App_raw (Lam_raw n t) = None"quotient_definition "match_App :: lam \<Rightarrow> (lam \<times> lam) option"is match_App_rawlemma [quot_respect]: "(alpha_lam_raw ===> option_rel (prod_rel alpha_lam_raw alpha_lam_raw)) match_App_raw match_App_raw" by (intro fun_relI, induct_tac a b rule: alpha_lam_raw.induct, simp_all)lemmas match_App_simps = match_App_raw.simps[quot_lifted]definition next_name where "next_name (s :: 'a :: fs) = (THE x. \<forall>a \<in> supp s. atom x \<noteq> a)"lemma lam_eq: "Lam a t = Lam b s \<longleftrightarrow> (a \<leftrightarrow> b) \<bullet> t = s" apply (simp add: lam.eq_iff Abs_eq_iff alphas) sorrylemma lam_half_inj: "(Lam z s = Lam z sa) = (s = sa)" by (auto simp add: lam_eq)definition "match_Lam (S :: 'a :: fs) t = (if (\<exists>n s. (t = Lam n s)) then (let z = next_name (S, t) in Some (z, THE s. t = Lam z s)) else None)"lemma match_Lam_simps: "match_Lam S (Var n) = None" "match_Lam S (App l r) = None" "match_Lam S (Lam z s) = (let n = next_name (S, (Lam z s)) in Some (n, (z \<leftrightarrow> n) \<bullet> s))" apply (simp_all add: match_Lam_def lam.distinct) apply (auto simp add: lam_eq) donelemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b"by (induct x rule: lam.induct) (simp_all add: match_App_simps)lemma lam_some: "match_Lam S x = Some (n, t) \<Longrightarrow> x = Lam n t" apply (induct x rule: lam.induct) apply (simp add: match_Lam_simps) apply (simp add: match_Lam_simps) apply (simp add: match_Lam_simps Let_def lam_eq) apply clarify donefunction subst where"subst v s t = ( case match_Var t of Some n \<Rightarrow> if n = v then s else Var n | None \<Rightarrow> case match_App t of Some (l, r) \<Rightarrow> App (subst v s l) (subst v s r) | None \<Rightarrow> case match_Lam (v, s) t of Some (n, s') \<Rightarrow> Lam n (subst v s s') | None \<Rightarrow> undefined)"print_theoremsthm subst_rel.intros[no_vars]by pat_completeness autotermination apply (relation "measure (\<lambda>(_, _, t). size t)") apply auto[1] apply (case_tac a) apply simp apply (frule lam_some) apply (simp add: lam.size) apply (case_tac a) apply simp apply (frule app_some) apply (simp add: lam.size) apply (case_tac a) apply simp apply (frule app_some) apply (simp add: lam.size)donelemma subst_eqs: "subst y s (Var x) = (if x = y then s else (Var x))" "subst y s (App l r) = App (subst y s l) (subst y s r)" "subst y s (Lam x t) = (let n = next_name ((y, s), Lam x t) in Lam n (subst y s ((x \<leftrightarrow> n) \<bullet> t)))" apply (subst subst.simps) apply (simp only: match_Var_simps option.simps) apply (subst subst.simps) apply (simp only: match_App_simps option.simps prod.simps match_Var_simps) apply (subst subst.simps) apply (simp only: match_App_simps option.simps prod.simps match_Var_simps match_Lam_simps Let_def) donelemma subst_eqvt: "p \<bullet> (subst v s t) = subst (p \<bullet> v) (p \<bullet> s) (p \<bullet> t)" proof (induct v s t rule: subst.induct) case (1 v s t) show ?case proof (cases t rule: lam.exhaust) fix n assume "t = Var n" then show ?thesis by (simp add: match_Var_simps) next fix l r assume "t = App l r" then show ?thesis apply (simp only: subst_eqs lam.perm_simps) apply (subst 1(2)[of "(l, r)" "l" "r"]) apply (simp add: match_Var_simps) apply (simp add: match_App_simps) apply (rule refl) apply (subst 1(3)[of "(l, r)" "l" "r"]) apply (simp add: match_Var_simps) apply (simp add: match_App_simps) apply (rule refl) apply (rule refl) done next fix n t' assume "t = Lam n t'" then show ?thesis apply (simp only: subst_eqs lam.perm_simps Let_def) apply (subst 1(1)) apply (simp add: match_Var_simps) apply (simp add: match_App_simps) apply (simp add: match_Lam_simps Let_def) apply (rule refl) (* next_name is not equivariant :( *) apply (simp only: lam_eq) sorry qed qedlemma subst_eqvt': "p \<bullet> (subst v s t) = subst (p \<bullet> v) (p \<bullet> s) (p \<bullet> t)" apply (induct t arbitrary: v s rule: lam.induct) apply (simp only: subst_eqs lam.perm_simps eqvts) apply (simp only: subst_eqs lam.perm_simps) apply (simp only: subst_eqs lam.perm_simps Let_def) apply (simp only: lam_eq) sorrylemma subst_eq3: "atom x \<sharp> (y, s) \<Longrightarrow> subst y s (Lam x t) = Lam x (subst y s t)" apply (simp only: subst_eqs Let_def) apply (simp only: lam_eq) (* p # y p # s subst_eqvt *) (* p \<bullet> -p \<bullet> (subst y s t) = subst y s t *) sorryend