diff -r fb201e383f1b -r da575186d492 Nominal/Ex/Lambda.thy
--- 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