- record_split_tac now also works for object-level universal quantifier
authorberghofe
Sun Jun 29 21:25:34 2003 +0200 (2003-06-29)
changeset 140791c22e5499eeb
parent 14078 cddad2aa025b
child 14080 9a50427d7165
- record_split_tac now also works for object-level universal quantifier
- bound variables in split rule now have nicer names
- added new simproc record_eq_simproc which prevents simplifier
from choosing the "wrong" equality rule
src/HOL/Tools/record_package.ML
     1.1 --- a/src/HOL/Tools/record_package.ML	Sat Jun 28 13:42:56 2003 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Sun Jun 29 21:25:34 2003 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  signature BASIC_RECORD_PACKAGE =
     1.5  sig
     1.6    val record_simproc: simproc
     1.7 +  val record_eq_simproc: simproc
     1.8    val record_split_tac: int -> tactic
     1.9    val record_split_name: string
    1.10    val record_split_wrapper: string * wrapper
    1.11 @@ -52,6 +53,7 @@
    1.12  val product_type_induct = thm "product_type.induct";
    1.13  val product_type_cases = thm "product_type.cases";
    1.14  val product_type_split_paired_all = thm "product_type.split_paired_all";
    1.15 +val product_type_split_paired_All = thm "product_type.split_paired_All";
    1.16  
    1.17  
    1.18  
    1.19 @@ -163,6 +165,11 @@
    1.20        | Some c => ((c, T), U))
    1.21    | dest_fieldT typ = raise TYPE ("dest_fieldT", [typ], []);
    1.22  
    1.23 +fun dest_fieldTs T =
    1.24 +  let val ((c, T), U) = dest_fieldT T
    1.25 +  in (c, T) :: dest_fieldTs U
    1.26 +  end handle TYPE _ => [];
    1.27 +
    1.28  
    1.29  (* morphisms *)
    1.30  
    1.31 @@ -389,10 +396,12 @@
    1.32      simpset: Simplifier.simpset},
    1.33    field_splits:
    1.34     {fields: unit Symtab.table,
    1.35 -    simpset: Simplifier.simpset}};
    1.36 +    simpset: Simplifier.simpset},
    1.37 +  equalities: thm Symtab.table};
    1.38  
    1.39 -fun make_record_data records sel_upd field_splits =
    1.40 - {records = records, sel_upd = sel_upd, field_splits = field_splits}: record_data;
    1.41 +fun make_record_data records sel_upd field_splits equalities=
    1.42 + {records = records, sel_upd = sel_upd, field_splits = field_splits,
    1.43 +  equalities = equalities}: record_data;
    1.44  
    1.45  structure RecordsArgs =
    1.46  struct
    1.47 @@ -402,24 +411,27 @@
    1.48    val empty =
    1.49      make_record_data Symtab.empty
    1.50        {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss}
    1.51 -      {fields = Symtab.empty, simpset = HOL_basic_ss};
    1.52 +      {fields = Symtab.empty, simpset = HOL_basic_ss} Symtab.empty;
    1.53  
    1.54    val copy = I;
    1.55    val prep_ext = I;
    1.56    fun merge
    1.57     ({records = recs1,
    1.58       sel_upd = {selectors = sels1, updates = upds1, simpset = ss1},
    1.59 -     field_splits = {fields = flds1, simpset = fld_ss1}},
    1.60 +     field_splits = {fields = flds1, simpset = fld_ss1},
    1.61 +     equalities = equalities1},
    1.62      {records = recs2,
    1.63       sel_upd = {selectors = sels2, updates = upds2, simpset = ss2},
    1.64 -     field_splits = {fields = flds2, simpset = fld_ss2}}) =
    1.65 +     field_splits = {fields = flds2, simpset = fld_ss2},
    1.66 +     equalities = equalities2}) =
    1.67      make_record_data
    1.68        (Symtab.merge (K true) (recs1, recs2))
    1.69        {selectors = Symtab.merge (K true) (sels1, sels2),
    1.70          updates = Symtab.merge (K true) (upds1, upds2),
    1.71          simpset = Simplifier.merge_ss (ss1, ss2)}
    1.72        {fields = Symtab.merge (K true) (flds1, flds2),
    1.73 -        simpset = Simplifier.merge_ss (fld_ss1, fld_ss2)};
    1.74 +        simpset = Simplifier.merge_ss (fld_ss1, fld_ss2)}
    1.75 +      (Symtab.merge Thm.eq_thm (equalities1, equalities2));
    1.76  
    1.77    fun print sg ({records = recs, ...}: record_data) =
    1.78      let
    1.79 @@ -450,8 +462,9 @@
    1.80  
    1.81  fun put_record name info thy =
    1.82    let
    1.83 -    val {records, sel_upd, field_splits} = RecordsData.get thy;
    1.84 -    val data = make_record_data (Symtab.update ((name, info), records)) sel_upd field_splits;
    1.85 +    val {records, sel_upd, field_splits, equalities} = RecordsData.get thy;
    1.86 +    val data = make_record_data (Symtab.update ((name, info), records))
    1.87 +      sel_upd field_splits equalities;
    1.88    in RecordsData.put data thy end;
    1.89  
    1.90  
    1.91 @@ -469,27 +482,42 @@
    1.92      val sels = map (rpair ()) names;
    1.93      val upds = map (suffix updateN) names ~~ names;
    1.94  
    1.95 -    val {records, sel_upd = {selectors, updates, simpset}, field_splits} = RecordsData.get thy;
    1.96 +    val {records, sel_upd = {selectors, updates, simpset}, field_splits,
    1.97 +      equalities} = RecordsData.get thy;
    1.98      val data = make_record_data records
    1.99        {selectors = Symtab.extend (selectors, sels),
   1.100          updates = Symtab.extend (updates, upds),
   1.101          simpset = Simplifier.addsimps (simpset, simps)}
   1.102 -      field_splits;
   1.103 +      field_splits equalities;
   1.104    in RecordsData.put data thy end;
   1.105  
   1.106  
   1.107  (* access 'field_splits' *)
   1.108  
   1.109 -fun add_record_splits splits thy =
   1.110 +fun add_record_splits names simps thy =
   1.111    let
   1.112 -    val {records, sel_upd, field_splits = {fields, simpset}} = RecordsData.get thy;
   1.113 -    val flds = map (rpair () o fst) splits;
   1.114 -    val simps = map snd splits;
   1.115 +    val {records, sel_upd, field_splits = {fields, simpset},
   1.116 +      equalities} = RecordsData.get thy;
   1.117 +    val flds = map (rpair ()) names;
   1.118      val data = make_record_data records sel_upd
   1.119 -      {fields = Symtab.extend (fields, flds), simpset = Simplifier.addsimps (simpset, simps)};
   1.120 +      {fields = Symtab.extend (fields, flds),
   1.121 +       simpset = Simplifier.addsimps (simpset, simps)} equalities;
   1.122    in RecordsData.put data thy end;
   1.123  
   1.124  
   1.125 +(* access 'equalities' *)
   1.126 +
   1.127 +fun add_record_equalities name thm thy =
   1.128 +  let
   1.129 +    val {records, sel_upd, field_splits, equalities} = RecordsData.get thy;
   1.130 +    val data = make_record_data records sel_upd field_splits
   1.131 +      (Symtab.update_new ((name, thm), equalities));
   1.132 +  in RecordsData.put data thy end;
   1.133 +
   1.134 +fun get_equalities sg name =
   1.135 +  Symtab.lookup (#equalities (RecordsData.get_sg sg), name);
   1.136 +
   1.137 +
   1.138  (* parent records *)
   1.139  
   1.140  fun add_parents thy None parents = parents
   1.141 @@ -542,6 +570,17 @@
   1.142          | None => None)
   1.143        | _ => None));
   1.144  
   1.145 +val record_eq_simproc =
   1.146 +  Simplifier.simproc (Theory.sign_of HOL.thy) "record_eq_simp" ["r = s"]
   1.147 +    (fn sg => fn _ => fn t =>
   1.148 +      (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ =>
   1.149 +        (case rev (dest_fieldTs T) of
   1.150 +           [] => None
   1.151 +         | (name, _) :: _ => (case get_equalities sg name of
   1.152 +             None => None
   1.153 +           | Some thm => Some (thm RS Eq_TrueI)))
   1.154 +       | _ => None));
   1.155 +
   1.156  
   1.157  
   1.158  (** record field splitting **)
   1.159 @@ -552,11 +591,16 @@
   1.160    let
   1.161      val {field_splits = {fields, simpset}, ...} = RecordsData.get_sg (Thm.sign_of_thm st);
   1.162  
   1.163 -    fun is_fieldT (_, Type (a, [_, _])) = is_some (Symtab.lookup (fields, a))
   1.164 +    fun is_fieldT (Type (a, [_, _])) = is_some (Symtab.lookup (fields, a))
   1.165        | is_fieldT _ = false;
   1.166 -    val params = Logic.strip_params (Library.nth_elem (i - 1, Thm.prems_of st));
   1.167 +    val has_field = exists_Const
   1.168 +      (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   1.169 +          (s = "all" orelse s = "All") andalso is_fieldT T
   1.170 +        | _ => false);
   1.171 +
   1.172 +    val goal = Library.nth_elem (i - 1, Thm.prems_of st);
   1.173    in
   1.174 -    if exists is_fieldT params then Simplifier.full_simp_tac simpset i st
   1.175 +    if has_field goal then Simplifier.full_simp_tac simpset i st
   1.176      else Seq.empty
   1.177    end handle Library.LIST _ => Seq.empty;
   1.178  
   1.179 @@ -641,13 +685,16 @@
   1.180  
   1.181      (* 2nd stage: thms_thy *)
   1.182  
   1.183 -    fun make th = map (fn prod_type => Drule.standard (th OF [prod_type])) prod_types;
   1.184 +    fun make ren th = map (fn (prod_type, field) => Drule.standard
   1.185 +      (Drule.rename_bvars (ren ~~ [base (fst field), moreN] handle LIST _ => [])
   1.186 +        (th OF [prod_type]))) (prod_types ~~ fields);
   1.187  
   1.188 -    val dest_convs = make product_type_conv1 @ make product_type_conv2;
   1.189 -    val field_injects = make product_type_inject;
   1.190 -    val field_inducts = make product_type_induct;
   1.191 -    val field_cases = make product_type_cases;
   1.192 -    val field_splits = make product_type_split_paired_all;
   1.193 +    val dest_convs = make [] product_type_conv1 @ make [] product_type_conv2;
   1.194 +    val field_injects = make [] product_type_inject;
   1.195 +    val field_inducts = make ["x", "y"] product_type_induct;
   1.196 +    val field_cases = make ["x", "y"] product_type_cases;
   1.197 +    val field_splits = make ["a", "b"] product_type_split_paired_all @
   1.198 +      make ["a", "b"] product_type_split_paired_All;
   1.199  
   1.200      val (thms_thy, [field_defs', dest_defs', dest_convs', field_injects',
   1.201          field_splits', field_inducts', field_cases']) = defs_thy
   1.202 @@ -843,14 +890,12 @@
   1.203      val all_field_inducts = flat (map #field_inducts parents) @ field_inducts;
   1.204      val all_field_cases = flat (map #field_cases parents) @ field_cases;
   1.205  
   1.206 -    val named_splits = map2 (fn (c, th) => (suffix field_typeN c, th)) (names, field_splits);
   1.207 -
   1.208  
   1.209      (* 2nd stage: defs_thy *)
   1.210  
   1.211      val (defs_thy, (((sel_defs, update_defs), derived_defs))) =
   1.212        fields_thy
   1.213 -      |> add_record_splits named_splits
   1.214 +      |> add_record_splits (map (suffix field_typeN) names) field_splits
   1.215        |> Theory.parent_path
   1.216        |> Theory.add_tyabbrs_i recordT_specs
   1.217        |> Theory.add_path bname
   1.218 @@ -950,7 +995,7 @@
   1.219          [(("more_induct", more_induct), induct_type_global ""),
   1.220           (("more_cases", more_cases), cases_type_global "")];
   1.221  
   1.222 -    val simps = sel_convs' @ update_convs' @ [equality'];
   1.223 +    val simps = sel_convs' @ update_convs';
   1.224      val iffs = field_injects;
   1.225  
   1.226      val more_thms_thy' =
   1.227 @@ -966,6 +1011,7 @@
   1.228        |> put_record name (make_record_info args parent fields field_inducts field_cases
   1.229          (field_simps @ simps))
   1.230        |> put_sel_upd (names @ [full_moreN]) (field_simps @ sel_defs' @ update_defs')
   1.231 +      |> add_record_equalities (snd (split_last names)) equality'
   1.232        |> Theory.parent_path;
   1.233  
   1.234    in (final_thy, {simps = simps, iffs = iffs}) end;
   1.235 @@ -1092,7 +1138,8 @@
   1.236   [RecordsData.init,
   1.237    Theory.add_trfuns ([], parse_translation, [], []),
   1.238    Method.add_methods [record_split_method],
   1.239 -  Simplifier.change_simpset_of Simplifier.addsimprocs [record_simproc]];
   1.240 +  Simplifier.change_simpset_of Simplifier.addsimprocs
   1.241 +    [record_simproc, record_eq_simproc]];
   1.242  
   1.243  
   1.244  (* outer syntax *)