renamed rules to iprover
authornipkow
Thu Sep 22 23:56:15 2005 +0200 (2005-09-22)
changeset 1758958eeffd73be1
parent 17588 f2bd501398ee
child 17590 56dc95e8b5c5
renamed rules to iprover
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/AxSound.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/DefiniteAssignment.thy
src/HOL/Bali/DefiniteAssignmentCorrect.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Datatype_Universe.thy
src/HOL/Equiv_Relations.thy
src/HOL/Finite_Set.thy
src/HOL/FixedPoint.thy
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/Induct/PropLog.thy
src/HOL/Integ/Presburger.thy
src/HOL/Lambda/Commutation.thy
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/Type.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/List.thy
src/HOL/MicroJava/BV/EffectMono.thy
src/HOL/Nat.thy
src/HOL/Presburger.thy
src/HOL/Real/HahnBanach/HahnBanach.thy
src/HOL/Relation.thy
src/HOL/Set.thy
src/HOL/Transitive_Closure.thy
src/HOL/ex/Intuitionistic.thy
     1.1 --- a/src/HOL/Bali/AxCompl.thy	Thu Sep 22 23:55:42 2005 +0200
     1.2 +++ b/src/HOL/Bali/AxCompl.thy	Thu Sep 22 23:56:15 2005 +0200
     1.3 @@ -451,9 +451,9 @@
     1.4  	  proof -
     1.5  	    from eval_e wt_e da_e wf normal_s1
     1.6  	    have "nrm C \<subseteq>  dom (locals (store s1))"
     1.7 -	      by (cases rule: da_good_approxE') rules
     1.8 +	      by (cases rule: da_good_approxE') iprover
     1.9  	    with da_ps show ?thesis
    1.10 -	      by (rule da_weakenE) rules
    1.11 +	      by (rule da_weakenE) iprover
    1.12  	  qed
    1.13  	}
    1.14  	ultimately show ?thesis
    1.15 @@ -845,7 +845,7 @@
    1.16  	  show ?thesis
    1.17  	    by (rule eval_type_soundE)
    1.18  	qed
    1.19 -	ultimately show ?thesis by rules
    1.20 +	ultimately show ?thesis by iprover
    1.21        qed
    1.22      qed
    1.23    next
    1.24 @@ -1528,7 +1528,7 @@
    1.25      proof -
    1.26        from eval_t type_ok wf 
    1.27        obtain n where evaln: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y', s')"
    1.28 -	by (rule eval_to_evaln [elim_format]) rules
    1.29 +	by (rule eval_to_evaln [elim_format]) iprover
    1.30        from valid have 
    1.31  	valid_expanded:
    1.32  	"\<forall>n Y s Z. P Y s Z \<longrightarrow> type_ok G t s 
     2.1 --- a/src/HOL/Bali/AxSound.thy	Thu Sep 22 23:55:42 2005 +0200
     2.2 +++ b/src/HOL/Bali/AxSound.thy	Thu Sep 22 23:56:15 2005 +0200
     2.3 @@ -192,7 +192,7 @@
     2.4    from evaln have "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)"
     2.5      by (rule evaln_eval)
     2.6    from this wt da wf elim show P
     2.7 -    by (rule da_good_approxE') rules+
     2.8 +    by (rule da_good_approxE') iprover+
     2.9  qed
    2.10  
    2.11  lemma validI: 
    2.12 @@ -336,7 +336,7 @@
    2.13  proof -
    2.14    from evaln have "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" by (rule evaln_eval)
    2.15    from this hyps show ?thesis
    2.16 -    by (rule dom_locals_eval_mono_elim) rules+
    2.17 +    by (rule dom_locals_eval_mono_elim) iprover+
    2.18  qed
    2.19  
    2.20  
    2.21 @@ -616,7 +616,7 @@
    2.22  	proof -
    2.23  	  from eval_e1  wt_e1 da_e1 wf True
    2.24  	  have "nrm E1 \<subseteq> dom (locals (store s1))"
    2.25 -	    by (cases rule: da_good_approx_evalnE) rules
    2.26 +	    by (cases rule: da_good_approx_evalnE) iprover
    2.27  	  with da_e2 show ?thesis
    2.28  	    by (rule da_weakenE)
    2.29  	qed
    2.30 @@ -944,7 +944,7 @@
    2.31  	obtain E2 where
    2.32  	  da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) 
    2.33                     \<guillemotright>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<guillemotright> E2"
    2.34 -	  by (rule da_e2_BinOp [elim_format]) rules
    2.35 +	  by (rule da_e2_BinOp [elim_format]) iprover
    2.36  	from wt_e2 wt_Skip obtain T2 
    2.37  	  where "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
    2.38                    \<turnstile>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<Colon>T2"
    2.39 @@ -957,7 +957,7 @@
    2.40  	case False
    2.41  	note ve=validE [OF valid_e2,OF Q' valid_A conf_s1 eval_e2]
    2.42  	with False show ?thesis
    2.43 -	  by rules
    2.44 +	  by iprover
    2.45        qed
    2.46        with v have "R \<lfloor>v\<rfloor>\<^sub>e s2 Z"
    2.47  	by simp
    2.48 @@ -1068,7 +1068,7 @@
    2.49  	  proof -
    2.50  	    from eval_var wt_var da_var wf True
    2.51  	    have "nrm V \<subseteq>  dom (locals (store s1))"
    2.52 -	      by (cases rule: da_good_approx_evalnE) rules
    2.53 +	      by (cases rule: da_good_approx_evalnE) iprover
    2.54  	    with da_e show ?thesis
    2.55  	      by (rule da_weakenE) 
    2.56  	  qed
    2.57 @@ -1079,7 +1079,7 @@
    2.58  	  case False
    2.59  	  note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e]
    2.60  	  with False show ?thesis
    2.61 -	    by rules
    2.62 +	    by iprover
    2.63  	qed
    2.64  	with s3 show "R \<lfloor>v\<rfloor>\<^sub>e s3 Z"
    2.65  	  by simp
    2.66 @@ -1120,7 +1120,7 @@
    2.67  	  case False
    2.68  	  note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e]
    2.69  	  with False show ?thesis
    2.70 -	    by rules
    2.71 +	    by iprover
    2.72  	qed
    2.73  	with s3 show "R \<lfloor>v\<rfloor>\<^sub>e s3 Z"
    2.74  	  by simp
    2.75 @@ -1213,7 +1213,7 @@
    2.76  	case False
    2.77  	with valid_then_else P' valid_A conf_s1 eval_then_else
    2.78  	show ?thesis
    2.79 -	  by (cases rule: validE) rules+
    2.80 +	  by (cases rule: validE) iprover+
    2.81        qed
    2.82        moreover
    2.83        from eval wt da conf_s0 wf
    2.84 @@ -1308,7 +1308,7 @@
    2.85  	proof -
    2.86  	  from evaln_e wt_e da_e wf True
    2.87  	  have "nrm C \<subseteq>  dom (locals (store s1))"
    2.88 -	    by (cases rule: da_good_approx_evalnE) rules
    2.89 +	    by (cases rule: da_good_approx_evalnE) iprover
    2.90  	  with da_args show ?thesis
    2.91  	    by (rule da_weakenE) 
    2.92  	qed
    2.93 @@ -1328,7 +1328,7 @@
    2.94  	case False
    2.95  	with valid_args Q valid_A conf_s1 evaln_args
    2.96  	obtain "(R a) \<lfloor>vs\<rfloor>\<^sub>l s2 Z" "s2\<Colon>\<preceq>(G,L)" 
    2.97 -	  by (cases rule: validE) rules+
    2.98 +	  by (cases rule: validE) iprover+
    2.99  	moreover
   2.100  	from False evaln_args have "s2=s1"
   2.101  	  by auto
   2.102 @@ -1413,7 +1413,7 @@
   2.103  	proof -
   2.104  	  from evaln_e wt_e da_e wf normal_s1
   2.105  	  have "nrm C \<subseteq>  dom (locals (store s1))"
   2.106 -	    by (cases rule: da_good_approx_evalnE) rules
   2.107 +	    by (cases rule: da_good_approx_evalnE) iprover
   2.108  	  with da_args show ?thesis
   2.109  	    by (rule da_weakenE) 
   2.110  	qed
   2.111 @@ -1545,7 +1545,7 @@
   2.112                 ,lcl=callee_lcl invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> (mthd dynM)
   2.113                 \<rparr> \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'" and
   2.114                res: "Result \<in> nrm M'"
   2.115 -	      by (rule wf_mdeclE) rules
   2.116 +	      by (rule wf_mdeclE) iprover
   2.117  	    from da_body is_static_eq L' have
   2.118  	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
   2.119                   \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'"
   2.120 @@ -1594,7 +1594,7 @@
   2.121  	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> \<turnstile> dom (locals (store s3')) 
   2.122                       \<guillemotright>\<langle>Body (declclass dynM) (stmt (mbody (mthd dynM)))\<rangle>\<guillemotright> M3"
   2.123  	      using da
   2.124 -	      by (rules intro: da.Body assigned.select_convs)
   2.125 +	      by (iprover intro: da.Body assigned.select_convs)
   2.126  	    from _ this [simplified]
   2.127  	    show ?thesis
   2.128  	      by (rule da.Methd [simplified,elim_format])
   2.129 @@ -1602,12 +1602,12 @@
   2.130  	  qed
   2.131  	  from valid_methd R' valid_A conf_s3' evaln_methd wt_methd da_methd
   2.132  	  have "(set_lvars l .; S) \<lfloor>v\<rfloor>\<^sub>e s4 Z"
   2.133 -	    by (cases rule: validE) rules+
   2.134 +	    by (cases rule: validE) iprover+
   2.135  	  with s5 l show ?thesis
   2.136  	    by simp
   2.137  	qed
   2.138        qed
   2.139 -      with conf_s5 show ?thesis by rules
   2.140 +      with conf_s5 show ?thesis by iprover
   2.141      qed
   2.142    qed
   2.143  next
   2.144 @@ -1755,7 +1755,7 @@
   2.145  	proof -
   2.146  	  from eval_e wt_e da_e wf True
   2.147  	  have "nrm E1 \<subseteq> dom (locals (store s1))"
   2.148 -	    by (cases rule: da_good_approx_evalnE) rules
   2.149 +	    by (cases rule: da_good_approx_evalnE) iprover
   2.150  	  with da_es show ?thesis
   2.151  	    by (rule da_weakenE)
   2.152  	qed
   2.153 @@ -1766,7 +1766,7 @@
   2.154  	case False
   2.155  	with valid_es Q' valid_A conf_s1 eval_es 
   2.156  	show ?thesis
   2.157 -	  by (cases rule: validE) rules+
   2.158 +	  by (cases rule: validE) iprover+
   2.159        qed
   2.160        with v have "R \<lfloor>v\<rfloor>\<^sub>l s2 Z"
   2.161  	by simp
   2.162 @@ -1904,7 +1904,7 @@
   2.163  	proof -
   2.164  	  from eval_c1 wt_c1 da_c1 wf True
   2.165  	  have "nrm C1 \<subseteq> dom (locals (store s1))"
   2.166 -	    by (cases rule: da_good_approx_evalnE) rules
   2.167 +	    by (cases rule: da_good_approx_evalnE) iprover
   2.168  	  with da_c2 show ?thesis
   2.169  	    by (rule da_weakenE)
   2.170  	qed
   2.171 @@ -1915,7 +1915,7 @@
   2.172  	case False
   2.173  	from valid_c2 Q valid_A conf_s1 eval_c2 False
   2.174  	show ?thesis
   2.175 -	  by (cases rule: validE) rules+
   2.176 +	  by (cases rule: validE) iprover+
   2.177        qed
   2.178        moreover
   2.179        from eval wt da conf_s0 wf
   2.180 @@ -1992,7 +1992,7 @@
   2.181  	case False
   2.182  	with valid_then_else P' valid_A conf_s1 eval_then_else
   2.183  	show ?thesis
   2.184 -	  by (cases rule: validE) rules+
   2.185 +	  by (cases rule: validE) iprover+
   2.186        qed
   2.187        moreover
   2.188        from eval wt da conf_s0 wf
     3.1 --- a/src/HOL/Bali/Decl.thy	Thu Sep 22 23:55:42 2005 +0200
     3.2 +++ b/src/HOL/Bali/Decl.thy	Thu Sep 22 23:56:15 2005 +0200
     3.3 @@ -80,7 +80,7 @@
     3.4      have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
     3.5        by (auto simp add: less_acc_def split add: acc_modi.split)
     3.6      with prems show ?thesis
     3.7 -      by (unfold le_acc_def) rules
     3.8 +      by (unfold le_acc_def) iprover
     3.9    qed
    3.10    next
    3.11    show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
     4.1 --- a/src/HOL/Bali/DefiniteAssignment.thy	Thu Sep 22 23:55:42 2005 +0200
     4.2 +++ b/src/HOL/Bali/DefiniteAssignment.thy	Thu Sep 22 23:56:15 2005 +0200
     4.3 @@ -1350,18 +1350,18 @@
     4.4    from da  
     4.5    show "\<And> B'. B \<subseteq> B' \<Longrightarrow> \<exists> A'. Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" (is "PROP ?Hyp Env B t")
     4.6    proof (induct) 
     4.7 -    case Skip thus ?case by (rules intro: da.Skip)
     4.8 +    case Skip thus ?case by (iprover intro: da.Skip)
     4.9    next
    4.10 -    case Expr thus ?case by (rules intro: da.Expr)
    4.11 +    case Expr thus ?case by (iprover intro: da.Expr)
    4.12    next
    4.13      case (Lab A B C Env c l B')  
    4.14      have "PROP ?Hyp Env B \<langle>c\<rangle>" .
    4.15      moreover
    4.16      have B': "B \<subseteq> B'" .
    4.17      ultimately obtain C' where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
    4.18 -      by rules
    4.19 +      by iprover
    4.20      then obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A'"
    4.21 -      by (rules intro: da.Lab)
    4.22 +      by (iprover intro: da.Lab)
    4.23      thus ?case ..
    4.24    next
    4.25      case (Comp A B C1 C2 Env c1 c2 B')
    4.26 @@ -1370,7 +1370,7 @@
    4.27      moreover
    4.28      have B': "B \<subseteq> B'" .
    4.29      ultimately obtain C1' where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
    4.30 -      by rules
    4.31 +      by iprover
    4.32      with da_c1 B'
    4.33      have
    4.34        "nrm C1 \<subseteq> nrm C1'"
    4.35 @@ -1378,9 +1378,9 @@
    4.36      moreover
    4.37      have "PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle>" .
    4.38      ultimately obtain C2' where "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
    4.39 -      by rules
    4.40 +      by iprover
    4.41      with da_c1' obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'"
    4.42 -      by (rules intro: da.Comp)
    4.43 +      by (iprover intro: da.Comp)
    4.44      thus ?case ..
    4.45    next
    4.46      case (If A B C1 C2 E Env c1 c2 e B')
    4.47 @@ -1389,7 +1389,7 @@
    4.48      proof -
    4.49        have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule If.hyps)
    4.50        with B'  
    4.51 -      show ?thesis using that by rules
    4.52 +      show ?thesis using that by iprover
    4.53      qed
    4.54      moreover
    4.55      obtain C1' where "Env\<turnstile> (B' \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
    4.56 @@ -1400,7 +1400,7 @@
    4.57        moreover
    4.58        have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle>" by (rule If.hyps)
    4.59        ultimately 
    4.60 -      show ?thesis using that by rules
    4.61 +      show ?thesis using that by iprover
    4.62      qed
    4.63      moreover
    4.64      obtain C2' where "Env\<turnstile> (B' \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
    4.65 @@ -1410,11 +1410,11 @@
    4.66        moreover
    4.67        have "PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle>" by (rule If.hyps)
    4.68        ultimately
    4.69 -      show ?thesis using that by rules
    4.70 +      show ?thesis using that by iprover
    4.71      qed
    4.72      ultimately
    4.73      obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'"
    4.74 -      by (rules intro: da.If)
    4.75 +      by (iprover intro: da.If)
    4.76      thus ?case ..
    4.77    next  
    4.78      case (Loop A B C E Env c e l B')
    4.79 @@ -1423,7 +1423,7 @@
    4.80      proof -
    4.81        have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Loop.hyps)
    4.82        with B'  
    4.83 -      show ?thesis using that by rules
    4.84 +      show ?thesis using that by iprover
    4.85      qed
    4.86      moreover
    4.87      obtain C' where "Env\<turnstile> (B' \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
    4.88 @@ -1434,11 +1434,11 @@
    4.89        moreover
    4.90        have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle>" by (rule Loop.hyps)
    4.91        ultimately 
    4.92 -      show ?thesis using that by rules
    4.93 +      show ?thesis using that by iprover
    4.94      qed
    4.95      ultimately
    4.96      obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'"
    4.97 -      by (rules intro: da.Loop )
    4.98 +      by (iprover intro: da.Loop )
    4.99      thus ?case ..
   4.100    next
   4.101      case (Jmp A B Env jump B') 
   4.102 @@ -1453,12 +1453,12 @@
   4.103                                  | Cont l \<Rightarrow> \<lambda>k. UNIV
   4.104                                  | Ret \<Rightarrow> \<lambda>k. UNIV)"
   4.105                       
   4.106 -      by  rules
   4.107 +      by  iprover
   4.108      ultimately have "Env\<turnstile> B' \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A'"
   4.109        by (rule da.Jmp)
   4.110      thus ?case ..
   4.111    next
   4.112 -    case Throw thus ?case by (rules intro: da.Throw )
   4.113 +    case Throw thus ?case by (iprover intro: da.Throw )
   4.114    next
   4.115      case (Try A B C C1 C2 Env c1 c2 vn B')
   4.116      have B': "B \<subseteq> B'" .
   4.117 @@ -1466,7 +1466,7 @@
   4.118      proof -
   4.119        have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Try.hyps)
   4.120        with B'  
   4.121 -      show ?thesis using that by rules
   4.122 +      show ?thesis using that by iprover
   4.123      qed
   4.124      moreover
   4.125      obtain C2' where 
   4.126 @@ -1478,11 +1478,11 @@
   4.127                        (B \<union> {VName vn}) \<langle>c2\<rangle>" 
   4.128  	by (rule Try.hyps)
   4.129        ultimately
   4.130 -      show ?thesis using that by rules
   4.131 +      show ?thesis using that by iprover
   4.132      qed
   4.133      ultimately
   4.134      obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'"
   4.135 -      by (rules intro: da.Try )
   4.136 +      by (iprover intro: da.Try )
   4.137      thus ?case ..
   4.138    next
   4.139      case (Fin A B C1 C2 Env c1 c2 B')
   4.140 @@ -1491,33 +1491,33 @@
   4.141      proof -
   4.142        have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Fin.hyps)
   4.143        with B'  
   4.144 -      show ?thesis using that by rules
   4.145 +      show ?thesis using that by iprover
   4.146      qed
   4.147      moreover
   4.148      obtain C2' where "Env\<turnstile> B' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
   4.149      proof -
   4.150        have "PROP ?Hyp Env B \<langle>c2\<rangle>" by (rule Fin.hyps)
   4.151        with B'
   4.152 -      show ?thesis using that by rules
   4.153 +      show ?thesis using that by iprover
   4.154      qed
   4.155      ultimately
   4.156      obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'"
   4.157 -      by (rules intro: da.Fin )
   4.158 +      by (iprover intro: da.Fin )
   4.159      thus ?case ..
   4.160    next
   4.161 -    case Init thus ?case by (rules intro: da.Init)
   4.162 +    case Init thus ?case by (iprover intro: da.Init)
   4.163    next
   4.164 -    case NewC thus ?case by (rules intro: da.NewC)
   4.165 +    case NewC thus ?case by (iprover intro: da.NewC)
   4.166    next
   4.167 -    case NewA thus ?case by (rules intro: da.NewA)
   4.168 +    case NewA thus ?case by (iprover intro: da.NewA)
   4.169    next
   4.170 -    case Cast thus ?case by (rules intro: da.Cast)
   4.171 +    case Cast thus ?case by (iprover intro: da.Cast)
   4.172    next
   4.173 -    case Inst thus ?case by (rules intro: da.Inst)
   4.174 +    case Inst thus ?case by (iprover intro: da.Inst)
   4.175    next
   4.176 -    case Lit thus ?case by (rules intro: da.Lit)
   4.177 +    case Lit thus ?case by (iprover intro: da.Lit)
   4.178    next
   4.179 -    case UnOp thus ?case by (rules intro: da.UnOp)
   4.180 +    case UnOp thus ?case by (iprover intro: da.UnOp)
   4.181    next
   4.182      case (CondAnd A B E1 E2 Env e1 e2 B')
   4.183      have B': "B \<subseteq> B'" .
   4.184 @@ -1525,7 +1525,7 @@
   4.185      proof -
   4.186        have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondAnd.hyps)
   4.187        with B'  
   4.188 -      show ?thesis using that by rules
   4.189 +      show ?thesis using that by iprover
   4.190      qed
   4.191      moreover
   4.192      obtain E2' where "Env\<turnstile> B' \<union>  assigns_if True e1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
   4.193 @@ -1534,11 +1534,11 @@
   4.194  	by blast
   4.195        moreover
   4.196        have "PROP ?Hyp Env (B \<union> assigns_if True e1) \<langle>e2\<rangle>" by (rule CondAnd.hyps)
   4.197 -      ultimately show ?thesis using that by rules
   4.198 +      ultimately show ?thesis using that by iprover
   4.199      qed
   4.200      ultimately
   4.201      obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'"
   4.202 -      by (rules intro: da.CondAnd)
   4.203 +      by (iprover intro: da.CondAnd)
   4.204      thus ?case ..
   4.205    next
   4.206      case (CondOr A B E1 E2 Env e1 e2 B')
   4.207 @@ -1547,7 +1547,7 @@
   4.208      proof -
   4.209        have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondOr.hyps)
   4.210        with B'  
   4.211 -      show ?thesis using that by rules
   4.212 +      show ?thesis using that by iprover
   4.213      qed
   4.214      moreover
   4.215      obtain E2' where "Env\<turnstile> B' \<union> assigns_if False e1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
   4.216 @@ -1556,11 +1556,11 @@
   4.217  	by blast
   4.218        moreover
   4.219        have "PROP ?Hyp Env (B \<union> assigns_if False e1) \<langle>e2\<rangle>" by (rule CondOr.hyps)
   4.220 -      ultimately show ?thesis using that by rules
   4.221 +      ultimately show ?thesis using that by iprover
   4.222      qed
   4.223      ultimately
   4.224      obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondOr e1 e2\<rangle>\<guillemotright> A'"
   4.225 -      by (rules intro: da.CondOr)
   4.226 +      by (iprover intro: da.CondOr)
   4.227      thus ?case ..
   4.228    next
   4.229      case (BinOp A B E1 Env binop e1 e2 B')
   4.230 @@ -1569,7 +1569,7 @@
   4.231      proof -
   4.232        have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule BinOp.hyps)
   4.233        with B'  
   4.234 -      show ?thesis using that by rules
   4.235 +      show ?thesis using that by iprover
   4.236      qed
   4.237      moreover
   4.238      obtain A' where "Env\<turnstile> nrm E1' \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'"
   4.239 @@ -1580,35 +1580,35 @@
   4.240  	by (rule da_monotone [THEN conjE])
   4.241        moreover 
   4.242        have "PROP ?Hyp Env (nrm E1) \<langle>e2\<rangle>" by (rule BinOp.hyps)
   4.243 -      ultimately show ?thesis using that by rules
   4.244 +      ultimately show ?thesis using that by iprover
   4.245      qed
   4.246      ultimately
   4.247      have "Env\<turnstile> B' \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A'"
   4.248 -      using BinOp.hyps by (rules intro: da.BinOp)
   4.249 +      using BinOp.hyps by (iprover intro: da.BinOp)
   4.250      thus ?case ..
   4.251    next
   4.252      case (Super B Env B')
   4.253      have B': "B \<subseteq> B'" .
   4.254      with Super.hyps have "This \<in> B' "
   4.255        by auto
   4.256 -    thus ?case by (rules intro: da.Super)
   4.257 +    thus ?case by (iprover intro: da.Super)
   4.258    next
   4.259      case (AccLVar A B Env vn B')
   4.260      have "vn \<in> B" .
   4.261      moreover
   4.262      have "B \<subseteq> B'" .
   4.263      ultimately have "vn \<in> B'" by auto
   4.264 -    thus ?case by (rules intro: da.AccLVar)
   4.265 +    thus ?case by (iprover intro: da.AccLVar)
   4.266    next
   4.267 -    case Acc thus ?case by (rules intro: da.Acc)
   4.268 +    case Acc thus ?case by (iprover intro: da.Acc)
   4.269    next 
   4.270      case (AssLVar A B E Env e vn B')
   4.271      have B': "B \<subseteq> B'" .
   4.272      then obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
   4.273 -      by (rule AssLVar.hyps [elim_format]) rules
   4.274 +      by (rule AssLVar.hyps [elim_format]) iprover
   4.275      then obtain A' where  
   4.276        "Env\<turnstile> B' \<guillemotright>\<langle>LVar vn:=e\<rangle>\<guillemotright> A'"
   4.277 -      by (rules intro: da.AssLVar)
   4.278 +      by (iprover intro: da.AssLVar)
   4.279      thus ?case ..
   4.280    next
   4.281      case (Ass A B Env V e v B') 
   4.282 @@ -1619,7 +1619,7 @@
   4.283      proof -
   4.284        have "PROP ?Hyp Env B \<langle>v\<rangle>" by (rule Ass.hyps)
   4.285        with B'  
   4.286 -      show ?thesis using that by rules
   4.287 +      show ?thesis using that by iprover
   4.288      qed
   4.289      moreover
   4.290      obtain A' where "Env\<turnstile> nrm V' \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'"
   4.291 @@ -1630,11 +1630,11 @@
   4.292  	by (rule da_monotone [THEN conjE])
   4.293        moreover 
   4.294        have "PROP ?Hyp Env (nrm V) \<langle>e\<rangle>" by (rule Ass.hyps)
   4.295 -      ultimately show ?thesis using that by rules
   4.296 +      ultimately show ?thesis using that by iprover
   4.297      qed  
   4.298      ultimately
   4.299      have "Env\<turnstile> B' \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A'"
   4.300 -      by (rules intro: da.Ass)
   4.301 +      by (iprover intro: da.Ass)
   4.302      thus ?case ..
   4.303    next
   4.304      case (CondBool A B C E1 E2 Env c e1 e2 B')
   4.305 @@ -1644,7 +1644,7 @@
   4.306      proof -
   4.307        have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule CondBool.hyps)
   4.308        with B'  
   4.309 -      show ?thesis using that by rules
   4.310 +      show ?thesis using that by iprover
   4.311      qed
   4.312      moreover 
   4.313      obtain E1' where "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
   4.314 @@ -1655,7 +1655,7 @@
   4.315        moreover
   4.316        have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle>" by (rule CondBool.hyps)
   4.317        ultimately 
   4.318 -      show ?thesis using that by rules
   4.319 +      show ?thesis using that by iprover
   4.320      qed
   4.321      moreover
   4.322      obtain E2' where "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
   4.323 @@ -1666,11 +1666,11 @@
   4.324        moreover
   4.325        have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle>" by(rule CondBool.hyps)
   4.326        ultimately 
   4.327 -      show ?thesis using that by rules
   4.328 +      show ?thesis using that by iprover
   4.329      qed
   4.330      ultimately 
   4.331      obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'"
   4.332 -      by (rules intro: da.CondBool)
   4.333 +      by (iprover intro: da.CondBool)
   4.334      thus ?case ..
   4.335    next
   4.336      case (Cond A B C E1 E2 Env c e1 e2 B')
   4.337 @@ -1680,7 +1680,7 @@
   4.338      proof -
   4.339        have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule Cond.hyps)
   4.340        with B'  
   4.341 -      show ?thesis using that by rules
   4.342 +      show ?thesis using that by iprover
   4.343      qed
   4.344      moreover 
   4.345      obtain E1' where "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
   4.346 @@ -1691,7 +1691,7 @@
   4.347        moreover
   4.348        have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle>" by (rule Cond.hyps)
   4.349        ultimately 
   4.350 -      show ?thesis using that by rules
   4.351 +      show ?thesis using that by iprover
   4.352      qed
   4.353      moreover
   4.354      obtain E2' where "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
   4.355 @@ -1702,11 +1702,11 @@
   4.356        moreover
   4.357        have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle>" by (rule Cond.hyps)
   4.358        ultimately 
   4.359 -      show ?thesis using that by rules
   4.360 +      show ?thesis using that by iprover
   4.361      qed
   4.362      ultimately 
   4.363      obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'"
   4.364 -      by (rules intro: da.Cond)
   4.365 +      by (iprover intro: da.Cond)
   4.366      thus ?case ..
   4.367    next
   4.368      case (Call A B E Env accC args e mn mode pTs statT B')
   4.369 @@ -1715,7 +1715,7 @@
   4.370      proof -
   4.371        have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Call.hyps)
   4.372        with B'  
   4.373 -      show ?thesis using that by rules
   4.374 +      show ?thesis using that by iprover
   4.375      qed
   4.376      moreover
   4.377      obtain A' where "Env\<turnstile> nrm E' \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'"
   4.378 @@ -1726,14 +1726,14 @@
   4.379  	by (rule da_monotone [THEN conjE])
   4.380        moreover 
   4.381        have "PROP ?Hyp Env (nrm E) \<langle>args\<rangle>" by (rule Call.hyps)
   4.382 -      ultimately show ?thesis using that by rules
   4.383 +      ultimately show ?thesis using that by iprover
   4.384      qed  
   4.385      ultimately
   4.386      have "Env\<turnstile> B' \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn( {pTs}args)\<rangle>\<guillemotright> A'"
   4.387 -      by (rules intro: da.Call)
   4.388 +      by (iprover intro: da.Call)
   4.389      thus ?case ..
   4.390    next
   4.391 -    case Methd thus ?case by (rules intro: da.Methd)
   4.392 +    case Methd thus ?case by (iprover intro: da.Methd)
   4.393    next
   4.394      case (Body A B C D Env c B')  
   4.395      have B': "B \<subseteq> B'" .
   4.396 @@ -1747,7 +1747,7 @@
   4.397        ultimately
   4.398        have "nrm C \<subseteq> nrm C'"
   4.399  	by (rule da_monotone [THEN conjE])
   4.400 -      with da_c that show ?thesis by rules
   4.401 +      with da_c that show ?thesis by iprover
   4.402      qed
   4.403      moreover 
   4.404      have "Result \<in> nrm C" .
   4.405 @@ -1756,12 +1756,12 @@
   4.406      moreover have "jumpNestingOkS {Ret} c" .
   4.407      ultimately obtain A' where
   4.408        "Env\<turnstile> B' \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A'"
   4.409 -      by (rules intro: da.Body)
   4.410 +      by (iprover intro: da.Body)
   4.411      thus ?case ..
   4.412    next
   4.413 -    case LVar thus ?case by (rules intro: da.LVar)
   4.414 +    case LVar thus ?case by (iprover intro: da.LVar)
   4.415    next
   4.416 -    case FVar thus ?case by (rules intro: da.FVar)
   4.417 +    case FVar thus ?case by (iprover intro: da.FVar)
   4.418    next
   4.419      case (AVar A B E1 Env e1 e2 B')
   4.420      have B': "B \<subseteq> B'" .
   4.421 @@ -1769,7 +1769,7 @@
   4.422      proof -
   4.423        have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule AVar.hyps)
   4.424        with B'  
   4.425 -      show ?thesis using that by rules
   4.426 +      show ?thesis using that by iprover
   4.427      qed
   4.428      moreover
   4.429      obtain A' where "Env\<turnstile> nrm E1' \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'"
   4.430 @@ -1780,14 +1780,14 @@
   4.431  	by (rule da_monotone [THEN conjE])
   4.432        moreover 
   4.433        have "PROP ?Hyp Env (nrm E1) \<langle>e2\<rangle>" by (rule AVar.hyps)
   4.434 -      ultimately show ?thesis using that by rules
   4.435 +      ultimately show ?thesis using that by iprover
   4.436      qed  
   4.437      ultimately
   4.438      have "Env\<turnstile> B' \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A'"
   4.439 -      by (rules intro: da.AVar)
   4.440 +      by (iprover intro: da.AVar)
   4.441      thus ?case ..
   4.442    next
   4.443 -    case Nil thus ?case by (rules intro: da.Nil)
   4.444 +    case Nil thus ?case by (iprover intro: da.Nil)
   4.445    next
   4.446      case (Cons A B E Env e es B')
   4.447      have B': "B \<subseteq> B'" .
   4.448 @@ -1795,7 +1795,7 @@
   4.449      proof -
   4.450        have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Cons.hyps)
   4.451        with B'  
   4.452 -      show ?thesis using that by rules
   4.453 +      show ?thesis using that by iprover
   4.454      qed
   4.455      moreover
   4.456      obtain A' where "Env\<turnstile> nrm E' \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'"
   4.457 @@ -1806,11 +1806,11 @@
   4.458  	by (rule da_monotone [THEN conjE])
   4.459        moreover 
   4.460        have "PROP ?Hyp Env (nrm E) \<langle>es\<rangle>" by (rule Cons.hyps)
   4.461 -      ultimately show ?thesis using that by rules
   4.462 +      ultimately show ?thesis using that by iprover
   4.463      qed  
   4.464      ultimately
   4.465      have "Env\<turnstile> B' \<guillemotright>\<langle>e # es\<rangle>\<guillemotright> A'"
   4.466 -      by (rules intro: da.Cons)
   4.467 +      by (iprover intro: da.Cons)
   4.468      thus ?case ..
   4.469    qed
   4.470  qed
   4.471 @@ -1841,13 +1841,13 @@
   4.472  proof -
   4.473    from da B'
   4.474    obtain A' where A': "Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'"
   4.475 -    by (rule da_weaken [elim_format]) rules
   4.476 +    by (rule da_weaken [elim_format]) iprover
   4.477    with da B'
   4.478    have "nrm A \<subseteq> nrm A' \<and> (\<forall> l. brk A l \<subseteq> brk A' l)"
   4.479      by (rule da_monotone)
   4.480    with A' ex_mono
   4.481    show ?thesis
   4.482 -    by rules
   4.483 +    by iprover
   4.484  qed
   4.485  
   4.486 -end
   4.487 \ No newline at end of file
   4.488 +end
     5.1 --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Thu Sep 22 23:55:42 2005 +0200
     5.2 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Thu Sep 22 23:56:15 2005 +0200
     5.3 @@ -165,7 +165,7 @@
     5.4    qed (simp_all)
     5.5    with jumpNestingOk_l' subset
     5.6    show ?thesis
     5.7 -    by rules
     5.8 +    by iprover
     5.9  qed
    5.10     
    5.11  corollary jumpNestingOk_mono: 
    5.12 @@ -429,7 +429,7 @@
    5.13              by simp
    5.14            moreover from jmp_s1 have "?Jmp ({Cont l} \<union> jmps) s1" by simp
    5.15            ultimately have jmp_s2: "?Jmp ({Cont l} \<union> jmps) s2" 
    5.16 -            using wt_c G by rules
    5.17 +            using wt_c G by iprover
    5.18            have "?Jmp jmps (abupd (absorb (Cont l)) s2)"
    5.19            proof -
    5.20              {
    5.21 @@ -1701,7 +1701,7 @@
    5.22  	by - (erule halloc_no_abrupt [rule_format])
    5.23        hence "normal s2" by (cases s2) simp
    5.24        with NewA.hyps
    5.25 -      show ?thesis by rules
    5.26 +      show ?thesis by iprover
    5.27      qed
    5.28      also
    5.29      from halloc 
    5.30 @@ -1732,7 +1732,7 @@
    5.31      hence "normal s1" by - (erule eval_no_abrupt_lemma [rule_format]) 
    5.32      with BinOp.hyps
    5.33      have "assigns (In1l e1) \<subseteq> dom (locals (store s1))"
    5.34 -      by rules
    5.35 +      by iprover
    5.36      also
    5.37      have "\<dots>  \<subseteq> dom (locals (store s2))"
    5.38      proof -
    5.39 @@ -1768,7 +1768,7 @@
    5.40        by - (erule eval_no_abrupt_lemma [rule_format]) 
    5.41      with Ass.hyps
    5.42      have "assigns (In2 va) \<subseteq> dom (locals (store s1))" 
    5.43 -      by rules
    5.44 +      by iprover
    5.45      also
    5.46      from Ass.hyps
    5.47      have "\<dots> \<subseteq> dom (locals (store s2))"
    5.48 @@ -1776,7 +1776,7 @@
    5.49      also
    5.50      from nrm_s2 Ass.hyps
    5.51      have "assigns (In1l e) \<subseteq> dom (locals (store s2))"
    5.52 -      by rules
    5.53 +      by iprover
    5.54      ultimately
    5.55      have "assigns (In2 va) \<union> assigns (In1l e) \<subseteq>  dom (locals (store s2))"
    5.56        by (rule Un_least)
    5.57 @@ -1816,7 +1816,7 @@
    5.58        by - (erule eval_no_abrupt_lemma [rule_format])
    5.59      with Cond.hyps
    5.60      have "assigns (In1l e0) \<subseteq> dom (locals (store s1))"
    5.61 -      by rules
    5.62 +      by iprover
    5.63      also from Cond.hyps
    5.64      have "\<dots> \<subseteq> dom (locals (store s2))"
    5.65        by - (erule dom_locals_eval_mono_elim)
    5.66 @@ -1868,14 +1868,14 @@
    5.67        by - (erule eval_no_abrupt_lemma [rule_format])
    5.68      with Call.hyps
    5.69      have "assigns (In1l e) \<subseteq> dom (locals (store s1))"
    5.70 -      by rules
    5.71 +      by iprover
    5.72      also from Call.hyps
    5.73      have "\<dots> \<subseteq>  dom (locals (store s2))"
    5.74        by - (erule dom_locals_eval_mono_elim)
    5.75      also
    5.76      from nrm_s2 Call.hyps
    5.77      have "assigns (In3 args) \<subseteq> dom (locals (store s2))"
    5.78 -      by rules
    5.79 +      by iprover
    5.80      ultimately have "assigns (In1l e) \<union> assigns (In3 args) \<subseteq> \<dots>"
    5.81        by (rule Un_least)
    5.82      also 
    5.83 @@ -1903,7 +1903,7 @@
    5.84      qed
    5.85      with FVar.hyps 
    5.86      have "assigns (In1l e) \<subseteq> dom (locals (store s2))"
    5.87 -      by rules
    5.88 +      by iprover
    5.89      also
    5.90      have "\<dots> \<subseteq>  dom (locals (store s2'))"
    5.91      proof -
    5.92 @@ -1932,14 +1932,14 @@
    5.93        by - (erule eval_no_abrupt_lemma [rule_format])
    5.94      with AVar.hyps
    5.95      have "assigns (In1l e1) \<subseteq> dom (locals (store s1))"
    5.96 -      by rules
    5.97 +      by iprover
    5.98      also from AVar.hyps
    5.99      have "\<dots> \<subseteq>  dom (locals (store s2))"
   5.100        by - (erule dom_locals_eval_mono_elim)
   5.101      also
   5.102      from AVar.hyps nrm_s2
   5.103      have "assigns (In1l e2) \<subseteq> dom (locals (store s2))"
   5.104 -      by rules
   5.105 +      by iprover
   5.106      ultimately
   5.107      have "assigns (In1l e1) \<union> assigns (In1l e2) \<subseteq> \<dots>"
   5.108        by (rule Un_least)
   5.109 @@ -1962,14 +1962,14 @@
   5.110      proof -
   5.111        from Cons
   5.112        have "normal s1" by - (erule eval_no_abrupt_lemma [rule_format])
   5.113 -      with Cons.hyps show ?thesis by rules
   5.114 +      with Cons.hyps show ?thesis by iprover
   5.115      qed
   5.116      also from Cons.hyps
   5.117      have "\<dots> \<subseteq>  dom (locals (store s2))"
   5.118        by - (erule dom_locals_eval_mono_elim)
   5.119      also from Cons
   5.120      have "assigns (In3 es) \<subseteq> dom (locals (store s2))"
   5.121 -      by rules
   5.122 +      by iprover
   5.123      ultimately
   5.124      have "assigns (In1l e) \<union> assigns (In3 es) \<subseteq> dom (locals (store s2))"
   5.125        by (rule Un_least)
   5.126 @@ -2043,7 +2043,7 @@
   5.127        by cases simp
   5.128      from ce ve
   5.129      obtain eq_ve_ce: "ve=ce" and nrm_s: "normal s"
   5.130 -      by (rule UnOp.hyps [elim_format]) rules
   5.131 +      by (rule UnOp.hyps [elim_format]) iprover
   5.132      from eq_ve_ce const ce v 
   5.133      have "v=c" 
   5.134        by simp
   5.135 @@ -2066,7 +2066,7 @@
   5.136      from c1 v1
   5.137      obtain eq_v1_c1: "v1 = c1" and 
   5.138               nrm_s1: "normal s1"
   5.139 -      by (rule BinOp.hyps [elim_format]) rules
   5.140 +      by (rule BinOp.hyps [elim_format]) iprover
   5.141      show ?case
   5.142      proof (cases "need_second_arg binop v1")
   5.143        case True
   5.144 @@ -2074,7 +2074,7 @@
   5.145  	where "G\<turnstile>Norm s1' \<midarrow>e2-\<succ>v2\<rightarrow> s" 
   5.146  	by (cases s1) simp
   5.147        with c2 obtain "v2 = c2" "normal s"
   5.148 -	by (rule BinOp.hyps [elim_format]) rules
   5.149 +	by (rule BinOp.hyps [elim_format]) iprover
   5.150        with c c1 c2 eq_v1_c1 v 
   5.151        show ?thesis by simp
   5.152      next
   5.153 @@ -2111,7 +2111,7 @@
   5.154        by cases simp 
   5.155      from cb vb
   5.156      obtain eq_vb_cb: "vb = cb" and nrm_s1: "normal s1"
   5.157 -      by (rule Cond.hyps [elim_format]) rules 
   5.158 +      by (rule Cond.hyps [elim_format]) iprover 
   5.159      show ?case
   5.160      proof (cases "the_Bool vb")
   5.161        case True
   5.162 @@ -2123,7 +2123,7 @@
   5.163  	where "G\<turnstile>Norm s1' \<midarrow>e1-\<succ>v\<rightarrow> s"
   5.164  	by (cases s1) simp
   5.165        with c1 obtain "c1 = v" "normal s"
   5.166 -	by (rule Cond.hyps [elim_format]) rules 
   5.167 +	by (rule Cond.hyps [elim_format]) iprover 
   5.168        ultimately show ?thesis by simp
   5.169      next
   5.170        case False
   5.171 @@ -2135,7 +2135,7 @@
   5.172  	where "G\<turnstile>Norm s1' \<midarrow>e2-\<succ>v\<rightarrow> s"
   5.173  	by (cases s1) simp
   5.174        with c2 obtain "c2 = v" "normal s"
   5.175 -	by (rule Cond.hyps [elim_format]) rules 
   5.176 +	by (rule Cond.hyps [elim_format]) iprover 
   5.177        ultimately show ?thesis by simp
   5.178      qed
   5.179    next
   5.180 @@ -2143,7 +2143,7 @@
   5.181    qed simp_all
   5.182    with const eval
   5.183    show ?thesis
   5.184 -    by rules
   5.185 +    by iprover
   5.186  qed
   5.187    
   5.188  lemmas constVal_eval_elim = constVal_eval [THEN conjE]
   5.189 @@ -2235,7 +2235,7 @@
   5.190    qed simp_all
   5.191    with const wt
   5.192    show ?thesis
   5.193 -    by rules
   5.194 +    by iprover
   5.195  qed	
   5.196        
   5.197  lemma assigns_if_good_approx:
   5.198 @@ -2777,12 +2777,12 @@
   5.199      show ?case
   5.200      proof (cases "normal s1")
   5.201        case True
   5.202 -      with nrm_c1 have "nrm C1 \<subseteq> dom (locals (snd s1))" by rules
   5.203 +      with nrm_c1 have "nrm C1 \<subseteq> dom (locals (snd s1))" by iprover
   5.204        with da_c2 obtain C2' 
   5.205  	where  da_c2': "Env\<turnstile> dom (locals (snd s1)) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
   5.206                 nrm_c2: "nrm C2 \<subseteq> nrm C2'"                  and
   5.207                 brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"
   5.208 -        by (rule da_weakenE) rules
   5.209 +        by (rule da_weakenE) iprover
   5.210        have "PROP ?Hyp (In1r c2) s1 s2" .
   5.211        with wt_c2 da_c2' G
   5.212        obtain nrm_c2': "?NormalAssigned s2 C2'" and 
   5.213 @@ -2871,7 +2871,7 @@
   5.214  	  where da_c1': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
   5.215  	        nrm_c1: "nrm C1 \<subseteq> nrm C1'"                  and
   5.216                  brk_c1: "\<forall> l. brk C1 l \<subseteq> brk C1' l"
   5.217 -          by (rule da_weakenE) rules
   5.218 +          by (rule da_weakenE) iprover
   5.219  	from If.hyps True have "PROP ?Hyp (In1r c1) s1 s2" by simp
   5.220  	with wt_c1 da_c1'
   5.221  	obtain nrm_c1': "?NormalAssigned s2 C1'" and 
   5.222 @@ -2901,7 +2901,7 @@
   5.223  	  where da_c2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
   5.224  	        nrm_c2: "nrm C2 \<subseteq> nrm C2'"                  and
   5.225                  brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"
   5.226 -          by (rule da_weakenE) rules
   5.227 +          by (rule da_weakenE) iprover
   5.228  	from If.hyps False have "PROP ?Hyp (In1r c2) s1 s2" by simp
   5.229  	with wt_c2 da_c2'
   5.230  	obtain nrm_c2': "?NormalAssigned s2 C2'" and 
   5.231 @@ -2993,7 +2993,7 @@
   5.232  	  where da_c': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and
   5.233  	     nrm_C_C': "nrm C \<subseteq> nrm C'"                  and
   5.234               brk_C_C': "\<forall> l. brk C l \<subseteq> brk C' l"
   5.235 -          by (rule da_weakenE) rules
   5.236 +          by (rule da_weakenE) iprover
   5.237  	from hyp_c wt_c da_c'
   5.238  	obtain nrm_C': "?NormalAssigned s2 C'" and 
   5.239            brk_C': "?BreakAssigned s1 s2 C'" and
   5.240 @@ -3855,11 +3855,11 @@
   5.241            with wt_e1 da_e1 G normal_s1
   5.242            obtain "?NormalAssigned s1 E1"  
   5.243              by simp
   5.244 -          with normal_s1 have "nrm E1 \<subseteq> dom (locals (store s1))" by rules
   5.245 +          with normal_s1 have "nrm E1 \<subseteq> dom (locals (store s1))" by iprover
   5.246            with da_e2 obtain A' 
   5.247              where  da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and
   5.248                   nrm_A_A': "nrm A \<subseteq> nrm A'"                  
   5.249 -            by (rule da_weakenE) rules
   5.250 +            by (rule da_weakenE) iprover
   5.251            from notAndOr have "need_second_arg binop v1" by simp
   5.252            with BinOp.hyps 
   5.253            have "PROP ?Hyp (In1l e2) s1 s2" by simp
   5.254 @@ -4004,7 +4004,7 @@
   5.255          with da_e obtain A' 
   5.256            where  da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and
   5.257                   nrm_A_A': "nrm A \<subseteq> nrm A'"                  
   5.258 -          by (rule da_weakenE) rules
   5.259 +          by (rule da_weakenE) iprover
   5.260          from hyp_e wt_e da_e' G normal_s2
   5.261          obtain "nrm A' \<subseteq> dom (locals (store s2))"   
   5.262            by simp
   5.263 @@ -4121,7 +4121,7 @@
   5.264            with da_e1 obtain E1' where
   5.265                    da_e1': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" and
   5.266                nrm_E1_E1': "nrm E1 \<subseteq> nrm E1'"
   5.267 -            by (rule da_weakenE) rules
   5.268 +            by (rule da_weakenE) iprover
   5.269            ultimately have "nrm E1' \<subseteq> dom (locals (store s2))"
   5.270              using wt_e1 G normal_s2 by simp 
   5.271            with nrm_E1_E1' show ?thesis
   5.272 @@ -4140,7 +4140,7 @@
   5.273            with da_e2 obtain E2' where
   5.274                    da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" and
   5.275                nrm_E2_E2': "nrm E2 \<subseteq> nrm E2'"
   5.276 -            by (rule da_weakenE) rules
   5.277 +            by (rule da_weakenE) iprover
   5.278            ultimately have "nrm E2' \<subseteq> dom (locals (store s2))"
   5.279              using wt_e2 G normal_s2 by simp 
   5.280            with nrm_E2_E2' show ?thesis
   5.281 @@ -4206,7 +4206,7 @@
   5.282          with da_args obtain A' where
   5.283            da_args': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'" and
   5.284            nrm_A_A': "nrm A \<subseteq> nrm A'"
   5.285 -          by (rule da_weakenE) rules
   5.286 +          by (rule da_weakenE) iprover
   5.287          have "PROP ?Hyp (In3 args) s1 s2" .
   5.288          with da_args' wt_args G normal_s2
   5.289          have "nrm A' \<subseteq> dom (locals (store s2))"
   5.290 @@ -4313,7 +4313,7 @@
   5.291          with da_e obtain A' where
   5.292            da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and
   5.293            nrm_A_A': "nrm A \<subseteq> nrm A'"
   5.294 -          by (rule da_weakenE) rules
   5.295 +          by (rule da_weakenE) iprover
   5.296          have normal_s2: "normal s2"
   5.297          proof -
   5.298            from normal_s3 s3 
   5.299 @@ -4391,7 +4391,7 @@
   5.300          with da_e2 obtain A' where
   5.301            da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and
   5.302            nrm_A_A': "nrm A \<subseteq> nrm A'"
   5.303 -          by (rule da_weakenE) rules
   5.304 +          by (rule da_weakenE) iprover
   5.305          have "PROP ?Hyp (In1l e2) s1 s2" .
   5.306          with da_e2' wt_e2 G normal_s2
   5.307          have "nrm A' \<subseteq> dom (locals (store s2))"
   5.308 @@ -4459,7 +4459,7 @@
   5.309          with da_es obtain A' where
   5.310            da_es': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'" and
   5.311            nrm_A_A': "nrm A \<subseteq> nrm A'"
   5.312 -          by (rule da_weakenE) rules
   5.313 +          by (rule da_weakenE) iprover
   5.314          have "PROP ?Hyp (In3 es) s1 s2" .
   5.315          with da_es' wt_es G normal_s2
   5.316          have "nrm A' \<subseteq> dom (locals (store s2))"
   5.317 @@ -4523,10 +4523,10 @@
   5.318    moreover note wt da
   5.319    moreover from wf have "wf_prog (prg \<lparr>prg=G,cls=C,lcl=L\<rparr>)" by simp
   5.320    ultimately show ?thesis
   5.321 -    using elim by (rule da_good_approxE) rules+
   5.322 +    using elim by (rule da_good_approxE) iprover+
   5.323  qed
   5.324  
   5.325  ML {*
   5.326  Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
   5.327  *}
   5.328 -end
   5.329 \ No newline at end of file
   5.330 +end
     6.1 --- a/src/HOL/Bali/Eval.thy	Thu Sep 22 23:55:42 2005 +0200
     6.2 +++ b/src/HOL/Bali/Eval.thy	Thu Sep 22 23:56:15 2005 +0200
     6.3 @@ -192,7 +192,7 @@
     6.4  defer 
     6.5  apply (case_tac "a' = Null")
     6.6  apply  simp_all
     6.7 -apply rules
     6.8 +apply iprover
     6.9  done
    6.10  
    6.11  constdefs
     7.1 --- a/src/HOL/Bali/Evaln.thy	Thu Sep 22 23:55:42 2005 +0200
     7.2 +++ b/src/HOL/Bali/Evaln.thy	Thu Sep 22 23:56:15 2005 +0200
     7.3 @@ -554,7 +554,7 @@
     7.4    case (Abrupt s t xc)
     7.5    obtain n where
     7.6      "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, Some xc, s)"
     7.7 -    by (rules intro: evaln.Abrupt)
     7.8 +    by (iprover intro: evaln.Abrupt)
     7.9    then show ?case ..
    7.10  next
    7.11    case Skip
    7.12 @@ -563,7 +563,7 @@
    7.13    case (Expr e s0 s1 v)
    7.14    then obtain n where
    7.15      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
    7.16 -    by (rules)
    7.17 +    by (iprover)
    7.18    then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
    7.19      by (rule evaln.Expr) 
    7.20    then show ?case ..
    7.21 @@ -571,7 +571,7 @@
    7.22    case (Lab c l s0 s1)
    7.23    then obtain n where
    7.24      "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
    7.25 -    by (rules)
    7.26 +    by (iprover)
    7.27    then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
    7.28      by (rule evaln.Lab)
    7.29    then show ?case ..
    7.30 @@ -580,7 +580,7 @@
    7.31    then obtain n1 n2 where
    7.32      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
    7.33      "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
    7.34 -    by (rules)
    7.35 +    by (iprover)
    7.36    then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2"
    7.37      by (blast intro: evaln.Comp dest: evaln_max2 )
    7.38    then show ?case ..
    7.39 @@ -589,7 +589,7 @@
    7.40    then obtain n1 n2 where
    7.41      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
    7.42      "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
    7.43 -    by (rules)
    7.44 +    by (iprover)
    7.45    then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2"
    7.46      by (blast intro: evaln.If dest: evaln_max2)
    7.47    then show ?case ..
    7.48 @@ -597,18 +597,18 @@
    7.49    case (Loop b c e l s0 s1 s2 s3)
    7.50    from Loop.hyps obtain n1 where
    7.51      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
    7.52 -    by (rules)
    7.53 +    by (iprover)
    7.54    moreover from Loop.hyps obtain n2 where
    7.55      "if the_Bool b 
    7.56          then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and> 
    7.57                G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
    7.58  	else s3 = s1"
    7.59 -    by simp (rules intro: evaln_nonstrict le_maxI1 le_maxI2)
    7.60 +    by simp (iprover intro: evaln_nonstrict le_maxI1 le_maxI2)
    7.61    ultimately
    7.62    have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
    7.63      apply -
    7.64      apply (rule evaln.Loop)
    7.65 -    apply   (rules intro: evaln_nonstrict intro: le_maxI1)
    7.66 +    apply   (iprover intro: evaln_nonstrict intro: le_maxI1)
    7.67  
    7.68      apply   (auto intro: evaln_nonstrict intro: le_maxI2)
    7.69      done
    7.70 @@ -622,7 +622,7 @@
    7.71    case (Throw a e s0 s1)
    7.72    then obtain n where
    7.73      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
    7.74 -    by (rules)
    7.75 +    by (iprover)
    7.76    then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
    7.77      by (rule evaln.Throw)
    7.78    then show ?case ..
    7.79 @@ -630,7 +630,7 @@
    7.80    case (Try catchC c1 c2 s0 s1 s2 s3 vn)
    7.81    from Try.hyps obtain n1 where
    7.82      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
    7.83 -    by (rules)
    7.84 +    by (iprover)
    7.85    moreover 
    7.86    have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
    7.87    moreover
    7.88 @@ -646,7 +646,7 @@
    7.89    from Fin obtain n1 n2 where 
    7.90      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
    7.91      "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
    7.92 -    by rules
    7.93 +    by iprover
    7.94    moreover
    7.95    have s3: "s3 = (if \<exists>err. x1 = Some (Error err) 
    7.96                       then (x1, s1)
    7.97 @@ -673,17 +673,17 @@
    7.98    case (NewC C a s0 s1 s2)
    7.99    then obtain n where 
   7.100      "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
   7.101 -    by (rules)
   7.102 +    by (iprover)
   7.103    with NewC 
   7.104    have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
   7.105 -    by (rules intro: evaln.NewC)
   7.106 +    by (iprover intro: evaln.NewC)
   7.107    then show ?case ..
   7.108  next
   7.109    case (NewA T a e i s0 s1 s2 s3)
   7.110    then obtain n1 n2 where 
   7.111      "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
   7.112      "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"      
   7.113 -    by (rules)
   7.114 +    by (iprover)
   7.115    moreover
   7.116    have "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
   7.117    ultimately
   7.118 @@ -694,7 +694,7 @@
   7.119    case (Cast castT e s0 s1 s2 v)
   7.120    then obtain n where
   7.121      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   7.122 -    by (rules)
   7.123 +    by (iprover)
   7.124    moreover 
   7.125    have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1" .
   7.126    ultimately
   7.127 @@ -705,7 +705,7 @@
   7.128    case (Inst T b e s0 s1 v)
   7.129    then obtain n where
   7.130      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   7.131 -    by (rules)
   7.132 +    by (iprover)
   7.133    moreover 
   7.134    have "b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)" .
   7.135    ultimately
   7.136 @@ -721,7 +721,7 @@
   7.137    case (UnOp e s0 s1 unop v )
   7.138    then obtain n where
   7.139      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   7.140 -    by (rules)
   7.141 +    by (iprover)
   7.142    hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
   7.143      by (rule evaln.UnOp)
   7.144    then show ?case ..
   7.145 @@ -731,7 +731,7 @@
   7.146      "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
   7.147      "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
   7.148                 else In1r Skip)\<succ>\<midarrow>n2\<rightarrow> (In1 v2, s2)"    
   7.149 -    by (rules)
   7.150 +    by (iprover)
   7.151    hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
   7.152            \<rightarrow> s2"
   7.153      by (blast intro!: evaln.BinOp dest: evaln_max2)
   7.154 @@ -749,7 +749,7 @@
   7.155    case (Acc f s0 s1 v va)
   7.156    then obtain n where
   7.157      "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
   7.158 -    by (rules)
   7.159 +    by (iprover)
   7.160    then
   7.161    have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
   7.162      by (rule evaln.Acc)
   7.163 @@ -759,7 +759,7 @@
   7.164    then obtain n1 n2 where 
   7.165      "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
   7.166      "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"      
   7.167 -    by (rules)
   7.168 +    by (iprover)
   7.169    then
   7.170    have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
   7.171      by (blast intro: evaln.Ass dest: evaln_max2)
   7.172 @@ -769,7 +769,7 @@
   7.173    then obtain n1 n2 where 
   7.174      "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
   7.175      "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
   7.176 -    by (rules)
   7.177 +    by (iprover)
   7.178    then
   7.179    have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
   7.180      by (blast intro: evaln.Cond dest: evaln_max2)
   7.181 @@ -780,7 +780,7 @@
   7.182    then obtain n1 n2 where
   7.183      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
   7.184      "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
   7.185 -    by rules
   7.186 +    by iprover
   7.187    moreover
   7.188    have "invDeclC = invocation_declclass G mode (store s2) a' statT 
   7.189                         \<lparr>name=mn,parTs=pTs'\<rparr>" .
   7.190 @@ -792,7 +792,7 @@
   7.191    from Call.hyps
   7.192    obtain m where 
   7.193      "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name=mn, parTs=pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
   7.194 -    by rules
   7.195 +    by iprover
   7.196    ultimately
   7.197    have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
   7.198              (set_lvars (locals (store s2))) s4"
   7.199 @@ -802,7 +802,7 @@
   7.200    case (Methd D s0 s1 sig v )
   7.201    then obtain n where
   7.202      "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
   7.203 -    by rules
   7.204 +    by iprover
   7.205    then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
   7.206      by (rule evaln.Methd)
   7.207    then show ?case ..
   7.208 @@ -811,7 +811,7 @@
   7.209    from Body.hyps obtain n1 n2 where 
   7.210      evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1" and
   7.211      evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
   7.212 -    by (rules)
   7.213 +    by (iprover)
   7.214    moreover
   7.215    have "s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or> 
   7.216                       fst s2 = Some (Jump (Cont l))
   7.217 @@ -821,33 +821,33 @@
   7.218    have
   7.219       "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
   7.220         \<rightarrow> abupd (absorb Ret) s3"
   7.221 -    by (rules intro: evaln.Body dest: evaln_max2)
   7.222 +    by (iprover intro: evaln.Body dest: evaln_max2)
   7.223    then show ?case ..
   7.224  next
   7.225    case (LVar s vn )
   7.226    obtain n where
   7.227      "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
   7.228 -    by (rules intro: evaln.LVar)
   7.229 +    by (iprover intro: evaln.LVar)
   7.230    then show ?case ..
   7.231  next
   7.232    case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v)
   7.233    then obtain n1 n2 where
   7.234      "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
   7.235      "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
   7.236 -    by rules
   7.237 +    by iprover
   7.238    moreover
   7.239    have "s3 = check_field_access G accC statDeclC fn stat a s2'" 
   7.240         "(v, s2') = fvar statDeclC stat fn a s2" .
   7.241    ultimately
   7.242    have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
   7.243 -    by (rules intro: evaln.FVar dest: evaln_max2)
   7.244 +    by (iprover intro: evaln.FVar dest: evaln_max2)
   7.245    then show ?case ..
   7.246  next
   7.247    case (AVar a e1 e2 i s0 s1 s2 s2' v )
   7.248    then obtain n1 n2 where 
   7.249      "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
   7.250      "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"      
   7.251 -    by rules
   7.252 +    by iprover
   7.253    moreover 
   7.254    have "(v, s2') = avar G i a s2" .
   7.255    ultimately 
   7.256 @@ -856,13 +856,13 @@
   7.257    then show ?case ..
   7.258  next
   7.259    case (Nil s0)
   7.260 -  show ?case by (rules intro: evaln.Nil)
   7.261 +  show ?case by (iprover intro: evaln.Nil)
   7.262  next
   7.263    case (Cons e es s0 s1 s2 v vs)
   7.264    then obtain n1 n2 where 
   7.265      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
   7.266      "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"      
   7.267 -    by rules
   7.268 +    by iprover
   7.269    then
   7.270    have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
   7.271      by (blast intro!: evaln.Cons dest: evaln_max2)
     8.1 --- a/src/HOL/Bali/TypeSafe.thy	Thu Sep 22 23:55:42 2005 +0200
     8.2 +++ b/src/HOL/Bali/TypeSafe.thy	Thu Sep 22 23:56:15 2005 +0200
     8.3 @@ -1233,7 +1233,7 @@
     8.4    next
     8.5      case (Cons y ys')
     8.6      have "(tab(x\<mapsto>y)(xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y)(xs[\<mapsto>]ys')) z"
     8.7 -      by (rules intro: Hyps map_upd_cong_ext)
     8.8 +      by (iprover intro: Hyps map_upd_cong_ext)
     8.9      with Cons show ?thesis
    8.10        by simp
    8.11    qed
    8.12 @@ -1701,7 +1701,7 @@
    8.13  	  by cases simp+
    8.14  	from eval_e1 wt_e1 da_e1 wf normal_s1 
    8.15  	have "nrm E1' \<subseteq> dom (locals (store s1))"
    8.16 -	  by (cases rule: da_good_approxE') rules
    8.17 +	  by (cases rule: da_good_approxE') iprover
    8.18  	with da_e2 show ?thesis
    8.19  	  using that by (rule da_weakenE) (simp add: True)
    8.20        qed
    8.21 @@ -1836,7 +1836,7 @@
    8.22        proof -
    8.23  	from eval_c1 wt_c1 da_c1 wf True
    8.24  	have "nrm C1 \<subseteq> dom (locals (store s1))"
    8.25 -	  by (cases rule: da_good_approxE') rules
    8.26 +	  by (cases rule: da_good_approxE') iprover
    8.27  	with da_c2 show ?thesis
    8.28  	  by (rule da_weakenE)
    8.29        qed
    8.30 @@ -2806,7 +2806,7 @@
    8.31  	proof -
    8.32  	  from eval_var wt_var da_var wf normal_s1
    8.33  	  have "nrm V \<subseteq>  dom (locals (store s1))"
    8.34 -	    by (cases rule: da_good_approxE') rules
    8.35 +	    by (cases rule: da_good_approxE') iprover
    8.36  	  with da_e show ?thesis
    8.37  	    by (rule da_weakenE) 
    8.38  	qed
    8.39 @@ -3094,7 +3094,7 @@
    8.40        proof -
    8.41  	from eval_e wt_e da_e wf normal_s1
    8.42  	have "nrm E \<subseteq>  dom (locals (store s1))"
    8.43 -	  by (cases rule: da_good_approxE') rules
    8.44 +	  by (cases rule: da_good_approxE') iprover
    8.45  	with da_args show ?thesis
    8.46  	  by (rule da_weakenE) 
    8.47        qed
    8.48 @@ -3256,7 +3256,7 @@
    8.49                 ,lcl=callee_lcl invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> (mthd dynM)
    8.50                 \<rparr> \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'" and
    8.51                res: "Result \<in> nrm M'"
    8.52 -	      by (rule wf_mdeclE) rules
    8.53 +	      by (rule wf_mdeclE) iprover
    8.54  	    from da_body is_static_eq L' have
    8.55  	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
    8.56                   \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'"
    8.57 @@ -3308,7 +3308,7 @@
    8.58  	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> \<turnstile> dom (locals (store s3')) 
    8.59                       \<guillemotright>\<langle>Body (declclass dynM) (stmt (mbody (mthd dynM)))\<rangle>\<guillemotright> M3"
    8.60  	      using da
    8.61 -	      by (rules intro: da.Body assigned.select_convs)
    8.62 +	      by (iprover intro: da.Body assigned.select_convs)
    8.63  	    from _ this [simplified]
    8.64  	    show ?thesis
    8.65  	      by (rule da.Methd [simplified,elim_format])
    8.66 @@ -3672,7 +3672,7 @@
    8.67        proof -
    8.68  	from eval_e1 wt_e1 da_e1 wf True
    8.69  	have "nrm E1 \<subseteq> dom (locals (store s1))"
    8.70 -	  by (cases rule: da_good_approxE') rules
    8.71 +	  by (cases rule: da_good_approxE') iprover
    8.72  	with da_e2 show ?thesis
    8.73  	  by (rule da_weakenE)
    8.74        qed
    8.75 @@ -3768,7 +3768,7 @@
    8.76        proof -
    8.77  	from eval_e wt_e da_e wf True
    8.78  	have "nrm E \<subseteq> dom (locals (store s1))"
    8.79 -	  by (cases rule: da_good_approxE') rules
    8.80 +	  by (cases rule: da_good_approxE') iprover
    8.81  	with da_es show ?thesis
    8.82  	  by (rule da_weakenE)
    8.83        qed
    8.84 @@ -3806,7 +3806,7 @@
    8.85                    error_free s0 = error_free s1\<rbrakk> \<Longrightarrow> P"
    8.86    shows "P"
    8.87  using eval wt da wf conf
    8.88 -by (rule eval_type_sound [elim_format]) (rules intro: elim) 
    8.89 +by (rule eval_type_sound [elim_format]) (iprover intro: elim) 
    8.90  
    8.91   
    8.92  corollary eval_ts: 
    8.93 @@ -3995,19 +3995,19 @@
    8.94  	proof -
    8.95  	  from eval_c1 wt_c1 da_c1 wf normal_s1
    8.96  	  have "nrm C1 \<subseteq> dom (locals (store s1))"
    8.97 -	    by (cases rule: da_good_approxE') rules
    8.98 +	    by (cases rule: da_good_approxE') iprover
    8.99  	  with da_c2 show ?thesis
   8.100  	    by (rule da_weakenE)
   8.101  	qed
   8.102  	with wt_c2 have "P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2"
   8.103  	  by (rule Comp.hyps)
   8.104  	with da show ?thesis
   8.105 -	  using elim by rules
   8.106 +	  using elim by iprover
   8.107        qed
   8.108      }
   8.109      with eval_c1 eval_c2 wt_c1 wt_c2 da_c1 P_c1 
   8.110      show ?case
   8.111 -      by (rule comp) rules+
   8.112 +      by (rule comp) iprover+
   8.113    next
   8.114      case (If b c1 c2 e s0 s1 s2 L accC T A)
   8.115      have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
   8.116 @@ -4058,12 +4058,12 @@
   8.117  	with wt_then_else
   8.118  	have "P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2"
   8.119  	  by (rule If.hyps)
   8.120 -	with da show ?thesis using elim by rules
   8.121 +	with da show ?thesis using elim by iprover
   8.122        qed
   8.123      }
   8.124      with eval_e eval_then_else wt_e wt_then_else da_e P_e
   8.125      show ?case
   8.126 -      by (rule if) rules+
   8.127 +      by (rule if) iprover+
   8.128    next
   8.129      oops
   8.130  
     9.1 --- a/src/HOL/Datatype_Universe.thy	Thu Sep 22 23:55:42 2005 +0200
     9.2 +++ b/src/HOL/Datatype_Universe.thy	Thu Sep 22 23:56:15 2005 +0200
     9.3 @@ -218,17 +218,17 @@
     9.4  
     9.5  lemma Scons_inject1: "Scons M N = Scons M' N' ==> M=M'"
     9.6  apply (erule equalityE)
     9.7 -apply (rules intro: equalityI Scons_inject_lemma1)
     9.8 +apply (iprover intro: equalityI Scons_inject_lemma1)
     9.9  done
    9.10  
    9.11  lemma Scons_inject2: "Scons M N = Scons M' N' ==> N=N'"
    9.12  apply (erule equalityE)
    9.13 -apply (rules intro: equalityI Scons_inject_lemma2)
    9.14 +apply (iprover intro: equalityI Scons_inject_lemma2)
    9.15  done
    9.16  
    9.17  lemma Scons_inject:
    9.18      "[| Scons M N = Scons M' N';  [| M=M';  N=N' |] ==> P |] ==> P"
    9.19 -by (rules dest: Scons_inject1 Scons_inject2)
    9.20 +by (iprover dest: Scons_inject1 Scons_inject2)
    9.21  
    9.22  lemma Scons_Scons_eq [iff]: "(Scons M N = Scons M' N') = (M=M' & N=N')"
    9.23  by (blast elim!: Scons_inject)
    10.1 --- a/src/HOL/Equiv_Relations.thy	Thu Sep 22 23:55:42 2005 +0200
    10.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Sep 22 23:56:15 2005 +0200
    10.3 @@ -35,7 +35,7 @@
    10.4    apply (unfold equiv_def)
    10.5    apply clarify
    10.6    apply (rule equalityI)
    10.7 -   apply (rules intro: sym_trans_comp_subset refl_comp_subset)+
    10.8 +   apply (iprover intro: sym_trans_comp_subset refl_comp_subset)+
    10.9    done
   10.10  
   10.11  text {* Second half. *}
   10.12 @@ -73,7 +73,7 @@
   10.13  
   10.14  lemma eq_equiv_class:
   10.15      "r``{a} = r``{b} ==> equiv A r ==> b \<in> A ==> (a, b) \<in> r"
   10.16 -  by (rules intro: equalityD2 subset_equiv_class)
   10.17 +  by (iprover intro: equalityD2 subset_equiv_class)
   10.18  
   10.19  lemma equiv_class_nondisjoint:
   10.20      "equiv A r ==> x \<in> (r``{a} \<inter> r``{b}) ==> (a, b) \<in> r"
    11.1 --- a/src/HOL/Finite_Set.thy	Thu Sep 22 23:55:42 2005 +0200
    11.2 +++ b/src/HOL/Finite_Set.thy	Thu Sep 22 23:56:15 2005 +0200
    11.3 @@ -604,7 +604,7 @@
    11.4  	  have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
    11.5  	  with AbB have "finite ?D" by simp
    11.6  	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z"
    11.7 -	    using finite_imp_foldSet by rules
    11.8 +	    using finite_imp_foldSet by iprover
    11.9  	  moreover have cinB: "c \<in> B" using B by auto
   11.10  	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z"
   11.11  	    by(rule Diff1_foldSet)
    12.1 --- a/src/HOL/FixedPoint.thy	Thu Sep 22 23:55:42 2005 +0200
    12.2 +++ b/src/HOL/FixedPoint.thy	Thu Sep 22 23:56:15 2005 +0200
    12.3 @@ -31,13 +31,13 @@
    12.4  by (auto simp add: lfp_def)
    12.5  
    12.6  lemma lfp_lemma2: "mono(f) ==> f(lfp(f)) \<subseteq> lfp(f)"
    12.7 -by (rules intro: lfp_greatest subset_trans monoD lfp_lowerbound)
    12.8 +by (iprover intro: lfp_greatest subset_trans monoD lfp_lowerbound)
    12.9  
   12.10  lemma lfp_lemma3: "mono(f) ==> lfp(f) \<subseteq> f(lfp(f))"
   12.11 -by (rules intro: lfp_lemma2 monoD lfp_lowerbound)
   12.12 +by (iprover intro: lfp_lemma2 monoD lfp_lowerbound)
   12.13  
   12.14  lemma lfp_unfold: "mono(f) ==> lfp(f) = f(lfp(f))"
   12.15 -by (rules intro: equalityI lfp_lemma2 lfp_lemma3)
   12.16 +by (iprover intro: equalityI lfp_lemma2 lfp_lemma3)
   12.17  
   12.18  subsection{*General induction rules for greatest fixed points*}
   12.19  
   12.20 @@ -105,13 +105,13 @@
   12.21  by (auto simp add: gfp_def)
   12.22  
   12.23  lemma gfp_lemma2: "mono(f) ==> gfp(f) \<subseteq> f(gfp(f))"
   12.24 -by (rules intro: gfp_least subset_trans monoD gfp_upperbound)
   12.25 +by (iprover intro: gfp_least subset_trans monoD gfp_upperbound)
   12.26  
   12.27  lemma gfp_lemma3: "mono(f) ==> f(gfp(f)) \<subseteq> gfp(f)"
   12.28 -by (rules intro: gfp_lemma2 monoD gfp_upperbound)
   12.29 +by (iprover intro: gfp_lemma2 monoD gfp_upperbound)
   12.30  
   12.31  lemma gfp_unfold: "mono(f) ==> gfp(f) = f(gfp(f))"
   12.32 -by (rules intro: equalityI gfp_lemma2 gfp_lemma3)
   12.33 +by (iprover intro: equalityI gfp_lemma2 gfp_lemma3)
   12.34  
   12.35  subsection{*Coinduction rules for greatest fixed points*}
   12.36  
   12.37 @@ -141,7 +141,7 @@
   12.38    @{term lfp} and @{term gfp}*}
   12.39  
   12.40  lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un X Un B)"
   12.41 -by (rules intro: subset_refl monoI Un_mono monoD)
   12.42 +by (iprover intro: subset_refl monoI Un_mono monoD)
   12.43  
   12.44  lemma coinduct3_lemma:
   12.45       "[| X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f)));  mono(f) |]
    13.1 --- a/src/HOL/Fun.thy	Thu Sep 22 23:55:42 2005 +0200
    13.2 +++ b/src/HOL/Fun.thy	Thu Sep 22 23:56:15 2005 +0200
    13.3 @@ -429,11 +429,11 @@
    13.4  proof 
    13.5    assume "inj_on (swap a b f) A"
    13.6    with A have "inj_on (swap a b (swap a b f)) A" 
    13.7 -    by (rules intro: inj_on_imp_inj_on_swap) 
    13.8 +    by (iprover intro: inj_on_imp_inj_on_swap) 
    13.9    thus "inj_on f A" by simp 
   13.10  next
   13.11    assume "inj_on f A"
   13.12 -  with A show "inj_on (swap a b f) A" by (rules intro: inj_on_imp_inj_on_swap)
   13.13 +  with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
   13.14  qed
   13.15  
   13.16  lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
    14.1 --- a/src/HOL/HOL.thy	Thu Sep 22 23:55:42 2005 +0200
    14.2 +++ b/src/HOL/HOL.thy	Thu Sep 22 23:56:15 2005 +0200
    14.3 @@ -287,7 +287,7 @@
    14.4  subsection {*Equality of booleans -- iff*}
    14.5  
    14.6  lemma iffI: assumes prems: "P ==> Q" "Q ==> P" shows "P=Q"
    14.7 -apply (rules intro: iff [THEN mp, THEN mp] impI prems)
    14.8 +apply (iprover intro: iff [THEN mp, THEN mp] impI prems)
    14.9  done
   14.10  
   14.11  lemma iffD2: "[| P=Q; Q |] ==> P"
   14.12 @@ -307,7 +307,7 @@
   14.13    assumes major: "P=Q"
   14.14        and minor: "[| P --> Q; Q --> P |] ==> R"
   14.15    shows "R"
   14.16 -by (rules intro: minor impI major [THEN iffD2] major [THEN iffD1])
   14.17 +by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1])
   14.18  
   14.19  
   14.20  subsection {*True*}
   14.21 @@ -318,7 +318,7 @@
   14.22  done
   14.23  
   14.24  lemma eqTrueI: "P ==> P=True"
   14.25 -by (rules intro: iffI TrueI)
   14.26 +by (iprover intro: iffI TrueI)
   14.27  
   14.28  lemma eqTrueE: "P=True ==> P"
   14.29  apply (erule iffD2)
   14.30 @@ -330,7 +330,7 @@
   14.31  
   14.32  lemma allI: assumes p: "!!x::'a. P(x)" shows "ALL x. P(x)"
   14.33  apply (unfold All_def)
   14.34 -apply (rules intro: ext eqTrueI p)
   14.35 +apply (iprover intro: ext eqTrueI p)
   14.36  done
   14.37  
   14.38  lemma spec: "ALL x::'a. P(x) ==> P(x)"
   14.39 @@ -343,13 +343,13 @@
   14.40    assumes major: "ALL x. P(x)"
   14.41        and minor: "P(x) ==> R"
   14.42    shows "R"
   14.43 -by (rules intro: minor major [THEN spec])
   14.44 +by (iprover intro: minor major [THEN spec])
   14.45  
   14.46  lemma all_dupE:
   14.47    assumes major: "ALL x. P(x)"
   14.48        and minor: "[| P(x); ALL x. P(x) |] ==> R"
   14.49    shows "R"
   14.50 -by (rules intro: minor major major [THEN spec])
   14.51 +by (iprover intro: minor major major [THEN spec])
   14.52  
   14.53  
   14.54  subsection {*False*}
   14.55 @@ -370,7 +370,7 @@
   14.56    assumes p: "P ==> False"
   14.57    shows "~P"
   14.58  apply (unfold not_def)
   14.59 -apply (rules intro: impI p)
   14.60 +apply (iprover intro: impI p)
   14.61  done
   14.62  
   14.63  lemma False_not_True: "False ~= True"
   14.64 @@ -399,24 +399,24 @@
   14.65  lemma impE:
   14.66    assumes "P-->Q" "P" "Q ==> R"
   14.67    shows "R"
   14.68 -by (rules intro: prems mp)
   14.69 +by (iprover intro: prems mp)
   14.70  
   14.71  (* Reduces Q to P-->Q, allowing substitution in P. *)
   14.72  lemma rev_mp: "[| P;  P --> Q |] ==> Q"
   14.73 -by (rules intro: mp)
   14.74 +by (iprover intro: mp)
   14.75  
   14.76  lemma contrapos_nn:
   14.77    assumes major: "~Q"
   14.78        and minor: "P==>Q"
   14.79    shows "~P"
   14.80 -by (rules intro: notI minor major [THEN notE])
   14.81 +by (iprover intro: notI minor major [THEN notE])
   14.82  
   14.83  (*not used at all, but we already have the other 3 combinations *)
   14.84  lemma contrapos_pn:
   14.85    assumes major: "Q"
   14.86        and minor: "P ==> ~Q"
   14.87    shows "~P"
   14.88 -by (rules intro: notI minor major notE)
   14.89 +by (iprover intro: notI minor major notE)
   14.90  
   14.91  lemma not_sym: "t ~= s ==> s ~= t"
   14.92  apply (erule contrapos_nn)
   14.93 @@ -436,7 +436,7 @@
   14.94  
   14.95  lemma exI: "P x ==> EX x::'a. P x"
   14.96  apply (unfold Ex_def)
   14.97 -apply (rules intro: allI allE impI mp)
   14.98 +apply (iprover intro: allI allE impI mp)
   14.99  done
  14.100  
  14.101  lemma exE:
  14.102 @@ -444,7 +444,7 @@
  14.103        and minor: "!!x. P(x) ==> Q"
  14.104    shows "Q"
  14.105  apply (rule major [unfolded Ex_def, THEN spec, THEN mp])
  14.106 -apply (rules intro: impI [THEN allI] minor)
  14.107 +apply (iprover intro: impI [THEN allI] minor)
  14.108  done
  14.109  
  14.110  
  14.111 @@ -452,17 +452,17 @@
  14.112  
  14.113  lemma conjI: "[| P; Q |] ==> P&Q"
  14.114  apply (unfold and_def)
  14.115 -apply (rules intro: impI [THEN allI] mp)
  14.116 +apply (iprover intro: impI [THEN allI] mp)
  14.117  done
  14.118  
  14.119  lemma conjunct1: "[| P & Q |] ==> P"
  14.120  apply (unfold and_def)
  14.121 -apply (rules intro: impI dest: spec mp)
  14.122 +apply (iprover intro: impI dest: spec mp)
  14.123  done
  14.124  
  14.125  lemma conjunct2: "[| P & Q |] ==> Q"
  14.126  apply (unfold and_def)
  14.127 -apply (rules intro: impI dest: spec mp)
  14.128 +apply (iprover intro: impI dest: spec mp)
  14.129  done
  14.130  
  14.131  lemma conjE:
  14.132 @@ -476,19 +476,19 @@
  14.133  
  14.134  lemma context_conjI:
  14.135    assumes prems: "P" "P ==> Q" shows "P & Q"
  14.136 -by (rules intro: conjI prems)
  14.137 +by (iprover intro: conjI prems)
  14.138  
  14.139  
  14.140  subsection {*Disjunction*}
  14.141  
  14.142  lemma disjI1: "P ==> P|Q"
  14.143  apply (unfold or_def)
  14.144 -apply (rules intro: allI impI mp)
  14.145 +apply (iprover intro: allI impI mp)
  14.146  done
  14.147  
  14.148  lemma disjI2: "Q ==> P|Q"
  14.149  apply (unfold or_def)
  14.150 -apply (rules intro: allI impI mp)
  14.151 +apply (iprover intro: allI impI mp)
  14.152  done
  14.153  
  14.154  lemma disjE:
  14.155 @@ -496,7 +496,7 @@
  14.156        and minorP: "P ==> R"
  14.157        and minorQ: "Q ==> R"
  14.158    shows "R"
  14.159 -by (rules intro: minorP minorQ impI
  14.160 +by (iprover intro: minorP minorQ impI
  14.161                   major [unfolded or_def, THEN spec, THEN mp, THEN mp])
  14.162  
  14.163  
  14.164 @@ -536,7 +536,7 @@
  14.165    assumes p1: "Q"
  14.166        and p2: "~P ==> ~Q"
  14.167    shows "P"
  14.168 -by (rules intro: classical p1 p2 notE)
  14.169 +by (iprover intro: classical p1 p2 notE)
  14.170  
  14.171  
  14.172  subsection {*Unique existence*}
  14.173 @@ -544,14 +544,14 @@
  14.174  lemma ex1I:
  14.175    assumes prems: "P a" "!!x. P(x) ==> x=a"
  14.176    shows "EX! x. P(x)"
  14.177 -by (unfold Ex1_def, rules intro: prems exI conjI allI impI)
  14.178 +by (unfold Ex1_def, iprover intro: prems exI conjI allI impI)
  14.179  
  14.180  text{*Sometimes easier to use: the premises have no shared variables.  Safe!*}
  14.181  lemma ex_ex1I:
  14.182    assumes ex_prem: "EX x. P(x)"
  14.183        and eq: "!!x y. [| P(x); P(y) |] ==> x=y"
  14.184    shows "EX! x. P(x)"
  14.185 -by (rules intro: ex_prem [THEN exE] ex1I eq)
  14.186 +by (iprover intro: ex_prem [THEN exE] ex1I eq)
  14.187  
  14.188  lemma ex1E:
  14.189    assumes major: "EX! x. P(x)"
  14.190 @@ -559,7 +559,7 @@
  14.191    shows "R"
  14.192  apply (rule major [unfolded Ex1_def, THEN exE])
  14.193  apply (erule conjE)
  14.194 -apply (rules intro: minor)
  14.195 +apply (iprover intro: minor)
  14.196  done
  14.197  
  14.198  lemma ex1_implies_ex: "EX! x. P x ==> EX x. P x"
  14.199 @@ -586,7 +586,7 @@
  14.200  lemma theI:
  14.201    assumes "P a" and "!!x. P x ==> x=a"
  14.202    shows "P (THE x. P x)"
  14.203 -by (rules intro: prems the_equality [THEN ssubst])
  14.204 +by (iprover intro: prems the_equality [THEN ssubst])
  14.205  
  14.206  lemma theI': "EX! x. P x ==> P (THE x. P x)"
  14.207  apply (erule ex1E)
  14.208 @@ -600,7 +600,7 @@
  14.209  lemma theI2:
  14.210    assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x"
  14.211    shows "Q (THE x. P x)"
  14.212 -by (rules intro: prems theI)
  14.213 +by (iprover intro: prems theI)
  14.214  
  14.215  lemma the1_equality: "[| EX!x. P x; P a |] ==> (THE x. P x) = a"
  14.216  apply (rule the_equality)
  14.217 @@ -627,11 +627,11 @@
  14.218  lemma disjCI:
  14.219    assumes "~Q ==> P" shows "P|Q"
  14.220  apply (rule classical)
  14.221 -apply (rules intro: prems disjI1 disjI2 notI elim: notE)
  14.222 +apply (iprover intro: prems disjI1 disjI2 notI elim: notE)
  14.223  done
  14.224  
  14.225  lemma excluded_middle: "~P | P"
  14.226 -by (rules intro: disjCI)
  14.227 +by (iprover intro: disjCI)
  14.228  
  14.229  text{*case distinction as a natural deduction rule. Note that @{term "~P"}
  14.230     is the second case, not the first.*}
  14.231 @@ -650,7 +650,7 @@
  14.232        and minor: "~P ==> R" "Q ==> R"
  14.233    shows "R"
  14.234  apply (rule excluded_middle [of P, THEN disjE])
  14.235 -apply (rules intro: minor major [THEN mp])+
  14.236 +apply (iprover intro: minor major [THEN mp])+
  14.237  done
  14.238  
  14.239  (*This version of --> elimination works on Q before P.  It works best for
  14.240 @@ -661,7 +661,7 @@
  14.241        and minor: "Q ==> R" "~P ==> R"
  14.242    shows "R"
  14.243  apply (rule excluded_middle [of P, THEN disjE])
  14.244 -apply (rules intro: minor major [THEN mp])+
  14.245 +apply (iprover intro: minor major [THEN mp])+
  14.246  done
  14.247  
  14.248  (*Classical <-> elimination. *)
  14.249 @@ -670,14 +670,14 @@
  14.250        and minor: "[| P; Q |] ==> R"  "[| ~P; ~Q |] ==> R"
  14.251    shows "R"
  14.252  apply (rule major [THEN iffE])
  14.253 -apply (rules intro: minor elim: impCE notE)
  14.254 +apply (iprover intro: minor elim: impCE notE)
  14.255  done
  14.256  
  14.257  lemma exCI:
  14.258    assumes "ALL x. ~P(x) ==> P(a)"
  14.259    shows "EX x. P(x)"
  14.260  apply (rule ccontr)
  14.261 -apply (rules intro: prems exI allI notI notE [of "\<exists>x. P x"])
  14.262 +apply (iprover intro: prems exI allI notI notE [of "\<exists>x. P x"])
  14.263  done
  14.264  
  14.265  
  14.266 @@ -949,10 +949,10 @@
  14.267      "!!P. (EX x. t=x & P(x)) = P(t)"
  14.268      "!!P. (ALL x. x=t --> P(x)) = P(t)"
  14.269      "!!P. (ALL x. t=x --> P(x)) = P(t)"
  14.270 -  by (blast, blast, blast, blast, blast, rules+)
  14.271 +  by (blast, blast, blast, blast, blast, iprover+)
  14.272  
  14.273  lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
  14.274 -  by rules
  14.275 +  by iprover
  14.276  
  14.277  lemma ex_simps:
  14.278    "!!P Q. (EX x. P x & Q)   = ((EX x. P x) & Q)"
  14.279 @@ -962,7 +962,7 @@
  14.280    "!!P Q. (EX x. P x --> Q) = ((ALL x. P x) --> Q)"
  14.281    "!!P Q. (EX x. P --> Q x) = (P --> (EX x. Q x))"
  14.282    -- {* Miniscoping: pushing in existential quantifiers. *}
  14.283 -  by (rules | blast)+
  14.284 +  by (iprover | blast)+
  14.285  
  14.286  lemma all_simps:
  14.287    "!!P Q. (ALL x. P x & Q)   = ((ALL x. P x) & Q)"
  14.288 @@ -972,7 +972,7 @@
  14.289    "!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)"
  14.290    "!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))"
  14.291    -- {* Miniscoping: pushing in universal quantifiers. *}
  14.292 -  by (rules | blast)+
  14.293 +  by (iprover | blast)+
  14.294  
  14.295  lemma disj_absorb: "(A | A) = A"
  14.296    by blast
  14.297 @@ -989,28 +989,28 @@
  14.298  lemma eq_ac:
  14.299    shows eq_commute: "(a=b) = (b=a)"
  14.300      and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))"
  14.301 -    and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (rules, blast+)
  14.302 -lemma neq_commute: "(a~=b) = (b~=a)" by rules
  14.303 +    and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (iprover, blast+)
  14.304 +lemma neq_commute: "(a~=b) = (b~=a)" by iprover
  14.305  
  14.306  lemma conj_comms:
  14.307    shows conj_commute: "(P&Q) = (Q&P)"
  14.308 -    and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by rules+
  14.309 -lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by rules
  14.310 +    and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+
  14.311 +lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover
  14.312  
  14.313  lemma disj_comms:
  14.314    shows disj_commute: "(P|Q) = (Q|P)"
  14.315 -    and disj_left_commute: "(P|(Q|R)) = (Q|(P|R))" by rules+
  14.316 -lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by rules
  14.317 +    and disj_left_commute: "(P|(Q|R)) = (Q|(P|R))" by iprover+
  14.318 +lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by iprover
  14.319  
  14.320 -lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by rules
  14.321 -lemma conj_disj_distribR: "((P|Q)&R) = (P&R | Q&R)" by rules
  14.322 +lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by iprover
  14.323 +lemma conj_disj_distribR: "((P|Q)&R) = (P&R | Q&R)" by iprover
  14.324  
  14.325 -lemma disj_conj_distribL: "(P|(Q&R)) = ((P|Q) & (P|R))" by rules
  14.326 -lemma disj_conj_distribR: "((P&Q)|R) = ((P|R) & (Q|R))" by rules
  14.327 +lemma disj_conj_distribL: "(P|(Q&R)) = ((P|Q) & (P|R))" by iprover
  14.328 +lemma disj_conj_distribR: "((P&Q)|R) = ((P|R) & (Q|R))" by iprover
  14.329  
  14.330 -lemma imp_conjR: "(P --> (Q&R)) = ((P-->Q) & (P-->R))" by rules
  14.331 -lemma imp_conjL: "((P&Q) -->R)  = (P --> (Q --> R))" by rules
  14.332 -lemma imp_disjL: "((P|Q) --> R) = ((P-->R)&(Q-->R))" by rules
  14.333 +lemma imp_conjR: "(P --> (Q&R)) = ((P-->Q) & (P-->R))" by iprover
  14.334 +lemma imp_conjL: "((P&Q) -->R)  = (P --> (Q --> R))" by iprover
  14.335 +lemma imp_disjL: "((P|Q) --> R) = ((P-->R)&(Q-->R))" by iprover
  14.336  
  14.337  text {* These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}. *}
  14.338  lemma imp_disj_not1: "(P --> Q | R) = (~Q --> P --> R)" by blast
  14.339 @@ -1019,7 +1019,7 @@
  14.340  lemma imp_disj1: "((P-->Q)|R) = (P--> Q|R)" by blast
  14.341  lemma imp_disj2: "(Q|(P-->R)) = (P--> Q|R)" by blast
  14.342  
  14.343 -lemma de_Morgan_disj: "(~(P | Q)) = (~P & ~Q)" by rules
  14.344 +lemma de_Morgan_disj: "(~(P | Q)) = (~P & ~Q)" by iprover
  14.345  lemma de_Morgan_conj: "(~(P & Q)) = (~P | ~Q)" by blast
  14.346  lemma not_imp: "(~(P --> Q)) = (P & ~Q)" by blast
  14.347  lemma not_iff: "(P~=Q) = (P = (~Q))" by blast
  14.348 @@ -1028,7 +1028,7 @@
  14.349    by blast
  14.350  lemma imp_conv_disj: "(P --> Q) = ((~P) | Q)" by blast
  14.351  
  14.352 -lemma iff_conv_conj_imp: "(P = Q) = ((P --> Q) & (Q --> P))" by rules
  14.353 +lemma iff_conv_conj_imp: "(P = Q) = ((P --> Q) & (Q --> P))" by iprover
  14.354  
  14.355  
  14.356  lemma cases_simp: "((P --> Q) & (~P --> Q)) = Q"
  14.357 @@ -1038,11 +1038,11 @@
  14.358  
  14.359  lemma not_all: "(~ (! x. P(x))) = (? x.~P(x))" by blast
  14.360  lemma imp_all: "((! x. P x) --> Q) = (? x. P x --> Q)" by blast
  14.361 -lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by rules
  14.362 -lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by rules
  14.363 +lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by iprover
  14.364 +lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by iprover
  14.365  
  14.366 -lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by rules
  14.367 -lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by rules
  14.368 +lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by iprover
  14.369 +lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by iprover
  14.370  
  14.371  text {*
  14.372    \medskip The @{text "&"} congruence rule: not included by default!
  14.373 @@ -1050,11 +1050,11 @@
  14.374  
  14.375  lemma conj_cong:
  14.376      "(P = P') ==> (P' ==> (Q = Q')) ==> ((P & Q) = (P' & Q'))"
  14.377 -  by rules
  14.378 +  by iprover
  14.379  
  14.380  lemma rev_conj_cong:
  14.381      "(Q = Q') ==> (Q' ==> (P = P')) ==> ((P & Q) = (P' & Q'))"
  14.382 -  by rules
  14.383 +  by iprover
  14.384  
  14.385  text {* The @{text "|"} congruence rule: not included by default! *}
  14.386  
  14.387 @@ -1063,7 +1063,7 @@
  14.388    by blast
  14.389  
  14.390  lemma eq_sym_conv: "(x = y) = (y = x)"
  14.391 -  by rules
  14.392 +  by iprover
  14.393  
  14.394  
  14.395  text {* \medskip if-then-else rules *}
  14.396 @@ -1109,8 +1109,8 @@
  14.397    apply (simplesubst split_if, blast)
  14.398    done
  14.399  
  14.400 -lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) rules
  14.401 -lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) rules
  14.402 +lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) iprover
  14.403 +lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) iprover
  14.404  
  14.405  text {* \medskip let rules for simproc *}
  14.406  
  14.407 @@ -1285,11 +1285,11 @@
  14.408  
  14.409  lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) =
  14.410      induct_conj (induct_forall A) (induct_forall B)"
  14.411 -  by (unfold induct_forall_def induct_conj_def) rules
  14.412 +  by (unfold induct_forall_def induct_conj_def) iprover
  14.413  
  14.414  lemma induct_implies_conj: "induct_implies C (induct_conj A B) =
  14.415      induct_conj (induct_implies C A) (induct_implies C B)"
  14.416 -  by (unfold induct_implies_def induct_conj_def) rules
  14.417 +  by (unfold induct_implies_def induct_conj_def) iprover
  14.418  
  14.419  lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)"
  14.420  proof
    15.1 --- a/src/HOL/Induct/PropLog.thy	Thu Sep 22 23:55:42 2005 +0200
    15.2 +++ b/src/HOL/Induct/PropLog.thy	Thu Sep 22 23:56:15 2005 +0200
    15.3 @@ -236,12 +236,12 @@
    15.4  apply (rule hyps_subset [THEN hyps_finite [THEN finite_subset_induct]])
    15.5   apply (simp add: sat_thms_p, safe)
    15.6   txt{*Case @{text"hyps p t-insert(#v,Y) |- p"} *}
    15.7 - apply (rules intro: thms_excluded_middle_rule 
    15.8 + apply (iprover intro: thms_excluded_middle_rule 
    15.9  		     insert_Diff_same [THEN weaken_left]
   15.10                       insert_Diff_subset2 [THEN weaken_left] 
   15.11                       hyps_Diff [THEN Diff_weaken_left])
   15.12  txt{*Case @{text"hyps p t-insert(#v -> false,Y) |- p"} *}
   15.13 - apply (rules intro: thms_excluded_middle_rule 
   15.14 + apply (iprover intro: thms_excluded_middle_rule 
   15.15  		     insert_Diff_same [THEN weaken_left]
   15.16                       insert_Diff_subset2 [THEN weaken_left] 
   15.17                       hyps_insert [THEN Diff_weaken_left])
   15.18 @@ -260,7 +260,7 @@
   15.19  theorem completeness [rule_format]: "finite H ==> \<forall>p. H |= p --> H |- p"
   15.20  apply (erule finite_induct)
   15.21   apply (blast intro: completeness_0)
   15.22 -apply (rules intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP])
   15.23 +apply (iprover intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP])
   15.24  done
   15.25  
   15.26  theorem syntax_iff_semantics: "finite H ==> (H |- p) = (H |= p)"
    16.1 --- a/src/HOL/Integ/Presburger.thy	Thu Sep 22 23:55:42 2005 +0200
    16.2 +++ b/src/HOL/Integ/Presburger.thy	Thu Sep 22 23:56:15 2005 +0200
    16.3 @@ -244,10 +244,10 @@
    16.4  text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
    16.5  
    16.6  lemma P_eqtrue: "(P=True) = P"
    16.7 -  by rules
    16.8 +  by iprover
    16.9  
   16.10  lemma P_eqfalse: "(P=False) = (~P)"
   16.11 -  by rules
   16.12 +  by iprover
   16.13  
   16.14  text {*
   16.15    \medskip Theorems for the generation of the bachwards direction of
   16.16 @@ -831,10 +831,10 @@
   16.17    by simp
   16.18  
   16.19  lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
   16.20 -  by rules
   16.21 +  by iprover
   16.22  
   16.23  lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))"
   16.24 -  by rules
   16.25 +  by iprover
   16.26  
   16.27  lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j)))
   16.28  ==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) "
   16.29 @@ -952,13 +952,13 @@
   16.30    apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
   16.31      nat_0_le cong add: conj_cong)
   16.32    apply (rule iffI)
   16.33 -  apply rules
   16.34 +  apply iprover
   16.35    apply (erule exE)
   16.36    apply (case_tac "x=0")
   16.37    apply (rule_tac x=0 in exI)
   16.38    apply simp
   16.39    apply (case_tac "0 \<le> k")
   16.40 -  apply rules
   16.41 +  apply iprover
   16.42    apply (simp add: linorder_not_le)
   16.43    apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
   16.44    apply assumption
    17.1 --- a/src/HOL/Lambda/Commutation.thy	Thu Sep 22 23:55:42 2005 +0200
    17.2 +++ b/src/HOL/Lambda/Commutation.thy	Thu Sep 22 23:56:15 2005 +0200
    17.3 @@ -154,7 +154,7 @@
    17.4    proof (rule converse_rtranclE)
    17.5      assume "x = b"
    17.6      with xc have "(b, c) \<in> R\<^sup>*" by simp
    17.7 -    thus ?thesis by rules
    17.8 +    thus ?thesis by iprover
    17.9    next
   17.10      fix y
   17.11      assume xy: "(x, y) \<in> R"
   17.12 @@ -163,23 +163,23 @@
   17.13      proof (rule converse_rtranclE)
   17.14        assume "x = c"
   17.15        with xb have "(c, b) \<in> R\<^sup>*" by simp
   17.16 -      thus ?thesis by rules
   17.17 +      thus ?thesis by iprover
   17.18      next
   17.19        fix y'
   17.20        assume y'c: "(y', c) \<in> R\<^sup>*"
   17.21        assume xy': "(x, y') \<in> R"
   17.22        with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc)
   17.23 -      then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by rules
   17.24 +      then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by iprover
   17.25        from xy have "(y, x) \<in> R\<inverse>" ..
   17.26        from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less)
   17.27 -      then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by rules
   17.28 +      then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by iprover
   17.29        from xy' have "(y', x) \<in> R\<inverse>" ..
   17.30        moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans)
   17.31        moreover note y'c
   17.32        ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less)
   17.33 -      then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by rules
   17.34 +      then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by iprover
   17.35        from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans)
   17.36 -      with cw show ?thesis by rules
   17.37 +      with cw show ?thesis by iprover
   17.38      qed
   17.39    qed
   17.40  qed
   17.41 @@ -208,7 +208,7 @@
   17.42    proof (rule converse_rtranclE)
   17.43      assume "x = b"
   17.44      with xc have "(b, c) \<in> R\<^sup>*" by simp
   17.45 -    thus ?thesis by rules
   17.46 +    thus ?thesis by iprover
   17.47    next
   17.48      fix y
   17.49      assume xy: "(x, y) \<in> R"
   17.50 @@ -217,7 +217,7 @@
   17.51      proof (rule converse_rtranclE)
   17.52        assume "x = c"
   17.53        with xb have "(c, b) \<in> R\<^sup>*" by simp
   17.54 -      thus ?thesis by rules
   17.55 +      thus ?thesis by iprover
   17.56      next
   17.57        fix y'
   17.58        assume y'c: "(y', c) \<in> R\<^sup>*"
    18.1 --- a/src/HOL/Lambda/Eta.thy	Thu Sep 22 23:55:42 2005 +0200
    18.2 +++ b/src/HOL/Lambda/Eta.thy	Thu Sep 22 23:56:15 2005 +0200
    18.3 @@ -370,7 +370,7 @@
    18.4      by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm)
    18.5    then have "\<exists>u1 u2 k. s = eta_expand k (u1 \<degree> u2) \<and> u1 \<Rightarrow>\<^sub>\<eta> u1'' \<and> u2 \<Rightarrow>\<^sub>\<eta> u2''" by (rule eta)
    18.6    then obtain u1 u2 k where s: "s = eta_expand k (u1 \<degree> u2)"
    18.7 -    and u1: "u1 \<Rightarrow>\<^sub>\<eta> u1''" and u2: "u2 \<Rightarrow>\<^sub>\<eta> u2''" by rules
    18.8 +    and u1: "u1 \<Rightarrow>\<^sub>\<eta> u1''" and u2: "u2 \<Rightarrow>\<^sub>\<eta> u2''" by iprover
    18.9    from u1 u2 eta s' have "\<not> free u1 0" and "\<not> free u2 0"
   18.10      by (simp_all del: free_par_eta add: free_par_eta [symmetric])
   18.11    with s have "Abs (s \<degree> Var 0) = eta_expand (Suc k) (u1[dummy/0] \<degree> u2[dummy/0])"
   18.12 @@ -399,7 +399,7 @@
   18.13    then obtain u'' where s': "s' = Abs u''"
   18.14      by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm)
   18.15    then have "\<exists>u k. s = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u''" by (rule eta)
   18.16 -  then obtain u k where s: "s = eta_expand k (Abs u)" and u: "u \<Rightarrow>\<^sub>\<eta> u''" by rules
   18.17 +  then obtain u k where s: "s = eta_expand k (Abs u)" and u: "u \<Rightarrow>\<^sub>\<eta> u''" by iprover
   18.18    from eta u s' have "\<not> free u (Suc 0)"
   18.19      by (simp del: free_par_eta add: free_par_eta [symmetric])
   18.20    with s have "Abs (s \<degree> Var 0) = eta_expand (Suc k) (Abs (u[lift dummy 0/Suc 0]))"
   18.21 @@ -481,7 +481,7 @@
   18.22      by (blast dest: 2)
   18.23    from par_eta_subset_eta t' have "t' -e>> s'''" ..
   18.24    with t'' have "t'' -e>> s'''" by (rule rtrancl_trans)
   18.25 -  with s show ?case by rules
   18.26 +  with s show ?case by iprover
   18.27  qed
   18.28  
   18.29  theorem eta_postponement:
    19.1 --- a/src/HOL/Lambda/Type.thy	Thu Sep 22 23:55:42 2005 +0200
    19.2 +++ b/src/HOL/Lambda/Type.thy	Thu Sep 22 23:56:15 2005 +0200
    19.3 @@ -149,7 +149,7 @@
    19.4    apply simp
    19.5    apply (case_tac "ts @ [t]")
    19.6    apply (simp add: types_snoc_eq)+
    19.7 -  apply rules
    19.8 +  apply iprover
    19.9    done
   19.10  
   19.11  
   19.12 @@ -269,7 +269,7 @@
   19.13  lemma var_app_typesE: "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow>
   19.14    (\<And>Ts. e \<turnstile> Var i : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> P) \<Longrightarrow> P"
   19.15    apply (drule var_app_types [of _ _ "[]", simplified])
   19.16 -  apply (rules intro: typing.Var)+
   19.17 +  apply (iprover intro: typing.Var)+
   19.18    done
   19.19  
   19.20  lemma abs_typeE: "e \<turnstile> Abs t : T \<Longrightarrow> (\<And>U V. e\<langle>0:U\<rangle> \<turnstile> t : V \<Longrightarrow> P) \<Longrightarrow> P"
   19.21 @@ -346,7 +346,7 @@
   19.22    done
   19.23  
   19.24  theorem subject_reduction': "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<turnstile> t' : T"
   19.25 -  by (induct set: rtrancl) (rules intro: subject_reduction)+
   19.26 +  by (induct set: rtrancl) (iprover intro: subject_reduction)+
   19.27  
   19.28  
   19.29  subsection {* Alternative induction rule for types *}
    20.1 --- a/src/HOL/Lambda/WeakNorm.thy	Thu Sep 22 23:55:42 2005 +0200
    20.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Thu Sep 22 23:56:15 2005 +0200
    20.3 @@ -26,7 +26,7 @@
    20.4    by (simp add: listall_def)
    20.5  
    20.6  theorem listall_nil_eq [simp]: "listall P [] = True"
    20.7 -  by (rules intro: listall_nil)
    20.8 +  by (iprover intro: listall_nil)
    20.9  
   20.10  theorem listall_cons: "P x \<Longrightarrow> listall P xs \<Longrightarrow> listall P (x # xs)"
   20.11    apply (simp add: listall_def)
   20.12 @@ -84,14 +84,14 @@
   20.13    apply (induct m)
   20.14    apply (case_tac n)
   20.15    apply (case_tac [3] n)
   20.16 -  apply (simp only: nat.simps, rules?)+
   20.17 +  apply (simp only: nat.simps, iprover?)+
   20.18    done
   20.19  
   20.20  lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)"
   20.21    apply (induct m)
   20.22    apply (case_tac n)
   20.23    apply (case_tac [3] n)
   20.24 -  apply (simp del: simp_thms, rules?)+
   20.25 +  apply (simp del: simp_thms, iprover?)+
   20.26    done
   20.27  
   20.28  lemma App_NF_D: assumes NF: "Var n \<degree>\<degree> ts \<in> NF"
   20.29 @@ -125,11 +125,11 @@
   20.30    apply (erule NF.App)
   20.31    apply (rule_tac m=j and n=x in nat_le_dec [THEN disjE, standard])
   20.32    apply simp
   20.33 -  apply (rules intro: NF.App)
   20.34 +  apply (iprover intro: NF.App)
   20.35    apply simp
   20.36 -  apply (rules intro: NF.App)
   20.37 +  apply (iprover intro: NF.App)
   20.38    apply simp
   20.39 -  apply (rules intro: NF.Abs)
   20.40 +  apply (iprover intro: NF.Abs)
   20.41    done
   20.42  
   20.43  lemma app_Var_NF: "t \<in> NF \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
   20.44 @@ -199,7 +199,7 @@
   20.45  	proof (cases ts)
   20.46  	  case Nil
   20.47  	  with eq have "(Var x \<degree>\<degree> [])[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* u" by simp
   20.48 -	  with Nil and uNF show ?thesis by simp rules
   20.49 +	  with Nil and uNF show ?thesis by simp iprover
   20.50  	next
   20.51  	  case (Cons a as)
   20.52            with appT have "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> (a # as) : T'" by simp
   20.53 @@ -235,10 +235,10 @@
   20.54  	    then obtain bs' where
   20.55  	      bsred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) bs \<rightarrow>\<^sub>\<beta>\<^sup>*
   20.56  	        Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) bs'"
   20.57 -	      and bsNF: "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) bs' \<in> NF" by rules
   20.58 +	      and bsNF: "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) bs' \<in> NF" by iprover
   20.59  	    from snoc have "?R b" by simp
   20.60 -	    with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> b' \<in> NF" by rules
   20.61 -	    then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "b' \<in> NF" by rules
   20.62 +	    with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> b' \<in> NF" by iprover
   20.63 +	    then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "b' \<in> NF" by iprover
   20.64  	    from bsNF have "listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t 0) bs')"
   20.65  	      by (rule App_NF_D)
   20.66  	    moreover have "lift b' 0 \<in> NF" by (rule lift_NF)
   20.67 @@ -253,20 +253,20 @@
   20.68  	    ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp
   20.69  	    thus ?case ..
   20.70  	  qed
   20.71 -	  from App and Cons have "listall ?R as" by simp (rules dest: listall_conj2)
   20.72 +	  from App and Cons have "listall ?R as" by simp (iprover dest: listall_conj2)
   20.73  	  with argsT have "\<exists>as'. ?ex Ts as as'" by (rule as)
   20.74  	  then obtain as' where
   20.75  	    asred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>*
   20.76  	      Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as'"
   20.77 -	    and asNF: "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<in> NF" by rules
   20.78 +	    and asNF: "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<in> NF" by iprover
   20.79  	  from App and Cons have "?R a" by simp
   20.80  	  with argT and uNF and uT have "\<exists>a'. a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a' \<and> a' \<in> NF"
   20.81 -	    by rules
   20.82 -	  then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "a' \<in> NF" by rules
   20.83 +	    by iprover
   20.84 +	  then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "a' \<in> NF" by iprover
   20.85  	  from uNF have "lift u 0 \<in> NF" by (rule lift_NF)
   20.86  	  hence "\<exists>u'. lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u' \<and> u' \<in> NF" by (rule app_Var_NF)
   20.87  	  then obtain u' where ured: "lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u'" and u'NF: "u' \<in> NF"
   20.88 -	    by rules
   20.89 +	    by iprover
   20.90  	  from T and u'NF have "\<exists>ua. u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua \<and> ua \<in> NF"
   20.91  	  proof (rule MI1)
   20.92  	    have "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
   20.93 @@ -278,7 +278,7 @@
   20.94  	    from ared aT show "e \<turnstile> a' : T''" by (rule subject_reduction')
   20.95  	  qed
   20.96  	  then obtain ua where uared: "u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" and uaNF: "ua \<in> NF"
   20.97 -	    by rules
   20.98 +	    by iprover
   20.99  	  from ared have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* (lift u 0 \<degree> Var 0)[a'/0]"
  20.100  	    by (rule subst_preserves_beta2')
  20.101  	  also from ured have "(lift u 0 \<degree> Var 0)[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u'[a'/0]"
  20.102 @@ -305,7 +305,7 @@
  20.103  	    with uared' show "e \<turnstile> ua : Ts \<Rrightarrow> T'" by (rule subject_reduction')
  20.104  	  qed
  20.105  	  then obtain r where rred: "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r"
  20.106 -	    and rnf: "r \<in> NF" by rules
  20.107 +	    and rnf: "r \<in> NF" by iprover
  20.108  	  from asred have
  20.109  	    "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>*
  20.110  	    (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0]"
  20.111 @@ -315,7 +315,7 @@
  20.112  	  also note rred
  20.113  	  finally have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r" .
  20.114  	  with rnf Cons eq show ?thesis
  20.115 -	    by (simp add: map_compose [symmetric] o_def) rules
  20.116 +	    by (simp add: map_compose [symmetric] o_def) iprover
  20.117  	qed
  20.118        next
  20.119  	assume neq: "x \<noteq> i"
  20.120 @@ -342,10 +342,10 @@
  20.121  	    with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc)
  20.122  	    then obtain bs' where
  20.123  	      bsred: "\<And>x'. Var x' \<degree>\<degree> map (\<lambda>t. t[u/i]) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var x' \<degree>\<degree> bs'"
  20.124 -	      and bsNF: "\<And>x'. Var x' \<degree>\<degree> bs' \<in> NF" by rules
  20.125 +	      and bsNF: "\<And>x'. Var x' \<degree>\<degree> bs' \<in> NF" by iprover
  20.126  	    from snoc have "?R b" by simp
  20.127 -	    with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> b' \<in> NF" by rules
  20.128 -	    then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "b' \<in> NF" by rules
  20.129 +	    with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> b' \<in> NF" by iprover
  20.130 +	    then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "b' \<in> NF" by iprover
  20.131  	    from bsred bred have "\<And>x'. (Var x' \<degree>\<degree> map (\<lambda>t. t[u/i]) bs) \<degree> b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>*
  20.132                (Var x' \<degree>\<degree> bs') \<degree> b'" by (rule rtrancl_beta_App)
  20.133  	    moreover from bsNF [of 0] have "listall (\<lambda>t. t \<in> NF) bs'"
  20.134 @@ -355,16 +355,16 @@
  20.135  	    ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp
  20.136  	    thus ?case ..
  20.137  	  qed
  20.138 -	  from App have "listall ?R ts" by (rules dest: listall_conj2)
  20.139 +	  from App have "listall ?R ts" by (iprover dest: listall_conj2)
  20.140  	  with argsT have "\<exists>ts'. ?ex Ts ts ts'" by (rule ts)
  20.141  	  then obtain ts' where NF: "?ex Ts ts ts'" ..
  20.142  	  from nat_le_dec show ?thesis
  20.143  	  proof
  20.144  	    assume "i < x"
  20.145 -	    with NF show ?thesis by simp rules
  20.146 +	    with NF show ?thesis by simp iprover
  20.147  	  next
  20.148  	    assume "\<not> (i < x)"
  20.149 -	    with NF neq show ?thesis by (simp add: subst_Var) rules
  20.150 +	    with NF neq show ?thesis by (simp add: subst_Var) iprover
  20.151  	  qed
  20.152  	qed
  20.153        qed
  20.154 @@ -376,7 +376,7 @@
  20.155        moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" by (rule lift_type)
  20.156        ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" by (rule Abs)
  20.157        thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
  20.158 -	by simp (rules intro: rtrancl_beta_Abs NF.Abs)
  20.159 +	by simp (iprover intro: rtrancl_beta_Abs NF.Abs)
  20.160      }
  20.161    qed
  20.162  qed
  20.163 @@ -411,15 +411,15 @@
  20.164    shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" using T
  20.165  proof induct
  20.166    case Var
  20.167 -  show ?case by (rules intro: Var_NF)
  20.168 +  show ?case by (iprover intro: Var_NF)
  20.169  next
  20.170    case Abs
  20.171 -  thus ?case by (rules intro: rtrancl_beta_Abs NF.Abs)
  20.172 +  thus ?case by (iprover intro: rtrancl_beta_Abs NF.Abs)
  20.173  next
  20.174    case (App T U e s t)
  20.175    from App obtain s' t' where
  20.176      sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and sNF: "s' \<in> NF"
  20.177 -    and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "t' \<in> NF" by rules
  20.178 +    and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "t' \<in> NF" by iprover
  20.179    have "\<exists>u. (Var 0 \<degree> lift t' 0)[s'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u \<and> u \<in> NF"
  20.180    proof (rule subst_type_NF)
  20.181      have "lift t' 0 \<in> NF" by (rule lift_NF)
  20.182 @@ -438,10 +438,10 @@
  20.183      from sred show "e \<turnstile> s' : T \<Rightarrow> U"
  20.184        by (rule subject_reduction') (rule rtyping_imp_typing)
  20.185    qed
  20.186 -  then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "u \<in> NF" by simp rules
  20.187 +  then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "u \<in> NF" by simp iprover
  20.188    from sred tred have "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" by (rule rtrancl_beta_App)
  20.189    hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtrancl_trans)
  20.190 -  with unf show ?case by rules
  20.191 +  with unf show ?case by iprover
  20.192  qed
  20.193  
  20.194  
    21.1 --- a/src/HOL/List.thy	Thu Sep 22 23:55:42 2005 +0200
    21.2 +++ b/src/HOL/List.thy	Thu Sep 22 23:56:15 2005 +0200
    21.3 @@ -264,7 +264,7 @@
    21.4  
    21.5  lemma length_induct:
    21.6  "(!!xs. \<forall>ys. length ys < length xs --> P ys ==> P xs) ==> P xs"
    21.7 -by (rule measure_induct [of length]) rules
    21.8 +by (rule measure_induct [of length]) iprover
    21.9  
   21.10  
   21.11  subsubsection {* @{text length} *}
   21.12 @@ -550,7 +550,7 @@
   21.13  by(blast dest:map_injective)
   21.14  
   21.15  lemma inj_mapI: "inj f ==> inj (map f)"
   21.16 -by (rules dest: map_injective injD intro: inj_onI)
   21.17 +by (iprover dest: map_injective injD intro: inj_onI)
   21.18  
   21.19  lemma inj_mapD: "inj (map f) ==> inj f"
   21.20  apply (unfold inj_on_def, clarify)
   21.21 @@ -977,6 +977,9 @@
   21.22  apply (auto split:nat.split)
   21.23  done
   21.24  
   21.25 +lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
   21.26 +by(induct xs)(auto simp:neq_Nil_conv)
   21.27 +
   21.28  
   21.29  subsubsection {* @{text take} and @{text drop} *}
   21.30  
    22.1 --- a/src/HOL/MicroJava/BV/EffectMono.thy	Thu Sep 22 23:55:42 2005 +0200
    22.2 +++ b/src/HOL/MicroJava/BV/EffectMono.thy	Thu Sep 22 23:56:15 2005 +0200
    22.3 @@ -78,7 +78,7 @@
    22.4        fix n' assume s: "n = Suc n'"
    22.5        with l have  "n' \<le> length ls" by simp
    22.6        hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rule_format])
    22.7 -      then obtain a b where "ls = a @ b" "length a = n'" by rules
    22.8 +      then obtain a b where "ls = a @ b" "length a = n'" by iprover
    22.9        with s have "l # ls = (l#a) @ b \<and> length (l#a) = n" by simp
   22.10        thus ?thesis by blast
   22.11      qed
   22.12 @@ -91,9 +91,9 @@
   22.13    assume n: "n < length x"
   22.14    hence "n \<le> length x" by simp
   22.15    hence "\<exists>a b. x = a @ b \<and> length a = n" by (rule append_length_n)
   22.16 -  then obtain r d where x: "x = r@d" "length r = n" by rules
   22.17 +  then obtain r d where x: "x = r@d" "length r = n" by iprover
   22.18    with n have "\<exists>b c. d = b#c" by (simp add: neq_Nil_conv)
   22.19 -  then obtain b c where "d = b#c" by rules
   22.20 +  then obtain b c where "d = b#c" by iprover
   22.21    with x have "x = (rev (rev r)) @ b # c \<and> length (rev r) = n" by simp
   22.22    thus ?thesis by blast
   22.23  qed
    23.1 --- a/src/HOL/Nat.thy	Thu Sep 22 23:55:42 2005 +0200
    23.2 +++ b/src/HOL/Nat.thy	Thu Sep 22 23:56:15 2005 +0200
    23.3 @@ -73,7 +73,7 @@
    23.4    apply (unfold Zero_nat_def Suc_def)
    23.5    apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    23.6    apply (erule Rep_Nat [THEN Nat.induct])
    23.7 -  apply (rules elim: Abs_Nat_inverse [THEN subst])
    23.8 +  apply (iprover elim: Abs_Nat_inverse [THEN subst])
    23.9    done
   23.10  
   23.11  text {* Distinctness of constructors *}
   23.12 @@ -128,7 +128,7 @@
   23.13    apply (induct n)
   23.14    prefer 2
   23.15    apply (rule allI)
   23.16 -  apply (induct_tac x, rules+)
   23.17 +  apply (induct_tac x, iprover+)
   23.18    done
   23.19  
   23.20  subsection {* Basic properties of "less than" *}
   23.21 @@ -340,7 +340,7 @@
   23.22    by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq)
   23.23  
   23.24  lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R"
   23.25 -  by (drule le_Suc_eq [THEN iffD1], rules+)
   23.26 +  by (drule le_Suc_eq [THEN iffD1], iprover+)
   23.27  
   23.28  lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
   23.29    apply (simp add: le_def less_Suc_eq)
   23.30 @@ -385,7 +385,7 @@
   23.31    done
   23.32  
   23.33  lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)"
   23.34 -  by (rules intro: less_or_eq_imp_le le_imp_less_or_eq)
   23.35 +  by (iprover intro: less_or_eq_imp_le le_imp_less_or_eq)
   23.36  
   23.37  text {* Useful with @{text Blast}. *}
   23.38  lemma eq_imp_le: "(m::nat) = n ==> m \<le> n"
   23.39 @@ -505,7 +505,7 @@
   23.40  
   23.41  text {* This theorem is useful with @{text blast} *}
   23.42  lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
   23.43 -  by (rule iffD1, rule neq0_conv, rules)
   23.44 +  by (rule iffD1, rule neq0_conv, iprover)
   23.45  
   23.46  lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
   23.47    by (fast intro: not0_implies_Suc)
   23.48 @@ -779,7 +779,7 @@
   23.49    by (rule le_less_trans, rule le_add2, rule lessI)
   23.50  
   23.51  lemma less_iff_Suc_add: "(m < n) = (\<exists>k. n = Suc (m + k))"
   23.52 -  by (rules intro!: less_add_Suc1 less_imp_Suc_add)
   23.53 +  by (iprover intro!: less_add_Suc1 less_imp_Suc_add)
   23.54  
   23.55  lemma trans_le_add1: "(i::nat) \<le> j ==> i \<le> j + m"
   23.56    by (rule le_trans, assumption, rule le_add1)
   23.57 @@ -909,12 +909,12 @@
   23.58  lemma zero_induct_lemma: "P k ==> (!!n. P (Suc n) ==> P n) ==> P (k - i)"
   23.59    apply (induct k i rule: diff_induct)
   23.60    apply (simp_all (no_asm))
   23.61 -  apply rules
   23.62 +  apply iprover
   23.63    done
   23.64  
   23.65  lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
   23.66    apply (rule diff_self_eq_0 [THEN subst])
   23.67 -  apply (rule zero_induct_lemma, rules+)
   23.68 +  apply (rule zero_induct_lemma, iprover+)
   23.69    done
   23.70  
   23.71  lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)"
    24.1 --- a/src/HOL/Presburger.thy	Thu Sep 22 23:55:42 2005 +0200
    24.2 +++ b/src/HOL/Presburger.thy	Thu Sep 22 23:56:15 2005 +0200
    24.3 @@ -244,10 +244,10 @@
    24.4  text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
    24.5  
    24.6  lemma P_eqtrue: "(P=True) = P"
    24.7 -  by rules
    24.8 +  by iprover
    24.9  
   24.10  lemma P_eqfalse: "(P=False) = (~P)"
   24.11 -  by rules
   24.12 +  by iprover
   24.13  
   24.14  text {*
   24.15    \medskip Theorems for the generation of the bachwards direction of
   24.16 @@ -831,10 +831,10 @@
   24.17    by simp
   24.18  
   24.19  lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
   24.20 -  by rules
   24.21 +  by iprover
   24.22  
   24.23  lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))"
   24.24 -  by rules
   24.25 +  by iprover
   24.26  
   24.27  lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j)))
   24.28  ==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) "
   24.29 @@ -952,13 +952,13 @@
   24.30    apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
   24.31      nat_0_le cong add: conj_cong)
   24.32    apply (rule iffI)
   24.33 -  apply rules
   24.34 +  apply iprover
   24.35    apply (erule exE)
   24.36    apply (case_tac "x=0")
   24.37    apply (rule_tac x=0 in exI)
   24.38    apply simp
   24.39    apply (case_tac "0 \<le> k")
   24.40 -  apply rules
   24.41 +  apply iprover
   24.42    apply (simp add: linorder_not_le)
   24.43    apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
   24.44    apply assumption
    25.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Sep 22 23:55:42 2005 +0200
    25.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Sep 22 23:56:15 2005 +0200
    25.3 @@ -405,7 +405,7 @@
    25.4          linearformE: "linearform E g"
    25.5        and a: "\<forall>x \<in> F. g x = f x"
    25.6        and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
    25.7 -    by (rule abs_HahnBanach [elim_format]) rules
    25.8 +    by (rule abs_HahnBanach [elim_format]) iprover
    25.9  
   25.10    txt {* We furthermore have to show that @{text g} is also continuous: *}
   25.11  
    26.1 --- a/src/HOL/Relation.thy	Thu Sep 22 23:55:42 2005 +0200
    26.2 +++ b/src/HOL/Relation.thy	Thu Sep 22 23:56:15 2005 +0200
    26.3 @@ -70,7 +70,7 @@
    26.4    by (simp add: Id_def)
    26.5  
    26.6  lemma IdE [elim!]: "p : Id ==> (!!x. p = (x, x) ==> P) ==> P"
    26.7 -  by (unfold Id_def) (rules elim: CollectE)
    26.8 +  by (unfold Id_def) (iprover elim: CollectE)
    26.9  
   26.10  lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (a = b)"
   26.11    by (unfold Id_def) blast
   26.12 @@ -100,7 +100,7 @@
   26.13  lemma diagE [elim!]:
   26.14    "c : diag A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
   26.15    -- {* The general elimination rule. *}
   26.16 -  by (unfold diag_def) (rules elim!: UN_E singletonE)
   26.17 +  by (unfold diag_def) (iprover elim!: UN_E singletonE)
   26.18  
   26.19  lemma diag_iff: "((x, y) : diag A) = (x = y & x : A)"
   26.20    by blast
   26.21 @@ -117,11 +117,11 @@
   26.22  
   26.23  lemma rel_compE [elim!]: "xz : r O s ==>
   26.24    (!!x y z. xz = (x, z) ==> (x, y) : s ==> (y, z) : r  ==> P) ==> P"
   26.25 -  by (unfold rel_comp_def) (rules elim!: CollectE splitE exE conjE)
   26.26 +  by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE)
   26.27  
   26.28  lemma rel_compEpair:
   26.29    "(a, c) : r O s ==> (!!y. (a, y) : s ==> (y, c) : r ==> P) ==> P"
   26.30 -  by (rules elim: rel_compE Pair_inject ssubst)
   26.31 +  by (iprover elim: rel_compE Pair_inject ssubst)
   26.32  
   26.33  lemma R_O_Id [simp]: "R O Id = R"
   26.34    by fast
   26.35 @@ -146,7 +146,7 @@
   26.36  subsection {* Reflexivity *}
   26.37  
   26.38  lemma reflI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r"
   26.39 -  by (unfold refl_def) (rules intro!: ballI)
   26.40 +  by (unfold refl_def) (iprover intro!: ballI)
   26.41  
   26.42  lemma reflD: "refl A r ==> a : A ==> (a, a) : r"
   26.43    by (unfold refl_def) blast
   26.44 @@ -156,10 +156,10 @@
   26.45  
   26.46  lemma antisymI:
   26.47    "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
   26.48 -  by (unfold antisym_def) rules
   26.49 +  by (unfold antisym_def) iprover
   26.50  
   26.51  lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
   26.52 -  by (unfold antisym_def) rules
   26.53 +  by (unfold antisym_def) iprover
   26.54  
   26.55  
   26.56  subsection {* Symmetry and Transitivity *}
   26.57 @@ -169,10 +169,10 @@
   26.58  
   26.59  lemma transI:
   26.60    "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
   26.61 -  by (unfold trans_def) rules
   26.62 +  by (unfold trans_def) iprover
   26.63  
   26.64  lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r"
   26.65 -  by (unfold trans_def) rules
   26.66 +  by (unfold trans_def) iprover
   26.67  
   26.68  
   26.69  subsection {* Converse *}
   26.70 @@ -189,7 +189,7 @@
   26.71  lemma converseE [elim!]:
   26.72    "yx : r^-1 ==> (!!x y. yx = (y, x) ==> (x, y) : r ==> P) ==> P"
   26.73      -- {* More general than @{text converseD}, as it ``splits'' the member of the relation. *}
   26.74 -  by (unfold converse_def) (rules elim!: CollectE splitE bexE)
   26.75 +  by (unfold converse_def) (iprover elim!: CollectE splitE bexE)
   26.76  
   26.77  lemma converse_converse [simp]: "(r^-1)^-1 = r"
   26.78    by (unfold converse_def) blast
   26.79 @@ -219,11 +219,11 @@
   26.80    by (unfold Domain_def) blast
   26.81  
   26.82  lemma DomainI [intro]: "(a, b) : r ==> a : Domain r"
   26.83 -  by (rules intro!: iffD2 [OF Domain_iff])
   26.84 +  by (iprover intro!: iffD2 [OF Domain_iff])
   26.85  
   26.86  lemma DomainE [elim!]:
   26.87    "a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
   26.88 -  by (rules dest!: iffD1 [OF Domain_iff])
   26.89 +  by (iprover dest!: iffD1 [OF Domain_iff])
   26.90  
   26.91  lemma Domain_empty [simp]: "Domain {} = {}"
   26.92    by blast
   26.93 @@ -259,10 +259,10 @@
   26.94    by (simp add: Domain_def Range_def)
   26.95  
   26.96  lemma RangeI [intro]: "(a, b) : r ==> b : Range r"
   26.97 -  by (unfold Range_def) (rules intro!: converseI DomainI)
   26.98 +  by (unfold Range_def) (iprover intro!: converseI DomainI)
   26.99  
  26.100  lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
  26.101 -  by (unfold Range_def) (rules elim!: DomainE dest!: converseD)
  26.102 +  by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
  26.103  
  26.104  lemma Range_empty [simp]: "Range {} = {}"
  26.105    by blast
  26.106 @@ -305,7 +305,7 @@
  26.107  
  26.108  lemma ImageE [elim!]:
  26.109      "b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P"
  26.110 -  by (unfold Image_def) (rules elim!: CollectE bexE)
  26.111 +  by (unfold Image_def) (iprover elim!: CollectE bexE)
  26.112  
  26.113  lemma rev_ImageI: "a : A ==> (a, b) : r ==> b : r `` A"
  26.114    -- {* This version's more effective when we already have the required @{text a} *}
  26.115 @@ -334,7 +334,7 @@
  26.116    by blast
  26.117  
  26.118  lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B"
  26.119 -  by (rules intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
  26.120 +  by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
  26.121  
  26.122  lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})"
  26.123    -- {* NOT suitable for rewriting *}
    27.1 --- a/src/HOL/Set.thy	Thu Sep 22 23:55:42 2005 +0200
    27.2 +++ b/src/HOL/Set.thy	Thu Sep 22 23:56:15 2005 +0200
    27.3 @@ -542,7 +542,7 @@
    27.4  
    27.5  lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
    27.6    -- {* Anti-symmetry of the subset relation. *}
    27.7 -  by (rules intro: set_ext subsetD)
    27.8 +  by (iprover intro: set_ext subsetD)
    27.9  
   27.10  lemmas equalityI [intro!] = subset_antisym
   27.11  
   27.12 @@ -1046,10 +1046,10 @@
   27.13  text {* \medskip Big Union -- least upper bound of a set. *}
   27.14  
   27.15  lemma Union_upper: "B \<in> A ==> B \<subseteq> Union A"
   27.16 -  by (rules intro: subsetI UnionI)
   27.17 +  by (iprover intro: subsetI UnionI)
   27.18  
   27.19  lemma Union_least: "(!!X. X \<in> A ==> X \<subseteq> C) ==> Union A \<subseteq> C"
   27.20 -  by (rules intro: subsetI elim: UnionE dest: subsetD)
   27.21 +  by (iprover intro: subsetI elim: UnionE dest: subsetD)
   27.22  
   27.23  
   27.24  text {* \medskip General union. *}
   27.25 @@ -1058,7 +1058,7 @@
   27.26    by blast
   27.27  
   27.28  lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
   27.29 -  by (rules intro: subsetI elim: UN_E dest: subsetD)
   27.30 +  by (iprover intro: subsetI elim: UN_E dest: subsetD)
   27.31  
   27.32  
   27.33  text {* \medskip Big Intersection -- greatest lower bound of a set. *}
   27.34 @@ -1071,13 +1071,13 @@
   27.35    by blast
   27.36  
   27.37  lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
   27.38 -  by (rules intro: InterI subsetI dest: subsetD)
   27.39 +  by (iprover intro: InterI subsetI dest: subsetD)
   27.40  
   27.41  lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
   27.42    by blast
   27.43  
   27.44  lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
   27.45 -  by (rules intro: INT_I subsetI dest: subsetD)
   27.46 +  by (iprover intro: INT_I subsetI dest: subsetD)
   27.47  
   27.48  
   27.49  text {* \medskip Finite Union -- the least upper bound of two sets. *}
   27.50 @@ -1809,7 +1809,7 @@
   27.51    by blast
   27.52  
   27.53  lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
   27.54 -  by rules
   27.55 +  by iprover
   27.56  
   27.57  
   27.58  text {* \medskip Miniscoping: pushing in quantifiers and big Unions
   27.59 @@ -1955,21 +1955,21 @@
   27.60    done
   27.61  
   27.62  lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)"
   27.63 -  by rules
   27.64 +  by iprover
   27.65  
   27.66  lemma disj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 | P2) --> (Q1 | Q2)"
   27.67 -  by rules
   27.68 +  by iprover
   27.69  
   27.70  lemma imp_mono: "Q1 --> P1 ==> P2 --> Q2 ==> (P1 --> P2) --> (Q1 --> Q2)"
   27.71 -  by rules
   27.72 +  by iprover
   27.73  
   27.74  lemma imp_refl: "P --> P" ..
   27.75  
   27.76  lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)"
   27.77 -  by rules
   27.78 +  by iprover
   27.79  
   27.80  lemma all_mono: "(!!x. P x --> Q x) ==> (ALL x. P x) --> (ALL x. Q x)"
   27.81 -  by rules
   27.82 +  by iprover
   27.83  
   27.84  lemma Collect_mono: "(!!x. P x --> Q x) ==> Collect P \<subseteq> Collect Q"
   27.85    by blast
   27.86 @@ -1983,10 +1983,10 @@
   27.87    ex_mono Collect_mono in_mono
   27.88  
   27.89  lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c"
   27.90 -  by rules
   27.91 +  by iprover
   27.92  
   27.93  lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c"
   27.94 -  by rules
   27.95 +  by iprover
   27.96  
   27.97  lemma Least_mono:
   27.98    "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
    28.1 --- a/src/HOL/Transitive_Closure.thy	Thu Sep 22 23:55:42 2005 +0200
    28.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Sep 22 23:56:15 2005 +0200
    28.3 @@ -74,8 +74,8 @@
    28.4    shows "P b"
    28.5  proof -
    28.6    from a have "a = a --> P b"
    28.7 -    by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
    28.8 -  thus ?thesis by rules
    28.9 +    by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
   28.10 +  thus ?thesis by iprover
   28.11  qed
   28.12  
   28.13  lemmas rtrancl_induct2 =
   28.14 @@ -88,7 +88,7 @@
   28.15    fix x y z
   28.16    assume "(x, y) \<in> r\<^sup>*"
   28.17    assume "(y, z) \<in> r\<^sup>*"
   28.18 -  thus "(x, z) \<in> r\<^sup>*" by induct (rules!)+
   28.19 +  thus "(x, z) \<in> r\<^sup>*" by induct (iprover!)+
   28.20  qed
   28.21  
   28.22  lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
   28.23 @@ -112,7 +112,7 @@
   28.24  
   28.25  lemma converse_rtrancl_into_rtrancl:
   28.26    "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> r\<^sup>* \<Longrightarrow> (a, c) \<in> r\<^sup>*"
   28.27 -  by (rule rtrancl_trans) rules+
   28.28 +  by (rule rtrancl_trans) iprover+
   28.29  
   28.30  text {*
   28.31    \medskip More @{term "r^*"} equations and inclusions.
   28.32 @@ -158,7 +158,7 @@
   28.33    shows "(y, x) \<in> r^*"
   28.34  proof -
   28.35    from r show ?thesis
   28.36 -    by induct (rules intro: rtrancl_trans dest!: converseD)+
   28.37 +    by induct (iprover intro: rtrancl_trans dest!: converseD)+
   28.38  qed
   28.39  
   28.40  theorem rtrancl_converseI:
   28.41 @@ -166,7 +166,7 @@
   28.42    shows "(x, y) \<in> (r^-1)^*"
   28.43  proof -
   28.44    from r show ?thesis
   28.45 -    by induct (rules intro: rtrancl_trans converseI)+
   28.46 +    by induct (iprover intro: rtrancl_trans converseI)+
   28.47  qed
   28.48  
   28.49  lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
   28.50 @@ -179,7 +179,7 @@
   28.51  proof -
   28.52    from rtrancl_converseI [OF major]
   28.53    show ?thesis
   28.54 -    by induct (rules intro: cases dest!: converseD rtrancl_converseD)+
   28.55 +    by induct (iprover intro: cases dest!: converseD rtrancl_converseD)+
   28.56  qed
   28.57  
   28.58  lemmas converse_rtrancl_induct2 =
   28.59 @@ -197,8 +197,8 @@
   28.60    show ?thesis
   28.61      apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
   28.62       apply (rule_tac [2] major [THEN converse_rtrancl_induct])
   28.63 -      prefer 2 apply rules
   28.64 -     prefer 2 apply rules
   28.65 +      prefer 2 apply iprover
   28.66 +     prefer 2 apply iprover
   28.67      apply (erule asm_rl exE disjE conjE prems)+
   28.68      done
   28.69  qed
   28.70 @@ -221,7 +221,7 @@
   28.71  lemma trancl_mono: "!!p. p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+"
   28.72    apply (simp only: split_tupled_all)
   28.73    apply (erule trancl.induct)
   28.74 -  apply (rules dest: subsetD)+
   28.75 +  apply (iprover dest: subsetD)+
   28.76    done
   28.77  
   28.78  lemma r_into_trancl': "!!p. p : r ==> p : r^+"
   28.79 @@ -232,15 +232,15 @@
   28.80  *}
   28.81  
   28.82  lemma trancl_into_rtrancl: "(a, b) \<in> r^+ ==> (a, b) \<in> r^*"
   28.83 -  by (erule trancl.induct) rules+
   28.84 +  by (erule trancl.induct) iprover+
   28.85  
   28.86  lemma rtrancl_into_trancl1: assumes r: "(a, b) \<in> r^*"
   28.87    shows "!!c. (b, c) \<in> r ==> (a, c) \<in> r^+" using r
   28.88 -  by induct rules+
   28.89 +  by induct iprover+
   28.90  
   28.91  lemma rtrancl_into_trancl2: "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+"
   28.92    -- {* intro rule from @{text r} and @{text rtrancl} *}
   28.93 -  apply (erule rtranclE, rules)
   28.94 +  apply (erule rtranclE, iprover)
   28.95    apply (rule rtrancl_trans [THEN rtrancl_into_trancl1])
   28.96     apply (assumption | rule r_into_rtrancl)+
   28.97    done
   28.98 @@ -253,8 +253,8 @@
   28.99    -- {* Nice induction rule for @{text trancl} *}
  28.100  proof -
  28.101    from a have "a = a --> P b"
  28.102 -    by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
  28.103 -  thus ?thesis by rules
  28.104 +    by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
  28.105 +  thus ?thesis by iprover
  28.106  qed
  28.107  
  28.108  lemma trancl_trans_induct:
  28.109 @@ -267,7 +267,7 @@
  28.110    assume major: "(x,y) : r^+"
  28.111    case rule_context
  28.112    show ?thesis
  28.113 -    by (rules intro: r_into_trancl major [THEN trancl_induct] prems)
  28.114 +    by (iprover intro: r_into_trancl major [THEN trancl_induct] prems)
  28.115  qed
  28.116  
  28.117  inductive_cases tranclE: "(a, b) : r^+"
  28.118 @@ -281,14 +281,14 @@
  28.119    fix x y z
  28.120    assume "(x, y) \<in> r^+"
  28.121    assume "(y, z) \<in> r^+"
  28.122 -  thus "(x, z) \<in> r^+" by induct (rules!)+
  28.123 +  thus "(x, z) \<in> r^+" by induct (iprover!)+
  28.124  qed
  28.125  
  28.126  lemmas trancl_trans = trans_trancl [THEN transD, standard]
  28.127  
  28.128  lemma rtrancl_trancl_trancl: assumes r: "(x, y) \<in> r^*"
  28.129    shows "!!z. (y, z) \<in> r^+ ==> (x, z) \<in> r^+" using r
  28.130 -  by induct (rules intro: trancl_trans)+
  28.131 +  by induct (iprover intro: trancl_trans)+
  28.132  
  28.133  lemma trancl_into_trancl2: "(a, b) \<in> r ==> (b, c) \<in> r^+ ==> (a, c) \<in> r^+"
  28.134    by (erule transD [OF trans_trancl r_into_trancl])
  28.135 @@ -309,13 +309,13 @@
  28.136  lemma trancl_converseI: "(x, y) \<in> (r^+)^-1 ==> (x, y) \<in> (r^-1)^+"
  28.137    apply (drule converseD)
  28.138    apply (erule trancl.induct)
  28.139 -  apply (rules intro: converseI trancl_trans)+
  28.140 +  apply (iprover intro: converseI trancl_trans)+
  28.141    done
  28.142  
  28.143  lemma trancl_converseD: "(x, y) \<in> (r^-1)^+ ==> (x, y) \<in> (r^+)^-1"
  28.144    apply (rule converseI)
  28.145    apply (erule trancl.induct)
  28.146 -  apply (rules dest: converseD intro: trancl_trans)+
  28.147 +  apply (iprover dest: converseD intro: trancl_trans)+
  28.148    done
  28.149  
  28.150  lemma trancl_converse: "(r^-1)^+ = (r^+)^-1"
    29.1 --- a/src/HOL/ex/Intuitionistic.thy	Thu Sep 22 23:55:42 2005 +0200
    29.2 +++ b/src/HOL/ex/Intuitionistic.thy	Thu Sep 22 23:56:15 2005 +0200
    29.3 @@ -24,44 +24,44 @@
    29.4  intuitionstically equivalent to P.  [Andy Pitts] *)
    29.5  
    29.6  lemma "(~~(P&Q)) = ((~~P) & (~~Q))"
    29.7 -  by rules
    29.8 +  by iprover
    29.9  
   29.10  lemma "~~ ((~P --> Q) --> (~P --> ~Q) --> P)"
   29.11 -  by rules
   29.12 +  by iprover
   29.13  
   29.14  (* ~~ does NOT distribute over | *)
   29.15  
   29.16  lemma "(~~(P-->Q))  = (~~P --> ~~Q)"
   29.17 -  by rules
   29.18 +  by iprover
   29.19  
   29.20  lemma "(~~~P) = (~P)"
   29.21 -  by rules
   29.22 +  by iprover
   29.23  
   29.24  lemma "~~((P --> Q | R)  -->  (P-->Q) | (P-->R))"
   29.25 -  by rules
   29.26 +  by iprover
   29.27  
   29.28  lemma "(P=Q) = (Q=P)"
   29.29 -  by rules
   29.30 +  by iprover
   29.31  
   29.32  lemma "((P --> (Q | (Q-->R))) --> R) --> R"
   29.33 -  by rules
   29.34 +  by iprover
   29.35  
   29.36  lemma "(((G-->A) --> J) --> D --> E) --> (((H-->B)-->I)-->C-->J)
   29.37        --> (A-->H) --> F --> G --> (((C-->B)-->I)-->D)-->(A-->C)
   29.38        --> (((F-->A)-->B) --> I) --> E"
   29.39 -  by rules
   29.40 +  by iprover
   29.41  
   29.42  
   29.43  (* Lemmas for the propositional double-negation translation *)
   29.44  
   29.45  lemma "P --> ~~P"
   29.46 -  by rules
   29.47 +  by iprover
   29.48  
   29.49  lemma "~~(~~P --> P)"
   29.50 -  by rules
   29.51 +  by iprover
   29.52  
   29.53  lemma "~~P & ~~(P --> Q) --> ~~Q"
   29.54 -  by rules
   29.55 +  by iprover
   29.56  
   29.57  
   29.58  (* de Bruijn formulae *)
   29.59 @@ -70,7 +70,7 @@
   29.60  lemma "((P=Q) --> P&Q&R) &
   29.61         ((Q=R) --> P&Q&R) &
   29.62         ((R=P) --> P&Q&R) --> P&Q&R"
   29.63 -  by rules
   29.64 +  by iprover
   29.65  
   29.66  (*de Bruijn formula with five predicates*)
   29.67  lemma "((P=Q) --> P&Q&R&S&T) &
   29.68 @@ -78,7 +78,7 @@
   29.69         ((R=S) --> P&Q&R&S&T) &
   29.70         ((S=T) --> P&Q&R&S&T) &
   29.71         ((T=P) --> P&Q&R&S&T) --> P&Q&R&S&T"
   29.72 -  by rules
   29.73 +  by iprover
   29.74  
   29.75  
   29.76  (*** Problems from Sahlin, Franzen and Haridi, 
   29.77 @@ -89,81 +89,81 @@
   29.78  (*Problem 1.1*)
   29.79  lemma "(ALL x. EX y. ALL z. p(x) & q(y) & r(z)) =
   29.80         (ALL z. EX y. ALL x. p(x) & q(y) & r(z))"
   29.81 -  by (rules del: allE elim 2: allE')
   29.82 +  by (iprover del: allE elim 2: allE')
   29.83  
   29.84  (*Problem 3.1*)
   29.85  lemma "~ (EX x. ALL y. p y x = (~ p x x))"
   29.86 -  by rules
   29.87 +  by iprover
   29.88  
   29.89  
   29.90  (* Intuitionistic FOL: propositional problems based on Pelletier. *)
   29.91  
   29.92  (* Problem ~~1 *)
   29.93  lemma "~~((P-->Q)  =  (~Q --> ~P))"
   29.94 -  by rules
   29.95 +  by iprover
   29.96  
   29.97  (* Problem ~~2 *)
   29.98  lemma "~~(~~P  =  P)"
   29.99 -  by rules
  29.100 +  by iprover
  29.101  
  29.102  (* Problem 3 *)
  29.103  lemma "~(P-->Q) --> (Q-->P)"
  29.104 -  by rules
  29.105 +  by iprover
  29.106  
  29.107  (* Problem ~~4 *)
  29.108  lemma "~~((~P-->Q)  =  (~Q --> P))"
  29.109 -  by rules
  29.110 +  by iprover
  29.111  
  29.112  (* Problem ~~5 *)
  29.113  lemma "~~((P|Q-->P|R) --> P|(Q-->R))"
  29.114 -  by rules
  29.115 +  by iprover
  29.116  
  29.117  (* Problem ~~6 *)
  29.118  lemma "~~(P | ~P)"
  29.119 -  by rules
  29.120 +  by iprover
  29.121  
  29.122  (* Problem ~~7 *)
  29.123  lemma "~~(P | ~~~P)"
  29.124 -  by rules
  29.125 +  by iprover
  29.126  
  29.127  (* Problem ~~8.  Peirce's law *)
  29.128  lemma "~~(((P-->Q) --> P)  -->  P)"
  29.129 -  by rules
  29.130 +  by iprover
  29.131  
  29.132  (* Problem 9 *)
  29.133  lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
  29.134 -  by rules
  29.135 +  by iprover
  29.136  
  29.137  (* Problem 10 *)
  29.138  lemma "(Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P=Q)"
  29.139 -  by rules
  29.140 +  by iprover
  29.141  
  29.142  (* 11.  Proved in each direction (incorrectly, says Pelletier!!) *)
  29.143  lemma "P=P"
  29.144 -  by rules
  29.145 +  by iprover
  29.146  
  29.147  (* Problem ~~12.  Dijkstra's law *)
  29.148  lemma "~~(((P = Q) = R)  =  (P = (Q = R)))"
  29.149 -  by rules
  29.150 +  by iprover
  29.151  
  29.152  lemma "((P = Q) = R)  -->  ~~(P = (Q = R))"
  29.153 -  by rules
  29.154 +  by iprover
  29.155  
  29.156  (* Problem 13.  Distributive law *)
  29.157  lemma "(P | (Q & R))  = ((P | Q) & (P | R))"
  29.158 -  by rules
  29.159 +  by iprover
  29.160  
  29.161  (* Problem ~~14 *)
  29.162  lemma "~~((P = Q) = ((Q | ~P) & (~Q|P)))"
  29.163 -  by rules
  29.164 +  by iprover
  29.165  
  29.166  (* Problem ~~15 *)
  29.167  lemma "~~((P --> Q) = (~P | Q))"
  29.168 -  by rules
  29.169 +  by iprover
  29.170  
  29.171  (* Problem ~~16 *)
  29.172  lemma "~~((P-->Q) | (Q-->P))"
  29.173 -by rules
  29.174 +by iprover
  29.175  
  29.176  (* Problem ~~17 *)
  29.177  lemma "~~(((P & (Q-->R))-->S) = ((~P | Q | S) & (~P | ~R | S)))"
  29.178 @@ -171,7 +171,7 @@
  29.179  
  29.180  (*Dijkstra's "Golden Rule"*)
  29.181  lemma "(P&Q) = (P = (Q = (P|Q)))"
  29.182 -  by rules
  29.183 +  by iprover
  29.184  
  29.185  
  29.186  (****Examples with quantifiers****)
  29.187 @@ -179,19 +179,19 @@
  29.188  (* The converse is classical in the following implications... *)
  29.189  
  29.190  lemma "(EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q"
  29.191 -  by rules
  29.192 +  by iprover
  29.193  
  29.194  lemma "((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
  29.195 -  by rules
  29.196 +  by iprover
  29.197  
  29.198  lemma "((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))"
  29.199 -  by rules
  29.200 +  by iprover
  29.201  
  29.202  lemma "(ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)"
  29.203 -  by rules 
  29.204 +  by iprover 
  29.205  
  29.206  lemma "(EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
  29.207 -  by rules
  29.208 +  by iprover
  29.209  
  29.210  
  29.211  (* Hard examples with quantifiers *)
  29.212 @@ -201,24 +201,24 @@
  29.213  
  29.214  (* Problem ~~19 *)
  29.215  lemma "~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))"
  29.216 -  by rules
  29.217 +  by iprover
  29.218  
  29.219  (* Problem 20 *)
  29.220  lemma "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))
  29.221      --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
  29.222 -  by rules
  29.223 +  by iprover
  29.224  
  29.225  (* Problem 21 *)
  29.226  lemma "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P=Q(x))"
  29.227 -  by rules
  29.228 +  by iprover
  29.229  
  29.230  (* Problem 22 *)
  29.231  lemma "(ALL x. P = Q(x))  -->  (P = (ALL x. Q(x)))"
  29.232 -  by rules
  29.233 +  by iprover
  29.234  
  29.235  (* Problem ~~23 *)
  29.236  lemma "~~ ((ALL x. P | Q(x))  =  (P | (ALL x. Q(x))))"
  29.237 -  by rules
  29.238 +  by iprover
  29.239  
  29.240  (* Problem 25 *)
  29.241  lemma "(EX x. P(x)) &
  29.242 @@ -226,7 +226,7 @@
  29.243         (ALL x. P(x) --> (M(x) & L(x))) &
  29.244         ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))
  29.245     --> (EX x. Q(x)&P(x))"
  29.246 -  by rules
  29.247 +  by iprover
  29.248  
  29.249  (* Problem 27 *)
  29.250  lemma "(EX x. P(x) & ~Q(x)) &
  29.251 @@ -234,40 +234,40 @@
  29.252               (ALL x. M(x) & L(x) --> P(x)) &
  29.253               ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))
  29.254           --> (ALL x. M(x) --> ~L(x))"
  29.255 -  by rules
  29.256 +  by iprover
  29.257  
  29.258  (* Problem ~~28.  AMENDED *)
  29.259  lemma "(ALL x. P(x) --> (ALL x. Q(x))) &
  29.260         (~~(ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &
  29.261         (~~(EX x. S(x)) --> (ALL x. L(x) --> M(x)))
  29.262     --> (ALL x. P(x) & L(x) --> M(x))"
  29.263 -  by rules
  29.264 +  by iprover
  29.265  
  29.266  (* Problem 29.  Essentially the same as Principia Mathematica *11.71 *)
  29.267  lemma "(((EX x. P(x)) & (EX y. Q(y))) -->
  29.268     (((ALL x. (P(x) --> R(x))) & (ALL y. (Q(y) --> S(y)))) =
  29.269      (ALL x y. ((P(x) & Q(y)) --> (R(x) & S(y))))))"
  29.270 -  by rules
  29.271 +  by iprover
  29.272  
  29.273  (* Problem ~~30 *)
  29.274  lemma "(ALL x. (P(x) | Q(x)) --> ~ R(x)) &
  29.275         (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
  29.276     --> (ALL x. ~~S(x))"
  29.277 -  by rules
  29.278 +  by iprover
  29.279  
  29.280  (* Problem 31 *)
  29.281  lemma "~(EX x. P(x) & (Q(x) | R(x))) & 
  29.282          (EX x. L(x) & P(x)) &
  29.283          (ALL x. ~ R(x) --> M(x))
  29.284      --> (EX x. L(x) & M(x))"
  29.285 -  by rules
  29.286 +  by iprover
  29.287  
  29.288  (* Problem 32 *)
  29.289  lemma "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) &
  29.290         (ALL x. S(x) & R(x) --> L(x)) &
  29.291         (ALL x. M(x) --> R(x))
  29.292     --> (ALL x. P(x) & M(x) --> L(x))"
  29.293 -  by rules
  29.294 +  by iprover
  29.295  
  29.296  (* Problem ~~33 *)
  29.297  lemma "(ALL x. ~~(P(a) & (P(x)-->P(b))-->P(c)))  =
  29.298 @@ -280,50 +280,50 @@
  29.299        (ALL x. EX y. G x y) &
  29.300        (ALL x y. J x y | G x y --> (ALL z. J y z | G y z --> H x z))
  29.301    --> (ALL x. EX y. H x y)"
  29.302 -  by rules
  29.303 +  by iprover
  29.304  
  29.305  (* Problem 39 *)
  29.306  lemma "~ (EX x. ALL y. F y x = (~F y y))"
  29.307 -  by rules
  29.308 +  by iprover
  29.309  
  29.310  (* Problem 40.  AMENDED *)
  29.311  lemma "(EX y. ALL x. F x y = F x x) -->
  29.312               ~(ALL x. EX y. ALL z. F z y = (~ F z x))"
  29.313 -  by rules
  29.314 +  by iprover
  29.315  
  29.316  (* Problem 44 *)
  29.317  lemma "(ALL x. f(x) -->
  29.318               (EX y. g(y) & h x y & (EX y. g(y) & ~ h x y)))  &
  29.319               (EX x. j(x) & (ALL y. g(y) --> h x y))
  29.320               --> (EX x. j(x) & ~f(x))"
  29.321 -  by rules
  29.322 +  by iprover
  29.323  
  29.324  (* Problem 48 *)
  29.325  lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
  29.326 -  by rules
  29.327 +  by iprover
  29.328  
  29.329  (* Problem 51 *)
  29.330  lemma "((EX z w. (ALL x y. (P x y = ((x = z) & (y = w))))) -->
  29.331    (EX z. (ALL x. (EX w. ((ALL y. (P x y = (y = w))) = (x = z))))))"
  29.332 -  by rules
  29.333 +  by iprover
  29.334  
  29.335  (* Problem 52 *)
  29.336  (*Almost the same as 51. *)
  29.337  lemma "((EX z w. (ALL x y. (P x y = ((x = z) & (y = w))))) -->
  29.338     (EX w. (ALL y. (EX z. ((ALL x. (P x y = (x = z))) = (y = w))))))"
  29.339 -  by rules
  29.340 +  by iprover
  29.341  
  29.342  (* Problem 56 *)
  29.343  lemma "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) = (ALL x. P(x) --> P(f(x)))"
  29.344 -  by rules
  29.345 +  by iprover
  29.346  
  29.347  (* Problem 57 *)
  29.348  lemma "P (f a b) (f b c) & P (f b c) (f a c) &
  29.349       (ALL x y z. P x y & P y z --> P x z) --> P (f a b) (f a c)"
  29.350 -  by rules
  29.351 +  by iprover
  29.352  
  29.353  (* Problem 60 *)
  29.354  lemma "ALL x. P x (f x) = (EX y. (ALL z. P z y --> P z (f x)) & P x y)"
  29.355 -  by rules
  29.356 +  by iprover
  29.357  
  29.358  end