Record patch imported and working.
authorThomas Sewell <tsewell@nicta.com.au>
Thu Sep 10 15:18:43 2009 +1000 (2009-09-10)
changeset 3274450406c4951d9
parent 32743 c4e9a48bc50e
child 32745 192d58483fdf
Record patch imported and working.
src/HOL/IsTuple.thy
src/HOL/Record.thy
src/HOL/Tools/istuple_support.ML
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/IsTuple.thy	Thu Aug 27 00:40:53 2009 +1000
     1.2 +++ b/src/HOL/IsTuple.thy	Thu Sep 10 15:18:43 2009 +1000
     1.3 @@ -265,7 +265,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -interpretation tuple_automorphic: isomorphic_tuple [id id Pair]
     1.8 +interpretation tuple_automorphic: isomorphic_tuple "id" "id" "Pair"
     1.9    by (unfold_locales, simp_all add: curry_def)
    1.10  
    1.11  lemma refl_conj_eq:
    1.12 @@ -282,8 +282,6 @@
    1.13  lemma istuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
    1.14    by simp
    1.15  
    1.16 -ML {* val traceref = ref [TrueI]; *}
    1.17 -
    1.18  use "Tools/istuple_support.ML";
    1.19  
    1.20  end
     2.1 --- a/src/HOL/Record.thy	Thu Aug 27 00:40:53 2009 +1000
     2.2 +++ b/src/HOL/Record.thy	Thu Sep 10 15:18:43 2009 +1000
     2.3 @@ -7,7 +7,7 @@
     2.4  
     2.5  theory Record
     2.6  imports Product_Type IsTuple
     2.7 -uses ("Tools/record_package.ML")
     2.8 +uses ("Tools/record.ML")
     2.9  begin
    2.10  
    2.11  lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
    2.12 @@ -65,7 +65,7 @@
    2.13    "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
    2.14    "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
    2.15  
    2.16 -use "Tools/record_package.ML"
    2.17 -setup RecordPackage.setup
    2.18 +use "Tools/record.ML"
    2.19 +setup Record.setup
    2.20  
    2.21  end
     3.1 --- a/src/HOL/Tools/istuple_support.ML	Thu Aug 27 00:40:53 2009 +1000
     3.2 +++ b/src/HOL/Tools/istuple_support.ML	Thu Sep 10 15:18:43 2009 +1000
     3.3 @@ -90,16 +90,23 @@
     3.4      fun get_thms thy name =
     3.5        let
     3.6          val SOME { Rep_inject=rep_inject, Abs_name=absN, abs_type=absT,
     3.7 -          Abs_inverse=abs_inverse, ...} = TypedefPackage.get_info thy name;
     3.8 +          Abs_inverse=abs_inverse, ...} = Typedef.get_info thy name;
     3.9          val rewrite_rule = MetaSimplifier.rewrite_rule [istuple_UNIV_I, istuple_True_simp];
    3.10        in (map rewrite_rule [rep_inject, abs_inverse],
    3.11              Const (absN, repT --> absT)) end;
    3.12    in
    3.13      thy
    3.14 -    |> TypecopyPackage.add_typecopy (name, alphas) repT NONE
    3.15 +    |> Typecopy.typecopy (Binding.name name, alphas) repT NONE
    3.16      |-> (fn (name, _) => `(fn thy => get_thms thy name))
    3.17    end;
    3.18  
    3.19 +(* copied from earlier version of HOLogic *)
    3.20 +fun mk_curry t =
    3.21 +  (case Term.fastype_of t of
    3.22 +    T as (Type ("fun", [Type ("*", [A, B]), C])) =>
    3.23 +      Const ("curry", T --> A --> B --> C) $ t
    3.24 +  | _ => raise TERM ("mk_curry: bad body type", [t]));
    3.25 +
    3.26  fun add_istuple_type (name, alphas) (left, right) thy =
    3.27  let
    3.28    val repT = HOLogic.mk_prodT (left, right);
    3.29 @@ -109,15 +116,16 @@
    3.30      |> do_typedef name repT alphas
    3.31      ||> Sign.add_path name;
    3.32  
    3.33 -  val abs_curry = HOLogic.mk_curry abs;
    3.34 +  val abs_curry = mk_curry abs;
    3.35    val consT     = fastype_of abs_curry;
    3.36 -  val cons      = Const (Sign.full_name typ_thy (name ^ consN), consT);
    3.37 +  val consBind  = Binding.name (name ^ consN);
    3.38 +  val cons      = Const (Sign.full_name typ_thy consBind, consT);
    3.39    val cons_spec = (name ^ consN ^ defN, Logic.mk_equals (cons, abs_curry));
    3.40  
    3.41    val ([cons_def], cdef_thy) =
    3.42      typ_thy
    3.43 -    |> Sign.add_consts_i [Syntax.no_syn (name ^ consN, consT)]
    3.44 -    |> PureThy.add_defs_i false [Thm.no_attributes cons_spec];
    3.45 +    |> Sign.add_consts_i [Syntax.no_syn (consBind, consT)]
    3.46 +    |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name cons_spec)];
    3.47  
    3.48    val istuple = [abs_inverse, cons_def] MRS (rep_inject RS istuple_intro);
    3.49    val intros = [istuple] RL istuple_intros;
    3.50 @@ -133,13 +141,4 @@
    3.51  
    3.52  end;
    3.53  
    3.54 -structure IsTupleIntros2 = TheoryDataFun
    3.55 -(
    3.56 -  type T = IsTupleSupport.tagged_net;
    3.57 -  val empty = IsTupleSupport.build_tagged_net "" [];
    3.58 -  val copy = I;
    3.59 -  val extend = I;
    3.60 -  val merge = K IsTupleSupport.merge_tagged_nets;
    3.61 -);
    3.62  
    3.63 -
     4.1 --- a/src/HOL/Tools/record.ML	Thu Aug 27 00:40:53 2009 +1000
     4.2 +++ b/src/HOL/Tools/record.ML	Thu Sep 10 15:18:43 2009 +1000
     4.3 @@ -286,9 +286,12 @@
     4.4  type record_data =
     4.5   {records: record_info Symtab.table,
     4.6    sel_upd:
     4.7 -   {selectors: unit Symtab.table,
     4.8 +   {selectors: (int * bool) Symtab.table,
     4.9      updates: string Symtab.table,
    4.10 -    simpset: Simplifier.simpset},
    4.11 +    simpset: Simplifier.simpset,
    4.12 +    defset: Simplifier.simpset,
    4.13 +    foldcong: Simplifier.simpset,
    4.14 +    unfoldcong: Simplifier.simpset},
    4.15    equalities: thm Symtab.table,
    4.16    extinjects: thm list,
    4.17    extsplit: thm Symtab.table, (* maps extension name to split rule *)
    4.18 @@ -410,15 +413,25 @@
    4.19        in SOME (s, dep, ismore) end
    4.20    | NONE => NONE end;
    4.21  
    4.22 -fun put_sel_upd names simps = RecordsData.map (fn {records,
    4.23 -  sel_upd = {selectors, updates, simpset},
    4.24 -    equalities, extinjects, extsplit, splits, extfields, fieldext} =>
    4.25 -  make_record_data records
    4.26 -    {selectors = fold (fn name => Symtab.update (name, ())) names selectors,
    4.27 -      updates = fold (fn name => Symtab.update ((suffix updateN) name, name)) names updates,
    4.28 -      simpset = Simplifier.addsimps (simpset, simps)}
    4.29 -      equalities extinjects extsplit splits extfields fieldext);
    4.30 -
    4.31 +fun put_sel_upd names more depth simps defs (folds, unfolds) thy =
    4.32 +  let
    4.33 +    val all  = names @ [more];
    4.34 +    val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
    4.35 +    val upds = map (suffix updateN) all ~~ all;
    4.36 +
    4.37 +    val {records, sel_upd = {selectors, updates, simpset,
    4.38 +                             defset, foldcong, unfoldcong},
    4.39 +      equalities, extinjects, extsplit, splits, extfields,
    4.40 +      fieldext} = RecordsData.get thy;
    4.41 +    val data = make_record_data records
    4.42 +      {selectors = fold Symtab.update_new sels selectors,
    4.43 +        updates = fold Symtab.update_new upds updates,
    4.44 +        simpset = Simplifier.addsimps (simpset, simps),
    4.45 +        defset = Simplifier.addsimps (defset, defs),
    4.46 +        foldcong = foldcong addcongs folds,
    4.47 +        unfoldcong = unfoldcong addcongs unfolds}
    4.48 +       equalities extinjects extsplit splits extfields fieldext;
    4.49 +  in RecordsData.put data thy end;
    4.50  
    4.51  (* access 'equalities' *)
    4.52  
    4.53 @@ -958,7 +971,7 @@
    4.54  fun get_accupd_simps thy term defset intros_tac = let
    4.55      val (acc, [body]) = strip_comb term;
    4.56      val recT          = domain_type (fastype_of acc);
    4.57 -    val updfuns       = sort_distinct Term.fast_term_ord
    4.58 +    val updfuns       = sort_distinct TermOrd.fast_term_ord
    4.59                             (get_updfuns body);
    4.60      fun get_simp upd  = let
    4.61          val T    = domain_type (fastype_of upd);
    4.62 @@ -975,8 +988,8 @@
    4.63        in standard (othm RS dest) end;
    4.64    in map get_simp updfuns end;
    4.65  
    4.66 -structure SymSymTab = TableFun(type key = string * string
    4.67 -                                val ord = prod_ord fast_string_ord fast_string_ord);
    4.68 +structure SymSymTab = Table(type key = string * string
    4.69 +                            val ord = prod_ord fast_string_ord fast_string_ord);
    4.70  
    4.71  fun get_updupd_simp thy defset intros_tac u u' comp = let
    4.72      val f    = Free ("f", domain_type (fastype_of u));
    4.73 @@ -1019,7 +1032,8 @@
    4.74  fun named_cterm_instantiate values thm = let
    4.75      fun match name (Var ((name', _), _)) = name = name'
    4.76        | match name _ = false;
    4.77 -    fun getvar name = case (find_first (match name) (term_vars (prop_of thm)))
    4.78 +    fun getvar name = case (find_first (match name)
    4.79 +                                    (OldTerm.term_vars (prop_of thm)))
    4.80        of SOME var => cterm_of (theory_of_thm thm) var
    4.81         | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm])
    4.82    in
    4.83 @@ -1114,7 +1128,7 @@
    4.84                (case mk_eq_terms (upd$k$r) of
    4.85                   SOME (trm,trm',vars)
    4.86                   => SOME (prove_unfold_defs thy ss domS [] []
    4.87 -                             (list_all(vars,(equals rangeS$(sel$trm)$trm'))))
    4.88 +                             (list_all(vars,(Logic.mk_equals (sel$trm, trm')))))
    4.89                 | NONE => NONE)
    4.90              end
    4.91            | NONE => NONE)
    4.92 @@ -1206,7 +1220,7 @@
    4.93          fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term = let
    4.94              val (lhs, rhs, vars, dups, simp, noops) =
    4.95                    mk_updterm upds (Symtab.update (u, ()) above) term;
    4.96 -            val (fvar, skelf) = K_skeleton (Sign.base_name s) (domain_type T)
    4.97 +            val (fvar, skelf) = K_skeleton (Long_Name.base_name s) (domain_type T)
    4.98                                        (Bound (length vars)) f;
    4.99              val (isnoop, skelf') = is_upd_noop s f term;
   4.100              val funT  = domain_type T;
   4.101 @@ -1240,7 +1254,7 @@
   4.102        in
   4.103          if simp then
   4.104             SOME (prove_unfold_defs thy ss baseT noops' [record_simproc]
   4.105 -                             (list_all(vars,(equals baseT$lhs$rhs))))
   4.106 +                             (list_all(vars,(Logic.mk_equals (lhs, rhs)))))
   4.107          else NONE
   4.108        end)
   4.109  
   4.110 @@ -1559,7 +1573,7 @@
   4.111      fun mk_istuple ((thy, i), (left, rght)) =
   4.112      let
   4.113        val suff = if i = 0 then ext_typeN else inner_typeN ^ (string_of_int i);
   4.114 -      val nm   = suffix suff (Sign.base_name name);
   4.115 +      val nm   = suffix suff (Long_Name.base_name name);
   4.116        val (cons, thy') = IsTupleSupport.add_istuple_type
   4.117                 (nm, alphas_zeta) (fastype_of left, fastype_of rght) thy;
   4.118      in
   4.119 @@ -1586,7 +1600,7 @@
   4.120                               :: group16 (Library.drop (16, xs));
   4.121            val vars' = group16 vars;
   4.122            val ((thy', i'), composites) =
   4.123 -                   foldl_map mk_even_istuple ((thy, i), vars');
   4.124 +                   Library.foldl_map mk_even_istuple ((thy, i), vars');
   4.125          in
   4.126            build_meta_tree_type i' thy' composites more
   4.127          end
   4.128 @@ -1711,14 +1725,13 @@
   4.129                    asm_simp_tac HOL_ss 1]) end;
   4.130      val induct = timeit_msg "record extension induct proof:" induct_prf;
   4.131  
   4.132 -    val (([inject',induct',surjective',split_meta',ext_def'],
   4.133 -          [dest_convs',upd_convs']),
   4.134 +    val ([inject',induct',surjective',split_meta',ext_def'],
   4.135        thm_thy) =
   4.136        defs_thy
   4.137        |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
   4.138             [("ext_inject", inject),
   4.139              ("ext_induct", induct),
   4.140 -            ("ext_surjective", surjective),
   4.141 +            ("ext_surjective", surject),
   4.142              ("ext_split", split_meta),
   4.143              ("ext_def", ext_def)]
   4.144  
   4.145 @@ -2114,7 +2127,7 @@
   4.146      fun get_upd_acc_congs () = let
   4.147          val symdefs  = map symmetric (sel_defs @ upd_defs);
   4.148          val fold_ss  = HOL_basic_ss addsimps symdefs;
   4.149 -        val ua_congs = map (simplify fold_ss) upd_acc_cong_assists;
   4.150 +        val ua_congs = map (standard o simplify fold_ss) upd_acc_cong_assists;
   4.151        in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
   4.152      val (fold_congs, unfold_congs) =
   4.153            timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
   4.154 @@ -2138,12 +2151,6 @@
   4.155        end;
   4.156      val induct = timeit_msg "record induct proof:" induct_prf;
   4.157  
   4.158 -    fun surjective_prf () =
   4.159 -      prove_standard [] surjective_prop (fn prems =>
   4.160 -          (EVERY [try_param_tac rN induct_scheme 1,
   4.161 -                  simp_tac (ss addsimps sel_convs_standard) 1]))
   4.162 -    val surjective = timeit_msg "record surjective proof:" surjective_prf;
   4.163 -
   4.164      fun cases_scheme_prf_opt () =
   4.165        let
   4.166          val (_$(Pvar$_)) = concl_of induct_scheme;
   4.167 @@ -2171,17 +2178,16 @@
   4.168      val cases = timeit_msg "record cases proof:" cases_prf;
   4.169  
   4.170      fun surjective_prf () = let
   4.171 -        val o_ass_thm = symmetric (mk_meta_eq o_assoc);
   4.172 -        val o_reassoc = simplify (HOL_basic_ss addsimps [o_ass_thm]);
   4.173 -        val sel_defs' = map o_reassoc sel_defs;
   4.174 -        val ss        = HOL_basic_ss addsimps (ext_defs @ sel_defs');
   4.175 +        val leaf_ss   = get_sel_upd_defs defs_thy
   4.176 +                                addsimps (sel_defs @ (o_assoc :: id_o_apps));
   4.177 +        val init_ss   = HOL_basic_ss addsimps ext_defs;
   4.178        in
   4.179          prove_standard [] surjective_prop (fn prems =>
   4.180              (EVERY [rtac surject_assist_idE 1,
   4.181 -                    simp_tac ss 1,
   4.182 +                    simp_tac init_ss 1,
   4.183                      REPEAT (intros_tac 1 ORELSE
   4.184                              (rtac surject_assistI 1 THEN
   4.185 -                             simp_tac (HOL_basic_ss addsimps id_o_apps) 1))]))
   4.186 +                             simp_tac leaf_ss 1))]))
   4.187        end;
   4.188      val surjective = timeit_msg "record surjective proof:" surjective_prf;
   4.189  
   4.190 @@ -2230,7 +2236,7 @@
   4.191      fun split_ex_prf () =
   4.192        let
   4.193          val ss   = HOL_basic_ss addsimps [not_ex RS sym, nth simp_thms 1];
   4.194 -        val [Pv] = term_vars (prop_of split_object);
   4.195 +        val [Pv] = OldTerm.term_vars (prop_of split_object);
   4.196          val cPv  = cterm_of defs_thy Pv;
   4.197          val cP   = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
   4.198          val so3  = cterm_instantiate ([(cPv, cP)]) split_object;
   4.199 @@ -2256,16 +2262,18 @@
   4.200       val equality = timeit_msg "record equality proof:" equality_prf;
   4.201  
   4.202      val ((([sel_convs', upd_convs', sel_defs', upd_defs',
   4.203 -            fold_congs', unfold_congs', surjective',
   4.204 +            fold_congs', unfold_congs',
   4.205            [split_meta', split_object', split_ex'], derived_defs'],
   4.206            [surjective', equality']),
   4.207            [induct_scheme', induct', cases_scheme', cases']), thms_thy) =
   4.208        defs_thy
   4.209        |> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
   4.210           [("select_convs", sel_convs_standard),
   4.211 -          ("update_convs", upd_convs),
   4.212 +          ("update_convs", upd_convs_standard),
   4.213            ("select_defs", sel_defs),
   4.214            ("update_defs", upd_defs),
   4.215 +          ("fold_congs", fold_congs),
   4.216 +          ("unfold_congs", unfold_congs),
   4.217            ("splits", [split_meta_standard,split_object,split_ex]),
   4.218            ("defs", derived_defs)]
   4.219        ||>> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
   4.220 @@ -2289,7 +2297,7 @@
   4.221              [Simplifier.simp_add, Nitpick_Const_Simps.add]),
   4.222             ((Binding.name "iffs", iffs), [iff_add])]
   4.223        |> put_record name (make_record_info args parent fields extension induct_scheme' ext_def)
   4.224 -      |> put_sel_upd_names full_moreN depth sel_upd_simps
   4.225 +      |> put_sel_upd names full_moreN depth sel_upd_simps
   4.226                             sel_upd_defs (fold_congs', unfold_congs')
   4.227        |> add_record_equalities extension_id equality'
   4.228        |> add_extinjects ext_inject