--- a/src/HOL/Auth/KerberosIV.thy Fri Aug 14 15:36:57 2009 +0200
+++ b/src/HOL/Auth/KerberosIV.thy Fri Aug 14 17:27:34 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 14 15:36:57 2009 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy Fri Aug 14 17:27:34 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 14 15:36:57 2009 +0200
+++ b/src/HOL/Auth/Yahalom.thy Fri Aug 14 17:27:34 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,6 @@
(\<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)
-
+atp_minimize [atp=spass] A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz
+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 14 15:36:57 2009 +0200
+++ b/src/HOL/Bali/Basis.thy Fri Aug 14 17:27:34 2009 +0200
@@ -7,8 +7,6 @@
theory Basis imports Main begin
-declare [[unify_search_bound = 40, unify_trace_bound = 40]]
-
section "misc"
@@ -65,36 +63,36 @@
by (auto intro: r_into_rtrancl rtrancl_trans)
lemma triangle_lemma:
- "\<lbrakk> \<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c; (a,x)\<in>r\<^sup>*; (a,y)\<in>r\<^sup>*\<rbrakk>
- \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
+ "\<lbrakk> \<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c; (a,x)\<in>r*; (a,y)\<in>r*\<rbrakk>
+ \<Longrightarrow> (x,y)\<in>r* \<or> (y,x)\<in>r*"
proof -
note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1]
note converse_rtranclE = converse_rtranclE [consumes 1]
assume unique: "\<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c"
- assume "(a,x)\<in>r\<^sup>*"
- then show "(a,y)\<in>r\<^sup>* \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
+ assume "(a,x)\<in>r*"
+ then show "(a,y)\<in>r* \<Longrightarrow> (x,y)\<in>r* \<or> (y,x)\<in>r*"
proof (induct rule: converse_rtrancl_induct)
- assume "(x,y)\<in>r\<^sup>*"
+ assume "(x,y)\<in>r*"
then show ?thesis
by blast
next
fix a v
assume a_v_r: "(a, v) \<in> r" and
- v_x_rt: "(v, x) \<in> r\<^sup>*" and
- a_y_rt: "(a, y) \<in> r\<^sup>*" and
- hyp: "(v, y) \<in> r\<^sup>* \<Longrightarrow> (x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
+ v_x_rt: "(v, x) \<in> r*" and
+ a_y_rt: "(a, y) \<in> r*" and
+ hyp: "(v, y) \<in> r* \<Longrightarrow> (x, y) \<in> r* \<or> (y, x) \<in> r*"
from a_y_rt
- show "(x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
+ show "(x, y) \<in> r* \<or> (y, x) \<in> r*"
proof (cases rule: converse_rtranclE)
assume "a=y"
- with a_v_r v_x_rt have "(y,x) \<in> r\<^sup>*"
+ with a_v_r v_x_rt have "(y,x) \<in> r*"
by (auto intro: r_into_rtrancl rtrancl_trans)
then show ?thesis
by blast
next
fix w
assume a_w_r: "(a, w) \<in> r" and
- w_y_rt: "(w, y) \<in> r\<^sup>*"
+ w_y_rt: "(w, y) \<in> r*"
from a_v_r a_w_r unique
have "v=w"
by auto
@@ -107,7 +105,7 @@
lemma rtrancl_cases [consumes 1, case_names Refl Trancl]:
- "\<lbrakk>(a,b)\<in>r\<^sup>*; a = b \<Longrightarrow> P; (a,b)\<in>r\<^sup>+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+ "\<lbrakk>(a,b)\<in>r*; a = b \<Longrightarrow> P; (a,b)\<in>r+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
apply (erule rtranclE)
apply (auto dest: rtrancl_into_trancl1)
done
--- a/src/HOL/Induct/Com.thy Fri Aug 14 15:36:57 2009 +0200
+++ b/src/HOL/Induct/Com.thy Fri Aug 14 17:27:34 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 14 15:36:57 2009 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Fri Aug 14 17:27:34 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/Tools/lin_arith.ML Fri Aug 14 15:36:57 2009 +0200
+++ b/src/HOL/Tools/lin_arith.ML Fri Aug 14 17:27:34 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