# HG changeset patch # User Thomas Sewell # Date 1252559923 -36000 # Node ID 50406c4951d9e3b747f1981a58518ab0e9f2c1b7 # Parent c4e9a48bc50e4ff53e51d9f7c0632b102c56fa2f Record patch imported and working. diff -r c4e9a48bc50e -r 50406c4951d9 src/HOL/IsTuple.thy --- a/src/HOL/IsTuple.thy Thu Aug 27 00:40:53 2009 +1000 +++ b/src/HOL/IsTuple.thy Thu Sep 10 15:18:43 2009 +1000 @@ -265,7 +265,7 @@ end -interpretation tuple_automorphic: isomorphic_tuple [id id Pair] +interpretation tuple_automorphic: isomorphic_tuple "id" "id" "Pair" by (unfold_locales, simp_all add: curry_def) lemma refl_conj_eq: @@ -282,8 +282,6 @@ lemma istuple_True_simp: "(True \ PROP P) \ PROP P" by simp -ML {* val traceref = ref [TrueI]; *} - use "Tools/istuple_support.ML"; end diff -r c4e9a48bc50e -r 50406c4951d9 src/HOL/Record.thy --- a/src/HOL/Record.thy Thu Aug 27 00:40:53 2009 +1000 +++ b/src/HOL/Record.thy Thu Sep 10 15:18:43 2009 +1000 @@ -7,7 +7,7 @@ theory Record imports Product_Type IsTuple -uses ("Tools/record_package.ML") +uses ("Tools/record.ML") begin lemma prop_subst: "s = t \ PROP P t \ PROP P s" @@ -65,7 +65,7 @@ "_record_scheme" :: "[fields, 'a] => 'a" ("(3\_,/ (2\ =/ _)\)") "_record_update" :: "['a, updates] => 'b" ("_/(3\_\)" [900,0] 900) -use "Tools/record_package.ML" -setup RecordPackage.setup +use "Tools/record.ML" +setup Record.setup end diff -r c4e9a48bc50e -r 50406c4951d9 src/HOL/Tools/istuple_support.ML --- a/src/HOL/Tools/istuple_support.ML Thu Aug 27 00:40:53 2009 +1000 +++ b/src/HOL/Tools/istuple_support.ML Thu Sep 10 15:18:43 2009 +1000 @@ -90,16 +90,23 @@ fun get_thms thy name = let val SOME { Rep_inject=rep_inject, Abs_name=absN, abs_type=absT, - Abs_inverse=abs_inverse, ...} = TypedefPackage.get_info thy name; + Abs_inverse=abs_inverse, ...} = Typedef.get_info thy name; val rewrite_rule = MetaSimplifier.rewrite_rule [istuple_UNIV_I, istuple_True_simp]; in (map rewrite_rule [rep_inject, abs_inverse], Const (absN, repT --> absT)) end; in thy - |> TypecopyPackage.add_typecopy (name, alphas) repT NONE + |> Typecopy.typecopy (Binding.name name, alphas) repT NONE |-> (fn (name, _) => `(fn thy => get_thms thy name)) end; +(* copied from earlier version of HOLogic *) +fun mk_curry t = + (case Term.fastype_of t of + T as (Type ("fun", [Type ("*", [A, B]), C])) => + Const ("curry", T --> A --> B --> C) $ t + | _ => raise TERM ("mk_curry: bad body type", [t])); + fun add_istuple_type (name, alphas) (left, right) thy = let val repT = HOLogic.mk_prodT (left, right); @@ -109,15 +116,16 @@ |> do_typedef name repT alphas ||> Sign.add_path name; - val abs_curry = HOLogic.mk_curry abs; + val abs_curry = mk_curry abs; val consT = fastype_of abs_curry; - val cons = Const (Sign.full_name typ_thy (name ^ consN), consT); + val consBind = Binding.name (name ^ consN); + val cons = Const (Sign.full_name typ_thy consBind, consT); val cons_spec = (name ^ consN ^ defN, Logic.mk_equals (cons, abs_curry)); val ([cons_def], cdef_thy) = typ_thy - |> Sign.add_consts_i [Syntax.no_syn (name ^ consN, consT)] - |> PureThy.add_defs_i false [Thm.no_attributes cons_spec]; + |> Sign.add_consts_i [Syntax.no_syn (consBind, consT)] + |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name cons_spec)]; val istuple = [abs_inverse, cons_def] MRS (rep_inject RS istuple_intro); val intros = [istuple] RL istuple_intros; @@ -133,13 +141,4 @@ end; -structure IsTupleIntros2 = TheoryDataFun -( - type T = IsTupleSupport.tagged_net; - val empty = IsTupleSupport.build_tagged_net "" []; - val copy = I; - val extend = I; - val merge = K IsTupleSupport.merge_tagged_nets; -); - diff -r c4e9a48bc50e -r 50406c4951d9 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Thu Aug 27 00:40:53 2009 +1000 +++ b/src/HOL/Tools/record.ML Thu Sep 10 15:18:43 2009 +1000 @@ -286,9 +286,12 @@ type record_data = {records: record_info Symtab.table, sel_upd: - {selectors: unit Symtab.table, + {selectors: (int * bool) Symtab.table, updates: string Symtab.table, - simpset: Simplifier.simpset}, + simpset: Simplifier.simpset, + defset: Simplifier.simpset, + foldcong: Simplifier.simpset, + unfoldcong: Simplifier.simpset}, equalities: thm Symtab.table, extinjects: thm list, extsplit: thm Symtab.table, (* maps extension name to split rule *) @@ -410,15 +413,25 @@ in SOME (s, dep, ismore) end | NONE => NONE end; -fun put_sel_upd names simps = RecordsData.map (fn {records, - sel_upd = {selectors, updates, simpset}, - equalities, extinjects, extsplit, splits, extfields, fieldext} => - make_record_data records - {selectors = fold (fn name => Symtab.update (name, ())) names selectors, - updates = fold (fn name => Symtab.update ((suffix updateN) name, name)) names updates, - simpset = Simplifier.addsimps (simpset, simps)} - equalities extinjects extsplit splits extfields fieldext); - +fun put_sel_upd names more depth simps defs (folds, unfolds) thy = + let + val all = names @ [more]; + val sels = map (rpair (depth, false)) names @ [(more, (depth, true))]; + val upds = map (suffix updateN) all ~~ all; + + val {records, sel_upd = {selectors, updates, simpset, + defset, foldcong, unfoldcong}, + equalities, extinjects, extsplit, splits, extfields, + fieldext} = RecordsData.get thy; + val data = make_record_data records + {selectors = fold Symtab.update_new sels selectors, + updates = fold Symtab.update_new upds updates, + simpset = Simplifier.addsimps (simpset, simps), + defset = Simplifier.addsimps (defset, defs), + foldcong = foldcong addcongs folds, + unfoldcong = unfoldcong addcongs unfolds} + equalities extinjects extsplit splits extfields fieldext; + in RecordsData.put data thy end; (* access 'equalities' *) @@ -958,7 +971,7 @@ fun get_accupd_simps thy term defset intros_tac = let val (acc, [body]) = strip_comb term; val recT = domain_type (fastype_of acc); - val updfuns = sort_distinct Term.fast_term_ord + val updfuns = sort_distinct TermOrd.fast_term_ord (get_updfuns body); fun get_simp upd = let val T = domain_type (fastype_of upd); @@ -975,8 +988,8 @@ in standard (othm RS dest) end; in map get_simp updfuns end; -structure SymSymTab = TableFun(type key = string * string - val ord = prod_ord fast_string_ord fast_string_ord); +structure SymSymTab = Table(type key = string * string + val ord = prod_ord fast_string_ord fast_string_ord); fun get_updupd_simp thy defset intros_tac u u' comp = let val f = Free ("f", domain_type (fastype_of u)); @@ -1019,7 +1032,8 @@ fun named_cterm_instantiate values thm = let fun match name (Var ((name', _), _)) = name = name' | match name _ = false; - fun getvar name = case (find_first (match name) (term_vars (prop_of thm))) + fun getvar name = case (find_first (match name) + (OldTerm.term_vars (prop_of thm))) of SOME var => cterm_of (theory_of_thm thm) var | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]) in @@ -1114,7 +1128,7 @@ (case mk_eq_terms (upd$k$r) of SOME (trm,trm',vars) => SOME (prove_unfold_defs thy ss domS [] [] - (list_all(vars,(equals rangeS$(sel$trm)$trm')))) + (list_all(vars,(Logic.mk_equals (sel$trm, trm'))))) | NONE => NONE) end | NONE => NONE) @@ -1206,7 +1220,7 @@ fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term = let val (lhs, rhs, vars, dups, simp, noops) = mk_updterm upds (Symtab.update (u, ()) above) term; - val (fvar, skelf) = K_skeleton (Sign.base_name s) (domain_type T) + val (fvar, skelf) = K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f; val (isnoop, skelf') = is_upd_noop s f term; val funT = domain_type T; @@ -1240,7 +1254,7 @@ in if simp then SOME (prove_unfold_defs thy ss baseT noops' [record_simproc] - (list_all(vars,(equals baseT$lhs$rhs)))) + (list_all(vars,(Logic.mk_equals (lhs, rhs))))) else NONE end) @@ -1559,7 +1573,7 @@ fun mk_istuple ((thy, i), (left, rght)) = let val suff = if i = 0 then ext_typeN else inner_typeN ^ (string_of_int i); - val nm = suffix suff (Sign.base_name name); + val nm = suffix suff (Long_Name.base_name name); val (cons, thy') = IsTupleSupport.add_istuple_type (nm, alphas_zeta) (fastype_of left, fastype_of rght) thy; in @@ -1586,7 +1600,7 @@ :: group16 (Library.drop (16, xs)); val vars' = group16 vars; val ((thy', i'), composites) = - foldl_map mk_even_istuple ((thy, i), vars'); + Library.foldl_map mk_even_istuple ((thy, i), vars'); in build_meta_tree_type i' thy' composites more end @@ -1711,14 +1725,13 @@ asm_simp_tac HOL_ss 1]) end; val induct = timeit_msg "record extension induct proof:" induct_prf; - val (([inject',induct',surjective',split_meta',ext_def'], - [dest_convs',upd_convs']), + val ([inject',induct',surjective',split_meta',ext_def'], thm_thy) = defs_thy |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name)) [("ext_inject", inject), ("ext_induct", induct), - ("ext_surjective", surjective), + ("ext_surjective", surject), ("ext_split", split_meta), ("ext_def", ext_def)] @@ -2114,7 +2127,7 @@ fun get_upd_acc_congs () = let val symdefs = map symmetric (sel_defs @ upd_defs); val fold_ss = HOL_basic_ss addsimps symdefs; - val ua_congs = map (simplify fold_ss) upd_acc_cong_assists; + val ua_congs = map (standard o simplify fold_ss) upd_acc_cong_assists; in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end; val (fold_congs, unfold_congs) = timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs; @@ -2138,12 +2151,6 @@ end; val induct = timeit_msg "record induct proof:" induct_prf; - fun surjective_prf () = - prove_standard [] surjective_prop (fn prems => - (EVERY [try_param_tac rN induct_scheme 1, - simp_tac (ss addsimps sel_convs_standard) 1])) - val surjective = timeit_msg "record surjective proof:" surjective_prf; - fun cases_scheme_prf_opt () = let val (_$(Pvar$_)) = concl_of induct_scheme; @@ -2171,17 +2178,16 @@ val cases = timeit_msg "record cases proof:" cases_prf; fun surjective_prf () = let - val o_ass_thm = symmetric (mk_meta_eq o_assoc); - val o_reassoc = simplify (HOL_basic_ss addsimps [o_ass_thm]); - val sel_defs' = map o_reassoc sel_defs; - val ss = HOL_basic_ss addsimps (ext_defs @ sel_defs'); + val leaf_ss = get_sel_upd_defs defs_thy + addsimps (sel_defs @ (o_assoc :: id_o_apps)); + val init_ss = HOL_basic_ss addsimps ext_defs; in prove_standard [] surjective_prop (fn prems => (EVERY [rtac surject_assist_idE 1, - simp_tac ss 1, + simp_tac init_ss 1, REPEAT (intros_tac 1 ORELSE (rtac surject_assistI 1 THEN - simp_tac (HOL_basic_ss addsimps id_o_apps) 1))])) + simp_tac leaf_ss 1))])) end; val surjective = timeit_msg "record surjective proof:" surjective_prf; @@ -2230,7 +2236,7 @@ fun split_ex_prf () = let val ss = HOL_basic_ss addsimps [not_ex RS sym, nth simp_thms 1]; - val [Pv] = term_vars (prop_of split_object); + val [Pv] = OldTerm.term_vars (prop_of split_object); val cPv = cterm_of defs_thy Pv; val cP = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0))); val so3 = cterm_instantiate ([(cPv, cP)]) split_object; @@ -2256,16 +2262,18 @@ val equality = timeit_msg "record equality proof:" equality_prf; val ((([sel_convs', upd_convs', sel_defs', upd_defs', - fold_congs', unfold_congs', surjective', + fold_congs', unfold_congs', [split_meta', split_object', split_ex'], derived_defs'], [surjective', equality']), [induct_scheme', induct', cases_scheme', cases']), thms_thy) = defs_thy |> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name)) [("select_convs", sel_convs_standard), - ("update_convs", upd_convs), + ("update_convs", upd_convs_standard), ("select_defs", sel_defs), ("update_defs", upd_defs), + ("fold_congs", fold_congs), + ("unfold_congs", unfold_congs), ("splits", [split_meta_standard,split_object,split_ex]), ("defs", derived_defs)] ||>> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name)) @@ -2289,7 +2297,7 @@ [Simplifier.simp_add, Nitpick_Const_Simps.add]), ((Binding.name "iffs", iffs), [iff_add])] |> put_record name (make_record_info args parent fields extension induct_scheme' ext_def) - |> put_sel_upd_names full_moreN depth sel_upd_simps + |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs') |> add_record_equalities extension_id equality' |> add_extinjects ext_inject