# HG changeset patch # User paulson # Date 1136299479 -3600 # Node ID 60a0f9caa0a2c51663ef654216e01adf50e9a495 # Parent dc39832e928096e4c29a7bf3499ed340b437feff Provers/classical: stricter checks to ensure that supplied intro, dest and elim rules are well-formed diff -r dc39832e9280 -r 60a0f9caa0a2 NEWS --- 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 diff -r dc39832e9280 -r 60a0f9caa0a2 src/HOL/Auth/Guard/Extensions.thy --- 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) diff -r dc39832e9280 -r 60a0f9caa0a2 src/HOL/IMP/Transition.thy --- 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!]: "\s\ -n\\<^sub>1 y = (n = 0 \ y = \s\)" +lemma evalc1_None_0 [simp]: "\s\ -n\\<^sub>1 y = (n = 0 \ y = \s\)" by (cases n) auto lemma SKIP_n: "\\, s\ -n\\<^sub>1 \s'\ \ s' = s \ n=1" diff -r dc39832e9280 -r 60a0f9caa0a2 src/HOL/Lambda/Eta.thy --- 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' \\<^sub>\ 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' \\<^sub>\ q''" and "r => t''" and "t'' \\<^sub>\ 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' \\<^sub>\ q''" and "r => t''" and "t'' \\<^sub>\ 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' \\<^sub>\ 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 diff -r dc39832e9280 -r 60a0f9caa0a2 src/Provers/classical.ML --- 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,