# HG changeset patch # User berghofe # Date 1056914734 -7200 # Node ID 1c22e5499eeba9d8124242d0f59bf206fdd5b5b4 # Parent cddad2aa025b41b21cf1690c2fdd2173d286de72 - 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 diff -r cddad2aa025b -r 1c22e5499eeb src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Sat Jun 28 13:42:56 2003 +0200 +++ b/src/HOL/Tools/record_package.ML Sun Jun 29 21:25:34 2003 +0200 @@ -9,6 +9,7 @@ signature BASIC_RECORD_PACKAGE = sig val record_simproc: simproc + val record_eq_simproc: simproc val record_split_tac: int -> tactic val record_split_name: string val record_split_wrapper: string * wrapper @@ -52,6 +53,7 @@ val product_type_induct = thm "product_type.induct"; val product_type_cases = thm "product_type.cases"; val product_type_split_paired_all = thm "product_type.split_paired_all"; +val product_type_split_paired_All = thm "product_type.split_paired_All"; @@ -163,6 +165,11 @@ | Some c => ((c, T), U)) | dest_fieldT typ = raise TYPE ("dest_fieldT", [typ], []); +fun dest_fieldTs T = + let val ((c, T), U) = dest_fieldT T + in (c, T) :: dest_fieldTs U + end handle TYPE _ => []; + (* morphisms *) @@ -389,10 +396,12 @@ simpset: Simplifier.simpset}, field_splits: {fields: unit Symtab.table, - simpset: Simplifier.simpset}}; + simpset: Simplifier.simpset}, + equalities: thm Symtab.table}; -fun make_record_data records sel_upd field_splits = - {records = records, sel_upd = sel_upd, field_splits = field_splits}: record_data; +fun make_record_data records sel_upd field_splits equalities= + {records = records, sel_upd = sel_upd, field_splits = field_splits, + equalities = equalities}: record_data; structure RecordsArgs = struct @@ -402,24 +411,27 @@ val empty = make_record_data Symtab.empty {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss} - {fields = Symtab.empty, simpset = HOL_basic_ss}; + {fields = Symtab.empty, simpset = HOL_basic_ss} Symtab.empty; val copy = I; val prep_ext = I; fun merge ({records = recs1, sel_upd = {selectors = sels1, updates = upds1, simpset = ss1}, - field_splits = {fields = flds1, simpset = fld_ss1}}, + field_splits = {fields = flds1, simpset = fld_ss1}, + equalities = equalities1}, {records = recs2, sel_upd = {selectors = sels2, updates = upds2, simpset = ss2}, - field_splits = {fields = flds2, simpset = fld_ss2}}) = + field_splits = {fields = flds2, simpset = fld_ss2}, + equalities = equalities2}) = make_record_data (Symtab.merge (K true) (recs1, recs2)) {selectors = Symtab.merge (K true) (sels1, sels2), updates = Symtab.merge (K true) (upds1, upds2), simpset = Simplifier.merge_ss (ss1, ss2)} {fields = Symtab.merge (K true) (flds1, flds2), - simpset = Simplifier.merge_ss (fld_ss1, fld_ss2)}; + simpset = Simplifier.merge_ss (fld_ss1, fld_ss2)} + (Symtab.merge Thm.eq_thm (equalities1, equalities2)); fun print sg ({records = recs, ...}: record_data) = let @@ -450,8 +462,9 @@ fun put_record name info thy = let - val {records, sel_upd, field_splits} = RecordsData.get thy; - val data = make_record_data (Symtab.update ((name, info), records)) sel_upd field_splits; + val {records, sel_upd, field_splits, equalities} = RecordsData.get thy; + val data = make_record_data (Symtab.update ((name, info), records)) + sel_upd field_splits equalities; in RecordsData.put data thy end; @@ -469,27 +482,42 @@ val sels = map (rpair ()) names; val upds = map (suffix updateN) names ~~ names; - val {records, sel_upd = {selectors, updates, simpset}, field_splits} = RecordsData.get thy; + val {records, sel_upd = {selectors, updates, simpset}, field_splits, + equalities} = RecordsData.get thy; val data = make_record_data records {selectors = Symtab.extend (selectors, sels), updates = Symtab.extend (updates, upds), simpset = Simplifier.addsimps (simpset, simps)} - field_splits; + field_splits equalities; in RecordsData.put data thy end; (* access 'field_splits' *) -fun add_record_splits splits thy = +fun add_record_splits names simps thy = let - val {records, sel_upd, field_splits = {fields, simpset}} = RecordsData.get thy; - val flds = map (rpair () o fst) splits; - val simps = map snd splits; + val {records, sel_upd, field_splits = {fields, simpset}, + equalities} = RecordsData.get thy; + val flds = map (rpair ()) names; val data = make_record_data records sel_upd - {fields = Symtab.extend (fields, flds), simpset = Simplifier.addsimps (simpset, simps)}; + {fields = Symtab.extend (fields, flds), + simpset = Simplifier.addsimps (simpset, simps)} equalities; in RecordsData.put data thy end; +(* access 'equalities' *) + +fun add_record_equalities name thm thy = + let + val {records, sel_upd, field_splits, equalities} = RecordsData.get thy; + val data = make_record_data records sel_upd field_splits + (Symtab.update_new ((name, thm), equalities)); + in RecordsData.put data thy end; + +fun get_equalities sg name = + Symtab.lookup (#equalities (RecordsData.get_sg sg), name); + + (* parent records *) fun add_parents thy None parents = parents @@ -542,6 +570,17 @@ | None => None) | _ => None)); +val record_eq_simproc = + Simplifier.simproc (Theory.sign_of HOL.thy) "record_eq_simp" ["r = s"] + (fn sg => fn _ => fn t => + (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ => + (case rev (dest_fieldTs T) of + [] => None + | (name, _) :: _ => (case get_equalities sg name of + None => None + | Some thm => Some (thm RS Eq_TrueI))) + | _ => None)); + (** record field splitting **) @@ -552,11 +591,16 @@ let val {field_splits = {fields, simpset}, ...} = RecordsData.get_sg (Thm.sign_of_thm st); - fun is_fieldT (_, Type (a, [_, _])) = is_some (Symtab.lookup (fields, a)) + fun is_fieldT (Type (a, [_, _])) = is_some (Symtab.lookup (fields, a)) | is_fieldT _ = false; - val params = Logic.strip_params (Library.nth_elem (i - 1, Thm.prems_of st)); + val has_field = exists_Const + (fn (s, Type (_, [Type (_, [T, _]), _])) => + (s = "all" orelse s = "All") andalso is_fieldT T + | _ => false); + + val goal = Library.nth_elem (i - 1, Thm.prems_of st); in - if exists is_fieldT params then Simplifier.full_simp_tac simpset i st + if has_field goal then Simplifier.full_simp_tac simpset i st else Seq.empty end handle Library.LIST _ => Seq.empty; @@ -641,13 +685,16 @@ (* 2nd stage: thms_thy *) - fun make th = map (fn prod_type => Drule.standard (th OF [prod_type])) prod_types; + fun make ren th = map (fn (prod_type, field) => Drule.standard + (Drule.rename_bvars (ren ~~ [base (fst field), moreN] handle LIST _ => []) + (th OF [prod_type]))) (prod_types ~~ fields); - val dest_convs = make product_type_conv1 @ make product_type_conv2; - val field_injects = make product_type_inject; - val field_inducts = make product_type_induct; - val field_cases = make product_type_cases; - val field_splits = make product_type_split_paired_all; + val dest_convs = make [] product_type_conv1 @ make [] product_type_conv2; + val field_injects = make [] product_type_inject; + val field_inducts = make ["x", "y"] product_type_induct; + val field_cases = make ["x", "y"] product_type_cases; + val field_splits = make ["a", "b"] product_type_split_paired_all @ + make ["a", "b"] product_type_split_paired_All; val (thms_thy, [field_defs', dest_defs', dest_convs', field_injects', field_splits', field_inducts', field_cases']) = defs_thy @@ -843,14 +890,12 @@ val all_field_inducts = flat (map #field_inducts parents) @ field_inducts; val all_field_cases = flat (map #field_cases parents) @ field_cases; - val named_splits = map2 (fn (c, th) => (suffix field_typeN c, th)) (names, field_splits); - (* 2nd stage: defs_thy *) val (defs_thy, (((sel_defs, update_defs), derived_defs))) = fields_thy - |> add_record_splits named_splits + |> add_record_splits (map (suffix field_typeN) names) field_splits |> Theory.parent_path |> Theory.add_tyabbrs_i recordT_specs |> Theory.add_path bname @@ -950,7 +995,7 @@ [(("more_induct", more_induct), induct_type_global ""), (("more_cases", more_cases), cases_type_global "")]; - val simps = sel_convs' @ update_convs' @ [equality']; + val simps = sel_convs' @ update_convs'; val iffs = field_injects; val more_thms_thy' = @@ -966,6 +1011,7 @@ |> put_record name (make_record_info args parent fields field_inducts field_cases (field_simps @ simps)) |> put_sel_upd (names @ [full_moreN]) (field_simps @ sel_defs' @ update_defs') + |> add_record_equalities (snd (split_last names)) equality' |> Theory.parent_path; in (final_thy, {simps = simps, iffs = iffs}) end; @@ -1092,7 +1138,8 @@ [RecordsData.init, Theory.add_trfuns ([], parse_translation, [], []), Method.add_methods [record_split_method], - Simplifier.change_simpset_of Simplifier.addsimprocs [record_simproc]]; + Simplifier.change_simpset_of Simplifier.addsimprocs + [record_simproc, record_eq_simproc]]; (* outer syntax *)