# HG changeset patch # User wenzelm # Date 1325263513 -3600 # Node ID 9a790f4a72be825bdc98f710ecbad0c401f7ea4d # Parent 8664713db1818a60301a051e0d9caaf2bf103262# Parent 4dba48d010d5d34dc3e56b980158e57b28bf6d3e merged diff -r 8664713db181 -r 9a790f4a72be src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Dec 30 11:11:57 2011 +0100 +++ b/src/HOL/Tools/record.ML Fri Dec 30 17:45:13 2011 +0100 @@ -949,14 +949,6 @@ (** record simprocs **) -fun future_forward_prf thy prf prop = - let val thm = - if ! quick_and_dirty then Skip_Proof.make_thm thy prop - else if Goal.future_enabled () then - Goal.future_result (Proof_Context.init_global thy) (Goal.fork prf) prop - else prf () - in Drule.export_without_context thm end; - fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) = (case get_updates thy u of SOME u_name => u_name = s @@ -1331,11 +1323,6 @@ Simplifier.simproc_global @{theory HOL} "ex_sel_eq_simproc" ["Ex t"] (fn thy => fn ss => fn t => let - fun prove prop = - Skip_Proof.prove_global thy [] [] prop - (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy) - addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1); - fun mkeq (lr, Teq, (sel, Tsel), x) i = if is_selector thy sel then let @@ -1362,8 +1349,11 @@ list_all ([("r", T)], Logic.mk_equals (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True})); - in SOME (prove prop) end - handle TERM _ => NONE) + in + SOME (Skip_Proof.prove_global thy [] [] prop + (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy) + addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1)) + end handle TERM _ => NONE) | _ => NONE) end); @@ -1479,8 +1469,7 @@ val params = Logic.strip_params g; val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g); val rule' = Thm.lift_rule cgoal rule; - val (P, ys) = strip_comb (HOLogic.dest_Trueprop - (Logic.strip_assums_concl (prop_of rule'))); + val (P, ys) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_assums_concl (prop_of rule'))); (*ca indicates if rule is a case analysis or induction rule*) val (x, ca) = (case rev (drop (length params) ys) of @@ -1600,16 +1589,14 @@ (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s)); val split_meta_prop = (* FIXME local P *) - let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in + let val P = Free (singleton (Name.variant_list variants) "P", extT --> propT) in Logic.mk_equals (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext)) end; - val prove = Skip_Proof.prove_global defs_thy; - val inject = timeit_msg ctxt "record extension inject proof:" (fn () => simplify HOL_ss - (prove [] [] inject_prop + (Skip_Proof.prove_global defs_thy [] [] inject_prop (fn _ => simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN REPEAT_DETERM @@ -1639,9 +1626,8 @@ surject end); - val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () => - prove [] [] split_meta_prop + Skip_Proof.prove_global defs_thy [] [] split_meta_prop (fn _ => EVERY1 [rtac equal_intr_rule, Goal.norm_hhf_tac, @@ -1651,21 +1637,20 @@ val induct = timeit_msg ctxt "record extension induct proof:" (fn () => let val (assm, concl) = induct_prop in - prove [] [assm] concl + Skip_Proof.prove_global defs_thy [] [assm] concl (fn {prems, ...} => cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1 THEN resolve_tac prems 2 THEN asm_simp_tac HOL_ss 1) end); - val ([induct', inject', surjective', split_meta'], thm_thy) = + val ([(_, [induct']), (_, [inject']), (_, [surjective']), (_, [split_meta'])], thm_thy) = defs_thy - |> Global_Theory.add_thms (map (Thm.no_attributes o apfst Binding.name) - [("ext_induct", induct), - ("ext_inject", inject), - ("ext_surjective", surject), - ("ext_split", split_meta)]); - + |> Global_Theory.note_thmss "" + [((Binding.name "ext_induct", []), [([induct], [])]), + ((Binding.name "ext_inject", []), [([inject], [])]), + ((Binding.name "ext_surjective", []), [([surject], [])]), + ((Binding.name "ext_split", []), [([split_meta], [])])]; in (((ext_name, ext_type), (ext_tyco, alphas_zeta), extT, induct', inject', surjective', split_meta', ext_def), thm_thy) @@ -1692,27 +1677,6 @@ fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT; -fun obj_to_meta_all thm = - let - fun E thm = (* FIXME proper name *) - (case SOME (spec OF [thm]) handle THM _ => NONE of - SOME thm' => E thm' - | NONE => thm); - val th1 = E thm; - val th2 = Drule.forall_intr_vars th1; - in th2 end; - -fun meta_to_obj_all thm = - let - val thy = Thm.theory_of_thm thm; - val prop = Thm.prop_of thm; - val params = Logic.strip_params prop; - val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop); - val ct = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl))); - val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct)); - in Thm.implies_elim thm' thm end; - - (* code generation *) fun mk_random_eq tyco vs extN Ts = @@ -1786,16 +1750,16 @@ fun add_code ext_tyco vs extT ext simps inject thy = let val eq = - (HOLogic.mk_Trueprop o HOLogic.mk_eq) + HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT), - Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT)); + Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT))); fun tac eq_def = Class.intro_classes_tac [] THEN rewrite_goals_tac [Simpdata.mk_eq eq_def] THEN ALLGOALS (rtac @{thm refl}); fun mk_eq thy eq_def = Simplifier.rewrite_rule - [(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject; + [AxClass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject; fun mk_eq_refl thy = @{thm equal_refl} |> Thm.instantiate @@ -2042,7 +2006,8 @@ |> Sign.restore_naming thy |> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd |> Typedecl.abbrev_global - (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0 |> snd + (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0 + |> snd |> Sign.qualified_path false binding |> fold (fn ((x, T), mx) => snd o Sign.declare_const_global ((Binding.name x, T), mx)) (sel_decls ~~ (field_syntax @ [NoSyn])) @@ -2091,8 +2056,7 @@ (*cases*) val cases_scheme_prop = - (All (map dest_Free all_vars_more) ((r0 === r_rec0) ==> Trueprop C)) - ==> Trueprop C; + (All (map dest_Free all_vars_more) ((r0 === r_rec0) ==> Trueprop C), Trueprop C); val cases_prop = (All (map dest_Free all_vars) ((r_unit0 === r_rec_unit0) ==> Trueprop C)) @@ -2101,7 +2065,7 @@ (*split*) val split_meta_prop = let - val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0-->Term.propT); + val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> propT); in Logic.mk_equals (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0)) @@ -2126,17 +2090,15 @@ (* 3rd stage: thms_thy *) - val prove = Skip_Proof.prove_global defs_thy; - - val ss = get_simpset defs_thy; - val simp_defs_tac = - asm_full_simp_tac (ss addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms)); + val record_ss = get_simpset defs_thy; + val sel_upd_ss = record_ss addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms); - val sel_convs = timeit_msg ctxt "record sel_convs proof:" (fn () => - map (fn prop => prove [] [] prop (K (ALLGOALS simp_defs_tac))) sel_conv_props); - - val upd_convs = timeit_msg ctxt "record upd_convs proof:" (fn () => - map (fn prop => prove [] [] prop (K (ALLGOALS simp_defs_tac))) upd_conv_props); + val (sel_convs, upd_convs) = + timeit_msg ctxt "record sel_convs/upd_convs proof:" (fn () => + Par_List.map (fn prop => + Skip_Proof.prove_global defs_thy [] [] prop + (K (ALLGOALS (asm_full_simp_tac sel_upd_ss)))) (sel_conv_props @ upd_conv_props)) + |> chop (length sel_conv_props); val (fold_congs, unfold_congs) = timeit_msg ctxt "record upd fold/unfold congs:" (fn () => let @@ -2148,7 +2110,7 @@ val parent_induct = Option.map #induct_scheme (try List.last parents); val induct_scheme = timeit_msg ctxt "record induct_scheme proof:" (fn () => - prove [] [] induct_scheme_prop + Skip_Proof.prove_global defs_thy [] [] induct_scheme_prop (fn _ => EVERY [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1, @@ -2156,31 +2118,10 @@ asm_simp_tac HOL_basic_ss 1])); val induct = timeit_msg ctxt "record induct proof:" (fn () => - let val (assm, concl) = induct_prop in - prove [] [assm] concl (fn {prems, ...} => - try_param_tac rN induct_scheme 1 - THEN try_param_tac "more" @{thm unit.induct} 1 - THEN resolve_tac prems 1) - end); - - fun cases_scheme_prf () = - let - val _ $ (Pvar $ _) = concl_of induct_scheme; - val ind = - cterm_instantiate - [(cterm_of defs_thy Pvar, cterm_of defs_thy - (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))] - induct_scheme; - in Object_Logic.rulify (mp OF [ind, refl]) end; - - val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" (fn () => - future_forward_prf defs_thy cases_scheme_prf cases_scheme_prop); - - val cases = timeit_msg ctxt "record cases proof:" (fn () => - prove [] [] cases_prop - (fn _ => - try_param_tac rN cases_scheme 1 THEN - ALLGOALS (asm_full_simp_tac (HOL_basic_ss addsimps [@{thm unit_all_eq1}])))); + Skip_Proof.prove_global defs_thy [] [#1 induct_prop] (#2 induct_prop) (fn {prems, ...} => + try_param_tac rN induct_scheme 1 + THEN try_param_tac "more" @{thm unit.induct} 1 + THEN resolve_tac prems 1)); val surjective = timeit_msg ctxt "record surjective proof:" (fn () => let @@ -2188,7 +2129,7 @@ get_sel_upd_defs defs_thy addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id}); val init_ss = HOL_basic_ss addsimps ext_defs; in - prove [] [] surjective_prop + Skip_Proof.prove_global defs_thy [] [] surjective_prop (fn _ => EVERY [rtac surject_assist_idE 1, @@ -2198,8 +2139,20 @@ (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))]) end); + val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" (fn () => + Skip_Proof.prove_global defs_thy [] [#1 cases_scheme_prop] (#2 cases_scheme_prop) + (fn {prems, ...} => + resolve_tac prems 1 THEN + rtac surjective 1)); + + val cases = timeit_msg ctxt "record cases proof:" (fn () => + Skip_Proof.prove_global defs_thy [] [] cases_prop + (fn _ => + try_param_tac rN cases_scheme 1 THEN + ALLGOALS (asm_full_simp_tac (HOL_basic_ss addsimps @{thms unit_all_eq1})))); + val split_meta = timeit_msg ctxt "record split_meta proof:" (fn () => - prove [] [] split_meta_prop + Skip_Proof.prove_global defs_thy [] [] split_meta_prop (fn _ => EVERY1 [rtac equal_intr_rule, Goal.norm_hhf_tac, @@ -2207,91 +2160,57 @@ rtac (@{thm prop_subst} OF [surjective]), REPEAT o etac @{thm meta_allE}, atac])); - fun split_object_prf () = - let - val cPI = cterm_of defs_thy (lambda r0 (Trueprop (P $ r0))); - val _ $ Abs (_, _, P $ _) = fst (Logic.dest_equals (concl_of split_meta)); - val cP = cterm_of defs_thy P; - val split_meta' = cterm_instantiate [(cP, cPI)] split_meta; - val (l, r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop); - val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l); - val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r); - val thl = - Thm.assume cl (*All r. P r*) (* 1 *) - |> obj_to_meta_all (*!!r. P r*) - |> Thm.equal_elim split_meta' (*!!n m more. P (ext n m more)*) - |> meta_to_obj_all (*All n m more. P (ext n m more)*) (* 2*) - |> Thm.implies_intr cl (* 1 ==> 2 *) - val thr = - Thm.assume cr (*All n m more. P (ext n m more)*) - |> obj_to_meta_all (*!!n m more. P (ext n m more)*) - |> Thm.equal_elim (Thm.symmetric split_meta') (*!!r. P r*) - |> meta_to_obj_all (*All r. P r*) - |> Thm.implies_intr cr (* 2 ==> 1 *) - in thr COMP (thl COMP iffI) end; - val split_object = timeit_msg ctxt "record split_object proof:" (fn () => - future_forward_prf defs_thy split_object_prf split_object_prop); + Skip_Proof.prove_global defs_thy [] [] split_object_prop + (fn _ => + rtac @{lemma "Trueprop A == Trueprop B ==> A = B" by (rule iffI) unfold} 1 THEN + rewrite_goals_tac @{thms atomize_all [symmetric]} THEN + rtac split_meta 1)); val split_ex = timeit_msg ctxt "record split_ex proof:" (fn () => - let - val ss = HOL_basic_ss addsimps @{thms not_ex [symmetric] Not_eq_iff}; - val P_nm = fst (dest_Free P); - val not_P = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0))); - val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object; - val so'' = simplify ss so'; - in prove [] [] split_ex_prop (fn _ => resolve_tac [so''] 1) end); - - fun equality_tac thms = - let - val s' :: s :: eqs = rev thms; - val ss' = ss addsimps (s' :: s :: sel_convs); - val eqs' = map (simplify ss') eqs; - in simp_tac (HOL_basic_ss addsimps (s' :: s :: eqs')) 1 end; + Skip_Proof.prove_global defs_thy [] [] split_ex_prop + (fn _ => + simp_tac + (HOL_basic_ss addsimps + (@{lemma "EX x. P x == ~ (ALL x. ~ P x)" by simp} :: + @{thms not_not Not_eq_iff})) 1 THEN + rtac split_object 1)); val equality = timeit_msg ctxt "record equality proof:" (fn () => - prove [] [] equality_prop (fn {context, ...} => - fn st => - let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in - st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 THEN - res_inst_tac context [((rN, 0), s')] cases_scheme 1 THEN - Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1) - (*simp_defs_tac would also work but is less efficient*) - end)); + Skip_Proof.prove_global defs_thy [] [] equality_prop + (fn _ => asm_full_simp_tac (record_ss addsimps (split_meta :: sel_convs)) 1)); - val ((([sel_convs', upd_convs', sel_defs', upd_defs', - fold_congs', unfold_congs', - splits' as [split_meta', split_object', split_ex'], derived_defs'], - [surjective', equality']), - [induct_scheme', induct', cases_scheme', cases']), thms_thy) = - defs_thy - |> (Global_Theory.add_thmss o map (Thm.no_attributes o apfst Binding.name)) - [("select_convs", sel_convs), - ("update_convs", upd_convs), - ("select_defs", sel_defs), - ("update_defs", upd_defs), - ("fold_congs", fold_congs), - ("unfold_congs", unfold_congs), - ("splits", [split_meta, split_object, split_ex]), - ("defs", derived_defs)] - ||>> (Global_Theory.add_thms o map (Thm.no_attributes o apfst Binding.name)) - [("surjective", surjective), - ("equality", equality)] - ||>> (Global_Theory.add_thms o (map o apfst o apfst) Binding.name) - [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)), - (("induct", induct), induct_type_global name), - (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)), - (("cases", cases), cases_type_global name)]; + val ([(_, sel_convs'), (_, upd_convs'), (_, sel_defs'), (_, upd_defs'), + (_, fold_congs'), (_, unfold_congs'), + (_, splits' as [split_meta', split_object', split_ex']), (_, derived_defs'), + (_, [surjective']), (_, [equality']), (_, [induct_scheme']), (_, [induct']), + (_, [cases_scheme']), (_, [cases'])], thms_thy) = defs_thy + |> Global_Theory.note_thmss "" + [((Binding.name "select_convs", []), [(sel_convs, [])]), + ((Binding.name "update_convs", []), [(upd_convs, [])]), + ((Binding.name "select_defs", []), [(sel_defs, [])]), + ((Binding.name "update_defs", []), [(upd_defs, [])]), + ((Binding.name "fold_congs", []), [(fold_congs, [])]), + ((Binding.name "unfold_congs", []), [(unfold_congs, [])]), + ((Binding.name "splits", []), [([split_meta, split_object, split_ex], [])]), + ((Binding.name "defs", []), [(derived_defs, [])]), + ((Binding.name "surjective", []), [([surjective], [])]), + ((Binding.name "equality", []), [([equality], [])]), + ((Binding.name "induct_scheme", induct_type_global (suffix schemeN name)), + [([induct_scheme], [])]), + ((Binding.name "induct", induct_type_global name), [([induct], [])]), + ((Binding.name "cases_scheme", cases_type_global (suffix schemeN name)), + [([cases_scheme], [])]), + ((Binding.name "cases", cases_type_global name), [([cases], [])])]; val sel_upd_simps = sel_convs' @ upd_convs'; val sel_upd_defs = sel_defs' @ upd_defs'; val depth = parent_len + 1; - val ([simps', iffs'], thms_thy') = - thms_thy - |> Global_Theory.add_thmss - [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]), - ((Binding.name "iffs", [ext_inject]), [iff_add])]; + val ([(_, simps'), (_, iffs')], thms_thy') = thms_thy + |> Global_Theory.note_thmss "" + [((Binding.name "simps", [Simplifier.simp_add]), [(sel_upd_simps, [])]), + ((Binding.name "iffs", [iff_add]), [([ext_inject], [])])]; val info = make_info alphas parent fields extension