# HG changeset patch
# User huffman
# Date 1287088111 25200
# Node ID 2eff1cbc1ccb2901db7f846ada7f74fe37034162
# Parent  2fda967490810908068534f5cd28ef19450bf352
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors

diff -r 2fda96749081 -r 2eff1cbc1ccb src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu Oct 14 10:16:46 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu Oct 14 13:28:31 2010 -0700
@@ -854,6 +854,7 @@
     (thy : theory) =
   let
     val dname = Binding.name_of dbind;
+    val _ = writeln ("Proving isomorphism properties of domain "^dname^" ...");
 
     (* retrieve facts about rep/abs *)
     val lhsT = #absT iso_info;
@@ -865,6 +866,7 @@
     val abs_strict = iso_locale RS @{thm iso.abs_strict};
     val rep_defined_iff = iso_locale RS @{thm iso.rep_defined_iff};
     val abs_defined_iff = iso_locale RS @{thm iso.abs_defined_iff};
+    val iso_rews = [abs_iso_thm, rep_iso_thm, abs_strict, rep_strict];
 
     (* qualify constants and theorems with domain name *)
     val thy = Sign.add_path dname thy;
@@ -878,7 +880,8 @@
       in
         add_constructors con_spec abs_const iso_locale thy
       end;
-    val {con_consts, con_betas, exhaust, ...} = con_result;
+    val {con_consts, con_betas, nchotomy, exhaust, compacts, con_rews,
+          inverts, injects, dist_les, dist_eqs} = con_result;
 
     (* define case combinator *)
     val ((case_const : typ -> term, cases : thm list), thy) =
@@ -928,17 +931,43 @@
     (* restore original signature path *)
     val thy = Sign.parent_path thy;
 
+    (* bind theorem names in global theory *)
+    val (_, thy) =
+      let
+        fun qualified name = Binding.qualified true name dbind;
+        val names = "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec;
+        val dname = fst (dest_Type lhsT);
+        val simp = Simplifier.simp_add;
+        val case_names = Rule_Cases.case_names names;
+        val cases_type = Induct.cases_type dname;
+      in
+        Global_Theory.add_thmss [
+          ((qualified "iso_rews"  , iso_rews    ), [simp]),
+          ((qualified "nchotomy"  , [nchotomy]  ), []),
+          ((qualified "exhaust"   , [exhaust]   ), [case_names, cases_type]),
+          ((qualified "when_rews" , cases       ), [simp]),
+          ((qualified "compacts"  , compacts    ), [simp]),
+          ((qualified "con_rews"  , con_rews    ), [simp]),
+          ((qualified "sel_rews"  , sel_thms    ), [simp]),
+          ((qualified "dis_rews"  , dis_thms    ), [simp]),
+          ((qualified "dist_les"  , dist_les    ), [simp]),
+          ((qualified "dist_eqs"  , dist_eqs    ), [simp]),
+          ((qualified "inverts"   , inverts     ), [simp]),
+          ((qualified "injects"   , injects     ), [simp]),
+          ((qualified "match_rews", match_thms  ), [simp])] thy
+      end;
+
     val result =
       { con_consts = con_consts,
         con_betas = con_betas,
-        nchotomy = #nchotomy con_result,
+        nchotomy = nchotomy,
         exhaust = exhaust,
-        compacts = #compacts con_result,
-        con_rews = #con_rews con_result,
-        inverts = #inverts con_result,
-        injects = #injects con_result,
-        dist_les = #dist_les con_result,
-        dist_eqs = #dist_eqs con_result,
+        compacts = compacts,
+        con_rews = con_rews,
+        inverts = inverts,
+        injects = injects,
+        dist_les = dist_les,
+        dist_eqs = dist_eqs,
         cases = cases,
         sel_rews = sel_thms,
         dis_rews = dis_thms,
diff -r 2fda96749081 -r 2eff1cbc1ccb src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Thu Oct 14 10:16:46 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Thu Oct 14 13:28:31 2010 -0700
@@ -189,18 +189,18 @@
     val eqs : eq list =
         map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
 
-    val ((rewss, take_rews), theorems_thy) =
+    val (constr_infos, thy) =
         thy
-          |> fold_map (fn (((dbind, eq), (_,cs)), info) =>
-                Domain_Theorems.theorems (eq, eqs) dbind cs info take_info)
-             (dbinds ~~ eqs ~~ eqs' ~~ iso_infos)
-          ||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info;
+          |> fold_map (fn ((dbind, (_,cs)), info) =>
+                Domain_Constructors.add_domain_constructors dbind cs info)
+             (dbinds ~~ eqs' ~~ iso_infos);
+
+    val (take_rews, theorems_thy) =
+        thy
+          |> Domain_Theorems.comp_theorems (comp_dbind, eqs)
+              (dbinds ~~ map snd eqs') iso_infos take_info constr_infos;
   in
     theorems_thy
-      |> Global_Theory.add_thmss
-           [((Binding.qualified true "rews" comp_dbind,
-              flat rewss @ take_rews), [])]
-      |> snd
   end;
 
 fun define_isos (spec : (binding * mixfix * (typ * typ)) list) =
diff -r 2fda96749081 -r 2eff1cbc1ccb src/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Thu Oct 14 10:16:46 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Thu Oct 14 13:28:31 2010 -0700
@@ -303,7 +303,7 @@
         val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
         val take_0_thm = Goal.prove_global thy [] [] goal (K tac);
       in
-        add_qualified_thm "take_0" (dbind, take_0_thm) thy
+        add_qualified_simp_thm "take_0" (dbind, take_0_thm) thy
       end;
     val (take_0_thms, thy) =
       fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy;
@@ -373,7 +373,7 @@
             Drule.zero_var_indexes
               (@{thm deflation_strict} OF [deflation_take]);
       in
-        add_qualified_thm "take_strict" (dbind, take_strict_thm) thy
+        add_qualified_simp_thm "take_strict" (dbind, take_strict_thm) thy
       end;
     val (take_strict_thms, thy) =
       fold_map prove_take_strict
diff -r 2fda96749081 -r 2eff1cbc1ccb src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 10:16:46 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 13:28:31 2010 -0700
@@ -9,17 +9,12 @@
 
 signature DOMAIN_THEOREMS =
 sig
-  val theorems:
-      Domain_Library.eq * Domain_Library.eq list ->
-      binding ->
-      (binding * (bool * binding option * typ) list * mixfix) list ->
-      Domain_Take_Proofs.iso_info ->
-      Domain_Take_Proofs.take_induct_info ->
-      theory -> thm list * theory;
-
   val comp_theorems :
       binding * Domain_Library.eq list ->
+      (binding * (binding * (bool * binding option * typ) list * mixfix) list) list ->
+      Domain_Take_Proofs.iso_info list ->
       Domain_Take_Proofs.take_induct_info ->
+      Domain_Constructors.constr_info list ->
       theory -> thm list * theory
 
   val quiet_mode: bool Unsynchronized.ref;
@@ -103,131 +98,66 @@
 (******************************************************************************)
 
 fun take_theorems
-    (((dname, _), cons) : eq, eqs : eq list)
-    (iso_info : Domain_Take_Proofs.iso_info)
+    (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
+    (iso_infos : Domain_Take_Proofs.iso_info list)
     (take_info : Domain_Take_Proofs.take_induct_info)
-    (result : Domain_Constructors.constr_info)
-    (thy : theory) =
+    (constr_infos : Domain_Constructors.constr_info list)
+    (thy : theory) : thm list list * theory =
 let
-  val map_tab = Domain_Take_Proofs.get_map_tab thy;
+  open HOLCF_Library;
 
-  val ax_abs_iso = #abs_inverse iso_info;
-  val {take_Suc_thms, deflation_take_thms, ...} = take_info;
-  val con_appls = #con_betas result;
-
-  local
-    fun ga s dn = Global_Theory.get_thm thy (dn ^ "." ^ s);
-  in
-    val ax_take_0      = ga "take_0" dname;
-    val ax_take_strict = ga "take_strict" dname;
-  end;
-
-  fun dc_take dn = %%:(dn^"_take");
-  val dnames = map (fst o fst) eqs;
+  val {take_consts, take_Suc_thms, deflation_take_thms, ...} = take_info;
   val deflation_thms = Domain_Take_Proofs.get_deflation_thms thy;
 
-  fun copy_of_dtyp tab r dt =
-      if Datatype_Aux.is_rec_type dt then copy tab r dt else ID
-  and copy tab r (Datatype_Aux.DtRec i) = r i
-    | copy tab r (Datatype_Aux.DtTFree a) = ID
-    | copy tab r (Datatype_Aux.DtType (c, ds)) =
-      case Symtab.lookup tab c of
-        SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds)
-      | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
+  val n = Free ("n", @{typ nat});
+  val n' = @{const Suc} $ n;
 
-  fun one_take_app (con, args) =
+  local
+    val newTs = map #absT iso_infos;
+    val subs = newTs ~~ map (fn t => t $ n) take_consts;
+    fun is_ID (Const (c, _)) = (c = @{const_name ID})
+      | is_ID _              = false;
+  in
+    fun map_of_arg v T =
+      let val m = Domain_Take_Proofs.map_of_typ thy subs T;
+      in if is_ID m then v else mk_capply (m, v) end;
+  end
+
+  fun prove_take_apps
+      ((((dbind, spec), iso_info), take_const), constr_info) thy =
     let
-      fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
-      fun one_rhs arg =
-          if Datatype_Aux.is_rec_type (dtyp_of arg)
-          then copy_of_dtyp map_tab
-                 mk_take (dtyp_of arg) ` (%# arg)
-          else (%# arg);
-      val lhs = (dc_take dname $ (%%: @{const_name Suc} $ %:"n")) ` (con_app con args);
-      val rhs = con_app2 con one_rhs args;
-      val goal = mk_trp (lhs === rhs);
-      val rules =
-          [ax_abs_iso] @ @{thms take_con_rules}
-          @ take_Suc_thms @ deflation_thms @ deflation_take_thms;
-      val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
-    in pg' thy con_appls goal (K tacs) end;
-  val take_apps = map one_take_app cons;
-  val take_rews = ax_take_0 :: ax_take_strict :: take_apps;
+      val {con_consts, con_betas, ...} = constr_info;
+      val {abs_inverse, ...} = iso_info;
+      fun prove_take_app (con_const : term) (bind, args, mx) =
+        let
+          val Ts = map (fn (_, _, T) => T) args;
+          val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts);
+          val vs = map Free (ns ~~ Ts);
+          val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs));
+          val rhs = list_ccomb (con_const, map2 map_of_arg vs Ts);
+          val goal = mk_trp (mk_eq (lhs, rhs));
+          val rules =
+              [abs_inverse] @ con_betas @ @{thms take_con_rules}
+              @ take_Suc_thms @ deflation_thms @ deflation_take_thms;
+          val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
+        in
+          Goal.prove_global thy [] [] goal (K tac)
+        end;
+      val take_apps = map2 prove_take_app con_consts spec;
+    in
+      yield_singleton Global_Theory.add_thmss
+        ((Binding.qualified true "take_rews" dbind, take_apps),
+        [Simplifier.simp_add]) thy
+    end;
 in
-  take_rews
+  fold_map prove_take_apps
+    (specs ~~ iso_infos ~~ take_consts ~~ constr_infos) thy
 end;
 
 (* ----- general proofs ----------------------------------------------------- *)
 
 val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
 
-fun theorems
-    (eq as ((dname, _), cons) : eq, eqs : eq list)
-    (dbind : binding)
-    (spec : (binding * (bool * binding option * typ) list * mixfix) list)
-    (iso_info : Domain_Take_Proofs.iso_info)
-    (take_info : Domain_Take_Proofs.take_induct_info)
-    (thy : theory) =
-let
-
-val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
-
-(* ----- define constructors ------------------------------------------------ *)
-
-val (result, thy) =
-    Domain_Constructors.add_domain_constructors dbind spec iso_info thy;
-
-val {nchotomy, exhaust, ...} = result;
-val {compacts, con_rews, inverts, injects, dist_les, dist_eqs, ...} = result;
-val {sel_rews, ...} = result;
-val when_rews = #cases result;
-val when_strict = hd when_rews;
-val dis_rews = #dis_rews result;
-val mat_rews = #match_rews result;
-
-(* ----- theorems concerning the isomorphism -------------------------------- *)
-
-val ax_abs_iso = #abs_inverse iso_info;
-val ax_rep_iso = #rep_inverse iso_info;
-
-val retraction_strict = @{thm retraction_strict};
-val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
-val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
-val iso_rews = [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
-
-(* ----- theorems concerning one induction step ----------------------------- *)
-
-val take_rews = take_theorems (eq, eqs) iso_info take_info result thy;
-
-val case_ns =
-    "bottom" :: map (fn (b,_,_) => Binding.name_of b) spec;
-
-fun qualified name = Binding.qualified true name dbind;
-val simp = Simplifier.simp_add;
-
-in
-  thy
-  |> Global_Theory.add_thmss [
-     ((qualified "iso_rews"  , iso_rews    ), [simp]),
-     ((qualified "nchotomy"  , [nchotomy]  ), []),
-     ((qualified "exhaust"   , [exhaust]   ),
-      [Rule_Cases.case_names case_ns, Induct.cases_type dname]),
-     ((qualified "when_rews" , when_rews   ), [simp]),
-     ((qualified "compacts"  , compacts    ), [simp]),
-     ((qualified "con_rews"  , con_rews    ), [simp]),
-     ((qualified "sel_rews"  , sel_rews    ), [simp]),
-     ((qualified "dis_rews"  , dis_rews    ), [simp]),
-     ((qualified "dist_les"  , dist_les    ), [simp]),
-     ((qualified "dist_eqs"  , dist_eqs    ), [simp]),
-     ((qualified "inverts"   , inverts     ), [simp]),
-     ((qualified "injects"   , injects     ), [simp]),
-     ((qualified "take_rews" , take_rews   ), [simp]),
-     ((qualified "match_rews", mat_rews    ), [simp])]
-  |> snd
-  |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
-      dist_les @ dist_eqs)
-end; (* let *)
-
 (******************************************************************************)
 (****************************** induction rules *******************************)
 (******************************************************************************)
@@ -440,6 +370,7 @@
 
 fun prove_coinduction
     (comp_dbind : binding, eqs : eq list)
+    (take_rews : thm list)
     (take_lemmas : thm list)
     (thy : theory) : theory =
 let
@@ -450,9 +381,6 @@
 val x_name = idx_name dnames "x"; 
 val n_eqs = length eqs;
 
-val take_rews =
-    maps (fn dn => Global_Theory.get_thms thy (dn ^ ".take_rews")) dnames;
-
 (* ----- define bisimulation predicate -------------------------------------- *)
 
 local
@@ -581,7 +509,10 @@
 
 fun comp_theorems
     (comp_dbind : binding, eqs : eq list)
+    (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
+    (iso_infos : Domain_Take_Proofs.iso_info list)
     (take_info : Domain_Take_Proofs.take_induct_info)
+    (constr_infos : Domain_Constructors.constr_info list)
     (thy : theory) =
 let
 val map_tab = Domain_Take_Proofs.get_map_tab thy;
@@ -607,10 +538,12 @@
 
 (* theorems about take *)
 
-val take_lemmas = #take_lemma_thms take_info;
+val (take_rewss, thy) =
+    take_theorems specs iso_infos take_info constr_infos thy;
 
-val take_rews =
-    maps (fn dn => Global_Theory.get_thms thy (dn ^ ".take_rews")) dnames;
+val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info;
+
+val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss;
 
 (* prove induction rules, unless definition is indirect recursive *)
 val thy =
@@ -619,7 +552,7 @@
 
 val thy =
     if is_indirect then thy else
-    prove_coinduction (comp_dbind, eqs) take_lemmas thy;
+    prove_coinduction (comp_dbind, eqs) take_rews take_lemma_thms thy;
 
 in
   (take_rews, thy)