# 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 \<notin> analz (knows Spy evs)", standard]
+
 ML
 {*
 val analz_mono_contra_tac = 
-  let val analz_impI = OldGoals.inst "P" "?Y \<notin> 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 \<subseteq> 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 \<notin> 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 \<notin> 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 \<notin> analz (knows Spy evs)", standard]
+
 ML
 {*
 val analz_mono_contra_tac = 
-  let val analz_impI = OldGoals.inst "P" "?Y \<notin> 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 \<notin> synth (analz (knows Spy evs))", standard]
+
 ML
 {*
 val synth_analz_mono_contra_tac = 
-  let val syan_impI = OldGoals.inst "P" "?Y \<notin> 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 \<notin> analz (knows Spy evs)", standard]
+
 ML
 {*
 val analz_mono_contra_tac = 
-  let val analz_impI = OldGoals.inst "P" "?Y \<notin> 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.*}