move proofs of when_rews intro domain_constructors.ML

--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Sat Feb 27 10:12:47 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Sat Feb 27 14:04:46 2010 -0800
@@ -12,6 +12,7 @@
       -> typ * (binding * (bool * binding option * typ) list * mixfix) list
       -> term * term
       -> thm * thm
+      -> thm
       -> theory
       -> { con_consts : term list,
            con_betas : thm list,
@@ -23,6 +24,7 @@
            injects : thm list,
            dist_les : thm list,
            dist_eqs : thm list,
+           cases : thm list,
            sel_rews : thm list
          } * theory;
 end;
@@ -267,6 +269,12 @@
 
 val simple_ss : simpset = HOL_basic_ss addsimps simp_thms;
 
+val beta_ss =
+  HOL_basic_ss
+    addsimps simp_thms
+    addsimps [@{thm beta_cfun}]
+    addsimprocs [@{simproc cont_proc}];
+
 fun define_consts
     (specs : (binding * term * mixfix) list)
     (thy : theory)
@@ -571,6 +579,76 @@
   end;
 
 (******************************************************************************)
+(**************** definition and theorems for case combinator *****************)
+(******************************************************************************)
+
+fun add_case_combinator
+    (spec : (term * (bool * typ) list) list)
+    (lhsT : typ)
+    (dname : string)
+    (case_def : thm)
+    (con_betas : thm list)
+    (casedist : thm)
+    (iso_locale : thm)
+    (thy : theory) =
+  let
+
+    (* prove rep/abs rules *)
+    val rep_strict = iso_locale RS @{thm iso.rep_strict};
+    val abs_inverse = iso_locale RS @{thm iso.abs_iso};
+
+    (* calculate function arguments of case combinator *)
+    val resultT = TVar (("'a",0), @{sort pcpo});
+    val fTs = map (fn (_, args) => map snd args -->> resultT) spec;
+    val fns = Datatype_Prop.indexify_names (map (K "f") spec);
+    val fs = map Free (fns ~~ fTs);
+    val caseT = fTs -->> (lhsT ->> resultT);
+
+    (* TODO: move definition of case combinator here *)
+    val case_bind = Binding.name (dname ^ "_when");
+    val case_const = Const (Sign.full_name thy case_bind, caseT);
+    val case_app = list_ccomb (case_const, fs);
+
+    (* prove beta reduction rule for case combinator *)
+    val case_beta = beta_of_def thy case_def;
+
+    (* prove strictness of case combinator *)
+    val case_strict =
+      let
+        val defs = [case_beta, mk_meta_eq rep_strict];
+        val lhs = case_app ` mk_bottom lhsT;
+        val goal = mk_trp (mk_eq (lhs, mk_bottom resultT));
+        val tacs = [resolve_tac @{thms sscase1 ssplit1 strictify1} 1];
+      in prove thy defs goal (K tacs) end;
+        
+    (* prove rewrites for case combinator *)
+    local
+      fun one_case (con, args) f =
+        let
+          val Ts = map snd args;
+          val ns = Name.variant_list fns (Datatype_Prop.make_tnames Ts);
+          val vs = map Free (ns ~~ Ts);
+          val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs));
+          val assms = map (mk_trp o mk_defined) nonlazy;
+          val lhs = case_app ` list_ccomb (con, vs);
+          val rhs = list_ccomb (f, vs);
+          val concl = mk_trp (mk_eq (lhs, rhs));
+          val goal = Logic.list_implies (assms, concl);
+          val defs = case_beta :: con_betas;
+          val rules1 = @{thms sscase2 sscase3 ssplit2 fup2 ID1};
+          val rules2 = @{thms con_defined_iff_rules};
+          val rules = abs_inverse :: rules1 @ rules2;
+          val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
+        in prove thy defs goal (K tacs) end;
+    in
+      val case_apps = map2 one_case spec fs;
+    end
+
+  in
+    (case_strict :: case_apps, thy)
+  end
+
+(******************************************************************************)
 (************** definitions and theorems for selector functions ***************)
 (******************************************************************************)
 
@@ -722,6 +800,7 @@
      spec : (binding * (bool * binding option * typ) list * mixfix) list)
     (rep_const : term, abs_const : term)
     (rep_iso_thm : thm, abs_iso_thm : thm)
+    (case_def : thm)
     (thy : theory) =
   let
 
@@ -741,7 +820,18 @@
       in
         add_constructors con_spec abs_const iso_locale thy
       end;
-    val {con_consts, con_betas, ...} = con_result;
+    val {con_consts, con_betas, casedist, ...} = con_result;
+
+    (* define case combinator *)
+    val (cases : thm list, thy) =
+      let
+        fun prep_arg (lazy, sel, T) = (lazy, T);
+        fun prep_con c (b, args, mx) = (c, map prep_arg args);
+        val case_spec = map2 prep_con con_consts spec;
+      in
+        add_case_combinator case_spec lhsT dname
+          case_def con_betas casedist iso_locale thy
+      end;
 
     (* TODO: enable this earlier *)
     val thy = Sign.add_path dname thy;
@@ -762,13 +852,14 @@
       { con_consts = con_consts,
         con_betas = con_betas,
         exhaust = #exhaust con_result,
-        casedist = #casedist con_result,
+        casedist = casedist,
         con_compacts = #con_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,
+        cases = cases,
         sel_rews = sel_thms };
   in
     (result, thy)

--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Feb 27 10:12:47 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Feb 27 14:04:46 2010 -0800
@@ -73,8 +73,6 @@
 val iso_rep_iso     = @{thm iso.rep_iso};
 val iso_abs_strict  = @{thm iso.abs_strict};
 val iso_rep_strict  = @{thm iso.rep_strict};
-val iso_abs_defin'  = @{thm iso.abs_defin'};
-val iso_rep_defin'  = @{thm iso.rep_defin'};
 val iso_abs_defined = @{thm iso.abs_defined};
 val iso_rep_defined = @{thm iso.rep_defined};
 val iso_compact_abs = @{thm iso.compact_abs};
@@ -161,16 +159,6 @@
   val axs_dis_def = map (get_def dis_name) cons;
   val axs_mat_def = map (get_def mat_name) cons;
   val axs_pat_def = map (get_def pat_name) cons;
-(*
-  val axs_sel_def =
-    let
-      fun def_of_sel sel = ga (sel^"_def") dname;
-      fun def_of_arg arg = Option.map def_of_sel (sel_of arg);
-      fun defs_of_con (_, _, args) = map_filter def_of_arg args;
-    in
-      maps defs_of_con cons
-    end;
-*)
   val ax_copy_def = ga "copy_def" dname;
 end; (* local *)
 
@@ -195,13 +183,14 @@
 val (result, thy) =
   Domain_Constructors.add_domain_constructors
     (Long_Name.base_name dname) dom_eqn
-    (rep_const, abs_const) (ax_rep_iso, ax_abs_iso) thy;
+    (rep_const, abs_const) (ax_rep_iso, ax_abs_iso) ax_when_def thy;
 
 val con_appls = #con_betas result;
 val {exhaust, casedist, ...} = result;
 val {con_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;
 
 (* ----- theorems concerning the isomorphism -------------------------------- *)
 
@@ -215,66 +204,8 @@
 val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso];
 val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
 val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
-val abs_defin' = iso_locale RS iso_abs_defin';
-val rep_defin' = iso_locale RS iso_rep_defin';
 val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
 
-(* ----- generating beta reduction rules from definitions-------------------- *)
-
-val _ = trace " Proving beta reduction rules...";
-
-local
-  fun arglist (Const _ $ Abs (s, _, t)) =
-    let
-      val (vars,body) = arglist t;
-    in (s :: vars, body) end
-    | arglist t = ([], t);
-  fun bind_fun vars t = Library.foldr mk_All (vars, t);
-  fun bound_vars 0 = []
-    | bound_vars i = Bound (i-1) :: bound_vars (i - 1);
-in
-  fun appl_of_def def =
-    let
-      val (_ $ con $ lam) = concl_of def;
-      val (vars, rhs) = arglist lam;
-      val lhs = list_ccomb (con, bound_vars (length vars));
-      val appl = bind_fun vars (lhs == rhs);
-      val cs = ContProc.cont_thms lam;
-      val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs;
-    in pg (def::betas) appl (K [rtac reflexive_thm 1]) end;
-end;
-
-val _ = trace "Proving when_appl...";
-val when_appl = appl_of_def ax_when_def;
-
-local 
-  fun bind_fun t = Library.foldr mk_All (when_funs cons, t);
-  fun bound_fun i _ = Bound (length cons - i);
-  val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons);
-in
-  val _ = trace " Proving when_strict...";
-  val when_strict =
-    let
-      val axs = [when_appl, mk_meta_eq rep_strict];
-      val goal = bind_fun (mk_trp (strict when_app));
-      val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1];
-    in pg axs goal (K tacs) end;
-
-  val _ = trace " Proving when_apps...";
-  val when_apps =
-    let
-      fun one_when n (con, _, args) =
-        let
-          val axs = when_appl :: con_appls;
-          val goal = bind_fun (lift_defined %: (nonlazy args, 
-                mk_trp (when_app`(con_app con args) ===
-                       list_ccomb (bound_fun n 0, map %# args))));
-          val tacs = [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1];
-        in pg axs goal (K tacs) end;
-    in mapn one_when 1 cons end;
-end;
-val when_rews = when_strict :: when_apps;
-
 (* ----- theorems concerning the constructors, discriminators and selectors - *)
 
 local