--- a/Nominal/Ex/Classical.thy	Wed Jun 29 17:01:09 2011 +0100
+++ b/Nominal/Ex/Classical.thy	Wed Jun 29 19:21:26 2011 +0100
@@ -2,6 +2,7 @@
 imports "../Nominal2"
 begin
 
+
 (* example from Urban's PhD *)
 
 atom_decl name
@@ -177,7 +178,9 @@
   then have "(q \<bullet> (as \<inter> supp x)) \<sharp>* f (q \<bullet> (as \<inter> supp x)) (q \<bullet> x) c"
     apply(simp add: fresh_star_eqvt set_eqvt)
     sorry (* perm? *)
-  then have "r \<bullet> (bs \<inter> supp y) \<sharp>* f (r \<bullet> (bs \<inter> supp y)) (r \<bullet> y) c" using qq2 apply (simp add: inter_eqvt)
+  then have "r \<bullet> (bs \<inter> supp y) \<sharp>* f (r \<bullet> (bs \<inter> supp y)) (r \<bullet> y) c" using qq2 
+    apply (simp add: inter_eqvt)
+    sorry
   (* rest similar reversing it other way around... *)
   show ?thesis sorry
 qed
@@ -476,6 +479,8 @@
   apply(blast)
   done
 
+
+
 end
 
 

--- a/Nominal/Ex/Let.thy	Wed Jun 29 17:01:09 2011 +0100
+++ b/Nominal/Ex/Let.thy	Wed Jun 29 19:21:26 2011 +0100
@@ -2,6 +2,7 @@
 imports "../Nominal2" 
 begin
 
+
 atom_decl name
 
 nominal_datatype trm =
@@ -305,6 +306,7 @@
   apply (erule alpha_bn_inducts)
  oops
 
+
 end
 
 

--- a/Nominal/ROOT.ML	Wed Jun 29 17:01:09 2011 +0100
+++ b/Nominal/ROOT.ML	Wed Jun 29 19:21:26 2011 +0100
@@ -4,7 +4,7 @@
    ["Atoms",
     "Eqvt",
     "Ex/Weakening",
-    "Ex/Classical",    
+    (*"Ex/Classical",*)    
     "Ex/Datatypes",
     "Ex/Ex1",
     "Ex/ExPS3",
@@ -12,7 +12,7 @@
     "Ex/Multi_Recs2",
     "Ex/LF",
     "Ex/Lambda",
-    "Ex/Let",
+    (*"Ex/Let",*)
     "Ex/LetPat",
     "Ex/LetRec",
     "Ex/LetRec2",
@@ -28,3 +28,12 @@
     "Ex/CoreHaskell",
     "Ex/CoreHaskell2" 
    ];
+
+quick_and_dirty := true;
+
+no_document use_thys
+   ["Ex/Classical",    
+    "Ex/Let"
+   ];
+
+

--- a/Nominal/nominal_dt_alpha.ML	Wed Jun 29 17:01:09 2011 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Wed Jun 29 19:21:26 2011 +0100
@@ -13,18 +13,18 @@
     bclause list list list -> term list -> Proof.context -> 
     term list * term list * thm list * thm list * thm * local_theory
 
-  val raw_prove_alpha_distincts: Proof.context -> thm list -> thm list -> 
-    term list -> string list -> thm list
-
-  val raw_prove_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> 
-    thm list -> thm list
-
   val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> 
     (Proof.context -> int -> tactic) -> Proof.context -> thm list
   
   val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> 
     (Proof.context -> int -> tactic) -> Proof.context -> thm list
 
+  val raw_prove_alpha_distincts: Proof.context -> thm list -> thm list -> 
+    term list -> string list -> thm list
+
+  val raw_prove_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> 
+    thm list -> thm list
+  
   val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list
   val raw_prove_sym: term list -> thm list -> thm -> thm list -> Proof.context -> thm list
   val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> thm list -> 
@@ -53,6 +53,7 @@
 fun lookup xs x = the (AList.lookup (op=) xs x)
 fun group xs = AList.group (op=) xs
 
+
 (** definition of the inductive rules for alpha and alpha_bn **)
 
 (* construct the compound terms for prod_fv and prod_alpha *)
@@ -276,9 +277,97 @@
   end
 
 
+(** induction proofs **)
+
+
+(* proof by structural induction over data types *)
+
+fun induct_prove tys props induct_thm cases_tac ctxt =
+  let
+    val (arg_names, ctxt') =
+      Variable.variant_fixes (replicate (length tys) "x") ctxt
+
+    val args = map2 (curry Free) arg_names tys
+
+    val true_trms = replicate (length tys) (K @{term True})
+  
+    fun apply_all x fs = map (fn f => f x) fs
+    
+    val goals = 
+        group (props @ (tys ~~ true_trms))
+        |> map snd 
+        |> map2 apply_all args
+        |> map fold_conj
+        |> foldr1 HOLogic.mk_conj
+        |> HOLogic.mk_Trueprop
+
+    fun tac ctxt =
+      HEADGOAL 
+        (DETERM o (rtac induct_thm) 
+         THEN_ALL_NEW 
+           (REPEAT_ALL_NEW (FIRST' [resolve_tac @{thms TrueI conjI}, cases_tac ctxt])))
+  in
+    Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
+    |> singleton (ProofContext.export ctxt' ctxt)
+    |> Datatype_Aux.split_conj_thm
+    |> map Datatype_Aux.split_conj_thm
+    |> flat
+    |> filter_out (is_true o concl_of)
+    |> map zero_var_indexes
+  end
+
+(* proof by rule induction over the alpha-definitions *)
+
+fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt =
+  let
+    val arg_tys = map (domain_type o fastype_of) alphas
+
+    val ((arg_names1, arg_names2), ctxt') =
+      ctxt
+      |> Variable.variant_fixes (replicate (length alphas) "x") 
+      ||>> Variable.variant_fixes (replicate (length alphas) "y")
+
+    val args1 = map2 (curry Free) arg_names1 arg_tys
+    val args2 = map2 (curry Free) arg_names2 arg_tys
+
+    val true_trms = replicate (length alphas) (K @{term True})
+  
+    fun apply_all x fs = map (fn f => f x) fs
+    
+    val goals_rhs = 
+        group (props @ (alphas ~~ true_trms))
+        |> map snd 
+        |> map2 apply_all (args1 ~~ args2)
+        |> map fold_conj
+
+    fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2
+    val goals_lhs = map2 apply_trm_pair alphas (args1 ~~ args2)
+
+    val goals =
+      (map2 (curry HOLogic.mk_imp) goals_lhs goals_rhs)
+      |> foldr1 HOLogic.mk_conj
+      |> HOLogic.mk_Trueprop
+
+    fun tac ctxt =
+      HEADGOAL 
+        (DETERM o (rtac alpha_induct_thm) 
+         THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt])
+  in
+    Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
+    |> singleton (ProofContext.export ctxt' ctxt)
+    |> Datatype_Aux.split_conj_thm
+    |> map (fn th => th RS mp) 
+    |> map Datatype_Aux.split_conj_thm
+    |> flat
+    |> filter_out (is_true o concl_of)
+    |> map zero_var_indexes
+  end
+
+
 
 (** produces the distinctness theorems **)
 
+
 (* transforms the distinctness theorems of the constructors 
    into "not-alphas" of the constructors *)
 fun mk_distinct_goal ty_trm_assoc neq =
@@ -296,7 +385,6 @@
   rtac notI THEN' eresolve_tac cases_thms 
   THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms)
 
-
 fun raw_prove_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_str =
   let
     val ty_trm_assoc = alpha_str ~~ (map (fst o dest_Const) alpha_trms)
@@ -353,91 +441,6 @@
   end
 
 
-(** proof by induction over types **)
-
-fun induct_prove tys props induct_thm cases_tac ctxt =
-  let
-    val (arg_names, ctxt') =
-      Variable.variant_fixes (replicate (length tys) "x") ctxt
-
-    val args = map2 (curry Free) arg_names tys
-
-    val true_trms = replicate (length tys) (K @{term True})
-  
-    fun apply_all x fs = map (fn f => f x) fs
-    
-    val goals = 
-        group (props @ (tys ~~ true_trms))
-        |> map snd 
-        |> map2 apply_all args
-        |> map fold_conj
-        |> foldr1 HOLogic.mk_conj
-        |> HOLogic.mk_Trueprop
-
-    fun tac ctxt =
-      HEADGOAL 
-        (DETERM o (rtac induct_thm) 
-         THEN_ALL_NEW 
-           (REPEAT_ALL_NEW (FIRST' [resolve_tac @{thms TrueI conjI}, cases_tac ctxt])))
-  in
-    Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
-    |> singleton (ProofContext.export ctxt' ctxt)
-    |> Datatype_Aux.split_conj_thm
-    |> map Datatype_Aux.split_conj_thm
-    |> flat
-    |> filter_out (is_true o concl_of)
-    |> map zero_var_indexes
-  end
-
-
-(** proof by induction over the alpha-definitions **)
-
-fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt =
-  let
-    val arg_tys = map (domain_type o fastype_of) alphas
-
-    val ((arg_names1, arg_names2), ctxt') =
-      ctxt
-      |> Variable.variant_fixes (replicate (length alphas) "x") 
-      ||>> Variable.variant_fixes (replicate (length alphas) "y")
-
-    val args1 = map2 (curry Free) arg_names1 arg_tys
-    val args2 = map2 (curry Free) arg_names2 arg_tys
-
-    val true_trms = replicate (length alphas) (K @{term True})
-  
-    fun apply_all x fs = map (fn f => f x) fs
-    
-    val goals_rhs = 
-        group (props @ (alphas ~~ true_trms))
-        |> map snd 
-        |> map2 apply_all (args1 ~~ args2)
-        |> map fold_conj
-
-    fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2
-    val goals_lhs = map2 apply_trm_pair alphas (args1 ~~ args2)
-
-    val goals =
-      (map2 (curry HOLogic.mk_imp) goals_lhs goals_rhs)
-      |> foldr1 HOLogic.mk_conj
-      |> HOLogic.mk_Trueprop
-
-    fun tac ctxt =
-      HEADGOAL 
-        (DETERM o (rtac alpha_induct_thm) 
-         THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt])
-  in
-    Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
-    |> singleton (ProofContext.export ctxt' ctxt)
-    |> Datatype_Aux.split_conj_thm
-    |> map (fn th => th RS mp) 
-    |> map Datatype_Aux.split_conj_thm
-    |> flat
-    |> filter_out (is_true o concl_of)
-    |> map zero_var_indexes
-  end
-
-
 (** reflexivity proof for the alphas **)
 
 val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto}