--- a/src/HOL/Auth/KerberosIV.thy Fri Aug 21 13:23:53 2009 +0200
+++ b/src/HOL/Auth/KerberosIV.thy Fri Aug 21 13:25:05 2009 +0200
@@ -379,6 +379,7 @@
lemma Spy_see_shrK_D [dest!]:
"\<lbrakk> Key (shrK A) \<in> parts (spies evs); evs \<in> kerbIV \<rbrakk> \<Longrightarrow> A:bad"
by (blast dest: Spy_see_shrK)
+
lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!]
text{*Nobody can have used non-existent keys!*}
@@ -479,21 +480,7 @@
txt{*K2*}
apply (simp (no_asm) add: takeWhile_tail)
apply (rule conjI)
-apply clarify
-apply (rule conjI)
-apply clarify
-apply (rule conjI)
-apply blast
-apply (rule conjI)
-apply clarify
-apply (rule conjI)
-txt{*subcase: used before*}
-apply (blast dest: used_evs_rev [THEN equalityD2, THEN contra_subsetD]
- used_takeWhile_used)
-txt{*subcase: CT before*}
-apply (fastsimp dest!: set_evs_rev [THEN equalityD2, THEN contra_subsetD, THEN takeWhile_void])
-apply blast
-txt{*rest*}
+apply (metis Key_not_used authKeys_used length_rev set_rev takeWhile_void used_evs_rev)
apply blast+
done
@@ -570,10 +557,9 @@
apply (blast dest: authTicket_crypt_authK)
apply (blast dest!: authKeys_used Says_Kas_message_form)
txt{*subcase: used before*}
-apply (blast dest: used_evs_rev [THEN equalityD2, THEN contra_subsetD]
- used_takeWhile_used)
+apply (metis used_evs_rev used_takeWhile_used)
txt{*subcase: CT before*}
-apply (fastsimp dest!: set_evs_rev [THEN equalityD2, THEN contra_subsetD, THEN takeWhile_void])
+apply (metis length_rev set_evs_rev takeWhile_void)
done
lemma authTicket_form:
@@ -794,8 +780,7 @@
lemma u_NotexpiredSK_NotexpiredAK:
"\<lbrakk> \<not> expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \<rbrakk>
\<Longrightarrow> \<not> expiredAK Ta evs"
-apply (blast dest: leI le_trans dest: leD)
-done
+ by (metis nat_add_commute le_less_trans)
subsection{* Reliability: friendly agents send something if something else happened*}
@@ -854,16 +839,8 @@
txt{*K3*}
apply (blast dest: Key_unique_SesKey)
txt{*K5*}
-txt{*If authKa were compromised, so would be authK*}
-apply (case_tac "Key authKa \<in> analz (spies evs5)")
-apply (force dest!: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
-txt{*Besides, since authKa originated with Kas anyway...*}
-apply (clarify, drule K3_imp_K2, assumption, assumption)
-apply (clarify, drule Says_Kas_message_form, assumption)
-txt{*...it cannot be a shared key*. Therefore @{text servK_authentic} applies.
- Contradition: Tgs used authK as a servkey,
- while Kas used it as an authkey*}
-apply (blast dest: servK_authentic Says_Tgs_message_form)
+apply (metis K3_imp_K2 Key_unique_SesKey Spy_see_shrK parts.Body parts.Fst
+ Says_imp_knows_Spy [THEN parts.Inj])
done
lemma Says_K5:
@@ -922,9 +899,12 @@
apply (frule_tac [7] Says_ticket_parts)
apply (simp_all (no_asm_simp))
apply blast
-apply (force dest!: Crypt_imp_keysFor, clarify)
-apply (frule Says_Tgs_message_form, assumption, clarify) (*PROOF FAILED if omitted*)
-apply (blast dest: unique_CryptKey)
+atp_minimize [atp=spass] Crypt_imp_invKey_keysFor invKey_K new_keys_not_used
+apply (metis Crypt_imp_invKey_keysFor invKey_K new_keys_not_used)
+apply (clarify)
+apply (frule Says_Tgs_message_form, assumption)
+apply (metis K3_msg_in_parts_spies parts.Fst Says_imp_knows_Spy [THEN parts.Inj]
+ unique_CryptKey)
done
text{*Needs a unicity theorem, hence moved here*}
@@ -1099,13 +1079,8 @@
apply (erule kerbIV.induct, analz_mono_contra)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
-txt{*K4 splits into distinct subcases*}
-apply auto
-txt{*servK can't have been enclosed in two certificates*}
- prefer 2 apply (blast dest: unique_CryptKey)
-txt{*servK is fresh and so could not have been used, by
- @{text new_keys_not_used}*}
-apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def)
+txt{*K4*}
+apply (metis Auth_fresh_not_AKcryptSK Crypt_imp_keysFor new_keys_not_used parts.Fst parts.Snd Says_imp_knows_Spy [THEN parts.Inj] unique_CryptKey)
done
text{*Long term keys are not issued as servKeys*}
@@ -1143,16 +1118,9 @@
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, safe)
-txt{*K4 splits into subcases*}
-apply simp_all
-prefer 4 apply (blast dest!: authK_not_AKcryptSK)
-txt{*servK is fresh and so could not have been used, by
- @{text new_keys_not_used}*}
- prefer 2
- apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def)
-txt{*Others by freshness*}
-apply (blast+)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
+apply (metis Auth_fresh_not_AKcryptSK Says_imp_spies authK_not_AKcryptSK
+ authKeys_used authTicket_crypt_authK parts.Fst parts.Inj)
done
text{*The only session keys that can be found with the help of session keys are
@@ -1304,7 +1272,7 @@
\<in> set evs; authK \<in> symKeys;
Key authK \<in> analz (spies evs); evs \<in> kerbIV \<rbrakk>
\<Longrightarrow> Key servK \<in> analz (spies evs)"
-by (force dest: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
+ by (metis Says_imp_analz_Spy analz.Fst analz_Decrypt')
lemma servK_notin_authKeysD:
"\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts,
@@ -1348,6 +1316,7 @@
txt{*K4*}
apply blast
txt{*Level 8: K5*}
+atp_minimize [atp=e] Tgs_not_bad authKeysI less_SucI mem_def nat_add_commute servK_notin_authKeysD spies_partsEs(1)
apply (blast dest: servK_notin_authKeysD Says_Kas_message_form intro: less_SucI)
txt{*Oops1*}
apply (blast dest!: unique_authKeys intro: less_SucI)
@@ -1395,24 +1364,17 @@
apply (safe del: impI conjI impCE)
apply (simp_all add: less_SucI new_keys_not_analzd Says_Kas_message_form Says_Tgs_message_form analz_insert_eq not_parts_not_analz analz_insert_freshK1 analz_insert_freshK2 analz_insert_freshK3_bis pushes)
txt{*Fake*}
-apply spy_analz
+ apply spy_analz
txt{*K2*}
-apply (blast intro: parts_insertI less_SucI)
+ apply (blast intro: parts_insertI less_SucI)
txt{*K4*}
-apply (blast dest: authTicket_authentic Confidentiality_Kas)
-txt{*Oops2*}
- prefer 3
- apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI)
+ apply (blast dest: authTicket_authentic Confidentiality_Kas)
+txt{*K5*}
+ apply (metis Says_imp_spies Says_ticket_parts Tgs_not_bad analz_insert_freshK2
+ less_SucI parts.Inj servK_notin_authKeysD unique_CryptKey)
txt{*Oops1*}
- prefer 2
-apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI)
-txt{*K5. Not obvious how this step could be integrated with the main
- simplification step. Done in KerberosV.thy *}
-apply clarify
-apply (erule_tac V = "Says Aa Tgs ?X \<in> set ?evs" in thin_rl)
-apply (frule Says_imp_spies [THEN parts.Inj, THEN servK_notin_authKeysD])
-apply (assumption, blast, assumption)
-apply (simp add: analz_insert_freshK2)
+ apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI)
+txt{*Oops2*}
apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI)
done
@@ -1669,9 +1631,7 @@
lemma honest_never_says_current_timestamp_in_auth:
"\<lbrakk> (CT evs) = T; Number T \<in> parts {X}; evs \<in> kerbIV \<rbrakk>
\<Longrightarrow> \<forall> A B Y. A \<notin> bad \<longrightarrow> Says A B \<lbrace>Y, X\<rbrace> \<notin> set evs"
-apply (frule eq_imp_le)
-apply (blast dest: honest_never_says_newer_timestamp_in_auth)
-done
+ by (metis eq_imp_le honest_never_says_newer_timestamp_in_auth)
lemma A_trusts_secure_authenticator:
"\<lbrakk> Crypt K \<lbrace>Agent A, Number T\<rbrace> \<in> parts (spies evs);
--- a/src/HOL/Auth/OtwayRees_AN.thy Fri Aug 21 13:23:53 2009 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy Fri Aug 21 13:25:05 2009 +0200
@@ -246,7 +246,7 @@
Notes Spy {|NA, NB, Key K|} \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> otway |]
==> Key K \<notin> analz (knows Spy evs)"
-by (blast dest: Says_Server_message_form secrecy_lemma)
+ by (metis secrecy_lemma)
text{*A's guarantee. The Oops premise quantifies over NB because A cannot know
@@ -256,7 +256,7 @@
\<forall>NB. Notes Spy {|NA, NB, Key K|} \<notin> set evs;
A \<notin> bad; B \<notin> bad; A \<noteq> B; evs \<in> otway |]
==> Key K \<notin> analz (knows Spy evs)"
-by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key)
+ by (metis A_trusts_OR4 secrecy_lemma)
--- a/src/HOL/Auth/Yahalom.thy Fri Aug 21 13:23:53 2009 +0200
+++ b/src/HOL/Auth/Yahalom.thy Fri Aug 21 13:25:05 2009 +0200
@@ -129,8 +129,7 @@
lemma YM4_Key_parts_knows_Spy:
"Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \<in> set evs
==> K \<in> parts (knows Spy evs)"
-by (blast dest!: parts.Body Says_imp_knows_Spy [THEN parts.Inj])
-
+ by (metis parts.Body parts.Fst parts.Snd Says_imp_knows_Spy parts.Inj)
text{*Theorems of the form @{term "X \<notin> parts (knows Spy evs)"} imply
that NOBODY sends messages containing X! *}
@@ -275,7 +274,7 @@
Notes Spy {|na, nb, Key K|} \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> analz (knows Spy evs)"
-by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
+ by (metis A_trusts_YM3 secrecy_lemma)
subsubsection{* Security Guarantees for B upon receiving YM4 *}
@@ -409,9 +408,8 @@
txt{*If @{prop "A \<in> bad"} then @{term NBa} is known, therefore
@{prop "NBa \<noteq> NB"}. Previous two steps make the next step
faster.*}
-apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad
- dest: analz.Inj
- parts.Inj [THEN parts.Fst, THEN A_trusts_YM3, THEN KeyWithNonceI])
+apply (metis A_trusts_YM3 Gets_imp_analz_Spy Gets_imp_knows_Spy KeyWithNonce_def
+ Spy_analz_shrK analz.Fst analz.Snd analz_shrK_Decrypt parts.Fst parts.Inj)
done
@@ -514,12 +512,7 @@
covered by the quantified Oops assumption.*}
apply (clarify, simp add: all_conj_distrib)
apply (frule Says_Server_imp_YM2, assumption)
-apply (case_tac "NB = NBa")
-txt{*If NB=NBa then all other components of the Oops message agree*}
-apply (blast dest: Says_unique_NB)
-txt{*case @{prop "NB \<noteq> NBa"}*}
-apply (simp add: single_Nonce_secrecy)
-apply (blast dest!: no_nonce_YM1_YM2 (*to prove NB\<noteq>NAa*))
+apply (metis Gets_imp_Says Says_Server_not_range Says_unique_NB no_nonce_YM1_YM2 parts.Snd single_Nonce_secrecy spies_partsEs(1))
done
@@ -557,7 +550,7 @@
\<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> analz (knows Spy evs)"
-by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
+ by (metis B_trusts_YM4 Spy_not_see_encrypted_key)
subsection{*Authenticating B to A*}
@@ -594,7 +587,8 @@
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
\<in> set evs"
-by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma elim: knows_Spy_partsEs)
+ by (metis A_trusts_YM3 Gets_imp_analz_Spy YM3_auth_B_to_A_lemma analz.Fst
+ not_parts_not_analz)
subsection{*Authenticating A to B using the certificate
@@ -639,7 +633,5 @@
(\<forall>NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
-by (blast intro!: A_Said_YM3_lemma
- dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says)
-
+by (metis A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz)
end
--- a/src/HOL/Bali/Basis.thy Fri Aug 21 13:23:53 2009 +0200
+++ b/src/HOL/Bali/Basis.thy Fri Aug 21 13:25:05 2009 +0200
@@ -7,8 +7,6 @@
theory Basis imports Main begin
-declare [[unify_search_bound = 40, unify_trace_bound = 40]]
-
section "misc"
--- a/src/HOL/Code_Eval.thy Fri Aug 21 13:23:53 2009 +0200
+++ b/src/HOL/Code_Eval.thy Fri Aug 21 13:25:05 2009 +0200
@@ -134,7 +134,7 @@
lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c =
(let (n, m) = nibble_pair_of_char c
- in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
+ in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
(Code_Eval.term_of n)) (Code_Eval.term_of m))"
by (subst term_of_anything) rule
--- a/src/HOL/Induct/Com.thy Fri Aug 21 13:23:53 2009 +0200
+++ b/src/HOL/Induct/Com.thy Fri Aug 21 13:25:05 2009 +0200
@@ -91,8 +91,6 @@
"((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
by (auto simp add: le_fun_def le_bool_def mem_def)
-declare [[unify_trace_bound = 30, unify_search_bound = 60]]
-
text{*Command execution is functional (deterministic) provided evaluation is*}
theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
apply (simp add: single_valued_def)
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Fri Aug 21 13:23:53 2009 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Fri Aug 21 13:25:05 2009 +0200
@@ -183,8 +183,6 @@
(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
*}
-declare [[unify_search_bound = 40, unify_trace_bound = 40]]
-
theorem eval_evals_exec_type_sound:
"wf_java_prog G ==>
@@ -368,8 +366,6 @@
done
-declare [[unify_search_bound = 20, unify_trace_bound = 20]]
-
lemma eval_type_sound: "!!E s s'.
[| wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T; G=prg E |]
--- a/src/HOL/Predicate.thy Fri Aug 21 13:23:53 2009 +0200
+++ b/src/HOL/Predicate.thy Fri Aug 21 13:25:05 2009 +0200
@@ -646,7 +646,7 @@
@{code_datatype pred = Seq};
@{code_datatype seq = Empty | Insert | Join};
-fun yield (Seq f) = next (f ())
+fun yield (@{code Seq} f) = next (f ())
and next @{code Empty} = NONE
| next (@{code Insert} (x, P)) = SOME (x, P)
| next (@{code Join} (P, xq)) = (case yield P
--- a/src/HOL/Quickcheck.thy Fri Aug 21 13:23:53 2009 +0200
+++ b/src/HOL/Quickcheck.thy Fri Aug 21 13:25:05 2009 +0200
@@ -54,7 +54,7 @@
begin
definition
- "random _ = Pair (STR [], \<lambda>u. Code_Eval.term_of (STR []))"
+ "random _ = Pair (STR '''', \<lambda>u. Code_Eval.term_of (STR ''''))"
instance ..
--- a/src/HOL/Tools/Datatype/datatype.ML Fri Aug 21 13:23:53 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Fri Aug 21 13:25:05 2009 +0200
@@ -119,7 +119,7 @@
val tycos = map fst dataTs;
val _ = if gen_eq_set (op =) (tycos, raw_tycos) then ()
else error ("Type constructors " ^ commas (map quote raw_tycos)
- ^ "do not belong exhaustively to one mutual recursive datatype");
+ ^ " do not belong exhaustively to one mutual recursive datatype");
val (Ts, Us) = (pairself o map) Type protoTs;
--- a/src/HOL/Tools/lin_arith.ML Fri Aug 21 13:23:53 2009 +0200
+++ b/src/HOL/Tools/lin_arith.ML Fri Aug 21 13:25:05 2009 +0200
@@ -67,7 +67,7 @@
and ct = cterm_of thy t
in instantiate ([], [(cn, ct)]) @{thm le0} end;
-end;
+end; (* LA_Logic *)
(* arith context data *)
@@ -279,7 +279,7 @@
(*---------------------------------------------------------------------------*)
-(* the following code performs splitting of certain constants (e.g. min, *)
+(* the following code performs splitting of certain constants (e.g., min, *)
(* max) in a linear arithmetic problem; similar to what split_tac later does *)
(* to the proof state *)
(*---------------------------------------------------------------------------*)
@@ -342,23 +342,30 @@
(* takes a list [t1, ..., tn] to the term *)
(* tn' --> ... --> t1' --> False , *)
(* where ti' = HOLogic.dest_Trueprop ti *)
- fun REPEAT_DETERM_etac_rev_mp terms' =
- fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop terms') HOLogic.false_const
- val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
- val cmap = Splitter.cmap_of_split_thms split_thms
- val splits = Splitter.split_posns cmap thy Ts (REPEAT_DETERM_etac_rev_mp terms)
+ fun REPEAT_DETERM_etac_rev_mp tms =
+ fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop tms)
+ HOLogic.false_const
+ val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
+ val cmap = Splitter.cmap_of_split_thms split_thms
+ val goal_tm = REPEAT_DETERM_etac_rev_mp terms
+ val splits = Splitter.split_posns cmap thy Ts goal_tm
val split_limit = Config.get ctxt split_limit
in
- if length splits > split_limit then
- (tracing ("linarith_split_limit exceeded (current value is " ^
- string_of_int split_limit ^ ")"); NONE)
- else (
- case splits of [] =>
+ if length splits > split_limit then (
+ tracing ("linarith_split_limit exceeded (current value is " ^
+ string_of_int split_limit ^ ")");
+ NONE
+ ) else case splits of
+ [] =>
(* split_tac would fail: no possible split *)
NONE
- | ((_, _, _, split_type, split_term) :: _) => (
- (* ignore all but the first possible split *)
- case strip_comb split_term of
+ | (_, _::_, _, _, _) :: _ =>
+ (* disallow a split that involves non-locally bound variables (except *)
+ (* when bound by outermost meta-quantifiers) *)
+ NONE
+ | (_, [], _, split_type, split_term) :: _ =>
+ (* ignore all but the first possible split *)
+ (case strip_comb split_term of
(* ?P (max ?i ?j) = ((?i <= ?j --> ?P ?j) & (~ ?i <= ?j --> ?P ?i)) *)
(Const (@{const_name Orderings.max}, _), [t1, t2]) =>
let
@@ -627,12 +634,11 @@
(* out *)
| (t, ts) => (
warning ("Lin. Arith.: split rule for " ^ Syntax.string_of_term ctxt t ^
- " (with " ^ string_of_int (length ts) ^
- " argument(s)) not implemented; proof reconstruction is likely to fail");
+ " (with " ^ string_of_int (length ts) ^
+ " argument(s)) not implemented; proof reconstruction is likely to fail");
NONE
))
- )
-end;
+end; (* split_once_items *)
(* remove terms that do not satisfy 'p'; change the order of the remaining *)
(* terms in the same way as filter_prems_tac does *)
@@ -651,29 +657,32 @@
fun negated_term_occurs_positively (terms : term list) : bool =
List.exists
- (fn (Trueprop $ (Const ("Not", _) $ t)) => member Pattern.aeconv terms (Trueprop $ t)
- | _ => false)
+ (fn (Trueprop $ (Const ("Not", _) $ t)) =>
+ member Pattern.aeconv terms (Trueprop $ t)
+ | _ => false)
terms;
fun pre_decomp ctxt (Ts : typ list, terms : term list) : (typ list * term list) list =
let
(* repeatedly split (including newly emerging subgoals) until no further *)
(* splitting is possible *)
- fun split_loop ([] : (typ list * term list) list) = ([] : (typ list * term list) list)
- | split_loop (subgoal::subgoals) = (
- case split_once_items ctxt subgoal of
- SOME new_subgoals => split_loop (new_subgoals @ subgoals)
- | NONE => subgoal :: split_loop subgoals
- )
+ fun split_loop ([] : (typ list * term list) list) =
+ ([] : (typ list * term list) list)
+ | split_loop (subgoal::subgoals) =
+ (case split_once_items ctxt subgoal of
+ SOME new_subgoals => split_loop (new_subgoals @ subgoals)
+ | NONE => subgoal :: split_loop subgoals)
fun is_relevant t = isSome (decomp ctxt t)
(* filter_prems_tac is_relevant: *)
val relevant_terms = filter_prems_tac_items is_relevant terms
(* split_tac, NNF normalization: *)
val split_goals = split_loop [(Ts, relevant_terms)]
(* necessary because split_once_tac may normalize terms: *)
- val beta_eta_norm = map (apsnd (map (Envir.eta_contract o Envir.beta_norm))) split_goals
+ val beta_eta_norm = map (apsnd (map (Envir.eta_contract o Envir.beta_norm)))
+ split_goals
(* TRY (etac notE) THEN eq_assume_tac: *)
- val result = List.filter (not o negated_term_occurs_positively o snd) beta_eta_norm
+ val result = List.filter (not o negated_term_occurs_positively o snd)
+ beta_eta_norm
in
result
end;
@@ -694,7 +703,8 @@
addsimps [imp_conv_disj, iff_conv_conj_imp, de_Morgan_disj, de_Morgan_conj,
not_all, not_ex, not_not]
fun prem_nnf_tac i st =
- full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st
+ full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset)
+ i st
in
fun split_once_tac ctxt split_thms =
@@ -706,10 +716,15 @@
val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal)
val cmap = Splitter.cmap_of_split_thms split_thms
val splits = Splitter.split_posns cmap thy Ts concl
- val split_limit = Config.get ctxt split_limit
in
- if length splits > split_limit then no_tac
- else split_tac split_thms i
+ if null splits orelse length splits > Config.get ctxt split_limit then
+ no_tac
+ else if null (#2 (hd splits)) then
+ split_tac split_thms i
+ else
+ (* disallow a split that involves non-locally bound variables *)
+ (* (except when bound by outermost meta-quantifiers) *)
+ no_tac
end)
in
EVERY' [
@@ -726,7 +741,7 @@
(* remove irrelevant premises, then split the i-th subgoal (and all new *)
(* subgoals) by using 'split_once_tac' repeatedly. Beta-eta-normalize new *)
(* subgoals and finally attempt to solve them by finding an immediate *)
-(* contradiction (i.e. a term and its negation) in their premises. *)
+(* contradiction (i.e., a term and its negation) in their premises. *)
fun pre_tac ctxt i =
let
--- a/src/HOL/Tools/quickcheck_generators.ML Fri Aug 21 13:23:53 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Fri Aug 21 13:25:05 2009 +0200
@@ -321,24 +321,23 @@
fun ensure_random_datatype config raw_tycos thy =
let
- val pp = Syntax.pp_global thy;
val algebra = Sign.classes_of thy;
val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
Datatype.the_descr thy raw_tycos;
- val typrep_vs = (map o apsnd)
+ val typerep_vs = (map o apsnd)
(curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
val random_insts = (map (rpair @{sort random}) o flat o maps snd o maps snd)
- (DatatypeAux.interpret_construction descr typrep_vs
+ (DatatypeAux.interpret_construction descr typerep_vs
{ atyp = single, dtyp = (K o K o K) [] });
val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
- (DatatypeAux.interpret_construction descr typrep_vs
+ (DatatypeAux.interpret_construction descr typerep_vs
{ atyp = K [], dtyp = K o K });
val has_inst = exists (fn tyco =>
can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
in if has_inst then thy
- else case perhaps_constrain thy (random_insts @ term_of_insts) typrep_vs
+ else case perhaps_constrain thy (random_insts @ term_of_insts) typerep_vs
of SOME constrain => mk_random_datatype config descr
- (map constrain typrep_vs) tycos prfx (names, auxnames)
+ (map constrain typerep_vs) tycos prfx (names, auxnames)
((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
| NONE => thy
end;
--- a/src/HOL/Tools/typecopy.ML Fri Aug 21 13:23:53 2009 +0200
+++ b/src/HOL/Tools/typecopy.ML Fri Aug 21 13:25:05 2009 +0200
@@ -91,11 +91,10 @@
fun add_default_code tyco thy =
let
- val SOME { constr = constr_name, proj = (proj, _), proj_def = proj_eq, vs = raw_vs,
+ val SOME { constr = c, proj = (proj, _), proj_def = proj_eq, vs = vs,
typ = ty_rep, ... } = get_info thy tyco;
val SOME { Rep_inject = proj_inject, ... } = Typedef.get_info thy tyco;
- val constr = (constr_name, Logic.unvarifyT (Sign.the_const_type thy constr_name));
- val vs = (map dest_TFree o snd o dest_Type) (Type (tyco, map TFree raw_vs));
+ val constr = (c, Logic.unvarifyT (Sign.the_const_type thy c));
val ty = Type (tyco, map TFree vs);
val proj = Const (proj, ty --> ty_rep);
val (t_x, t_y) = (Free ("x", ty), Free ("y", ty));
--- a/src/Pure/Isar/class_target.ML Fri Aug 21 13:23:53 2009 +0200
+++ b/src/Pure/Isar/class_target.ML Fri Aug 21 13:25:05 2009 +0200
@@ -513,6 +513,7 @@
| NONE => NONE;
in
thy
+ |> Theory.checkpoint
|> ProofContext.init
|> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
|> fold (Variable.declare_typ o TFree) vs
--- a/src/Pure/Isar/overloading.ML Fri Aug 21 13:23:53 2009 +0200
+++ b/src/Pure/Isar/overloading.ML Fri Aug 21 13:25:05 2009 +0200
@@ -154,6 +154,7 @@
val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading;
in
thy
+ |> Theory.checkpoint
|> ProofContext.init
|> OverloadingData.put overloading
|> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
--- a/src/ZF/ex/Limit.thy Fri Aug 21 13:23:53 2009 +0200
+++ b/src/ZF/ex/Limit.thy Fri Aug 21 13:25:05 2009 +0200
@@ -488,18 +488,24 @@
and Mfun: "M \<in> nat->nat->set(D)"
and cpoD: "cpo(D)"
shows "matrix(D,M)"
-apply (simp add: matrix_def, safe)
-apply (rule Mfun)
-apply (cut_tac y1 = m and n = n in yprem [THEN chain_rel], simp+)
-apply (simp add: chain_rel xprem)
-apply (rule cpo_trans [OF cpoD])
-apply (cut_tac y1 = m and n = n in yprem [THEN chain_rel], simp+)
-apply (simp_all add: chain_fun [THEN apply_type] xprem)
-done
-
-lemma lemma_rel_rel:
- "[|m \<in> nat; rel(D, (\<lambda>n \<in> nat. M`n`n)`m, y)|] ==> rel(D,M`m`m, y)"
-by simp
+proof -
+ {
+ fix n m assume "n : nat" "m : nat"
+ with chain_rel [OF yprem]
+ have "rel(D, M ` n ` m, M ` succ(n) ` m)" by simp
+ } note rel_succ = this
+ show "matrix(D,M)"
+ proof (simp add: matrix_def Mfun rel_succ, intro conjI ballI)
+ fix n m assume n: "n : nat" and m: "m : nat"
+ thus "rel(D, M ` n ` m, M ` n ` succ(m))"
+ by (simp add: chain_rel xprem)
+ next
+ fix n m assume n: "n : nat" and m: "m : nat"
+ thus "rel(D, M ` n ` m, M ` succ(n) ` succ(m))"
+ by (rule cpo_trans [OF cpoD rel_succ],
+ simp_all add: chain_fun [THEN apply_type] xprem)
+ qed
+qed
lemma lemma2:
"[|x \<in> nat; m \<in> nat; rel(D,(\<lambda>n \<in> nat. M`n`m1)`x,(\<lambda>n \<in> nat. M`n`m1)`m)|]
@@ -509,65 +515,72 @@
lemma isub_lemma:
"[|isub(D, \<lambda>n \<in> nat. M`n`n, y); matrix(D,M); cpo(D)|]
==> isub(D, \<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m), y)"
-apply (unfold isub_def, safe)
-apply (simp (no_asm_simp))
-apply (frule matrix_fun [THEN apply_type], assumption)
-apply (simp (no_asm_simp))
-apply (rule matrix_chain_left [THEN cpo_lub, THEN islub_least], assumption+)
-apply (unfold isub_def, safe)
-(*???VERY indirect proof: beta-redexes could be simplified now!*)
-apply (rename_tac k n)
-apply (case_tac "k le n")
-apply (rule cpo_trans, assumption)
-apply (rule lemma2)
-apply (rule_tac [4] lemma_rel_rel)
-prefer 5 apply blast
-apply (assumption | rule chain_rel_gen matrix_chain_right matrix_in isubD1)+
-txt{*opposite case*}
-apply (rule cpo_trans, assumption)
-apply (rule not_le_iff_lt [THEN iffD1, THEN leI, THEN chain_rel_gen])
-prefer 3 apply assumption
-apply (assumption | rule nat_into_Ord matrix_chain_left)+
-apply (rule lemma_rel_rel)
-apply (simp_all add: matrix_in)
-done
+proof (simp add: isub_def, safe)
+ fix n
+ assume DM: "matrix(D, M)" and D: "cpo(D)" and n: "n \<in> nat" and y: "y \<in> set(D)"
+ and rel: "\<forall>n\<in>nat. rel(D, M ` n ` n, y)"
+ have "rel(D, lub(D, M ` n), y)"
+ proof (rule matrix_chain_left [THEN cpo_lub, THEN islub_least], simp_all add: n D DM)
+ show "isub(D, M ` n, y)"
+ proof (unfold isub_def, intro conjI ballI y)
+ fix k assume k: "k \<in> nat"
+ show "rel(D, M ` n ` k, y)"
+ proof (cases "n le k")
+ case True
+ hence yy: "rel(D, M`n`k, M`k`k)"
+ by (blast intro: lemma2 n k y DM D chain_rel_gen matrix_chain_right)
+ show "?thesis"
+ by (rule cpo_trans [OF D yy],
+ simp_all add: k rel n y DM matrix_in)
+ next
+ case False
+ hence le: "k le n"
+ by (blast intro: not_le_iff_lt [THEN iffD1, THEN leI] nat_into_Ord n k)
+ show "?thesis"
+ by (rule cpo_trans [OF D chain_rel_gen [OF le]],
+ simp_all add: n y k rel DM D matrix_chain_left)
+ qed
+ qed
+ qed
+ moreover
+ have "M ` n \<in> nat \<rightarrow> set(D)" by (blast intro: DM n matrix_fun [THEN apply_type])
+ ultimately show "rel(D, lub(D, Lambda(nat, op `(M ` n))), y)" by simp
+qed
lemma matrix_chain_lub:
"[|matrix(D,M); cpo(D)|] ==> chain(D,\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m))"
-apply (simp add: chain_def, safe)
-apply (rule lam_type)
-apply (rule islub_in)
-apply (rule cpo_lub)
-prefer 2 apply assumption
-apply (rule chainI)
-apply (rule lam_type)
-apply (simp_all add: matrix_in)
-apply (rule matrix_rel_0_1, assumption+)
-apply (simp add: matrix_chain_left [THEN chain_fun, THEN eta])
-apply (rule dominate_islub)
-apply (rule_tac [3] cpo_lub)
-apply (rule_tac [2] cpo_lub)
-apply (simp add: dominate_def)
-apply (blast intro: matrix_rel_1_0)
-apply (simp_all add: matrix_chain_left nat_succI chain_fun)
-done
+proof (simp add: chain_def, intro conjI ballI)
+ assume "matrix(D, M)" "cpo(D)"
+ thus "(\<lambda>x\<in>nat. lub(D, Lambda(nat, op `(M ` x)))) \<in> nat \<rightarrow> set(D)"
+ by (force intro: islub_in cpo_lub chainI lam_type matrix_in matrix_rel_0_1)
+next
+ fix n
+ assume DD: "matrix(D, M)" "cpo(D)" "n \<in> nat"
+ hence "dominate(D, M ` n, M ` succ(n))"
+ by (force simp add: dominate_def intro: matrix_rel_1_0)
+ with DD show "rel(D, lub(D, Lambda(nat, op `(M ` n))),
+ lub(D, Lambda(nat, op `(M ` succ(n)))))"
+ by (simp add: matrix_chain_left [THEN chain_fun, THEN eta]
+ dominate_islub cpo_lub matrix_chain_left chain_fun)
+qed
lemma isub_eq:
- "[|matrix(D,M); cpo(D)|]
- ==> isub(D,(\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m)),y) <->
- isub(D,(\<lambda>n \<in> nat. M`n`n),y)"
-apply (rule iffI)
-apply (rule dominate_isub)
-prefer 2 apply assumption
-apply (simp add: dominate_def)
-apply (rule ballI)
-apply (rule bexI, auto)
-apply (simp add: matrix_chain_left [THEN chain_fun, THEN eta])
-apply (rule islub_ub)
-apply (rule cpo_lub)
-apply (simp_all add: matrix_chain_left matrix_chain_diag chain_fun
- matrix_chain_lub isub_lemma)
-done
+ assumes DM: "matrix(D, M)" and D: "cpo(D)"
+ shows "isub(D,(\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m)),y) <-> isub(D,(\<lambda>n \<in> nat. M`n`n),y)"
+proof
+ assume isub: "isub(D, \<lambda>n\<in>nat. lub(D, Lambda(nat, op `(M ` n))), y)"
+ hence dom: "dominate(D, \<lambda>n\<in>nat. M ` n ` n, \<lambda>n\<in>nat. lub(D, Lambda(nat, op `(M ` n))))"
+ using DM D
+ by (simp add: dominate_def, intro ballI bexI,
+ simp_all add: matrix_chain_left [THEN chain_fun, THEN eta] islub_ub cpo_lub matrix_chain_left)
+ thus "isub(D, \<lambda>n\<in>nat. M ` n ` n, y)" using DM D
+ by - (rule dominate_isub [OF dom isub],
+ simp_all add: matrix_chain_diag chain_fun matrix_chain_lub)
+next
+ assume isub: "isub(D, \<lambda>n\<in>nat. M ` n ` n, y)"
+ thus "isub(D, \<lambda>n\<in>nat. lub(D, Lambda(nat, op `(M ` n))), y)" using DM D
+ by (simp add: isub_lemma)
+qed
lemma lub_matrix_diag_aux1:
"lub(D,(\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m))) =
@@ -695,34 +708,43 @@
"[|chain(cf(D,E),X); chain(D,Xa); cpo(D); cpo(E) |]
==> matrix(E,\<lambda>x \<in> nat. \<lambda>xa \<in> nat. X`x`(Xa`xa))"
apply (rule matrix_chainI, auto)
-apply (rule chainI)
-apply (blast intro: lam_type apply_funtype cont_fun cf_cont chain_in, simp)
-apply (blast intro: cont_mono nat_succI chain_rel cf_cont chain_in)
-apply (rule chainI)
-apply (blast intro: lam_type apply_funtype cont_fun cf_cont chain_in, simp)
-apply (rule rel_cf)
-apply (simp_all add: chain_in chain_rel)
+apply (force intro: chainI lam_type apply_funtype cont_fun cf_cont cont_mono)
+apply (force intro: chainI lam_type apply_funtype cont_fun cf_cont rel_cf)
apply (blast intro: lam_type apply_funtype cont_fun cf_cont chain_in)
done
lemma chain_cf_lub_cont:
- "[|chain(cf(D,E),X); cpo(D); cpo(E) |]
- ==> (\<lambda>x \<in> set(D). lub(E, \<lambda>n \<in> nat. X ` n ` x)) \<in> cont(D, E)"
-apply (rule contI)
-apply (rule lam_type)
-apply (assumption | rule chain_cf [THEN cpo_lub, THEN islub_in])+
-apply simp
-apply (rule dominate_islub)
-apply (erule_tac [2] chain_cf [THEN cpo_lub], simp_all)+
-apply (rule dominateI, assumption, simp)
-apply (assumption | rule chain_in [THEN cf_cont, THEN cont_mono])+
-apply (assumption | rule chain_cf [THEN chain_fun])+
-apply (simp add: cpo_lub [THEN islub_in]
- chain_in [THEN cf_cont, THEN cont_lub])
-apply (frule matrix_lemma [THEN lub_matrix_diag], assumption+)
-apply (simp add: chain_in [THEN beta])
-apply (drule matrix_lemma [THEN lub_matrix_diag_sym], auto)
-done
+ assumes ch: "chain(cf(D,E),X)" and D: "cpo(D)" and E: "cpo(E)"
+ shows "(\<lambda>x \<in> set(D). lub(E, \<lambda>n \<in> nat. X ` n ` x)) \<in> cont(D, E)"
+proof (rule contI)
+ show "(\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) \<in> set(D) \<rightarrow> set(E)"
+ by (blast intro: lam_type chain_cf [THEN cpo_lub, THEN islub_in] ch E)
+next
+ fix x y
+ assume xy: "rel(D, x, y)" "x \<in> set(D)" "y \<in> set(D)"
+ hence dom: "dominate(E, \<lambda>n\<in>nat. X ` n ` x, \<lambda>n\<in>nat. X ` n ` y)"
+ by (force intro: dominateI chain_in [OF ch, THEN cf_cont, THEN cont_mono])
+ note chE = chain_cf [OF ch]
+ from xy show "rel(E, (\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) ` x,
+ (\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) ` y)"
+ by (simp add: dominate_islub [OF dom] cpo_lub [OF chE] E chain_fun [OF chE])
+next
+ fix Y
+ assume chDY: "chain(D,Y)"
+ have "lub(E, \<lambda>x\<in>nat. lub(E, \<lambda>y\<in>nat. X ` x ` (Y ` y))) =
+ lub(E, \<lambda>x\<in>nat. X ` x ` (Y ` x))"
+ using matrix_lemma [THEN lub_matrix_diag, OF ch chDY]
+ by (simp add: D E)
+ also have "... = lub(E, \<lambda>x\<in>nat. lub(E, \<lambda>n\<in>nat. X ` n ` (Y ` x)))"
+ using matrix_lemma [THEN lub_matrix_diag_sym, OF ch chDY]
+ by (simp add: D E)
+ finally have "lub(E, \<lambda>x\<in>nat. lub(E, \<lambda>n\<in>nat. X ` x ` (Y ` n))) =
+ lub(E, \<lambda>x\<in>nat. lub(E, \<lambda>n\<in>nat. X ` n ` (Y ` x)))" .
+ thus "(\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) ` lub(D, Y) =
+ lub(E, \<lambda>n\<in>nat. (\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) ` (Y ` n))"
+ by (simp add: cpo_lub [THEN islub_in] D chDY
+ chain_in [THEN cf_cont, THEN cont_lub, OF ch])
+ qed
lemma islub_cf:
"[| chain(cf(D,E),X); cpo(D); cpo(E)|]