tuned proofs: avoid implicit prems;
authorwenzelm
Wed Jun 13 10:43:38 2007 +0200 (2007-06-13)
changeset 23366a1e61b5c000f
parent 23365 f31794033ae1
child 23367 05f399115ba5
tuned proofs: avoid implicit prems;
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/AxSound.thy
     1.1 --- a/src/HOL/Bali/AxCompl.thy	Wed Jun 13 03:31:11 2007 +0200
     1.2 +++ b/src/HOL/Bali/AxCompl.thy	Wed Jun 13 10:43:38 2007 +0200
     1.3 @@ -937,7 +937,7 @@
     1.4                 \<rightarrow> abupd (abrupt_if (\<exists>y. abrupt s1 = Some y) (abrupt s1)) s2"
     1.5        proof -
     1.6  	obtain abr1 str1 where s1: "s1=(abr1,str1)"
     1.7 -	  by (cases s1) simp
     1.8 +	  by (cases s1)
     1.9  	with eval_c1 eval_c2 obtain
    1.10  	  eval_c1': "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (abr1,str1)" and
    1.11  	  eval_c2': "G\<turnstile>Norm str1 \<midarrow>c2\<rightarrow> s2"
    1.12 @@ -1072,14 +1072,13 @@
    1.13  	done
    1.14      next
    1.15        case (FVar accC statDeclC stat e fn)
    1.16 -      have "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}".
    1.17 -      from MGFn_Init [OF hyp] this wf 
    1.18 +      from MGFn_Init [OF hyp] and `G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}` and wf
    1.19        show ?case
    1.20  	by (rule MGFn_FVar)
    1.21      next
    1.22        case (AVar e1 e2)
    1.23 -      have mgf_e1: "G,A\<turnstile>{=:n} \<langle>e1\<rangle>\<^sub>e\<succ> {G\<rightarrow>}".
    1.24 -      have mgf_e2: "G,A\<turnstile>{=:n} \<langle>e2\<rangle>\<^sub>e\<succ> {G\<rightarrow>}".
    1.25 +      note mgf_e1 = `G,A\<turnstile>{=:n} \<langle>e1\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
    1.26 +      note mgf_e2 = `G,A\<turnstile>{=:n} \<langle>e2\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
    1.27        show "G,A\<turnstile>{=:n} \<langle>e1.[e2]\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
    1.28  	apply (rule MGFn_NormalI)
    1.29  	apply (rule ax_derivs.AVar)
    1.30 @@ -1222,8 +1221,8 @@
    1.31  	done
    1.32      next
    1.33        case (Call accC statT mode e mn pTs' ps)
    1.34 -      have mgf_e:  "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}".
    1.35 -      have mgf_ps: "G,A\<turnstile>{=:n} \<langle>ps\<rangle>\<^sub>l\<succ> {G\<rightarrow>}".
    1.36 +      note mgf_e = `G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
    1.37 +      note mgf_ps = `G,A\<turnstile>{=:n} \<langle>ps\<rangle>\<^sub>l\<succ> {G\<rightarrow>}`
    1.38        from mgf_methds mgf_e mgf_ps wf
    1.39        show "G,A\<turnstile>{=:n} \<langle>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
    1.40  	by (rule MGFn_Call)
    1.41 @@ -1234,7 +1233,7 @@
    1.42  	by simp
    1.43      next
    1.44        case (Body D c)
    1.45 -      have mgf_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" .
    1.46 +      note mgf_c = `G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}`
    1.47        from wf MGFn_Init [OF hyp] mgf_c
    1.48        show "G,A\<turnstile>{=:n} \<langle>Body D c\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
    1.49  	by (rule MGFn_Body)
    1.50 @@ -1302,8 +1301,8 @@
    1.51  	done
    1.52      next
    1.53        case (Loop l e c)
    1.54 -      have mgf_e: "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}".
    1.55 -      have mgf_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}".
    1.56 +      note mgf_e = `G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
    1.57 +      note mgf_c = `G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}`
    1.58        from mgf_e mgf_c wf
    1.59        show "G,A\<turnstile>{=:n} \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
    1.60  	by (rule MGFn_Loop)
    1.61 @@ -1339,8 +1338,8 @@
    1.62  	done
    1.63      next
    1.64        case (Fin c1 c2)
    1.65 -      have mgf_c1: "G,A\<turnstile>{=:n} \<langle>c1\<rangle>\<^sub>s\<succ> {G\<rightarrow>}".
    1.66 -      have mgf_c2: "G,A\<turnstile>{=:n} \<langle>c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}".
    1.67 +      note mgf_c1 = `G,A\<turnstile>{=:n} \<langle>c1\<rangle>\<^sub>s\<succ> {G\<rightarrow>}`
    1.68 +      note mgf_c2 = `G,A\<turnstile>{=:n} \<langle>c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}`
    1.69        from wf mgf_c1 mgf_c2
    1.70        show "G,A\<turnstile>{=:n} \<langle>c1 Finally c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
    1.71  	by (rule MGFn_Fin)
     2.1 --- a/src/HOL/Bali/AxSound.thy	Wed Jun 13 03:31:11 2007 +0200
     2.2 +++ b/src/HOL/Bali/AxSound.thy	Wed Jun 13 10:43:38 2007 +0200
     2.3 @@ -564,7 +564,7 @@
     2.4        from eval wt da conf_s0 wf
     2.5        have "s3\<Colon>\<preceq>(G, L)"
     2.6  	by (rule evaln_type_sound [elim_format]) simp
     2.7 -      ultimately show ?thesis using Q by simp
     2.8 +      ultimately show ?thesis using Q R by simp
     2.9      qed
    2.10    qed
    2.11  next
    2.12 @@ -612,8 +612,8 @@
    2.13  	  from eval_e1  wt_e1 da_e1 wf True
    2.14  	  have "nrm E1 \<subseteq> dom (locals (store s1))"
    2.15  	    by (cases rule: da_good_approx_evalnE) iprover
    2.16 -	  with da_e2 show ?thesis
    2.17 -	    by (rule da_weakenE)
    2.18 +	  with da_e2 show thesis
    2.19 +	    by (rule da_weakenE) (rule that)
    2.20  	qed
    2.21  	with valid_e2 Q' valid_A conf_s1 eval_e2 wt_e2 
    2.22  	show ?thesis
    2.23 @@ -633,7 +633,7 @@
    2.24    qed
    2.25  next
    2.26    case (NewC A P C Q)
    2.27 -  have valid_init: "G,A|\<Turnstile>\<Colon>{ {Normal P} .Init C. {Alloc G (CInst C) Q} }".
    2.28 +  note valid_init = `G,A|\<Turnstile>\<Colon>{ {Normal P} .Init C. {Alloc G (CInst C) Q} }`
    2.29    show "G,A|\<Turnstile>\<Colon>{ {Normal P} NewC C-\<succ> {Q} }"
    2.30    proof (rule valid_expr_NormalI)
    2.31      fix n s0 L accC T E v s2 Y Z
    2.32 @@ -728,8 +728,8 @@
    2.33  	from eval_init 
    2.34  	have "dom (locals (store s0)) \<subseteq> dom (locals (store s1))"
    2.35  	  by (rule dom_locals_evaln_mono_elim)
    2.36 -	with da_e show ?thesis
    2.37 -	  by (rule da_weakenE)
    2.38 +	with da_e show thesis
    2.39 +	  by (rule da_weakenE) (rule that)
    2.40        qed
    2.41        with valid_e Q valid_A conf_s1 eval_e wt_e
    2.42        have "(\<lambda>Val:i:. abupd (check_neg i) .; 
    2.43 @@ -746,9 +746,9 @@
    2.44    qed
    2.45  next
    2.46    case (Cast A P e T Q)
    2.47 -  have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> 
    2.48 +  note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> 
    2.49                   {\<lambda>Val:v:. \<lambda>s.. abupd (raise_if (\<not> G,s\<turnstile>v fits T) ClassCast) .;
    2.50 -                  Q\<leftarrow>In1 v} }" .
    2.51 +                  Q\<leftarrow>In1 v} }`
    2.52    show "G,A|\<Turnstile>\<Colon>{ {Normal P} Cast T e-\<succ> {Q} }"
    2.53    proof (rule valid_expr_NormalI)
    2.54      fix n s0 L accC castT E v s2 Y Z
    2.55 @@ -1060,8 +1060,8 @@
    2.56  	    from eval_var wt_var da_var wf True
    2.57  	    have "nrm V \<subseteq>  dom (locals (store s1))"
    2.58  	      by (cases rule: da_good_approx_evalnE) iprover
    2.59 -	    with da_e show ?thesis
    2.60 -	      by (rule da_weakenE) 
    2.61 +	    with da_e show thesis
    2.62 +	      by (rule da_weakenE) (rule that)
    2.63  	  qed
    2.64  	  note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e wt_e da_e']
    2.65  	  show ?thesis
    2.66 @@ -1101,8 +1101,8 @@
    2.67  	    from eval_var
    2.68  	    have "dom (locals (store s0)) \<subseteq> dom (locals (store (s1)))"
    2.69  	      by (rule dom_locals_evaln_mono_elim)
    2.70 -	    with da_e show ?thesis
    2.71 -	      by (rule da_weakenE)
    2.72 +	    with da_e show thesis
    2.73 +	      by (rule da_weakenE) (rule that)
    2.74  	  qed
    2.75  	  note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e wt_e da_e']
    2.76  	  show ?thesis
    2.77 @@ -1296,8 +1296,8 @@
    2.78  	  from evaln_e wt_e da_e wf True
    2.79  	  have "nrm C \<subseteq>  dom (locals (store s1))"
    2.80  	    by (cases rule: da_good_approx_evalnE) iprover
    2.81 -	  with da_args show ?thesis
    2.82 -	    by (rule da_weakenE) 
    2.83 +	  with da_args show thesis
    2.84 +	    by (rule da_weakenE) (rule that)
    2.85  	qed
    2.86  	with valid_args Q valid_A conf_s1 evaln_args wt_args 
    2.87  	obtain "(R a) \<lfloor>vs\<rfloor>\<^sub>l s2 Z" "s2\<Colon>\<preceq>(G,L)" 
    2.88 @@ -1364,7 +1364,7 @@
    2.89  	      by (cases s2) (auto simp add: init_lvars_def2 split: split_if_asm)
    2.90  	    moreover
    2.91  	    obtain abr2 str2 where s2: "s2=(abr2,str2)"
    2.92 -	      by (cases s2) simp
    2.93 +	      by (cases s2)
    2.94  	    from s3 s2 conf_s2 have "(abrupt s3,str2)\<Colon>\<preceq>(G, L)"
    2.95  	      by (auto simp add: init_lvars_def2 split: split_if_asm)
    2.96  	    ultimately show ?thesis
    2.97 @@ -1401,8 +1401,8 @@
    2.98  	  from evaln_e wt_e da_e wf normal_s1
    2.99  	  have "nrm C \<subseteq>  dom (locals (store s1))"
   2.100  	    by (cases rule: da_good_approx_evalnE) iprover
   2.101 -	  with da_args show ?thesis
   2.102 -	    by (rule da_weakenE) 
   2.103 +	  with da_args show thesis
   2.104 +	    by (rule da_weakenE) (rule that)
   2.105  	qed
   2.106  	from evaln_args
   2.107  	have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2"
   2.108 @@ -1583,9 +1583,9 @@
   2.109  	      using da
   2.110  	      by (iprover intro: da.Body assigned.select_convs)
   2.111  	    from _ this [simplified]
   2.112 -	    show ?thesis
   2.113 +	    show thesis
   2.114  	      by (rule da.Methd [simplified,elim_format])
   2.115 -	         (auto intro: dynM')
   2.116 +	         (auto intro: dynM' that)
   2.117  	  qed
   2.118  	  from valid_methd R' valid_A conf_s3' evaln_methd wt_methd da_methd
   2.119  	  have "(set_lvars l .; S) \<lfloor>v\<rfloor>\<^sub>e s4 Z"
   2.120 @@ -1599,9 +1599,9 @@
   2.121    qed
   2.122  next
   2.123    case (Methd A P Q ms)
   2.124 -  have valid_body: "G,A \<union> {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}".
   2.125 +  note valid_body = `G,A \<union> {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}`
   2.126    show "G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}"
   2.127 -    by (rule Methd_sound)
   2.128 +    by (rule Methd_sound) (rule Methd.hyps)
   2.129  next
   2.130    case (Body A P D Q c R)
   2.131    note valid_init = `G,A|\<Turnstile>\<Colon>{ {Normal P} .Init D. {Q} }`
   2.132 @@ -1646,7 +1646,7 @@
   2.133  	from eval_init 
   2.134  	have "(dom (locals (store s0))) \<subseteq> (dom (locals (store s1)))"
   2.135  	  by (rule dom_locals_evaln_mono_elim)
   2.136 -	with da_c show ?thesis by (rule da_weakenE)
   2.137 +	with da_c show thesis by (rule da_weakenE) (rule that)
   2.138        qed
   2.139        from valid_init P valid_A conf_s0 eval_init wt_init da_init
   2.140        obtain Q: "Q \<diamondsuit> s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"
   2.141 @@ -1697,7 +1697,7 @@
   2.142    qed
   2.143  next
   2.144    case (Cons A P e Q es R)
   2.145 -  have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }".
   2.146 +  note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }`
   2.147    have valid_es: "\<And> v. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>\<lfloor>v\<rfloor>\<^sub>e} es\<doteq>\<succ> {\<lambda>Vals:vs:. R\<leftarrow>\<lfloor>(v # vs)\<rfloor>\<^sub>l} }"
   2.148      using Cons.hyps by simp
   2.149    show "G,A|\<Turnstile>\<Colon>{ {Normal P} e # es\<doteq>\<succ> {R} }"
   2.150 @@ -1739,8 +1739,8 @@
   2.151  	  from eval_e wt_e da_e wf True
   2.152  	  have "nrm E1 \<subseteq> dom (locals (store s1))"
   2.153  	    by (cases rule: da_good_approx_evalnE) iprover
   2.154 -	  with da_es show ?thesis
   2.155 -	    by (rule da_weakenE)
   2.156 +	  with da_es show thesis
   2.157 +	    by (rule da_weakenE) (rule that)
   2.158  	qed
   2.159  	from valid_es Q' valid_A conf_s1 eval_es wt_es da_es'
   2.160  	show ?thesis
   2.161 @@ -1884,8 +1884,8 @@
   2.162  	  from eval_c1 wt_c1 da_c1 wf True
   2.163  	  have "nrm C1 \<subseteq> dom (locals (store s1))"
   2.164  	    by (cases rule: da_good_approx_evalnE) iprover
   2.165 -	  with da_c2 show ?thesis
   2.166 -	    by (rule da_weakenE)
   2.167 +	  with da_c2 show thesis
   2.168 +	    by (rule da_weakenE) (rule that)
   2.169  	qed
   2.170  	with valid_c2 Q valid_A conf_s1 eval_c2 wt_c2 
   2.171  	show ?thesis
   2.172 @@ -2091,8 +2091,8 @@
   2.173  		  have "dom (locals (store ((Norm s0')::state)))
   2.174                             \<union> assigns_if True e \<subseteq> dom (locals (store s1'))"
   2.175  		    by (rule Un_least)
   2.176 -		  with da_c show ?thesis
   2.177 -		    by (rule da_weakenE)
   2.178 +		  with da_c show thesis
   2.179 +		    by (rule da_weakenE) (rule that)
   2.180  		qed
   2.181  		with valid_c P'' valid_A conf_s1' eval_c wt_c
   2.182  		obtain "(abupd (absorb (Cont l)) .; P) \<diamondsuit> s2' Z" and 
   2.183 @@ -2173,10 +2173,10 @@
   2.184  	  qed
   2.185  	next
   2.186  	  case (Abrupt abr s t' n' Y' T E)
   2.187 -	  have t': "t' = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s".
   2.188 -	  have conf: "(Some abr, s)\<Colon>\<preceq>(G, L)".
   2.189 -	  have P: "P Y' (Some abr, s) Z".
   2.190 -	  have valid_A: "\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t". 
   2.191 +	  note t' = `t' = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s`
   2.192 +	  note conf = `(Some abr, s)\<Colon>\<preceq>(G, L)`
   2.193 +	  note P = `P Y' (Some abr, s) Z`
   2.194 +	  note valid_A = `\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t`
   2.195  	  show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) (arbitrary3 t') (Some abr, s) Z"
   2.196  	  proof -
   2.197  	    have eval_e: 
   2.198 @@ -2188,7 +2188,7 @@
   2.199  	    with t' show ?thesis
   2.200  	      by auto
   2.201  	  qed
   2.202 -	qed (simp_all)
   2.203 +	qed simp_all
   2.204        } note generalized=this
   2.205        from eval _ valid_A P conf_s0 wt da
   2.206        have "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3 Z"
   2.207 @@ -2388,8 +2388,8 @@
   2.208                ultimately show ?thesis
   2.209  		by (rule Un_least)
   2.210              qed
   2.211 -	    with da_c2 show ?thesis
   2.212 -	      by (rule da_weakenE)
   2.213 +	    with da_c2 show thesis
   2.214 +	      by (rule da_weakenE) (rule that)
   2.215  	  qed
   2.216  	  from Q eval_c2 True 
   2.217  	  have "(Q \<and>. (\<lambda>s. G,s\<turnstile>catch C) ;. new_xcpt_var vn) 
   2.218 @@ -2466,8 +2466,8 @@
   2.219  	hence "dom (locals (store s0)) 
   2.220                   \<subseteq> dom (locals (store ((Norm s1)::state)))"
   2.221  	  by simp
   2.222 -	with da_c2 show ?thesis
   2.223 -	  by (rule da_weakenE)
   2.224 +	with da_c2 show thesis
   2.225 +	  by (rule da_weakenE) (rule that)
   2.226        qed
   2.227        from valid_c2 Q' valid_A conf_Norm_s1 eval_c2 wt_c2 da_c2'
   2.228        have "(abupd (abrupt_if (abr1 \<noteq> None) abr1) .; R) \<diamondsuit> s2 Z"