# HG changeset patch # User wenzelm # Date 1398429551 -7200 # Node ID f2ffead641d46c027dd50bb85ab2874affc5a328 # Parent d8f32f55e4633a9e4fbc96ae0df9c9ddfe9924eb# Parent e1317a26f8c0a704f3cea900187fc6dad445294c merged diff -r e1317a26f8c0 -r f2ffead641d4 src/Doc/Classes/Classes.thy --- a/src/Doc/Classes/Classes.thy Fri Apr 25 14:18:13 2014 +0200 +++ b/src/Doc/Classes/Classes.thy Fri Apr 25 14:39:11 2014 +0200 @@ -175,7 +175,7 @@ end %quote text {* - \noindent Note the occurence of the name @{text mult_nat} in the + \noindent Note the occurrence of the name @{text mult_nat} in the primrec declaration; by default, the local name of a class operation @{text f} to be instantiated on type constructor @{text \} is mangled as @{text f_\}. In case of uncertainty, these names may be diff -r e1317a26f8c0 -r f2ffead641d4 src/HOL/Auth/Guard/Extensions.thy --- a/src/HOL/Auth/Guard/Extensions.thy Fri Apr 25 14:18:13 2014 +0200 +++ b/src/HOL/Auth/Guard/Extensions.thy Fri Apr 25 14:39:11 2014 +0200 @@ -37,7 +37,6 @@ subsubsection{*declarations for tactics*} declare analz_subset_parts [THEN subsetD, dest] -declare image_eq_UN [simp] declare parts_insert2 [simp] declare analz_cut [dest] declare split_if_asm [split] @@ -112,8 +111,9 @@ lemma finite_keysFor [intro]: "finite G ==> finite (keysFor G)" apply (simp add: keysFor_def) -apply (rule finite_UN_I, auto) -apply (erule finite_induct, auto) +apply (rule finite_imageI) +apply (induct G rule: finite_induct) +apply auto apply (case_tac "EX K X. x = Crypt K X", clarsimp) apply (subgoal_tac "{Ka. EX Xa. (Ka=K & Xa=X) | Crypt Ka Xa:F} = insert K (usekeys F)", auto simp: usekeys_def) diff -r e1317a26f8c0 -r f2ffead641d4 src/HOL/Auth/Guard/Guard.thy --- a/src/HOL/Auth/Guard/Guard.thy Fri Apr 25 14:18:13 2014 +0200 +++ b/src/HOL/Auth/Guard/Guard.thy Fri Apr 25 14:39:11 2014 +0200 @@ -56,7 +56,7 @@ by (erule guard.induct, auto) lemma guard_Crypt: "[| Crypt K Y:guard n Ks; K ~:invKey`Ks |] ==> Y:guard n Ks" -by (ind_cases "Crypt K Y:guard n Ks", auto) + by (ind_cases "Crypt K Y:guard n Ks") (auto intro!: image_eqI) lemma guard_MPair [iff]: "({|X,Y|}:guard n Ks) = (X:guard n Ks & Y:guard n Ks)" by (auto, (ind_cases "{|X,Y|}:guard n Ks", auto)+) diff -r e1317a26f8c0 -r f2ffead641d4 src/HOL/Auth/Guard/GuardK.thy --- a/src/HOL/Auth/Guard/GuardK.thy Fri Apr 25 14:18:13 2014 +0200 +++ b/src/HOL/Auth/Guard/GuardK.thy Fri Apr 25 14:39:11 2014 +0200 @@ -63,7 +63,7 @@ by (erule guardK.induct, auto dest: kparts_parts parts_sub) lemma guardK_Crypt: "[| Crypt K Y:guardK n Ks; K ~:invKey`Ks |] ==> Y:guardK n Ks" -by (ind_cases "Crypt K Y:guardK n Ks", auto) + by (ind_cases "Crypt K Y:guardK n Ks") (auto intro!: image_eqI) lemma guardK_MPair [iff]: "({|X,Y|}:guardK n Ks) = (X:guardK n Ks & Y:guardK n Ks)" diff -r e1317a26f8c0 -r f2ffead641d4 src/HOL/Auth/Guard/Guard_Shared.thy --- a/src/HOL/Auth/Guard/Guard_Shared.thy Fri Apr 25 14:18:13 2014 +0200 +++ b/src/HOL/Auth/Guard/Guard_Shared.thy Fri Apr 25 14:39:11 2014 +0200 @@ -171,7 +171,7 @@ lemma GuardK_Key_analz: "[| GuardK n Ks (spies evs); evs:p; shrK_set Ks; good Ks; regular p; n ~:range shrK |] ==> Key n ~:analz (spies evs)" apply (clarify, simp only: knows_decomp) -apply (drule GuardK_invKey_keyset, clarify, simp+, simp add: initState.simps) +apply (drule GuardK_invKey_keyset, clarify, simp+, simp add: initState.simps image_eq_UN) apply clarify apply (drule in_good, simp) apply (drule in_shrK_set, simp+, clarify) diff -r e1317a26f8c0 -r f2ffead641d4 src/HOL/Auth/Guard/Proto.thy --- a/src/HOL/Auth/Guard/Proto.thy Fri Apr 25 14:18:13 2014 +0200 +++ b/src/HOL/Auth/Guard/Proto.thy Fri Apr 25 14:39:11 2014 +0200 @@ -56,7 +56,7 @@ Nonce n ~:parts (apm s `(msg `(fst R))) |] ==> (EX k. Nonce k:parts {X} & nonce s k = n)" apply (erule Nonce_apm, unfold wdef_def) -apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp) +apply (drule_tac x=R in spec, drule_tac x=k in spec, clarsimp simp: image_eq_UN) apply (drule_tac x=x in bspec, simp) apply (drule_tac Y="msg x" and s=s in apm_parts, simp) by (blast dest: parts_parts) @@ -134,7 +134,7 @@ lemma ok_not_used: "[| Nonce n ~:used evs; ok evs R s; ALL x. x:fst R --> is_Says x |] ==> Nonce n ~:parts (apm s `(msg `(fst R)))" -apply (unfold ok_def, clarsimp) +apply (unfold ok_def, clarsimp simp: image_eq_UN) apply (drule_tac x=x in spec, drule_tac x=x in spec) by (auto simp: is_Says_def dest: Says_imp_spies not_used_not_spied parts_parts) @@ -188,10 +188,10 @@ apply (drule wdef_Nonce, simp+) apply (frule ok_not_used, simp+) apply (clarify, erule ok_is_Says, simp+) -apply (clarify, rule_tac x=k in exI, simp add: newn_def) +apply (clarify, rule_tac x=k in exI, simp add: newn_def image_eq_UN) apply (clarify, drule_tac Y="msg x" and s=s in apm_parts) apply (drule ok_not_used, simp+) -by (clarify, erule ok_is_Says, simp+) +by (clarify, erule ok_is_Says, simp_all add: image_eq_UN) lemma fresh_rule: "[| evs' @ ev # evs:tr p; wdef p; Nonce n ~:used evs; Nonce n:parts {msg ev} |] ==> EX R s. R:p & ap' s R = ev" diff -r e1317a26f8c0 -r f2ffead641d4 src/HOL/Auth/NS_Public.thy --- a/src/HOL/Auth/NS_Public.thy Fri Apr 25 14:18:13 2014 +0200 +++ b/src/HOL/Auth/NS_Public.thy Fri Apr 25 14:39:11 2014 +0200 @@ -42,8 +42,7 @@ declare knows_Spy_partsEs [elim] declare knows_Spy_partsEs [elim] declare analz_into_parts [dest] -declare Fake_parts_insert_in_Un [dest] -declare image_eq_UN [simp] (*accelerates proofs involving nested images*) +declare Fake_parts_insert_in_Un [dest] (*A "possibility property": there are traces that reach the end*) lemma "\NB. \evs \ ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \ set evs" diff -r e1317a26f8c0 -r f2ffead641d4 src/HOL/Auth/NS_Public_Bad.thy --- a/src/HOL/Auth/NS_Public_Bad.thy Fri Apr 25 14:18:13 2014 +0200 +++ b/src/HOL/Auth/NS_Public_Bad.thy Fri Apr 25 14:39:11 2014 +0200 @@ -44,8 +44,7 @@ declare knows_Spy_partsEs [elim] declare analz_into_parts [dest] -declare Fake_parts_insert_in_Un [dest] -declare image_eq_UN [simp] (*accelerates proofs involving nested images*) +declare Fake_parts_insert_in_Un [dest] (*A "possibility property": there are traces that reach the end*) lemma "\NB. \evs \ ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \ set evs" diff -r e1317a26f8c0 -r f2ffead641d4 src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Fri Apr 25 14:18:13 2014 +0200 +++ b/src/HOL/Auth/NS_Shared.thy Fri Apr 25 14:39:11 2014 +0200 @@ -86,7 +86,6 @@ declare parts.Body [dest] declare Fake_parts_insert_in_Un [dest] declare analz_into_parts [dest] -declare image_eq_UN [simp] (*accelerates proofs involving nested images*) text{*A "possibility property": there are traces that reach the end*} diff -r e1317a26f8c0 -r f2ffead641d4 src/HOL/BNF_FP_Base.thy --- a/src/HOL/BNF_FP_Base.thy Fri Apr 25 14:18:13 2014 +0200 +++ b/src/HOL/BNF_FP_Base.thy Fri Apr 25 14:39:11 2014 +0200 @@ -166,10 +166,7 @@ lemma fun_cong_unused_0: "f = (\x. g) \ f (\x. 0) = g" by (erule arg_cong) -lemma snd_o_convol: "(snd \ (\x. (f x, g x))) = g" - by (rule ext) simp - -lemma inj_on_convol_id: "inj_on (\x. (x, f x)) X" +lemma inj_on_convol_ident: "inj_on (\x. (x, f x)) X" unfolding inj_on_def by simp lemma case_prod_app: "case_prod f x y = case_prod (\l r. f l r y) x" diff -r e1317a26f8c0 -r f2ffead641d4 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Fri Apr 25 14:18:13 2014 +0200 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Fri Apr 25 14:39:11 2014 +0200 @@ -174,16 +174,16 @@ subsection {* Alternative rules for @{text length} *} -definition size_list :: "'a list => nat" -where "size_list = size" +definition size_list' :: "'a list => nat" +where "size_list' = size" -lemma size_list_simps: - "size_list [] = 0" - "size_list (x # xs) = Suc (size_list xs)" -by (auto simp add: size_list_def) +lemma size_list'_simps: + "size_list' [] = 0" + "size_list' (x # xs) = Suc (size_list' xs)" +by (auto simp add: size_list'_def) -declare size_list_simps[code_pred_def] -declare size_list_def[symmetric, code_pred_inline] +declare size_list'_simps[code_pred_def] +declare size_list'_def[symmetric, code_pred_inline] subsection {* Alternative rules for @{text list_all2} *} diff -r e1317a26f8c0 -r f2ffead641d4 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Fri Apr 25 14:18:13 2014 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Fri Apr 25 14:39:11 2014 +0200 @@ -1077,12 +1077,12 @@ *) subsection {* Inverting list functions *} -code_pred [inductify, skip_proof] size_list . -code_pred [new_random_dseq inductify] size_list . -thm size_listP.equation -thm size_listP.new_random_dseq_equation +code_pred [inductify, skip_proof] size_list' . +code_pred [new_random_dseq inductify] size_list' . +thm size_list'P.equation +thm size_list'P.new_random_dseq_equation -values [new_random_dseq 2,3,10] 3 "{xs. size_listP (xs::nat list) (5::nat)}" +values [new_random_dseq 2,3,10] 3 "{xs. size_list'P (xs::nat list) (5::nat)}" code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat . thm concatP.equation diff -r e1317a26f8c0 -r f2ffead641d4 src/HOL/ROOT --- a/src/HOL/ROOT Fri Apr 25 14:18:13 2014 +0200 +++ b/src/HOL/ROOT Fri Apr 25 14:39:11 2014 +0200 @@ -560,7 +560,6 @@ HarmonicSeries Refute_Examples Execute_Choice - Summation Gauge_Integration Dedekind_Real Quicksort diff -r e1317a26f8c0 -r f2ffead641d4 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Fri Apr 25 14:18:13 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Fri Apr 25 14:39:11 2014 +0200 @@ -50,7 +50,8 @@ Class_Decl of string * 'a * 'a list | Type_Decl of string * 'a * int | Sym_Decl of string * 'a * 'a atp_type | - Datatype_Decl of string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list | + Datatype_Decl of + string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list * bool | Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a | Formula of (string * string) * atp_formula_role * ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula @@ -194,7 +195,8 @@ Class_Decl of string * 'a * 'a list | Type_Decl of string * 'a * int | Sym_Decl of string * 'a * 'a atp_type | - Datatype_Decl of string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list | + Datatype_Decl of + string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list * bool | Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a | Formula of (string * string) * atp_formula_role * ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula @@ -613,7 +615,9 @@ (if null xs then "" else "[" ^ commas (map bound_tvar xs) ^ "], ") ^ typ ty fun sort_decl xs ty cl = "sort(" ^ binder_typ xs ty ^ ", " ^ cl ^ ")." - fun datatype_decl xs ty tms = "datatype(" ^ commas (binder_typ xs ty :: map term tms) ^ ")." + fun datatype_decl xs ty tms exhaust = + "datatype(" ^ commas (binder_typ xs ty :: map term tms @ (if exhaust then [] else ["..."])) ^ + ")." fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")." fun formula pred (Formula ((ident, alt), kind, phi, _, info)) = if pred kind then @@ -661,7 +665,8 @@ else NONE | _ => NONE) |> flat val datatype_decls = - filt (try (fn Datatype_Decl (_, xs, ty, tms) => datatype_decl xs ty tms)) |> flat + filt (try (fn Datatype_Decl (_, xs, ty, tms, exhaust) => datatype_decl xs ty tms exhaust)) + |> flat val sort_decls = filt (try (fn Class_Memb (_, xs, ty, cl) => sort_decl xs ty cl)) |> flat val subclass_decls = @@ -938,9 +943,9 @@ nice_name ty #>> (fn ty => Type_Decl (ident, ty, ary)) | nice_line (Sym_Decl (ident, sym, ty)) = nice_name sym ##>> nice_type ty #>> (fn (sym, ty) => Sym_Decl (ident, sym, ty)) - | nice_line (Datatype_Decl (ident, xs, ty, tms)) = + | nice_line (Datatype_Decl (ident, xs, ty, tms, exhaust)) = nice_bound_tvars xs ##>> nice_type ty ##>> fold_map nice_term tms - #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms)) + #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms, exhaust)) | nice_line (Class_Memb (ident, xs, ty, cl)) = nice_bound_tvars xs ##>> nice_type ty ##>> nice_name cl #>> (fn ((xs, ty), cl) => Class_Memb (ident, xs, ty, cl)) diff -r e1317a26f8c0 -r f2ffead641d4 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Apr 25 14:18:13 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Apr 25 14:39:11 2014 +0200 @@ -2462,21 +2462,19 @@ fun datatype_of_ctrs (ctrs as (_, T1) :: _) = let val ctrs' = map do_ctr ctrs in - if forall is_some ctrs' then - SOME (native_atp_type_of_typ type_enc false 0 (body_type T1), map_filter I ctrs') - else - NONE + (native_atp_type_of_typ type_enc false 0 (body_type T1), map_filter I ctrs', + forall is_some ctrs') end in - map_filter datatype_of_ctrs ctrss + ctrss |> map datatype_of_ctrs |> filter_out (null o #2) end else [] | datatypes_of_sym_table _ _ _ _ _ _ = [] -fun decl_line_of_datatype (ty as AType (((_, s'), _), ty_args), ctrs) = +fun decl_line_of_datatype (ty as AType (((_, s'), _), ty_args), ctrs, exhaust) = let val xs = map (fn AType ((name, _), []) => name) ty_args in - Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty, ctrs) + Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty, ctrs, exhaust) end fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2) @@ -2589,7 +2587,7 @@ fun do_line (Class_Decl (_, _, cls)) = fold do_class cls | do_line (Type_Decl _) = I | do_line (Sym_Decl (_, _, ty)) = do_type ty - | do_line (Datatype_Decl (_, xs, ty, tms)) = + | do_line (Datatype_Decl (_, xs, ty, tms, _)) = fold do_bound_tvars xs #> do_type ty #> fold (do_term false) tms | do_line (Class_Memb (_, xs, ty, cl)) = fold do_bound_tvars xs #> do_type ty #> do_class cl | do_line (Formula (_, _, phi, _, _)) = do_formula phi diff -r e1317a26f8c0 -r f2ffead641d4 src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Apr 25 14:18:13 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Apr 25 14:39:11 2014 +0200 @@ -217,18 +217,23 @@ val overloaded_size_defs' = map (mk_unabs_def 1 o (fn thm => thm RS meta_eq_to_obj_eq)) overloaded_size_defs; + val all_overloaded_size_defs = overloaded_size_defs @ + (Spec_Rules.retrieve lthy0 @{const size ('a)} + |> map_filter (try (fn (Equational, (_, [thm])) => thm))); + val nested_size_maps = map (pointfill lthy2) nested_size_o_maps @ nested_size_o_maps; val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ nested_bnfs @ nesting_bnfs); fun derive_size_simp size_def' simp0 = (trans OF [size_def', simp0]) - |> Simplifier.asm_full_simplify (ss_only (@{thms inj_on_convol_id snd_o_convol} @ + |> Simplifier.asm_full_simplify (ss_only (@{thms inj_on_convol_ident id_def o_def snd_conv} @ all_inj_maps @ nested_size_maps) lthy2) |> fold_thms lthy2 size_defs_unused_0; - fun derive_overloaded_size_simp size_def' simp0 = - (trans OF [size_def', simp0]) + + fun derive_overloaded_size_simp overloaded_size_def' simp0 = + (trans OF [overloaded_size_def', simp0]) |> unfold_thms lthy2 @{thms add_0_left add_0_right} - |> fold_thms lthy2 overloaded_size_defs'; + |> fold_thms lthy2 all_overloaded_size_defs; val size_simpss = map2 (map o derive_size_simp) size_defs' rec_thmss; val size_simps = flat size_simpss; diff -r e1317a26f8c0 -r f2ffead641d4 src/HOL/ex/Summation.thy --- a/src/HOL/ex/Summation.thy Fri Apr 25 14:18:13 2014 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,107 +0,0 @@ -(* Author: Florian Haftmann, TU Muenchen *) - -header {* Some basic facts about discrete summation *} - -theory Summation -imports Main -begin - -text {* Auxiliary. *} - -lemma add_setsum_orient: - "setsum f {k.. k < l \ setsum f {j.. :: "(int \ 'a\ab_group_add) \ int \ 'a" where - "\ f k = f (k + 1) - f k" - -lemma \_shift: - "\ (\k. l + f k) = \ f" - by (simp add: \_def fun_eq_iff) - -lemma \_same_shift: - assumes "\ f = \ g" - shows "\l. plus l \ f = g" -proof - - fix k - from assms have "\k. \ f k = \ g k" by simp - then have k_incr: "\k. f (k + 1) - g (k + 1) = f k - g k" - by (simp add: \_def algebra_simps) - then have "\k. f ((k - 1) + 1) - g ((k - 1) + 1) = f (k - 1) - g (k - 1)" - by blast - then have k_decr: "\k. f (k - 1) - g (k - 1) = f k - g k" - by simp - have "\k. f k - g k = f 0 - g 0" - proof - - fix k - show "f k - g k = f 0 - g 0" - by (induct k rule: int_induct) (simp_all add: k_incr k_decr) - qed - then have "\k. (plus (g 0 - f 0) \ f) k = g k" - by (simp add: algebra_simps) - then have "plus (g 0 - f 0) \ f = g" .. - then show ?thesis .. -qed - -text {* The formal sum operator. *} - -definition \ :: "(int \ 'a\ab_group_add) \ int \ int \ 'a" where - "\ f j l = (if j < l then setsum f {j.. l then - setsum f {l.._same [simp]: - "\ f j j = 0" - by (simp add: \_def) - -lemma \_positive: - "j < l \ \ f j l = setsum f {j.._def) - -lemma \_negative: - "j > l \ \ f j l = - \ f l j" - by (simp add: \_def) - -lemma add_\: - "\ f j k + \ f k l = \ f j l" - by (simp add: \_def algebra_simps add_setsum_int) - (simp_all add: add_setsum_orient [of f k j l] - add_setsum_orient [of f j l k] - add_setsum_orient [of f j k l] add_setsum_int) - -lemma \_incr_upper: - "\ f j (l + 1) = \ f j l + f l" -proof - - have "{l.. f l (l + 1) = f l" by (simp add: \_def) - moreover have "\ f j (l + 1) = \ f j l + \ f l (l + 1)" by (simp add: add_\) - ultimately show ?thesis by simp -qed - -text {* Fundamental lemmas: The relation between @{term \} and @{term \}. *} - -lemma \_\: - "\ (\ f j) = f" -proof - fix k - show "\ (\ f j) k = f k" - by (simp add: \_def \_incr_upper) -qed - -lemma \_\: - "\ (\ f) j l = f l - f j" -proof - - from \_\ have "\ (\ (\ f) j) = \ f" . - then obtain k where "plus k \ \ (\ f) j = f" by (blast dest: \_same_shift) - then have "\q. f q = k + \ (\ f) j q" by (simp add: fun_eq_iff) - then show ?thesis by simp -qed - -end