# HG changeset patch
# User huffman
# Date 1267206956 28800
# Node ID debbdbb45fbc3be5dc1b0f379e63e13b367138c8
# Parent  cf8c5a751a9ad1f3ff3ca5b7afc3c543b943fc59
reorder sections

diff -r cf8c5a751a9a -r debbdbb45fbc src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Fri Feb 26 09:47:37 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Fri Feb 26 09:55:56 2010 -0800
@@ -17,8 +17,8 @@
            con_betas : thm list,
            con_compacts : thm list,
            con_rews : thm list,
-           sel_rews : thm list }
-         * theory;
+           sel_rews : thm list
+         } * theory;
 end;
 
 
@@ -307,6 +307,124 @@
 end;
 
 (******************************************************************************)
+(************* definitions and theorems for constructor functions *************)
+(******************************************************************************)
+
+fun add_constructors
+    (spec : (binding * (bool * 'b * typ) list * mixfix) list)
+    (abs_const : term)
+    (iso_locale : thm)
+    (thy : theory)
+    =
+  let
+
+    (* get theorems about rep and abs *)
+    val abs_strict = iso_locale RS @{thm iso.abs_strict};
+
+    (* define constructor functions *)
+    val ((con_consts, con_defs), thy) =
+      let
+        fun vars_of args =
+          let
+            val Ts = map (fn (lazy,sel,T) => T) args;
+            val ns = Datatype_Prop.make_tnames Ts;
+          in
+            map Free (ns ~~ Ts)
+          end;
+        fun one_arg (lazy,_,_) var = if lazy then mk_up var else var;
+        fun one_con (_,args,_) = mk_stuple (map2 one_arg args (vars_of args));
+        fun mk_abs t = abs_const ` t;
+        val rhss = map mk_abs (mk_sinjects (map one_con spec));
+        fun mk_def (bind, args, mx) rhs =
+          (bind, big_lambdas (vars_of args) rhs, mx);
+      in
+        define_consts (map2 mk_def spec rhss) thy
+      end;
+
+    (* prove beta reduction rules for constructors *)
+    val con_betas = map (beta_of_def thy) con_defs;
+
+    (* replace bindings with terms in constructor spec *)
+    val spec' : (term * (bool * typ) list) list =
+      let fun one_arg (lazy, sel, T) = (lazy, T);
+          fun one_con con (b, args, mx) = (con, map one_arg args);
+      in map2 one_con con_consts spec end;
+
+    (* prove compactness rules for constructors *)
+    val con_compacts =
+      let
+        val rules = @{thms compact_sinl compact_sinr compact_spair
+                           compact_up compact_ONE};
+        val tacs =
+          [rtac (iso_locale RS @{thm iso.compact_abs}) 1,
+           REPEAT (resolve_tac rules 1 ORELSE atac 1)];
+        fun con_compact (con, args) =
+          let
+            val Ts = map snd args;
+            val ns = Datatype_Prop.make_tnames Ts;
+            val vs = map Free (ns ~~ Ts);
+            val con_app = list_ccomb (con, vs);
+            val concl = mk_trp (mk_compact con_app);
+            val assms = map (mk_trp o mk_compact) vs;
+            val goal = Logic.list_implies (assms, concl);
+          in
+            prove thy con_betas goal (K tacs)
+          end;
+      in
+        map con_compact spec'
+      end;
+
+    (* prove strictness rules for constructors *)
+    local
+      fun con_strict (con, args) = 
+        let
+          val rules = abs_strict :: @{thms con_strict_rules};
+          val Ts = map snd args;
+          val ns = Datatype_Prop.make_tnames Ts;
+          val vs = map Free (ns ~~ Ts);
+          val nonlazy = map snd (filter_out fst (map fst args ~~ vs));
+          fun one_strict v' =
+            let
+              val UU = mk_bottom (Term.fastype_of v');
+              val vs' = map (fn v => if v = v' then UU else v) vs;
+              val goal = mk_trp (mk_undef (list_ccomb (con, vs')));
+              val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
+            in prove thy con_betas goal (K tacs) end;
+        in map one_strict nonlazy end;
+
+      fun con_defin (con, args) =
+        let
+          fun iff_disj (t, []) = HOLogic.mk_not t
+            | iff_disj (t, ts) = mk_eq (t, foldr1 HOLogic.mk_disj ts);
+          val Ts = map snd args;
+          val ns = Datatype_Prop.make_tnames Ts;
+          val vs = map Free (ns ~~ Ts);
+          val nonlazy = map snd (filter_out fst (map fst args ~~ vs));
+          val lhs = mk_undef (list_ccomb (con, vs));
+          val rhss = map mk_undef nonlazy;
+          val goal = mk_trp (iff_disj (lhs, rhss));
+          val rule1 = iso_locale RS @{thm iso.abs_defined_iff};
+          val rules = rule1 :: @{thms con_defined_iff_rules};
+          val tacs = [simp_tac (HOL_ss addsimps rules) 1];
+        in prove thy con_betas goal (K tacs) end;
+    in
+      val con_stricts = maps con_strict spec';
+      val con_defins = map con_defin spec';
+      val con_rews = con_stricts @ con_defins;
+    end;
+
+    val result =
+      {
+        con_consts = con_consts,
+        con_betas = con_betas,
+        con_compacts = con_compacts,
+        con_rews = con_rews
+      };
+  in
+    (result, thy)
+  end;
+
+(******************************************************************************)
 (************** definitions and theorems for selector functions ***************)
 (******************************************************************************)
 
@@ -450,124 +568,6 @@
   end
 
 (******************************************************************************)
-(************* definitions and theorems for constructor functions *************)
-(******************************************************************************)
-
-fun add_constructors
-    (spec : (binding * (bool * 'b * typ) list * mixfix) list)
-    (abs_const : term)
-    (iso_locale : thm)
-    (thy : theory)
-    =
-  let
-
-    (* get theorems about rep and abs *)
-    val abs_strict = iso_locale RS @{thm iso.abs_strict};
-
-    (* define constructor functions *)
-    val ((con_consts, con_defs), thy) =
-      let
-        fun vars_of args =
-          let
-            val Ts = map (fn (lazy,sel,T) => T) args;
-            val ns = Datatype_Prop.make_tnames Ts;
-          in
-            map Free (ns ~~ Ts)
-          end;
-        fun one_arg (lazy,_,_) var = if lazy then mk_up var else var;
-        fun one_con (_,args,_) = mk_stuple (map2 one_arg args (vars_of args));
-        fun mk_abs t = abs_const ` t;
-        val rhss = map mk_abs (mk_sinjects (map one_con spec));
-        fun mk_def (bind, args, mx) rhs =
-          (bind, big_lambdas (vars_of args) rhs, mx);
-      in
-        define_consts (map2 mk_def spec rhss) thy
-      end;
-
-    (* prove beta reduction rules for constructors *)
-    val con_betas = map (beta_of_def thy) con_defs;
-
-    (* replace bindings with terms in constructor spec *)
-    val spec' : (term * (bool * typ) list) list =
-      let fun one_arg (lazy, sel, T) = (lazy, T);
-          fun one_con con (b, args, mx) = (con, map one_arg args);
-      in map2 one_con con_consts spec end;
-
-    (* prove compactness rules for constructors *)
-    val con_compacts =
-      let
-        val rules = @{thms compact_sinl compact_sinr compact_spair
-                           compact_up compact_ONE};
-        val tacs =
-          [rtac (iso_locale RS @{thm iso.compact_abs}) 1,
-           REPEAT (resolve_tac rules 1 ORELSE atac 1)];
-        fun con_compact (con, args) =
-          let
-            val Ts = map snd args;
-            val ns = Datatype_Prop.make_tnames Ts;
-            val vs = map Free (ns ~~ Ts);
-            val con_app = list_ccomb (con, vs);
-            val concl = mk_trp (mk_compact con_app);
-            val assms = map (mk_trp o mk_compact) vs;
-            val goal = Logic.list_implies (assms, concl);
-          in
-            prove thy con_betas goal (K tacs)
-          end;
-      in
-        map con_compact spec'
-      end;
-
-    (* prove strictness rules for constructors *)
-    local
-      fun con_strict (con, args) = 
-        let
-          val rules = abs_strict :: @{thms con_strict_rules};
-          val Ts = map snd args;
-          val ns = Datatype_Prop.make_tnames Ts;
-          val vs = map Free (ns ~~ Ts);
-          val nonlazy = map snd (filter_out fst (map fst args ~~ vs));
-          fun one_strict v' =
-            let
-              val UU = mk_bottom (Term.fastype_of v');
-              val vs' = map (fn v => if v = v' then UU else v) vs;
-              val goal = mk_trp (mk_undef (list_ccomb (con, vs')));
-              val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
-            in prove thy con_betas goal (K tacs) end;
-        in map one_strict nonlazy end;
-
-      fun con_defin (con, args) =
-        let
-          fun iff_disj (t, []) = HOLogic.mk_not t
-            | iff_disj (t, ts) = mk_eq (t, foldr1 HOLogic.mk_disj ts);
-          val Ts = map snd args;
-          val ns = Datatype_Prop.make_tnames Ts;
-          val vs = map Free (ns ~~ Ts);
-          val nonlazy = map snd (filter_out fst (map fst args ~~ vs));
-          val lhs = mk_undef (list_ccomb (con, vs));
-          val rhss = map mk_undef nonlazy;
-          val goal = mk_trp (iff_disj (lhs, rhss));
-          val rule1 = iso_locale RS @{thm iso.abs_defined_iff};
-          val rules = rule1 :: @{thms con_defined_iff_rules};
-          val tacs = [simp_tac (HOL_ss addsimps rules) 1];
-        in prove thy con_betas goal (K tacs) end;
-    in
-      val con_stricts = maps con_strict spec';
-      val con_defins = map con_defin spec';
-      val con_rews = con_stricts @ con_defins;
-    end;
-
-    val result =
-      {
-        con_consts = con_consts,
-        con_betas = con_betas,
-        con_compacts = con_compacts,
-        con_rews = con_rews
-      };
-  in
-    (result, thy)
-  end;
-
-(******************************************************************************)
 (******************************* main function ********************************)
 (******************************************************************************)