--- a/Nominal/Ex/Lambda.thy Fri Jun 10 15:31:14 2011 +0900
+++ b/Nominal/Ex/Lambda.thy Fri Jun 10 15:45:49 2011 +0900
@@ -10,68 +10,30 @@
| App "lam" "lam"
| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100)
-lemma cheat: "P" sorry
-
-thm lam.strong_exhaust
-
-lemma lam_strong_exhaust2:
- "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P;
- \<And>lam1 lam2. y = App lam1 lam2 \<Longrightarrow> P;
- \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P;
- finite (supp c)\<rbrakk>
- \<Longrightarrow> P"
-sorry
-
-abbreviation
- "FCB f \<equiv> \<forall>x t r. atom x \<sharp> f x t r"
-
nominal_primrec (invariant "\<lambda>x (y::atom set). finite y")
frees_set :: "lam \<Rightarrow> atom set"
where
"frees_set (Var x) = {atom x}"
| "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2"
| "frees_set (Lam [x]. t) = (frees_set t) - {atom x}"
-apply(simp add: eqvt_def frees_set_graph_def)
-apply (rule, perm_simp, rule)
-apply(erule frees_set_graph.induct)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(rule_tac y="x" in lam.exhaust)
-apply(auto)[6]
-apply(simp)
-apply(simp)
-apply(simp)
-apply (erule Abs_lst1_fcb)
-apply(simp add: fresh_def)
-apply(subst supp_of_finite_sets)
-apply(simp)
-apply(simp add: supp_atom)
-apply(simp add: fresh_def)
-apply(subst supp_of_finite_sets)
-apply(simp)
-apply(simp add: supp_atom)
-apply(subst supp_finite_atom_set[symmetric])
-apply(simp)
-apply(simp add: fresh_def[symmetric])
-apply(rule fresh_eqvt_at)
-apply(assumption)
-apply(simp add: finite_supp)
-apply(simp)
-apply(simp add: eqvt_at_def eqvts)
-apply(simp)
-done
+ apply(simp add: eqvt_def frees_set_graph_def)
+ apply(rule, perm_simp, rule)
+ apply(erule frees_set_graph.induct)
+ apply(auto)[9]
+ apply(rule_tac y="x" in lam.exhaust)
+ apply(auto)[3]
+ apply(simp)
+ apply(erule Abs_lst1_fcb)
+ apply(simp_all add: fresh_minus_atom_set)
+ apply(erule fresh_eqvt_at)
+ apply(simp_all add: finite_supp eqvt_at_def eqvts)
+ done
termination
by (relation "measure size") (auto simp add: lam.size)
-thm frees_set.simps
-thm frees_set.induct
-
lemma "frees_set t = supp t"
-apply(induct rule: frees_set.induct)
-apply(simp_all add: lam.supp supp_at_base)
-done
+ by (induct rule: frees_set.induct) (simp_all add: lam.supp supp_at_base)
lemma fresh_fun_eqvt_app3:
assumes a: "eqvt f"
@@ -89,7 +51,7 @@
and fcb: "\<forall>x t r. atom x \<sharp> f3 x t r"
begin
-nominal_primrec
+nominal_primrec
f :: "lam \<Rightarrow> ('a::pt)"
where
"f (Var x) = f1 x"
@@ -223,11 +185,8 @@
by (relation "measure size") (simp_all add: lam.size)
text {* a small test lemma *}
-lemma
- shows "supp t = set (frees_lst t)"
-apply(induct t rule: frees_lst.induct)
-apply(simp_all add: lam.supp supp_at_base)
-done
+lemma shows "supp t = set (frees_lst t)"
+ by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base)
text {* capture - avoiding substitution *}
@@ -263,26 +222,23 @@
lemma forget:
shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
-apply(nominal_induct t avoiding: x s rule: lam.strong_induct)
-apply(auto simp add: lam.fresh fresh_at_base)
-done
+ by (nominal_induct t avoiding: x s rule: lam.strong_induct)
+ (auto simp add: lam.fresh fresh_at_base)
text {* same lemma but with subst.induction *}
lemma forget2:
shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
-apply(induct t x s rule: subst.induct)
-apply(auto simp add: lam.fresh fresh_at_base fresh_Pair)
-done
+ by (induct t x s rule: subst.induct)
+ (auto simp add: lam.fresh fresh_at_base fresh_Pair)
lemma fresh_fact:
fixes z::"name"
assumes a: "atom z \<sharp> s"
- and b: "z = y \<or> atom z \<sharp> t"
+ and b: "z = y \<or> atom z \<sharp> t"
shows "atom z \<sharp> t[y ::= s]"
-using a b
-apply (nominal_induct t avoiding: z y s rule: lam.strong_induct)
-apply (auto simp add: lam.fresh fresh_at_base)
-done
+ using a b
+ by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
+ (auto simp add: lam.fresh fresh_at_base)
lemma substitution_lemma:
assumes a: "x \<noteq> y" "atom x \<sharp> u"
@@ -497,12 +453,7 @@
lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs"
unfolding fresh_def supp_set[symmetric]
- apply (induct xs)
- apply (simp add: supp_set_empty)
- apply simp
- apply auto
- apply (simp_all add: insert_absorb UnI2 finite_set supp_of_finite_insert supp_at_base)
- done
+ by (induct xs) (auto simp add: supp_of_finite_insert supp_at_base supp_set_empty)
fun
vindex :: "name list \<Rightarrow> name \<Rightarrow> nat \<Rightarrow> db option"
@@ -549,12 +500,10 @@
apply auto
done
-(*
lemma db_trans_test:
assumes a: "y \<noteq> x"
- shows "trans (Lam [x]. Lam [y]. App (Var x) (Var y)) [] 0 = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))"
+ shows "transdb (Lam [x]. Lam [y]. App (Var x) (Var y)) [] = 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)
@@ -654,6 +603,8 @@
apply rule
apply simp
oops (* can this be defined ? *)
+ (* Yes, if "sub" is a constant. *)
+
text {* tests of functions containing if and case *}
@@ -744,19 +695,6 @@
apply (rule, perm_simp, rule)
oops
-(* function tests *)
-
-(* similar problem with function package *)
-function
- f :: "int list \<Rightarrow> int"
-where
- "f [] = 0"
-| "f [e] = e"
-| "f (l @ m) = f l + f m"
- apply(simp_all)
-oops
-
-