src/HOL/Bali/Example.thy
changeset 22708 fff918feff45
parent 21404 eb85850d3eb7
child 24019 67bde7cfcf10
     1.1 --- a/src/HOL/Bali/Example.thy	Sun Apr 15 14:32:55 2007 +0200
     1.2 +++ b/src/HOL/Bali/Example.thy	Sun Apr 15 23:25:49 2007 +0200
     1.3 @@ -65,62 +65,62 @@
     1.4  section "type and expression names"
     1.5  
     1.6  (** unfortunately cannot simply instantiate tnam **)
     1.7 -datatype tnam_  = HasFoo_ | Base_ | Ext_ | Main_
     1.8 -datatype vnam_  = arr_ | vee_ | z_ | e_
     1.9 -datatype label_ = lab1_
    1.10 +datatype tnam'  = HasFoo' | Base' | Ext' | Main'
    1.11 +datatype vnam'  = arr' | vee' | z' | e'
    1.12 +datatype label' = lab1'
    1.13  
    1.14  consts
    1.15  
    1.16 -  tnam_ :: "tnam_  \<Rightarrow> tnam"
    1.17 -  vnam_ :: "vnam_  \<Rightarrow> vname"
    1.18 -  label_:: "label_ \<Rightarrow> label"
    1.19 -axioms  (** tnam_, vnam_ and label are intended to be isomorphic 
    1.20 +  tnam' :: "tnam'  \<Rightarrow> tnam"
    1.21 +  vnam' :: "vnam'  \<Rightarrow> vname"
    1.22 +  label':: "label' \<Rightarrow> label"
    1.23 +axioms  (** tnam', vnam' and label are intended to be isomorphic 
    1.24              to tnam, vname and label **)
    1.25  
    1.26 -  inj_tnam_  [simp]: "(tnam_  x = tnam_  y) = (x = y)"
    1.27 -  inj_vnam_  [simp]: "(vnam_  x = vnam_  y) = (x = y)"
    1.28 -  inj_label_ [simp]: "(label_ x = label_ y) = (x = y)"
    1.29 +  inj_tnam'  [simp]: "(tnam'  x = tnam'  y) = (x = y)"
    1.30 +  inj_vnam'  [simp]: "(vnam'  x = vnam'  y) = (x = y)"
    1.31 +  inj_label' [simp]: "(label' x = label' y) = (x = y)"
    1.32    
    1.33    
    1.34 -  surj_tnam_:  "\<exists>m. n = tnam_  m"
    1.35 -  surj_vnam_:  "\<exists>m. n = vnam_  m"
    1.36 -  surj_label_:" \<exists>m. n = label_ m"
    1.37 +  surj_tnam':  "\<exists>m. n = tnam'  m"
    1.38 +  surj_vnam':  "\<exists>m. n = vnam'  m"
    1.39 +  surj_label':" \<exists>m. n = label' m"
    1.40  
    1.41  abbreviation
    1.42    HasFoo :: qtname where
    1.43 -  "HasFoo == \<lparr>pid=java_lang,tid=TName (tnam_ HasFoo_)\<rparr>"
    1.44 +  "HasFoo == \<lparr>pid=java_lang,tid=TName (tnam' HasFoo')\<rparr>"
    1.45  
    1.46  abbreviation
    1.47    Base :: qtname where
    1.48 -  "Base == \<lparr>pid=java_lang,tid=TName (tnam_ Base_)\<rparr>"
    1.49 +  "Base == \<lparr>pid=java_lang,tid=TName (tnam' Base')\<rparr>"
    1.50  
    1.51  abbreviation
    1.52    Ext :: qtname where
    1.53 -  "Ext == \<lparr>pid=java_lang,tid=TName (tnam_ Ext_)\<rparr>"
    1.54 +  "Ext == \<lparr>pid=java_lang,tid=TName (tnam' Ext')\<rparr>"
    1.55  
    1.56  abbreviation
    1.57    Main :: qtname where
    1.58 -  "Main == \<lparr>pid=java_lang,tid=TName (tnam_ Main_)\<rparr>"
    1.59 +  "Main == \<lparr>pid=java_lang,tid=TName (tnam' Main')\<rparr>"
    1.60  
    1.61  abbreviation
    1.62    arr :: vname where
    1.63 -  "arr == (vnam_ arr_)"
    1.64 +  "arr == (vnam' arr')"
    1.65  
    1.66  abbreviation
    1.67    vee :: vname where
    1.68 -  "vee == (vnam_ vee_)"
    1.69 +  "vee == (vnam' vee')"
    1.70  
    1.71  abbreviation
    1.72    z :: vname where
    1.73 -  "z == (vnam_ z_)"
    1.74 +  "z == (vnam' z')"
    1.75  
    1.76  abbreviation
    1.77    e :: vname where
    1.78 -  "e == (vnam_ e_)"
    1.79 +  "e == (vnam' e')"
    1.80  
    1.81  abbreviation
    1.82    lab1:: label where
    1.83 -  "lab1 == label_ lab1_"
    1.84 +  "lab1 == label' lab1'"
    1.85  
    1.86  
    1.87  lemma neq_Base_Object [simp]: "Base\<noteq>Object"
    1.88 @@ -307,9 +307,9 @@
    1.89  lemma not_TName_n_subcls_TName_n [rule_format (no_asm), elim!]: 
    1.90    "(\<lparr>pid=java_lang,tid=TName tn\<rparr>, \<lparr>pid=java_lang,tid=TName tn\<rparr>) 
    1.91     \<in> (subcls1 tprg)^+ \<longrightarrow> R"
    1.92 -apply (rule_tac n1 = "tn" in surj_tnam_ [THEN exE])
    1.93 +apply (rule_tac n1 = "tn" in surj_tnam' [THEN exE])
    1.94  apply (erule ssubst)
    1.95 -apply (rule tnam_.induct)
    1.96 +apply (rule tnam'.induct)
    1.97  apply  safe
    1.98  apply (auto dest!: tranclD subcls1D simp add: BaseCl_def ExtCl_def MainCl_def)
    1.99  apply (drule rtranclD)
   1.100 @@ -435,13 +435,13 @@
   1.101  apply  (simp (no_asm_simp))
   1.102  by (rule ws_tprg [THEN fields_emptyI], force+)
   1.103  
   1.104 -lemmas fields_rec_ = fields_rec [OF _ ws_tprg]
   1.105 +lemmas fields_rec' = fields_rec [OF _ ws_tprg]
   1.106  
   1.107  lemma fields_Base [simp]: 
   1.108  "DeclConcepts.fields tprg Base 
   1.109    = [((arr,Base), \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
   1.110       ((vee,Base), \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)]"
   1.111 -apply (subst fields_rec_)
   1.112 +apply (subst fields_rec')
   1.113  apply   (auto simp add: BaseCl_def)
   1.114  done
   1.115  
   1.116 @@ -450,29 +450,29 @@
   1.117    = [((vee,Ext), \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)] 
   1.118      @ DeclConcepts.fields tprg Base"
   1.119  apply (rule trans)
   1.120 -apply (rule fields_rec_)
   1.121 +apply (rule fields_rec')
   1.122  apply   (auto simp add: ExtCl_def Object_def)
   1.123  done
   1.124  
   1.125 -lemmas imethds_rec_ = imethds_rec [OF _ ws_tprg]
   1.126 -lemmas methd_rec_  = methd_rec  [OF _ ws_tprg]
   1.127 +lemmas imethds_rec' = imethds_rec [OF _ ws_tprg]
   1.128 +lemmas methd_rec'  = methd_rec  [OF _ ws_tprg]
   1.129  
   1.130  lemma imethds_HasFoo [simp]: 
   1.131    "imethds tprg HasFoo = o2s \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
   1.132  apply (rule trans)
   1.133 -apply (rule imethds_rec_)
   1.134 +apply (rule imethds_rec')
   1.135  apply  (auto simp add: HasFooInt_def)
   1.136  done
   1.137  
   1.138  lemma methd_tprg_Object [simp]: "methd tprg Object = empty"
   1.139 -apply (subst methd_rec_)
   1.140 +apply (subst methd_rec')
   1.141  apply (auto simp add: Object_mdecls_def)
   1.142  done
   1.143  
   1.144  lemma methd_Base [simp]: 
   1.145    "methd tprg Base = table_of [(\<lambda>(s,m). (s, Base, m)) Base_foo]"
   1.146  apply (rule trans)
   1.147 -apply (rule methd_rec_)
   1.148 +apply (rule methd_rec')
   1.149  apply   (auto simp add: BaseCl_def)
   1.150  done
   1.151  
   1.152 @@ -527,7 +527,7 @@
   1.153  lemma methd_Ext [simp]: "methd tprg Ext =   
   1.154    table_of [(\<lambda>(s,m). (s, Ext, m)) Ext_foo]"
   1.155  apply (rule trans)
   1.156 -apply (rule methd_rec_)
   1.157 +apply (rule methd_rec')
   1.158  apply   (auto simp add: ExtCl_def Object_def Ext_method_inheritance)
   1.159  done
   1.160