quote "method" to allow Eisbach using this keyword;
authorwenzelm
Thu Mar 12 14:58:32 2015 +0100 (2015-03-12)
changeset 59682d662d096f72b
parent 59675 55eb8932d539
child 59683 d6824d8490be
quote "method" to allow Eisbach using this keyword;
src/HOL/Bali/DeclConcepts.thy
src/HOL/MicroJava/BV/BVNoTypeError.thy
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/NanoJava/TypeRel.thy
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Tue Mar 10 23:04:40 2015 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Thu Mar 12 14:58:32 2015 +0100
     1.3 @@ -368,7 +368,7 @@
     1.4  class) to a qualified member declaration:  @{text method}  *}
     1.5  
     1.6  definition
     1.7 -  method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
     1.8 +  "method" :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
     1.9    where "method sig m = (declclass m, mdecl (sig, mthd m))"
    1.10  
    1.11  lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"
     2.1 --- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Tue Mar 10 23:04:40 2015 +0100
     2.2 +++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Thu Mar 12 14:58:32 2015 +0100
     2.3 @@ -429,14 +429,14 @@
     2.4    fixes G ("\<Gamma>") and Phi ("\<Phi>")
     2.5    assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"  
     2.6    assumes is_class: "is_class \<Gamma> C"
     2.7 -    and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
     2.8 +    and "method": "method (\<Gamma>,C) (m,[]) = Some (C, b)"
     2.9      and m: "m \<noteq> init"
    2.10    defines start: "s \<equiv> start_state \<Gamma> C m"
    2.11  
    2.12    assumes s: "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> t" 
    2.13    shows "t \<noteq> TypeError"
    2.14  proof -
    2.15 -  from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
    2.16 +  from wt is_class "method" have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
    2.17      unfolding start by (rule BV_correct_initial)
    2.18    from wt this s show ?thesis by (rule no_type_errors)
    2.19  qed
    2.20 @@ -461,12 +461,12 @@
    2.21    fixes G ("\<Gamma>") and Phi ("\<Phi>")
    2.22    assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"  
    2.23    assumes is_class: "is_class \<Gamma> C"
    2.24 -    and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
    2.25 +    and "method": "method (\<Gamma>,C) (m,[]) = Some (C, b)"
    2.26      and m: "m \<noteq> init"
    2.27    defines start: "s \<equiv> start_state \<Gamma> C m"
    2.28    shows "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s \<midarrow>jvm\<rightarrow> t"
    2.29  proof -
    2.30 -  from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
    2.31 +  from wt is_class "method" have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
    2.32      unfolding start by (rule BV_correct_initial)
    2.33    with wt show ?thesis by (rule welltyped_commutes)
    2.34  qed
     3.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Mar 10 23:04:40 2015 +0100
     3.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Mar 12 14:58:32 2015 +0100
     3.3 @@ -811,7 +811,7 @@
     3.4  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
     3.5  proof -
     3.6    assume wtprog: "wt_jvm_prog G phi"
     3.7 -  assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
     3.8 +  assume "method": "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
     3.9    assume ins:    "ins ! pc = Invoke C' mn pTs"
    3.10    assume wti:    "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
    3.11    assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
    3.12 @@ -823,7 +823,7 @@
    3.13      wfprog: "wf_prog wfmb G" 
    3.14      by (simp add: wt_jvm_prog_def)
    3.15        
    3.16 -  from ins method approx
    3.17 +  from ins "method" approx
    3.18    obtain s where
    3.19      heap_ok: "G\<turnstile>h hp\<surd>" and
    3.20      prealloc:"preallocated hp" and
    3.21 @@ -880,7 +880,7 @@
    3.22    from stk' l_o l
    3.23    have oX_pos: "last (take (Suc (length pTs)) stk) = oX" by simp
    3.24  
    3.25 -  with state' method ins no_xcp oX_conf
    3.26 +  with state' "method" ins no_xcp oX_conf
    3.27    obtain ref where oX_Addr: "oX = Addr ref"
    3.28      by (auto simp add: raise_system_xcpt_def dest: conf_RefTD)
    3.29  
    3.30 @@ -922,7 +922,7 @@
    3.31        
    3.32    from loc obj_ty have "fst (the (hp ref)) = D" by (simp add: obj_ty_def)
    3.33  
    3.34 -  with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD no_xcp
    3.35 +  with oX_Addr oX_pos state' "method" ins stk' l_o l loc obj_ty mD no_xcp
    3.36    have state'_val:
    3.37      "state' =
    3.38       Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' undefined, 
    3.39 @@ -972,7 +972,7 @@
    3.40      show ?thesis by (simp add: correct_frame_def)
    3.41    qed
    3.42  
    3.43 -  from state'_val heap_ok mD'' ins method phi_pc s X' l mX
    3.44 +  from state'_val heap_ok mD'' ins "method" phi_pc s X' l mX
    3.45         frames s' LT0 c_f is_class_C stk' oX_Addr frame prealloc and l
    3.46    show ?thesis
    3.47      apply (simp add: correct_state_def)
     4.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Mar 10 23:04:40 2015 +0100
     4.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Thu Mar 12 14:58:32 2015 +0100
     4.3 @@ -177,7 +177,7 @@
     4.4  qed
     4.5  
     4.6  consts
     4.7 -  method :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
     4.8 +  "method" :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
     4.9    field  :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty     )" (* ###curry *)
    4.10    fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
    4.11  
     5.1 --- a/src/HOL/NanoJava/TypeRel.thy	Tue Mar 10 23:04:40 2015 +0100
     5.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Thu Mar 12 14:58:32 2015 +0100
     5.3 @@ -108,7 +108,7 @@
     5.4  done
     5.5  
     5.6  --{* Methods of a class, with inheritance and hiding *}
     5.7 -definition method :: "cname => (mname \<rightharpoonup> methd)" where
     5.8 +definition "method" :: "cname => (mname \<rightharpoonup> methd)" where
     5.9    "method C \<equiv> class_rec C methods"
    5.10  
    5.11  lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>