eliminated OldGoals.inst;
authorwenzelm
Mon Jun 16 17:54:35 2008 +0200 (2008-06-16)
changeset 27225b316dde851f5
parent 27224 ac158759125c
child 27226 5a3e5e46d977
eliminated OldGoals.inst;
doc-src/TutorialI/Protocol/Event.thy
doc-src/TutorialI/Protocol/Message.thy
src/HOL/Auth/Event.thy
src/HOL/Auth/Message.thy
src/HOL/Real/rat_arith.ML
src/HOL/SET-Protocol/EventSET.thy
src/HOL/SET-Protocol/MessageSET.thy
     1.1 --- a/doc-src/TutorialI/Protocol/Event.thy	Mon Jun 16 14:18:55 2008 +0200
     1.2 +++ b/doc-src/TutorialI/Protocol/Event.thy	Mon Jun 16 17:54:35 2008 +0200
     1.3 @@ -258,19 +258,16 @@
     1.4         knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
     1.5         knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
     1.6  
     1.7 +lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
     1.8 +
     1.9  ML
    1.10  {*
    1.11  val analz_mono_contra_tac = 
    1.12 -  let val analz_impI = OldGoals.inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
    1.13 -  in
    1.14 -    rtac analz_impI THEN' 
    1.15 -    REPEAT1 o 
    1.16 -      (dresolve_tac (thms"analz_mono_contra"))
    1.17 -    THEN' mp_tac
    1.18 -  end
    1.19 +  rtac @{thm analz_impI} THEN' 
    1.20 +  REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
    1.21 +  THEN' mp_tac
    1.22  *}
    1.23  
    1.24 -
    1.25  lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
    1.26  by (induct e, auto simp: knows_Cons)
    1.27  
    1.28 @@ -295,6 +292,8 @@
    1.29  
    1.30  subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
    1.31  
    1.32 +lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))", standard]
    1.33 +
    1.34  ML
    1.35  {*
    1.36  val knows_Cons     = thm "knows_Cons"
    1.37 @@ -334,17 +333,14 @@
    1.38  
    1.39  
    1.40  val synth_analz_mono_contra_tac = 
    1.41 -  let val syan_impI = OldGoals.inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
    1.42 -  in
    1.43 -    rtac syan_impI THEN' 
    1.44 -    REPEAT1 o 
    1.45 -      (dresolve_tac 
    1.46 -       [knows_Spy_subset_knows_Spy_Says RS synth_analz_mono RS contra_subsetD,
    1.47 -        knows_Spy_subset_knows_Spy_Notes RS synth_analz_mono RS contra_subsetD,
    1.48 -	knows_Spy_subset_knows_Spy_Gets RS synth_analz_mono RS contra_subsetD])
    1.49 -    THEN'
    1.50 -    mp_tac
    1.51 -  end;
    1.52 +  rtac @{thm syan_impI} THEN'
    1.53 +  REPEAT1 o 
    1.54 +    (dresolve_tac 
    1.55 +     [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    1.56 +      @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    1.57 +      @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
    1.58 +  THEN'
    1.59 +  mp_tac
    1.60  *}
    1.61  
    1.62  method_setup synth_analz_mono_contra = {*
     2.1 --- a/doc-src/TutorialI/Protocol/Message.thy	Mon Jun 16 14:18:55 2008 +0200
     2.2 +++ b/doc-src/TutorialI/Protocol/Message.thy	Mon Jun 16 17:54:35 2008 +0200
     2.3 @@ -787,20 +787,22 @@
     2.4  
     2.5  text{*Rewrites to push in Key and Crypt messages, so that other messages can
     2.6      be pulled out using the @{text analz_insert} rules*}
     2.7 -ML
     2.8 -{*
     2.9 -fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute);
    2.10  
    2.11 -bind_thms ("pushKeys",
    2.12 -           map (insComm "Key ?K") 
    2.13 -                   ["Agent ?C", "Nonce ?N", "Number ?N", 
    2.14 -		    "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]);
    2.15 +lemmas pushKeys [standard] =
    2.16 +  insert_commute [of "Key K" "Agent C"]
    2.17 +  insert_commute [of "Key K" "Nonce N"]
    2.18 +  insert_commute [of "Key K" "Number N"]
    2.19 +  insert_commute [of "Key K" "Hash X"]
    2.20 +  insert_commute [of "Key K" "MPair X Y"]
    2.21 +  insert_commute [of "Key K" "Crypt X K'"]
    2.22  
    2.23 -bind_thms ("pushCrypts",
    2.24 -           map (insComm "Crypt ?X ?K") 
    2.25 -                     ["Agent ?C", "Nonce ?N", "Number ?N", 
    2.26 -		      "Hash ?X'", "MPair ?X' ?Y"]);
    2.27 -*}
    2.28 +lemmas pushCrypts [standard] =
    2.29 +  insert_commute [of "Crypt X K" "Agent C"]
    2.30 +  insert_commute [of "Crypt X K" "Agent C"]
    2.31 +  insert_commute [of "Crypt X K" "Nonce N"]
    2.32 +  insert_commute [of "Crypt X K" "Number N"]
    2.33 +  insert_commute [of "Crypt X K" "Hash X'"]
    2.34 +  insert_commute [of "Crypt X K" "MPair X' Y"]
    2.35  
    2.36  text{*Cannot be added with @{text "[simp]"} -- messages should not always be
    2.37    re-ordered. *}
     3.1 --- a/src/HOL/Auth/Event.thy	Mon Jun 16 14:18:55 2008 +0200
     3.2 +++ b/src/HOL/Auth/Event.thy	Mon Jun 16 17:54:35 2008 +0200
     3.3 @@ -278,16 +278,14 @@
     3.4      intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
     3.5  
     3.6  
     3.7 +lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
     3.8 +
     3.9  ML
    3.10  {*
    3.11  val analz_mono_contra_tac = 
    3.12 -  let val analz_impI = OldGoals.inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
    3.13 -  in
    3.14 -    rtac analz_impI THEN' 
    3.15 -    REPEAT1 o 
    3.16 -      (dresolve_tac @{thms analz_mono_contra})
    3.17 -    THEN' mp_tac
    3.18 -  end
    3.19 +  rtac @{thm analz_impI} THEN' 
    3.20 +  REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
    3.21 +  THEN' mp_tac
    3.22  *}
    3.23  
    3.24  method_setup analz_mono_contra = {*
    3.25 @@ -296,20 +294,19 @@
    3.26  
    3.27  subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
    3.28  
    3.29 +lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))", standard]
    3.30 +
    3.31  ML
    3.32  {*
    3.33  val synth_analz_mono_contra_tac = 
    3.34 -  let val syan_impI = OldGoals.inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
    3.35 -  in
    3.36 -    rtac syan_impI THEN' 
    3.37 -    REPEAT1 o 
    3.38 -      (dresolve_tac 
    3.39 -       [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    3.40 -       @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    3.41 -       @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
    3.42 -    THEN'
    3.43 -    mp_tac
    3.44 -  end;
    3.45 +  rtac @{thm syan_impI} THEN'
    3.46 +  REPEAT1 o 
    3.47 +    (dresolve_tac 
    3.48 +     [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    3.49 +      @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    3.50 +      @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
    3.51 +  THEN'
    3.52 +  mp_tac
    3.53  *}
    3.54  
    3.55  method_setup synth_analz_mono_contra = {*
     4.1 --- a/src/HOL/Auth/Message.thy	Mon Jun 16 14:18:55 2008 +0200
     4.2 +++ b/src/HOL/Auth/Message.thy	Mon Jun 16 17:54:35 2008 +0200
     4.3 @@ -819,20 +819,22 @@
     4.4  
     4.5  text{*Rewrites to push in Key and Crypt messages, so that other messages can
     4.6      be pulled out using the @{text analz_insert} rules*}
     4.7 -ML
     4.8 -{*
     4.9 -fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute);
    4.10  
    4.11 -bind_thms ("pushKeys",
    4.12 -           map (insComm "Key ?K") 
    4.13 -                   ["Agent ?C", "Nonce ?N", "Number ?N", 
    4.14 -		    "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]);
    4.15 +lemmas pushKeys [standard] =
    4.16 +  insert_commute [of "Key K" "Agent C"]
    4.17 +  insert_commute [of "Key K" "Nonce N"]
    4.18 +  insert_commute [of "Key K" "Number N"]
    4.19 +  insert_commute [of "Key K" "Hash X"]
    4.20 +  insert_commute [of "Key K" "MPair X Y"]
    4.21 +  insert_commute [of "Key K" "Crypt X K'"]
    4.22  
    4.23 -bind_thms ("pushCrypts",
    4.24 -           map (insComm "Crypt ?X ?K") 
    4.25 -                     ["Agent ?C", "Nonce ?N", "Number ?N", 
    4.26 -		      "Hash ?X'", "MPair ?X' ?Y"]);
    4.27 -*}
    4.28 +lemmas pushCrypts [standard] =
    4.29 +  insert_commute [of "Crypt X K" "Agent C"]
    4.30 +  insert_commute [of "Crypt X K" "Agent C"]
    4.31 +  insert_commute [of "Crypt X K" "Nonce N"]
    4.32 +  insert_commute [of "Crypt X K" "Number N"]
    4.33 +  insert_commute [of "Crypt X K" "Hash X'"]
    4.34 +  insert_commute [of "Crypt X K" "MPair X' Y"]
    4.35  
    4.36  text{*Cannot be added with @{text "[simp]"} -- messages should not always be
    4.37    re-ordered. *}
     5.1 --- a/src/HOL/Real/rat_arith.ML	Mon Jun 16 14:18:55 2008 +0200
     5.2 +++ b/src/HOL/Real/rat_arith.ML	Mon Jun 16 17:54:35 2008 +0200
     5.3 @@ -12,14 +12,15 @@
     5.4  
     5.5  val simprocs = field_cancel_numeral_factors
     5.6  
     5.7 -val simps = [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
     5.8 -             OldGoals.inst "a" "(number_of ?v)" @{thm right_distrib},
     5.9 -             @{thm divide_1}, @{thm divide_zero_left},
    5.10 -             @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
    5.11 -             @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
    5.12 -             @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
    5.13 -             @{thm of_int_minus}, @{thm of_int_diff},
    5.14 -             @{thm of_int_mult}, @{thm of_int_of_nat_eq}]
    5.15 +val simps =
    5.16 + [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
    5.17 +  RuleInsts.read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
    5.18 +  @{thm divide_1}, @{thm divide_zero_left},
    5.19 +  @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
    5.20 +  @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
    5.21 +  @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
    5.22 +  @{thm of_int_minus}, @{thm of_int_diff},
    5.23 +  @{thm of_int_mult}, @{thm of_int_of_nat_eq}]
    5.24  
    5.25  val nat_inj_thms = [@{thm of_nat_le_iff} RS iffD2,
    5.26                      @{thm of_nat_eq_iff} RS iffD2]
     6.1 --- a/src/HOL/SET-Protocol/EventSET.thy	Mon Jun 16 14:18:55 2008 +0200
     6.2 +++ b/src/HOL/SET-Protocol/EventSET.thy	Mon Jun 16 17:54:35 2008 +0200
     6.3 @@ -177,14 +177,15 @@
     6.4         knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD]
     6.5         knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
     6.6         knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
     6.7 +
     6.8 +lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
     6.9 +
    6.10  ML
    6.11  {*
    6.12  val analz_mono_contra_tac = 
    6.13 -  let val analz_impI = OldGoals.inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
    6.14 -  in rtac analz_impI THEN' 
    6.15 -     REPEAT1 o (dresolve_tac @{thms analz_mono_contra}) THEN'
    6.16 -     mp_tac
    6.17 -  end
    6.18 +  rtac @{thm analz_impI} THEN' 
    6.19 +  REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
    6.20 +  THEN' mp_tac
    6.21  *}
    6.22  
    6.23  method_setup analz_mono_contra = {*
     7.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Mon Jun 16 14:18:55 2008 +0200
     7.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Mon Jun 16 17:54:35 2008 +0200
     7.3 @@ -813,20 +813,23 @@
     7.4  
     7.5  text{*Rewrites to push in Key and Crypt messages, so that other messages can
     7.6      be pulled out using the @{text analz_insert} rules*}
     7.7 -ML
     7.8 -{*
     7.9 -fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute);
    7.10  
    7.11 -bind_thms ("pushKeys",
    7.12 -           map (insComm "Key ?K")
    7.13 -                   ["Agent ?C", "Nonce ?N", "Number ?N", "Pan ?PAN",
    7.14 -		    "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]);
    7.15 +lemmas pushKeys [standard] =
    7.16 +  insert_commute [of "Key K" "Agent C"]
    7.17 +  insert_commute [of "Key K" "Nonce N"]
    7.18 +  insert_commute [of "Key K" "Number N"]
    7.19 +  insert_commute [of "Key K" "Pan PAN"]
    7.20 +  insert_commute [of "Key K" "Hash X"]
    7.21 +  insert_commute [of "Key K" "MPair X Y"]
    7.22 +  insert_commute [of "Key K" "Crypt X K'"]
    7.23  
    7.24 -bind_thms ("pushCrypts",
    7.25 -           map (insComm "Crypt ?X ?K")
    7.26 -                     ["Agent ?C", "Nonce ?N", "Number ?N", "Pan ?PAN",
    7.27 -		      "Hash ?X'", "MPair ?X' ?Y"]);
    7.28 -*}
    7.29 +lemmas pushCrypts [standard] =
    7.30 +  insert_commute [of "Crypt X K" "Agent C"]
    7.31 +  insert_commute [of "Crypt X K" "Nonce N"]
    7.32 +  insert_commute [of "Crypt X K" "Number N"]
    7.33 +  insert_commute [of "Crypt X K" "Pan PAN"]
    7.34 +  insert_commute [of "Crypt X K" "Hash X'"]
    7.35 +  insert_commute [of "Crypt X K" "MPair X' Y"]
    7.36  
    7.37  text{*Cannot be added with @{text "[simp]"} -- messages should not always be
    7.38    re-ordered.*}