# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1234456505 0
# Node ID 3798baeee55f4147f16de6d9823d003d6b5e263f
# Parent  12533bb49615b0efa304904abab517aeffd9e4ea
rearranged some functions

diff -r 12533bb49615 -r 3798baeee55f CookBook/Package/simple_inductive_package.ML
--- a/CookBook/Package/simple_inductive_package.ML	Thu Feb 12 16:09:42 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML	Thu Feb 12 16:35:05 2009 +0000
@@ -17,8 +17,33 @@
 structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE =
 struct
 
+fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P 
 
-fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P 
+(* @chunk definitions *) 
+fun define_aux s ((binding, syn), (attr, trm)) lthy =
+let 
+  val ((_, (_ , thm)), lthy) = LocalTheory.define s ((binding, syn), (attr, trm)) lthy
+in 
+  (thm, lthy) 
+end
+
+fun DEFINITION params' rules preds preds' Tss lthy =
+let
+  val rules' = map (ObjectLogic.atomize_term (ProofContext.theory_of lthy)) rules
+in
+  fold_map (fn ((((R, _), syn), pred), Ts) =>
+    let 
+      val zs = map Free (Variable.variant_frees lthy rules' (map (pair "z") Ts))
+        
+      val t0 = list_comb (pred, zs);
+      val t1 = fold_rev (curry HOLogic.mk_imp) rules' t0;
+      val t2 = fold_rev mk_all preds' t1;      
+      val t3 = fold_rev lambda (params' @ zs) t2;
+    in
+      define_aux Thm.internalK ((R, syn), (Attrib.empty_binding, t3))
+    end) (preds ~~ preds' ~~ Tss) lthy
+end
+(* @end *)
 
 fun inst_spec ct = 
   Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec};
@@ -26,6 +51,7 @@
 val all_elims = fold (fn ct => fn th => th RS inst_spec ct);
 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp});
 
+
 (* @chunk induction_rules *)
 fun INDUCTION rules preds' Tss defs lthy1 lthy2 =
 let
@@ -90,32 +116,6 @@
 end
 (* @end *)
 
-(* @chunk definitions *) 
-fun define_aux s ((binding, syn), (attr, trm)) lthy =
-let 
-  val ((_, (_ , thm)), lthy) = LocalTheory.define s ((binding, syn), (attr, trm)) lthy
-in 
-  (thm, lthy) 
-end
-
-fun DEFINITION params' rules preds preds' Tss lthy =
-let
-  val rules' = map (ObjectLogic.atomize_term (ProofContext.theory_of lthy)) rules
-in
-  fold_map (fn ((((R, _), syn), pred), Ts) =>
-    let 
-      val zs = map Free (Variable.variant_frees lthy rules' (map (pair "z") Ts))
-        
-      val t0 = list_comb (pred, zs);
-      val t1 = fold_rev (curry HOLogic.mk_imp) rules' t0;
-      val t2 = fold_rev mk_all preds' t1;      
-      val t3 = fold_rev lambda (params' @ zs) t2;
-    in
-      define_aux Thm.internalK ((R, syn), (Attrib.empty_binding, t3))
-    end) (preds ~~ preds' ~~ Tss) lthy
-end
-(* @end *)
-
 (* @chunk add_inductive_i *)
 fun add_inductive_i preds params specs lthy =
   let
diff -r 12533bb49615 -r 3798baeee55f cookbook.pdf
Binary file cookbook.pdf has changed