src/HOL/Bali/TypeSafe.thy
changeset 17589 58eeffd73be1
parent 16417 9bc16273c2d4
child 17876 b9c92f384109
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Thu Sep 22 23:55:42 2005 +0200
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Thu Sep 22 23:56:15 2005 +0200
     1.3 @@ -1233,7 +1233,7 @@
     1.4    next
     1.5      case (Cons y ys')
     1.6      have "(tab(x\<mapsto>y)(xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y)(xs[\<mapsto>]ys')) z"
     1.7 -      by (rules intro: Hyps map_upd_cong_ext)
     1.8 +      by (iprover intro: Hyps map_upd_cong_ext)
     1.9      with Cons show ?thesis
    1.10        by simp
    1.11    qed
    1.12 @@ -1701,7 +1701,7 @@
    1.13  	  by cases simp+
    1.14  	from eval_e1 wt_e1 da_e1 wf normal_s1 
    1.15  	have "nrm E1' \<subseteq> dom (locals (store s1))"
    1.16 -	  by (cases rule: da_good_approxE') rules
    1.17 +	  by (cases rule: da_good_approxE') iprover
    1.18  	with da_e2 show ?thesis
    1.19  	  using that by (rule da_weakenE) (simp add: True)
    1.20        qed
    1.21 @@ -1836,7 +1836,7 @@
    1.22        proof -
    1.23  	from eval_c1 wt_c1 da_c1 wf True
    1.24  	have "nrm C1 \<subseteq> dom (locals (store s1))"
    1.25 -	  by (cases rule: da_good_approxE') rules
    1.26 +	  by (cases rule: da_good_approxE') iprover
    1.27  	with da_c2 show ?thesis
    1.28  	  by (rule da_weakenE)
    1.29        qed
    1.30 @@ -2806,7 +2806,7 @@
    1.31  	proof -
    1.32  	  from eval_var wt_var da_var wf normal_s1
    1.33  	  have "nrm V \<subseteq>  dom (locals (store s1))"
    1.34 -	    by (cases rule: da_good_approxE') rules
    1.35 +	    by (cases rule: da_good_approxE') iprover
    1.36  	  with da_e show ?thesis
    1.37  	    by (rule da_weakenE) 
    1.38  	qed
    1.39 @@ -3094,7 +3094,7 @@
    1.40        proof -
    1.41  	from eval_e wt_e da_e wf normal_s1
    1.42  	have "nrm E \<subseteq>  dom (locals (store s1))"
    1.43 -	  by (cases rule: da_good_approxE') rules
    1.44 +	  by (cases rule: da_good_approxE') iprover
    1.45  	with da_args show ?thesis
    1.46  	  by (rule da_weakenE) 
    1.47        qed
    1.48 @@ -3256,7 +3256,7 @@
    1.49                 ,lcl=callee_lcl invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> (mthd dynM)
    1.50                 \<rparr> \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'" and
    1.51                res: "Result \<in> nrm M'"
    1.52 -	      by (rule wf_mdeclE) rules
    1.53 +	      by (rule wf_mdeclE) iprover
    1.54  	    from da_body is_static_eq L' have
    1.55  	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
    1.56                   \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'"
    1.57 @@ -3308,7 +3308,7 @@
    1.58  	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> \<turnstile> dom (locals (store s3')) 
    1.59                       \<guillemotright>\<langle>Body (declclass dynM) (stmt (mbody (mthd dynM)))\<rangle>\<guillemotright> M3"
    1.60  	      using da
    1.61 -	      by (rules intro: da.Body assigned.select_convs)
    1.62 +	      by (iprover intro: da.Body assigned.select_convs)
    1.63  	    from _ this [simplified]
    1.64  	    show ?thesis
    1.65  	      by (rule da.Methd [simplified,elim_format])
    1.66 @@ -3672,7 +3672,7 @@
    1.67        proof -
    1.68  	from eval_e1 wt_e1 da_e1 wf True
    1.69  	have "nrm E1 \<subseteq> dom (locals (store s1))"
    1.70 -	  by (cases rule: da_good_approxE') rules
    1.71 +	  by (cases rule: da_good_approxE') iprover
    1.72  	with da_e2 show ?thesis
    1.73  	  by (rule da_weakenE)
    1.74        qed
    1.75 @@ -3768,7 +3768,7 @@
    1.76        proof -
    1.77  	from eval_e wt_e da_e wf True
    1.78  	have "nrm E \<subseteq> dom (locals (store s1))"
    1.79 -	  by (cases rule: da_good_approxE') rules
    1.80 +	  by (cases rule: da_good_approxE') iprover
    1.81  	with da_es show ?thesis
    1.82  	  by (rule da_weakenE)
    1.83        qed
    1.84 @@ -3806,7 +3806,7 @@
    1.85                    error_free s0 = error_free s1\<rbrakk> \<Longrightarrow> P"
    1.86    shows "P"
    1.87  using eval wt da wf conf
    1.88 -by (rule eval_type_sound [elim_format]) (rules intro: elim) 
    1.89 +by (rule eval_type_sound [elim_format]) (iprover intro: elim) 
    1.90  
    1.91   
    1.92  corollary eval_ts: 
    1.93 @@ -3995,19 +3995,19 @@
    1.94  	proof -
    1.95  	  from eval_c1 wt_c1 da_c1 wf normal_s1
    1.96  	  have "nrm C1 \<subseteq> dom (locals (store s1))"
    1.97 -	    by (cases rule: da_good_approxE') rules
    1.98 +	    by (cases rule: da_good_approxE') iprover
    1.99  	  with da_c2 show ?thesis
   1.100  	    by (rule da_weakenE)
   1.101  	qed
   1.102  	with wt_c2 have "P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2"
   1.103  	  by (rule Comp.hyps)
   1.104  	with da show ?thesis
   1.105 -	  using elim by rules
   1.106 +	  using elim by iprover
   1.107        qed
   1.108      }
   1.109      with eval_c1 eval_c2 wt_c1 wt_c2 da_c1 P_c1 
   1.110      show ?case
   1.111 -      by (rule comp) rules+
   1.112 +      by (rule comp) iprover+
   1.113    next
   1.114      case (If b c1 c2 e s0 s1 s2 L accC T A)
   1.115      have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
   1.116 @@ -4058,12 +4058,12 @@
   1.117  	with wt_then_else
   1.118  	have "P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2"
   1.119  	  by (rule If.hyps)
   1.120 -	with da show ?thesis using elim by rules
   1.121 +	with da show ?thesis using elim by iprover
   1.122        qed
   1.123      }
   1.124      with eval_e eval_then_else wt_e wt_then_else da_e P_e
   1.125      show ?case
   1.126 -      by (rule if) rules+
   1.127 +      by (rule if) iprover+
   1.128    next
   1.129      oops
   1.130