# HG changeset patch
# User krauss
# Date 1313957584 -7200
# Node ID dfc2e722fe47314064aba798bab2671d59e4c364
# Parent  0b217404522a576e0ea934b8f3808122f614dbe0
modernized specifications

diff -r 0b217404522a -r dfc2e722fe47 src/HOL/NanoJava/Decl.thy
--- a/src/HOL/NanoJava/Decl.thy	Sun Aug 21 22:13:04 2011 +0200
+++ b/src/HOL/NanoJava/Decl.thy	Sun Aug 21 22:13:04 2011 +0200
@@ -44,9 +44,9 @@
   (type) "cdecl" \<leftharpoondown> (type) "cname \<times> class"
   (type) "prog " \<leftharpoondown> (type) "cdecl list"
 
-consts
-
+axiomatization
   Prog    :: prog       --{* program as a global value *}
+and
   Object  :: cname      --{* name of root class *}
 
 
diff -r 0b217404522a -r dfc2e722fe47 src/HOL/NanoJava/Example.thy
--- a/src/HOL/NanoJava/Example.thy	Sun Aug 21 22:13:04 2011 +0200
+++ b/src/HOL/NanoJava/Example.thy	Sun Aug 21 22:13:04 2011 +0200
@@ -41,17 +41,18 @@
 
 *}
 
-axioms This_neq_Par [simp]: "This \<noteq> Par"
-       Res_neq_This [simp]: "Res  \<noteq> This"
+axiomatization where
+  This_neq_Par [simp]: "This \<noteq> Par" and
+  Res_neq_This [simp]: "Res  \<noteq> This"
 
 
 subsection "Program representation"
 
-consts N    :: cname ("Nat") (* with mixfix because of clash with NatDef.Nat *)
-consts pred :: fname
-consts suc  :: mname
-       add  :: mname
-consts any  :: vname
+axiomatization 
+  N    :: cname ("Nat") (* with mixfix because of clash with NatDef.Nat *)
+  and pred :: fname
+  and suc add :: mname
+  and any  :: vname
 
 abbreviation
   dummy :: expr ("<>")
@@ -64,19 +65,19 @@
 text {* The following properties could be derived from a more complete
         program model, which we leave out for laziness. *}
 
-axioms Nat_no_subclasses [simp]: "D \<preceq>C Nat = (D=Nat)"
+axiomatization where Nat_no_subclasses [simp]: "D \<preceq>C Nat = (D=Nat)"
 
-axioms method_Nat_add [simp]: "method Nat add = Some 
+axiomatization where method_Nat_add [simp]: "method Nat add = Some 
   \<lparr> par=Class Nat, res=Class Nat, lcl=[], 
    bdy= If((LAcc This..pred)) 
           (Res :== {Nat}(LAcc This..pred)..add({Nat}LAcc Par..suc(<>))) 
         Else Res :== LAcc Par \<rparr>"
 
-axioms method_Nat_suc [simp]: "method Nat suc = Some 
+axiomatization where method_Nat_suc [simp]: "method Nat suc = Some 
   \<lparr> par=NT, res=Class Nat, lcl=[], 
    bdy= Res :== new Nat;; LAcc Res..pred :== LAcc This \<rparr>"
 
-axioms field_Nat [simp]: "field Nat = empty(pred\<mapsto>Class Nat)"
+axiomatization where field_Nat [simp]: "field Nat = empty(pred\<mapsto>Class Nat)"
 
 lemma init_locs_Nat_add [simp]: "init_locs Nat add s = s"
 by (simp add: init_locs_def init_vars_def)
diff -r 0b217404522a -r dfc2e722fe47 src/HOL/NanoJava/Term.thy
--- a/src/HOL/NanoJava/Term.thy	Sun Aug 21 22:13:04 2011 +0200
+++ b/src/HOL/NanoJava/Term.thy	Sun Aug 21 22:13:04 2011 +0200
@@ -11,14 +11,13 @@
 typedecl fname  --{* field    name *}
 typedecl vname  --{* variable name *}
 
-consts 
-  This :: vname --{* This pointer *}
-  Par  :: vname --{* method parameter *}
+axiomatization
+  This --{* This pointer *}
+  Par  --{* method parameter *}
   Res  :: vname --{* method result *}
-
-text {* Inequality axioms are not required for the meta theory. *}
+ -- {* Inequality axioms are not required for the meta theory. *}
 (*
-axioms
+where
   This_neq_Par [simp]: "This \<noteq> Par"
   Par_neq_Res  [simp]: "Par \<noteq> Res"
   Res_neq_This [simp]: "Res \<noteq> This"
diff -r 0b217404522a -r dfc2e722fe47 src/HOL/NanoJava/TypeRel.thy
--- a/src/HOL/NanoJava/TypeRel.thy	Sun Aug 21 22:13:04 2011 +0200
+++ b/src/HOL/NanoJava/TypeRel.thy	Sun Aug 21 22:13:04 2011 +0200
@@ -6,8 +6,11 @@
 
 theory TypeRel imports Decl "~~/src/HOL/Library/Wfrec" begin
 
-consts
-  subcls1 :: "(cname \<times> cname) set"  --{* subclass *}
+text{* Direct subclass relation *}
+
+definition subcls1 :: "(cname \<times> cname) set"
+where
+  "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}"
 
 abbreviation
   subcls1_syntax :: "[cname, cname] => bool"  ("_ <=C1 _" [71,71] 70)
@@ -20,17 +23,9 @@
   subcls1_syntax  ("_ \<prec>C1 _"  [71,71] 70) and
   subcls_syntax  ("_ \<preceq>C _"   [71,71] 70)
 
-consts
-  method :: "cname => (mname \<rightharpoonup> methd)"
-  field  :: "cname => (fname \<rightharpoonup> ty)"
-
 
 subsection "Declarations and properties not used in the meta theory"
 
-text{* Direct subclass relation *}
-defs
- subcls1_def: "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}"
-
 text{* Widening, viz. method invocation conversion *}
 inductive
   widen :: "ty => ty => bool"  ("_ \<preceq> _" [71,71] 70)
@@ -111,7 +106,8 @@
 done
 
 --{* Methods of a class, with inheritance and hiding *}
-defs method_def: "method C \<equiv> class_rec C methods"
+definition method :: "cname => (mname \<rightharpoonup> methd)" where
+  "method C \<equiv> class_rec C methods"
 
 lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
 method C = (if C=Object then empty else method (super m)) ++ map_of (methods m)"
@@ -122,7 +118,8 @@
 
 
 --{* Fields of a class, with inheritance and hiding *}
-defs field_def: "field C \<equiv> class_rec C flds"
+definition field  :: "cname => (fname \<rightharpoonup> ty)" where
+  "field C \<equiv> class_rec C flds"
 
 lemma flds_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
 field C = (if C=Object then empty else field (super m)) ++ map_of (flds m)"