--- a/Nominal/Ex/Lambda.thy Tue Feb 19 05:38:46 2013 +0000
+++ b/Nominal/Ex/Lambda.thy Tue Feb 19 06:58:14 2013 +0000
@@ -1,35 +1,16 @@
theory Lambda
imports
"../Nominal2"
- "~~/src/HOL/Library/Monad_Syntax"
begin
atom_decl name
-ML {* trace := true *}
-
nominal_datatype lam =
Var "name"
| App "lam" "lam"
| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100)
-lemma alpha_lam_raw_eqvt[eqvt]: "p \<bullet> (alpha_lam_raw x y) = alpha_lam_raw (p \<bullet> x) (p \<bullet> y)"
- unfolding alpha_lam_raw_def
- by perm_simp rule
-
-lemma abs_lam_eqvt[eqvt]: "(p \<bullet> abs_lam t) = abs_lam (p \<bullet> t)"
-proof -
- have "alpha_lam_raw (rep_lam (abs_lam t)) t"
- using rep_abs_rsp_left Quotient3_lam equivp_reflp lam_equivp by metis
- then have "alpha_lam_raw (p \<bullet> rep_lam (abs_lam t)) (p \<bullet> t)"
- unfolding alpha_lam_raw_eqvt[symmetric] permute_pure .
- then have "abs_lam (p \<bullet> rep_lam (abs_lam t)) = abs_lam (p \<bullet> t)"
- using Quotient3_rel Quotient3_lam by metis
- thus ?thesis using permute_lam_def id_apply map_fun_apply by metis
-qed
-
-
section {* Simple examples from Norrish 2004 *}
nominal_primrec
@@ -49,7 +30,6 @@
thm is_app_def
thm is_app.eqvt
-
thm eqvts
nominal_primrec
@@ -609,18 +589,6 @@
termination (eqvt)
by lexicographic_order
-lemma transdb_eqvt[eqvt]:
- "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)"
- 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)
- apply (subst transdb.simps)
- apply (simp add: fresh_at_list[symmetric])
- apply (drule_tac x="name # l" in meta_spec)
- apply auto
- done
-
lemma db_trans_test:
assumes a: "y \<noteq> x"
shows "transdb (Lam [x]. Lam [y]. App (Var x) (Var y)) [] =
@@ -681,44 +649,6 @@
done
-(* a small test
-termination (eqvt) sorry
-
-lemma
- assumes "x \<noteq> y"
- shows "eval (App (Lam [x].App (Var x) (Var x)) (Var y)) = App (Var y) (Var y)"
-using assms
-apply(simp add: lam.supp fresh_def supp_at_base)
-done
-*)
-
-
-text {* TODO: eqvt_at for the other side *}
-nominal_primrec q where
- "atom c \<sharp> (x, M) \<Longrightarrow> q (Lam [x]. M) (N :: lam) = Lam [x]. (Lam [c]. (App M (q (Var c) N)))"
-| "q (Var x) N = Var x"
-| "q (App l r) N = App l r"
-apply(simp add: eqvt_def q_graph_aux_def)
-apply (rule TrueI)
-apply (case_tac x)
-apply (rule_tac y="a" in lam.exhaust)
-using [[simproc del: alpha_lst]]
-apply simp_all
-apply blast
-apply blast
-apply (rule_tac x="(name, lam)" and ?'a="name" in obtain_fresh)
-apply blast
-apply clarify
-apply (rule_tac x="(x, xa, M, Ma, c, ca, Na)" and ?'a="name" in obtain_fresh)
-apply (subgoal_tac "eqvt_at q_sumC (Var ca, Na)") --"Could come from nominal_function?"
-apply (subgoal_tac "Lam [c]. App M (q_sumC (Var c, Na)) = Lam [a]. App M (q_sumC (Var a, Na))")
-apply (subgoal_tac "Lam [ca]. App Ma (q_sumC (Var ca, Na)) = Lam [a]. App Ma (q_sumC (Var a, Na))")
-apply (simp only:)
-apply (erule Abs_lst1_fcb)
-oops
-
-text {* Working Examples *}
-
nominal_primrec
map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam"
where
@@ -740,226 +670,6 @@
by lexicographic_order
-(*
-abbreviation
- mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65)
-where
- "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v"
-
-lemma mbind_eqvt:
- fixes c::"'a::pt option"
- shows "(p \<bullet> (c \<guillemotright>= f)) = ((p \<bullet> c) \<guillemotright>= (p \<bullet> f))"
-apply(cases c)
-apply(simp_all)
-apply(perm_simp)
-apply(rule refl)
-done
-
-lemma mbind_eqvt_raw[eqvt_raw]:
- shows "(p \<bullet> option_case) \<equiv> option_case"
-apply(rule eq_reflection)
-apply(rule ext)+
-apply(case_tac xb)
-apply(simp_all)
-apply(rule_tac p="-p" in permute_boolE)
-apply(perm_simp add: permute_minus_cancel)
-apply(simp)
-apply(rule_tac p="-p" in permute_boolE)
-apply(perm_simp add: permute_minus_cancel)
-apply(simp)
-done
-
-fun
- index :: "atom list \<Rightarrow> nat \<Rightarrow> atom \<Rightarrow> nat option"
-where
- "index [] n x = None"
-| "index (y # ys) n x = (if x = y then (Some n) else (index ys (n + 1) x))"
-
-lemma [eqvt]:
- shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
-apply(induct xs arbitrary: n)
-apply(simp_all add: permute_pure)
-done
-*)
-
-(*
-nominal_primrec
- trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
-where
- "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n::nat. Some (DBVar n)))"
-| "trans2 (App t1 t2) xs =
- ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1::db. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2::db. Some (DBApp db1 db2))))"
-| "trans2 (Lam [x].t) xs = (trans2 t (atom x # xs) \<guillemotright>= (\<lambda>db::db. Some (DBLam db)))"
-oops
-*)
-
-nominal_primrec
- CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
-where
- "CPS (Var x) k = Var x"
-| "CPS (App M N) k = CPS M (\<lambda>m. CPS N (\<lambda>n. n))"
-oops
-
-consts b :: name
-nominal_primrec
- Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
-where
- "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"
-| "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))"
-apply(simp add: eqvt_def Z_graph_aux_def)
-apply (rule, perm_simp, rule)
-oops
-
-lemma test:
- assumes "t = s"
- and "supp p \<sharp>* t" "supp p \<sharp>* x"
- and "(p \<bullet> t) = s \<Longrightarrow> (p \<bullet> x) = y"
- shows "x = y"
-using assms by (simp add: perm_supp_eq)
-
-lemma test2:
- assumes "cs \<subseteq> as \<union> bs"
- and "as \<sharp>* x" "bs \<sharp>* x"
- shows "cs \<sharp>* x"
-using assms
-by (auto simp add: fresh_star_def)
-
-lemma test3:
- assumes "cs \<subseteq> as"
- and "as \<sharp>* x"
- shows "cs \<sharp>* x"
-using assms
-by (auto simp add: fresh_star_def)
-
-
-
-nominal_primrec (invariant "\<lambda>(_, _, xs) y. atom ` fst ` set xs \<sharp>* y \<and> atom ` snd ` set xs \<sharp>* y")
- aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool"
-where
- "aux (Var x) (Var y) xs = ((x, y) \<in> set xs)"
-| "aux (App t1 t2) (App s1 s2) xs = (aux t1 s1 xs \<and> aux t2 s2 xs)"
-| "aux (Var x) (App t1 t2) xs = False"
-| "aux (Var x) (Lam [y].t) xs = False"
-| "aux (App t1 t2) (Var x) xs = False"
-| "aux (App t1 t2) (Lam [x].t) xs = False"
-| "aux (Lam [x].t) (Var y) xs = False"
-| "aux (Lam [x].t) (App t1 t2) xs = False"
-| "\<lbrakk>{atom x} \<sharp>* (s, xs); {atom y} \<sharp>* (t, xs); x \<noteq> y\<rbrakk> \<Longrightarrow>
- aux (Lam [x].t) (Lam [y].s) xs = aux t s ((x, y) # xs)"
- apply (simp add: eqvt_def aux_graph_aux_def)
- apply(erule aux_graph.induct)
- apply(simp_all add: fresh_star_def pure_fresh)[9]
- apply(case_tac x)
- apply(simp)
- apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
- apply(simp)
- apply(rule_tac y="b" and c="c" in lam.strong_exhaust)
- apply(metis)+
- apply(simp)
- apply(rule_tac y="b" and c="c" in lam.strong_exhaust)
- apply(metis)+
- apply(simp)
- apply(rule_tac y="b" and c="(lam, c, name)" in lam.strong_exhaust)
- apply(metis)+
- apply(simp)
- apply(drule_tac x="name" in meta_spec)
- apply(drule_tac x="lama" in meta_spec)
- apply(drule_tac x="c" in meta_spec)
- apply(drule_tac x="namea" in meta_spec)
- apply(drule_tac x="lam" in meta_spec)
- apply(simp add: fresh_star_Pair)
- apply(simp add: fresh_star_def fresh_at_base )
- apply(auto)[1]
- apply(simp_all)[44]
- apply(simp del: Product_Type.prod.inject)
- oops
-
-lemma abs_same_binder:
- fixes t ta s sa :: "_ :: fs"
- and x y::"'a::at"
- 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_aux_def)
- apply(rule TrueI)
- 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)
- using [[simproc del: alpha_lst]]
- 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)
- using [[simproc del: alpha_lst]]
- apply(simp add: Abs1_eq_iff fresh_star_def fresh_Pair_elim fresh_at_base flip_def)
- apply (metis Nominal2_Base.swap_commute fresh_permute_iff sort_of_atom_eq swap_atom_simps(2))
- using [[simproc del: alpha_lst]]
- 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