# HG changeset patch # User boehmes # Date 1250853905 -7200 # Node ID e1ebd4d5d18163b159d7dc277c7e356f6523bf3b # Parent 18bbd9f4c2cdc1bef9153fa179b32f3cf99ee223# Parent f3fed9cc423f1d15ae76c2e3dae005c371c9f7b3 merged diff -r 18bbd9f4c2cd -r e1ebd4d5d181 src/HOL/Auth/KerberosIV.thy --- 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!]: "\ Key (shrK A) \ parts (spies evs); evs \ kerbIV \ \ 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: "\ \ expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \ \ \ 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 \ 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 @@ \ set evs; authK \ symKeys; Key authK \ analz (spies evs); evs \ kerbIV \ \ Key servK \ 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: "\ Crypt authK \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 \ 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: "\ (CT evs) = T; Number T \ parts {X}; evs \ kerbIV \ \ \ A B Y. A \ bad \ Says A B \Y, X\ \ 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: "\ Crypt K \Agent A, Number T\ \ parts (spies evs); diff -r 18bbd9f4c2cd -r e1ebd4d5d181 src/HOL/Auth/OtwayRees_AN.thy --- 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|} \ set evs; A \ bad; B \ bad; evs \ otway |] ==> Key K \ 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 @@ \NB. Notes Spy {|NA, NB, Key K|} \ set evs; A \ bad; B \ bad; A \ B; evs \ otway |] ==> Key K \ analz (knows Spy evs)" -by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key) + by (metis A_trusts_OR4 secrecy_lemma) diff -r 18bbd9f4c2cd -r e1ebd4d5d181 src/HOL/Auth/Yahalom.thy --- 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|} \ set evs ==> K \ 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 \ parts (knows Spy evs)"} imply that NOBODY sends messages containing X! *} @@ -275,7 +274,7 @@ Notes Spy {|na, nb, Key K|} \ set evs; A \ bad; B \ bad; evs \ yahalom |] ==> Key K \ 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 \ bad"} then @{term NBa} is known, therefore @{prop "NBa \ 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 \ NBa"}*} -apply (simp add: single_Nonce_secrecy) -apply (blast dest!: no_nonce_YM1_YM2 (*to prove NB\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 @@ \k. Notes Spy {|Nonce NA, Nonce NB, k|} \ set evs; A \ bad; B \ bad; evs \ yahalom |] ==> Key K \ 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 \ bad; B \ bad; evs \ yahalom |] ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \ 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 @@ (\NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \ set evs); A \ bad; B \ bad; evs \ yahalom |] ==> \X. Says A B {|X, Crypt K (Nonce NB)|} \ 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 diff -r 18bbd9f4c2cd -r e1ebd4d5d181 src/HOL/Bali/Basis.thy --- 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" diff -r 18bbd9f4c2cd -r e1ebd4d5d181 src/HOL/Code_Eval.thy --- 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 \ nibble \ char))) + in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''String.char.Char'') (TYPEREP(nibble \ nibble \ char))) (Code_Eval.term_of n)) (Code_Eval.term_of m))" by (subst term_of_anything) rule diff -r 18bbd9f4c2cd -r e1ebd4d5d181 src/HOL/Induct/Com.thy --- 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 @@ "((\x x' y. ((x, x'), y) \ R) <= (\x x' y. ((x, x'), y) \ 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) diff -r 18bbd9f4c2cd -r e1ebd4d5d181 src/HOL/MicroJava/J/JTypeSafe.thy --- 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\(x,s) -e\v -> (x',s'); (x,s)::\E; E\e::T; G=prg E |] diff -r 18bbd9f4c2cd -r e1ebd4d5d181 src/HOL/Predicate.thy --- 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 diff -r 18bbd9f4c2cd -r e1ebd4d5d181 src/HOL/Quickcheck.thy --- 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 [], \u. Code_Eval.term_of (STR []))" + "random _ = Pair (STR '''', \u. Code_Eval.term_of (STR ''''))" instance .. diff -r 18bbd9f4c2cd -r e1ebd4d5d181 src/HOL/Tools/Datatype/datatype.ML --- 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; diff -r 18bbd9f4c2cd -r e1ebd4d5d181 src/HOL/Tools/lin_arith.ML --- 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 diff -r 18bbd9f4c2cd -r e1ebd4d5d181 src/HOL/Tools/quickcheck_generators.ML --- 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; diff -r 18bbd9f4c2cd -r e1ebd4d5d181 src/HOL/Tools/typecopy.ML --- 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)); diff -r 18bbd9f4c2cd -r e1ebd4d5d181 src/Pure/Isar/class_target.ML --- 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 diff -r 18bbd9f4c2cd -r e1ebd4d5d181 src/Pure/Isar/overloading.ML --- 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 diff -r 18bbd9f4c2cd -r e1ebd4d5d181 src/ZF/ex/Limit.thy --- 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 \ 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 \ nat; rel(D, (\n \ 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 \ nat; m \ nat; rel(D,(\n \ nat. M`n`m1)`x,(\n \ nat. M`n`m1)`m)|] @@ -509,65 +515,72 @@ lemma isub_lemma: "[|isub(D, \n \ nat. M`n`n, y); matrix(D,M); cpo(D)|] ==> isub(D, \n \ nat. lub(D,\m \ 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 \ nat" and y: "y \ set(D)" + and rel: "\n\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 \ 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 \ nat \ 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,\n \ nat. lub(D,\m \ 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 "(\x\nat. lub(D, Lambda(nat, op `(M ` x)))) \ nat \ 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 \ 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,(\n \ nat. lub(D,\m \ nat. M`n`m)),y) <-> - isub(D,(\n \ 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,(\n \ nat. lub(D,\m \ nat. M`n`m)),y) <-> isub(D,(\n \ nat. M`n`n),y)" +proof + assume isub: "isub(D, \n\nat. lub(D, Lambda(nat, op `(M ` n))), y)" + hence dom: "dominate(D, \n\nat. M ` n ` n, \n\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, \n\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, \n\nat. M ` n ` n, y)" + thus "isub(D, \n\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,(\n \ nat. lub(D,\m \ nat. M`n`m))) = @@ -695,34 +708,43 @@ "[|chain(cf(D,E),X); chain(D,Xa); cpo(D); cpo(E) |] ==> matrix(E,\x \ nat. \xa \ 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) |] - ==> (\x \ set(D). lub(E, \n \ nat. X ` n ` x)) \ 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 "(\x \ set(D). lub(E, \n \ nat. X ` n ` x)) \ cont(D, E)" +proof (rule contI) + show "(\x\set(D). lub(E, \n\nat. X ` n ` x)) \ set(D) \ 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 \ set(D)" "y \ set(D)" + hence dom: "dominate(E, \n\nat. X ` n ` x, \n\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, (\x\set(D). lub(E, \n\nat. X ` n ` x)) ` x, + (\x\set(D). lub(E, \n\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, \x\nat. lub(E, \y\nat. X ` x ` (Y ` y))) = + lub(E, \x\nat. X ` x ` (Y ` x))" + using matrix_lemma [THEN lub_matrix_diag, OF ch chDY] + by (simp add: D E) + also have "... = lub(E, \x\nat. lub(E, \n\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, \x\nat. lub(E, \n\nat. X ` x ` (Y ` n))) = + lub(E, \x\nat. lub(E, \n\nat. X ` n ` (Y ` x)))" . + thus "(\x\set(D). lub(E, \n\nat. X ` n ` x)) ` lub(D, Y) = + lub(E, \n\nat. (\x\set(D). lub(E, \n\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)|]