diff -r bfa48c000aa7 -r 478c5648e73f Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Wed Dec 22 23:12:51 2010 +0000
+++ b/Nominal/Nominal2.thy	Thu Dec 23 00:22:41 2010 +0000
@@ -18,41 +18,6 @@
 
 text {* TEST *}
 
-ML {*
-fun strip_outer_params (Const("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T)
-  | strip_outer_params B = ([], B)
-
-fun strip_params_prems_concl trm =
-  let
-    val (params, body) = strip_outer_params trm
-    val (prems, concl) = Logic.strip_horn body
-  in
-    (params, prems, concl)
-  end
-
-fun list_params_prems_concl params prems concl =
-  Logic.list_implies (prems, concl)
-  |> fold_rev mk_all params
-
-fun mk_binop_env tys c (t, u) =
-  let val ty = fastype_of1 (tys, t) in
-    Const (c, [ty, ty] ---> ty) $ t $ u
-  end
-
-fun mk_union_env tys (t1, @{term "{}::atom set"}) = t1
-  | mk_union_env tys (@{term "{}::atom set"}, t2) = t2
-  | mk_union_env tys (t1, @{term "set ([]::atom list)"}) = t1
-  | mk_union_env tys (@{term "set ([]::atom list)"}, t2) = t2
-  | mk_union_env tys (t1, t2) = mk_binop_env tys @{const_name "sup"} (t1, t2)  
-
-fun fold_left f [] z = z
-  | fold_left f [x] z = x
-  | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z
-
-fun fold_union_env tys trms = fold_left (mk_union_env tys) trms @{term "{}::atom set"} 
-*}
-
-
 
 ML {*
 (* adds a freshness condition to the assumptions *)
@@ -79,7 +44,7 @@
           |> (fn t => mk_fresh_star t c)
           |> (fn t => HOLogic.mk_Trueprop t :: prems)
   in
-    list_params_prems_concl params prems' concl
+    mk_full_horn params prems' concl
   end  
 *}
 
@@ -119,77 +84,20 @@
 *} 
 
 ML {*
-(* derives an abs_eq theorem of the form 
-
-   Exists q. [as].x = [p o as].(q o x)  for non-recursive binders 
-   Exists q. [as].x = [q o as].(q o x)  for recursive binders
-*)
-fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns
-  (bclause as (BC (bmode, binders, bodies))) =
-  case binders of
-    [] => [] 
-  | _ =>
-      let
-        val flag = is_recursive_binder bclause
-        val binder_trm = comb_binders ctxt bmode parms binders
-        val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies)
-        val body_ty = fastype_of body_trm
-
-        fun mk_abs cnst_name ty1 ty2 =
-          Const (cnst_name, [ty1, body_ty] ---> Type (ty2, [body_ty]))
-
-        val abs_const = 
-          case bmode of
-            Lst => mk_abs @{const_name "Abs_lst"} @{typ "atom list"} @{type_name abs_lst}
-          | Set => mk_abs @{const_name "Abs_set"} @{typ "atom set"}  @{type_name abs_set}
-          | Res => mk_abs @{const_name "Abs_res"} @{typ "atom set"}  @{type_name abs_res}
-
-        val abs_lhs = abs_const $ binder_trm $ body_trm
-        val abs_rhs = 
-          if flag
-          then abs_const $ mk_perm p binder_trm $ mk_perm (Bound 0) body_trm
-          else abs_const $ mk_perm (Bound 0) binder_trm $ mk_perm (Bound 0) body_trm
-        
-        val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs)
-        val peq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) 
+fun abs_const bmode ty =
+  let
+    val (const_name, binder_ty, abs_ty) = 
+      case bmode of
+        Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst})
+      | Set => (@{const_name "Abs_set"}, @{typ "atom set"},  @{type_name abs_set})
+      | Res => (@{const_name "Abs_res"}, @{typ "atom set"},  @{type_name abs_res})
+  in
+    Const (const_name, [binder_ty, ty] ---> Type (abs_ty, [ty]))
+  end
 
-        val goal = HOLogic.mk_conj (abs_eq, peq)
-          |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t))
-          |> HOLogic.mk_Trueprop  
- 
-        val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt}
-          @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset
-          fresh_star_set} @ @{thms finite.intros finite_fset}
-  
-        val tac1 = 
-          if flag
-          then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}
-          else resolve_tac @{thms Abs_rename_set  Abs_rename_res  Abs_rename_lst}
-        
-        val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss] 
-     in
-       [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2)))
-         |> (if flag
-             then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []
-             else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns [])
-       ]
-     end
-*}
+fun mk_abs bmode trm1 trm2 =
+  abs_const bmode (fastype_of trm2) $ trm1 $ trm2  
 
-ML {*
-fun conj_tac tac i =
-  let
-     fun select (t, i) =
-       case t of
-         @{term "Trueprop"} $ t' => select (t', i)
-       | @{term "op \<and>"} $ _ $ _ => (rtac @{thm conjI} THEN' RANGE [conj_tac tac, conj_tac tac]) i
-       | _ => tac i
-  in
-    SUBGOAL select i
-  end
-*}
-
-ML {*
 fun is_abs_eq thm =
   let
     fun is_abs trm =
@@ -207,6 +115,57 @@
   end
 *}
 
+
+
+ML {*
+(* derives an abs_eq theorem of the form 
+
+   Exists q. [as].x = [p o as].(q o x)  for non-recursive binders 
+   Exists q. [as].x = [q o as].(q o x)  for recursive binders
+*)
+fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns
+  (bclause as (BC (bmode, binders, bodies))) =
+  case binders of
+    [] => [] 
+  | _ =>
+      let
+        val rec_flag = is_recursive_binder bclause
+        val binder_trm = comb_binders ctxt bmode parms binders
+        val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies)
+
+        val abs_lhs = mk_abs bmode binder_trm body_trm
+        val abs_rhs = 
+          if rec_flag
+          then mk_abs bmode (mk_perm (Bound 0) binder_trm) (mk_perm (Bound 0) body_trm)
+          else mk_abs bmode (mk_perm p binder_trm) (mk_perm (Bound 0) body_trm)
+        
+        val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs)
+        val peq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) 
+
+        val goal = HOLogic.mk_conj (abs_eq, peq)
+          |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t))
+          |> HOLogic.mk_Trueprop  
+ 
+        val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt}
+          @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset
+          fresh_star_set} @ @{thms finite.intros finite_fset}
+  
+        val tac1 = 
+          if rec_flag
+          then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'}
+          else resolve_tac @{thms Abs_rename_set  Abs_rename_res  Abs_rename_lst}
+        
+        val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss] 
+     in
+       [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2)))
+         |> (if rec_flag
+             then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []
+             else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) ]
+     end
+*}
+
+
+
 lemma setify:
   shows "xs = ys \<Longrightarrow> set xs = set ys" 
   by simp
@@ -241,43 +200,27 @@
 
             val (abs_eqs, peqs) = split_filter is_abs_eq eqs
 
-            val fprops' = map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops
-            val fprops'' = map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops
+            val fprops' = 
+              map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops
+              @ map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops
 
-            val _ = tracing ("prem:\n" ^ (Syntax.string_of_term ctxt'' o prop_of) prem)
-            val _ = tracing ("prems:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) prems))
-            val _ = tracing ("fprop':\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) fprops'))
-            val _ = tracing ("fprop'':\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) fprops''))
-            val _ = tracing ("abseq:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) abs_eqs))
-            val _ = tracing ("peqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt'' o prop_of) peqs))
-              
- 
-            val tac1 = EVERY'
+            (* for freshness conditions *) 
+            val tac1 = SOLVED' (EVERY'
               [ simp_tac (HOL_basic_ss addsimps peqs),
                 rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}),
-                K (print_tac "before solving freshness"), 
-                conj_tac (TRY o DETERM o resolve_tac (fprops' @ fprops'')) ] 
+                conj_tac (DETERM o resolve_tac fprops') ]) 
 
-            val tac2 = EVERY' 
+            (* for equalities between constructors *)
+            val tac2 = SOLVED' (EVERY' 
               [ rtac (@{thm ssubst} OF prems),
                 rewrite_goal_tac (map safe_mk_equiv eq_iff_thms),
-                K (print_tac "before substituting"),
                 rewrite_goal_tac (map safe_mk_equiv abs_eqs),
-                K (print_tac "after substituting"),
-                conj_tac (TRY o DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)),
-                K (print_tac "end") 
-              ] 
+                conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ]) 
 
+            (* proves goal "P" *)
             val side_thm = Goal.prove ctxt'' [] [] (term_of concl)
-              (fn _ => (* Skip_Proof.cheat_tac (ProofContext.theory_of ctxt'') *)
-                       EVERY 
-                        [ rtac prem 1,
-                          print_tac "after applying prem",
-                          RANGE [SOLVED' tac1, SOLVED' tac2] 1,
-                          print_tac "final" ] )
+              (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ]))
               |> singleton (ProofContext.export ctxt'' ctxt)  
-
-            val _ = tracing ("side_thm:\n" ^ (Syntax.string_of_term ctxt o prop_of) side_thm)
           in
             rtac side_thm 1 
           end) ctxt
@@ -295,13 +238,14 @@
     val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
     val c = Free (c, TFree (a, @{sort fs}))
 
-    val (ecases, main_concls) = exhausts' (* ecases or of the form (params, prems, concl) *)
+    val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *)
       |> map prop_of
       |> map Logic.strip_horn
       |> split_list
-      |>> (map o map) strip_params_prems_concl     
 
-    val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases bclausesss
+    val ecases' = (map o map) strip_full_horn ecases
+
+    val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases' bclausesss
    
     fun tac bclausess exhaust {prems, context} =
       case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas