# HG changeset patch # User wenzelm # Date 1213631675 -7200 # Node ID b316dde851f52ea9fe526c17083254b9c13968c8 # Parent ac158759125cb7e5e976a71e6d48321216e373de eliminated OldGoals.inst; diff -r ac158759125c -r b316dde851f5 doc-src/TutorialI/Protocol/Event.thy --- a/doc-src/TutorialI/Protocol/Event.thy Mon Jun 16 14:18:55 2008 +0200 +++ b/doc-src/TutorialI/Protocol/Event.thy Mon Jun 16 17:54:35 2008 +0200 @@ -258,19 +258,16 @@ knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD] knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD] +lemmas analz_impI = impI [where P = "Y \ analz (knows Spy evs)", standard] + ML {* val analz_mono_contra_tac = - let val analz_impI = OldGoals.inst "P" "?Y \ analz (knows Spy ?evs)" impI - in - rtac analz_impI THEN' - REPEAT1 o - (dresolve_tac (thms"analz_mono_contra")) - THEN' mp_tac - end + rtac @{thm analz_impI} THEN' + REPEAT1 o (dresolve_tac @{thms analz_mono_contra}) + THEN' mp_tac *} - lemma knows_subset_knows_Cons: "knows A evs \ knows A (e # evs)" by (induct e, auto simp: knows_Cons) @@ -295,6 +292,8 @@ subsubsection{*Useful for case analysis on whether a hash is a spoof or not*} +lemmas syan_impI = impI [where P = "Y \ synth (analz (knows Spy evs))", standard] + ML {* val knows_Cons = thm "knows_Cons" @@ -334,17 +333,14 @@ val synth_analz_mono_contra_tac = - let val syan_impI = OldGoals.inst "P" "?Y \ synth (analz (knows Spy ?evs))" impI - in - rtac syan_impI THEN' - REPEAT1 o - (dresolve_tac - [knows_Spy_subset_knows_Spy_Says RS synth_analz_mono RS contra_subsetD, - knows_Spy_subset_knows_Spy_Notes RS synth_analz_mono RS contra_subsetD, - knows_Spy_subset_knows_Spy_Gets RS synth_analz_mono RS contra_subsetD]) - THEN' - mp_tac - end; + rtac @{thm syan_impI} THEN' + REPEAT1 o + (dresolve_tac + [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}, + @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}, + @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}]) + THEN' + mp_tac *} method_setup synth_analz_mono_contra = {* diff -r ac158759125c -r b316dde851f5 doc-src/TutorialI/Protocol/Message.thy --- a/doc-src/TutorialI/Protocol/Message.thy Mon Jun 16 14:18:55 2008 +0200 +++ b/doc-src/TutorialI/Protocol/Message.thy Mon Jun 16 17:54:35 2008 +0200 @@ -787,20 +787,22 @@ text{*Rewrites to push in Key and Crypt messages, so that other messages can be pulled out using the @{text analz_insert} rules*} -ML -{* -fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute); -bind_thms ("pushKeys", - map (insComm "Key ?K") - ["Agent ?C", "Nonce ?N", "Number ?N", - "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]); +lemmas pushKeys [standard] = + insert_commute [of "Key K" "Agent C"] + insert_commute [of "Key K" "Nonce N"] + insert_commute [of "Key K" "Number N"] + insert_commute [of "Key K" "Hash X"] + insert_commute [of "Key K" "MPair X Y"] + insert_commute [of "Key K" "Crypt X K'"] -bind_thms ("pushCrypts", - map (insComm "Crypt ?X ?K") - ["Agent ?C", "Nonce ?N", "Number ?N", - "Hash ?X'", "MPair ?X' ?Y"]); -*} +lemmas pushCrypts [standard] = + insert_commute [of "Crypt X K" "Agent C"] + insert_commute [of "Crypt X K" "Agent C"] + insert_commute [of "Crypt X K" "Nonce N"] + insert_commute [of "Crypt X K" "Number N"] + insert_commute [of "Crypt X K" "Hash X'"] + insert_commute [of "Crypt X K" "MPair X' Y"] text{*Cannot be added with @{text "[simp]"} -- messages should not always be re-ordered. *} diff -r ac158759125c -r b316dde851f5 src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Mon Jun 16 14:18:55 2008 +0200 +++ b/src/HOL/Auth/Event.thy Mon Jun 16 17:54:35 2008 +0200 @@ -278,16 +278,14 @@ intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD]) +lemmas analz_impI = impI [where P = "Y \ analz (knows Spy evs)", standard] + ML {* val analz_mono_contra_tac = - let val analz_impI = OldGoals.inst "P" "?Y \ analz (knows Spy ?evs)" impI - in - rtac analz_impI THEN' - REPEAT1 o - (dresolve_tac @{thms analz_mono_contra}) - THEN' mp_tac - end + rtac @{thm analz_impI} THEN' + REPEAT1 o (dresolve_tac @{thms analz_mono_contra}) + THEN' mp_tac *} method_setup analz_mono_contra = {* @@ -296,20 +294,19 @@ subsubsection{*Useful for case analysis on whether a hash is a spoof or not*} +lemmas syan_impI = impI [where P = "Y \ synth (analz (knows Spy evs))", standard] + ML {* val synth_analz_mono_contra_tac = - let val syan_impI = OldGoals.inst "P" "?Y \ synth (analz (knows Spy ?evs))" impI - in - rtac syan_impI THEN' - REPEAT1 o - (dresolve_tac - [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}, - @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}, - @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}]) - THEN' - mp_tac - end; + rtac @{thm syan_impI} THEN' + REPEAT1 o + (dresolve_tac + [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}, + @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}, + @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}]) + THEN' + mp_tac *} method_setup synth_analz_mono_contra = {* diff -r ac158759125c -r b316dde851f5 src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Mon Jun 16 14:18:55 2008 +0200 +++ b/src/HOL/Auth/Message.thy Mon Jun 16 17:54:35 2008 +0200 @@ -819,20 +819,22 @@ text{*Rewrites to push in Key and Crypt messages, so that other messages can be pulled out using the @{text analz_insert} rules*} -ML -{* -fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute); -bind_thms ("pushKeys", - map (insComm "Key ?K") - ["Agent ?C", "Nonce ?N", "Number ?N", - "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]); +lemmas pushKeys [standard] = + insert_commute [of "Key K" "Agent C"] + insert_commute [of "Key K" "Nonce N"] + insert_commute [of "Key K" "Number N"] + insert_commute [of "Key K" "Hash X"] + insert_commute [of "Key K" "MPair X Y"] + insert_commute [of "Key K" "Crypt X K'"] -bind_thms ("pushCrypts", - map (insComm "Crypt ?X ?K") - ["Agent ?C", "Nonce ?N", "Number ?N", - "Hash ?X'", "MPair ?X' ?Y"]); -*} +lemmas pushCrypts [standard] = + insert_commute [of "Crypt X K" "Agent C"] + insert_commute [of "Crypt X K" "Agent C"] + insert_commute [of "Crypt X K" "Nonce N"] + insert_commute [of "Crypt X K" "Number N"] + insert_commute [of "Crypt X K" "Hash X'"] + insert_commute [of "Crypt X K" "MPair X' Y"] text{*Cannot be added with @{text "[simp]"} -- messages should not always be re-ordered. *} diff -r ac158759125c -r b316dde851f5 src/HOL/Real/rat_arith.ML --- a/src/HOL/Real/rat_arith.ML Mon Jun 16 14:18:55 2008 +0200 +++ b/src/HOL/Real/rat_arith.ML Mon Jun 16 17:54:35 2008 +0200 @@ -12,14 +12,15 @@ val simprocs = field_cancel_numeral_factors -val simps = [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals}, - OldGoals.inst "a" "(number_of ?v)" @{thm right_distrib}, - @{thm divide_1}, @{thm divide_zero_left}, - @{thm times_divide_eq_right}, @{thm times_divide_eq_left}, - @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, - @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add}, - @{thm of_int_minus}, @{thm of_int_diff}, - @{thm of_int_mult}, @{thm of_int_of_nat_eq}] +val simps = + [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals}, + RuleInsts.read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib}, + @{thm divide_1}, @{thm divide_zero_left}, + @{thm times_divide_eq_right}, @{thm times_divide_eq_left}, + @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, + @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add}, + @{thm of_int_minus}, @{thm of_int_diff}, + @{thm of_int_mult}, @{thm of_int_of_nat_eq}] val nat_inj_thms = [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2] diff -r ac158759125c -r b316dde851f5 src/HOL/SET-Protocol/EventSET.thy --- a/src/HOL/SET-Protocol/EventSET.thy Mon Jun 16 14:18:55 2008 +0200 +++ b/src/HOL/SET-Protocol/EventSET.thy Mon Jun 16 17:54:35 2008 +0200 @@ -177,14 +177,15 @@ knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD] knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD] knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD] + +lemmas analz_impI = impI [where P = "Y \ analz (knows Spy evs)", standard] + ML {* val analz_mono_contra_tac = - let val analz_impI = OldGoals.inst "P" "?Y \ analz (knows Spy ?evs)" impI - in rtac analz_impI THEN' - REPEAT1 o (dresolve_tac @{thms analz_mono_contra}) THEN' - mp_tac - end + rtac @{thm analz_impI} THEN' + REPEAT1 o (dresolve_tac @{thms analz_mono_contra}) + THEN' mp_tac *} method_setup analz_mono_contra = {* diff -r ac158759125c -r b316dde851f5 src/HOL/SET-Protocol/MessageSET.thy --- a/src/HOL/SET-Protocol/MessageSET.thy Mon Jun 16 14:18:55 2008 +0200 +++ b/src/HOL/SET-Protocol/MessageSET.thy Mon Jun 16 17:54:35 2008 +0200 @@ -813,20 +813,23 @@ text{*Rewrites to push in Key and Crypt messages, so that other messages can be pulled out using the @{text analz_insert} rules*} -ML -{* -fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute); -bind_thms ("pushKeys", - map (insComm "Key ?K") - ["Agent ?C", "Nonce ?N", "Number ?N", "Pan ?PAN", - "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]); +lemmas pushKeys [standard] = + insert_commute [of "Key K" "Agent C"] + insert_commute [of "Key K" "Nonce N"] + insert_commute [of "Key K" "Number N"] + insert_commute [of "Key K" "Pan PAN"] + insert_commute [of "Key K" "Hash X"] + insert_commute [of "Key K" "MPair X Y"] + insert_commute [of "Key K" "Crypt X K'"] -bind_thms ("pushCrypts", - map (insComm "Crypt ?X ?K") - ["Agent ?C", "Nonce ?N", "Number ?N", "Pan ?PAN", - "Hash ?X'", "MPair ?X' ?Y"]); -*} +lemmas pushCrypts [standard] = + insert_commute [of "Crypt X K" "Agent C"] + insert_commute [of "Crypt X K" "Nonce N"] + insert_commute [of "Crypt X K" "Number N"] + insert_commute [of "Crypt X K" "Pan PAN"] + insert_commute [of "Crypt X K" "Hash X'"] + insert_commute [of "Crypt X K" "MPair X' Y"] text{*Cannot be added with @{text "[simp]"} -- messages should not always be re-ordered.*}