# HG changeset patch
# User narasche
# Date 884684438 -3600
# Node ID dc45cf21dbd21a26b9e99c0d71f9aa8d66d04073
# Parent  6b9a8e956af9c425686edee384c2c188a8281dd0
Simplification: sel make and update make

diff -r 6b9a8e956af9 -r dc45cf21dbd2 src/HOL/record.ML
--- a/src/HOL/record.ML	Mon Jan 12 17:51:32 1998 +0100
+++ b/src/HOL/record.ML	Tue Jan 13 10:40:38 1998 +0100
@@ -92,6 +92,8 @@
       and T2 = fastype_of t2
   in Const ("Pair", [T1, T2] ---> mk_prodT (T1,T2)) $ t1 $ t2  end;
 
+val mk_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
+
 fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2)
   | dest_prodT T = raise TYPE ("dest_prodT: product type expected", [T], []);
 
@@ -109,11 +111,16 @@
 val base_free = Free o apfst base;
 val make_scheme_name = "make_scheme";
 val make_name = "make";
-val update_suffix = "_update";
+fun def_suffix s = s ^ "_def";
+fun update_suffix s = s ^ "_update";
 fun make_schemeC full make_schemeT = Const (full make_scheme_name, make_schemeT);
 fun makeC full makeT = Const (full make_name, makeT);
+fun make_args_scheme full make_schemeT base_frees z = 
+  list_comb (make_schemeC full make_schemeT, base_frees) $ z;
+fun make_args full makeT base_frees = 
+  list_comb (makeC full makeT, base_frees); 
 fun selC s T recT = Const (s, selT T recT);
-fun updateC full s T recT = Const (full (base s ^ update_suffix), updateT T recT);
+fun updateC s T recT = Const (update_suffix s, updateT T recT);
 fun frees xs = foldr add_typ_tfree_names (xs, []);
 
 
@@ -127,7 +134,7 @@
       val make_decl = (make_name, makeT, NoSyn);
       val sel_decls = map (fn (c, T) => (c, selT T recT, NoSyn)) current_fields;
       val update_decls = 
-        map (fn (c, T) => (c ^ update_suffix, updateT T recT, NoSyn)) current_fields
+        map (fn (c, T) => (update_suffix c, updateT T recT, NoSyn)) current_fields
   in 
     make_scheme_decl :: make_decl :: sel_decls @ update_decls
   end;
@@ -140,12 +147,12 @@
   let
     val sign = sign_of thy;
     val full = Sign.full_name sign;
-    val make_args_scheme = list_comb (make_schemeC full make_schemeT, base_frees) $ z;
-    val make_args = list_comb (makeC full makeT, base_frees); 
     val make_scheme_def = 
-      mk_defpair (make_args_scheme, foldr mk_Pair (base_frees, z));
+      mk_defpair (make_args_scheme full make_schemeT base_frees z, 
+                  foldr mk_Pair (base_frees, z));
     val make_def = 
-      mk_defpair (make_args, foldr mk_Pair (base_frees, unit))
+      mk_defpair (make_args full makeT base_frees, 
+                  foldr mk_Pair (base_frees, unit))
   in
     make_scheme_def :: [make_def]
   end;
@@ -166,8 +173,6 @@
 (*update*)
 fun update_defs recT r all_fields current_fullfields thy = 
   let
-    val sign = sign_of thy;
-    val full = Sign.full_name sign;
     val len_all_fields = length all_fields;
     fun sel_last r = funpow len_all_fields ap_snd r;
     fun update_def_s (s, T) = 
@@ -175,7 +180,7 @@
         if s = s' then base_free (s, T) else selC s' T' recT $ r)
         all_fields
       in
-        mk_defpair (updateC full s T recT $ base_free (s, T) $ r,
+        mk_defpair (updateC s T recT $ base_free (s, T) $ r,
                     foldr mk_Pair (updates, sel_last r)) 
       end;
   in 
@@ -183,6 +188,66 @@
   end
 
 
+(* theorems for make, selectors and update *)
+ 
+(*preparations*)
+fun get_all_selector_defs all_fields full thy = 
+  map (fn (s, T) => get_axiom thy (def_suffix s)) all_fields; 
+fun get_all_update_defs all_fields full thy = 
+  map (fn (s, T) => get_axiom thy (def_suffix (update_suffix s))) all_fields;
+fun get_make_scheme_def full thy = get_axiom thy (full (def_suffix make_scheme_name));
+fun get_make_def full thy = get_axiom thy (full (def_suffix make_name));
+fun all_rec_defs all_fields full thy = 
+  get_make_scheme_def full thy :: get_make_def full thy :: 
+  get_all_selector_defs all_fields full thy @ get_all_update_defs all_fields full thy; 
+fun prove_goal_s goal_s all_fields full thy = 
+  map (fn (s,T) => 
+         (prove_goalw_cterm (all_rec_defs all_fields full thy) 
+                            (cterm_of (sign_of thy) (mk_eq (goal_s (s,T))))
+                            (K [simp_tac (HOL_basic_ss addsimps [fst_conv,snd_conv]) 1])))
+      all_fields;
+
+(*si (make(_scheme) x1 ... xi ... xn) = xi*)
+fun sel_make_scheme_thms recT make_schemeT base_frees z all_fields full thy = 
+  let     
+    fun sel_make_scheme_s (s, T) = 
+        (selC s T recT $ make_args_scheme full make_schemeT base_frees z, base_free(s,T)) 
+  in
+    prove_goal_s sel_make_scheme_s all_fields full thy
+  end;
+
+fun sel_make_thms recT_unitT makeT base_frees all_fields full thy = 
+  let     
+    fun sel_make_s (s, T) = 
+        (selC s T recT_unitT $ make_args full makeT base_frees, Free(base s,T)) 
+  in
+    prove_goal_s sel_make_s all_fields full thy
+  end;
+
+(*si_update xia (make(_scheme) x1 ... xi ... xn) = (make x1 ... xia ... xn)*)
+fun update_make_scheme_thms recT make_schemeT base_frees z all_fields full thy = 
+  let 
+    fun update_make_scheme_s (s, T) = 
+     (updateC s T recT $ base_free(s ^ "'", T) $ 
+        make_args_scheme full make_schemeT base_frees z, 
+      make_args_scheme full make_schemeT 
+        (map (fn t => if t = base_free(s, T) then base_free(s ^ "'", T) else t) base_frees) z)
+  in 
+    prove_goal_s update_make_scheme_s all_fields full thy
+  end;
+
+fun update_make_thms recT_unitT makeT base_frees all_fields full thy = 
+  let 
+    fun update_make_s (s, T) = 
+     (updateC s T recT_unitT $ base_free(s ^ "'", T) $ 
+        make_args full makeT base_frees, 
+      make_args full makeT 
+        (map (fn t => if t = base_free(s, T) then base_free(s ^ "'", T) else t) base_frees))
+  in 
+    prove_goal_s update_make_s all_fields full thy
+  end;
+
+
 
 (** errors **)
 
@@ -275,15 +340,29 @@
   in
     if not (null errors) 
       then error (cat_lines errors) else 
+      let val thy = 
         thy |> Theory.add_path ".."
-            |> Theory.add_tyabbrs_i [(name, tfrees @ [zeta], recT, NoSyn)]  
+            |> Theory.add_tyabbrs_i [(name ^ "_scheme", tfrees @ [zeta], recT, NoSyn)]  
+            |> Theory.add_tyabbrs_i [(name, tfrees, recT_unitT, NoSyn)]  
             |> Theory.add_path name
             |> Theory.add_consts_i (decls make_schemeT makeT selT updateT recT current_fields)
             |> Theory.add_defs_i 
                   ((make_defs make_schemeT makeT base_frees z thy) @ 
                    (sel_defs recT r all_fields current_fullfields) @
                    (update_defs recT r all_fields current_fullfields thy))
+      in 
+        thy |> PureThy.store_thmss 
+                 [("record_simps", 
+                   sel_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @  
+                   sel_make_thms recT_unitT makeT base_frees all_fields full thy @
+                   update_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @
+                   update_make_thms recT_unitT makeT base_frees all_fields full thy )] 
             |> Theory.add_path ".." 
+      end
+
+(* @ update_make_thms @ 
+                     update_update_thms @ sel_update_thms)]  *)
+
   end;
 
 
@@ -348,5 +427,4 @@
 val add_record = add_record_aux read_typ read_parent;
 val add_record_i = add_record_aux cert_typ (K I);
 
-
 end;