# HG changeset patch # User wenzelm # Date 1251366857 -7200 # Node ID 016134424f71926d7fb3747404337eced61f3dff # Parent e87d9c78910c10a4bc3b63fa53e2aa047c2aca8e# Parent 030be5c12d9619abbfdb8bdbfc4cacab96cb351a merged diff -r 030be5c12d96 -r 016134424f71 src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/Auth/Event.thy Thu Aug 27 11:54:17 2009 +0200 @@ -139,9 +139,11 @@ text{*Elimination rules: derive contradictions from old Says events containing items known to be fresh*} +lemmas Says_imp_parts_knows_Spy = + Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] + lemmas knows_Spy_partsEs = - Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard] - parts.Body [THEN revcut_rl, standard] + Says_imp_parts_knows_Spy parts.Body [THEN revcut_rl, standard] lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj] diff -r 030be5c12d96 -r 016134424f71 src/HOL/Auth/KerberosV.thy --- a/src/HOL/Auth/KerberosV.thy Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/Auth/KerberosV.thy Thu Aug 27 11:54:17 2009 +0200 @@ -697,9 +697,7 @@ txt{*K4*} apply (force dest!: Crypt_imp_keysFor, clarify) txt{*K6*} -apply (drule Says_imp_spies [THEN parts.Inj, THEN parts.Fst]) -apply (drule Says_imp_spies [THEN parts.Inj, THEN parts.Snd]) -apply (blast dest!: unique_CryptKey) +apply (metis Says_imp_spies Says_ticket_parts analz.Fst analz.Inj analz_conj_parts unique_CryptKey) done text{*Needs a unicity theorem, hence moved here*} @@ -841,13 +839,10 @@ apply (erule kerbV.induct, analz_mono_contra) apply (frule_tac [7] Says_ticket_parts) apply (frule_tac [5] Says_ticket_parts, 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_invKey_keysFor Says_ticket_analz + analz.Fst invKey_K new_keys_not_analzd parts.Fst Says_imp_parts_knows_Spy + unique_CryptKey) done text{*Long term keys are not issued as servKeys*} @@ -981,9 +976,7 @@ txt{*K4*} apply (blast dest!: authK_not_AKcryptSK) txt{*Oops1*} -apply clarify -apply simp -apply (blast dest!: AKcryptSK_analz_insert) +apply (metis AKcryptSK_analz_insert insert_Key_singleton) done text{* First simplification law for analz: no session keys encrypt @@ -1039,8 +1032,8 @@ \ set evs; authK \ symKeys; Key authK \ analz (spies evs); evs \ kerbV \ \ Key servK \ analz (spies evs)" -apply (force dest: Says_imp_spies [THEN analz.Inj, THEN analz.Fst, THEN analz.Decrypt, THEN analz.Fst]) -done + by (metis Says_imp_analz_Spy analz.Fst analz_Decrypt') + text{*lemma @{text servK_notin_authKeysD} not needed in version V*} @@ -1112,16 +1105,16 @@ apply (frule_tac [5] Says_ticket_analz) 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 -txt{*K2*} -apply (blast intro: parts_insertI less_SucI) -txt{*K4*} -apply (blast dest: authTicket_authentic Confidentiality_Kas) -txt{*Oops1*} + txt{*Fake*} + apply spy_analz + txt{*K2*} + apply (blast intro: parts_insertI less_SucI) + txt{*K4*} + apply (blast dest: authTicket_authentic Confidentiality_Kas) + txt{*Oops1*} 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) +apply (metis Suc_le_eq linorder_linear linorder_not_le msg.simps(2) unique_servKeys) done @@ -1270,17 +1263,7 @@ Key authK \ analz (spies evs); Key servK \ analz (spies evs); A \ bad; B \ bad; evs \ kerbV \ \ Says B A (Crypt servK (Number T3)) \ set evs" -apply (frule authK_authentic) -apply assumption+ -apply (frule servK_authentic) -prefer 2 apply (blast dest: authK_authentic Says_Kas_message_form) -apply assumption+ -apply clarify -apply (blast dest: K4_imp_K2 Key_unique_SesKey intro!: Says_K6) -(*Single command proof: much slower! -apply (blast dest: authK_authentic servK_authentic Says_Kas_message_form Key_unique_SesKey K4_imp_K2 intro!: Says_K6) -*) -done + by (metis authK_authentic Oops_range_spies1 Says_K6 servK_authentic u_K4_imp_K2 unique_authKeys) lemma A_authenticates_B_r: "\ Crypt servK (Number T3) \ parts (spies evs); @@ -1301,8 +1284,7 @@ apply (erule_tac [9] exE) apply (frule_tac [9] K4_imp_K2) apply assumption+ -apply (blast dest: Key_unique_SesKey intro!: Says_K6 dest: Confidentiality_Tgs -) +apply (blast dest: Key_unique_SesKey intro!: Says_K6 dest: Confidentiality_Tgs) done @@ -1478,7 +1460,7 @@ ...expands as follows - including extra exE because of new form of lemmas*) apply (frule K3_imp_K2, assumption, assumption, erule exE, erule exE) apply (case_tac "Key authK \ analz (spies evs5)") -apply (drule Says_imp_knows_Spy [THEN analz.Inj, THEN analz.Fst, THEN analz_Decrypt', THEN analz.Fst], assumption, assumption, simp) + apply (metis Says_imp_analz_Spy analz.Fst analz_Decrypt') apply (frule K3_imp_K2, assumption, assumption, erule exE, erule exE) apply (drule Says_imp_knows_Spy [THEN parts.Inj, THEN parts.Fst]) apply (frule servK_authentic_ter, blast, assumption+) diff -r 030be5c12d96 -r 016134424f71 src/HOL/Auth/Kerberos_BAN.thy --- a/src/HOL/Auth/Kerberos_BAN.thy Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/Auth/Kerberos_BAN.thy Thu Aug 27 11:54:17 2009 +0200 @@ -288,15 +288,8 @@ on evs)" apply (unfold before_def) apply (erule rev_mp) -apply (erule bankerberos.induct, simp_all) -txt{*We need this simplification only for Message 2*} -apply (simp (no_asm) add: takeWhile_tail) -apply auto -txt{*Two subcases of Message 2. 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 (erule bankerberos.induct, simp_all add: takeWhile_tail) +apply (metis length_rev set_rev takeWhile_void used_evs_rev) done @@ -492,6 +485,7 @@ txt{*BK3*} apply (blast dest: Kab_authentic unique_session_keys) done + lemma lemma_B [rule_format]: "\ B \ bad; evs \ bankerberos \ \ Key K \ analz (spies evs) \ @@ -585,9 +579,8 @@ txt{*BK2*} apply (blast intro: parts_insertI less_SucI) txt{*BK3*} -apply (case_tac "Aa \ bad") - prefer 2 apply (blast dest: Kab_authentic unique_session_keys) -apply (blast dest: Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz intro: less_SucI) +apply (metis Crypt_Spy_analz_bad Kab_authentic Says_imp_analz_Spy + Says_imp_parts_knows_Spy analz.Snd less_SucI unique_session_keys) txt{*Oops: PROOF FAILS if unsafe intro below*} apply (blast dest: unique_session_keys intro!: less_SucI) done diff -r 030be5c12d96 -r 016134424f71 src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/Auth/NS_Shared.thy Thu Aug 27 11:54:17 2009 +0200 @@ -273,11 +273,11 @@ apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz) txt{*NS2*} apply blast -txt{*NS3, Server sub-case*} +txt{*NS3*} apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2 dest: Says_imp_knows_Spy analz.Inj unique_session_keys) -txt{*NS3, Spy sub-case; also Oops*} -apply (blast dest: unique_session_keys)+ +txt{*Oops*} +apply (blast dest: unique_session_keys) done diff -r 030be5c12d96 -r 016134424f71 src/HOL/Auth/Recur.thy --- a/src/HOL/Auth/Recur.thy Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/Auth/Recur.thy Thu Aug 27 11:54:17 2009 +0200 @@ -419,15 +419,10 @@ apply spy_analz txt{*RA2*} apply blast -txt{*RA3 remains*} +txt{*RA3*} apply (simp add: parts_insert_spies) -txt{*Now we split into two cases. A single blast could do it, but it would take - a CPU minute.*} -apply (safe del: impCE) -txt{*RA3, case 1: use lemma previously proved by induction*} -apply (blast elim: rev_notE [OF _ respond_Spy_not_see_session_key]) -txt{*RA3, case 2: K is an old key*} -apply (blast dest: resp_analz_insert dest: Key_in_parts_respond) +apply (metis Key_in_parts_respond parts.Body parts.Fst resp_analz_insert + respond_Spy_not_see_session_key usedI) txt{*RA4*} apply blast done diff -r 030be5c12d96 -r 016134424f71 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/GCD.thy Thu Aug 27 11:54:17 2009 +0200 @@ -1895,8 +1895,6 @@ lemmas prime_int_simp_number_of[simp] = prime_int_simp[of "number_of m", standard] -declare successor_int_def[simp] - lemma two_is_prime_nat [simp]: "prime (2::nat)" by simp diff -r 030be5c12d96 -r 016134424f71 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/HOL.thy Thu Aug 27 11:54:17 2009 +0200 @@ -29,6 +29,7 @@ "~~/src/Tools/induct.ML" ("~~/src/Tools/induct_tacs.ML") ("Tools/recfun_codegen.ML") + "~~/src/Tools/more_conv.ML" begin setup {* Intuitionistic.method_setup @{binding iprover} *} diff -r 030be5c12d96 -r 016134424f71 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/IsaMakefile Thu Aug 27 11:54:17 2009 +0200 @@ -108,6 +108,7 @@ $(SRC)/Tools/random_word.ML \ $(SRC)/Tools/value.ML \ $(SRC)/Tools/Code_Generator.thy \ + $(SRC)/Tools/more_conv.ML \ HOL.thy \ Tools/hologic.ML \ Tools/recfun_codegen.ML \ diff -r 030be5c12d96 -r 016134424f71 src/HOL/Library/Euclidean_Space.thy --- a/src/HOL/Library/Euclidean_Space.thy Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/Library/Euclidean_Space.thy Thu Aug 27 11:54:17 2009 +0200 @@ -3926,14 +3926,6 @@ shows "finite s \ card s \ card t" by (metis exchange_lemma[OF f i sp] hassize_def finite_subset card_mono) -lemma finite_Atleast_Atmost[simp]: "finite {f x |x. x\ {(i::'a::finite_intvl_succ) .. j}}" -proof- - have eq: "{f x |x. x\ {i .. j}} = f ` {i .. j}" by auto - show ?thesis unfolding eq - apply (rule finite_imageI) - apply (rule finite_intvl) - done -qed lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\ (UNIV::'a::finite set)}" proof- diff -r 030be5c12d96 -r 016134424f71 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Thu Aug 27 11:54:17 2009 +0200 @@ -2503,6 +2503,29 @@ then show ?thesis unfolding fps_inv_right[OF c0 c1] by simp qed +lemma fps_ginv_deriv: + assumes a0:"a$0 = (0::'a::{field})" and a1: "a$1 \ 0" + shows "fps_deriv (fps_ginv b a) = (fps_deriv b / fps_deriv a) oo fps_ginv X a" +proof- + let ?ia = "fps_ginv b a" + let ?iXa = "fps_ginv X a" + let ?d = "fps_deriv" + let ?dia = "?d ?ia" + have iXa0: "?iXa $ 0 = 0" by (simp add: fps_ginv_def) + have da0: "?d a $ 0 \ 0" using a1 by simp + from fps_ginv[OF a0 a1, of b] have "?d (?ia oo a) = fps_deriv b" by simp + then have "(?d ?ia oo a) * ?d a = ?d b" unfolding fps_compose_deriv[OF a0] . + then have "(?d ?ia oo a) * ?d a * inverse (?d a) = ?d b * inverse (?d a)" by simp + then have "(?d ?ia oo a) * (inverse (?d a) * ?d a) = ?d b / ?d a" + by (simp add: fps_divide_def) + then have "(?d ?ia oo a) oo ?iXa = (?d b / ?d a) oo ?iXa " + unfolding inverse_mult_eq_1[OF da0] by simp + then have "?d ?ia oo (a oo ?iXa) = (?d b / ?d a) oo ?iXa" + unfolding fps_compose_assoc[OF iXa0 a0] . + then show ?thesis unfolding fps_inv_ginv[symmetric] + unfolding fps_inv_right[OF a0 a1] by simp +qed + subsection{* Elementary series *} subsubsection{* Exponential series *} diff -r 030be5c12d96 -r 016134424f71 src/HOL/Library/normarith.ML --- a/src/HOL/Library/normarith.ML Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/Library/normarith.ML Thu Aug 27 11:54:17 2009 +0200 @@ -15,7 +15,7 @@ structure NormArith : NORM_ARITH = struct - open Conv Thm Conv2; + open Conv Thm; val bool_eq = op = : bool *bool -> bool fun dest_ratconst t = case term_of t of Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd) @@ -322,6 +322,7 @@ val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE else SOME(norm_cmul_rule v t)) (v ~~ nubs) + fun end_itlist f xs = split_last xs |> uncurry (fold_rev f) in inequality_canon_rule ctxt (end_itlist norm_add_rule ths) end val ges' = map_filter (try compute_ineq) (fold_rev (append o consider) destfuns []) @ @@ -332,9 +333,9 @@ in RealArith.real_linear_prover translator (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero) zerodests, - map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv + map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv arg_conv (arg_conv real_poly_conv))) ges', - map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv + map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv arg_conv (arg_conv real_poly_conv))) gts) end in val real_vector_combo_prover = real_vector_combo_prover @@ -353,6 +354,7 @@ val ntms = fold_rev find_normedterms (map (dest_arg o concl) (ges @ gts)) [] val lctab = vector_lincombs (map snd (filter (not o fst) ntms)) val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt + fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms) fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t fun mk_equals l r = capply (capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r val asl = map2 (fn (t,_) => fn n => assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns diff -r 030be5c12d96 -r 016134424f71 src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Thu Aug 27 11:54:17 2009 +0200 @@ -81,82 +81,6 @@ structure Ctermfunc = FuncFun(type key = cterm val ord = (fn (s,t) => TermOrd.fast_term_ord(term_of s, term_of t))); structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord); - (* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*) -structure Conv2 = -struct - open Conv -fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms) -fun is_comb t = case (term_of t) of _$_ => true | _ => false; -fun is_abs t = case (term_of t) of Abs _ => true | _ => false; - -fun end_itlist f l = - case l of - [] => error "end_itlist" - | [x] => x - | (h::t) => f h (end_itlist f t); - - fun absc cv ct = case term_of ct of - Abs (v,_, _) => - let val (x,t) = Thm.dest_abs (SOME v) ct - in Thm.abstract_rule ((fst o dest_Free o term_of) x) x (cv t) - end - | _ => all_conv ct; - -fun cache_conv conv = - let - val tab = ref Termtab.empty - fun cconv t = - case Termtab.lookup (!tab) (term_of t) of - SOME th => th - | NONE => let val th = conv t - in ((tab := Termtab.insert Thm.eq_thm (term_of t, th) (!tab)); th) end - in cconv end; -fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct')) - handle CTERM _ => false; - -local - fun thenqc conv1 conv2 tm = - case try conv1 tm of - SOME th1 => (case try conv2 (Thm.rhs_of th1) of SOME th2 => Thm.transitive th1 th2 | NONE => th1) - | NONE => conv2 tm - - fun thencqc conv1 conv2 tm = - let val th1 = conv1 tm - in (case try conv2 (Thm.rhs_of th1) of SOME th2 => Thm.transitive th1 th2 | NONE => th1) - end - fun comb_qconv conv tm = - let val (l,r) = Thm.dest_comb tm - in (case try conv l of - SOME th1 => (case try conv r of SOME th2 => Thm.combination th1 th2 - | NONE => Drule.fun_cong_rule th1 r) - | NONE => Drule.arg_cong_rule l (conv r)) - end - fun repeatqc conv tm = thencqc conv (repeatqc conv) tm - fun sub_qconv conv tm = if is_abs tm then absc conv tm else comb_qconv conv tm - fun once_depth_qconv conv tm = - (conv else_conv (sub_qconv (once_depth_qconv conv))) tm - fun depth_qconv conv tm = - thenqc (sub_qconv (depth_qconv conv)) - (repeatqc conv) tm - fun redepth_qconv conv tm = - thenqc (sub_qconv (redepth_qconv conv)) - (thencqc conv (redepth_qconv conv)) tm - fun top_depth_qconv conv tm = - thenqc (repeatqc conv) - (thencqc (sub_qconv (top_depth_qconv conv)) - (thencqc conv (top_depth_qconv conv))) tm - fun top_sweep_qconv conv tm = - thenqc (repeatqc conv) - (sub_qconv (top_sweep_qconv conv)) tm -in -val (once_depth_conv, depth_conv, rdepth_conv, top_depth_conv, top_sweep_conv) = - (fn c => try_conv (once_depth_qconv c), - fn c => try_conv (depth_qconv c), - fn c => try_conv (redepth_qconv c), - fn c => try_conv (top_depth_qconv c), - fn c => try_conv (top_sweep_qconv c)); -end; -end; (* Some useful derived rules *) @@ -373,15 +297,6 @@ fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms) fun is_comb t = case (term_of t) of _$_ => true | _ => false; -fun cache_conv conv = - let - val tab = ref Termtab.empty - fun cconv t = - case Termtab.lookup (!tab) (term_of t) of - SOME th => th - | NONE => let val th = conv t - in ((tab := Termtab.insert Thm.eq_thm (term_of t, th) (!tab)); th) end - in cconv end; fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct')) handle CTERM _ => false; @@ -571,7 +486,7 @@ val nnf_norm_conv' = nnf_conv then_conv literals_conv [@{term "op &"}, @{term "op |"}] [] - (cache_conv + (More_Conv.cache_conv (first_conv [real_lt_conv, real_le_conv, real_eq_conv, real_not_lt_conv, real_not_le_conv, real_not_eq_conv, all_conv])) diff -r 030be5c12d96 -r 016134424f71 src/HOL/List.thy --- a/src/HOL/List.thy Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/List.thy Thu Aug 27 11:54:17 2009 +0200 @@ -881,10 +881,8 @@ lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \ P x}" by (induct xs) auto -lemma set_upt [simp]: "set[i.. k \ k < j}" -apply (induct j, simp_all) -apply (erule ssubst, auto) -done +lemma set_upt [simp]: "set[i.. \ys zs. xs = ys @ x # zs" @@ -2394,6 +2392,30 @@ nth_Cons_number_of [simp] +subsubsection {* @{text upto}: interval-list on @{typ int} *} + +(* FIXME make upto tail recursive? *) + +function upto :: "int \ int \ int list" ("(1[_../_])") where +"upto i j = (if i \ j then i # [i+1..j] else [])" +by auto +termination +by(relation "measure(%(i::int,j). nat(j - i + 1))") auto + +declare upto.simps[code, simp del] + +lemmas upto_rec_number_of[simp] = + upto.simps[of "number_of m" "number_of n", standard] + +lemma upto_empty[simp]: "j < i \ [i..j] = []" +by(simp add: upto.simps) + +lemma set_upto[simp]: "set[i..j] = {i..j}" +apply(induct i j rule:upto.induct) +apply(simp add: upto.simps simp_from_to) +done + + subsubsection {* @{text "distinct"} and @{text remdups} *} lemma distinct_append [simp]: @@ -2448,6 +2470,12 @@ lemma distinct_upt[simp]: "distinct[i.. distinct (take i xs)" apply(induct xs arbitrary: i) apply simp @@ -3091,6 +3119,12 @@ lemma sorted_upt[simp]: "sorted[i.. 'a" -assumes finite_intvl: "finite{a..b}" -and successor_incr: "a < successor a" -and ord_discrete: "\(\x. a < x & x < successor a)" - -context finite_intvl_succ -begin - -definition - upto :: "'a \ 'a \ 'a list" ("(1[_../_])") where -"upto i j == sorted_list_of_set {i..j}" - -lemma upto[simp]: "set[a..b] = {a..b} & sorted[a..b] & distinct[a..b]" -by(simp add:upto_def finite_intvl) - -lemma insert_intvl: "i \ j \ insert i {successor i..j} = {i..j}" -apply(insert successor_incr[of i]) -apply(auto simp: atLeastAtMost_def atLeast_def atMost_def) -apply(metis ord_discrete less_le not_le) -done - -lemma sorted_list_of_set_rec: "i \ j \ - sorted_list_of_set {i..j} = i # sorted_list_of_set {successor i..j}" -apply(simp add:sorted_list_of_set_def upto_def) -apply (rule the1_equality[OF finite_sorted_distinct_unique]) - apply (simp add:finite_intvl) -apply(rule the1I2[OF finite_sorted_distinct_unique]) - apply (simp add:finite_intvl) -apply (simp add: sorted_Cons insert_intvl Ball_def) -apply (metis successor_incr leD less_imp_le order_trans) -done - -lemma sorted_list_of_set_rec2: "i \ j \ - sorted_list_of_set {i..successor j} = - sorted_list_of_set {i..j} @ [successor j]" -apply(simp add:sorted_list_of_set_def upto_def) -apply (rule the1_equality[OF finite_sorted_distinct_unique]) - apply (simp add:finite_intvl) -apply(rule the1I2[OF finite_sorted_distinct_unique]) - apply (simp add:finite_intvl) -apply (simp add: sorted_append Ball_def expand_set_eq) -apply(rule conjI) -apply (metis eq_iff leD linear not_leE ord_discrete order_trans successor_incr) -apply (metis leD linear order_trans successor_incr) -done - -lemma upto_rec[code]: "[i..j] = (if i \ j then i # [successor i..j] else [])" -by(simp add: upto_def sorted_list_of_set_rec) - -lemma upto_empty[simp]: "j < i \ [i..j] = []" -by(simp add: upto_rec) - -lemma upto_rec2: "i \ j \ [i..successor j] = [i..j] @ [successor j]" -by(simp add: upto_def sorted_list_of_set_rec2) - -end - -text{* The integers are an instance of the above class: *} - -instantiation int:: finite_intvl_succ -begin - -definition -successor_int_def[simp]: "successor = (%i\int. i+1)" - -instance -by intro_classes (simp_all add: successor_int_def) - -end - -text{* Now @{term"[i..j::int]"} is defined for integers. *} - -hide (open) const successor - -lemma upto_rec2_int: "(i::int) \ j \ [i..j+1] = [i..j] @ [j+1]" -by(rule upto_rec2[where 'a = int, simplified successor_int_def]) - -lemmas upto_rec_number_of_int[simp] = upto_rec[of "number_of m :: int" "number_of n", standard] - - subsubsection {* @{text lists}: the list-forming operator over sets *} inductive_set @@ -3829,9 +3780,7 @@ "{n<..p. p < n \ (\s. ap p s \ (\(q,s') \ set (step p s). q < n)) \ bounded (err_step n ap step) n" -apply (unfold bounded_def) -apply clarify -apply (simp add: err_step_def split: err.splits) -apply (simp add: error_def) - apply blast -apply (simp split: split_if_asm) - apply (blast dest: in_map_sndD) -apply (simp add: error_def) -apply blast +apply (clarsimp simp: bounded_def err_step_def split: err.splits) +apply (simp add: error_def image_def) +apply (blast dest: in_map_sndD) done diff -r 030be5c12d96 -r 016134424f71 src/HOL/SET-Protocol/Cardholder_Registration.thy --- a/src/HOL/SET-Protocol/Cardholder_Registration.thy Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy Thu Aug 27 11:54:17 2009 +0200 @@ -715,6 +715,7 @@ ==> P --> (Nonce N \ analz (Key`KK Un H)) = (Nonce N \ analz H)" by (blast intro: analz_mono [THEN [2] rev_subsetD]) + text{*The @{text "(no_asm)"} attribute is essential, since it retains the quantifier and allows the simprule's condition to itself be simplified.*} lemma Nonce_compromise [rule_format (no_asm)]: @@ -741,12 +742,11 @@ apply blast --{*3*} apply blast --{*5*} txt{*Message 6*} -apply (force del: allE ballE impCE simp add: symKey_compromise) +apply (metis symKey_compromise) --{*cardSK compromised*} txt{*Simplify again--necessary because the previous simplification introduces - some logical connectives*} -apply (force del: allE ballE impCE - simp del: image_insert image_Un imp_disjL + some logical connectives*} +apply (force simp del: image_insert image_Un imp_disjL simp add: analz_image_keys_simps symKey_compromise) done diff -r 030be5c12d96 -r 016134424f71 src/HOL/SET-Protocol/Purchase.thy --- a/src/HOL/SET-Protocol/Purchase.thy Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/SET-Protocol/Purchase.thy Thu Aug 27 11:54:17 2009 +0200 @@ -1040,9 +1040,8 @@ apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*} apply simp_all apply blast -apply (force dest!: signed_Hash_imp_used) -apply (clarify) --{*speeds next step*} -apply (blast dest: unique_LID_M) +apply (metis subsetD insert_subset parts.Fst parts_increasing signed_Hash_imp_used) +apply (metis unique_LID_M) apply (blast dest!: Notes_Cardholder_self_False) done diff -r 030be5c12d96 -r 016134424f71 src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/SetInterval.thy Thu Aug 27 11:54:17 2009 +0200 @@ -186,28 +186,70 @@ seems to take forever (more than one hour). *} end -subsubsection{* Emptyness and singletons *} +subsubsection{* Emptyness, singletons, subset *} context order begin -lemma atLeastAtMost_empty [simp]: "n < m ==> {m..n} = {}"; -by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) +lemma atLeastatMost_empty[simp]: + "b < a \ {a..b} = {}" +by(auto simp: atLeastAtMost_def atLeast_def atMost_def) + +lemma atLeastatMost_empty_iff[simp]: + "{a..b} = {} \ (~ a <= b)" +by auto (blast intro: order_trans) + +lemma atLeastatMost_empty_iff2[simp]: + "{} = {a..b} \ (~ a <= b)" +by auto (blast intro: order_trans) + +lemma atLeastLessThan_empty[simp]: + "b <= a \ {a.. m ==> {m.. (~ a < b)" +by auto (blast intro: le_less_trans) + +lemma atLeastLessThan_empty_iff2[simp]: + "{} = {a.. (~ a < b)" +by auto (blast intro: le_less_trans) -lemma greaterThanAtMost_empty[simp]:"l \ k ==> {k<..l} = {}" +lemma greaterThanAtMost_empty[simp]: "l \ k ==> {k<..l} = {}" by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) +lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \ ~ k < l" +by auto (blast intro: less_le_trans) + +lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \ ~ k < l" +by auto (blast intro: less_le_trans) + lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<.. (~ a <= b) | c <= a & b <= d" +unfolding atLeastAtMost_def atLeast_def atMost_def +by (blast intro: order_trans) + +lemma atLeastatMost_psubset_iff: + "{a..b} < {c..d} \ + ((~ a <= b) | c <= a & b <= d & (c < a | b < d)) & c <= d" +by(simp add: psubset_eq expand_set_eq less_le_not_le)(blast intro: order_trans) + end +lemma (in linorder) atLeastLessThan_subset_iff: + "{a.. b <= a | c<=a & b<=d" +apply (auto simp:subset_eq Ball_def) +apply(frule_tac x=a in spec) +apply(erule_tac x=d in allE) +apply (simp add: less_imp_le) +done + subsection {* Intervals of natural numbers *} subsubsection {* The Constant @{term lessThan} *} diff -r 030be5c12d96 -r 016134424f71 src/HOL/Tools/Function/fundef_core.ML --- a/src/HOL/Tools/Function/fundef_core.ML Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/Tools/Function/fundef_core.ML Thu Aug 27 11:54:17 2009 +0200 @@ -577,8 +577,6 @@ val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm accp_subset_induct} -fun binder_conv cv ctxt = Conv.arg_conv (Conv.abs_conv (K cv) ctxt); - fun mk_partial_induct_rule thy globals R complete_thm clauses = let val Globals {domT, x, z, a, P, D, ...} = globals @@ -614,7 +612,7 @@ val case_hyp_conv = K (case_hyp RS eq_reflection) local open Conv in val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D - val sih = fconv_rule (binder_conv (arg1_conv (arg_conv (arg_conv case_hyp_conv))) ctxt) aihyp + val sih = fconv_rule (More_Conv.binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp end fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = diff -r 030be5c12d96 -r 016134424f71 src/HOL/Tools/Mirabelle/Tools/mirabelle.ML --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Thu Aug 27 11:54:17 2009 +0200 @@ -7,11 +7,11 @@ type action val register : string * action -> theory -> theory + val logfile : string Config.T val timeout : int Config.T val verbose : bool Config.T val start_line : int Config.T val end_line : int Config.T - val set_logfile : string -> theory -> theory val goal_thm_of : Proof.state -> thm val can_apply : (Proof.context -> int -> tactic) -> Proof.state -> bool @@ -59,10 +59,6 @@ val setup = setup1 #> setup2 #> setup3 #> setup4 #> setup5 -fun set_logfile name = - let val _ = File.write (Path.explode name) "" (* erase file content *) - in Config.put_thy logfile name end - local fun log thy s = @@ -90,15 +86,11 @@ let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line in if in_range l r (Position.line_of pos) then f x else [] end -fun pretty_print verbose pos name msgs = +fun pretty_print pos name msgs = let - val file = the_default "unknown file" (Position.file_of pos) - val str0 = string_of_int o the_default 0 val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) - - val full_loc = if verbose then file ^ ":" ^ loc else "at " ^ loc - val head = full_loc ^ " (" ^ name ^ "):" + val head = "at " ^ loc ^ " (" ^ name ^ "):" fun pretty_msg (name, msg) = Pretty.block (map Pretty.str [name, ": ", msg]) in @@ -119,7 +111,7 @@ Actions.get thy |> Symtab.dest |> only_within_range thy pos (map_filter (apply_action (verb, secs) st)) - |> (fn [] => () | msgs => log thy (pretty_print verb pos name msgs)) + |> (fn [] => () | msgs => log thy (pretty_print pos name msgs)) end end diff -r 030be5c12d96 -r 016134424f71 src/HOL/Tools/Mirabelle/lib/Tools/mirabelle --- a/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle Thu Aug 27 11:54:17 2009 +0200 @@ -7,15 +7,17 @@ PRG="$(basename "$0")" -function action_names() { +function print_action_names() { TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML" - ACTION_NAMES=`find $TOOLS | sed 's/.*mirabelle_$.*$\.ML/\1/'` + for NAME in $TOOLS + do + echo $NAME | sed 's/.*mirabelle_$.*$\.ML/ \1/' + done } function usage() { out="$MIRABELLE_OUTPUT_PATH" timeout="$MIRABELLE_TIMEOUT" - action_names echo echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES" echo @@ -31,14 +33,11 @@ echo echo " ACTIONS is a colon-separated list of actions, where each action is" echo " either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:" - for NAME in $ACTION_NAMES - do - echo " $NAME" - done + print_action_names echo - echo " FILES is a space-separated list of theory files, where each file is" - echo " either NAME.thy or NAME.thy[START:END] and START and END are numbers" - echo " indicating the range the given actions are to be applied." + echo " FILES is a list of theory files, where each file is either NAME.thy" + echo " or NAME.thy[START:END] and START and END are numbers indicating the" + echo " range the given actions are to be applied." echo exit 1 } @@ -48,7 +47,7 @@ # options -while getopts "L:T:O:vt:" OPT +while getopts "L:T:O:vt:?" OPT do case "$OPT" in L) @@ -61,7 +60,7 @@ MIRABELLE_OUTPUT_PATH="$OPTARG" ;; v) - MIRABELLE_VERBOSE=true + MIRABELLE_VERBOSE="true" ;; t) MIRABELLE_TIMEOUT="$OPTARG" @@ -81,13 +80,13 @@ # setup -mkdir -p $MIRABELLE_OUTPUT_PATH +mkdir -p "$MIRABELLE_OUTPUT_PATH" ## main for FILE in "$@" do - perl -w $MIRABELLE_HOME/lib/scripts/mirabelle.pl $ACTIONS "$FILE" + perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE" done diff -r 030be5c12d96 -r 016134424f71 src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl --- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl Thu Aug 27 11:54:17 2009 +0200 @@ -43,9 +43,11 @@ my $log_file = $output_path . "/" . $thy_name . ".log"; my @action_files; +my @action_names; foreach (split(/:/, $actions)) { if (m/([^[]*)/) { push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\""; + push @action_names, $1; } } my $tools = ""; @@ -62,7 +64,7 @@ begin setup {* - Mirabelle.set_logfile "$log_file" #> + Config.put_thy Mirabelle.logfile "$log_file" #> Config.put_thy Mirabelle.timeout $timeout #> Config.put_thy Mirabelle.verbose $verbose #> Config.put_thy Mirabelle.start_line $start_line #> @@ -99,7 +101,8 @@ my $thy_text = join("", @lines); my $old_len = length($thy_text); -$thy_text =~ s/\btheory\b[^\n]*\s*\bimports\s/theory $new_thy_name\nimports "$setup_thy_name" /gm; +$thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g; +$thy_text =~ s/(imports)(\s+)/$1 "$setup_thy_name"$2/g; die "No 'imports' found" if length($thy_text) == $old_len; open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'"; @@ -114,14 +117,21 @@ # run isabelle -my $r = system "$isabelle_home/bin/isabelle-process " . +open(LOG_FILE, ">$log_file"); +print LOG_FILE "Run of $new_thy_file with:\n"; +foreach $name (@action_names) { + print LOG_FILE " $name\n"; +} +print LOG_FILE "\n\n"; +close(LOG_FILE); + +my $r = system "\"$ISABELLE_PROCESS\" " . "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n"; # cleanup unlink $root_file; -unlink $new_thy_file; unlink $setup_file; exit $r; diff -r 030be5c12d96 -r 016134424f71 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Thu Aug 27 11:54:17 2009 +0200 @@ -246,8 +246,10 @@ RS eq_reflection end; -fun is_intrel (b$_$_) = domain_type (fastype_of b) = HOLogic.intT - | is_intrel (@{term "Not"}$(b$_$_)) = domain_type (fastype_of b) = HOLogic.intT +fun is_intrel_type T = T = @{typ "int => int => bool"}; + +fun is_intrel (b$_$_) = is_intrel_type (fastype_of b) + | is_intrel (@{term "Not"}$(b$_$_)) = is_intrel_type (fastype_of b) | is_intrel _ = false; fun linearize_conv ctxt vs ct = case term_of ct of diff -r 030be5c12d96 -r 016134424f71 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Thu Aug 27 11:54:17 2009 +0200 @@ -99,4 +99,33 @@ values 20 "{(n, m). tranclp succ n m}" *) +subsection{* CCS *} + +text{* This example formalizes finite CCS processes without communication or +recursion. For simplicity, labels are natural numbers. *} + +datatype proc = nil | pre nat proc | or proc proc | par proc proc + +inductive step :: "proc \ nat \ proc \ bool" where +"step (pre n p) n p" | +"step p1 a q \ step (or p1 p2) a q" | +"step p2 a q \ step (or p1 p2) a q" | +"step p1 a q \ step (par p1 p2) a (par q p2)" | +"step p2 a q \ step (par p1 p2) a (par p1 q)" + +code_pred step . + +inductive steps where +"steps p [] p" | +"step p a q \ steps q as r \ steps p (a#as) r" + +code_pred steps . + +values 5 + "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}" + +(* FIXME +values 3 "{(a,q). step (par nil nil) a q}" +*) + end \ No newline at end of file diff -r 030be5c12d96 -r 016134424f71 src/HOL/ex/Termination.thy --- a/src/HOL/ex/Termination.thy Thu Aug 27 11:54:05 2009 +0200 +++ b/src/HOL/ex/Termination.thy Thu Aug 27 11:54:17 2009 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/ex/Termination.thy - ID: $Id$ Author: Lukas Bulwahn, TU Muenchen Author: Alexander Krauss, TU Muenchen *) @@ -10,12 +9,33 @@ imports Main Multiset begin +subsection {* Manually giving termination relations using @{text relation} and +@{term measure} *} + +function sum :: "nat \ nat \ nat" +where + "sum i N = (if i > N then 0 else i + sum (Suc i) N)" +by pat_completeness auto + +termination by (relation "measure (\(i,N). N + 1 - i)") auto + +function foo :: "nat \ nat \ nat" +where + "foo i N = (if i > N + then (if N = 0 then 0 else foo 0 (N - 1)) + else i + foo (Suc i) N)" +by pat_completeness auto + +termination by (relation "measures [\(i, N). N, \(i,N). N + 1 - i]") auto + + +subsection {* @{text lexicographic_order}: Trivial examples *} + text {* - The @{text fun} command uses the method @{text lexicographic_order} by default. + The @{text fun} command uses the method @{text lexicographic_order} by default, + so it is not explicitly invoked. *} -subsection {* Trivial examples *} - fun identity :: "nat \ nat" where "identity n = n" diff -r 030be5c12d96 -r 016134424f71 src/Tools/more_conv.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/more_conv.ML Thu Aug 27 11:54:17 2009 +0200 @@ -0,0 +1,61 @@ +(* Title: Tools/more_conv.ML + Author: Sascha Boehme + +Further conversions and conversionals. +*) + +signature MORE_CONV = +sig + val rewrs_conv: thm list -> conv + + val sub_conv: (Proof.context -> conv) -> Proof.context -> conv + val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv + val top_conv: (Proof.context -> conv) -> Proof.context -> conv + val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv + + val binder_conv: (Proof.context -> conv) -> Proof.context -> conv + + val cache_conv: conv -> conv +end + + + +structure More_Conv : MORE_CONV = +struct + + +fun rewrs_conv eqs = Conv.first_conv (map Conv.rewr_conv eqs) + + +fun sub_conv conv ctxt = + Conv.comb_conv (conv ctxt) else_conv + Conv.abs_conv (fn (_, cx) => conv cx) ctxt else_conv + Conv.all_conv + +fun bottom_conv conv ctxt ct = + (sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct + +fun top_conv conv ctxt ct = + (conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct + +fun top_sweep_conv conv ctxt ct = + (conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct + + +fun binder_conv cv ctxt = + Conv.arg_conv (Conv.abs_conv (fn (_, cx) => cv cx) ctxt) + + +fun cache_conv conv = + let + val tab = ref Termtab.empty + fun add_result t thm = + let val _ = change tab (Termtab.insert Thm.eq_thm (t, thm)) + in thm end + fun cconv ct = + (case Termtab.lookup (!tab) (Thm.term_of ct) of + SOME thm => thm + | NONE => add_result (Thm.term_of ct) (conv ct)) + in cconv end + +end