Provers/classical: stricter checks to ensure that supplied intro, dest and
elim rules are well-formed

--- a/NEWS	Tue Jan 03 15:43:54 2006 +0100
+++ b/NEWS	Tue Jan 03 15:44:39 2006 +0100
@@ -189,6 +189,9 @@
 attribute; classical elim/dest rules are now treated uniformly when
 manipulating the claset.
 
+* Provers/classical: stricter checks to ensure that supplied intro, dest and 
+elim rules are well-formed; dest and elim rules must have at least one premise.
+
 * Syntax: input syntax now supports dummy variable binding "%_. b",
 where the body does not mention the bound variable.  Note that dummy
 patterns implicitly depend on their context of bounds, which makes

--- a/src/HOL/Auth/Guard/Extensions.thy	Tue Jan 03 15:43:54 2006 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy	Tue Jan 03 15:44:39 2006 +0100
@@ -11,7 +11,7 @@
 
 header {*Extensions to Standard Theories*}
 
-theory Extensions imports Event begin
+theory Extensions imports "../Event" begin
 
 subsection{*Extensions to Theory @{text Set}*}
 
@@ -279,8 +279,8 @@
 analz (G Un H) = H - keysfor G Un (analz (G Un (H Int keysfor G)))"
 apply (rule eq)
 apply (erule analz.induct, blast)
-apply (simp, blast dest: Un_upper1)
-apply (simp, blast dest: Un_upper2)
+apply (simp, blast)
+apply (simp, blast)
 apply (case_tac "Key (invKey K):H - keysfor G", clarsimp)
 apply (drule_tac X=X in no_key_no_Crypt)
 by (auto intro: analz_sub)
@@ -587,7 +587,7 @@
 
 lemma known_used [rule_format]: "[| evs:p; Gets_correct p; one_step p |]
 ==> X:parts (knows A evs) --> X:used evs"
-apply (case_tac "A=Spy", blast dest: parts_knows_Spy_subset_used)
+apply (case_tac "A=Spy", blast)
 apply (induct evs)
 apply (simp add: used.simps, blast)
 apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)
@@ -600,7 +600,7 @@
 lemma known_max_used [rule_format]: "[| evs:p; Gets_correct p; one_step p |]
 ==> X:parts (knows_max A evs) --> X:used evs"
 apply (case_tac "A=Spy")
-apply (simp, blast dest: parts_knows_Spy_subset_used)
+apply force
 apply (induct evs)
 apply (simp add: knows_max_def used.simps, blast)
 apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)

--- a/src/HOL/IMP/Transition.thy	Tue Jan 03 15:43:54 2006 +0100
+++ b/src/HOL/IMP/Transition.thy	Tue Jan 03 15:44:39 2006 +0100
@@ -208,7 +208,7 @@
 lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp
 lemmas [simp del] = relpow.simps
 (*>*)
-lemma evalc1_None_0 [simp, dest!]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
+lemma evalc1_None_0 [simp]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
   by (cases n) auto
 
 lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> n=1"

--- a/src/HOL/Lambda/Eta.thy	Tue Jan 03 15:43:54 2006 +0100
+++ b/src/HOL/Lambda/Eta.thy	Tue Jan 03 15:44:39 2006 +0100
@@ -407,7 +407,7 @@
       by (blast dest: par_eta_elim_abs)
     from abs have "size r' < size t" by simp
     with abs(2) rr obtain t' where rt: "r => t'" and t': "t' \<Rightarrow>\<^sub>\<eta> r''"
-      by (blast dest: less)
+      by (blast dest: less(1))
     with s abs show ?thesis
       by (auto intro: eta_expand_red eta_expand_eta)
   next
@@ -419,7 +419,7 @@
     from app have "size q' < size t" and "size r' < size t" by simp_all
     with app(2,3) qq rr obtain t' t'' where "q => t'" and
       "t' \<Rightarrow>\<^sub>\<eta> q''" and "r => t''" and "t'' \<Rightarrow>\<^sub>\<eta> r''"
-      by (blast dest: less)
+      by (blast dest: less(1))
     with s app show ?thesis
       by (fastsimp intro: eta_expand_red eta_expand_eta)
   next
@@ -431,7 +431,7 @@
     from beta have "size q' < size t" and "size r' < size t" by simp_all
     with beta(2,3) qq rr obtain t' t'' where "q => t'" and
       "t' \<Rightarrow>\<^sub>\<eta> q''" and "r => t''" and "t'' \<Rightarrow>\<^sub>\<eta> r''"
-      by (blast dest: less)
+      by (blast dest: less(1))
     with s beta show ?thesis
       by (auto intro: eta_expand_red eta_expand_beta eta_expand_eta par_eta_subst)
   qed
@@ -448,8 +448,8 @@
   case (2 s' s'' s''')
   from 2 obtain t' where s': "s' => t'" and t': "t' \<Rightarrow>\<^sub>\<eta> s'''"
     by (auto dest: par_eta_beta)
-  from s' obtain t'' where s: "s => t''" and t'': "t'' -e>> t'"
-    by (blast dest: 2)
+  from s' obtain t'' where s: "s => t''" and t'': "t'' -e>> t'" using 2
+    by blast
   from par_eta_subset_eta t' have "t' -e>> s'''" ..
   with t'' have "t'' -e>> s'''" by (rule rtrancl_trans)
   with s show ?case by iprover

--- a/src/Provers/classical.ML	Tue Jan 03 15:43:54 2006 +0100
+++ b/src/Provers/classical.ML	Tue Jan 03 15:44:39 2006 +0100
@@ -262,12 +262,8 @@
 fun dup_intr th = zero_var_indexes (th RS classical);
 
 fun dup_elim th =
-  (case try (fn () =>
     rule_by_tactic (TRYALL (etac revcut_rl))
-      ((th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd)) () of
-    SOME th' => th'
-  | _ => error ("Bad format for elimination rule\n" ^ string_of_thm th));
-
+      ((th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd);
 
 (**** Classical rule sets ****)
 
@@ -342,10 +338,10 @@
 (*For use with biresolve_tac.  Combines intro rules with swap to handle negated
   assumptions.  Pairs elim rules with true. *)
 fun joinrules (intrs, elims) =
-  (map (pair true) (elims @ swapify intrs) @ map (pair false) intrs);
+  (map (pair true) (elims @ swapify intrs)) @ map (pair false) intrs;
 
 fun joinrules' (intrs, elims) =
-  (map (pair true) elims @ map (pair false) intrs);
+  map (pair true) elims @ map (pair false) intrs;
 
 (*Priority: prefer rules with fewest subgoals,
   then rules added most recently (preferring the head of the list).*)
@@ -419,6 +415,8 @@
   if mem_thm (th, safeEs) then
          (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th);
           cs)
+  else if has_fewer_prems 1 th then
+    	error("Ill-formed elimination rule\n" ^ string_of_thm th)
   else
   let
       val th' = classical_rule th
@@ -445,6 +443,9 @@
 
 (*Give new theorem a name, if it has one already.*)
 fun name_make_elim th =
+    if has_fewer_prems 1 th then
+    	error("Ill-formed destruction rule\n" ^ string_of_thm th)
+    else
     case Thm.name_of_thm th of
         "" => Tactic.make_elim th
       | a  => Thm.name_thm (a ^ "_dest", Tactic.make_elim th);
@@ -475,7 +476,9 @@
         safe0_netpair = safe0_netpair,
         safep_netpair = safep_netpair,
         xtra_netpair = insert' 1 (nI,nE) ([th], []) xtra_netpair}
-  end;
+  end
+  handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
+         error ("Ill-formed introduction rule\n" ^ string_of_thm th);
 
 fun addE th
   (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
@@ -483,6 +486,8 @@
   if mem_thm (th, hazEs) then
          (warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th);
           cs)
+  else if has_fewer_prems 1 th then
+    	error("Ill-formed elimination rule\n" ^ string_of_thm th)
   else
   let
       val th' = classical_rule th
@@ -571,7 +576,10 @@
         safe0_netpair = safe0_netpair,
         safep_netpair = safep_netpair,
         xtra_netpair = delete' ([th], []) xtra_netpair}
- else cs;
+ else cs
+ handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
+        error ("Ill-formed introduction rule\n" ^ string_of_thm th);
+
 
 fun delE th
          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,