tuned proofs;
authorwenzelm
Mon Feb 27 17:40:59 2012 +0100 (2012-02-27)
changeset 46714a7ca72710dfe
parent 46713 e6e1ec6d5c1c
child 46715 6236ca7b32a7
tuned proofs;
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/AxSound.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Bali/WellType.thy
     1.1 --- a/src/HOL/Bali/AxCompl.thy	Mon Feb 27 17:39:34 2012 +0100
     1.2 +++ b/src/HOL/Bali/AxCompl.thy	Mon Feb 27 17:40:59 2012 +0100
     1.3 @@ -1299,7 +1299,7 @@
     1.4          apply -
     1.5          apply (rule MGFn_NormalI)
     1.6          apply (rule ax_derivs.Jmp [THEN conseq1])
     1.7 -        apply (auto intro: eval.Jmp simp add: abupd_def2)
     1.8 +        apply (auto intro: eval.Jmp)
     1.9          done
    1.10      next
    1.11        case (Throw e)
     2.1 --- a/src/HOL/Bali/AxSound.thy	Mon Feb 27 17:39:34 2012 +0100
     2.2 +++ b/src/HOL/Bali/AxSound.thy	Mon Feb 27 17:40:59 2012 +0100
     2.3 @@ -78,8 +78,7 @@
     2.4  done
     2.5  
     2.6  lemma Methd_triple_valid2_0: "G\<Turnstile>0\<Colon>{Normal P} Methd C sig-\<succ> {Q}"
     2.7 -apply (clarsimp elim!: evaln_elim_cases simp add: triple_valid2_def2)
     2.8 -done
     2.9 +by (auto elim!: evaln_elim_cases simp add: triple_valid2_def2)
    2.10  
    2.11  lemma Methd_triple_valid2_SucI: 
    2.12  "\<lbrakk>G\<Turnstile>n\<Colon>{Normal P} body G C sig-\<succ>{Q}\<rbrakk> 
    2.13 @@ -992,7 +991,7 @@
    2.14        from da obtain V where 
    2.15          da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>var\<rangle>\<^sub>v\<guillemotright> V"
    2.16          by (cases "\<exists> n. var=LVar n") (insert da.LVar,auto elim!: da_elim_cases)
    2.17 -      from eval obtain w upd where
    2.18 +      from eval obtain upd where
    2.19          eval_var: "G\<turnstile>s0 \<midarrow>var=\<succ>(v, upd)\<midarrow>n\<rightarrow> s1"
    2.20          using normal_s0 by (fastforce elim: evaln_elim_cases)
    2.21        from valid_var P valid_A conf_s0 eval_var wt_var da_var
    2.22 @@ -1408,7 +1407,7 @@
    2.23            by (rule evaln_type_sound [elim_format]) (insert normal_s1,simp)
    2.24          with normal_s1 normal_s2 eval_args 
    2.25          have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
    2.26 -          by (auto dest: eval_gext intro: conf_gext)
    2.27 +          by (auto dest: eval_gext)
    2.28          from evaln_args wt_args da_args' conf_s1 wf
    2.29          have conf_args: "list_all2 (conf G (store s2)) vs pTs"
    2.30            by (rule evaln_type_sound [elim_format]) (insert normal_s2,simp)
    2.31 @@ -1491,7 +1490,7 @@
    2.32              apply (rule dynM')
    2.33              apply (force dest: ty_expr_is_type)
    2.34              apply (rule invC_widen)
    2.35 -            apply (force intro: conf_gext dest: eval_gext)
    2.36 +            apply (force dest: eval_gext)
    2.37              apply simp
    2.38              apply simp
    2.39              apply (simp add: invC)
     3.1 --- a/src/HOL/Bali/DeclConcepts.thy	Mon Feb 27 17:39:34 2012 +0100
     3.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Mon Feb 27 17:40:59 2012 +0100
     3.3 @@ -2241,7 +2241,7 @@
     3.4    \<Longrightarrow> table_of (fields G C) (fn, declclass f) = Some (fld f)"
     3.5  apply (simp only: accfield_def Let_def)
     3.6  apply (rule table_of_remap_SomeD)
     3.7 -apply (auto dest: filter_tab_SomeD)
     3.8 +apply auto
     3.9  done
    3.10  
    3.11  
     4.1 --- a/src/HOL/Bali/Evaln.thy	Mon Feb 27 17:39:34 2012 +0100
     4.2 +++ b/src/HOL/Bali/Evaln.thy	Mon Feb 27 17:40:59 2012 +0100
     4.3 @@ -233,7 +233,6 @@
     4.4          "G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n\<rightarrow> (v, s')"
     4.5          "G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> (v, s')"
     4.6          "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
     4.7 -        "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
     4.8  
     4.9  declare split_if     [split] split_if_asm     [split] 
    4.10          option.split [split] option.split_asm [split]
    4.11 @@ -575,7 +574,6 @@
    4.12      apply -
    4.13      apply (rule evaln.Loop)
    4.14      apply   (iprover intro: evaln_nonstrict intro: le_maxI1)
    4.15 -
    4.16      apply   (auto intro: evaln_nonstrict intro: le_maxI2)
    4.17      done
    4.18    then show ?case ..
     5.1 --- a/src/HOL/Bali/Example.thy	Mon Feb 27 17:39:34 2012 +0100
     5.2 +++ b/src/HOL/Bali/Example.thy	Mon Feb 27 17:40:59 2012 +0100
     5.3 @@ -975,7 +975,6 @@
     5.4  done
     5.5  
     5.6  declare mhead_resTy_simp [simp add]
     5.7 -declare member_is_static_simp [simp add]
     5.8  
     5.9  lemma wf_BaseC: "wf_cdecl tprg (Base,BaseCl)"
    5.10  apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def)
     6.1 --- a/src/HOL/Bali/TypeSafe.thy	Mon Feb 27 17:39:34 2012 +0100
     6.2 +++ b/src/HOL/Bali/TypeSafe.thy	Mon Feb 27 17:40:59 2012 +0100
     6.3 @@ -28,7 +28,7 @@
     6.4    next
     6.5      case New
     6.6      then show ?case
     6.7 -      by (auto split: split_if_asm)
     6.8 +      by auto
     6.9    qed
    6.10    with eqs 
    6.11    show ?thesis
    6.12 @@ -68,19 +68,18 @@
    6.13   \<Longrightarrow> (check_method_access G accC statT mode sig a' s) = s"
    6.14  apply (cases s)
    6.15  apply (auto simp add: check_method_access_def Let_def error_free_def 
    6.16 -                      abrupt_if_def 
    6.17 -            split: split_if_asm)
    6.18 +                      abrupt_if_def)
    6.19  done
    6.20  
    6.21  lemma error_free_FVar_lemma: 
    6.22       "error_free s 
    6.23         \<Longrightarrow> error_free (abupd (if stat then id else np a) s)"
    6.24 -  by (case_tac s) (auto split: split_if) 
    6.25 +  by (case_tac s) auto
    6.26  
    6.27  lemma error_free_init_lvars [simp,intro]:
    6.28  "error_free s \<Longrightarrow> 
    6.29    error_free (init_lvars G C sig mode a pvs s)"
    6.30 -by (cases s) (auto simp add: init_lvars_def Let_def split: split_if)
    6.31 +by (cases s) (auto simp add: init_lvars_def Let_def)
    6.32  
    6.33  lemma error_free_LVar_lemma:   
    6.34  "error_free s \<Longrightarrow> error_free (assign (\<lambda>v. supd lupd(vn\<mapsto>v)) w s)"
    6.35 @@ -362,12 +361,12 @@
    6.36        case CInst
    6.37        with modeIntVir obj_props
    6.38        show ?thesis 
    6.39 -        by (auto dest!: widen_Array2 split add: split_if)
    6.40 +        by (auto dest!: widen_Array2)
    6.41      next
    6.42        case Arr
    6.43 -      from Arr obtain T where "obj_ty obj = T.[]" by (blast dest: obj_ty_Arr1)
    6.44 +      from Arr obtain T where "obj_ty obj = T.[]" by blast
    6.45        moreover from Arr have "obj_class obj = Object" 
    6.46 -        by (blast dest: obj_class_Arr1)
    6.47 +        by blast
    6.48        moreover note modeIntVir obj_props wf 
    6.49        ultimately show ?thesis by (auto dest!: widen_Array )
    6.50      qed
    6.51 @@ -411,8 +410,7 @@
    6.52                             dynimethd_def dynmethd_C_C 
    6.53                      intro: dynmethd_declclass
    6.54                      dest!: wf_imethdsD
    6.55 -                     dest: table_of_map_SomeI
    6.56 -                    split: split_if_asm)
    6.57 +                     dest: table_of_map_SomeI)
    6.58      next        
    6.59        case SuperM
    6.60        with not_SuperM show ?thesis ..
    6.61 @@ -421,8 +419,7 @@
    6.62        with wf dynlookup IfaceT invC_prop show ?thesis 
    6.63          by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
    6.64                             DynT_prop_def
    6.65 -                    intro: methd_declclass dynmethd_declclass
    6.66 -                    split: split_if_asm)
    6.67 +                    intro: methd_declclass dynmethd_declclass)
    6.68      qed
    6.69    next
    6.70      case ClassT
    6.71 @@ -1851,7 +1848,7 @@
    6.72        (*
    6.73                  wt_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
    6.74                  wt_c2: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"*)
    6.75 -      by (rule wt_elim_cases) (auto split add: split_if)
    6.76 +      by (rule wt_elim_cases) auto
    6.77      from If.prems obtain E C where
    6.78        da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0)::state))) 
    6.79                                         \<guillemotright>In1l e\<guillemotright> E" and
    6.80 @@ -3978,7 +3975,7 @@
    6.81      obtain 
    6.82                wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
    6.83        wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
    6.84 -      by (elim wt_elim_cases) (auto split add: split_if)
    6.85 +      by (elim wt_elim_cases) auto
    6.86      from If.prems obtain E C where
    6.87        da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0)::state))) 
    6.88                                         \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E" and
     7.1 --- a/src/HOL/Bali/WellType.thy	Mon Feb 27 17:39:34 2012 +0100
     7.2 +++ b/src/HOL/Bali/WellType.thy	Mon Feb 27 17:40:59 2012 +0100
     7.3 @@ -546,7 +546,7 @@
     7.4      then show ?thesis by blast
     7.5    next 
     7.6      case False then show ?thesis 
     7.7 -      by (auto simp add: invmode_def split: split_if_asm)
     7.8 +      by (auto simp add: invmode_def)
     7.9    qed
    7.10  qed
    7.11