--- a/Nominal/Ex/Lambda.thy	Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/Lambda.thy	Thu Aug 26 02:08:00 2010 +0800
@@ -5,32 +5,22 @@
 atom_decl name
 declare [[STEPS = 21]]
 
-class s1
-class s2
-
-nominal_datatype lambda: 
- ('a, 'b) lam =
+nominal_datatype lam =
   Var "name"
-| App "('a::s1, 'b::s2) lam" "('a, 'b) lam"
-| Lam x::"name" l::"('a, 'b) lam"  bind x in l
+| App "lam" "lam"
+| Lam x::"name" l::"lam"  bind x in l
 
-thm distinct
-thm induct
-thm exhaust
-thm fv_defs
-thm bn_defs
-thm perm_simps
-thm eq_iff
-thm fv_bn_eqvt
-thm size_eqvt
+thm lam.distinct
+thm lam.induct
+thm lam.exhaust
+thm lam.fv_defs
+thm lam.bn_defs
+thm lam.perm_simps
+thm lam.eq_iff
+thm lam.fv_bn_eqvt
+thm lam.size_eqvt
 
 
-thm lam.fv
-thm lam.supp
-lemmas supp_fn' = lam.fv[simplified lam.supp]
-
-declare lam.perm[eqvt]
-
 
 section {* Strong Induction Principles*}
 
@@ -38,6 +28,7 @@
   Old way of establishing strong induction
   principles by chosing a fresh name.
 *)
+(*
 lemma
   fixes c::"'a::fs"
   assumes a1: "\<And>name c. P c (Var name)"
@@ -79,11 +70,12 @@
   then have "P c (0 \<bullet> lam)" by blast
   then show "P c lam" by simp
 qed
-
+*)
 (* 
   New way of establishing strong induction
   principles by using a appropriate permutation.
 *)
+(*
 lemma
   fixes c::"'a::fs"
   assumes a1: "\<And>name c. P c (Var name)"
@@ -121,6 +113,7 @@
   then have "P c (0 \<bullet> lam)" by blast
   then show "P c lam" by simp
 qed
+*)
 
 section {* Typing *}
 
@@ -131,6 +124,7 @@
 notation
  TFun ("_ \<rightarrow> _") 
 
+(*
 declare ty.perm[eqvt]
 
 inductive
@@ -237,7 +231,7 @@
       apply(simp add: finite_supp)
       apply(rule_tac p="-p" in permute_boolE)
       apply(perm_strict_simp add: permute_minus_cancel)
-	(* supplied by the user *)
+	--"supplied by the user"
       apply(simp add: fresh_star_prod)
       apply(simp add: fresh_star_def)
       sorry
@@ -246,86 +240,9 @@
   then show "P c \<Gamma> t T" by simp
 qed
 
-
-
-
-
-
-
-inductive
-  tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"  
-  for r :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
-where
-    aa: "tt r a a"
-  | bb: "tt r a b ==> tt r a c"
-
-(* PROBLEM: derived eqvt-theorem does not conform with [eqvt]
-equivariance tt
 *)
 
 
-inductive
- alpha_lam_raw'
-where
-  a1: "name = namea \<Longrightarrow> alpha_lam_raw' (Var_raw name) (Var_raw namea)"
-| a2: "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow>
-   alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)"
-| a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw' fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>
-   alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"
-
-equivariance alpha_lam_raw'
-
-thm eqvts_raw
-
-section {* size function *}
-
-lemma size_eqvt_raw:
-  fixes t::"lam_raw"
-  shows "size (pi \<bullet> t)  = size t"
-  apply (induct rule: lam_raw.inducts)
-  apply simp_all
-  done
-
-instantiation lam :: size 
-begin
-
-quotient_definition
-  "size_lam :: lam \<Rightarrow> nat"
-is
-  "size :: lam_raw \<Rightarrow> nat"
-
-lemma size_rsp:
-  "alpha_lam_raw x y \<Longrightarrow> size x = size y"
-  apply (induct rule: alpha_lam_raw.inducts)
-  apply (simp_all only: lam_raw.size)
-  apply (simp_all only: alphas)
-  apply clarify
-  apply (simp_all only: size_eqvt_raw)
-  done
-
-lemma [quot_respect]:
-  "(alpha_lam_raw ===> op =) size size"
-  by (simp_all add: size_rsp)
-
-lemma [quot_preserve]:
-  "(rep_lam ---> id) size = size"
-  by (simp_all add: size_lam_def)
-
-instance
-  by default
-
-end
-
-lemmas size_lam[simp] = 
-  lam_raw.size(4)[quot_lifted]
-  lam_raw.size(5)[quot_lifted]
-  lam_raw.size(6)[quot_lifted]
-
-(* is this needed? *)
-lemma [measure_function]: 
-  "is_measure (size::lam\<Rightarrow>nat)" 
-  by (rule is_measure_trivial)
-
 section {* Matching *}
 
 definition
@@ -512,6 +429,7 @@
 | "match_App_raw (App_raw x y) = Some (x, y)"
 | "match_App_raw (Lam_raw n t) = None"
 
+(*
 quotient_definition
   "match_App :: lam \<Rightarrow> (lam \<times> lam) option"
 is match_App_raw
@@ -547,7 +465,7 @@
   apply (simp add: lam_half_inj)
   apply auto
   done
-
+*)
 (*
 lemma match_Lam_simps2:
   "atom n \<sharp> ((S :: 'a :: fs), Lam n s) \<Longrightarrow> match_Lam S (Lam n s) = Some (n, s)"
@@ -627,7 +545,7 @@
 
 lemmas match_Lam_simps = match_Lam_raw.simps[quot_lifted]
 *)
-
+(*
 lemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b"
 by (induct x rule: lam.induct) (simp_all add: match_App_simps)
 
@@ -767,7 +685,7 @@
   apply (simp only: option.simps)
   apply (simp only: prod.simps)
   sorry
-
+*)
 end