refined and exported record_info;
authorwenzelm
Mon Feb 15 23:58:24 2010 +0100 (2010-02-15)
changeset 35138ad213c602ec1
parent 35137 405bb7e38057
child 35139 e1a226a191b6
child 35150 082fa4bd403d
refined and exported record_info;
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Tools/record.ML	Mon Feb 15 22:40:03 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Mon Feb 15 23:58:24 2010 +0100
     1.3 @@ -9,6 +9,18 @@
     1.4  
     1.5  signature BASIC_RECORD =
     1.6  sig
     1.7 +  type record_info =
     1.8 +   {args: (string * sort) list,
     1.9 +    parent: (typ list * string) option,
    1.10 +    fields: (string * typ) list,
    1.11 +    extension: (string * typ list),
    1.12 +    ext_induct: thm, ext_inject: thm, ext_surjective: thm, ext_split: thm, ext_def: thm,
    1.13 +    select_convs: thm list, update_convs: thm list, select_defs: thm list, update_defs: thm list,
    1.14 +    fold_congs: thm list, unfold_congs: thm list, splits: thm list, defs: thm list,
    1.15 +    surjective: thm, equality: thm, induct_scheme: thm, induct: thm, cases_scheme: thm,
    1.16 +    cases: thm, simps: thm list, iffs: thm list}
    1.17 +  val get_record: theory -> string -> record_info option
    1.18 +  val the_record: theory -> string -> record_info
    1.19    val record_simproc: simproc
    1.20    val record_eq_simproc: simproc
    1.21    val record_upd_simproc: simproc
    1.22 @@ -337,24 +349,55 @@
    1.23    parent: (typ list * string) option,
    1.24    fields: (string * typ) list,
    1.25    extension: (string * typ list),
    1.26 +
    1.27 +  ext_induct: thm,
    1.28 +  ext_inject: thm,
    1.29 +  ext_surjective: thm,
    1.30 +  ext_split: thm,
    1.31 +  ext_def: thm,
    1.32 +
    1.33 +  select_convs: thm list,
    1.34 +  update_convs: thm list,
    1.35 +  select_defs: thm list,
    1.36 +  update_defs: thm list,
    1.37 +  fold_congs: thm list,
    1.38 +  unfold_congs: thm list,
    1.39 +  splits: thm list,
    1.40 +  defs: thm list,
    1.41 +
    1.42 +  surjective: thm,
    1.43 +  equality: thm,
    1.44 +  induct_scheme: thm,
    1.45    induct: thm,
    1.46 -  extdef: thm};
    1.47 -
    1.48 -fun make_record_info args parent fields extension induct extdef =
    1.49 +  cases_scheme: thm,
    1.50 +  cases: thm,
    1.51 +
    1.52 +  simps: thm list,
    1.53 +  iffs: thm list};
    1.54 +
    1.55 +fun make_record_info args parent fields extension
    1.56 +    ext_induct ext_inject ext_surjective ext_split ext_def
    1.57 +    select_convs update_convs select_defs update_defs fold_congs unfold_congs splits defs
    1.58 +    surjective equality induct_scheme induct cases_scheme cases
    1.59 +    simps iffs : record_info =
    1.60   {args = args, parent = parent, fields = fields, extension = extension,
    1.61 -  induct = induct, extdef = extdef}: record_info;
    1.62 -
    1.63 +  ext_induct = ext_induct, ext_inject = ext_inject, ext_surjective = ext_surjective,
    1.64 +  ext_split = ext_split, ext_def = ext_def, select_convs = select_convs,
    1.65 +  update_convs = update_convs, select_defs = select_defs, update_defs = update_defs,
    1.66 +  fold_congs = fold_congs, unfold_congs = unfold_congs, splits = splits, defs = defs,
    1.67 +  surjective = surjective, equality = equality, induct_scheme = induct_scheme,
    1.68 +  induct = induct, cases_scheme = cases_scheme, cases = cases, simps = simps, iffs = iffs};
    1.69  
    1.70  type parent_info =
    1.71   {name: string,
    1.72    fields: (string * typ) list,
    1.73    extension: (string * typ list),
    1.74 -  induct: thm,
    1.75 -  extdef: thm};
    1.76 -
    1.77 -fun make_parent_info name fields extension induct extdef =
    1.78 +  induct_scheme: thm,
    1.79 +  ext_def: thm};
    1.80 +
    1.81 +fun make_parent_info name fields extension ext_def induct_scheme : parent_info =
    1.82   {name = name, fields = fields, extension = extension,
    1.83 -  induct = induct, extdef = extdef}: parent_info;
    1.84 +  ext_def = ext_def, induct_scheme = induct_scheme};
    1.85  
    1.86  
    1.87  (* theory data *)
    1.88 @@ -456,6 +499,11 @@
    1.89  
    1.90  val get_record = Symtab.lookup o #records o Records_Data.get;
    1.91  
    1.92 +fun the_record thy name =
    1.93 +  (case get_record thy name of
    1.94 +    SOME info => info
    1.95 +  | NONE => error ("Unknown record type " ^ quote name));
    1.96 +
    1.97  fun put_record name info thy =
    1.98    let
    1.99      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   1.100 @@ -625,7 +673,7 @@
   1.101        let
   1.102          fun err msg = error (msg ^ " parent record " ^ quote name);
   1.103  
   1.104 -        val {args, parent, fields, extension, induct, extdef} =
   1.105 +        val {args, parent, fields, extension, induct_scheme, ext_def, ...} =
   1.106            (case get_record thy name of SOME info => info | NONE => err "Unknown");
   1.107          val _ = if length types <> length args then err "Bad number of arguments for" else ();
   1.108  
   1.109 @@ -641,7 +689,7 @@
   1.110          val extension' = apsnd (map subst) extension;
   1.111        in
   1.112          add_parents thy parent'
   1.113 -          (make_parent_info name fields' extension' induct extdef :: parents)
   1.114 +          (make_parent_info name fields' extension' ext_def induct_scheme :: parents)
   1.115        end;
   1.116  
   1.117  
   1.118 @@ -1783,16 +1831,16 @@
   1.119        end;
   1.120      val induct = timeit_msg "record extension induct proof:" induct_prf;
   1.121  
   1.122 -    val ([inject', induct', surjective', split_meta'], thm_thy) =
   1.123 +    val ([induct', inject', surjective', split_meta'], thm_thy) =
   1.124        defs_thy
   1.125        |> PureThy.add_thms (map (Thm.no_attributes o apfst Binding.name)
   1.126 -           [("ext_inject", inject),
   1.127 -            ("ext_induct", induct),
   1.128 +           [("ext_induct", induct),
   1.129 +            ("ext_inject", inject),
   1.130              ("ext_surjective", surject),
   1.131              ("ext_split", split_meta)])
   1.132        ||> Code.add_default_eqn ext_def;
   1.133  
   1.134 -  in (thm_thy, extT, induct', inject', split_meta', ext_def) end;
   1.135 +  in ((extT, induct', inject', surjective', split_meta', ext_def), thm_thy) end;
   1.136  
   1.137  fun chunks [] [] = []
   1.138    | chunks [] xs = [xs]
   1.139 @@ -1895,7 +1943,7 @@
   1.140  
   1.141      (* 1st stage: extension_thy *)
   1.142  
   1.143 -    val (extension_thy, extT, ext_induct, ext_inject, ext_split, ext_def) =
   1.144 +    val ((extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), extension_thy) =
   1.145        thy
   1.146        |> Sign.add_path base_name
   1.147        |> extension_definition extN fields alphas_ext zeta moreT more vars;
   1.148 @@ -1979,7 +2027,7 @@
   1.149        [(Binding.suffix_name schemeN b, alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
   1.150          (b, alphas, recT0, Syntax.NoSyn)];
   1.151  
   1.152 -    val ext_defs = ext_def :: map #extdef parents;
   1.153 +    val ext_defs = ext_def :: map #ext_def parents;
   1.154  
   1.155      (*Theorems from the iso_tuple intros.
   1.156        By unfolding ext_defs from r_rec0 we create a tree of constructor
   1.157 @@ -2182,13 +2230,13 @@
   1.158      val (fold_congs, unfold_congs) =
   1.159        timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
   1.160  
   1.161 -    val parent_induct = if null parents then [] else [#induct (hd (rev parents))];
   1.162 +    val parent_induct = Option.map #induct_scheme (try List.last parents);
   1.163  
   1.164      fun induct_scheme_prf () =
   1.165        prove_standard [] induct_scheme_prop
   1.166          (fn _ =>
   1.167            EVERY
   1.168 -           [if null parent_induct then all_tac else try_param_tac rN (hd parent_induct) 1,
   1.169 +           [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
   1.170              try_param_tac rN ext_induct 1,
   1.171              asm_simp_tac HOL_basic_ss 1]);
   1.172      val induct_scheme = timeit_msg "record induct_scheme proof:" induct_scheme_prf;
   1.173 @@ -2311,7 +2359,7 @@
   1.174  
   1.175      val ((([sel_convs', upd_convs', sel_defs', upd_defs',
   1.176              fold_congs', unfold_congs',
   1.177 -          [split_meta', split_object', split_ex'], derived_defs'],
   1.178 +          splits' as [split_meta', split_object', split_ex'], derived_defs'],
   1.179            [surjective', equality']),
   1.180            [induct_scheme', induct', cases_scheme', cases']), thms_thy) =
   1.181        defs_thy
   1.182 @@ -2337,12 +2385,22 @@
   1.183      val sel_upd_defs = sel_defs' @ upd_defs';
   1.184      val iffs = [ext_inject]
   1.185      val depth = parent_len + 1;
   1.186 -    val final_thy =
   1.187 +
   1.188 +    val ([simps', iffs'], thms_thy') =
   1.189        thms_thy
   1.190 -      |> (snd oo PureThy.add_thmss)
   1.191 +      |> PureThy.add_thmss
   1.192            [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
   1.193 -           ((Binding.name "iffs", iffs), [iff_add])]
   1.194 -      |> put_record name (make_record_info args parent fields extension induct_scheme' ext_def)
   1.195 +           ((Binding.name "iffs", iffs), [iff_add])];
   1.196 +
   1.197 +    val info =
   1.198 +      make_record_info args parent fields extension
   1.199 +        ext_induct ext_inject ext_surjective ext_split ext_def
   1.200 +        sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
   1.201 +        surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
   1.202 +
   1.203 +    val final_thy =
   1.204 +      thms_thy'
   1.205 +      |> put_record name info
   1.206        |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')
   1.207        |> add_record_equalities extension_id equality'
   1.208        |> add_extinjects ext_inject