--- 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 \<kappa>} is
mangled as @{text f_\<kappa>}. In case of uncertainty, these names may be
--- 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)
--- 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)+)
--- 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)"
--- 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)
--- 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"
--- 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 "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
--- 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 "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
--- 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*}
--- 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 = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
by (erule arg_cong)
-lemma snd_o_convol: "(snd \<circ> (\<lambda>x. (f x, g x))) = g"
- by (rule ext) simp
-
-lemma inj_on_convol_id: "inj_on (\<lambda>x. (x, f x)) X"
+lemma inj_on_convol_ident: "inj_on (\<lambda>x. (x, f x)) X"
unfolding inj_on_def by simp
lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"
--- 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} *}
--- 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
--- 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
--- 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))
--- 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
--- 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;
--- 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..<j} + setsum f {l..<k} = setsum f {l..<k} + setsum f {k..<j}"
- by (fact add.commute)
-
-lemma add_setsum_int:
- fixes j k l :: int
- shows "j < k \<Longrightarrow> k < l \<Longrightarrow> setsum f {j..<k} + setsum f {k..<l} = setsum f {j..<l}"
- by (simp_all add: setsum_Un_Int [symmetric] ivl_disj_un)
-
-text {* The shift operator. *}
-
-definition \<Delta> :: "(int \<Rightarrow> 'a\<Colon>ab_group_add) \<Rightarrow> int \<Rightarrow> 'a" where
- "\<Delta> f k = f (k + 1) - f k"
-
-lemma \<Delta>_shift:
- "\<Delta> (\<lambda>k. l + f k) = \<Delta> f"
- by (simp add: \<Delta>_def fun_eq_iff)
-
-lemma \<Delta>_same_shift:
- assumes "\<Delta> f = \<Delta> g"
- shows "\<exists>l. plus l \<circ> f = g"
-proof -
- fix k
- from assms have "\<And>k. \<Delta> f k = \<Delta> g k" by simp
- then have k_incr: "\<And>k. f (k + 1) - g (k + 1) = f k - g k"
- by (simp add: \<Delta>_def algebra_simps)
- then have "\<And>k. f ((k - 1) + 1) - g ((k - 1) + 1) = f (k - 1) - g (k - 1)"
- by blast
- then have k_decr: "\<And>k. f (k - 1) - g (k - 1) = f k - g k"
- by simp
- have "\<And>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 "\<And>k. (plus (g 0 - f 0) \<circ> f) k = g k"
- by (simp add: algebra_simps)
- then have "plus (g 0 - f 0) \<circ> f = g" ..
- then show ?thesis ..
-qed
-
-text {* The formal sum operator. *}
-
-definition \<Sigma> :: "(int \<Rightarrow> 'a\<Colon>ab_group_add) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a" where
- "\<Sigma> f j l = (if j < l then setsum f {j..<l}
- else if j > l then - setsum f {l..<j}
- else 0)"
-
-lemma \<Sigma>_same [simp]:
- "\<Sigma> f j j = 0"
- by (simp add: \<Sigma>_def)
-
-lemma \<Sigma>_positive:
- "j < l \<Longrightarrow> \<Sigma> f j l = setsum f {j..<l}"
- by (simp add: \<Sigma>_def)
-
-lemma \<Sigma>_negative:
- "j > l \<Longrightarrow> \<Sigma> f j l = - \<Sigma> f l j"
- by (simp add: \<Sigma>_def)
-
-lemma add_\<Sigma>:
- "\<Sigma> f j k + \<Sigma> f k l = \<Sigma> f j l"
- by (simp add: \<Sigma>_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 \<Sigma>_incr_upper:
- "\<Sigma> f j (l + 1) = \<Sigma> f j l + f l"
-proof -
- have "{l..<l+1} = {l}" by auto
- then have "\<Sigma> f l (l + 1) = f l" by (simp add: \<Sigma>_def)
- moreover have "\<Sigma> f j (l + 1) = \<Sigma> f j l + \<Sigma> f l (l + 1)" by (simp add: add_\<Sigma>)
- ultimately show ?thesis by simp
-qed
-
-text {* Fundamental lemmas: The relation between @{term \<Delta>} and @{term \<Sigma>}. *}
-
-lemma \<Delta>_\<Sigma>:
- "\<Delta> (\<Sigma> f j) = f"
-proof
- fix k
- show "\<Delta> (\<Sigma> f j) k = f k"
- by (simp add: \<Delta>_def \<Sigma>_incr_upper)
-qed
-
-lemma \<Sigma>_\<Delta>:
- "\<Sigma> (\<Delta> f) j l = f l - f j"
-proof -
- from \<Delta>_\<Sigma> have "\<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f" .
- then obtain k where "plus k \<circ> \<Sigma> (\<Delta> f) j = f" by (blast dest: \<Delta>_same_shift)
- then have "\<And>q. f q = k + \<Sigma> (\<Delta> f) j q" by (simp add: fun_eq_iff)
- then show ?thesis by simp
-qed
-
-end