# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1282851437 -28800
# Node ID 0a36825b16c166a988b0e0f0538eb4e899b5013f
# Parent  cc6e281d8f72afb9c68658d3d216ff25785abe8c
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)

diff -r cc6e281d8f72 -r 0a36825b16c1 IsaMakefile
--- a/IsaMakefile	Fri Aug 27 02:08:36 2010 +0800
+++ b/IsaMakefile	Fri Aug 27 03:37:17 2010 +0800
@@ -1,10 +1,10 @@
 
 ## targets
 
-default: Nominal2
+default: test
 images: 
 
-all: Nominal2 paper pearl pearl-jv qpaper
+all: test paper pearl pearl-jv qpaper
 
 
 ## global settings
@@ -18,7 +18,7 @@
 
 ## Nominal2
 
-Nominal2: $(LOG)/HOL-Nominal2.gz
+test: $(LOG)/HOL-Nominal2.gz
 
 $(LOG)/HOL-Nominal2.gz: Nominal/ROOT.ML Nominal/*.thy
 	@cd Nominal; $(USEDIR) -b -d "" HOL Nominal
diff -r cc6e281d8f72 -r 0a36825b16c1 Nominal/Ex/ExPS8.thy
--- a/Nominal/Ex/ExPS8.thy	Fri Aug 27 02:08:36 2010 +0800
+++ b/Nominal/Ex/ExPS8.thy	Fri Aug 27 03:37:17 2010 +0800
@@ -6,7 +6,7 @@
 
 atom_decl name
 
-declare [[STEPS = 15]]
+declare [[STEPS = 100]]
 
 nominal_datatype exp =
   EVar name
diff -r cc6e281d8f72 -r 0a36825b16c1 Nominal/Ex/LF.thy
--- a/Nominal/Ex/LF.thy	Fri Aug 27 02:08:36 2010 +0800
+++ b/Nominal/Ex/LF.thy	Fri Aug 27 03:37:17 2010 +0800
@@ -2,7 +2,7 @@
 imports "../NewParser"
 begin
 
-declare [[STEPS = 20]]
+declare [[STEPS = 100]]
 
 atom_decl name
 atom_decl ident
diff -r cc6e281d8f72 -r 0a36825b16c1 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Fri Aug 27 02:08:36 2010 +0800
+++ b/Nominal/Ex/Lambda.thy	Fri Aug 27 03:37:17 2010 +0800
@@ -3,7 +3,7 @@
 begin
 
 atom_decl name
-declare [[STEPS = 21]]
+declare [[STEPS = 100]]
 
 nominal_datatype lam =
   Var "name"
diff -r cc6e281d8f72 -r 0a36825b16c1 Nominal/Ex/TypeVarsTest.thy
--- a/Nominal/Ex/TypeVarsTest.thy	Fri Aug 27 02:08:36 2010 +0800
+++ b/Nominal/Ex/TypeVarsTest.thy	Fri Aug 27 03:37:17 2010 +0800
@@ -3,7 +3,7 @@
 begin
 
 atom_decl name
-declare [[STEPS = 21]]
+declare [[STEPS = 100]]
 
 class s1
 class s2
diff -r cc6e281d8f72 -r 0a36825b16c1 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Fri Aug 27 02:08:36 2010 +0800
+++ b/Nominal/NewParser.thy	Fri Aug 27 03:37:17 2010 +0800
@@ -434,7 +434,7 @@
 
   val alpha_bn_rsp = 
     if get_STEPS lthy > 20
-    then raw_alpha_bn_rsp alpha_bn_equivp_thms alpha_bn_imp_thms
+    then raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp_thms alpha_bn_imp_thms
     else raise TEST lthy6 
 
   (* noting the quot_respects lemmas *)
diff -r cc6e281d8f72 -r 0a36825b16c1 Nominal/ROOT.ML
--- a/Nominal/ROOT.ML	Fri Aug 27 02:08:36 2010 +0800
+++ b/Nominal/ROOT.ML	Fri Aug 27 03:37:17 2010 +0800
@@ -1,21 +1,19 @@
-quick_and_dirty := true;
 
-(*
+
 no_document use_thys
-   ["Ex/Lambda",
-    "Ex/LF",
-    "Ex/SingleLet",
-    "Ex/Ex1rec",
-    "Ex/Ex2",
-    "Ex/Ex3",
-    "Ex/ExLet",
-    "Ex/ExLetRec",
-    "Ex/TypeSchemes",
-    "Ex/Modules",
+   ["Ex/Classical",    
+    "Ex/CoreHaskell",
     "Ex/ExPS3",
     "Ex/ExPS7",
-    "Ex/CoreHaskell",
-    "Ex/Test"(*,
-    "Manual/Term4"*)
+    "Ex/ExPS8",
+    "Ex/LF",
+    "Ex/Lambda",
+    "Ex/Let",
+    "Ex/LetPat",
+    "Ex/LetRec",
+    "Ex/LetRec2",
+    "Ex/Modules",
+    "Ex/SingleLet",
+    "Ex/TypeSchemes",
+    "Ex/TypeVarsTest"
     ];
-*)
\ No newline at end of file
diff -r cc6e281d8f72 -r 0a36825b16c1 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Fri Aug 27 02:08:36 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Fri Aug 27 03:37:17 2010 +0800
@@ -29,7 +29,7 @@
     term list -> thm -> thm list -> Proof.context -> thm list
   val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list
   val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list
-  val raw_alpha_bn_rsp: thm list -> thm list -> thm list
+  val raw_alpha_bn_rsp: term list -> thm list -> thm list -> thm list
 
   val mk_funs_rsp: thm -> thm
   val mk_alpha_permute_rsp: thm -> thm 
@@ -703,12 +703,25 @@
   @{lemma "[|equivp Q; !!x y. R x y ==> Q x y|] ==> (R ===> R ===> op =) Q Q"
     by (simp only: fun_rel_def equivp_def, metis)}
 
-fun raw_alpha_bn_rsp alpha_bn_equivp alpha_bn_imps =
+
+(* we have to reorder the alpha_bn_imps theorems in order
+   to be in order with alpha_bn_trms *)
+fun raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp alpha_bn_imps =
 let
+  fun mk_map thm =
+    thm |> `prop_of
+        |>> List.last  o snd o strip_comb
+        |>> HOLogic.dest_Trueprop
+        |>> head_of
+        |>> fst o dest_Const
+
+  val alpha_bn_imps' = 
+    map (lookup (map mk_map alpha_bn_imps) o fst o dest_Const) alpha_bn_trms
+
   fun mk_thm thm1 thm2 = 
     (forall_intr_vars thm2) COMP (thm1 RS rsp_equivp)
 in
-  map2 mk_thm alpha_bn_equivp alpha_bn_imps
+  map2 mk_thm alpha_bn_equivp alpha_bn_imps'
 end