# HG changeset patch # User huffman # Date 1325406468 -3600 # Node ID d7eb081cf220ebda3193dcf709932efe0432f033 # Parent 88ef116e0522e58565434b5987535a778cbafc10# Parent 81ebd0cdb3003ed8d1fc275e72084ff5fc7db111 merged diff -r 88ef116e0522 -r d7eb081cf220 Admin/contributed_components --- a/Admin/contributed_components Fri Dec 30 16:08:35 2011 +0100 +++ b/Admin/contributed_components Sun Jan 01 09:27:48 2012 +0100 @@ -1,7 +1,7 @@ #contributed components contrib/cvc3-2.2 contrib/e-1.4 -contrib/kodkodi-1.2.16 +#contrib/kodkodi-1.2.16 contrib/spass-3.7 contrib/scala-2.8.1.final contrib/vampire-1.0 diff -r 88ef116e0522 -r d7eb081cf220 src/HOL/IMP/Abs_Int0.thy --- a/src/HOL/IMP/Abs_Int0.thy Fri Dec 30 16:08:35 2011 +0100 +++ b/src/HOL/IMP/Abs_Int0.thy Sun Jan 01 09:27:48 2012 +0100 @@ -12,7 +12,7 @@ context Val_abs begin -fun aval' :: "aexp \ 'a st \ 'a" where +fun aval' :: "aexp \ 'av st \ 'av" where "aval' (N n) S = num' n" | "aval' (V x) S = lookup S x" | "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" @@ -22,10 +22,14 @@ end -locale Abs_Int = Val_abs +text{* The for-clause (here and elsewhere) only serves the purpose of fixing +the name of the type parameter @{typ 'av} which would otherwise be renamed to +@{typ 'a}. *} + +locale Abs_Int = Val_abs \ for \ :: "'av::SL_top \ val set" begin -fun step' :: "'a st option \ 'a st option acom \ 'a st option acom" where +fun step' :: "'av st option \ 'av st option acom \ 'av st option acom" where "step' S (SKIP {P}) = (SKIP {S})" | "step' S (x ::= e {P}) = x ::= e {case S of None \ None | Some S \ Some(update S x (aval' e S))}" | @@ -36,7 +40,7 @@ "step' S ({Inv} WHILE b DO c {P}) = {S \ post c} WHILE b DO step' Inv c {Inv}" -definition AI :: "com \ 'a st option acom option" where +definition AI :: "com \ 'av st option acom option" where "AI = lpfp\<^isub>c (step' \)" diff -r 88ef116e0522 -r d7eb081cf220 src/HOL/IMP/Abs_Int0_const.thy --- a/src/HOL/IMP/Abs_Int0_const.thy Fri Dec 30 16:08:35 2011 +0100 +++ b/src/HOL/IMP/Abs_Int0_const.thy Sun Jan 01 09:27:48 2012 +0100 @@ -52,7 +52,8 @@ end -interpretation Val_abs \_cval Const plus_cval +interpretation Val_abs +where \ = \_cval and num' = Const and plus' = plus_cval defines aval'_const is aval' proof case goal1 thus ?case @@ -66,7 +67,8 @@ by(auto simp: plus_cval_cases split: cval.split) qed -interpretation Abs_Int \_cval Const plus_cval +interpretation Abs_Int +where \ = \_cval and num' = Const and plus' = plus_cval defines AI_const is AI and step_const is step' proof qed @@ -74,7 +76,8 @@ text{* Monotonicity: *} -interpretation Abs_Int_mono \_cval Const plus_cval +interpretation Abs_Int_mono +where \ = \_cval and num' = Const and plus' = plus_cval proof case goal1 thus ?case by(auto simp: plus_cval_cases split: cval.split) diff -r 88ef116e0522 -r d7eb081cf220 src/HOL/IMP/Abs_Int0_fun.thy --- a/src/HOL/IMP/Abs_Int0_fun.thy Fri Dec 30 16:08:35 2011 +0100 +++ b/src/HOL/IMP/Abs_Int0_fun.thy Sun Jan 01 09:27:48 2012 +0100 @@ -234,26 +234,26 @@ text{* The interface for abstract values: *} locale Val_abs = -fixes \ :: "'a::SL_top \ val set" +fixes \ :: "'av::SL_top \ val set" assumes mono_gamma: "a \ b \ \ a \ \ b" and gamma_Top[simp]: "\ \ = UNIV" -fixes num' :: "val \ 'a" -and plus' :: "'a \ 'a \ 'a" +fixes num' :: "val \ 'av" +and plus' :: "'av \ 'av \ 'av" assumes gamma_num': "n : \(num' n)" and gamma_plus': "n1 : \ a1 \ n2 : \ a2 \ n1+n2 : \(plus' a1 a2)" -type_synonym 'a st = "(vname \ 'a)" +type_synonym 'av st = "(vname \ 'av)" -locale Abs_Int_Fun = Val_abs +locale Abs_Int_Fun = Val_abs \ for \ :: "'av::SL_top \ val set" begin -fun aval' :: "aexp \ 'a st \ 'a" where +fun aval' :: "aexp \ 'av st \ 'av" where "aval' (N n) S = num' n" | "aval' (V x) S = S x" | "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" -fun step' :: "'a st option \ 'a st option acom \ 'a st option acom" +fun step' :: "'av st option \ 'av st option acom \ 'av st option acom" where "step' S (SKIP {P}) = (SKIP {S})" | "step' S (x ::= e {P}) = @@ -264,7 +264,7 @@ "step' S ({Inv} WHILE b DO c {P}) = {S \ post c} WHILE b DO (step' Inv c) {Inv}" -definition AI :: "com \ 'a st option acom option" where +definition AI :: "com \ 'av st option acom option" where "AI = lpfp\<^isub>c (step' \)" @@ -272,13 +272,13 @@ by(induct c arbitrary: S) (simp_all add: Let_def) -abbreviation \\<^isub>f :: "'a st \ state set" +abbreviation \\<^isub>f :: "'av st \ state set" where "\\<^isub>f == \_fun \" -abbreviation \\<^isub>o :: "'a st option \ state set" +abbreviation \\<^isub>o :: "'av st option \ state set" where "\\<^isub>o == \_option \\<^isub>f" -abbreviation \\<^isub>c :: "'a st option acom \ state set acom" +abbreviation \\<^isub>c :: "'av st option acom \ state set acom" where "\\<^isub>c == map_acom \\<^isub>o" lemma gamma_f_Top[simp]: "\\<^isub>f Top = UNIV" diff -r 88ef116e0522 -r d7eb081cf220 src/HOL/IMP/Abs_Int1.thy --- a/src/HOL/IMP/Abs_Int1.thy Fri Dec 30 16:08:35 2011 +0100 +++ b/src/HOL/IMP/Abs_Int1.thy Sun Jan 01 09:27:48 2012 +0100 @@ -38,8 +38,7 @@ end locale Val_abs1_gamma = - Val_abs \ num' plus' - for \ :: "'a::L_top_bot \ val set" and num' plus' + + Val_abs where \ = \ for \ :: "'av::L_top_bot \ val set" + assumes inter_gamma_subset_gamma_meet: "\ a1 \ \ a2 \ \(a1 \ a2)" and gamma_Bot[simp]: "\ \ = {}" @@ -54,22 +53,25 @@ end -locale Val_abs1 = Val_abs1_gamma + -fixes filter_plus' :: "'a \ 'a \ 'a \ 'a * 'a" -and filter_less' :: "bool \ 'a \ 'a \ 'a * 'a" +locale Val_abs1 = + Val_abs1_gamma where \ = \ + for \ :: "'av::L_top_bot \ val set" + +fixes filter_plus' :: "'av \ 'av \ 'av \ 'av * 'av" +and filter_less' :: "bool \ 'av \ 'av \ 'av * 'av" assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \ n1 : \ a1 \ n2 : \ a2 \ n1+n2 : \ a \ n1 : \ a1' \ n2 : \ a2'" and filter_less': "filter_less' (n1 n1 : \ a1 \ n2 : \ a2 \ n1 : \ a1' \ n2 : \ a2'" -locale Abs_Int1 = Val_abs1 +locale Abs_Int1 = + Val_abs1 where \ = \ for \ :: "'av::L_top_bot \ val set" begin lemma in_gamma_join_UpI: "s : \\<^isub>o S1 \ s : \\<^isub>o S2 \ s : \\<^isub>o(S1 \ S2)" by (metis (no_types) join_ge1 join_ge2 mono_gamma_o set_rev_mp) -fun aval'' :: "aexp \ 'a st option \ 'a" where +fun aval'' :: "aexp \ 'av st option \ 'av" where "aval'' e None = \" | "aval'' e (Some sa) = aval' e sa" @@ -78,7 +80,7 @@ subsubsection "Backward analysis" -fun afilter :: "aexp \ 'a \ 'a st option \ 'a st option" where +fun afilter :: "aexp \ 'av \ 'av st option \ 'av st option" where "afilter (N n) a S = (if n : \ a then S else None)" | "afilter (V x) a S = (case S of None \ None | Some S \ let a' = lookup S x \ a in @@ -97,7 +99,7 @@ making the analysis less precise. *} -fun bfilter :: "bexp \ bool \ 'a st option \ 'a st option" where +fun bfilter :: "bexp \ bool \ 'av st option \ 'av st option" where "bfilter (Bc v) res S = (if v=res then S else None)" | "bfilter (Not b) res S = bfilter b (\ res) S" | "bfilter (And b1 b2) res S = @@ -139,7 +141,7 @@ qed -fun step' :: "'a st option \ 'a st option acom \ 'a st option acom" +fun step' :: "'av st option \ 'av st option acom \ 'av st option acom" where "step' S (SKIP {P}) = (SKIP {S})" | "step' S (x ::= e {P}) = @@ -153,7 +155,7 @@ WHILE b DO step' (bfilter b True Inv) c {bfilter b False Inv}" -definition AI :: "com \ 'a st option acom option" where +definition AI :: "com \ 'av st option acom option" where "AI = lpfp\<^isub>c (step' \)" lemma strip_step'[simp]: "strip(step' S c) = strip c" diff -r 88ef116e0522 -r d7eb081cf220 src/HOL/IMP/Abs_Int1_ivl.thy --- a/src/HOL/IMP/Abs_Int1_ivl.thy Fri Dec 30 16:08:35 2011 +0100 +++ b/src/HOL/IMP/Abs_Int1_ivl.thy Sun Jan 01 09:27:48 2012 +0100 @@ -170,7 +170,8 @@ I (max_option False (l1 + Some 1) l2) h2) else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))" -interpretation Val_abs \_ivl num_ivl plus_ivl +interpretation Val_abs +where \ = \_ivl and num' = num_ivl and plus' = plus_ivl defines aval_ivl is aval' proof case goal1 thus ?case @@ -184,7 +185,8 @@ by(auto simp add: \_ivl_def plus_ivl_def split: ivl.split option.splits) qed -interpretation Val_abs1_gamma \_ivl num_ivl plus_ivl +interpretation Val_abs1_gamma +where \ = \_ivl and num' = num_ivl and plus' = plus_ivl proof case goal1 thus ?case by(auto simp add: \_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split) @@ -201,8 +203,9 @@ done -interpretation - Val_abs1 \_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl +interpretation Val_abs1 +where \ = \_ivl and num' = num_ivl and plus' = plus_ivl +and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl proof case goal1 thus ?case by(auto simp add: filter_plus_ivl_def) @@ -213,8 +216,9 @@ auto simp: \_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits) qed -interpretation - Abs_Int1 \_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl +interpretation Abs_Int1 +where \ = \_ivl and num' = num_ivl and plus' = plus_ivl +and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl defines afilter_ivl is afilter and bfilter_ivl is bfilter and step_ivl is step' @@ -225,8 +229,9 @@ text{* Monotonicity: *} -interpretation - Abs_Int1_mono \_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl +interpretation Abs_Int1_mono +where \ = \_ivl and num' = num_ivl and plus' = plus_ivl +and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl proof case goal1 thus ?case by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits) diff -r 88ef116e0522 -r d7eb081cf220 src/HOL/IMP/Abs_Int2.thy --- a/src/HOL/IMP/Abs_Int2.thy Fri Dec 30 16:08:35 2011 +0100 +++ b/src/HOL/IMP/Abs_Int2.thy Sun Jan 01 09:27:48 2012 +0100 @@ -180,10 +180,11 @@ apply(auto simp add: pfp_WN_def prefp_def split: option.splits) by (metis (no_types) strip_lpfpc strip_map2_acom strip_while) -locale Abs_Int2 = Abs_Int1_mono \ for \ :: "'a::{WN,L_top_bot} \ val set" +locale Abs_Int2 = Abs_Int1_mono +where \=\ for \ :: "'av::{WN,L_top_bot} \ val set" begin -definition AI_WN :: "com \ 'a st option acom option" where +definition AI_WN :: "com \ 'av st option acom option" where "AI_WN = pfp_WN (step' \)" lemma AI_WN_sound: "AI_WN c = Some c' \ CS UNIV c \ \\<^isub>c c'" @@ -206,8 +207,9 @@ end -interpretation - Abs_Int2 num_ivl plus_ivl filter_plus_ivl filter_less_ivl \_ivl +interpretation Abs_Int2 +where \ = \_ivl and num' = num_ivl and plus' = plus_ivl +and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl defines AI_ivl' is AI_WN proof qed diff -r 88ef116e0522 -r d7eb081cf220 src/HOL/IMP/Abs_State.thy --- a/src/HOL/IMP/Abs_State.thy Fri Dec 30 16:08:35 2011 +0100 +++ b/src/HOL/IMP/Abs_State.thy Sun Jan 01 09:27:48 2012 +0100 @@ -61,13 +61,13 @@ context Val_abs begin -abbreviation \\<^isub>f :: "'a st \ state set" +abbreviation \\<^isub>f :: "'av st \ state set" where "\\<^isub>f == \_st \" -abbreviation \\<^isub>o :: "'a st option \ state set" +abbreviation \\<^isub>o :: "'av st option \ state set" where "\\<^isub>o == \_option \\<^isub>f" -abbreviation \\<^isub>c :: "'a st option acom \ state set acom" +abbreviation \\<^isub>c :: "'av st option acom \ state set acom" where "\\<^isub>c == map_acom \\<^isub>o" lemma gamma_f_Top[simp]: "\\<^isub>f Top = UNIV" diff -r 88ef116e0522 -r d7eb081cf220 src/HOL/Metis_Examples/Proxies.thy --- a/src/HOL/Metis_Examples/Proxies.thy Fri Dec 30 16:08:35 2011 +0100 +++ b/src/HOL/Metis_Examples/Proxies.thy Sun Jan 01 09:27:48 2012 +0100 @@ -40,7 +40,7 @@ definition "A = {xs\'a list. True}" lemma "xs \ A" -sledgehammer [expect = some] +sledgehammer(* FIXME [expect = some] *) by (metis_exhaust A_def mem_Collect_eq) definition "B (y::int) \ y \ 0" diff -r 88ef116e0522 -r d7eb081cf220 src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Fri Dec 30 16:08:35 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Sun Jan 01 09:27:48 2012 +0100 @@ -310,22 +310,25 @@ local -(* FIXME proper name context!? *) fun gen_dest_case name_of type_of ctxt d used t = (case apfst name_of (strip_comb t) of (SOME cname, ts as _ :: _) => let val (fs, x) = split_last ts; - fun strip_abs i t = + fun strip_abs i Us t = let val zs = strip_abs_vars t; - val _ = if length zs < i then raise CASE_ERROR ("", 0) else (); - val (xs, ys) = chop i zs; + val j = length zs; + val (xs, ys) = + if j < i then (zs @ map (pair "x") (drop j Us), []) + else chop i zs; val u = list_abs (ys, strip_abs_body t); - val xs' = - map Free - (Name.variant_list (Misc_Legacy.add_term_names (u, used)) (map #1 xs) ~~ map #2 xs); - in (xs', subst_bounds (rev xs', u)) end; + val xs' = map Free + ((fold_map Name.variant (map fst xs) + (Term.declare_term_names u used) |> fst) ~~ + map snd xs); + val (xs1, xs2) = chop j xs' + in (xs', list_comb (subst_bounds (rev xs1, u), xs2)) end; fun is_dependent i t = let val k = length (strip_abs_vars t) - i in k < 0 orelse exists (fn j => j >= k) (loose_bnos (strip_abs_body t)) end; @@ -341,8 +344,9 @@ let val cases = map (fn (Const (s, U), t) => let - val k = length (binder_types U); - val p as (xs, _) = strip_abs k t; + val Us = binder_types U; + val k = length Us; + val p as (xs, _) = strip_abs k Us t; in (Const (s, map type_of xs ---> type_of x), p, is_dependent k t) end) (constructors ~~ fs); @@ -352,7 +356,7 @@ val R = type_of t; val dummy = if d then Term.dummy_pattern R - else Free (singleton (Name.variant_list used) "x", R); + else Free (Name.variant "x" used |> fst, R); in SOME (x, map mk_case @@ -370,7 +374,7 @@ else filter_out (fn (c, _, _) => member op aconv cs c) cases @ [(dummy, ([], default), false)]))) - end handle CASE_ERROR _ => NONE + end else NONE | _ => NONE) end @@ -389,7 +393,7 @@ local fun strip_case'' dest (pat, rhs) = - (case dest (Term.add_free_names pat []) rhs of + (case dest (Term.declare_term_frees pat Name.context) rhs of SOME (exp as Free _, clauses) => if Term.exists_subterm (curry (op aconv) exp) pat andalso not (exists (fn (_, rhs') => @@ -401,7 +405,7 @@ | _ => [(pat, rhs)]); fun gen_strip_case dest t = - (case dest [] t of + (case dest Name.context t of SOME (x, clauses) => SOME (x, maps (strip_case'' dest) clauses) | NONE => NONE); diff -r 88ef116e0522 -r d7eb081cf220 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Dec 30 16:08:35 2011 +0100 +++ b/src/HOL/Tools/record.ML Sun Jan 01 09:27:48 2012 +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