src/HOL/Bali/WellForm.thy
changeset 35416 d8d7d1b785af
parent 35067 af4c18c30593
child 35440 bdf8ad377877
     1.1 --- a/src/HOL/Bali/WellForm.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -31,8 +31,7 @@
     1.4  text  {* well-formed field declaration (common part for classes and interfaces),
     1.5          cf. 8.3 and (9.3) *}
     1.6  
     1.7 -constdefs
     1.8 -  wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool"
     1.9 +definition wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool" where
    1.10   "wf_fdecl G P \<equiv> \<lambda>(fn,f). is_acc_type G P (type f)"
    1.11  
    1.12  lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
    1.13 @@ -55,8 +54,7 @@
    1.14  \item the parameter names are unique
    1.15  \end{itemize} 
    1.16  *}
    1.17 -constdefs
    1.18 -  wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool"
    1.19 +definition wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" where
    1.20   "wf_mhead G P \<equiv> \<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
    1.21                              \<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 
    1.22                              is_acc_type G P (resTy mh) \<and>
    1.23 @@ -78,7 +76,7 @@
    1.24  \end{itemize}
    1.25  *}
    1.26  
    1.27 -constdefs callee_lcl:: "qtname \<Rightarrow> sig \<Rightarrow> methd \<Rightarrow> lenv"
    1.28 +definition callee_lcl :: "qtname \<Rightarrow> sig \<Rightarrow> methd \<Rightarrow> lenv" where
    1.29  "callee_lcl C sig m 
    1.30   \<equiv> \<lambda> k. (case k of
    1.31              EName e 
    1.32 @@ -88,12 +86,11 @@
    1.33                  | Res \<Rightarrow> Some (resTy m))
    1.34            | This \<Rightarrow> if is_static m then None else Some (Class C))"
    1.35  
    1.36 -constdefs parameters :: "methd \<Rightarrow> lname set"
    1.37 +definition parameters :: "methd \<Rightarrow> lname set" where
    1.38  "parameters m \<equiv>  set (map (EName \<circ> VNam) (pars m)) 
    1.39                    \<union> (if (static m) then {} else {This})"
    1.40  
    1.41 -constdefs
    1.42 -  wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool"
    1.43 +definition wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool" where
    1.44   "wf_mdecl G C \<equiv> 
    1.45        \<lambda>(sig,m).
    1.46            wf_mhead G (pid C) sig (mhead m) \<and> 
    1.47 @@ -219,8 +216,7 @@
    1.48        superinterfaces widens to each of the corresponding result types
    1.49  \end{itemize}
    1.50  *}
    1.51 -constdefs
    1.52 -  wf_idecl :: "prog  \<Rightarrow> idecl \<Rightarrow> bool"
    1.53 +definition wf_idecl :: "prog  \<Rightarrow> idecl \<Rightarrow> bool" where
    1.54   "wf_idecl G \<equiv> 
    1.55      \<lambda>(I,i). 
    1.56          ws_idecl G I (isuperIfs i) \<and> 
    1.57 @@ -321,8 +317,7 @@
    1.58  \end{itemize}
    1.59  *}
    1.60  (* to Table *)
    1.61 -constdefs entails:: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
    1.62 -                                 ("_ entails _" 20)
    1.63 +definition entails :: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" ("_ entails _" 20) where
    1.64  "t entails P \<equiv> \<forall>k. \<forall> x \<in> t k: P x"
    1.65  
    1.66  lemma entailsD:
    1.67 @@ -332,8 +327,7 @@
    1.68  lemma empty_entails[simp]: "empty entails P"
    1.69  by (simp add: entails_def)
    1.70  
    1.71 -constdefs
    1.72 - wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool"
    1.73 +definition wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where
    1.74  "wf_cdecl G \<equiv> 
    1.75     \<lambda>(C,c).
    1.76        \<not>is_iface G C \<and>
    1.77 @@ -361,8 +355,7 @@
    1.78              ))"
    1.79  
    1.80  (*
    1.81 -constdefs
    1.82 - wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool"
    1.83 +definition wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where
    1.84  "wf_cdecl G \<equiv> 
    1.85     \<lambda>(C,c).
    1.86        \<not>is_iface G C \<and>
    1.87 @@ -518,8 +511,7 @@
    1.88  \item all defined classes are wellformed
    1.89  \end{itemize}
    1.90  *}
    1.91 -constdefs
    1.92 -  wf_prog  :: "prog \<Rightarrow> bool"
    1.93 +definition wf_prog :: "prog \<Rightarrow> bool" where
    1.94   "wf_prog G \<equiv> let is = ifaces G; cs = classes G in
    1.95                   ObjectC \<in> set cs \<and> 
    1.96                  (\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package) \<and>
    1.97 @@ -919,7 +911,7 @@
    1.98       inheritable: "G \<turnstile>Method old inheritable_in pid C" and
    1.99           subclsC: "G\<turnstile>C\<prec>\<^sub>C declclass old"
   1.100      from cls_C neq_C_Obj  
   1.101 -    have super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c" 
   1.102 +    have super: "G\<turnstile>C \<prec>\<^sub>C1 super c" 
   1.103        by (rule subcls1I)
   1.104      from wf cls_C neq_C_Obj
   1.105      have accessible_super: "G\<turnstile>(Class (super c)) accessible_in (pid C)" 
   1.106 @@ -1385,7 +1377,7 @@
   1.107        moreover note wf False cls_C  
   1.108        ultimately have "G\<turnstile>super c \<preceq>\<^sub>C declclass m"  
   1.109          by (auto intro: Hyp [rule_format])
   1.110 -      moreover from cls_C False have  "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c" by (rule subcls1I)
   1.111 +      moreover from cls_C False have  "G\<turnstile>C \<prec>\<^sub>C1 super c" by (rule subcls1I)
   1.112        ultimately show ?thesis by - (rule rtrancl_into_rtrancl2)
   1.113      next
   1.114        case Some
   1.115 @@ -1539,7 +1531,7 @@
   1.116      by (auto intro: method_declared_inI)
   1.117    note trancl_rtrancl_tranc = trancl_rtrancl_trancl [trans] (* ### in Basis *)
   1.118    from clsC neq_C_Obj
   1.119 -  have subcls1_C_super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c"
   1.120 +  have subcls1_C_super: "G\<turnstile>C \<prec>\<^sub>C1 super c"
   1.121      by (rule subcls1I)
   1.122    then have "G\<turnstile>C \<prec>\<^sub>C super c" ..
   1.123    also from old wf is_cls_super
   1.124 @@ -1609,7 +1601,7 @@
   1.125        by (auto dest: ws_prog_cdeclD)
   1.126      from clsC wf neq_C_Obj 
   1.127      have superAccessible: "G\<turnstile>(Class (super c)) accessible_in (pid C)" and
   1.128 -         subcls1_C_super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c"
   1.129 +         subcls1_C_super: "G\<turnstile>C \<prec>\<^sub>C1 super c"
   1.130        by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD
   1.131                intro: subcls1I)
   1.132      show "\<exists>new. ?Constraint C new old"