src/HOL/Tools/record.ML
changeset 32744 50406c4951d9
parent 32743 c4e9a48bc50e
child 32745 192d58483fdf
     1.1 --- a/src/HOL/Tools/record.ML	Thu Aug 27 00:40:53 2009 +1000
     1.2 +++ b/src/HOL/Tools/record.ML	Thu Sep 10 15:18:43 2009 +1000
     1.3 @@ -286,9 +286,12 @@
     1.4  type record_data =
     1.5   {records: record_info Symtab.table,
     1.6    sel_upd:
     1.7 -   {selectors: unit Symtab.table,
     1.8 +   {selectors: (int * bool) Symtab.table,
     1.9      updates: string Symtab.table,
    1.10 -    simpset: Simplifier.simpset},
    1.11 +    simpset: Simplifier.simpset,
    1.12 +    defset: Simplifier.simpset,
    1.13 +    foldcong: Simplifier.simpset,
    1.14 +    unfoldcong: Simplifier.simpset},
    1.15    equalities: thm Symtab.table,
    1.16    extinjects: thm list,
    1.17    extsplit: thm Symtab.table, (* maps extension name to split rule *)
    1.18 @@ -410,15 +413,25 @@
    1.19        in SOME (s, dep, ismore) end
    1.20    | NONE => NONE end;
    1.21  
    1.22 -fun put_sel_upd names simps = RecordsData.map (fn {records,
    1.23 -  sel_upd = {selectors, updates, simpset},
    1.24 -    equalities, extinjects, extsplit, splits, extfields, fieldext} =>
    1.25 -  make_record_data records
    1.26 -    {selectors = fold (fn name => Symtab.update (name, ())) names selectors,
    1.27 -      updates = fold (fn name => Symtab.update ((suffix updateN) name, name)) names updates,
    1.28 -      simpset = Simplifier.addsimps (simpset, simps)}
    1.29 -      equalities extinjects extsplit splits extfields fieldext);
    1.30 -
    1.31 +fun put_sel_upd names more depth simps defs (folds, unfolds) thy =
    1.32 +  let
    1.33 +    val all  = names @ [more];
    1.34 +    val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
    1.35 +    val upds = map (suffix updateN) all ~~ all;
    1.36 +
    1.37 +    val {records, sel_upd = {selectors, updates, simpset,
    1.38 +                             defset, foldcong, unfoldcong},
    1.39 +      equalities, extinjects, extsplit, splits, extfields,
    1.40 +      fieldext} = RecordsData.get thy;
    1.41 +    val data = make_record_data records
    1.42 +      {selectors = fold Symtab.update_new sels selectors,
    1.43 +        updates = fold Symtab.update_new upds updates,
    1.44 +        simpset = Simplifier.addsimps (simpset, simps),
    1.45 +        defset = Simplifier.addsimps (defset, defs),
    1.46 +        foldcong = foldcong addcongs folds,
    1.47 +        unfoldcong = unfoldcong addcongs unfolds}
    1.48 +       equalities extinjects extsplit splits extfields fieldext;
    1.49 +  in RecordsData.put data thy end;
    1.50  
    1.51  (* access 'equalities' *)
    1.52  
    1.53 @@ -958,7 +971,7 @@
    1.54  fun get_accupd_simps thy term defset intros_tac = let
    1.55      val (acc, [body]) = strip_comb term;
    1.56      val recT          = domain_type (fastype_of acc);
    1.57 -    val updfuns       = sort_distinct Term.fast_term_ord
    1.58 +    val updfuns       = sort_distinct TermOrd.fast_term_ord
    1.59                             (get_updfuns body);
    1.60      fun get_simp upd  = let
    1.61          val T    = domain_type (fastype_of upd);
    1.62 @@ -975,8 +988,8 @@
    1.63        in standard (othm RS dest) end;
    1.64    in map get_simp updfuns end;
    1.65  
    1.66 -structure SymSymTab = TableFun(type key = string * string
    1.67 -                                val ord = prod_ord fast_string_ord fast_string_ord);
    1.68 +structure SymSymTab = Table(type key = string * string
    1.69 +                            val ord = prod_ord fast_string_ord fast_string_ord);
    1.70  
    1.71  fun get_updupd_simp thy defset intros_tac u u' comp = let
    1.72      val f    = Free ("f", domain_type (fastype_of u));
    1.73 @@ -1019,7 +1032,8 @@
    1.74  fun named_cterm_instantiate values thm = let
    1.75      fun match name (Var ((name', _), _)) = name = name'
    1.76        | match name _ = false;
    1.77 -    fun getvar name = case (find_first (match name) (term_vars (prop_of thm)))
    1.78 +    fun getvar name = case (find_first (match name)
    1.79 +                                    (OldTerm.term_vars (prop_of thm)))
    1.80        of SOME var => cterm_of (theory_of_thm thm) var
    1.81         | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])
    1.82    in
    1.83 @@ -1114,7 +1128,7 @@
    1.84                (case mk_eq_terms (upd$k$r) of
    1.85                   SOME (trm,trm',vars)
    1.86                   => SOME (prove_unfold_defs thy ss domS [] []
    1.87 -                             (list_all(vars,(equals rangeS$(sel$trm)$trm'))))
    1.88 +                             (list_all(vars,(Logic.mk_equals (sel$trm, trm')))))
    1.89                 | NONE => NONE)
    1.90              end
    1.91            | NONE => NONE)
    1.92 @@ -1206,7 +1220,7 @@
    1.93          fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term = let
    1.94              val (lhs, rhs, vars, dups, simp, noops) =
    1.95                    mk_updterm upds (Symtab.update (u, ()) above) term;
    1.96 -            val (fvar, skelf) = K_skeleton (Sign.base_name s) (domain_type T)
    1.97 +            val (fvar, skelf) = K_skeleton (Long_Name.base_name s) (domain_type T)
    1.98                                        (Bound (length vars)) f;
    1.99              val (isnoop, skelf') = is_upd_noop s f term;
   1.100              val funT  = domain_type T;
   1.101 @@ -1240,7 +1254,7 @@
   1.102        in
   1.103          if simp then
   1.104             SOME (prove_unfold_defs thy ss baseT noops' [record_simproc]
   1.105 -                             (list_all(vars,(equals baseT$lhs$rhs))))
   1.106 +                             (list_all(vars,(Logic.mk_equals (lhs, rhs)))))
   1.107          else NONE
   1.108        end)
   1.109  
   1.110 @@ -1559,7 +1573,7 @@
   1.111      fun mk_istuple ((thy, i), (left, rght)) =
   1.112      let
   1.113        val suff = if i = 0 then ext_typeN else inner_typeN ^ (string_of_int i);
   1.114 -      val nm   = suffix suff (Sign.base_name name);
   1.115 +      val nm   = suffix suff (Long_Name.base_name name);
   1.116        val (cons, thy') = IsTupleSupport.add_istuple_type
   1.117                 (nm, alphas_zeta) (fastype_of left, fastype_of rght) thy;
   1.118      in
   1.119 @@ -1586,7 +1600,7 @@
   1.120                               :: group16 (Library.drop (16, xs));
   1.121            val vars' = group16 vars;
   1.122            val ((thy', i'), composites) =
   1.123 -                   foldl_map mk_even_istuple ((thy, i), vars');
   1.124 +                   Library.foldl_map mk_even_istuple ((thy, i), vars');
   1.125          in
   1.126            build_meta_tree_type i' thy' composites more
   1.127          end
   1.128 @@ -1711,14 +1725,13 @@
   1.129                    asm_simp_tac HOL_ss 1]) end;
   1.130      val induct = timeit_msg "record extension induct proof:" induct_prf;
   1.131  
   1.132 -    val (([inject',induct',surjective',split_meta',ext_def'],
   1.133 -          [dest_convs',upd_convs']),
   1.134 +    val ([inject',induct',surjective',split_meta',ext_def'],
   1.135        thm_thy) =
   1.136        defs_thy
   1.137        |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
   1.138             [("ext_inject", inject),
   1.139              ("ext_induct", induct),
   1.140 -            ("ext_surjective", surjective),
   1.141 +            ("ext_surjective", surject),
   1.142              ("ext_split", split_meta),
   1.143              ("ext_def", ext_def)]
   1.144  
   1.145 @@ -2114,7 +2127,7 @@
   1.146      fun get_upd_acc_congs () = let
   1.147          val symdefs  = map symmetric (sel_defs @ upd_defs);
   1.148          val fold_ss  = HOL_basic_ss addsimps symdefs;
   1.149 -        val ua_congs = map (simplify fold_ss) upd_acc_cong_assists;
   1.150 +        val ua_congs = map (standard o simplify fold_ss) upd_acc_cong_assists;
   1.151        in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
   1.152      val (fold_congs, unfold_congs) =
   1.153            timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
   1.154 @@ -2138,12 +2151,6 @@
   1.155        end;
   1.156      val induct = timeit_msg "record induct proof:" induct_prf;
   1.157  
   1.158 -    fun surjective_prf () =
   1.159 -      prove_standard [] surjective_prop (fn prems =>
   1.160 -          (EVERY [try_param_tac rN induct_scheme 1,
   1.161 -                  simp_tac (ss addsimps sel_convs_standard) 1]))
   1.162 -    val surjective = timeit_msg "record surjective proof:" surjective_prf;
   1.163 -
   1.164      fun cases_scheme_prf_opt () =
   1.165        let
   1.166          val (_$(Pvar$_)) = concl_of induct_scheme;
   1.167 @@ -2171,17 +2178,16 @@
   1.168      val cases = timeit_msg "record cases proof:" cases_prf;
   1.169  
   1.170      fun surjective_prf () = let
   1.171 -        val o_ass_thm = symmetric (mk_meta_eq o_assoc);
   1.172 -        val o_reassoc = simplify (HOL_basic_ss addsimps [o_ass_thm]);
   1.173 -        val sel_defs' = map o_reassoc sel_defs;
   1.174 -        val ss        = HOL_basic_ss addsimps (ext_defs @ sel_defs');
   1.175 +        val leaf_ss   = get_sel_upd_defs defs_thy
   1.176 +                                addsimps (sel_defs @ (o_assoc :: id_o_apps));
   1.177 +        val init_ss   = HOL_basic_ss addsimps ext_defs;
   1.178        in
   1.179          prove_standard [] surjective_prop (fn prems =>
   1.180              (EVERY [rtac surject_assist_idE 1,
   1.181 -                    simp_tac ss 1,
   1.182 +                    simp_tac init_ss 1,
   1.183                      REPEAT (intros_tac 1 ORELSE
   1.184                              (rtac surject_assistI 1 THEN
   1.185 -                             simp_tac (HOL_basic_ss addsimps id_o_apps) 1))]))
   1.186 +                             simp_tac leaf_ss 1))]))
   1.187        end;
   1.188      val surjective = timeit_msg "record surjective proof:" surjective_prf;
   1.189  
   1.190 @@ -2230,7 +2236,7 @@
   1.191      fun split_ex_prf () =
   1.192        let
   1.193          val ss   = HOL_basic_ss addsimps [not_ex RS sym, nth simp_thms 1];
   1.194 -        val [Pv] = term_vars (prop_of split_object);
   1.195 +        val [Pv] = OldTerm.term_vars (prop_of split_object);
   1.196          val cPv  = cterm_of defs_thy Pv;
   1.197          val cP   = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
   1.198          val so3  = cterm_instantiate ([(cPv, cP)]) split_object;
   1.199 @@ -2256,16 +2262,18 @@
   1.200       val equality = timeit_msg "record equality proof:" equality_prf;
   1.201  
   1.202      val ((([sel_convs', upd_convs', sel_defs', upd_defs',
   1.203 -            fold_congs', unfold_congs', surjective',
   1.204 +            fold_congs', unfold_congs',
   1.205            [split_meta', split_object', split_ex'], derived_defs'],
   1.206            [surjective', equality']),
   1.207            [induct_scheme', induct', cases_scheme', cases']), thms_thy) =
   1.208        defs_thy
   1.209        |> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
   1.210           [("select_convs", sel_convs_standard),
   1.211 -          ("update_convs", upd_convs),
   1.212 +          ("update_convs", upd_convs_standard),
   1.213            ("select_defs", sel_defs),
   1.214            ("update_defs", upd_defs),
   1.215 +          ("fold_congs", fold_congs),
   1.216 +          ("unfold_congs", unfold_congs),
   1.217            ("splits", [split_meta_standard,split_object,split_ex]),
   1.218            ("defs", derived_defs)]
   1.219        ||>> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
   1.220 @@ -2289,7 +2297,7 @@
   1.221              [Simplifier.simp_add, Nitpick_Const_Simps.add]),
   1.222             ((Binding.name "iffs", iffs), [iff_add])]
   1.223        |> put_record name (make_record_info args parent fields extension induct_scheme' ext_def)
   1.224 -      |> put_sel_upd_names full_moreN depth sel_upd_simps
   1.225 +      |> put_sel_upd names full_moreN depth sel_upd_simps
   1.226                             sel_upd_defs (fold_congs', unfold_congs')
   1.227        |> add_record_equalities extension_id equality'
   1.228        |> add_extinjects ext_inject