--- 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