src/HOL/record.ML
changeset 4564 dc45cf21dbd2
parent 4459 4066db36616b
child 4574 b922012cc142
     1.1 --- a/src/HOL/record.ML	Mon Jan 12 17:51:32 1998 +0100
     1.2 +++ b/src/HOL/record.ML	Tue Jan 13 10:40:38 1998 +0100
     1.3 @@ -92,6 +92,8 @@
     1.4        and T2 = fastype_of t2
     1.5    in Const ("Pair", [T1, T2] ---> mk_prodT (T1,T2)) $ t1 $ t2  end;
     1.6  
     1.7 +val mk_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
     1.8 +
     1.9  fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2)
    1.10    | dest_prodT T = raise TYPE ("dest_prodT: product type expected", [T], []);
    1.11  
    1.12 @@ -109,11 +111,16 @@
    1.13  val base_free = Free o apfst base;
    1.14  val make_scheme_name = "make_scheme";
    1.15  val make_name = "make";
    1.16 -val update_suffix = "_update";
    1.17 +fun def_suffix s = s ^ "_def";
    1.18 +fun update_suffix s = s ^ "_update";
    1.19  fun make_schemeC full make_schemeT = Const (full make_scheme_name, make_schemeT);
    1.20  fun makeC full makeT = Const (full make_name, makeT);
    1.21 +fun make_args_scheme full make_schemeT base_frees z = 
    1.22 +  list_comb (make_schemeC full make_schemeT, base_frees) $ z;
    1.23 +fun make_args full makeT base_frees = 
    1.24 +  list_comb (makeC full makeT, base_frees); 
    1.25  fun selC s T recT = Const (s, selT T recT);
    1.26 -fun updateC full s T recT = Const (full (base s ^ update_suffix), updateT T recT);
    1.27 +fun updateC s T recT = Const (update_suffix s, updateT T recT);
    1.28  fun frees xs = foldr add_typ_tfree_names (xs, []);
    1.29  
    1.30  
    1.31 @@ -127,7 +134,7 @@
    1.32        val make_decl = (make_name, makeT, NoSyn);
    1.33        val sel_decls = map (fn (c, T) => (c, selT T recT, NoSyn)) current_fields;
    1.34        val update_decls = 
    1.35 -        map (fn (c, T) => (c ^ update_suffix, updateT T recT, NoSyn)) current_fields
    1.36 +        map (fn (c, T) => (update_suffix c, updateT T recT, NoSyn)) current_fields
    1.37    in 
    1.38      make_scheme_decl :: make_decl :: sel_decls @ update_decls
    1.39    end;
    1.40 @@ -140,12 +147,12 @@
    1.41    let
    1.42      val sign = sign_of thy;
    1.43      val full = Sign.full_name sign;
    1.44 -    val make_args_scheme = list_comb (make_schemeC full make_schemeT, base_frees) $ z;
    1.45 -    val make_args = list_comb (makeC full makeT, base_frees); 
    1.46      val make_scheme_def = 
    1.47 -      mk_defpair (make_args_scheme, foldr mk_Pair (base_frees, z));
    1.48 +      mk_defpair (make_args_scheme full make_schemeT base_frees z, 
    1.49 +                  foldr mk_Pair (base_frees, z));
    1.50      val make_def = 
    1.51 -      mk_defpair (make_args, foldr mk_Pair (base_frees, unit))
    1.52 +      mk_defpair (make_args full makeT base_frees, 
    1.53 +                  foldr mk_Pair (base_frees, unit))
    1.54    in
    1.55      make_scheme_def :: [make_def]
    1.56    end;
    1.57 @@ -166,8 +173,6 @@
    1.58  (*update*)
    1.59  fun update_defs recT r all_fields current_fullfields thy = 
    1.60    let
    1.61 -    val sign = sign_of thy;
    1.62 -    val full = Sign.full_name sign;
    1.63      val len_all_fields = length all_fields;
    1.64      fun sel_last r = funpow len_all_fields ap_snd r;
    1.65      fun update_def_s (s, T) = 
    1.66 @@ -175,7 +180,7 @@
    1.67          if s = s' then base_free (s, T) else selC s' T' recT $ r)
    1.68          all_fields
    1.69        in
    1.70 -        mk_defpair (updateC full s T recT $ base_free (s, T) $ r,
    1.71 +        mk_defpair (updateC s T recT $ base_free (s, T) $ r,
    1.72                      foldr mk_Pair (updates, sel_last r)) 
    1.73        end;
    1.74    in 
    1.75 @@ -183,6 +188,66 @@
    1.76    end
    1.77  
    1.78  
    1.79 +(* theorems for make, selectors and update *)
    1.80 + 
    1.81 +(*preparations*)
    1.82 +fun get_all_selector_defs all_fields full thy = 
    1.83 +  map (fn (s, T) => get_axiom thy (def_suffix s)) all_fields; 
    1.84 +fun get_all_update_defs all_fields full thy = 
    1.85 +  map (fn (s, T) => get_axiom thy (def_suffix (update_suffix s))) all_fields;
    1.86 +fun get_make_scheme_def full thy = get_axiom thy (full (def_suffix make_scheme_name));
    1.87 +fun get_make_def full thy = get_axiom thy (full (def_suffix make_name));
    1.88 +fun all_rec_defs all_fields full thy = 
    1.89 +  get_make_scheme_def full thy :: get_make_def full thy :: 
    1.90 +  get_all_selector_defs all_fields full thy @ get_all_update_defs all_fields full thy; 
    1.91 +fun prove_goal_s goal_s all_fields full thy = 
    1.92 +  map (fn (s,T) => 
    1.93 +         (prove_goalw_cterm (all_rec_defs all_fields full thy) 
    1.94 +                            (cterm_of (sign_of thy) (mk_eq (goal_s (s,T))))
    1.95 +                            (K [simp_tac (HOL_basic_ss addsimps [fst_conv,snd_conv]) 1])))
    1.96 +      all_fields;
    1.97 +
    1.98 +(*si (make(_scheme) x1 ... xi ... xn) = xi*)
    1.99 +fun sel_make_scheme_thms recT make_schemeT base_frees z all_fields full thy = 
   1.100 +  let     
   1.101 +    fun sel_make_scheme_s (s, T) = 
   1.102 +        (selC s T recT $ make_args_scheme full make_schemeT base_frees z, base_free(s,T)) 
   1.103 +  in
   1.104 +    prove_goal_s sel_make_scheme_s all_fields full thy
   1.105 +  end;
   1.106 +
   1.107 +fun sel_make_thms recT_unitT makeT base_frees all_fields full thy = 
   1.108 +  let     
   1.109 +    fun sel_make_s (s, T) = 
   1.110 +        (selC s T recT_unitT $ make_args full makeT base_frees, Free(base s,T)) 
   1.111 +  in
   1.112 +    prove_goal_s sel_make_s all_fields full thy
   1.113 +  end;
   1.114 +
   1.115 +(*si_update xia (make(_scheme) x1 ... xi ... xn) = (make x1 ... xia ... xn)*)
   1.116 +fun update_make_scheme_thms recT make_schemeT base_frees z all_fields full thy = 
   1.117 +  let 
   1.118 +    fun update_make_scheme_s (s, T) = 
   1.119 +     (updateC s T recT $ base_free(s ^ "'", T) $ 
   1.120 +        make_args_scheme full make_schemeT base_frees z, 
   1.121 +      make_args_scheme full make_schemeT 
   1.122 +        (map (fn t => if t = base_free(s, T) then base_free(s ^ "'", T) else t) base_frees) z)
   1.123 +  in 
   1.124 +    prove_goal_s update_make_scheme_s all_fields full thy
   1.125 +  end;
   1.126 +
   1.127 +fun update_make_thms recT_unitT makeT base_frees all_fields full thy = 
   1.128 +  let 
   1.129 +    fun update_make_s (s, T) = 
   1.130 +     (updateC s T recT_unitT $ base_free(s ^ "'", T) $ 
   1.131 +        make_args full makeT base_frees, 
   1.132 +      make_args full makeT 
   1.133 +        (map (fn t => if t = base_free(s, T) then base_free(s ^ "'", T) else t) base_frees))
   1.134 +  in 
   1.135 +    prove_goal_s update_make_s all_fields full thy
   1.136 +  end;
   1.137 +
   1.138 +
   1.139  
   1.140  (** errors **)
   1.141  
   1.142 @@ -275,15 +340,29 @@
   1.143    in
   1.144      if not (null errors) 
   1.145        then error (cat_lines errors) else 
   1.146 +      let val thy = 
   1.147          thy |> Theory.add_path ".."
   1.148 -            |> Theory.add_tyabbrs_i [(name, tfrees @ [zeta], recT, NoSyn)]  
   1.149 +            |> Theory.add_tyabbrs_i [(name ^ "_scheme", tfrees @ [zeta], recT, NoSyn)]  
   1.150 +            |> Theory.add_tyabbrs_i [(name, tfrees, recT_unitT, NoSyn)]  
   1.151              |> Theory.add_path name
   1.152              |> Theory.add_consts_i (decls make_schemeT makeT selT updateT recT current_fields)
   1.153              |> Theory.add_defs_i 
   1.154                    ((make_defs make_schemeT makeT base_frees z thy) @ 
   1.155                     (sel_defs recT r all_fields current_fullfields) @
   1.156                     (update_defs recT r all_fields current_fullfields thy))
   1.157 +      in 
   1.158 +        thy |> PureThy.store_thmss 
   1.159 +                 [("record_simps", 
   1.160 +                   sel_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @  
   1.161 +                   sel_make_thms recT_unitT makeT base_frees all_fields full thy @
   1.162 +                   update_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @
   1.163 +                   update_make_thms recT_unitT makeT base_frees all_fields full thy )] 
   1.164              |> Theory.add_path ".." 
   1.165 +      end
   1.166 +
   1.167 +(* @ update_make_thms @ 
   1.168 +                     update_update_thms @ sel_update_thms)]  *)
   1.169 +
   1.170    end;
   1.171  
   1.172  
   1.173 @@ -348,5 +427,4 @@
   1.174  val add_record = add_record_aux read_typ read_parent;
   1.175  val add_record_i = add_record_aux cert_typ (K I);
   1.176  
   1.177 -
   1.178  end;