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"