diff -r 8648ae682442 -r 70bbd18ad194 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Tue Jul 05 04:19:02 2011 +0200 +++ b/Nominal/Ex/Lambda.thy Tue Jul 05 04:23:33 2011 +0200 @@ -359,23 +359,13 @@ | DBApp db db | DBLam db -fun dbapp_in where - "dbapp_in None _ = None" -| "dbapp_in (Some _ ) None = None" -| "dbapp_in (Some x) (Some y) = Some (DBApp x y)" - -fun dblam_in where - "dblam_in None = None" -| "dblam_in (Some x) = Some (DBLam x)" +lemma option_map_eqvt[eqvt]: + "p \<bullet> (Option.map f x) = Option.map (p \<bullet> f) (p \<bullet> x)" + by (cases x) (simp_all, simp add: permute_fun_app_eq) -lemma db_in_eqvt[eqvt]: - "p \<bullet> (dbapp_in x y) = dbapp_in (p \<bullet> x) (p \<bullet> y)" - "p \<bullet> (dblam_in x) = dblam_in (p \<bullet> x)" - apply (case_tac [!] x) - apply (simp_all add: eqvts) - apply (case_tac y) - apply (simp_all add: eqvts) - done +lemma option_bind_eqvt[eqvt]: + shows "(p \<bullet> (Option.map f c)) = (Option.map (p \<bullet> f) (p \<bullet> c))" + by (cases c) (simp_all, simp add: permute_fun_app_eq) instance db :: pure apply default @@ -401,8 +391,8 @@ transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option" where "transdb (Var x) l = vindex l x 0" -| "transdb (App t1 t2) xs = dbapp_in (transdb t1 xs) (transdb t2 xs)" -| "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = dblam_in (transdb t (x # xs))" +| "transdb (App t1 t2) xs = Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))" +| "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))" unfolding eqvt_def transdb_graph_def apply (rule, perm_simp, rule) apply(rule TrueI) @@ -410,12 +400,11 @@ apply (rule_tac y="a" and c="b" in lam.strong_exhaust) apply (auto simp add: fresh_star_def fresh_at_list)[3] apply(simp_all) - apply(erule conjE) + apply(elim conjE) apply (erule_tac c="xsa" in Abs_lst1_fcb2') apply (simp add: pure_fresh) apply(simp add: fresh_star_def fresh_at_list) - apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq db_in_eqvt) - apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq db_in_eqvt) + apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq eqvts eqvts_raw)+ done termination @@ -423,7 +412,7 @@ lemma transdb_eqvt[eqvt]: "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)" - apply (nominal_induct t avoiding: l p rule: lam.strong_induct) + apply (nominal_induct t avoiding: l rule: lam.strong_induct) apply (simp add: vindex_eqvt) apply (simp_all add: permute_pure) apply (simp add: fresh_at_list) @@ -439,6 +428,7 @@ Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" using a by simp + abbreviation mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65) where @@ -611,48 +601,6 @@ apply (rule, perm_simp, rule) oops -text {* tests of functions containing if and case *} - -consts P :: "lam \<Rightarrow> bool" - -nominal_primrec - A :: "lam => lam" -where - "A (App M N) = (if (True \<or> P M) then (A M) else (A N))" -| "A (Var x) = (Var x)" -| "A (App M N) = (if True then M else A N)" -oops - -nominal_primrec - C :: "lam => lam" -where - "C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))" -| "C (Var x) = (Var x)" -| "C (App M N) = (if True then M else C N)" -oops - -nominal_primrec - A :: "lam => lam" -where - "A (Lam [x].M) = (Lam [x].M)" -| "A (Var x) = (Var x)" -| "A (App M N) = (if True then M else A N)" -oops - -nominal_primrec - B :: "lam => lam" -where - "B (Lam [x].M) = (Lam [x].M)" -| "B (Var x) = (Var x)" -| "B (App M N) = (if True then M else (B N))" -unfolding eqvt_def -unfolding B_graph_def -apply(perm_simp) -apply(rule allI) -apply(rule refl) -oops - - lemma test: assumes "t = s" and "supp p \<sharp>* t" "supp p \<sharp>* x" @@ -720,6 +668,88 @@ termination by lexicographic_order +lemma abs_same_binder: + fixes t ta s sa :: "_ :: fs" + assumes "sort_of (atom x) = sort_of (atom y)" + shows "[[atom x]]lst. t = [[atom y]]lst. ta \<and> [[atom x]]lst. s = [[atom y]]lst. sa + \<longleftrightarrow> [[atom x]]lst. (t, s) = [[atom y]]lst. (ta, sa)" + by (cases "atom x = atom y") (auto simp add: Abs1_eq_iff assms fresh_Pair) + +nominal_primrec + aux2 :: "lam \<Rightarrow> lam \<Rightarrow> bool" +where + "aux2 (Var x) (Var y) = (x = y)" +| "aux2 (App t1 t2) (App s1 s2) = (aux2 t1 s1 \<and> aux2 t2 s2)" +| "aux2 (Var x) (App t1 t2) = False" +| "aux2 (Var x) (Lam [y].t) = False" +| "aux2 (App t1 t2) (Var x) = False" +| "aux2 (App t1 t2) (Lam [x].t) = False" +| "aux2 (Lam [x].t) (Var y) = False" +| "aux2 (Lam [x].t) (App t1 t2) = False" +| "x = y \<Longrightarrow> aux2 (Lam [x].t) (Lam [y].s) = aux2 t s" + apply(simp add: eqvt_def aux2_graph_def) + apply(rule, perm_simp, rule, rule) + apply(case_tac x) + apply(rule_tac y="a" and c="b" in lam.strong_exhaust) + apply(rule_tac y="b" in lam.exhaust) + apply(auto)[3] + apply(rule_tac y="b" in lam.exhaust) + apply(auto)[3] + apply(rule_tac y="b" and c="(name, lam)" in lam.strong_exhaust) + apply(auto)[3] + apply(drule_tac x="name" in meta_spec) + apply(drule_tac x="name" in meta_spec) + apply(drule_tac x="lam" in meta_spec) + apply(drule_tac x="(name \<leftrightarrow> namea) \<bullet> lama" in meta_spec) + apply(simp add: Abs1_eq_iff fresh_star_def fresh_Pair_elim fresh_at_base lam.fresh flip_def) + apply (metis Nominal2_Base.swap_commute fresh_permute_iff sort_of_atom_eq swap_atom_simps(2)) + apply simp_all + apply (simp add: abs_same_binder) + apply (erule_tac c="()" in Abs_lst1_fcb2) + apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def) + done + +text {* tests of functions containing if and case *} + +consts P :: "lam \<Rightarrow> bool" + +nominal_primrec + A :: "lam => lam" +where + "A (App M N) = (if (True \<or> P M) then (A M) else (A N))" +| "A (Var x) = (Var x)" +| "A (App M N) = (if True then M else A N)" +oops + +nominal_primrec + C :: "lam => lam" +where + "C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))" +| "C (Var x) = (Var x)" +| "C (App M N) = (if True then M else C N)" +oops + +nominal_primrec + A :: "lam => lam" +where + "A (Lam [x].M) = (Lam [x].M)" +| "A (Var x) = (Var x)" +| "A (App M N) = (if True then M else A N)" +oops + +nominal_primrec + B :: "lam => lam" +where + "B (Lam [x].M) = (Lam [x].M)" +| "B (Var x) = (Var x)" +| "B (App M N) = (if True then M else (B N))" +unfolding eqvt_def +unfolding B_graph_def +apply(perm_simp) +apply(rule allI) +apply(rule refl) +oops + end