diff -r 4b4742aa43f2 -r 11f6a561eb4b Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Sat Dec 17 17:03:01 2011 +0000
+++ b/Nominal/Ex/Lambda.thy	Sat Dec 17 17:08:47 2011 +0000
@@ -12,20 +12,6 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
-ML {* Method.SIMPLE_METHOD' *}
-ML {* Sign.intern_const *}
-
-ML {*
-val test:((Proof.context -> Method.method) context_parser) =
-Scan.succeed (fn ctxt =>
- let
-   val _ = Inductive.the_inductive ctxt "local.frees_lst_graph"
- in 
-   Method.SIMPLE_METHOD' (K (all_tac))
- end)
-*}
-
-method_setup test = {* test *} {* test *}
 
 section {* Simple examples from Norrish 2004 *}
 
@@ -608,323 +594,6 @@
   "atom x \<sharp> s \<Longrightarrow> atom x \<sharp> (t[x ::= s])"
   by (induct t x s rule: subst.induct) (auto simp add: lam.supp lam.fresh fresh_at_base)
 
-(* function that evaluates a lambda term *)
-nominal_primrec
-   eval :: "lam \<Rightarrow> lam" and
-   apply_subst :: "lam \<Rightarrow> lam \<Rightarrow> lam"
-where
-  "eval (Var x) = Var x"
-| "eval (Lam [x].t) = Lam [x].(eval t)"
-| "eval (App t1 t2) = apply_subst (eval t1) (eval t2)"
-| "apply_subst (Var x) t2 = App (Var x) t2"
-| "apply_subst (App t0 t1) t2 = App (App t0 t1) t2"
-| "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])"
-  apply(simp add: eval_apply_subst_graph_def eqvt_def)
-  apply(rule, perm_simp, rule)
-  apply(rule TrueI)
-  apply (case_tac x)
-  apply (case_tac a rule: lam.exhaust)
-  apply simp_all[3]
-  apply blast
-  apply (case_tac b)
-  apply (rule_tac y="a" and c="ba" in lam.strong_exhaust)
-  apply simp_all[3]
-  apply blast
-  apply blast
-  apply (simp add: Abs1_eq_iff fresh_star_def)
-  apply(simp_all)
-  apply(erule_tac c="()" in Abs_lst1_fcb2)
-  apply (simp add: Abs_fresh_iff)
-  apply(simp add: fresh_star_def fresh_Unit)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
-  apply(erule conjE)
-  apply(erule_tac c="t2a" in Abs_lst1_fcb2')
-  apply (erule fresh_eqvt_at)
-  apply (simp add: finite_supp)
-  apply (simp add: fresh_Inl var_fresh_subst)
-  apply(simp add: fresh_star_def)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt)
-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"
-unfolding eqvt_def q_graph_def
-apply (rule, perm_simp, rule)
-apply (rule TrueI)
-apply (case_tac x)
-apply (rule_tac y="a" in lam.exhaust)
-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
-  "eqvt f \<Longrightarrow> map_term f (Var x) = f (Var x)"
-| "eqvt f \<Longrightarrow> map_term f (App t1 t2) = App (f t1) (f t2)"
-| "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)"
-| "\<not>eqvt f \<Longrightarrow> map_term f t = t"
-  apply (simp add: eqvt_def map_term_graph_def)
-  apply (rule, perm_simp, rule)
-  apply(rule TrueI)
-  apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
-  apply auto
-  apply (erule Abs_lst1_fcb)
-  apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
-  apply (simp add: eqvt_def permute_fun_app_eq)
-  done
-
-termination (eqvt)
-  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)))))))"
-unfolding eqvt_def Z_graph_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_def)
-  apply (rule, perm_simp, rule)
-  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 lam.fresh)
-  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"
-  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