diff -r 9909cc3566c5 -r 636de31888a6 Nominal-General/nominal_eqvt.ML
--- a/Nominal-General/nominal_eqvt.ML	Wed Apr 14 15:02:07 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML	Wed Apr 14 16:05:58 2010 +0200
@@ -1,5 +1,5 @@
 (*  Title:      nominal_eqvt.ML
-    Author:     Stefan Berghofer
+    Author:     Stefan Berghofer (original code)
     Author:     Christian Urban
 
     Automatic proofs for equivariance of inductive predicates.
@@ -7,7 +7,9 @@
 
 signature NOMINAL_EQVT =
 sig
-  val eqvt_rel_tac : xstring -> Proof.context -> local_theory
+  val equivariance: string -> Proof.context -> local_theory
+  val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic
+  val eqvt_rel_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic
 end
 
 structure Nominal_Eqvt : NOMINAL_EQVT =
@@ -23,6 +25,13 @@
 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
   (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
 
+
+(** 
+ proves F[f t] from F[t] which is the given theorem  
+  - F needs to be monotone
+  - f returns either SOME for a term it fires 
+    and NONE elsewhere 
+**)
 fun map_term f t = 
   (case f t of
      NONE => map_term' f t 
@@ -48,24 +57,21 @@
     REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]
 end
 
-(* 
- proves F[f t] from F[t] where F[t] is the given theorem  
-  
-  - F needs to be monotone
-  - f returns either SOME for a term it fires 
-    and NONE elsewhere 
-*)
 fun map_thm ctxt f tac thm =
 let
   val opt_goal_trm = map_term f (prop_of thm)
-  fun prove goal = 
-    Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm)
 in
   case opt_goal_trm of
     NONE => thm
-  | SOME goal => prove goal
+  | SOME goal =>
+     Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) 
 end
 
+(*
+ inductive premises can be of the form
+ R ... /\ P ...; split_conj picks out
+ the part P ...
+*)
 fun transform_prem ctxt names thm =
 let
   fun split_conj names (Const ("op &", _) $ p $ q) = 
@@ -77,36 +83,50 @@
   map_thm ctxt (split_conj names) (etac conjunct2 1) thm
 end
 
-fun single_case_tac ctxt pred_names pi intro  = 
+
+(** equivariance tactics **)
+
+fun eqvt_rel_case_tac ctxt pred_names pi intro  = 
 let
   val thy = ProofContext.theory_of ctxt
   val cpi = Thm.cterm_of thy (mk_minus pi)
   val rule = Drule.instantiate' [] [SOME cpi] @{thm permute_boolE}
+  val permute_cancel = @{thms permute_minus_cancel(2)}
 in
   eqvt_strict_tac ctxt [] [] THEN' 
-  SUBPROOF (fn {prems, context as ctxt, ...} =>
+  SUBPROOF (fn {prems, context, ...} =>
     let
       val prems' = map (transform_prem ctxt pred_names) prems
       val side_cond_tac = EVERY' 
-        [ rtac rule, 
-          eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [],
+        [ rtac rule, eqvt_strict_tac context permute_cancel [],
           resolve_tac prems' ]
     in
-      HEADGOAL (rtac intro THEN_ALL_NEW (resolve_tac prems' ORELSE' side_cond_tac)) 
+      (rtac intro THEN_ALL_NEW (resolve_tac prems' ORELSE' side_cond_tac)) 1 
     end) ctxt
 end
 
+fun eqvt_rel_tac ctxt pred_names pi induct intros =
+let
+  val cases = map (eqvt_rel_case_tac ctxt pred_names pi) intros
+in
+  EVERY' (rtac induct :: cases)
+end
 
-fun prepare_pred params_no pi pred =
+
+(** equivariance procedure *)
+
+(* sets up goal and makes sure parameters
+   are untouched PROBLEM: this violates the 
+   form of eqvt lemmas *)
+fun prepare_goal params_no pi pred =
 let
   val (c, xs) = strip_comb pred;
   val (xs1, xs2) = chop params_no xs
 in
-  HOLogic.mk_imp 
-    (pred, list_comb (c, xs1 @ map (mk_perm pi) xs2))
+  HOLogic.mk_imp (pred, list_comb (c, xs1 @ map (mk_perm pi) xs2))
 end
 
-
+(* stores thm under name.eqvt and adds [eqvt]-attribute *)
 fun note_named_thm (name, thm) ctxt = 
 let
   val thm_name = Binding.qualified_name 
@@ -116,30 +136,28 @@
   Local_Theory.note ((thm_name, [attr]), [thm]) ctxt
 end
 
-
-fun eqvt_rel_tac pred_name ctxt = 
+fun equivariance pred_name ctxt = 
 let
   val thy = ProofContext.theory_of ctxt
   val ({names, ...}, {raw_induct, intrs, ...}) =
     Inductive.the_inductive ctxt (Sign.intern_const thy pred_name)
-  val raw_induct = atomize_induct ctxt raw_induct;
-  val intros = map atomize_intr intrs;
+  val raw_induct = atomize_induct ctxt raw_induct
+  val intros = map atomize_intr intrs
   val params_no = length (Inductive.params_of raw_induct)
-  val (([raw_concl], [raw_pi]), ctxt') = 
-    ctxt |> Variable.import_terms false [concl_of raw_induct] 
+  val (([raw_concl], [raw_pi]), ctxt') = ctxt 
+         |> Variable.import_terms false [concl_of raw_induct] 
          ||>> Variable.variant_fixes ["pi"]
   val pi = Free (raw_pi, @{typ perm})
   val preds = map (fst o HOLogic.dest_imp)
     (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl));
   val goal = HOLogic.mk_Trueprop 
-    (foldr1 HOLogic.mk_conj (map (prepare_pred params_no pi) preds))
-  val thm = Goal.prove ctxt' [] [] goal (fn {context,...} => 
-    HEADGOAL (EVERY' (rtac raw_induct :: map (single_case_tac context names pi) intros)))
-    |> singleton (ProofContext.export ctxt' ctxt)
-  val thms = map (fn th => zero_var_indexes (th RS mp)) (Datatype_Aux.split_conj_thm thm)
+    (foldr1 HOLogic.mk_conj (map (prepare_goal params_no pi) preds))
+  val thms = Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] [] goal 
+    (fn {context,...} => eqvt_rel_tac context names pi raw_induct intros 1)
+    |> singleton (ProofContext.export ctxt' ctxt))
+  val thms' = map (fn th => zero_var_indexes (th RS mp)) thms
 in
-   ctxt |> fold_map note_named_thm (names ~~ thms)
-        |> snd  
+  ctxt |> fold_map note_named_thm (names ~~ thms') |> snd  
 end
 
 
@@ -147,9 +165,8 @@
 
 val _ =
   OuterSyntax.local_theory "equivariance"
-    "prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl
-    (P.xname >> eqvt_rel_tac);
-
+    "prove equivariance for inductive predicate involving nominal datatypes" 
+      K.thy_decl (P.xname >> equivariance);
 end;
 
 end (* structure *)
\ No newline at end of file