--- a/src/HOL/Bali/AxCompl.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/AxCompl.thy Mon Jul 26 18:25:19 2010 +0200
@@ -20,8 +20,9 @@
section "set of not yet initialzed classes"
-definition nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set" where
- "nyinitcls G s \<equiv> {C. is_class G C \<and> \<not> initd C s}"
+definition
+ nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set"
+ where "nyinitcls G s = {C. is_class G C \<and> \<not> initd C s}"
lemma nyinitcls_subset_class: "nyinitcls G s \<subseteq> {C. is_class G C}"
apply (unfold nyinitcls_def)
@@ -113,8 +114,9 @@
section "init-le"
-definition init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool" ("_\<turnstile>init\<le>_" [51,51] 50) where
- "G\<turnstile>init\<le>n \<equiv> \<lambda>s. card (nyinitcls G s) \<le> n"
+definition
+ init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool" ("_\<turnstile>init\<le>_" [51,51] 50)
+ where "G\<turnstile>init\<le>n = (\<lambda>s. card (nyinitcls G s) \<le> n)"
lemma init_le_def2 [simp]: "(G\<turnstile>init\<le>n) s = (card (nyinitcls G s)\<le>n)"
apply (unfold init_le_def)
@@ -132,27 +134,22 @@
section "Most General Triples and Formulas"
-definition remember_init_state :: "state assn" ("\<doteq>") where
- "\<doteq> \<equiv> \<lambda>Y s Z. s = Z"
+definition
+ remember_init_state :: "state assn" ("\<doteq>")
+ where "\<doteq> \<equiv> \<lambda>Y s Z. s = Z"
lemma remember_init_state_def2 [simp]: "\<doteq> Y = op ="
apply (unfold remember_init_state_def)
apply (simp (no_asm))
done
-consts
-
+definition
MGF ::"[state assn, term, prog] \<Rightarrow> state triple" ("{_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
- MGFn::"[nat , term, prog] \<Rightarrow> state triple" ("{=:_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
+ where "{P} t\<succ> {G\<rightarrow>} = {P} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
-defs
-
-
- MGF_def:
- "{P} t\<succ> {G\<rightarrow>} \<equiv> {P} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
-
- MGFn_def:
- "{=:n} t\<succ> {G\<rightarrow>} \<equiv> {\<doteq> \<and>. G\<turnstile>init\<le>n} t\<succ> {G\<rightarrow>}"
+definition
+ MGFn :: "[nat, term, prog] \<Rightarrow> state triple" ("{=:_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
+ where "{=:n} t\<succ> {G\<rightarrow>} = {\<doteq> \<and>. G\<turnstile>init\<le>n} t\<succ> {G\<rightarrow>}"
(* unused *)
lemma MGF_valid: "wf_prog G \<Longrightarrow> G,{}\<Turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
@@ -574,9 +571,9 @@
unroll the loop in iterated evaluations of the expression and evaluations of
the loop body. *}
-definition unroll :: "prog \<Rightarrow> label \<Rightarrow> expr \<Rightarrow> stmt \<Rightarrow> (state \<times> state) set" where
-
- "unroll G l e c \<equiv> {(s,t). \<exists> v s1 s2.
+definition
+ unroll :: "prog \<Rightarrow> label \<Rightarrow> expr \<Rightarrow> stmt \<Rightarrow> (state \<times> state) set" where
+ "unroll G l e c = {(s,t). \<exists> v s1 s2.
G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1 \<and> the_Bool v \<and> normal s1 \<and>
G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> t=(abupd (absorb (Cont l)) s2)}"
--- a/src/HOL/Bali/AxExample.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/AxExample.thy Mon Jul 26 18:25:19 2010 +0200
@@ -8,10 +8,11 @@
imports AxSem Example
begin
-definition arr_inv :: "st \<Rightarrow> bool" where
- "arr_inv \<equiv> \<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and>
+definition
+ arr_inv :: "st \<Rightarrow> bool" where
+ "arr_inv = (\<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and>
values obj (Inl (arr, Base)) = Some (Addr a) \<and>
- heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>"
+ heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>)"
lemma arr_inv_new_obj:
"\<And>a. \<lbrakk>arr_inv s; new_Addr (heap s)=Some a\<rbrakk> \<Longrightarrow> arr_inv (gupd(Inl a\<mapsto>x) s)"
--- a/src/HOL/Bali/AxSem.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/AxSem.thy Mon Jul 26 18:25:19 2010 +0200
@@ -62,8 +62,9 @@
translations
(type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
-definition assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25) where
- "P \<Rightarrow> Q \<equiv> \<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z"
+definition
+ assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25)
+ where "(P \<Rightarrow> Q) = (\<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z)"
lemma assn_imp_def2 [iff]: "(P \<Rightarrow> Q) = (\<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z)"
apply (unfold assn_imp_def)
@@ -75,8 +76,9 @@
subsection "peek-and"
-definition peek_and :: "'a assn \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> 'a assn" (infixl "\<and>." 13) where
- "P \<and>. p \<equiv> \<lambda>Y s Z. P Y s Z \<and> p s"
+definition
+ peek_and :: "'a assn \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> 'a assn" (infixl "\<and>." 13)
+ where "(P \<and>. p) = (\<lambda>Y s Z. P Y s Z \<and> p s)"
lemma peek_and_def2 [simp]: "peek_and P p Y s = (\<lambda>Z. (P Y s Z \<and> p s))"
apply (unfold peek_and_def)
@@ -114,8 +116,9 @@
subsection "assn-supd"
-definition assn_supd :: "'a assn \<Rightarrow> (state \<Rightarrow> state) \<Rightarrow> 'a assn" (infixl ";." 13) where
- "P ;. f \<equiv> \<lambda>Y s' Z. \<exists>s. P Y s Z \<and> s' = f s"
+definition
+ assn_supd :: "'a assn \<Rightarrow> (state \<Rightarrow> state) \<Rightarrow> 'a assn" (infixl ";." 13)
+ where "(P ;. f) = (\<lambda>Y s' Z. \<exists>s. P Y s Z \<and> s' = f s)"
lemma assn_supd_def2 [simp]: "assn_supd P f Y s' Z = (\<exists>s. P Y s Z \<and> s' = f s)"
apply (unfold assn_supd_def)
@@ -124,8 +127,9 @@
subsection "supd-assn"
-definition supd_assn :: "(state \<Rightarrow> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr ".;" 13) where
- "f .; P \<equiv> \<lambda>Y s. P Y (f s)"
+definition
+ supd_assn :: "(state \<Rightarrow> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr ".;" 13)
+ where "(f .; P) = (\<lambda>Y s. P Y (f s))"
lemma supd_assn_def2 [simp]: "(f .; P) Y s = P Y (f s)"
@@ -143,8 +147,9 @@
subsection "subst-res"
-definition subst_res :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<leftarrow>_" [60,61] 60) where
- "P\<leftarrow>w \<equiv> \<lambda>Y. P w"
+definition
+ subst_res :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<leftarrow>_" [60,61] 60)
+ where "P\<leftarrow>w = (\<lambda>Y. P w)"
lemma subst_res_def2 [simp]: "(P\<leftarrow>w) Y = P w"
apply (unfold subst_res_def)
@@ -178,8 +183,9 @@
subsection "subst-Bool"
-definition subst_Bool :: "'a assn \<Rightarrow> bool \<Rightarrow> 'a assn" ("_\<leftarrow>=_" [60,61] 60) where
- "P\<leftarrow>=b \<equiv> \<lambda>Y s Z. \<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b)"
+definition
+ subst_Bool :: "'a assn \<Rightarrow> bool \<Rightarrow> 'a assn" ("_\<leftarrow>=_" [60,61] 60)
+ where "P\<leftarrow>=b = (\<lambda>Y s Z. \<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b))"
lemma subst_Bool_def2 [simp]:
"(P\<leftarrow>=b) Y s Z = (\<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b))"
@@ -193,8 +199,9 @@
subsection "peek-res"
-definition peek_res :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn" where
- "peek_res Pf \<equiv> \<lambda>Y. Pf Y Y"
+definition
+ peek_res :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
+ where "peek_res Pf = (\<lambda>Y. Pf Y Y)"
syntax
"_peek_res" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_:. _" [0,3] 3)
@@ -221,8 +228,9 @@
subsection "ign-res"
-definition ign_res :: " 'a assn \<Rightarrow> 'a assn" ("_\<down>" [1000] 1000) where
- "P\<down> \<equiv> \<lambda>Y s Z. \<exists>Y. P Y s Z"
+definition
+ ign_res :: "'a assn \<Rightarrow> 'a assn" ("_\<down>" [1000] 1000)
+ where "P\<down> = (\<lambda>Y s Z. \<exists>Y. P Y s Z)"
lemma ign_res_def2 [simp]: "P\<down> Y s Z = (\<exists>Y. P Y s Z)"
apply (unfold ign_res_def)
@@ -252,8 +260,9 @@
subsection "peek-st"
-definition peek_st :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn" where
- "peek_st P \<equiv> \<lambda>Y s. P (store s) Y s"
+definition
+ peek_st :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
+ where "peek_st P = (\<lambda>Y s. P (store s) Y s)"
syntax
"_peek_st" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_.. _" [0,3] 3)
@@ -296,8 +305,9 @@
subsection "ign-res-eq"
-definition ign_res_eq :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<down>=_" [60,61] 60) where
- "P\<down>=w \<equiv> \<lambda>Y:. P\<down> \<and>. (\<lambda>s. Y=w)"
+definition
+ ign_res_eq :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<down>=_" [60,61] 60)
+ where "P\<down>=w \<equiv> (\<lambda>Y:. P\<down> \<and>. (\<lambda>s. Y=w))"
lemma ign_res_eq_def2 [simp]: "(P\<down>=w) Y s Z = ((\<exists>Y. P Y s Z) \<and> Y=w)"
apply (unfold ign_res_eq_def)
@@ -326,8 +336,9 @@
subsection "RefVar"
-definition RefVar :: "(state \<Rightarrow> vvar \<times> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr "..;" 13) where
- "vf ..; P \<equiv> \<lambda>Y s. let (v,s') = vf s in P (Var v) s'"
+definition
+ RefVar :: "(state \<Rightarrow> vvar \<times> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr "..;" 13)
+ where "(vf ..; P) = (\<lambda>Y s. let (v,s') = vf s in P (Var v) s')"
lemma RefVar_def2 [simp]: "(vf ..; P) Y s =
P (Var (fst (vf s))) (snd (vf s))"
@@ -337,12 +348,13 @@
subsection "allocation"
-definition Alloc :: "prog \<Rightarrow> obj_tag \<Rightarrow> 'a assn \<Rightarrow> 'a assn" where
- "Alloc G otag P \<equiv> \<lambda>Y s Z.
- \<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z"
+definition
+ Alloc :: "prog \<Rightarrow> obj_tag \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
+ where "Alloc G otag P = (\<lambda>Y s Z. \<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z)"
-definition SXAlloc :: "prog \<Rightarrow> 'a assn \<Rightarrow> 'a assn" where
- "SXAlloc G P \<equiv> \<lambda>Y s Z. \<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z"
+definition
+ SXAlloc :: "prog \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
+ where "SXAlloc G P = (\<lambda>Y s Z. \<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z)"
lemma Alloc_def2 [simp]: "Alloc G otag P Y s Z =
@@ -359,11 +371,12 @@
section "validity"
-definition type_ok :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool" where
- "type_ok G t s \<equiv>
- \<exists>L T C A. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and>
- \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A )
- \<and> s\<Colon>\<preceq>(G,L)"
+definition
+ type_ok :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool" where
+ "type_ok G t s =
+ (\<exists>L T C A. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and>
+ \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A )
+ \<and> s\<Colon>\<preceq>(G,L))"
datatype 'a triple = triple "('a assn)" "term" "('a assn)" (** should be
something like triple = \<forall>'a. triple ('a assn) term ('a assn) **)
@@ -407,34 +420,35 @@
definition mtriples :: "('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<Rightarrow> 'sig \<Rightarrow> expr) \<Rightarrow>
('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<times> 'sig) set \<Rightarrow> 'a triples" ("{{(1_)}/ _-\<succ>/ {(1_)} | _}"[3,65,3,65]75) where
- "{{P} tf-\<succ> {Q} | ms} \<equiv> (\<lambda>(C,sig). {Normal(P C sig)} tf C sig-\<succ> {Q C sig})`ms"
+ "{{P} tf-\<succ> {Q} | ms} = (\<lambda>(C,sig). {Normal(P C sig)} tf C sig-\<succ> {Q C sig})`ms"
-consts
-
- triple_valid :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool"
- ( "_\<Turnstile>_:_" [61,0, 58] 57)
- ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
- ("_,_|\<Turnstile>_" [61,58,58] 57)
+definition
+ triple_valid :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool" ("_\<Turnstile>_:_" [61,0, 58] 57)
+ where
+ "G\<Turnstile>n:t =
+ (case t of {P} t\<succ> {Q} \<Rightarrow>
+ \<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
+ (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z))"
abbreviation
- triples_valid:: "prog \<Rightarrow> nat \<Rightarrow> 'a triples \<Rightarrow> bool"
- ( "_||=_:_" [61,0, 58] 57)
- where "G||=n:ts == Ball ts (triple_valid G n)"
+ triples_valid:: "prog \<Rightarrow> nat \<Rightarrow> 'a triples \<Rightarrow> bool" ( "_||=_:_" [61,0, 58] 57)
+ where "G||=n:ts == Ball ts (triple_valid G n)"
+
+notation (xsymbols)
+ triples_valid ("_|\<Turnstile>_:_" [61,0, 58] 57)
+
+
+definition
+ ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<Turnstile>_" [61,58,58] 57)
+ where "(G,A|\<Turnstile>ts) = (\<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts)"
abbreviation
- ax_valid :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool"
- ( "_,_|=_" [61,58,58] 57)
- where "G,A |=t == G,A|\<Turnstile>{t}"
+ ax_valid :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool" ( "_,_|=_" [61,58,58] 57)
+ where "G,A |=t == G,A|\<Turnstile>{t}"
notation (xsymbols)
- triples_valid ("_|\<Turnstile>_:_" [61,0, 58] 57) and
ax_valid ("_,_\<Turnstile>_" [61,58,58] 57)
-defs triple_valid_def: "G\<Turnstile>n:t \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
- \<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
- (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z)"
-
-defs ax_valids_def:"G,A|\<Turnstile>ts \<equiv> \<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts"
lemma triple_valid_def2: "G\<Turnstile>n:{P} t\<succ> {Q} =
(\<forall>Y s Z. P Y s Z
@@ -625,8 +639,9 @@
axioms
*)
-definition adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" where
-"adapt_pre P Q Q'\<equiv>\<lambda>Y s Z. \<forall>Y' s'. \<exists>Z'. P Y s Z' \<and> (Q Y' s' Z' \<longrightarrow> Q' Y' s' Z)"
+definition
+ adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
+ where "adapt_pre P Q Q' = (\<lambda>Y s Z. \<forall>Y' s'. \<exists>Z'. P Y s Z' \<and> (Q Y' s' Z' \<longrightarrow> Q' Y' s' Z))"
section "rules derived by induction"
--- a/src/HOL/Bali/AxSound.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/AxSound.thy Mon Jul 26 18:25:19 2010 +0200
@@ -9,18 +9,15 @@
section "validity"
-consts
-
- triple_valid2:: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool"
- ( "_\<Turnstile>_\<Colon>_"[61,0, 58] 57)
- ax_valids2:: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool"
- ("_,_|\<Turnstile>\<Colon>_" [61,58,58] 57)
-
-defs triple_valid2_def: "G\<Turnstile>n\<Colon>t \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
- \<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>L. s\<Colon>\<preceq>(G,L)
- \<longrightarrow> (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and>
- \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<longrightarrow>
- (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z \<and> s'\<Colon>\<preceq>(G,L))))"
+definition
+ triple_valid2 :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool" ("_\<Turnstile>_\<Colon>_"[61,0, 58] 57)
+ where
+ "G\<Turnstile>n\<Colon>t =
+ (case t of {P} t\<succ> {Q} \<Rightarrow>
+ \<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>L. s\<Colon>\<preceq>(G,L)
+ \<longrightarrow> (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and>
+ \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<longrightarrow>
+ (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z \<and> s'\<Colon>\<preceq>(G,L)))))"
text {* This definition differs from the ordinary @{text triple_valid_def}
manly in the conclusion: We also ensures conformance of the result state. So
@@ -29,8 +26,10 @@
proof of the axiomatic semantics, in the end we will conclude to
the ordinary definition.
*}
-
-defs ax_valids2_def: "G,A|\<Turnstile>\<Colon>ts \<equiv> \<forall>n. (\<forall>t\<in>A. G\<Turnstile>n\<Colon>t) \<longrightarrow> (\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t)"
+
+definition
+ ax_valids2 :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<Turnstile>\<Colon>_" [61,58,58] 57)
+ where "G,A|\<Turnstile>\<Colon>ts = (\<forall>n. (\<forall>t\<in>A. G\<Turnstile>n\<Colon>t) \<longrightarrow> (\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t))"
lemma triple_valid2_def2: "G\<Turnstile>n\<Colon>{P} t\<succ> {Q} =
(\<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s')\<longrightarrow>
--- a/src/HOL/Bali/Basis.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Basis.thy Mon Jul 26 18:25:19 2010 +0200
@@ -180,31 +180,34 @@
notation sum_case (infixr "'(+')"80)
-consts the_Inl :: "'a + 'b \<Rightarrow> 'a"
- the_Inr :: "'a + 'b \<Rightarrow> 'b"
-primrec "the_Inl (Inl a) = a"
-primrec "the_Inr (Inr b) = b"
+primrec the_Inl :: "'a + 'b \<Rightarrow> 'a"
+ where "the_Inl (Inl a) = a"
+
+primrec the_Inr :: "'a + 'b \<Rightarrow> 'b"
+ where "the_Inr (Inr b) = b"
datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
-consts the_In1 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
- the_In2 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b"
- the_In3 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c"
-primrec "the_In1 (In1 a) = a"
-primrec "the_In2 (In2 b) = b"
-primrec "the_In3 (In3 c) = c"
+primrec the_In1 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
+ where "the_In1 (In1 a) = a"
+
+primrec the_In2 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'b"
+ where "the_In2 (In2 b) = b"
+
+primrec the_In3 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'c"
+ where "the_In3 (In3 c) = c"
abbreviation In1l :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
- where "In1l e == In1 (Inl e)"
+ where "In1l e == In1 (Inl e)"
abbreviation In1r :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
- where "In1r c == In1 (Inr c)"
+ where "In1r c == In1 (Inr c)"
abbreviation the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
- where "the_In1l == the_Inl \<circ> the_In1"
+ where "the_In1l == the_Inl \<circ> the_In1"
abbreviation the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
- where "the_In1r == the_Inr \<circ> the_In1"
+ where "the_In1r == the_Inr \<circ> the_In1"
ML {*
fun sum3_instantiate ctxt thm = map (fn s =>
@@ -232,8 +235,9 @@
text{* Deemed too special for theory Map. *}
-definition chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)" where
- "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
+definition
+ chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
+ where "chg_map f a m = (case m a of None => m | Some b => m(a|->f b))"
lemma chg_map_new[simp]: "m a = None ==> chg_map f a m = m"
by (unfold chg_map_def, auto)
@@ -247,8 +251,9 @@
section "unique association lists"
-definition unique :: "('a \<times> 'b) list \<Rightarrow> bool" where
- "unique \<equiv> distinct \<circ> map fst"
+definition
+ unique :: "('a \<times> 'b) list \<Rightarrow> bool"
+ where "unique = distinct \<circ> map fst"
lemma uniqueD [rule_format (no_asm)]:
"unique l--> (!x y. (x,y):set l --> (!x' y'. (x',y'):set l --> x=x'--> y=y'))"
@@ -296,11 +301,11 @@
section "list patterns"
-consts
- lsplit :: "[['a, 'a list] => 'b, 'a list] => 'b"
-defs
- lsplit_def: "lsplit == %f l. f (hd l) (tl l)"
-(* list patterns -- extends pre-defined type "pttrn" used in abstractions *)
+definition
+ lsplit :: "[['a, 'a list] => 'b, 'a list] => 'b" where
+ "lsplit = (\<lambda>f l. f (hd l) (tl l))"
+
+text {* list patterns -- extends pre-defined type "pttrn" used in abstractions *}
syntax
"_lpttrn" :: "[pttrn,pttrn] => pttrn" ("_#/_" [901,900] 900)
translations
--- a/src/HOL/Bali/Conform.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Conform.thy Mon Jul 26 18:25:19 2010 +0200
@@ -96,8 +96,8 @@
section "value conformance"
-definition conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_" [71,71,71,71] 70) where
- "G,s\<turnstile>v\<Colon>\<preceq>T \<equiv> \<exists>T'\<in>typeof (\<lambda>a. Option.map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T"
+definition conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_" [71,71,71,71] 70)
+ where "G,s\<turnstile>v\<Colon>\<preceq>T = (\<exists>T'\<in>typeof (\<lambda>a. Option.map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T)"
lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
by (auto simp: conf_def)
@@ -177,8 +177,9 @@
section "value list conformance"
-definition lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70) where
- "G,s\<turnstile>vs[\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<exists>v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T"
+definition
+ lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
+ where "G,s\<turnstile>vs[\<Colon>\<preceq>]Ts = (\<forall>n. \<forall>T\<in>Ts n: \<exists>v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T)"
lemma lconfD: "\<lbrakk>G,s\<turnstile>vs[\<Colon>\<preceq>]Ts; Ts n = Some T\<rbrakk> \<Longrightarrow> G,s\<turnstile>(the (vs n))\<Colon>\<preceq>T"
by (force simp: lconf_def)
@@ -260,8 +261,9 @@
*}
-definition wlconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70) where
- "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<forall> v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T"
+definition
+ wlconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70)
+ where "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts = (\<forall>n. \<forall>T\<in>Ts n: \<forall> v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T)"
lemma wlconfD: "\<lbrakk>G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts; Ts n = Some T; vs n = Some v\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T"
by (auto simp: wlconf_def)
@@ -338,11 +340,12 @@
section "object conformance"
-definition oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_" [71,71,71,71] 70) where
- "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<equiv> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and>
+definition
+ oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_" [71,71,71,71] 70) where
+ "(G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r) = (G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and>
(case r of
Heap a \<Rightarrow> is_type G (obj_ty obj)
- | Stat C \<Rightarrow> True)"
+ | Stat C \<Rightarrow> True))"
lemma oconf_is_type: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>Heap a \<Longrightarrow> is_type G (obj_ty obj)"
@@ -373,12 +376,14 @@
section "state conformance"
-definition conforms :: "state \<Rightarrow> env' \<Rightarrow> bool" ("_\<Colon>\<preceq>_" [71,71] 70) where
- "xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in
- (\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj \<Colon>\<preceq>\<surd>r) \<and>
- \<spacespace> G,s\<turnstile>l [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and>
- (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and>
- (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None)"
+definition
+ conforms :: "state \<Rightarrow> env' \<Rightarrow> bool" ("_\<Colon>\<preceq>_" [71,71] 70) where
+ "xs\<Colon>\<preceq>E =
+ (let (G, L) = E; s = snd xs; l = locals s in
+ (\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj \<Colon>\<preceq>\<surd>r) \<and>
+ \<spacespace> G,s\<turnstile>l [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and>
+ (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and>
+ (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None))"
section "conforms"
--- a/src/HOL/Bali/Decl.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Decl.thy Mon Jul 26 18:25:19 2010 +0200
@@ -206,8 +206,9 @@
(type) "mdecl" <= (type) "sig \<times> methd"
-definition mhead :: "methd \<Rightarrow> mhead" where
- "mhead m \<equiv> \<lparr>access=access m, static=static m, pars=pars m, resT=resT m\<rparr>"
+definition
+ mhead :: "methd \<Rightarrow> mhead"
+ where "mhead m = \<lparr>access=access m, static=static m, pars=pars m, resT=resT m\<rparr>"
lemma access_mhead [simp]:"access (mhead m) = access m"
by (simp add: mhead_def)
@@ -237,7 +238,7 @@
definition
memberdecl_memberid_def:
- "memberid m \<equiv> (case m of
+ "memberid m = (case m of
fdecl (vn,f) \<Rightarrow> fid vn
| mdecl (sig,m) \<Rightarrow> mid sig)"
@@ -262,7 +263,7 @@
definition
pair_memberid_def:
- "memberid p \<equiv> memberid (snd p)"
+ "memberid p = memberid (snd p)"
instance ..
@@ -274,8 +275,9 @@
lemma memberid_pair_simp1: "memberid p = memberid (snd p)"
by (simp add: pair_memberid_def)
-definition is_field :: "qtname \<times> memberdecl \<Rightarrow> bool" where
-"is_field m \<equiv> \<exists> declC f. m=(declC,fdecl f)"
+definition
+ is_field :: "qtname \<times> memberdecl \<Rightarrow> bool"
+ where "is_field m = (\<exists> declC f. m=(declC,fdecl f))"
lemma is_fieldD: "is_field m \<Longrightarrow> \<exists> declC f. m=(declC,fdecl f)"
by (simp add: is_field_def)
@@ -283,8 +285,9 @@
lemma is_fieldI: "is_field (C,fdecl f)"
by (simp add: is_field_def)
-definition is_method :: "qtname \<times> memberdecl \<Rightarrow> bool" where
-"is_method membr \<equiv> \<exists> declC m. membr=(declC,mdecl m)"
+definition
+ is_method :: "qtname \<times> memberdecl \<Rightarrow> bool"
+ where "is_method membr = (\<exists>declC m. membr=(declC,mdecl m))"
lemma is_methodD: "is_method membr \<Longrightarrow> \<exists> declC m. membr=(declC,mdecl m)"
by (simp add: is_method_def)
@@ -314,8 +317,9 @@
isuperIfs::qtname list,\<dots>::'a\<rparr>"
(type) "idecl" <= (type) "qtname \<times> iface"
-definition ibody :: "iface \<Rightarrow> ibody" where
- "ibody i \<equiv> \<lparr>access=access i,imethods=imethods i\<rparr>"
+definition
+ ibody :: "iface \<Rightarrow> ibody"
+ where "ibody i = \<lparr>access=access i,imethods=imethods i\<rparr>"
lemma access_ibody [simp]: "(access (ibody i)) = access i"
by (simp add: ibody_def)
@@ -349,8 +353,9 @@
super::qtname,superIfs::qtname list,\<dots>::'a\<rparr>"
(type) "cdecl" <= (type) "qtname \<times> class"
-definition cbody :: "class \<Rightarrow> cbody" where
- "cbody c \<equiv> \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
+definition
+ cbody :: "class \<Rightarrow> cbody"
+ where "cbody c = \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
lemma access_cbody [simp]:"access (cbody c) = access c"
by (simp add: cbody_def)
@@ -368,18 +373,17 @@
section "standard classes"
consts
-
Object_mdecls :: "mdecl list" --{* methods of Object *}
SXcpt_mdecls :: "mdecl list" --{* methods of SXcpts *}
- ObjectC :: "cdecl" --{* declaration of root class *}
- SXcptC ::"xname \<Rightarrow> cdecl" --{* declarations of throwable classes *}
-
-defs
+definition
+ ObjectC :: "cdecl" --{* declaration of root class *} where
+ "ObjectC = (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
+ init=Skip,super=undefined,superIfs=[]\<rparr>)"
-ObjectC_def:"ObjectC \<equiv> (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
- init=Skip,super=undefined,superIfs=[]\<rparr>)"
-SXcptC_def:"SXcptC xn\<equiv> (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
+definition
+ SXcptC ::"xname \<Rightarrow> cdecl" --{* declarations of throwable classes *} where
+ "SXcptC xn = (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
init=Skip,
super=if xn = Throwable then Object
else SXcpt Throwable,
@@ -391,8 +395,9 @@
lemma SXcptC_inject [simp]: "(SXcptC xn = SXcptC xm) = (xn = xm)"
by (simp add: SXcptC_def)
-definition standard_classes :: "cdecl list" where
- "standard_classes \<equiv> [ObjectC, SXcptC Throwable,
+definition
+ standard_classes :: "cdecl list" where
+ "standard_classes = [ObjectC, SXcptC Throwable,
SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast,
SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"
@@ -426,16 +431,15 @@
section "is type"
-consts
- is_type :: "prog \<Rightarrow> ty \<Rightarrow> bool"
- isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
-
-primrec "is_type G (PrimT pt) = True"
- "is_type G (RefT rt) = isrtype G rt"
- "isrtype G (NullT ) = True"
- "isrtype G (IfaceT tn) = is_iface G tn"
- "isrtype G (ClassT tn) = is_class G tn"
- "isrtype G (ArrayT T ) = is_type G T"
+primrec is_type :: "prog \<Rightarrow> ty \<Rightarrow> bool"
+ and isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
+where
+ "is_type G (PrimT pt) = True"
+| "is_type G (RefT rt) = isrtype G rt"
+| "isrtype G (NullT) = True"
+| "isrtype G (IfaceT tn) = is_iface G tn"
+| "isrtype G (ClassT tn) = is_class G tn"
+| "isrtype G (ArrayT T ) = is_type G T"
lemma type_is_iface: "is_type G (Iface I) \<Longrightarrow> is_iface G I"
by auto
@@ -446,13 +450,13 @@
section "subinterface and subclass relation, in anticipation of TypeRel.thy"
-consts
+definition
subint1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subinterface *}
- subcls1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subclass *}
+ where "subint1 G = {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
-defs
- subint1_def: "subint1 G \<equiv> {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
- subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
+definition
+ subcls1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subclass *}
+ where "subcls1 G = {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
abbreviation
subcls1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
@@ -517,15 +521,18 @@
section "well-structured programs"
-definition ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool" where
- "ws_idecl G I si \<equiv> \<forall>J\<in>set si. is_iface G J \<and> (J,I)\<notin>(subint1 G)^+"
+definition
+ ws_idecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname list \<Rightarrow> bool"
+ where "ws_idecl G I si = (\<forall>J\<in>set si. is_iface G J \<and> (J,I)\<notin>(subint1 G)^+)"
-definition ws_cdecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" where
- "ws_cdecl G C sc \<equiv> C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+"
+definition
+ ws_cdecl :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool"
+ where "ws_cdecl G C sc = (C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+)"
-definition ws_prog :: "prog \<Rightarrow> bool" where
- "ws_prog G \<equiv> (\<forall>(I,i)\<in>set (ifaces G). ws_idecl G I (isuperIfs i)) \<and>
- (\<forall>(C,c)\<in>set (classes G). ws_cdecl G C (super c))"
+definition
+ ws_prog :: "prog \<Rightarrow> bool" where
+ "ws_prog G = ((\<forall>(I,i)\<in>set (ifaces G). ws_idecl G I (isuperIfs i)) \<and>
+ (\<forall>(C,c)\<in>set (classes G). ws_cdecl G C (super c)))"
lemma ws_progI:
@@ -810,10 +817,10 @@
apply simp
done
-definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
+definition
+ imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
--{* methods of an interface, with overriding and inheritance, cf. 9.2 *}
-"imethds G I
- \<equiv> iface_rec G I
+ "imethds G I = iface_rec G I
(\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
(Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
--- a/src/HOL/Bali/DeclConcepts.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy Mon Jul 26 18:25:19 2010 +0200
@@ -9,7 +9,7 @@
section "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"
definition is_public :: "prog \<Rightarrow> qtname \<Rightarrow> bool" where
-"is_public G qn \<equiv> (case class G qn of
+"is_public G qn = (case class G qn of
None \<Rightarrow> (case iface G qn of
None \<Rightarrow> False
| Some i \<Rightarrow> access i = Public)
@@ -21,33 +21,35 @@
in their package or if they are defined public, an array type is accessible if
its element type is accessible *}
-consts accessible_in :: "prog \<Rightarrow> ty \<Rightarrow> pname \<Rightarrow> bool"
- ("_ \<turnstile> _ accessible'_in _" [61,61,61] 60)
- rt_accessible_in:: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool"
- ("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60)
primrec
-"G\<turnstile>(PrimT p) accessible_in pack = True"
-accessible_in_RefT_simp:
-"G\<turnstile>(RefT r) accessible_in pack = G\<turnstile>r accessible_in' pack"
-
-"G\<turnstile>(NullT) accessible_in' pack = True"
-"G\<turnstile>(IfaceT I) accessible_in' pack = ((pid I = pack) \<or> is_public G I)"
-"G\<turnstile>(ClassT C) accessible_in' pack = ((pid C = pack) \<or> is_public G C)"
-"G\<turnstile>(ArrayT ty) accessible_in' pack = G\<turnstile>ty accessible_in pack"
+ accessible_in :: "prog \<Rightarrow> ty \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ accessible'_in _" [61,61,61] 60) and
+ rt_accessible_in :: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60)
+where
+ "G\<turnstile>(PrimT p) accessible_in pack = True"
+| accessible_in_RefT_simp:
+ "G\<turnstile>(RefT r) accessible_in pack = G\<turnstile>r accessible_in' pack"
+| "G\<turnstile>(NullT) accessible_in' pack = True"
+| "G\<turnstile>(IfaceT I) accessible_in' pack = ((pid I = pack) \<or> is_public G I)"
+| "G\<turnstile>(ClassT C) accessible_in' pack = ((pid C = pack) \<or> is_public G C)"
+| "G\<turnstile>(ArrayT ty) accessible_in' pack = G\<turnstile>ty accessible_in pack"
declare accessible_in_RefT_simp [simp del]
-definition is_acc_class :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool" where
- "is_acc_class G P C \<equiv> is_class G C \<and> G\<turnstile>(Class C) accessible_in P"
+definition
+ is_acc_class :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
+ where "is_acc_class G P C = (is_class G C \<and> G\<turnstile>(Class C) accessible_in P)"
-definition is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool" where
- "is_acc_iface G P I \<equiv> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P"
+definition
+ is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool"
+ where "is_acc_iface G P I = (is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P)"
-definition is_acc_type :: "prog \<Rightarrow> pname \<Rightarrow> ty \<Rightarrow> bool" where
- "is_acc_type G P T \<equiv> is_type G T \<and> G\<turnstile>T accessible_in P"
+definition
+ is_acc_type :: "prog \<Rightarrow> pname \<Rightarrow> ty \<Rightarrow> bool"
+ where "is_acc_type G P T = (is_type G T \<and> G\<turnstile>T accessible_in P)"
-definition is_acc_reftype :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool" where
- "is_acc_reftype G P T \<equiv> isrtype G T \<and> G\<turnstile>T accessible_in' P"
+definition
+ is_acc_reftype :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool"
+ where "is_acc_reftype G P T = (isrtype G T \<and> G\<turnstile>T accessible_in' P)"
lemma is_acc_classD:
"is_acc_class G P C \<Longrightarrow> is_class G C \<and> G\<turnstile>(Class C) accessible_in P"
@@ -87,7 +89,7 @@
begin
definition
- acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
+ acc_modi_accmodi_def: "accmodi (a::acc_modi) = a"
instance ..
@@ -100,7 +102,7 @@
begin
definition
- decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
+ decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) = access d"
instance ..
@@ -113,7 +115,7 @@
begin
definition
- pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
+ pair_acc_modi_def: "accmodi p = accmodi (snd p)"
instance ..
@@ -126,7 +128,7 @@
begin
definition
- memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
+ memberdecl_acc_modi_def: "accmodi m = (case m of
fdecl f \<Rightarrow> accmodi f
| mdecl m \<Rightarrow> accmodi m)"
@@ -152,7 +154,7 @@
begin
definition
- "declclass q \<equiv> \<lparr> pid = pid q, tid = tid q \<rparr>"
+ "declclass q = \<lparr> pid = pid q, tid = tid q \<rparr>"
instance ..
@@ -169,7 +171,7 @@
begin
definition
- pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
+ pair_declclass_def: "declclass p = declclass (fst p)"
instance ..
@@ -208,7 +210,7 @@
begin
definition
- pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
+ pair_is_static_def: "is_static p = is_static (snd p)"
instance ..
@@ -225,7 +227,7 @@
definition
memberdecl_is_static_def:
- "is_static m \<equiv> (case m of
+ "is_static m = (case m of
fdecl f \<Rightarrow> is_static f
| mdecl m \<Rightarrow> is_static m)"
@@ -246,28 +248,34 @@
-- {* some mnemotic selectors for various pairs *}
-definition decliface :: "qtname \<times> 'a decl_scheme \<Rightarrow> qtname" where
+definition
+ decliface :: "qtname \<times> 'a decl_scheme \<Rightarrow> qtname" where
"decliface = fst" --{* get the interface component *}
-definition mbr :: "qtname \<times> memberdecl \<Rightarrow> memberdecl" where
+definition
+ mbr :: "qtname \<times> memberdecl \<Rightarrow> memberdecl" where
"mbr = snd" --{* get the memberdecl component *}
-definition mthd :: "'b \<times> 'a \<Rightarrow> 'a" where
+definition
+ mthd :: "'b \<times> 'a \<Rightarrow> 'a" where
"mthd = snd" --{* get the method component *}
--{* also used for mdecl, mhead *}
-definition fld :: "'b \<times> 'a decl_scheme \<Rightarrow> 'a decl_scheme" where
+definition
+ fld :: "'b \<times> 'a decl_scheme \<Rightarrow> 'a decl_scheme" where
"fld = snd" --{* get the field component *}
--{* also used for @{text "((vname \<times> qtname)\<times> field)"} *}
-- {* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
-definition fname:: "vname \<times> 'a \<Rightarrow> vname" where
- "fname = fst"
+definition
+ fname:: "vname \<times> 'a \<Rightarrow> vname"
+ where "fname = fst"
--{* also used for fdecl *}
-definition declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname" where
- "declclassf = snd"
+definition
+ declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname"
+ where "declclassf = snd"
lemma decliface_simp[simp]: "decliface (I,m) = I"
@@ -320,11 +328,13 @@
--{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
-definition fldname :: "vname \<times> qtname \<Rightarrow> vname" where
- "fldname = fst"
+definition
+ fldname :: "vname \<times> qtname \<Rightarrow> vname"
+ where "fldname = fst"
-definition fldclass :: "vname \<times> qtname \<Rightarrow> qtname" where
- "fldclass = snd"
+definition
+ fldclass :: "vname \<times> qtname \<Rightarrow> qtname"
+ where "fldclass = snd"
lemma fldname_simp[simp]: "fldname (n,c) = n"
by (simp add: fldname_def)
@@ -338,8 +348,9 @@
text {* Convert a qualified method declaration (qualified with its declaring
class) to a qualified member declaration: @{text methdMembr} *}
-definition methdMembr :: "qtname \<times> mdecl \<Rightarrow> qtname \<times> memberdecl" where
- "methdMembr m = (fst m, mdecl (snd m))"
+definition
+ methdMembr :: "qtname \<times> mdecl \<Rightarrow> qtname \<times> memberdecl"
+ where "methdMembr m = (fst m, mdecl (snd m))"
lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)"
by (simp add: methdMembr_def)
@@ -356,8 +367,9 @@
text {* Convert a qualified method (qualified with its declaring
class) to a qualified member declaration: @{text method} *}
-definition method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)" where
-"method sig m \<equiv> (declclass m, mdecl (sig, mthd m))"
+definition
+ method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
+ where "method sig m = (declclass m, mdecl (sig, mthd m))"
lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"
by (simp add: method_def)
@@ -377,8 +389,9 @@
lemma memberid_method_simp[simp]: "memberid (method sig m) = mid sig"
by (simp add: method_def)
-definition fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)" where
-"fieldm n f \<equiv> (declclass f, fdecl (n, fld f))"
+definition
+ fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)"
+ where "fieldm n f = (declclass f, fdecl (n, fld f))"
lemma fieldm_simp[simp]: "fieldm n (C,f) = (C,fdecl (n,f))"
by (simp add: fieldm_def)
@@ -401,8 +414,9 @@
text {* Select the signature out of a qualified method declaration:
@{text msig} *}
-definition msig :: "(qtname \<times> mdecl) \<Rightarrow> sig" where
-"msig m \<equiv> fst (snd m)"
+definition
+ msig :: "(qtname \<times> mdecl) \<Rightarrow> sig"
+ where "msig m = fst (snd m)"
lemma msig_simp[simp]: "msig (c,(s,m)) = s"
by (simp add: msig_def)
@@ -410,8 +424,9 @@
text {* Convert a qualified method (qualified with its declaring
class) to a qualified method declaration: @{text qmdecl} *}
-definition qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)" where
-"qmdecl sig m \<equiv> (declclass m, (sig,mthd m))"
+definition
+ qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)"
+ where "qmdecl sig m = (declclass m, (sig,mthd m))"
lemma qmdecl_simp[simp]: "qmdecl sig (C,m) = (C,(sig,m))"
by (simp add: qmdecl_def)
@@ -476,7 +491,7 @@
begin
definition
- pair_resTy_def: "resTy p \<equiv> resTy (snd p)"
+ pair_resTy_def: "resTy p = resTy (snd p)"
instance ..
@@ -503,14 +518,15 @@
it is not accessible for inheritance at all.
\end{itemize}
*}
-definition inheritable_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60) where
-
-"G\<turnstile>membr inheritable_in pack
- \<equiv> (case (accmodi membr) of
- Private \<Rightarrow> False
- | Package \<Rightarrow> (pid (declclass membr)) = pack
- | Protected \<Rightarrow> True
- | Public \<Rightarrow> True)"
+definition
+ inheritable_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60)
+where
+"G\<turnstile>membr inheritable_in pack =
+ (case (accmodi membr) of
+ Private \<Rightarrow> False
+ | Package \<Rightarrow> (pid (declclass membr)) = pack
+ | Protected \<Rightarrow> True
+ | Public \<Rightarrow> True)"
abbreviation
Method_inheritable_in_syntax::
@@ -526,24 +542,26 @@
subsubsection "declared-in/undeclared-in"
-definition cdeclaredmethd :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,methd) table" where
-"cdeclaredmethd G C
- \<equiv> (case class G C of
+definition
+ cdeclaredmethd :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,methd) table" where
+ "cdeclaredmethd G C =
+ (case class G C of
None \<Rightarrow> \<lambda> sig. None
- | Some c \<Rightarrow> table_of (methods c)
- )"
+ | Some c \<Rightarrow> table_of (methods c))"
-definition cdeclaredfield :: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table" where
-"cdeclaredfield G C
- \<equiv> (case class G C of
- None \<Rightarrow> \<lambda> sig. None
- | Some c \<Rightarrow> table_of (cfields c)
- )"
+definition
+ cdeclaredfield :: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table" where
+ "cdeclaredfield G C =
+ (case class G C of
+ None \<Rightarrow> \<lambda> sig. None
+ | Some c \<Rightarrow> table_of (cfields c))"
-definition declared_in :: "prog \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ declared'_in _" [61,61,61] 60) where
-"G\<turnstile>m declared_in C \<equiv> (case m of
- fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn = Some f
- | mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
+definition
+ declared_in :: "prog \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ declared'_in _" [61,61,61] 60)
+where
+ "G\<turnstile>m declared_in C = (case m of
+ fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn = Some f
+ | mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
abbreviation
method_declared_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
@@ -560,10 +578,12 @@
by (cases m)
(auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)
-definition undeclared_in :: "prog \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ undeclared'_in _" [61,61,61] 60) where
-"G\<turnstile>m undeclared_in C \<equiv> (case m of
- fid fn \<Rightarrow> cdeclaredfield G C fn = None
- | mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
+definition
+ undeclared_in :: "prog \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile> _ undeclared'_in _" [61,61,61] 60)
+where
+ "G\<turnstile>m undeclared_in C = (case m of
+ fid fn \<Rightarrow> cdeclaredfield G C fn = None
+ | mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
subsubsection "members"
@@ -607,17 +627,20 @@
("_ \<turnstile>Field _ _ member'_of _" [61,61,61] 60)
where "G\<turnstile>Field n f member_of C == G\<turnstile>fieldm n f member_of C"
-definition inherits :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool" ("_ \<turnstile> _ inherits _" [61,61,61] 60) where
-"G\<turnstile>C inherits m
- \<equiv> G\<turnstile>m inheritable_in (pid C) \<and> G\<turnstile>memberid m undeclared_in C \<and>
- (\<exists> S. G\<turnstile>C \<prec>\<^sub>C1 S \<and> G\<turnstile>(Class S) accessible_in (pid C) \<and> G\<turnstile>m member_of S)"
+definition
+ inherits :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool" ("_ \<turnstile> _ inherits _" [61,61,61] 60)
+where
+ "G\<turnstile>C inherits m =
+ (G\<turnstile>m inheritable_in (pid C) \<and> G\<turnstile>memberid m undeclared_in C \<and>
+ (\<exists>S. G\<turnstile>C \<prec>\<^sub>C1 S \<and> G\<turnstile>(Class S) accessible_in (pid C) \<and> G\<turnstile>m member_of S))"
lemma inherits_member: "G\<turnstile>C inherits m \<Longrightarrow> G\<turnstile>m member_of C"
by (auto simp add: inherits_def intro: members.Inherited)
-definition member_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ member'_in _" [61,61,61] 60) where
-"G\<turnstile>m member_in C \<equiv> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC"
+definition
+ member_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ member'_in _" [61,61,61] 60)
+ where "G\<turnstile>m member_in C = (\<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC)"
text {* A member is in a class if it is member of the class or a superclass.
If a member is in a class we can select this member. This additional notion
is necessary since not all members are inherited to subclasses. So such
@@ -703,13 +726,15 @@
subsubsection "Hiding"
-definition hides :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" ("_\<turnstile> _ hides _" [61,61,61] 60) where
-"G\<turnstile>new hides old
- \<equiv> is_static new \<and> msig new = msig old \<and>
- G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
- G\<turnstile>Method new declared_in (declclass new) \<and>
- G\<turnstile>Method old declared_in (declclass old) \<and>
- G\<turnstile>Method old inheritable_in pid (declclass new)"
+definition
+ hides :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" ("_\<turnstile> _ hides _" [61,61,61] 60)
+where
+ "G\<turnstile>new hides old =
+ (is_static new \<and> msig new = msig old \<and>
+ G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
+ G\<turnstile>Method new declared_in (declclass new) \<and>
+ G\<turnstile>Method old declared_in (declclass old) \<and>
+ G\<turnstile>Method old inheritable_in pid (declclass new))"
abbreviation
sig_hides:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool"
@@ -762,16 +787,18 @@
by (auto simp add: hides_def)
subsubsection "permits access"
-definition permits_acc :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60) where
-"G\<turnstile>membr in cls permits_acc_from accclass
- \<equiv> (case (accmodi membr) of
- Private \<Rightarrow> (declclass membr = accclass)
- | Package \<Rightarrow> (pid (declclass membr) = pid accclass)
- | Protected \<Rightarrow> (pid (declclass membr) = pid accclass)
+definition
+ permits_acc :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ in _ permits'_acc'_from _" [61,61,61,61] 60)
+where
+ "G\<turnstile>membr in cls permits_acc_from accclass =
+ (case (accmodi membr) of
+ Private \<Rightarrow> (declclass membr = accclass)
+ | Package \<Rightarrow> (pid (declclass membr) = pid accclass)
+ | Protected \<Rightarrow> (pid (declclass membr) = pid accclass)
\<or>
(G\<turnstile>accclass \<prec>\<^sub>C declclass membr
\<and> (G\<turnstile>cls \<preceq>\<^sub>C accclass \<or> is_static membr))
- | Public \<Rightarrow> True)"
+ | Public \<Rightarrow> True)"
text {*
The subcondition of the @{term "Protected"} case:
@{term "G\<turnstile>accclass \<prec>\<^sub>C declclass membr"} could also be relaxed to:
@@ -1380,24 +1407,25 @@
translations
(type) "fspec" <= (type) "vname \<times> qtname"
-definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
-"imethds G I
- \<equiv> iface_rec G I
- (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
+definition
+ imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
+ "imethds G I =
+ iface_rec G I (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
(Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
-definition accimethds :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
-"accimethds G pack I
- \<equiv> if G\<turnstile>Iface I accessible_in pack
- then imethds G I
- else (\<lambda> k. {})"
+definition
+ accimethds :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
+ "accimethds G pack I =
+ (if G\<turnstile>Iface I accessible_in pack
+ then imethds G I
+ else (\<lambda> k. {}))"
text {* only returns imethds if the interface is accessible *}
-definition methd :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
-
-"methd G C
- \<equiv> class_rec G C empty
+definition
+ methd :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
+ "methd G C =
+ class_rec G C empty
(\<lambda>C c subcls_mthds.
filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)
subcls_mthds
@@ -1409,10 +1437,10 @@
Every new method with the same signature coalesces the
method of a superclass. *}
-definition accmethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
-"accmethd G S C
- \<equiv> filter_tab (\<lambda>sig m. G\<turnstile>method sig m of C accessible_from S)
- (methd G C)"
+definition
+ accmethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
+ "accmethd G S C =
+ filter_tab (\<lambda>sig m. G\<turnstile>method sig m of C accessible_from S) (methd G C)"
text {* @{term "accmethd G S C"}: only those methods of @{term "methd G C"},
accessible from S *}
@@ -1423,23 +1451,24 @@
So we must test accessibility of method @{term m} of class @{term C}
(not @{term "declclass m"}) *}
-definition dynmethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
-"dynmethd G statC dynC
- \<equiv> \<lambda> sig.
- (if G\<turnstile>dynC \<preceq>\<^sub>C statC
- then (case methd G statC sig of
- None \<Rightarrow> None
- | Some statM
- \<Rightarrow> (class_rec G dynC empty
- (\<lambda>C c subcls_mthds.
- subcls_mthds
- ++
- (filter_tab
- (\<lambda> _ dynM. G,sig\<turnstile>dynM overrides statM \<or> dynM=statM)
- (methd G C) ))
- ) sig
- )
- else None)"
+definition
+ dynmethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
+ "dynmethd G statC dynC =
+ (\<lambda>sig.
+ (if G\<turnstile>dynC \<preceq>\<^sub>C statC
+ then (case methd G statC sig of
+ None \<Rightarrow> None
+ | Some statM
+ \<Rightarrow> (class_rec G dynC empty
+ (\<lambda>C c subcls_mthds.
+ subcls_mthds
+ ++
+ (filter_tab
+ (\<lambda> _ dynM. G,sig\<turnstile>dynM overrides statM \<or> dynM=statM)
+ (methd G C) ))
+ ) sig
+ )
+ else None))"
text {* @{term "dynmethd G statC dynC"}: dynamic method lookup of a reference
with dynamic class @{term dynC} and static class @{term statC} *}
@@ -1449,11 +1478,12 @@
filters the new methods (to get only those methods which actually
override the methods of the static class) *}
-definition dynimethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
-"dynimethd G I dynC
- \<equiv> \<lambda> sig. if imethds G I sig \<noteq> {}
- then methd G dynC sig
- else dynmethd G Object dynC sig"
+definition
+ dynimethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
+ "dynimethd G I dynC =
+ (\<lambda>sig. if imethds G I sig \<noteq> {}
+ then methd G dynC sig
+ else dynmethd G Object dynC sig)"
text {* @{term "dynimethd G I dynC"}: dynamic method lookup of a reference with
dynamic class dynC and static interface type I *}
text {*
@@ -1468,31 +1498,34 @@
down to the actual dynamic class.
*}
-definition dynlookup :: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
-"dynlookup G statT dynC
- \<equiv> (case statT of
- NullT \<Rightarrow> empty
- | IfaceT I \<Rightarrow> dynimethd G I dynC
- | ClassT statC \<Rightarrow> dynmethd G statC dynC
- | ArrayT ty \<Rightarrow> dynmethd G Object dynC)"
+definition
+ dynlookup :: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
+ "dynlookup G statT dynC =
+ (case statT of
+ NullT \<Rightarrow> empty
+ | IfaceT I \<Rightarrow> dynimethd G I dynC
+ | ClassT statC \<Rightarrow> dynmethd G statC dynC
+ | ArrayT ty \<Rightarrow> dynmethd G Object dynC)"
text {* @{term "dynlookup G statT dynC"}: dynamic lookup of a method within the
static reference type statT and the dynamic class dynC.
In a wellformd context statT will not be NullT and in case
statT is an array type, dynC=Object *}
-definition fields :: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list" where
-"fields G C
- \<equiv> class_rec G C [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
+definition
+ fields :: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list" where
+ "fields G C =
+ class_rec G C [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
text {* @{term "fields G C"}
list of fields of a class, including all the fields of the superclasses
(private, inherited and hidden ones) not only the accessible ones
(an instance of a object allocates all these fields *}
-definition accfield :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (vname, qtname \<times> field) table" where
-"accfield G S C
- \<equiv> let field_tab = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (fields G C))
- in filter_tab (\<lambda>n (declC,f). G\<turnstile> (declC,fdecl (n,f)) of C accessible_from S)
- field_tab"
+definition
+ accfield :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (vname, qtname \<times> field) table" where
+ "accfield G S C =
+ (let field_tab = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (fields G C))
+ in filter_tab (\<lambda>n (declC,f). G\<turnstile> (declC,fdecl (n,f)) of C accessible_from S)
+ field_tab)"
text {* @{term "accfield G C S"}: fields of a class @{term C} which are
accessible from scope of class
@{term S} with inheritance and hiding, cf. 8.3 *}
@@ -1503,11 +1536,13 @@
inheritance, too. So we must test accessibility of field @{term f} of class
@{term C} (not @{term "declclass f"}) *}
-definition is_methd :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> bool" where
- "is_methd G \<equiv> \<lambda>C sig. is_class G C \<and> methd G C sig \<noteq> None"
+definition
+ is_methd :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> bool"
+ where "is_methd G = (\<lambda>C sig. is_class G C \<and> methd G C sig \<noteq> None)"
-definition efname :: "((vname \<times> qtname) \<times> field) \<Rightarrow> (vname \<times> qtname)" where
-"efname \<equiv> fst"
+definition
+ efname :: "((vname \<times> qtname) \<times> field) \<Rightarrow> (vname \<times> qtname)"
+ where "efname = fst"
lemma efname_simp[simp]:"efname (n,f) = n"
by (simp add: efname_def)
@@ -2270,8 +2305,9 @@
section "calculation of the superclasses of a class"
-definition superclasses :: "prog \<Rightarrow> qtname \<Rightarrow> qtname set" where
- "superclasses G C \<equiv> class_rec G C {}
+definition
+ superclasses :: "prog \<Rightarrow> qtname \<Rightarrow> qtname set" where
+ "superclasses G C = class_rec G C {}
(\<lambda> C c superclss. (if C=Object
then {}
else insert (super c) superclss))"
--- a/src/HOL/Bali/DefiniteAssignment.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy Mon Jul 26 18:25:19 2010 +0200
@@ -49,33 +49,33 @@
with a jump, since no breaks, continues or returns are allowed in an
expression. *}
-consts jumpNestingOkS :: "jump set \<Rightarrow> stmt \<Rightarrow> bool"
-primrec
-"jumpNestingOkS jmps (Skip) = True"
-"jumpNestingOkS jmps (Expr e) = True"
-"jumpNestingOkS jmps (j\<bullet> s) = jumpNestingOkS ({j} \<union> jmps) s"
-"jumpNestingOkS jmps (c1;;c2) = (jumpNestingOkS jmps c1 \<and>
- jumpNestingOkS jmps c2)"
-"jumpNestingOkS jmps (If(e) c1 Else c2) = (jumpNestingOkS jmps c1 \<and>
- jumpNestingOkS jmps c2)"
-"jumpNestingOkS jmps (l\<bullet> While(e) c) = jumpNestingOkS ({Cont l} \<union> jmps) c"
+primrec jumpNestingOkS :: "jump set \<Rightarrow> stmt \<Rightarrow> bool"
+where
+ "jumpNestingOkS jmps (Skip) = True"
+| "jumpNestingOkS jmps (Expr e) = True"
+| "jumpNestingOkS jmps (j\<bullet> s) = jumpNestingOkS ({j} \<union> jmps) s"
+| "jumpNestingOkS jmps (c1;;c2) = (jumpNestingOkS jmps c1 \<and>
+ jumpNestingOkS jmps c2)"
+| "jumpNestingOkS jmps (If(e) c1 Else c2) = (jumpNestingOkS jmps c1 \<and>
+ jumpNestingOkS jmps c2)"
+| "jumpNestingOkS jmps (l\<bullet> While(e) c) = jumpNestingOkS ({Cont l} \<union> jmps) c"
--{* The label of the while loop only handles continue jumps. Breaks are only
handled by @{term Lab} *}
-"jumpNestingOkS jmps (Jmp j) = (j \<in> jmps)"
-"jumpNestingOkS jmps (Throw e) = True"
-"jumpNestingOkS jmps (Try c1 Catch(C vn) c2) = (jumpNestingOkS jmps c1 \<and>
- jumpNestingOkS jmps c2)"
-"jumpNestingOkS jmps (c1 Finally c2) = (jumpNestingOkS jmps c1 \<and>
- jumpNestingOkS jmps c2)"
-"jumpNestingOkS jmps (Init C) = True"
+| "jumpNestingOkS jmps (Jmp j) = (j \<in> jmps)"
+| "jumpNestingOkS jmps (Throw e) = True"
+| "jumpNestingOkS jmps (Try c1 Catch(C vn) c2) = (jumpNestingOkS jmps c1 \<and>
+ jumpNestingOkS jmps c2)"
+| "jumpNestingOkS jmps (c1 Finally c2) = (jumpNestingOkS jmps c1 \<and>
+ jumpNestingOkS jmps c2)"
+| "jumpNestingOkS jmps (Init C) = True"
--{* wellformedness of the program must enshure that for all initializers
jumpNestingOkS {} holds *}
--{* Dummy analysis for intermediate smallstep term @{term FinA} *}
-"jumpNestingOkS jmps (FinA a c) = False"
+| "jumpNestingOkS jmps (FinA a c) = False"
definition jumpNestingOk :: "jump set \<Rightarrow> term \<Rightarrow> bool" where
-"jumpNestingOk jmps t \<equiv> (case t of
+"jumpNestingOk jmps t = (case t of
In1 se \<Rightarrow> (case se of
Inl e \<Rightarrow> True
| Inr s \<Rightarrow> jumpNestingOkS jmps s)
@@ -116,48 +116,46 @@
subsection {* Very restricted calculation fallback calculation *}
-consts the_LVar_name:: "var \<Rightarrow> lname"
-primrec
-"the_LVar_name (LVar n) = n"
+primrec the_LVar_name :: "var \<Rightarrow> lname"
+ where "the_LVar_name (LVar n) = n"
-consts assignsE :: "expr \<Rightarrow> lname set"
- assignsV :: "var \<Rightarrow> lname set"
- assignsEs:: "expr list \<Rightarrow> lname set"
-text {* *}
-primrec
-"assignsE (NewC c) = {}"
-"assignsE (NewA t e) = assignsE e"
-"assignsE (Cast t e) = assignsE e"
-"assignsE (e InstOf r) = assignsE e"
-"assignsE (Lit val) = {}"
-"assignsE (UnOp unop e) = assignsE e"
-"assignsE (BinOp binop e1 e2) = (if binop=CondAnd \<or> binop=CondOr
- then (assignsE e1)
- else (assignsE e1) \<union> (assignsE e2))"
-"assignsE (Super) = {}"
-"assignsE (Acc v) = assignsV v"
-"assignsE (v:=e) = (assignsV v) \<union> (assignsE e) \<union>
- (if \<exists> n. v=(LVar n) then {the_LVar_name v}
- else {})"
-"assignsE (b? e1 : e2) = (assignsE b) \<union> ((assignsE e1) \<inter> (assignsE e2))"
-"assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args))
- = (assignsE objRef) \<union> (assignsEs args)"
+primrec assignsE :: "expr \<Rightarrow> lname set"
+ and assignsV :: "var \<Rightarrow> lname set"
+ and assignsEs:: "expr list \<Rightarrow> lname set"
+where
+ "assignsE (NewC c) = {}"
+| "assignsE (NewA t e) = assignsE e"
+| "assignsE (Cast t e) = assignsE e"
+| "assignsE (e InstOf r) = assignsE e"
+| "assignsE (Lit val) = {}"
+| "assignsE (UnOp unop e) = assignsE e"
+| "assignsE (BinOp binop e1 e2) = (if binop=CondAnd \<or> binop=CondOr
+ then (assignsE e1)
+ else (assignsE e1) \<union> (assignsE e2))"
+| "assignsE (Super) = {}"
+| "assignsE (Acc v) = assignsV v"
+| "assignsE (v:=e) = (assignsV v) \<union> (assignsE e) \<union>
+ (if \<exists> n. v=(LVar n) then {the_LVar_name v}
+ else {})"
+| "assignsE (b? e1 : e2) = (assignsE b) \<union> ((assignsE e1) \<inter> (assignsE e2))"
+| "assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args))
+ = (assignsE objRef) \<union> (assignsEs args)"
-- {* Only dummy analysis for intermediate expressions
@{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *}
-"assignsE (Methd C sig) = {}"
-"assignsE (Body C s) = {}"
-"assignsE (InsInitE s e) = {}"
-"assignsE (Callee l e) = {}"
+| "assignsE (Methd C sig) = {}"
+| "assignsE (Body C s) = {}"
+| "assignsE (InsInitE s e) = {}"
+| "assignsE (Callee l e) = {}"
-"assignsV (LVar n) = {}"
-"assignsV ({accC,statDeclC,stat}objRef..fn) = assignsE objRef"
-"assignsV (e1.[e2]) = assignsE e1 \<union> assignsE e2"
+| "assignsV (LVar n) = {}"
+| "assignsV ({accC,statDeclC,stat}objRef..fn) = assignsE objRef"
+| "assignsV (e1.[e2]) = assignsE e1 \<union> assignsE e2"
-"assignsEs [] = {}"
-"assignsEs (e#es) = assignsE e \<union> assignsEs es"
+| "assignsEs [] = {}"
+| "assignsEs (e#es) = assignsE e \<union> assignsEs es"
definition assigns :: "term \<Rightarrow> lname set" where
-"assigns t \<equiv> (case t of
+"assigns t = (case t of
In1 se \<Rightarrow> (case se of
Inl e \<Rightarrow> assignsE e
| Inr s \<Rightarrow> {})
@@ -190,42 +188,42 @@
subsection "Analysis of constant expressions"
-consts constVal :: "expr \<Rightarrow> val option"
-primrec
-"constVal (NewC c) = None"
-"constVal (NewA t e) = None"
-"constVal (Cast t e) = None"
-"constVal (Inst e r) = None"
-"constVal (Lit val) = Some val"
-"constVal (UnOp unop e) = (case (constVal e) of
- None \<Rightarrow> None
- | Some v \<Rightarrow> Some (eval_unop unop v))"
-"constVal (BinOp binop e1 e2) = (case (constVal e1) of
- None \<Rightarrow> None
- | Some v1 \<Rightarrow> (case (constVal e2) of
- None \<Rightarrow> None
- | Some v2 \<Rightarrow> Some (eval_binop
- binop v1 v2)))"
-"constVal (Super) = None"
-"constVal (Acc v) = None"
-"constVal (Ass v e) = None"
-"constVal (Cond b e1 e2) = (case (constVal b) of
+primrec constVal :: "expr \<Rightarrow> val option"
+where
+ "constVal (NewC c) = None"
+| "constVal (NewA t e) = None"
+| "constVal (Cast t e) = None"
+| "constVal (Inst e r) = None"
+| "constVal (Lit val) = Some val"
+| "constVal (UnOp unop e) = (case (constVal e) of
None \<Rightarrow> None
- | Some bv\<Rightarrow> (case the_Bool bv of
- True \<Rightarrow> (case (constVal e2) of
- None \<Rightarrow> None
- | Some v \<Rightarrow> constVal e1)
- | False\<Rightarrow> (case (constVal e1) of
- None \<Rightarrow> None
- | Some v \<Rightarrow> constVal e2)))"
+ | Some v \<Rightarrow> Some (eval_unop unop v))"
+| "constVal (BinOp binop e1 e2) = (case (constVal e1) of
+ None \<Rightarrow> None
+ | Some v1 \<Rightarrow> (case (constVal e2) of
+ None \<Rightarrow> None
+ | Some v2 \<Rightarrow> Some (eval_binop
+ binop v1 v2)))"
+| "constVal (Super) = None"
+| "constVal (Acc v) = None"
+| "constVal (Ass v e) = None"
+| "constVal (Cond b e1 e2) = (case (constVal b) of
+ None \<Rightarrow> None
+ | Some bv\<Rightarrow> (case the_Bool bv of
+ True \<Rightarrow> (case (constVal e2) of
+ None \<Rightarrow> None
+ | Some v \<Rightarrow> constVal e1)
+ | False\<Rightarrow> (case (constVal e1) of
+ None \<Rightarrow> None
+ | Some v \<Rightarrow> constVal e2)))"
--{* Note that @{text "constVal (Cond b e1 e2)"} is stricter as it could be.
It requires that all tree expressions are constant even if we can decide
which branch to choose, provided the constant value of @{term b} *}
-"constVal (Call accC statT mode objRef mn pTs args) = None"
-"constVal (Methd C sig) = None"
-"constVal (Body C s) = None"
-"constVal (InsInitE s e) = None"
-"constVal (Callee l e) = None"
+| "constVal (Call accC statT mode objRef mn pTs args) = None"
+| "constVal (Methd C sig) = None"
+| "constVal (Body C s) = None"
+| "constVal (InsInitE s e) = None"
+| "constVal (Callee l e) = None"
lemma constVal_Some_induct [consumes 1, case_names Lit UnOp BinOp CondL CondR]:
assumes const: "constVal e = Some v" and
@@ -282,55 +280,55 @@
to a specific boolean value. If the expression cannot evaluate to a
@{term Boolean} value UNIV is returned. If we expect true/false the opposite
constant false/true will also lead to UNIV. *}
-consts assigns_if:: "bool \<Rightarrow> expr \<Rightarrow> lname set"
-primrec
-"assigns_if b (NewC c) = UNIV" --{*can never evaluate to Boolean*}
-"assigns_if b (NewA t e) = UNIV" --{*can never evaluate to Boolean*}
-"assigns_if b (Cast t e) = assigns_if b e"
-"assigns_if b (Inst e r) = assignsE e" --{*Inst has type Boolean but
- e is a reference type*}
-"assigns_if b (Lit val) = (if val=Bool b then {} else UNIV)"
-"assigns_if b (UnOp unop e) = (case constVal (UnOp unop e) of
- None \<Rightarrow> (if unop = UNot
- then assigns_if (\<not>b) e
- else UNIV)
- | Some v \<Rightarrow> (if v=Bool b
- then {}
- else UNIV))"
-"assigns_if b (BinOp binop e1 e2)
- = (case constVal (BinOp binop e1 e2) of
- None \<Rightarrow> (if binop=CondAnd then
- (case b of
- True \<Rightarrow> assigns_if True e1 \<union> assigns_if True e2
- | False \<Rightarrow> assigns_if False e1 \<inter>
- (assigns_if True e1 \<union> assigns_if False e2))
- else
- (if binop=CondOr then
- (case b of
- True \<Rightarrow> assigns_if True e1 \<inter>
- (assigns_if False e1 \<union> assigns_if True e2)
- | False \<Rightarrow> assigns_if False e1 \<union> assigns_if False e2)
- else assignsE e1 \<union> assignsE e2))
- | Some v \<Rightarrow> (if v=Bool b then {} else UNIV))"
+primrec assigns_if :: "bool \<Rightarrow> expr \<Rightarrow> lname set"
+where
+ "assigns_if b (NewC c) = UNIV" --{*can never evaluate to Boolean*}
+| "assigns_if b (NewA t e) = UNIV" --{*can never evaluate to Boolean*}
+| "assigns_if b (Cast t e) = assigns_if b e"
+| "assigns_if b (Inst e r) = assignsE e" --{*Inst has type Boolean but
+ e is a reference type*}
+| "assigns_if b (Lit val) = (if val=Bool b then {} else UNIV)"
+| "assigns_if b (UnOp unop e) = (case constVal (UnOp unop e) of
+ None \<Rightarrow> (if unop = UNot
+ then assigns_if (\<not>b) e
+ else UNIV)
+ | Some v \<Rightarrow> (if v=Bool b
+ then {}
+ else UNIV))"
+| "assigns_if b (BinOp binop e1 e2)
+ = (case constVal (BinOp binop e1 e2) of
+ None \<Rightarrow> (if binop=CondAnd then
+ (case b of
+ True \<Rightarrow> assigns_if True e1 \<union> assigns_if True e2
+ | False \<Rightarrow> assigns_if False e1 \<inter>
+ (assigns_if True e1 \<union> assigns_if False e2))
+ else
+ (if binop=CondOr then
+ (case b of
+ True \<Rightarrow> assigns_if True e1 \<inter>
+ (assigns_if False e1 \<union> assigns_if True e2)
+ | False \<Rightarrow> assigns_if False e1 \<union> assigns_if False e2)
+ else assignsE e1 \<union> assignsE e2))
+ | Some v \<Rightarrow> (if v=Bool b then {} else UNIV))"
-"assigns_if b (Super) = UNIV" --{*can never evaluate to Boolean*}
-"assigns_if b (Acc v) = (assignsV v)"
-"assigns_if b (v := e) = (assignsE (Ass v e))"
-"assigns_if b (c? e1 : e2) = (assignsE c) \<union>
- (case (constVal c) of
- None \<Rightarrow> (assigns_if b e1) \<inter>
- (assigns_if b e2)
- | Some bv \<Rightarrow> (case the_Bool bv of
- True \<Rightarrow> assigns_if b e1
- | False \<Rightarrow> assigns_if b e2))"
-"assigns_if b ({accC,statT,mode}objRef\<cdot>mn({pTs}args))
- = assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) "
+| "assigns_if b (Super) = UNIV" --{*can never evaluate to Boolean*}
+| "assigns_if b (Acc v) = (assignsV v)"
+| "assigns_if b (v := e) = (assignsE (Ass v e))"
+| "assigns_if b (c? e1 : e2) = (assignsE c) \<union>
+ (case (constVal c) of
+ None \<Rightarrow> (assigns_if b e1) \<inter>
+ (assigns_if b e2)
+ | Some bv \<Rightarrow> (case the_Bool bv of
+ True \<Rightarrow> assigns_if b e1
+ | False \<Rightarrow> assigns_if b e2))"
+| "assigns_if b ({accC,statT,mode}objRef\<cdot>mn({pTs}args))
+ = assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) "
-- {* Only dummy analysis for intermediate expressions
@{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *}
-"assigns_if b (Methd C sig) = {}"
-"assigns_if b (Body C s) = {}"
-"assigns_if b (InsInitE s e) = {}"
-"assigns_if b (Callee l e) = {}"
+| "assigns_if b (Methd C sig) = {}"
+| "assigns_if b (Body C s) = {}"
+| "assigns_if b (InsInitE s e) = {}"
+| "assigns_if b (Callee l e) = {}"
lemma assigns_if_const_b_simp:
assumes boolConst: "constVal e = Some (Bool b)" (is "?Const b e")
@@ -429,14 +427,17 @@
subsection {* Lifting set operations to range of tables (map to a set) *}
-definition union_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<union> _" [67,67] 65) where
- "A \<Rightarrow>\<union> B \<equiv> \<lambda> k. A k \<union> B k"
+definition
+ union_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<union> _" [67,67] 65)
+ where "A \<Rightarrow>\<union> B = (\<lambda> k. A k \<union> B k)"
-definition intersect_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<inter> _" [72,72] 71) where
- "A \<Rightarrow>\<inter> B \<equiv> \<lambda> k. A k \<inter> B k"
+definition
+ intersect_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<inter> _" [72,72] 71)
+ where "A \<Rightarrow>\<inter> B = (\<lambda>k. A k \<inter> B k)"
-definition all_union_ts :: "('a,'b) tables \<Rightarrow> 'b set \<Rightarrow> ('a,'b) tables" (infixl "\<Rightarrow>\<union>\<^sub>\<forall>" 40) where
- "A \<Rightarrow>\<union>\<^sub>\<forall> B \<equiv> \<lambda> k. A k \<union> B"
+definition
+ all_union_ts :: "('a,'b) tables \<Rightarrow> 'b set \<Rightarrow> ('a,'b) tables" (infixl "\<Rightarrow>\<union>\<^sub>\<forall>" 40)
+ where "(A \<Rightarrow>\<union>\<^sub>\<forall> B) = (\<lambda> k. A k \<union> B)"
subsubsection {* Binary union of tables *}
@@ -507,16 +508,19 @@
brk :: "breakass" --{* Definetly assigned variables for
abrupt completion with a break *}
-definition rmlab :: "'a \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" where
-"rmlab k A \<equiv> \<lambda> x. if x=k then UNIV else A x"
+definition
+ rmlab :: "'a \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables"
+ where "rmlab k A = (\<lambda>x. if x=k then UNIV else A x)"
(*
-definition setbrk :: "breakass \<Rightarrow> assigned \<Rightarrow> breakass set" where
-"setbrk b A \<equiv> {b} \<union> {a| a. a\<in> brk A \<and> lab a \<noteq> lab b}"
+definition
+ setbrk :: "breakass \<Rightarrow> assigned \<Rightarrow> breakass set" where
+ "setbrk b A = {b} \<union> {a| a. a\<in> brk A \<and> lab a \<noteq> lab b}"
*)
-definition range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80) where
- "\<Rightarrow>\<Inter>A \<equiv> {x |x. \<forall> k. x \<in> A k}"
+definition
+ range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80)
+ where "\<Rightarrow>\<Inter>A = {x |x. \<forall> k. x \<in> A k}"
text {*
In @{text "E\<turnstile> B \<guillemotright>t\<guillemotright> A"},
--- a/src/HOL/Bali/Eval.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Eval.thy Mon Jul 26 18:25:19 2010 +0200
@@ -141,7 +141,7 @@
where "\<lfloor>es\<rfloor>\<^sub>l == In3 es"
definition undefined3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals" where
- "undefined3 \<equiv> sum3_case (In1 \<circ> sum_case (\<lambda>x. undefined) (\<lambda>x. Unit))
+ "undefined3 = sum3_case (In1 \<circ> sum_case (\<lambda>x. undefined) (\<lambda>x. Unit))
(\<lambda>x. In2 undefined) (\<lambda>x. In3 undefined)"
lemma [simp]: "undefined3 (In1l x) = In1 undefined"
@@ -159,8 +159,9 @@
section "exception throwing and catching"
-definition throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt" where
- "throw a' x \<equiv> abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
+definition
+ throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt" where
+ "throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
lemma throw_def2:
"throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
@@ -168,8 +169,9 @@
apply (simp (no_asm))
done
-definition fits :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60) where
- "G,s\<turnstile>a' fits T \<equiv> (\<exists>rt. T=RefT rt) \<longrightarrow> a'=Null \<or> G\<turnstile>obj_ty(lookup_obj s a')\<preceq>T"
+definition
+ fits :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60)
+ where "G,s\<turnstile>a' fits T = ((\<exists>rt. T=RefT rt) \<longrightarrow> a'=Null \<or> G\<turnstile>obj_ty(lookup_obj s a')\<preceq>T)"
lemma fits_Null [simp]: "G,s\<turnstile>Null fits T"
by (simp add: fits_def)
@@ -192,9 +194,10 @@
apply iprover
done
-definition catch :: "prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60) where
- "G,s\<turnstile>catch C\<equiv>\<exists>xc. abrupt s=Some (Xcpt xc) \<and>
- G,store s\<turnstile>Addr (the_Loc xc) fits Class C"
+definition
+ catch :: "prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60) where
+ "G,s\<turnstile>catch C = (\<exists>xc. abrupt s=Some (Xcpt xc) \<and>
+ G,store s\<turnstile>Addr (the_Loc xc) fits Class C)"
lemma catch_Norm [simp]: "\<not>G,Norm s\<turnstile>catch tn"
apply (unfold catch_def)
@@ -217,9 +220,9 @@
apply (simp (no_asm))
done
-definition new_xcpt_var :: "vname \<Rightarrow> state \<Rightarrow> state" where
- "new_xcpt_var vn \<equiv>
- \<lambda>(x,s). Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)"
+definition
+ new_xcpt_var :: "vname \<Rightarrow> state \<Rightarrow> state" where
+ "new_xcpt_var vn = (\<lambda>(x,s). Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s))"
lemma new_xcpt_var_def2 [simp]:
"new_xcpt_var vn (x,s) =
@@ -232,9 +235,10 @@
section "misc"
-definition assign :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state" where
- "assign f v \<equiv> \<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s)
- in (x',if x' = None then s' else s)"
+definition
+ assign :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state" where
+ "assign f v = (\<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s)
+ in (x',if x' = None then s' else s))"
(*
lemma assign_Norm_Norm [simp]:
@@ -293,26 +297,29 @@
done
*)
-definition init_comp_ty :: "ty \<Rightarrow> stmt" where
- "init_comp_ty T \<equiv> if (\<exists>C. T = Class C) then Init (the_Class T) else Skip"
+definition
+ init_comp_ty :: "ty \<Rightarrow> stmt"
+ where "init_comp_ty T = (if (\<exists>C. T = Class C) then Init (the_Class T) else Skip)"
lemma init_comp_ty_PrimT [simp]: "init_comp_ty (PrimT pt) = Skip"
apply (unfold init_comp_ty_def)
apply (simp (no_asm))
done
-definition invocation_class :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname" where
- "invocation_class m s a' statT
- \<equiv> (case m of
- Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC)
- then the_Class (RefT statT)
- else Object
- | SuperM \<Rightarrow> the_Class (RefT statT)
- | IntVir \<Rightarrow> obj_class (lookup_obj s a'))"
+definition
+ invocation_class :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname" where
+ "invocation_class m s a' statT =
+ (case m of
+ Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC)
+ then the_Class (RefT statT)
+ else Object
+ | SuperM \<Rightarrow> the_Class (RefT statT)
+ | IntVir \<Rightarrow> obj_class (lookup_obj s a'))"
-definition invocation_declclass::"prog \<Rightarrow> inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> qtname" where
-"invocation_declclass G m s a' statT sig
- \<equiv> declclass (the (dynlookup G statT
+definition
+ invocation_declclass :: "prog \<Rightarrow> inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> qtname" where
+ "invocation_declclass G m s a' statT sig =
+ declclass (the (dynlookup G statT
(invocation_class m s a' statT)
sig))"
@@ -330,10 +337,11 @@
else Object)"
by (simp add: invocation_class_def)
-definition init_lvars :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow>
- state \<Rightarrow> state" where
- "init_lvars G C sig mode a' pvs
- \<equiv> \<lambda> (x,s).
+definition
+ init_lvars :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow> state \<Rightarrow> state"
+where
+ "init_lvars G C sig mode a' pvs =
+ (\<lambda>(x,s).
let m = mthd (the (methd G C sig));
l = \<lambda> k.
(case k of
@@ -343,7 +351,7 @@
| Res \<Rightarrow> None)
| This
\<Rightarrow> (if mode=Static then None else Some a'))
- in set_lvars l (if mode = Static then x else np a' x,s)"
+ in set_lvars l (if mode = Static then x else np a' x,s))"
@@ -364,9 +372,11 @@
apply (simp (no_asm) add: Let_def)
done
-definition body :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> expr" where
- "body G C sig \<equiv> let m = the (methd G C sig)
- in Body (declclass m) (stmt (mbody (mthd m)))"
+definition
+ body :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> expr" where
+ "body G C sig =
+ (let m = the (methd G C sig)
+ in Body (declclass m) (stmt (mbody (mthd m))))"
lemma body_def2: --{* better suited for simplification *}
"body G C sig = Body (declclass (the (methd G C sig)))
@@ -377,28 +387,30 @@
section "variables"
-definition lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar" where
- "lvar vn s \<equiv> (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))"
+definition
+ lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar"
+ where "lvar vn s = (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))"
-definition fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
- "fvar C stat fn a' s
- \<equiv> let (oref,xf) = if stat then (Stat C,id)
- else (Heap (the_Addr a'),np a');
+definition
+ fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
+ "fvar C stat fn a' s =
+ (let (oref,xf) = if stat then (Stat C,id)
+ else (Heap (the_Addr a'),np a');
n = Inl (fn,C);
f = (\<lambda>v. supd (upd_gobj oref n v))
- in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)"
+ in ((the (values (the (globs (store s) oref)) n),f),abupd xf s))"
-definition avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
- "avar G i' a' s
- \<equiv> let oref = Heap (the_Addr a');
- i = the_Intg i';
- n = Inr i;
- (T,k,cs) = the_Arr (globs (store s) oref);
- f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T)
+definition
+ avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
+ "avar G i' a' s =
+ (let oref = Heap (the_Addr a');
+ i = the_Intg i';
+ n = Inr i;
+ (T,k,cs) = the_Arr (globs (store s) oref);
+ f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T)
ArrStore x
,upd_gobj oref n v s))
- in ((the (cs n),f)
- ,abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s)"
+ in ((the (cs n),f),abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s))"
lemma fvar_def2: --{* better suited for simplification *}
"fvar C stat fn a' s =
@@ -431,27 +443,29 @@
apply (simp (no_asm) add: Let_def split_beta)
done
-definition check_field_access :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> vname \<Rightarrow> bool \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
-"check_field_access G accC statDeclC fn stat a' s
- \<equiv> let oref = if stat then Stat statDeclC
- else Heap (the_Addr a');
- dynC = case oref of
+definition
+ check_field_access :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> vname \<Rightarrow> bool \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
+ "check_field_access G accC statDeclC fn stat a' s =
+ (let oref = if stat then Stat statDeclC
+ else Heap (the_Addr a');
+ dynC = case oref of
Heap a \<Rightarrow> obj_class (the (globs (store s) oref))
| Stat C \<Rightarrow> C;
- f = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC)))
- in abupd
+ f = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC)))
+ in abupd
(error_if (\<not> G\<turnstile>Field fn (statDeclC,f) in dynC dyn_accessible_from accC)
AccessViolation)
- s"
+ s)"
-definition check_method_access :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> inv_mode \<Rightarrow> sig \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
-"check_method_access G accC statT mode sig a' s
- \<equiv> let invC = invocation_class mode (store s) a' statT;
+definition
+ check_method_access :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> inv_mode \<Rightarrow> sig \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
+ "check_method_access G accC statT mode sig a' s =
+ (let invC = invocation_class mode (store s) a' statT;
dynM = the (dynlookup G statT invC sig)
- in abupd
+ in abupd
(error_if (\<not> G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC)
AccessViolation)
- s"
+ s)"
section "evaluation judgments"
--- a/src/HOL/Bali/Example.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Example.thy Mon Jul 26 18:25:19 2010 +0200
@@ -70,22 +70,21 @@
datatype vnam' = arr' | vee' | z' | e'
datatype label' = lab1'
-consts
-
- tnam' :: "tnam' \<Rightarrow> tnam"
- vnam' :: "vnam' \<Rightarrow> vname"
+axiomatization
+ tnam' :: "tnam' \<Rightarrow> tnam" and
+ vnam' :: "vnam' \<Rightarrow> vname" and
label':: "label' \<Rightarrow> label"
-axioms (** tnam', vnam' and label are intended to be isomorphic
+where
+ (** tnam', vnam' and label are intended to be isomorphic
to tnam, vname and label **)
- inj_tnam' [simp]: "(tnam' x = tnam' y) = (x = y)"
- inj_vnam' [simp]: "(vnam' x = vnam' y) = (x = y)"
- inj_label' [simp]: "(label' x = label' y) = (x = y)"
-
-
- surj_tnam': "\<exists>m. n = tnam' m"
- surj_vnam': "\<exists>m. n = vnam' m"
- surj_label':" \<exists>m. n = label' m"
+ inj_tnam' [simp]: "\<And>x y. (tnam' x = tnam' y) = (x = y)" and
+ inj_vnam' [simp]: "\<And>x y. (vnam' x = vnam' y) = (x = y)" and
+ inj_label' [simp]: "\<And>x y. (label' x = label' y) = (x = y)" and
+
+ surj_tnam': "\<And>n. \<exists>m. n = tnam' m" and
+ surj_vnam': "\<And>n. \<exists>m. n = vnam' m" and
+ surj_label':" \<And>n. \<exists>m. n = label' m"
abbreviation
HasFoo :: qtname where
@@ -149,22 +148,24 @@
Object_mdecls_def: "Object_mdecls \<equiv> []"
SXcpt_mdecls_def: "SXcpt_mdecls \<equiv> []"
-consts
-
+axiomatization
foo :: mname
-definition foo_sig :: sig
- where "foo_sig \<equiv> \<lparr>name=foo,parTs=[Class Base]\<rparr>"
+definition
+ foo_sig :: sig
+ where "foo_sig = \<lparr>name=foo,parTs=[Class Base]\<rparr>"
-definition foo_mhead :: mhead
- where "foo_mhead \<equiv> \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>"
+definition
+ foo_mhead :: mhead
+ where "foo_mhead = \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>"
-definition Base_foo :: mdecl
- where "Base_foo \<equiv> (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base,
+definition
+ Base_foo :: mdecl
+ where "Base_foo = (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base,
mbody=\<lparr>lcls=[],stmt=Return (!!z)\<rparr>\<rparr>)"
definition Ext_foo :: mdecl
- where "Ext_foo \<equiv> (foo_sig,
+ where "Ext_foo = (foo_sig,
\<lparr>access=Public,static=False,pars=[z],resT=Class Ext,
mbody=\<lparr>lcls=[]
,stmt=Expr({Ext,Ext,False}Cast (Class Ext) (!!z)..vee :=
@@ -172,11 +173,13 @@
Return (Lit Null)\<rparr>
\<rparr>)"
-definition arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var" where
-"arr_viewed_from accC C \<equiv> {accC,Base,True}StatRef (ClassT C)..arr"
+definition
+ arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var"
+ where "arr_viewed_from accC C = {accC,Base,True}StatRef (ClassT C)..arr"
-definition BaseCl :: "class" where
-"BaseCl \<equiv> \<lparr>access=Public,
+definition
+ BaseCl :: "class" where
+ "BaseCl = \<lparr>access=Public,
cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
(vee, \<lparr>access=Public,static=False,type=Iface HasFoo \<rparr>)],
methods=[Base_foo],
@@ -185,16 +188,18 @@
super=Object,
superIfs=[HasFoo]\<rparr>"
-definition ExtCl :: "class" where
-"ExtCl \<equiv> \<lparr>access=Public,
+definition
+ ExtCl :: "class" where
+ "ExtCl = \<lparr>access=Public,
cfields=[(vee, \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)],
methods=[Ext_foo],
init=Skip,
super=Base,
superIfs=[]\<rparr>"
-definition MainCl :: "class" where
-"MainCl \<equiv> \<lparr>access=Public,
+definition
+ MainCl :: "class" where
+ "MainCl = \<lparr>access=Public,
cfields=[],
methods=[],
init=Skip,
@@ -202,14 +207,17 @@
superIfs=[]\<rparr>"
(* The "main" method is modeled seperately (see tprg) *)
-definition HasFooInt :: iface
- where "HasFooInt \<equiv> \<lparr>access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\<rparr>"
+definition
+ HasFooInt :: iface
+ where "HasFooInt = \<lparr>access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\<rparr>"
-definition Ifaces ::"idecl list"
- where "Ifaces \<equiv> [(HasFoo,HasFooInt)]"
+definition
+ Ifaces ::"idecl list"
+ where "Ifaces = [(HasFoo,HasFooInt)]"
-definition "Classes" ::"cdecl list"
- where "Classes \<equiv> [(Base,BaseCl),(Ext,ExtCl),(Main,MainCl)]@standard_classes"
+definition
+ "Classes" ::"cdecl list"
+ where "Classes = [(Base,BaseCl),(Ext,ExtCl),(Main,MainCl)]@standard_classes"
lemmas table_classes_defs =
Classes_def standard_classes_def ObjectC_def SXcptC_def
@@ -264,12 +272,13 @@
tprg :: prog where
"tprg == \<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
-definition test :: "(ty)list \<Rightarrow> stmt" where
- "test pTs \<equiv> e:==NewC Ext;;
+definition
+ test :: "(ty)list \<Rightarrow> stmt" where
+ "test pTs = (e:==NewC Ext;;
\<spacespace> Try Expr({Main,ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))
\<spacespace> Catch((SXcpt NullPointer) z)
(lab1\<bullet> While(Acc
- (Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip)"
+ (Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip))"
section "well-structuredness"
@@ -1185,9 +1194,9 @@
rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
-consts
- a :: loc
- b :: loc
+axiomatization
+ a :: loc and
+ b :: loc and
c :: loc
abbreviation "one == Suc 0"
--- a/src/HOL/Bali/Name.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Name.thy Mon Jul 26 18:25:19 2010 +0200
@@ -68,14 +68,14 @@
begin
definition
- tname_tname_def: "tname (t::tname) \<equiv> t"
+ tname_tname_def: "tname (t::tname) = t"
instance ..
end
definition
- qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
+ qtname_qtname_def: "qtname (q::'a qtname_ext_type) = q"
translations
(type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
@@ -84,16 +84,17 @@
axiomatization java_lang::pname --{* package java.lang *}
-consts
+definition
Object :: qtname
- SXcpt :: "xname \<Rightarrow> qtname"
-defs
- Object_def: "Object \<equiv> \<lparr>pid = java_lang, tid = Object'\<rparr>"
- SXcpt_def: "SXcpt \<equiv> \<lambda>x. \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>"
+ where "Object = \<lparr>pid = java_lang, tid = Object'\<rparr>"
+
+definition SXcpt :: "xname \<Rightarrow> qtname"
+ where "SXcpt = (\<lambda>x. \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>)"
lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
by (simp add: Object_def SXcpt_def)
lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
by (simp add: SXcpt_def)
+
end
--- a/src/HOL/Bali/State.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/State.thy Mon Jul 26 18:25:19 2010 +0200
@@ -38,8 +38,9 @@
(type) "obj" <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>"
(type) "obj" <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>"
-definition the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table" where
- "the_Arr obj \<equiv> SOME (T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>"
+definition
+ the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table"
+ where "the_Arr obj = (SOME (T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>)"
lemma the_Arr_Arr [simp]: "the_Arr (Some \<lparr>tag=Arr T k,values=cs\<rparr>) = (T,k,cs)"
apply (auto simp: the_Arr_def)
@@ -50,18 +51,20 @@
apply (auto simp add: the_Arr_def)
done
-definition upd_obj :: "vn \<Rightarrow> val \<Rightarrow> obj \<Rightarrow> obj" where
- "upd_obj n v \<equiv> \<lambda> obj . obj \<lparr>values:=(values obj)(n\<mapsto>v)\<rparr>"
+definition
+ upd_obj :: "vn \<Rightarrow> val \<Rightarrow> obj \<Rightarrow> obj"
+ where "upd_obj n v = (\<lambda>obj. obj \<lparr>values:=(values obj)(n\<mapsto>v)\<rparr>)"
lemma upd_obj_def2 [simp]:
"upd_obj n v obj = obj \<lparr>values:=(values obj)(n\<mapsto>v)\<rparr>"
apply (auto simp: upd_obj_def)
done
-definition obj_ty :: "obj \<Rightarrow> ty" where
- "obj_ty obj \<equiv> case tag obj of
- CInst C \<Rightarrow> Class C
- | Arr T k \<Rightarrow> T.[]"
+definition
+ obj_ty :: "obj \<Rightarrow> ty" where
+ "obj_ty obj = (case tag obj of
+ CInst C \<Rightarrow> Class C
+ | Arr T k \<Rightarrow> T.[])"
lemma obj_ty_eq [intro!]: "obj_ty \<lparr>tag=oi,values=x\<rparr> = obj_ty \<lparr>tag=oi,values=y\<rparr>"
by (simp add: obj_ty_def)
@@ -97,10 +100,11 @@
apply (auto split add: obj_tag.split_asm)
done
-definition obj_class :: "obj \<Rightarrow> qtname" where
- "obj_class obj \<equiv> case tag obj of
- CInst C \<Rightarrow> C
- | Arr T k \<Rightarrow> Object"
+definition
+ obj_class :: "obj \<Rightarrow> qtname" where
+ "obj_class obj = (case tag obj of
+ CInst C \<Rightarrow> C
+ | Arr T k \<Rightarrow> Object)"
lemma obj_class_CInst [simp]: "obj_class \<lparr>tag=CInst C,values=vs\<rparr> = C"
@@ -136,9 +140,10 @@
"Stat" => "CONST Inr"
(type) "oref" <= (type) "loc + qtname"
-definition fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool) \<Rightarrow> (fspec, ty) table" where
- "fields_table G C P
- \<equiv> Option.map type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
+definition
+ fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool) \<Rightarrow> (fspec, ty) table" where
+ "fields_table G C P =
+ Option.map type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
lemma fields_table_SomeI:
"\<lbrakk>table_of (DeclConcepts.fields G C) n = Some f; P n f\<rbrakk>
@@ -173,20 +178,23 @@
apply simp
done
-definition in_bounds :: "int \<Rightarrow> int \<Rightarrow> bool" ("(_/ in'_bounds _)" [50, 51] 50) where
- "i in_bounds k \<equiv> 0 \<le> i \<and> i < k"
+definition
+ in_bounds :: "int \<Rightarrow> int \<Rightarrow> bool" ("(_/ in'_bounds _)" [50, 51] 50)
+ where "i in_bounds k = (0 \<le> i \<and> i < k)"
-definition arr_comps :: "'a \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a option" where
- "arr_comps T k \<equiv> \<lambda>i. if i in_bounds k then Some T else None"
+definition
+ arr_comps :: "'a \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a option"
+ where "arr_comps T k = (\<lambda>i. if i in_bounds k then Some T else None)"
-definition var_tys :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> (vn, ty) table" where
-"var_tys G oi r
- \<equiv> case r of
+definition
+ var_tys :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> (vn, ty) table" where
+ "var_tys G oi r =
+ (case r of
Heap a \<Rightarrow> (case oi of
CInst C \<Rightarrow> fields_table G C (\<lambda>n f. \<not>static f) (+) empty
| Arr T k \<Rightarrow> empty (+) arr_comps T k)
| Stat C \<Rightarrow> fields_table G C (\<lambda>fn f. declclassf fn = C \<and> static f)
- (+) empty"
+ (+) empty)"
lemma var_tys_Some_eq:
"var_tys G oi r n = Some T
@@ -222,14 +230,16 @@
subsection "access"
-definition globs :: "st \<Rightarrow> globs" where
- "globs \<equiv> st_case (\<lambda>g l. g)"
+definition
+ globs :: "st \<Rightarrow> globs"
+ where "globs = st_case (\<lambda>g l. g)"
-definition locals :: "st \<Rightarrow> locals" where
- "locals \<equiv> st_case (\<lambda>g l. l)"
+definition
+ locals :: "st \<Rightarrow> locals"
+ where "locals = st_case (\<lambda>g l. l)"
-definition heap :: "st \<Rightarrow> heap" where
- "heap s \<equiv> globs s \<circ> Heap"
+definition heap :: "st \<Rightarrow> heap" where
+ "heap s = globs s \<circ> Heap"
lemma globs_def2 [simp]: " globs (st g l) = g"
@@ -250,8 +260,9 @@
subsection "memory allocation"
-definition new_Addr :: "heap \<Rightarrow> loc option" where
- "new_Addr h \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (SOME a. h a = None)"
+definition
+ new_Addr :: "heap \<Rightarrow> loc option" where
+ "new_Addr h = (if (\<forall>a. h a \<noteq> None) then None else Some (SOME a. h a = None))"
lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None"
apply (auto simp add: new_Addr_def)
@@ -290,20 +301,25 @@
subsection "update"
-definition gupd :: "oref \<Rightarrow> obj \<Rightarrow> st \<Rightarrow> st" ("gupd'(_\<mapsto>_')"[10,10]1000) where
- "gupd r obj \<equiv> st_case (\<lambda>g l. st (g(r\<mapsto>obj)) l)"
+definition
+ gupd :: "oref \<Rightarrow> obj \<Rightarrow> st \<Rightarrow> st" ("gupd'(_\<mapsto>_')" [10, 10] 1000)
+ where "gupd r obj = st_case (\<lambda>g l. st (g(r\<mapsto>obj)) l)"
-definition lupd :: "lname \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" ("lupd'(_\<mapsto>_')"[10,10]1000) where
- "lupd vn v \<equiv> st_case (\<lambda>g l. st g (l(vn\<mapsto>v)))"
+definition
+ lupd :: "lname \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" ("lupd'(_\<mapsto>_')" [10, 10] 1000)
+ where "lupd vn v = st_case (\<lambda>g l. st g (l(vn\<mapsto>v)))"
-definition upd_gobj :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" where
- "upd_gobj r n v \<equiv> st_case (\<lambda>g l. st (chg_map (upd_obj n v) r g) l)"
+definition
+ upd_gobj :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st"
+ where "upd_gobj r n v = st_case (\<lambda>g l. st (chg_map (upd_obj n v) r g) l)"
-definition set_locals :: "locals \<Rightarrow> st \<Rightarrow> st" where
- "set_locals l \<equiv> st_case (\<lambda>g l'. st g l)"
+definition
+ set_locals :: "locals \<Rightarrow> st \<Rightarrow> st"
+ where "set_locals l = st_case (\<lambda>g l'. st g l)"
-definition init_obj :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st" where
- "init_obj G oi r \<equiv> gupd(r\<mapsto>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>)"
+definition
+ init_obj :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st"
+ where "init_obj G oi r = gupd(r\<mapsto>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>)"
abbreviation
init_class_obj :: "prog \<Rightarrow> qtname \<Rightarrow> st \<Rightarrow> st"
@@ -447,23 +463,22 @@
-consts
+primrec the_Xcpt :: "abrupt \<Rightarrow> xcpt"
+ where "the_Xcpt (Xcpt x) = x"
- the_Xcpt :: "abrupt \<Rightarrow> xcpt"
- the_Jump :: "abrupt => jump"
- the_Loc :: "xcpt \<Rightarrow> loc"
- the_Std :: "xcpt \<Rightarrow> xname"
+primrec the_Jump :: "abrupt => jump"
+ where "the_Jump (Jump j) = j"
-primrec "the_Xcpt (Xcpt x) = x"
-primrec "the_Jump (Jump j) = j"
-primrec "the_Loc (Loc a) = a"
-primrec "the_Std (Std x) = x"
+primrec the_Loc :: "xcpt \<Rightarrow> loc"
+ where "the_Loc (Loc a) = a"
-
+primrec the_Std :: "xcpt \<Rightarrow> xname"
+ where "the_Std (Std x) = x"
-definition abrupt_if :: "bool \<Rightarrow> abopt \<Rightarrow> abopt \<Rightarrow> abopt" where
- "abrupt_if c x' x \<equiv> if c \<and> (x = None) then x' else x"
+definition
+ abrupt_if :: "bool \<Rightarrow> abopt \<Rightarrow> abopt \<Rightarrow> abopt"
+ where "abrupt_if c x' x = (if c \<and> (x = None) then x' else x)"
lemma abrupt_if_True_None [simp]: "abrupt_if True x None = x"
by (simp add: abrupt_if_def)
@@ -542,8 +557,9 @@
apply auto
done
-definition absorb :: "jump \<Rightarrow> abopt \<Rightarrow> abopt" where
- "absorb j a \<equiv> if a=Some (Jump j) then None else a"
+definition
+ absorb :: "jump \<Rightarrow> abopt \<Rightarrow> abopt"
+ where "absorb j a = (if a=Some (Jump j) then None else a)"
lemma absorb_SomeD [dest!]: "absorb j a = Some x \<Longrightarrow> a = Some x"
by (auto simp add: absorb_def)
@@ -593,16 +609,18 @@
apply clarsimp
done
-definition normal :: "state \<Rightarrow> bool" where
- "normal \<equiv> \<lambda>s. abrupt s = None"
+definition
+ normal :: "state \<Rightarrow> bool"
+ where "normal = (\<lambda>s. abrupt s = None)"
lemma normal_def2 [simp]: "normal s = (abrupt s = None)"
apply (unfold normal_def)
apply (simp (no_asm))
done
-definition heap_free :: "nat \<Rightarrow> state \<Rightarrow> bool" where
- "heap_free n \<equiv> \<lambda>s. atleast_free (heap (store s)) n"
+definition
+ heap_free :: "nat \<Rightarrow> state \<Rightarrow> bool"
+ where "heap_free n = (\<lambda>s. atleast_free (heap (store s)) n)"
lemma heap_free_def2 [simp]: "heap_free n s = atleast_free (heap (store s)) n"
apply (unfold heap_free_def)
@@ -611,11 +629,13 @@
subsection "update"
-definition abupd :: "(abopt \<Rightarrow> abopt) \<Rightarrow> state \<Rightarrow> state" where
- "abupd f \<equiv> prod_fun f id"
+definition
+ abupd :: "(abopt \<Rightarrow> abopt) \<Rightarrow> state \<Rightarrow> state"
+ where "abupd f = prod_fun f id"
-definition supd :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state" where
- "supd \<equiv> prod_fun id"
+definition
+ supd :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state"
+ where "supd = prod_fun id"
lemma abupd_def2 [simp]: "abupd f (x,s) = (f x,s)"
by (simp add: abupd_def)
@@ -669,11 +689,13 @@
section "initialisation test"
-definition inited :: "qtname \<Rightarrow> globs \<Rightarrow> bool" where
- "inited C g \<equiv> g (Stat C) \<noteq> None"
+definition
+ inited :: "qtname \<Rightarrow> globs \<Rightarrow> bool"
+ where "inited C g = (g (Stat C) \<noteq> None)"
-definition initd :: "qtname \<Rightarrow> state \<Rightarrow> bool" where
- "initd C \<equiv> inited C \<circ> globs \<circ> store"
+definition
+ initd :: "qtname \<Rightarrow> state \<Rightarrow> bool"
+ where "initd C = inited C \<circ> globs \<circ> store"
lemma not_inited_empty [simp]: "\<not>inited C empty"
apply (unfold inited_def)
@@ -706,8 +728,10 @@
done
section {* @{text error_free} *}
-definition error_free :: "state \<Rightarrow> bool" where
-"error_free s \<equiv> \<not> (\<exists> err. abrupt s = Some (Error err))"
+
+definition
+ error_free :: "state \<Rightarrow> bool"
+ where "error_free s = (\<not> (\<exists> err. abrupt s = Some (Error err)))"
lemma error_free_Norm [simp,intro]: "error_free (Norm s)"
by (simp add: error_free_def)
--- a/src/HOL/Bali/Table.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Table.thy Mon Jul 26 18:25:19 2010 +0200
@@ -54,15 +54,15 @@
--{* when merging tables old and new, only override an entry of table old when
the condition cond holds *}
-"cond_override cond old new \<equiv>
- \<lambda> k.
+"cond_override cond old new =
+ (\<lambda>k.
(case new k of
None \<Rightarrow> old k
| Some new_val \<Rightarrow> (case old k of
None \<Rightarrow> Some new_val
| Some old_val \<Rightarrow> (if cond new_val old_val
then Some new_val
- else Some old_val)))"
+ else Some old_val))))"
lemma cond_override_empty1[simp]: "cond_override c empty t = t"
by (simp add: cond_override_def expand_fun_eq)
@@ -95,10 +95,11 @@
section {* Filter on Tables *}
-definition filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
-"filter_tab c t \<equiv> \<lambda> k. (case t k of
+definition
+ filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
+ "filter_tab c t = (\<lambda>k. (case t k of
None \<Rightarrow> None
- | Some x \<Rightarrow> if c k x then Some x else None)"
+ | Some x \<Rightarrow> if c k x then Some x else None))"
lemma filter_tab_empty[simp]: "filter_tab c empty = empty"
by (simp add: filter_tab_def empty_def)
@@ -279,27 +280,31 @@
done
-consts
- Un_tables :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
- overrides_t :: "('a, 'b) tables \<Rightarrow> ('a, 'b) tables \<Rightarrow>
- ('a, 'b) tables" (infixl "\<oplus>\<oplus>" 100)
- hidings_entails:: "('a, 'b) tables \<Rightarrow> ('a, 'c) tables \<Rightarrow>
- ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" ("_ hidings _ entails _" 20)
+definition
+ Un_tables :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
+ where "Un_tables ts\<spacespace>\<spacespace>= (\<lambda>k. \<Union>t\<in>ts. t k)"
+
+definition
+ overrides_t :: "('a, 'b) tables \<Rightarrow> ('a, 'b) tables \<Rightarrow> ('a, 'b) tables" (infixl "\<oplus>\<oplus>" 100)
+ where "s \<oplus>\<oplus> t = (\<lambda>k. if t k = {} then s k else t k)"
+
+definition
+ hidings_entails :: "('a, 'b) tables \<Rightarrow> ('a, 'c) tables \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"
+ ("_ hidings _ entails _" 20)
+ where "(t hidings s entails R) = (\<forall>k. \<forall>x\<in>t k. \<forall>y\<in>s k. R x y)"
+
+definition
--{* variant for unique table: *}
- hiding_entails :: "('a, 'b) table \<Rightarrow> ('a, 'c) table \<Rightarrow>
- ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" ("_ hiding _ entails _" 20)
+ hiding_entails :: "('a, 'b) table \<Rightarrow> ('a, 'c) table \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"
+ ("_ hiding _ entails _" 20)
+ where "(t hiding s entails R) = (\<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: R x y)"
+
+definition
--{* variant for a unique table and conditional overriding: *}
cond_hiding_entails :: "('a, 'b) table \<Rightarrow> ('a, 'c) table
\<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"
("_ hiding _ under _ entails _" 20)
-
-defs
- Un_tables_def: "Un_tables ts\<spacespace>\<spacespace>\<equiv> \<lambda>k. \<Union>t\<in>ts. t k"
- overrides_t_def: "s \<oplus>\<oplus> t \<equiv> \<lambda>k. if t k = {} then s k else t k"
- hidings_entails_def: "t hidings s entails R \<equiv> \<forall>k. \<forall>x\<in>t k. \<forall>y\<in>s k. R x y"
- hiding_entails_def: "t hiding s entails R \<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: R x y"
- cond_hiding_entails_def: "t hiding s under C entails R
- \<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: C x y \<longrightarrow> R x y"
+ where "(t hiding s under C entails R) = (\<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: C x y \<longrightarrow> R x y)"
section "Untables"
@@ -383,12 +388,10 @@
(*###TO Map?*)
-consts
- atleast_free :: "('a ~=> 'b) => nat => bool"
-primrec
- "atleast_free m 0 = True"
- atleast_free_Suc:
- "atleast_free m (Suc n) = (? a. m a = None & (!b. atleast_free (m(a|->b)) n))"
+primrec atleast_free :: "('a ~=> 'b) => nat => bool"
+where
+ "atleast_free m 0 = True"
+| atleast_free_Suc: "atleast_free m (Suc n) = (\<exists>a. m a = None & (!b. atleast_free (m(a|->b)) n))"
lemma atleast_free_weaken [rule_format (no_asm)]:
"!m. atleast_free m (Suc n) \<longrightarrow> atleast_free m n"
--- a/src/HOL/Bali/Term.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Term.thy Mon Jul 26 18:25:19 2010 +0200
@@ -258,8 +258,9 @@
StatRef :: "ref_ty \<Rightarrow> expr"
where "StatRef rt == Cast (RefT rt) (Lit Null)"
-definition is_stmt :: "term \<Rightarrow> bool" where
- "is_stmt t \<equiv> \<exists>c. t=In1r c"
+definition
+ is_stmt :: "term \<Rightarrow> bool"
+ where "is_stmt t = (\<exists>c. t=In1r c)"
ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def}) *}
@@ -307,7 +308,7 @@
begin
definition
- stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
+ stmt_inj_term_def: "\<langle>c::stmt\<rangle> = In1r c"
instance ..
@@ -323,7 +324,7 @@
begin
definition
- expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
+ expr_inj_term_def: "\<langle>e::expr\<rangle> = In1l e"
instance ..
@@ -339,7 +340,7 @@
begin
definition
- var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
+ var_inj_term_def: "\<langle>v::var\<rangle> = In2 v"
instance ..
@@ -368,7 +369,7 @@
begin
definition
- "\<langle>es::'a list\<rangle> \<equiv> In3 (map expr_of es)"
+ "\<langle>es::'a list\<rangle> = In3 (map expr_of es)"
instance ..
@@ -425,46 +426,47 @@
done
section {* Evaluation of unary operations *}
-consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
-primrec
-"eval_unop UPlus v = Intg (the_Intg v)"
-"eval_unop UMinus v = Intg (- (the_Intg v))"
-"eval_unop UBitNot v = Intg 42" -- "FIXME: Not yet implemented"
-"eval_unop UNot v = Bool (\<not> the_Bool v)"
+primrec eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
+where
+ "eval_unop UPlus v = Intg (the_Intg v)"
+| "eval_unop UMinus v = Intg (- (the_Intg v))"
+| "eval_unop UBitNot v = Intg 42" -- "FIXME: Not yet implemented"
+| "eval_unop UNot v = Bool (\<not> the_Bool v)"
section {* Evaluation of binary operations *}
-consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
-primrec
-"eval_binop Mul v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))"
-"eval_binop Div v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
-"eval_binop Mod v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
-"eval_binop Plus v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
-"eval_binop Minus v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
+primrec eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
+where
+ "eval_binop Mul v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))"
+| "eval_binop Div v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
+| "eval_binop Mod v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
+| "eval_binop Plus v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
+| "eval_binop Minus v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
-- "Be aware of the explicit coercion of the shift distance to nat"
-"eval_binop LShift v1 v2 = Intg ((the_Intg v1) * (2^(nat (the_Intg v2))))"
-"eval_binop RShift v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
-"eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
+| "eval_binop LShift v1 v2 = Intg ((the_Intg v1) * (2^(nat (the_Intg v2))))"
+| "eval_binop RShift v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
+| "eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
-"eval_binop Less v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))"
-"eval_binop Le v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
-"eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
-"eval_binop Ge v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
+| "eval_binop Less v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))"
+| "eval_binop Le v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
+| "eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
+| "eval_binop Ge v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
-"eval_binop Eq v1 v2 = Bool (v1=v2)"
-"eval_binop Neq v1 v2 = Bool (v1\<noteq>v2)"
-"eval_binop BitAnd v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
-"eval_binop And v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
-"eval_binop BitXor v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
-"eval_binop Xor v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
-"eval_binop BitOr v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
-"eval_binop Or v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
-"eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
-"eval_binop CondOr v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
+| "eval_binop Eq v1 v2 = Bool (v1=v2)"
+| "eval_binop Neq v1 v2 = Bool (v1\<noteq>v2)"
+| "eval_binop BitAnd v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
+| "eval_binop And v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
+| "eval_binop BitXor v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
+| "eval_binop Xor v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
+| "eval_binop BitOr v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
+| "eval_binop Or v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
+| "eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
+| "eval_binop CondOr v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
-definition need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool" where
-"need_second_arg binop v1 \<equiv> \<not> ((binop=CondAnd \<and> \<not> the_Bool v1) \<or>
- (binop=CondOr \<and> the_Bool v1))"
+definition
+ need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool" where
+ "need_second_arg binop v1 = (\<not> ((binop=CondAnd \<and> \<not> the_Bool v1) \<or>
+ (binop=CondOr \<and> the_Bool v1)))"
text {* @{term CondAnd} and @{term CondOr} only evalulate the second argument
if the value isn't already determined by the first argument*}
--- a/src/HOL/Bali/Trans.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Trans.thy Mon Jul 26 18:25:19 2010 +0200
@@ -9,12 +9,13 @@
theory Trans imports Evaln begin
-definition groundVar :: "var \<Rightarrow> bool" where
-"groundVar v \<longleftrightarrow> (case v of
- LVar ln \<Rightarrow> True
- | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
- | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
- | InsInitV c v \<Rightarrow> False)"
+definition
+ groundVar :: "var \<Rightarrow> bool" where
+ "groundVar v \<longleftrightarrow> (case v of
+ LVar ln \<Rightarrow> True
+ | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
+ | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i
+ | InsInitV c v \<Rightarrow> False)"
lemma groundVar_cases [consumes 1, case_names LVar FVar AVar]:
assumes ground: "groundVar v" and
@@ -34,14 +35,15 @@
done
qed
-definition groundExprs :: "expr list \<Rightarrow> bool" where
- "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
+definition
+ groundExprs :: "expr list \<Rightarrow> bool"
+ where "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)"
-primrec the_val:: "expr \<Rightarrow> val" where
- "the_val (Lit v) = v"
+primrec the_val:: "expr \<Rightarrow> val"
+ where "the_val (Lit v) = v"
primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where
- "the_var G s (LVar ln) =(lvar ln (store s),s)"
+ "the_var G s (LVar ln) = (lvar ln (store s),s)"
| the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s"
| the_var_AVar_def: "the_var G s(a.[i]) =avar G (the_val i) (the_val a) s"
--- a/src/HOL/Bali/Type.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Type.thy Mon Jul 26 18:25:19 2010 +0200
@@ -36,8 +36,9 @@
abbreviation Array :: "ty \<Rightarrow> ty" ("_.[]" [90] 90)
where "T.[] == RefT (ArrayT T)"
-definition the_Class :: "ty \<Rightarrow> qtname" where
- "the_Class T \<equiv> SOME C. T = Class C" (** primrec not possible here **)
+definition
+ the_Class :: "ty \<Rightarrow> qtname"
+ where "the_Class T = (SOME C. T = Class C)" (** primrec not possible here **)
lemma the_Class_eq [simp]: "the_Class (Class C)= C"
by (auto simp add: the_Class_def)
--- a/src/HOL/Bali/TypeRel.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/TypeRel.thy Mon Jul 26 18:25:19 2010 +0200
@@ -25,14 +25,17 @@
\end{itemize}
*}
-consts
-
(*subint1, in Decl.thy*) (* direct subinterface *)
(*subint , by translation*) (* subinterface (+ identity) *)
(*subcls1, in Decl.thy*) (* direct subclass *)
(*subcls , by translation*) (* subclass *)
(*subclseq, by translation*) (* subclass + identity *)
- implmt1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
+
+definition
+ implmt1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct implementation *}
+ --{* direct implementation, cf. 8.1.3 *}
+ where "implmt1 G = {(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))}"
+
abbreviation
subint1_syntax :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
@@ -325,16 +328,11 @@
section "implementation relation"
-defs
- --{* direct implementation, cf. 8.1.3 *}
-implmt1_def:"implmt1 G\<equiv>{(C,I). C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))}"
-
lemma implmt1D: "G\<turnstile>C\<leadsto>1I \<Longrightarrow> C\<noteq>Object \<and> (\<exists>c\<in>class G C: I\<in>set (superIfs c))"
apply (unfold implmt1_def)
apply auto
done
-
inductive --{* implementation, cf. 8.1.4 *}
implmt :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>_" [71,71,71] 70)
for G :: prog
@@ -568,8 +566,9 @@
apply (fast dest: widen_Class_Class widen_Class_Iface)
done
-definition widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70) where
- "G\<turnstile>Ts[\<preceq>]Ts' \<equiv> list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'"
+definition
+ widens :: "prog \<Rightarrow> [ty list, ty list] \<Rightarrow> bool" ("_\<turnstile>_[\<preceq>]_" [71,71,71] 70)
+ where "G\<turnstile>Ts[\<preceq>]Ts' = list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts'"
lemma widens_Nil [simp]: "G\<turnstile>[][\<preceq>][]"
apply (unfold widens_def)
--- a/src/HOL/Bali/TypeSafe.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Mon Jul 26 18:25:19 2010 +0200
@@ -93,23 +93,27 @@
section "result conformance"
-definition assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env' \<Rightarrow> bool" ("_\<le>|_\<preceq>_\<Colon>\<preceq>_" [71,71,71,71] 70) where
-"s\<le>|f\<preceq>T\<Colon>\<preceq>E \<equiv>
- (\<forall>s' w. Norm s'\<Colon>\<preceq>E \<longrightarrow> fst E,s'\<turnstile>w\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> assign f w (Norm s')\<Colon>\<preceq>E) \<and>
- (\<forall>s' w. error_free s' \<longrightarrow> (error_free (assign f w s')))"
+definition
+ assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env' \<Rightarrow> bool" ("_\<le>|_\<preceq>_\<Colon>\<preceq>_" [71,71,71,71] 70)
+where
+ "s\<le>|f\<preceq>T\<Colon>\<preceq>E =
+ ((\<forall>s' w. Norm s'\<Colon>\<preceq>E \<longrightarrow> fst E,s'\<turnstile>w\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> assign f w (Norm s')\<Colon>\<preceq>E) \<and>
+ (\<forall>s' w. error_free s' \<longrightarrow> (error_free (assign f w s'))))"
-definition rconf :: "prog \<Rightarrow> lenv \<Rightarrow> st \<Rightarrow> term \<Rightarrow> vals \<Rightarrow> tys \<Rightarrow> bool" ("_,_,_\<turnstile>_\<succ>_\<Colon>\<preceq>_" [71,71,71,71,71,71] 70) where
- "G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T
- \<equiv> case T of
- Inl T \<Rightarrow> if (\<exists> var. t=In2 var)
- then (\<forall> n. (the_In2 t) = LVar n
- \<longrightarrow> (fst (the_In2 v) = the (locals s n)) \<and>
- (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T)) \<and>
- (\<not> (\<exists> n. the_In2 t=LVar n) \<longrightarrow> (G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T))\<and>
- (s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L))
- else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
- | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts"
+definition
+ rconf :: "prog \<Rightarrow> lenv \<Rightarrow> st \<Rightarrow> term \<Rightarrow> vals \<Rightarrow> tys \<Rightarrow> bool" ("_,_,_\<turnstile>_\<succ>_\<Colon>\<preceq>_" [71,71,71,71,71,71] 70)
+where
+ "G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T =
+ (case T of
+ Inl T \<Rightarrow> if (\<exists> var. t=In2 var)
+ then (\<forall> n. (the_In2 t) = LVar n
+ \<longrightarrow> (fst (the_In2 v) = the (locals s n)) \<and>
+ (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T)) \<and>
+ (\<not> (\<exists> n. the_In2 t=LVar n) \<longrightarrow> (G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T))\<and>
+ (s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L))
+ else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
+ | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts)"
text {*
With @{term rconf} we describe the conformance of the result value of a term.
@@ -324,9 +328,11 @@
declare fun_upd_apply [simp del]
-definition DynT_prop :: "[prog,inv_mode,qtname,ref_ty] \<Rightarrow> bool" ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70) where
- "G\<turnstile>mode\<rightarrow>D\<preceq>t \<equiv> mode = IntVir \<longrightarrow> is_class G D \<and>
- (if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t)"
+definition
+ DynT_prop :: "[prog,inv_mode,qtname,ref_ty] \<Rightarrow> bool" ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70)
+where
+ "G\<turnstile>mode\<rightarrow>D\<preceq>t = (mode = IntVir \<longrightarrow> is_class G D \<and>
+ (if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t))"
lemma DynT_propI:
"\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); G,s\<turnstile>a'\<Colon>\<preceq>RefT statT; wf_prog G; mode = IntVir \<longrightarrow> a' \<noteq> Null\<rbrakk>
--- a/src/HOL/Bali/Value.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/Value.thy Mon Jul 26 18:25:19 2010 +0200
@@ -17,29 +17,34 @@
| Addr loc --{* addresses, i.e. locations of objects *}
-consts the_Bool :: "val \<Rightarrow> bool"
-primrec "the_Bool (Bool b) = b"
-consts the_Intg :: "val \<Rightarrow> int"
-primrec "the_Intg (Intg i) = i"
-consts the_Addr :: "val \<Rightarrow> loc"
-primrec "the_Addr (Addr a) = a"
+primrec the_Bool :: "val \<Rightarrow> bool"
+ where "the_Bool (Bool b) = b"
+
+primrec the_Intg :: "val \<Rightarrow> int"
+ where "the_Intg (Intg i) = i"
+
+primrec the_Addr :: "val \<Rightarrow> loc"
+ where "the_Addr (Addr a) = a"
types dyn_ty = "loc \<Rightarrow> ty option"
-consts
- typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
- defpval :: "prim_ty \<Rightarrow> val" --{* default value for primitive types *}
- default_val :: " ty \<Rightarrow> val" --{* default value for all types *}
+
+primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
+where
+ "typeof dt Unit = Some (PrimT Void)"
+| "typeof dt (Bool b) = Some (PrimT Boolean)"
+| "typeof dt (Intg i) = Some (PrimT Integer)"
+| "typeof dt Null = Some NT"
+| "typeof dt (Addr a) = dt a"
-primrec "typeof dt Unit = Some (PrimT Void)"
- "typeof dt (Bool b) = Some (PrimT Boolean)"
- "typeof dt (Intg i) = Some (PrimT Integer)"
- "typeof dt Null = Some NT"
- "typeof dt (Addr a) = dt a"
+primrec defpval :: "prim_ty \<Rightarrow> val" --{* default value for primitive types *}
+where
+ "defpval Void = Unit"
+| "defpval Boolean = Bool False"
+| "defpval Integer = Intg 0"
-primrec "defpval Void = Unit"
- "defpval Boolean = Bool False"
- "defpval Integer = Intg 0"
-primrec "default_val (PrimT pt) = defpval pt"
- "default_val (RefT r ) = Null"
+primrec default_val :: "ty \<Rightarrow> val" --{* default value for all types *}
+where
+ "default_val (PrimT pt) = defpval pt"
+| "default_val (RefT r ) = Null"
end
--- a/src/HOL/Bali/WellForm.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/WellForm.thy Mon Jul 26 18:25:19 2010 +0200
@@ -31,8 +31,9 @@
text {* well-formed field declaration (common part for classes and interfaces),
cf. 8.3 and (9.3) *}
-definition wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool" where
- "wf_fdecl G P \<equiv> \<lambda>(fn,f). is_acc_type G P (type f)"
+definition
+ wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool"
+ where "wf_fdecl G P = (\<lambda>(fn,f). is_acc_type G P (type f))"
lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
apply (unfold wf_fdecl_def)
@@ -54,11 +55,12 @@
\item the parameter names are unique
\end{itemize}
*}
-definition wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" where
- "wf_mhead G P \<equiv> \<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
+definition
+ wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" where
+ "wf_mhead G P = (\<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
\<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and>
is_acc_type G P (resTy mh) \<and>
- \<spacespace> distinct (pars mh)"
+ \<spacespace> distinct (pars mh))"
text {*
@@ -76,23 +78,25 @@
\end{itemize}
*}
-definition callee_lcl :: "qtname \<Rightarrow> sig \<Rightarrow> methd \<Rightarrow> lenv" where
-"callee_lcl C sig m
- \<equiv> \<lambda> k. (case k of
+definition
+ callee_lcl :: "qtname \<Rightarrow> sig \<Rightarrow> methd \<Rightarrow> lenv" where
+ "callee_lcl C sig m =
+ (\<lambda>k. (case k of
EName e
\<Rightarrow> (case e of
VNam v
\<Rightarrow>(table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
| Res \<Rightarrow> Some (resTy m))
- | This \<Rightarrow> if is_static m then None else Some (Class C))"
+ | This \<Rightarrow> if is_static m then None else Some (Class C)))"
-definition parameters :: "methd \<Rightarrow> lname set" where
-"parameters m \<equiv> set (map (EName \<circ> VNam) (pars m))
- \<union> (if (static m) then {} else {This})"
+definition
+ parameters :: "methd \<Rightarrow> lname set" where
+ "parameters m = set (map (EName \<circ> VNam) (pars m)) \<union> (if (static m) then {} else {This})"
-definition wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool" where
- "wf_mdecl G C \<equiv>
- \<lambda>(sig,m).
+definition
+ wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool" where
+ "wf_mdecl G C =
+ (\<lambda>(sig,m).
wf_mhead G (pid C) sig (mhead m) \<and>
unique (lcls (mbody m)) \<and>
(\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T) \<and>
@@ -102,7 +106,7 @@
\<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd> \<and>
(\<exists> A. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>
\<turnstile> parameters m \<guillemotright>\<langle>stmt (mbody m)\<rangle>\<guillemotright> A
- \<and> Result \<in> nrm A)"
+ \<and> Result \<in> nrm A))"
lemma callee_lcl_VNam_simp [simp]:
"callee_lcl C sig m (EName (VNam v))
@@ -216,9 +220,10 @@
superinterfaces widens to each of the corresponding result types
\end{itemize}
*}
-definition wf_idecl :: "prog \<Rightarrow> idecl \<Rightarrow> bool" where
- "wf_idecl G \<equiv>
- \<lambda>(I,i).
+definition
+ wf_idecl :: "prog \<Rightarrow> idecl \<Rightarrow> bool" where
+ "wf_idecl G =
+ (\<lambda>(I,i).
ws_idecl G I (isuperIfs i) \<and>
\<not>is_class G I \<and>
(\<forall>(sig,mh)\<in>set (imethods i). wf_mhead G (pid I) sig mh \<and>
@@ -233,7 +238,7 @@
is_static new = is_static old)) \<and>
(Option.set \<circ> table_of (imethods i)
hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i))
- entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old))"
+ entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old)))"
lemma wf_idecl_mhead: "\<lbrakk>wf_idecl G (I,i); (sig,mh)\<in>set (imethods i)\<rbrakk> \<Longrightarrow>
wf_mhead G (pid I) sig mh \<and> \<not>is_static mh \<and> accmodi mh = Public"
@@ -317,8 +322,9 @@
\end{itemize}
*}
(* to Table *)
-definition entails :: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" ("_ entails _" 20) where
-"t entails P \<equiv> \<forall>k. \<forall> x \<in> t k: P x"
+definition
+ entails :: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" ("_ entails _" 20)
+ where "(t entails P) = (\<forall>k. \<forall> x \<in> t k: P x)"
lemma entailsD:
"\<lbrakk>t entails P; t k = Some x\<rbrakk> \<Longrightarrow> P x"
@@ -327,9 +333,10 @@
lemma empty_entails[simp]: "empty entails P"
by (simp add: entails_def)
-definition wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where
-"wf_cdecl G \<equiv>
- \<lambda>(C,c).
+definition
+ wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where
+ "wf_cdecl G =
+ (\<lambda>(C,c).
\<not>is_iface G C \<and>
(\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and>
(\<forall>s. \<forall> im \<in> imethds G I s.
@@ -352,7 +359,7 @@
(G,sig\<turnstile>new hides old
\<longrightarrow> (accmodi old \<le> accmodi new \<and>
is_static old))))
- ))"
+ )))"
(*
definition wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where
@@ -511,13 +518,14 @@
\item all defined classes are wellformed
\end{itemize}
*}
-definition wf_prog :: "prog \<Rightarrow> bool" where
- "wf_prog G \<equiv> let is = ifaces G; cs = classes G in
+definition
+ wf_prog :: "prog \<Rightarrow> bool" where
+ "wf_prog G = (let is = ifaces G; cs = classes G in
ObjectC \<in> set cs \<and>
(\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package) \<and>
(\<forall>xn. SXcptC xn \<in> set cs) \<and>
(\<forall>i\<in>set is. wf_idecl G i) \<and> unique is \<and>
- (\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs"
+ (\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs)"
lemma wf_prog_idecl: "\<lbrakk>iface G I = Some i; wf_prog G\<rbrakk> \<Longrightarrow> wf_idecl G (I,i)"
apply (unfold wf_prog_def Let_def)
@@ -2095,16 +2103,16 @@
Class dynC
Array Object
*}
-consts valid_lookup_cls:: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> bool \<Rightarrow> bool"
+primrec valid_lookup_cls:: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> bool \<Rightarrow> bool"
("_,_ \<turnstile> _ valid'_lookup'_cls'_for _" [61,61,61,61] 60)
-primrec
-"G,NullT \<turnstile> dynC valid_lookup_cls_for static_membr = False"
-"G,IfaceT I \<turnstile> dynC valid_lookup_cls_for static_membr
- = (if static_membr
- then dynC=Object
- else G\<turnstile>Class dynC\<preceq> Iface I)"
-"G,ClassT C \<turnstile> dynC valid_lookup_cls_for static_membr = G\<turnstile>Class dynC\<preceq> Class C"
-"G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)"
+where
+ "G,NullT \<turnstile> dynC valid_lookup_cls_for static_membr = False"
+| "G,IfaceT I \<turnstile> dynC valid_lookup_cls_for static_membr
+ = (if static_membr
+ then dynC=Object
+ else G\<turnstile>Class dynC\<preceq> Iface I)"
+| "G,ClassT C \<turnstile> dynC valid_lookup_cls_for static_membr = G\<turnstile>Class dynC\<preceq> Class C"
+| "G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)"
lemma valid_lookup_cls_is_class:
assumes dynC: "G,statT \<turnstile> dynC valid_lookup_cls_for static_membr" and
--- a/src/HOL/Bali/WellType.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Bali/WellType.thy Mon Jul 26 18:25:19 2010 +0200
@@ -53,11 +53,13 @@
emhead = "ref_ty \<times> mhead"
--{* Some mnemotic selectors for emhead *}
-definition "declrefT" :: "emhead \<Rightarrow> ref_ty" where
- "declrefT \<equiv> fst"
+definition
+ "declrefT" :: "emhead \<Rightarrow> ref_ty"
+ where "declrefT = fst"
-definition "mhd" :: "emhead \<Rightarrow> mhead" where
- "mhd \<equiv> snd"
+definition
+ "mhd" :: "emhead \<Rightarrow> mhead"
+ where "mhd \<equiv> snd"
lemma declrefT_simp[simp]:"declrefT (r,m) = r"
by (simp add: declrefT_def)
@@ -77,50 +79,51 @@
lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m"
by (cases m) simp
-consts
- cmheads :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
- Objectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
- accObjectmheads:: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
- mheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
-defs
- cmheads_def:
-"cmheads G S C
- \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig)"
- Objectmheads_def:
-"Objectmheads G S
- \<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd)))
- ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
- accObjectmheads_def:
-"accObjectmheads G S T
- \<equiv> if G\<turnstile>RefT T accessible_in (pid S)
- then Objectmheads G S
- else (\<lambda>sig. {})"
-primrec
-"mheads G S NullT = (\<lambda>sig. {})"
-"mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h))
- ` accimethds G (pid S) I sig \<union>
- accObjectmheads G S (IfaceT I) sig)"
-"mheads G S (ClassT C) = cmheads G S C"
-"mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
+definition
+ cmheads :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
+ where "cmheads G S C = (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig))"
+
+definition
+ Objectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" where
+ "Objectmheads G S =
+ (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd)))
+ ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig))"
+
+definition
+ accObjectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
+where
+ "accObjectmheads G S T =
+ (if G\<turnstile>RefT T accessible_in (pid S)
+ then Objectmheads G S
+ else (\<lambda>sig. {}))"
+
+primrec mheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
+where
+ "mheads G S NullT = (\<lambda>sig. {})"
+| "mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h))
+ ` accimethds G (pid S) I sig \<union>
+ accObjectmheads G S (IfaceT I) sig)"
+| "mheads G S (ClassT C) = cmheads G S C"
+| "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
definition
--{* applicable methods, cf. 15.11.2.1 *}
- appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
- "appl_methds G S rt = (\<lambda> sig.
+ appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
+ "appl_methds G S rt = (\<lambda> sig.
{(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and>
G\<turnstile>(parTs sig)[\<preceq>]pTs'})"
definition
--{* more specific methods, cf. 15.11.2.2 *}
- more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
- "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
+ more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
+ "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
(*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*)
definition
--{* maximally specific methods, cf. 15.11.2.2 *}
- max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
- "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
- (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
+ max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" where
+ "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
+ (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
lemma max_spec2appl_meths:
@@ -138,13 +141,15 @@
done
-definition empty_dt :: "dyn_ty" where
- "empty_dt \<equiv> \<lambda>a. None"
+definition
+ empty_dt :: "dyn_ty"
+ where "empty_dt = (\<lambda>a. None)"
-definition invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" where
-"invmode m e \<equiv> if is_static m
+definition
+ invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" where
+ "invmode m e = (if is_static m
then Static
- else if e=Super then SuperM else IntVir"
+ else if e=Super then SuperM else IntVir)"
lemma invmode_nonstatic [simp]:
"invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir"
@@ -171,71 +176,71 @@
section "Typing for unary operations"
-consts unop_type :: "unop \<Rightarrow> prim_ty"
-primrec
-"unop_type UPlus = Integer"
-"unop_type UMinus = Integer"
-"unop_type UBitNot = Integer"
-"unop_type UNot = Boolean"
+primrec unop_type :: "unop \<Rightarrow> prim_ty"
+where
+ "unop_type UPlus = Integer"
+| "unop_type UMinus = Integer"
+| "unop_type UBitNot = Integer"
+| "unop_type UNot = Boolean"
-consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
-primrec
-"wt_unop UPlus t = (t = PrimT Integer)"
-"wt_unop UMinus t = (t = PrimT Integer)"
-"wt_unop UBitNot t = (t = PrimT Integer)"
-"wt_unop UNot t = (t = PrimT Boolean)"
+primrec wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool"
+where
+ "wt_unop UPlus t = (t = PrimT Integer)"
+| "wt_unop UMinus t = (t = PrimT Integer)"
+| "wt_unop UBitNot t = (t = PrimT Integer)"
+| "wt_unop UNot t = (t = PrimT Boolean)"
section "Typing for binary operations"
-consts binop_type :: "binop \<Rightarrow> prim_ty"
-primrec
-"binop_type Mul = Integer"
-"binop_type Div = Integer"
-"binop_type Mod = Integer"
-"binop_type Plus = Integer"
-"binop_type Minus = Integer"
-"binop_type LShift = Integer"
-"binop_type RShift = Integer"
-"binop_type RShiftU = Integer"
-"binop_type Less = Boolean"
-"binop_type Le = Boolean"
-"binop_type Greater = Boolean"
-"binop_type Ge = Boolean"
-"binop_type Eq = Boolean"
-"binop_type Neq = Boolean"
-"binop_type BitAnd = Integer"
-"binop_type And = Boolean"
-"binop_type BitXor = Integer"
-"binop_type Xor = Boolean"
-"binop_type BitOr = Integer"
-"binop_type Or = Boolean"
-"binop_type CondAnd = Boolean"
-"binop_type CondOr = Boolean"
+primrec binop_type :: "binop \<Rightarrow> prim_ty"
+where
+ "binop_type Mul = Integer"
+| "binop_type Div = Integer"
+| "binop_type Mod = Integer"
+| "binop_type Plus = Integer"
+| "binop_type Minus = Integer"
+| "binop_type LShift = Integer"
+| "binop_type RShift = Integer"
+| "binop_type RShiftU = Integer"
+| "binop_type Less = Boolean"
+| "binop_type Le = Boolean"
+| "binop_type Greater = Boolean"
+| "binop_type Ge = Boolean"
+| "binop_type Eq = Boolean"
+| "binop_type Neq = Boolean"
+| "binop_type BitAnd = Integer"
+| "binop_type And = Boolean"
+| "binop_type BitXor = Integer"
+| "binop_type Xor = Boolean"
+| "binop_type BitOr = Integer"
+| "binop_type Or = Boolean"
+| "binop_type CondAnd = Boolean"
+| "binop_type CondOr = Boolean"
-consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
-primrec
-"wt_binop G Mul t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Div t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Mod t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Plus t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Minus t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G LShift t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G RShift t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Less t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Le t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Ge t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Eq t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
-"wt_binop G Neq t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
-"wt_binop G BitAnd t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G And t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
-"wt_binop G BitXor t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Xor t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
-"wt_binop G BitOr t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
-"wt_binop G Or t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
-"wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
-"wt_binop G CondOr t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+primrec wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
+where
+ "wt_binop G Mul t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Div t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Mod t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Plus t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Minus t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G LShift t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G RShift t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Less t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Le t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Ge t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Eq t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
+| "wt_binop G Neq t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)"
+| "wt_binop G BitAnd t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G And t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+| "wt_binop G BitXor t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Xor t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+| "wt_binop G BitOr t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))"
+| "wt_binop G Or t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+| "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
+| "wt_binop G CondOr t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))"
section "Typing for terms"
@@ -244,9 +249,8 @@
(type) "tys" <= (type) "ty + ty list"
-inductive
- wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_" [51,51,51,51] 50)
- and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>" [51,51,51 ] 50)
+inductive wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_" [51,51,51,51] 50)
+ and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>" [51,51,51] 50)
and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
and ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
and ty_exprs :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, ty list] \<Rightarrow> bool"
--- a/src/HOL/Tools/inductive.ML Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Mon Jul 26 18:25:19 2010 +0200
@@ -522,9 +522,9 @@
fun gen_inductive_cases prep_att prep_prop args lthy =
let
val thy = ProofContext.theory_of lthy;
- val facts = args |> map (fn ((a, atts), props) =>
+ val facts = args |> Par_List.map (fn ((a, atts), props) =>
((a, map (prep_att thy) atts),
- map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
+ Par_List.map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
in lthy |> Local_Theory.notes facts |>> map snd end;
val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
--- a/src/Pure/Isar/isar_cmd.ML Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Mon Jul 26 18:25:19 2010 +0200
@@ -274,10 +274,8 @@
(* init and exit *)
fun init_theory (name, imports, uses) =
- Toplevel.init_theory name (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses))
- (fn thy =>
- if Thy_Info.check_known_thy (Context.theory_name thy)
- then Thy_Info.end_theory thy else ());
+ Toplevel.init_theory name
+ (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses));
val exit = Toplevel.keep (fn state =>
(Context.set_thread_data (try Toplevel.generic_theory_of state);
--- a/src/Pure/Isar/isar_document.ML Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML Mon Jul 26 18:25:19 2010 +0200
@@ -181,7 +181,7 @@
fun begin_document (id: document_id) path =
let
- val (dir, name) = Thy_Load.split_thy_path path;
+ val (dir, name) = Thy_Header.split_thy_path path;
val _ = define_document id (make_document dir name no_entries);
in () end;
@@ -192,13 +192,10 @@
val end_state =
the_state (the (#state (#3 (the
(first_entry (fn (_, {next, ...}) => is_none next) document)))));
- val _ = (* FIXME regular execution (??) *)
+ val _ = (* FIXME regular execution (??), result (??) *)
Future.fork (fn () =>
(case Lazy.force end_state of
- SOME st =>
- (Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st;
- Thy_Info.touch_child_thys name;
- Thy_Info.register_thy name)
+ SOME st => Toplevel.end_theory (Position.id_only id) st
| NONE => error ("Failed to finish theory " ^ quote name)));
in () end);
--- a/src/Pure/Isar/isar_syn.ML Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Mon Jul 26 18:25:19 2010 +0200
@@ -304,30 +304,23 @@
(* use ML text *)
-fun propagate_env (context as Context.Proof lthy) =
- Context.Proof (Local_Theory.map_contexts (ML_Env.inherit context) lthy)
- | propagate_env context = context;
-
-fun propagate_env_prf prf = Proof.map_contexts
- (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf;
-
val _ =
Outer_Syntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
- (Parse.path >>
- (fn path => Toplevel.generic_theory (Thy_Info.exec_file path #> propagate_env)));
+ (Parse.path >> (fn path => Toplevel.generic_theory (Thy_Load.exec_ml path)));
val _ =
Outer_Syntax.command "ML" "ML text within theory or local theory"
(Keyword.tag_ml Keyword.thy_decl)
(Parse.ML_source >> (fn (txt, pos) =>
Toplevel.generic_theory
- (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #> propagate_env)));
+ (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>
+ Local_Theory.propagate_ml_env)));
val _ =
Outer_Syntax.command "ML_prf" "ML text within proof" (Keyword.tag_proof Keyword.prf_decl)
(Parse.ML_source >> (fn (txt, pos) =>
Toplevel.proof (Proof.map_context (Context.proof_map
- (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf)));
+ (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env)));
val _ =
Outer_Syntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)
--- a/src/Pure/Isar/local_theory.ML Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Isar/local_theory.ML Mon Jul 26 18:25:19 2010 +0200
@@ -5,6 +5,7 @@
*)
type local_theory = Proof.context;
+type generic_theory = Context.generic;
signature LOCAL_THEORY =
sig
@@ -25,6 +26,7 @@
val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
+ val propagate_ml_env: generic_theory -> generic_theory
val standard_morphism: local_theory -> Proof.context -> morphism
val target_morphism: local_theory -> morphism
val global_morphism: local_theory -> morphism
@@ -173,6 +175,10 @@
target (Context.proof_map f) #>
Context.proof_map f;
+fun propagate_ml_env (context as Context.Proof lthy) =
+ Context.Proof (map_contexts (ML_Env.inherit context) lthy)
+ | propagate_ml_env context = context;
+
(* morphisms *)
--- a/src/Pure/Isar/outer_syntax.ML Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Mon Jul 26 18:25:19 2010 +0200
@@ -31,7 +31,7 @@
type isar
val isar: bool -> isar
val prepare_command: Position.T -> string -> Toplevel.transition
- val load_thy: string -> Position.T -> string -> unit -> unit
+ val load_thy: string -> Position.T -> string -> (unit -> unit) * theory
end;
structure Outer_Syntax: OUTER_SYNTAX =
@@ -204,7 +204,7 @@
fun process_file path thy =
let
val trs = parse (Path.position path) (File.read path);
- val init = Toplevel.init_theory "" (K thy) (K ()) Toplevel.empty;
+ val init = Toplevel.init_theory "" (K thy) Toplevel.empty;
val result = fold Toplevel.command (init :: trs) Toplevel.toplevel;
in
(case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of
@@ -285,14 +285,14 @@
(fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
- val results = cond_timeit time "" (fn () => Toplevel.excursion units);
+ val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion units);
val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
fun after_load () =
Thy_Output.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks
|> Buffer.content
|> Present.theory_output name;
- in after_load end;
+ in (after_load, thy) end;
end;
--- a/src/Pure/Isar/proof.ML Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Isar/proof.ML Mon Jul 26 18:25:19 2010 +0200
@@ -17,6 +17,7 @@
val theory_of: state -> theory
val map_context: (context -> context) -> state -> state
val map_contexts: (context -> context) -> state -> state
+ val propagate_ml_env: state -> state
val bind_terms: (indexname * term option) list -> state -> state
val put_thms: bool -> string * thm list option -> state -> state
val the_facts: state -> thm list
@@ -207,6 +208,9 @@
fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
+fun propagate_ml_env state = map_contexts
+ (Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state;
+
val bind_terms = map_context o ProofContext.bind_terms;
val put_thms = map_context oo ProofContext.put_thms;
--- a/src/Pure/Isar/toplevel.ML Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Mon Jul 26 18:25:19 2010 +0200
@@ -7,7 +7,6 @@
signature TOPLEVEL =
sig
exception UNDEF
- type generic_theory
type state
val toplevel: state
val is_toplevel: state -> bool
@@ -22,6 +21,7 @@
val proof_of: state -> Proof.state
val proof_position_of: state -> int
val enter_proof_body: state -> Proof.state
+ val end_theory: Position.T -> state -> theory
val print_state_context: state -> unit
val print_state: bool -> state -> unit
val pretty_abstract: state -> Pretty.T
@@ -46,7 +46,7 @@
val interactive: bool -> transition -> transition
val print: transition -> transition
val no_timing: transition -> transition
- val init_theory: string -> (bool -> theory) -> (theory -> unit) -> transition -> transition
+ val init_theory: string -> (bool -> theory) -> transition -> transition
val exit: transition -> transition
val keep: (state -> unit) -> transition -> transition
val keep': (bool -> state -> unit) -> transition -> transition
@@ -88,9 +88,8 @@
val add_hook: (transition -> state -> state -> unit) -> unit
val transition: bool -> transition -> state -> (state * (exn * string) option) option
val run_command: string -> transition -> state -> state option
- val commit_exit: Position.T -> transition
val command: transition -> state -> state
- val excursion: (transition * transition list) list -> (transition * state) list lazy
+ val excursion: (transition * transition list) list -> (transition * state) list lazy * theory
end;
structure Toplevel: TOPLEVEL =
@@ -103,8 +102,6 @@
(* local theory wrappers *)
-type generic_theory = Context.generic; (*theory or local_theory*)
-
val loc_init = Theory_Target.context_cmd;
val loc_exit = Local_Theory.exit_global;
@@ -140,8 +137,7 @@
(* datatype state *)
-type node_info = node * (theory -> unit); (*node with exit operation*)
-datatype state = State of node_info option * node_info option; (*current, previous*)
+datatype state = State of node option * node option; (*current, previous*)
val toplevel = State (NONE, NONE);
@@ -149,21 +145,21 @@
| is_toplevel _ = false;
fun level (State (NONE, _)) = 0
- | level (State (SOME (Theory _, _), _)) = 0
- | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (Proof_Node.current prf)
- | level (State (SOME (SkipProof (d, _), _), _)) = d + 1; (*different notion of proof depth!*)
+ | level (State (SOME (Theory _), _)) = 0
+ | level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf)
+ | level (State (SOME (SkipProof (d, _)), _)) = d + 1; (*different notion of proof depth!*)
fun str_of_state (State (NONE, _)) = "at top level"
- | str_of_state (State (SOME (Theory (Context.Theory _, _), _), _)) = "in theory mode"
- | str_of_state (State (SOME (Theory (Context.Proof _, _), _), _)) = "in local theory mode"
- | str_of_state (State (SOME (Proof _, _), _)) = "in proof mode"
- | str_of_state (State (SOME (SkipProof _, _), _)) = "in skipped proof mode";
+ | str_of_state (State (SOME (Theory (Context.Theory _, _)), _)) = "in theory mode"
+ | str_of_state (State (SOME (Theory (Context.Proof _, _)), _)) = "in local theory mode"
+ | str_of_state (State (SOME (Proof _), _)) = "in proof mode"
+ | str_of_state (State (SOME (SkipProof _), _)) = "in skipped proof mode";
(* current node *)
fun node_of (State (NONE, _)) = raise UNDEF
- | node_of (State (SOME (node, _), _)) = node;
+ | node_of (State (SOME node, _)) = node;
fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state));
fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state));
@@ -177,7 +173,7 @@
| NONE => raise UNDEF);
fun previous_context_of (State (_, NONE)) = NONE
- | previous_context_of (State (_, SOME (prev, _))) = SOME (context_node prev);
+ | previous_context_of (State (_, SOME prev)) = SOME (context_node prev);
val context_of = node_case Context.proof_of Proof.context_of;
val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
@@ -191,6 +187,9 @@
val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
+fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = Theory.end_theory thy
+ | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos);
+
(* print state *)
@@ -267,12 +266,12 @@
in
-fun apply_transaction f g (node, exit) =
+fun apply_transaction f g node =
let
val _ = is_draft_theory node andalso error "Illegal draft theory in toplevel state";
val cont_node = reset_presentation node;
val back_node = map_theory (Theory.checkpoint o Theory.copy) cont_node;
- fun state_error e nd = (State (SOME (nd, exit), SOME (node, exit)), e);
+ fun state_error e nd = (State (SOME nd, SOME node), e);
val (result, err) =
cont_node
@@ -296,21 +295,18 @@
(* primitive transitions *)
datatype trans =
- Init of string * (bool -> theory) * (theory -> unit) | (*theory name, init, exit*)
- Exit | (*formal exit of theory -- without committing*)
- CommitExit | (*exit and commit final theory*)
- Keep of bool -> state -> unit | (*peek at state*)
+ Init of string * (bool -> theory) | (*theory name, init*)
+ Exit | (*formal exit of theory*)
+ Keep of bool -> state -> unit | (*peek at state*)
Transaction of (bool -> node -> node) * (state -> unit); (*node transaction and presentation*)
local
-fun apply_tr int (Init (_, f, exit)) (State (NONE, _)) =
+fun apply_tr int (Init (_, f)) (State (NONE, _)) =
State (SOME (Theory (Context.Theory
- (Theory.checkpoint (Runtime.controlled_execution f int)), NONE), exit), NONE)
- | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
+ (Theory.checkpoint (Runtime.controlled_execution f int)), NONE)), NONE)
+ | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) =
State (NONE, prev)
- | apply_tr _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
- (Runtime.controlled_execution exit thy; toplevel)
| apply_tr int (Keep f) state =
Runtime.controlled_execution (fn x => tap (f int) x) state
| apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
@@ -355,7 +351,7 @@
(* diagnostics *)
-fun init_of (Transition {trans = [Init (name, _, _)], ...}) = SOME name
+fun init_of (Transition {trans = [Init (name, _)], ...}) = SOME name
| init_of _ = NONE;
fun name_of (Transition {name, ...}) = name;
@@ -397,7 +393,7 @@
(* basic transitions *)
-fun init_theory name f exit = add_trans (Init (name, f, exit));
+fun init_theory name f = add_trans (Init (name, f));
val exit = add_trans Exit;
val keep' = add_trans o Keep;
@@ -632,7 +628,7 @@
fun run_command thy_name tr st =
(case
(case init_of tr of
- SOME name => Exn.capture (fn () => Thy_Load.consistent_name thy_name name) ()
+ SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) ()
| NONE => Exn.Result ()) of
Exn.Result () =>
let val int = is_some (init_of tr) in
@@ -646,15 +642,6 @@
| Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
-(* commit final exit *)
-
-fun commit_exit pos =
- name "end" empty
- |> position pos
- |> add_trans CommitExit
- |> imperative (fn () => warning "Expected to find finished theory");
-
-
(* nested commands *)
fun command tr st =
@@ -696,8 +683,8 @@
(fn prf =>
Future.fork_pri ~1 (fn () =>
let val (states, result_state) =
- (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
- => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy)), exit), prev))
+ (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
+ => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
|> fold_map command_result body_trs
||> command (end_tr |> set_print false);
in (states, presentation_context_of result_state) end))
@@ -718,14 +705,9 @@
fun excursion input =
let
val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
-
val immediate = not (Goal.future_enabled ());
val (results, end_state) = fold_map (proof_result immediate) input toplevel;
- val _ =
- (case end_state of
- State (NONE, SOME (Theory (Context.Theory _, _), _)) =>
- command (commit_exit end_pos) end_state
- | _ => error "Unfinished development at end of input");
- in Lazy.lazy (fn () => maps Lazy.force results) end;
+ val thy = end_theory end_pos end_state;
+ in (Lazy.lazy (fn () => maps Lazy.force results), thy) end;
end;
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Jul 26 18:25:19 2010 +0200
@@ -137,12 +137,11 @@
val name = thy_name file;
val _ = name = "" andalso error ("Bad file name: " ^ quote file);
val _ =
- if Thy_Info.check_known_thy name then
- (Isar.>> (Toplevel.commit_exit Position.none);
- Thy_Info.touch_child_thys name; Thy_Info.register_thy name)
+ if Thy_Info.known_thy name then
+ Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ()))
handle ERROR msg =>
(warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
- tell_file_retracted (Thy_Load.thy_path name))
+ tell_file_retracted (Thy_Header.thy_path name))
else ();
val _ = Isar.init ();
in () end;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Jul 26 18:25:19 2010 +0200
@@ -218,15 +218,14 @@
val thy_name = Path.implode o #1 o Path.split_ext o Path.base;
val inform_file_retracted = Thy_Info.if_known_thy Thy_Info.remove_thy o thy_name;
-val inform_file_processed = Thy_Info.if_known_thy Thy_Info.touch_child_thys o thy_name;
-fun proper_inform_file_processed path state =
+fun inform_file_processed path state =
let val name = thy_name path in
if Toplevel.is_toplevel state andalso Thy_Info.known_thy name then
- (Thy_Info.touch_child_thys name;
- Thy_Info.register_thy name handle ERROR msg =>
- (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
- tell_file_retracted true (Path.base path)))
+ Thy_Info.register_thy (Toplevel.end_theory Position.none state)
+ handle ERROR msg =>
+ (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
+ tell_file_retracted true (Path.base path))
else raise Toplevel.UNDEF
end;
@@ -819,7 +818,7 @@
fun closefile _ =
case !currently_open_file of
- SOME f => (proper_inform_file_processed f (Isar.state());
+ SOME f => (inform_file_processed f (Isar.state ());
priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
currently_open_file := NONE)
| NONE => raise PGIP ("<closefile> when no file is open!")
--- a/src/Pure/ROOT.ML Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/ROOT.ML Mon Jul 26 18:25:19 2010 +0200
@@ -184,10 +184,8 @@
(*theory sources*)
use "Thy/thy_header.ML";
-use "Thy/thy_load.ML";
use "Thy/html.ML";
use "Thy/latex.ML";
-use "Thy/present.ML";
(*basic proof engine*)
use "Isar/proof_display.ML";
@@ -227,10 +225,12 @@
use "Isar/constdefs.ML";
(*toplevel transactions*)
+use "Thy/thy_load.ML";
use "Isar/proof_node.ML";
use "Isar/toplevel.ML";
(*theory syntax*)
+use "Thy/present.ML";
use "Thy/term_style.ML";
use "Thy/thy_output.ML";
use "Thy/thy_syntax.ML";
--- a/src/Pure/Thy/thy_header.ML Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Thy/thy_header.ML Mon Jul 26 18:25:19 2010 +0200
@@ -8,6 +8,9 @@
sig
val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
+ val thy_path: string -> Path.T
+ val split_thy_path: Path.T -> Path.T * string
+ val consistent_name: string -> string -> unit
end;
structure Thy_Header: THY_HEADER =
@@ -63,4 +66,19 @@
| NONE => error ("Unexpected end of input" ^ Position.str_of pos))
end;
+
+(* file formats *)
+
+val thy_path = Path.ext "thy" o Path.basic;
+
+fun split_thy_path path =
+ (case Path.split_ext path of
+ (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
+ | _ => error ("Bad theory file specification " ^ Path.implode path));
+
+fun consistent_name name name' =
+ if name = name' then ()
+ else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
+ " does not agree with theory name " ^ quote name');
+
end;
--- a/src/Pure/Thy/thy_info.ML Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML Mon Jul 26 18:25:19 2010 +0200
@@ -11,7 +11,6 @@
val add_hook: (action -> string -> unit) -> unit
val get_names: unit -> string list
val known_thy: string -> bool
- val check_known_thy: string -> bool
val if_known_thy: (string -> unit) -> string -> unit
val lookup_theory: string -> theory option
val get_theory: string -> theory
@@ -19,20 +18,13 @@
val master_directory: string -> Path.T
val loaded_files: string -> Path.T list
val touch_thy: string -> unit
- val touch_child_thys: string -> unit
val thy_ord: theory * theory -> order
val remove_thy: string -> unit
val kill_thy: string -> unit
- val provide_file: Path.T -> string -> unit
- val load_file: Path.T -> unit
- val exec_file: Path.T -> Context.generic -> Context.generic
- val use: string -> unit
val use_thys: string list -> unit
val use_thy: string -> unit
val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
- val end_theory: theory -> unit
- val register_thy: string -> unit
- val register_theory: theory -> unit
+ val register_thy: theory -> unit
val finish: unit -> unit
end;
@@ -80,18 +72,15 @@
(* thy database *)
type deps =
- {update_time: int, (*symbolic time of update; negative value means outdated*)
- master: (Path.T * File.ident) option, (*master dependencies for thy file*)
- text: string, (*source text for thy*)
- parents: string list, (*source specification of parents (partially qualified)*)
- (*auxiliary files: source path, physical path + identifier*)
- files: (Path.T * (Path.T * File.ident) option) list};
+ {update_time: int, (*symbolic time of update; negative value means outdated*)
+ master: (Path.T * File.ident) option, (*master dependencies for thy file*)
+ text: string, (*source text for thy*)
+ parents: string list}; (*source specification of parents (partially qualified)*)
-fun make_deps update_time master text parents files : deps =
- {update_time = update_time, master = master, text = text, parents = parents, files = files};
+fun make_deps update_time master text parents : deps =
+ {update_time = update_time, master = master, text = text, parents = parents};
-fun init_deps master text parents files =
- SOME (make_deps ~1 master text parents (map (rpair NONE) files));
+fun init_deps master text parents = SOME (make_deps ~1 master text parents);
fun master_dir NONE = Path.current
| master_dir (SOME (path, _)) = Path.dir path;
@@ -123,8 +112,7 @@
SOME (thy_graph Graph.get_node name) handle Graph.UNDEF _ => NONE;
val known_thy = is_some o lookup_thy;
-fun check_known_thy name = known_thy name orelse (warning ("Unknown theory " ^ quote name); false);
-fun if_known_thy f name = if check_known_thy name then f name else ();
+fun if_known_thy f name = if known_thy name then f name else ();
fun get_thy name =
(case lookup_thy name of
@@ -140,17 +128,11 @@
val lookup_deps = Option.map #1 o lookup_thy;
val get_deps = #1 o get_thy;
fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x));
+fun put_theory name theory = change_thy name (fn (deps, _) => (deps, SOME theory));
val is_finished = is_none o get_deps;
val master_directory = master_dir' o get_deps;
-fun loaded_files name =
- (case get_deps name of
- NONE => []
- | SOME {master, files, ...} =>
- (case master of SOME (thy_path, _) => [thy_path] | NONE => []) @
- (map_filter (Option.map #1 o #2) files));
-
fun get_parents name =
thy_graph Graph.imm_preds name handle Graph.UNDEF _ =>
error (loader_msg "nothing known about theory" [name]);
@@ -168,27 +150,18 @@
SOME theory => theory
| _ => error (loader_msg "undefined theory entry for" [name]));
+fun loaded_files name =
+ (case get_deps name of
+ NONE => []
+ | SOME {master, ...} =>
+ (case master of
+ NONE => []
+ | SOME (thy_path, _) => thy_path :: Thy_Load.loaded_files (get_theory name)));
+
(** thy operations **)
-(* check state *)
-
-fun check_unfinished fail name =
- if known_thy name andalso is_finished name then
- fail (loader_msg "cannot update finished theory" [name])
- else ();
-
-fun check_files name =
- let
- val files = (case get_deps name of SOME {files, ...} => files | NONE => []);
- val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path) | _ => NONE) files;
- val _ = null missing_files orelse
- error (loader_msg "unresolved dependencies of theory" [name] ^
- " on file(s): " ^ commas_quote missing_files);
- in () end;
-
-
(* maintain update_time *)
local
@@ -207,14 +180,13 @@
fun outdate_thy name =
if is_finished name orelse is_outdated name then ()
else CRITICAL (fn () =>
- (change_deps name (Option.map (fn {master, text, parents, files, ...} =>
- make_deps ~1 master text parents files)); perform Outdate name));
+ (change_deps name (Option.map (fn {master, text, parents, ...} =>
+ make_deps ~1 master text parents)); perform Outdate name));
fun touch_thys names =
List.app outdate_thy (thy_graph Graph.all_succs (map_filter unfinished names));
fun touch_thy name = touch_thys [name];
-fun touch_child_thys name = touch_thys (thy_graph Graph.imm_succs name);
end;
@@ -266,52 +238,6 @@
val kill_thy = if_known_thy remove_thy;
-(* load_file *)
-
-local
-
-fun provide path name info (SOME {update_time, master, text, parents, files}) =
- (if AList.defined (op =) files path then ()
- else warning (loader_msg "undeclared dependency of theory" [name] ^
- " on file: " ^ quote (Path.implode path));
- SOME (make_deps update_time master text parents
- (AList.update (op =) (path, SOME info) files)))
- | provide _ _ _ NONE = NONE;
-
-fun run_file path =
- (case Option.map (Context.theory_name o Context.the_theory) (Context.thread_data ()) of
- NONE => (Thy_Load.load_ml Path.current path; ())
- | SOME name =>
- (case lookup_deps name of
- SOME deps =>
- change_deps name (provide path name (Thy_Load.load_ml (master_dir' deps) path))
- | NONE => (Thy_Load.load_ml Path.current path; ())));
-
-in
-
-fun provide_file path name =
- let
- val dir = master_directory name;
- val _ = check_unfinished error name;
- in change_deps name (provide path name (Thy_Load.check_file dir path)) end;
-
-fun load_file path =
- if ! Output.timing then
- let val name = Path.implode path in
- timeit (fn () =>
- (priority ("\n**** Starting file " ^ quote name ^ " ****");
- run_file path;
- priority ("**** Finished file " ^ quote name ^ " ****\n")))
- end
- else run_file path;
-
-fun exec_file path = ML_Context.exec (fn () => load_file path);
-
-val use = load_file o Path.explode;
-
-end;
-
-
(* load_thy *)
fun required_by _ [] = ""
@@ -321,22 +247,23 @@
let
val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
fun corrupted () = error (loader_msg "corrupted dependency information" [name]);
- val (pos, text, _) =
+ val (pos, text) =
(case get_deps name of
- SOME {master = SOME (master_path, _), text, files, ...} =>
+ SOME {master = SOME (master_path, _), text, ...} =>
if text = "" then corrupted ()
- else (Path.position master_path, text, files)
+ else (Path.position master_path, text)
| _ => corrupted ());
val _ = touch_thy name;
- val _ = CRITICAL (fn () =>
- change_deps name (Option.map (fn {master, text, parents, files, ...} =>
- make_deps upd_time master text parents files)));
- val after_load = Outer_Syntax.load_thy name pos text;
+ val _ =
+ change_deps name (Option.map (fn {master, text, parents, ...} =>
+ make_deps upd_time master text parents));
+ val (after_load, theory) = Outer_Syntax.load_thy name pos text;
+ val _ = put_theory name theory;
val _ =
CRITICAL (fn () =>
(change_deps name
- (Option.map (fn {update_time, master, parents, files, ...} =>
- make_deps update_time master "" parents files));
+ (Option.map (fn {update_time, master, parents, ...} =>
+ make_deps update_time master "" parents));
perform Update name));
in after_load end;
@@ -410,43 +337,33 @@
local
-fun check_file master (src_path, info) =
- let val info' =
- (case info of
- NONE => NONE
- | SOME (_, id) =>
- (case Thy_Load.test_file (master_dir master) src_path of
- NONE => NONE
- | SOME (path', id') => if id <> id' then NONE else SOME (path', id')))
- in (src_path, info') end;
-
fun check_deps dir name =
(case lookup_deps name of
SOME NONE => (true, NONE, get_parents name)
| NONE =>
- let val {master, text, imports = parents, uses = files} = Thy_Load.deps_thy dir name
- in (false, init_deps (SOME master) text parents files, parents) end
- | SOME (SOME {update_time, master, text, parents, files}) =>
+ let val {master, text, imports = parents, ...} = Thy_Load.deps_thy dir name
+ in (false, init_deps (SOME master) text parents, parents) end
+ | SOME (SOME {update_time, master, text, parents}) =>
let
val (thy_path, thy_id) = Thy_Load.check_thy dir name;
val master' = SOME (thy_path, thy_id);
in
if Option.map #2 master <> SOME thy_id then
- let val {text = text', imports = parents', uses = files', ...} =
- Thy_Load.deps_thy dir name;
- in (false, init_deps master' text' parents' files', parents') end
+ let val {text = text', imports = parents', ...} = Thy_Load.deps_thy dir name;
+ in (false, init_deps master' text' parents', parents') end
else
let
- val files' = map (check_file master') files;
- val current = update_time >= 0 andalso can get_theory name
- andalso forall (is_some o snd) files';
+ val current =
+ (case lookup_theory name of
+ NONE => false
+ | SOME theory => update_time >= 0 andalso Thy_Load.all_current theory);
val update_time' = if current then update_time else ~1;
- val deps' = SOME (make_deps update_time' master' text parents files');
+ val deps' = SOME (make_deps update_time' master' text parents);
in (current, deps', parents) end
end);
-fun read_text (SOME {update_time, master = master as SOME (path, _), text = _, parents, files}) =
- SOME (make_deps update_time master (File.read path) parents files);
+fun read_text (SOME {update_time, master = master as SOME (path, _), text = _, parents}) =
+ SOME (make_deps update_time master (File.read path) parents);
in
@@ -495,28 +412,31 @@
schedule_tasks (snd (require_thys [] dir arg Graph.empty));
val use_thys = use_thys_dir Path.current;
-
-fun use_thy str =
- let
- val name = base_name str;
- val _ = check_unfinished warning name;
- in use_thys [str] end;
+val use_thy = use_thys o single;
-(* begin / end theory *)
+(* begin theory *)
+
+fun check_unfinished name =
+ if known_thy name andalso is_finished name then
+ error (loader_msg "cannot update finished theory" [name])
+ else ();
fun begin_theory name parents uses int =
let
val parent_names = map base_name parents;
val dir = master_dir'' (lookup_deps name);
- val _ = check_unfinished error name;
+ val _ = check_unfinished name;
val _ = if int then use_thys_dir dir parents else ();
- val theory = Theory.begin_theory name (map get_theory parent_names);
+ val theory =
+ Theory.begin_theory name (map get_theory parent_names)
+ |> Thy_Load.init dir
+ |> fold (Thy_Load.require o fst) uses;
val deps =
if known_thy name then get_deps name
- else init_deps NONE "" parents (map #1 uses);
+ else init_deps NONE "" parents;
val _ = change_thys (new_deps name parent_names (deps, NONE));
val update_time = (case deps of NONE => 0 | SOME {update_time, ...} => update_time);
@@ -527,59 +447,34 @@
val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
val theory'' =
- fold (fn x => Context.theory_map (exec_file x) o Theory.checkpoint) uses_now theory';
+ fold (fn x => Context.theory_map (Thy_Load.exec_ml x) o Theory.checkpoint) uses_now theory';
in theory'' end;
-fun end_theory theory =
- let
- val name = Context.theory_name theory;
- val _ = check_files name;
- val theory' = Theory.end_theory theory;
- val _ = change_thy name (fn (deps, _) => (deps, SOME theory'));
- in () end;
-
(* register existing theories *)
-fun register_thy name =
- let
- val _ = priority ("Registering theory " ^ quote name);
- val thy = get_theory name;
- val _ = map get_theory (get_parents name);
- val _ = check_unfinished error name;
- val _ = touch_thy name;
- val master = #master (Thy_Load.deps_thy Path.current name);
- val upd_time = #2 (Management_Data.get thy);
- in
- CRITICAL (fn () =>
- (change_deps name (Option.map
- (fn {parents, files, ...} => make_deps upd_time (SOME master) "" parents files));
- perform Update name))
- end;
-
-fun register_theory theory =
+fun register_thy theory =
let
val name = Context.theory_name theory;
- val parents = Theory.parents_of theory;
- val parent_names = map Context.theory_name parents;
-
- fun err txt bads =
- error (loader_msg txt bads ^ "\ncannot register theory " ^ quote name);
+ val _ = priority ("Registering theory " ^ quote name);
+ val parent_names = map Context.theory_name (Theory.parents_of theory);
+ val _ = map get_theory parent_names;
- val nonfinished = filter_out is_finished parent_names;
- fun get_variant (x, y_name) =
- if Theory.eq_thy (x, get_theory y_name) then NONE
- else SOME y_name;
- val variants = map_filter get_variant (parents ~~ parent_names);
-
- fun register G =
- (Graph.new_node (name, (NONE, SOME theory)) G
- handle Graph.DUP _ => err "duplicate theory entry" [])
- |> add_deps name parent_names;
+ val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
+ val update_time = #2 (Management_Data.get theory);
+ val parents =
+ (case lookup_deps name of
+ SOME (SOME {parents, ...}) => parents
+ | _ => parent_names);
+ val deps = make_deps update_time (SOME master) "" parents;
in
- if not (null nonfinished) then err "non-finished parent theories" nonfinished
- else if not (null variants) then err "different versions of parent theories" variants
- else CRITICAL (fn () => (change_thys register; perform Update name))
+ CRITICAL (fn () =>
+ (if known_thy name then
+ (List.app remove_thy (thy_graph Graph.imm_succs name);
+ change_thys (Graph.del_nodes [name]))
+ else ();
+ change_thys (new_deps name parents (SOME deps, SOME theory));
+ perform Update name))
end;
--- a/src/Pure/Thy/thy_load.ML Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML Mon Jul 26 18:25:19 2010 +0200
@@ -17,21 +17,65 @@
signature THY_LOAD =
sig
include BASIC_THY_LOAD
- val ml_path: string -> Path.T
- val thy_path: string -> Path.T
- val split_thy_path: Path.T -> Path.T * string
- val consistent_name: string -> string -> unit
+ val master_directory: theory -> Path.T
+ val init: Path.T -> theory -> theory
+ val require: Path.T -> theory -> theory
+ val provide: Path.T * (Path.T * File.ident) -> theory -> theory
val test_file: Path.T -> Path.T -> (Path.T * File.ident) option
val check_file: Path.T -> Path.T -> Path.T * File.ident
val check_thy: Path.T -> string -> Path.T * File.ident
val deps_thy: Path.T -> string ->
{master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
- val load_ml: Path.T -> Path.T -> Path.T * File.ident
+ val loaded_files: theory -> Path.T list
+ val all_current: theory -> bool
+ val provide_file: Path.T -> theory -> theory
+ val use_ml: Path.T -> unit
+ val exec_ml: Path.T -> generic_theory -> generic_theory
end;
structure Thy_Load: THY_LOAD =
struct
+(* manage source files *)
+
+type files =
+ {master_dir: Path.T, (*master directory of theory source*)
+ required: Path.T list, (*source path*)
+ provided: (Path.T * (Path.T * File.ident)) list}; (*source path, physical path, identifier*)
+
+fun make_files (master_dir, required, provided): files =
+ {master_dir = master_dir, required = required, provided = provided};
+
+structure Files = Theory_Data
+(
+ type T = files;
+ val empty = make_files (Path.current, [], []);
+ fun extend _ = empty;
+ fun merge _ = empty;
+);
+
+fun map_files f =
+ Files.map (fn {master_dir, required, provided} =>
+ make_files (f (master_dir, required, provided)));
+
+
+val master_directory = #master_dir o Files.get;
+
+fun init master_dir = map_files (fn _ => (master_dir, [], []));
+
+fun require src_path =
+ map_files (fn (master_dir, required, provided) =>
+ if member (op =) required src_path then
+ error ("Duplicate source file dependency: " ^ Path.implode src_path)
+ else (master_dir, src_path :: required, provided));
+
+fun provide (src_path, path_info) =
+ map_files (fn (master_dir, required, provided) =>
+ if AList.defined (op =) provided src_path then
+ error ("Duplicate resolution of source file dependency: " ^ Path.implode src_path)
+ else (master_dir, required, (src_path, path_info) :: provided));
+
+
(* maintain load path *)
local val load_path = Unsynchronized.ref [Path.current] in
@@ -56,22 +100,6 @@
end;
-(* file formats *)
-
-val ml_path = Path.ext "ML" o Path.basic;
-val thy_path = Path.ext "thy" o Path.basic;
-
-fun split_thy_path path =
- (case Path.split_ext path of
- (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
- | _ => error ("Bad theory file specification " ^ Path.implode path));
-
-fun consistent_name name name' =
- if name = name' then ()
- else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
- " does not agree with theory name " ^ quote name');
-
-
(* check files *)
local
@@ -103,7 +131,7 @@
error ("Could not find file " ^ quote (Path.implode path) ^
"\nin " ^ commas_quote (map Path.implode prfxs));
-fun check_thy dir name = check_file dir (thy_path name);
+fun check_thy dir name = check_file dir (Thy_Header.thy_path name);
end;
@@ -116,18 +144,63 @@
val text = File.read path;
val (name', imports, uses) =
Thy_Header.read (Path.position path) (Source.of_string_limited 8000 text);
- val _ = consistent_name name name';
+ val _ = Thy_Header.consistent_name name name';
val uses = map (Path.explode o #1) uses;
in {master = master, text = text, imports = imports, uses = uses} end;
-(* ML files *)
+
+(* loaded files *)
+
+val loaded_files = map (#1 o #2) o #provided o Files.get;
-fun load_ml dir raw_path =
+fun check_loaded thy =
+ let
+ val {required, provided, ...} = Files.get thy;
+ val provided_paths = map #1 provided;
+ val _ =
+ (case subtract (op =) provided_paths required of
+ [] => NONE
+ | bad => error ("Pending source file dependencies: " ^ commas (map Path.implode (rev bad))));
+ val _ =
+ (case subtract (op =) required provided_paths of
+ [] => NONE
+ | bad => error ("Undeclared source file dependencies: " ^ commas (map Path.implode (rev bad))));
+ in () end;
+
+fun all_current thy =
let
- val (path, id) = check_file dir raw_path;
- val _ = ML_Context.eval_file path;
- in (path, id) end;
+ val {master_dir, provided, ...} = Files.get thy;
+ fun current (src_path, path_info) =
+ (case test_file master_dir src_path of
+ NONE => false
+ | SOME path_info' => eq_snd (op =) (path_info, path_info'));
+ in can check_loaded thy andalso forall current provided end;
+
+val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE))));
+
+
+(* provide files *)
+
+fun provide_file src_path thy =
+ provide (src_path, check_file (master_directory thy) src_path) thy;
+
+fun use_ml src_path =
+ if is_none (Context.thread_data ()) then
+ ML_Context.eval_file (#1 (check_file Path.current src_path))
+ else
+ let
+ val thy = ML_Context.the_global_context ();
+ val (path, info) = check_file (master_directory thy) src_path;
+
+ val _ = ML_Context.eval_file path;
+ val _ = Context.>> Local_Theory.propagate_ml_env;
+
+ val provide = provide (src_path, (path, info));
+ val _ = Context.>> (Context.mapping provide (Local_Theory.theory provide));
+ in () end
+
+fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);
end;
--- a/src/Pure/pure_setup.ML Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Pure/pure_setup.ML Mon Jul 26 18:25:19 2010 +0200
@@ -4,14 +4,16 @@
Pure theory and ML toplevel setup.
*)
-(* the Pure theories *)
+(* the Pure theory *)
Context.>> (Context.map_theory
(Outer_Syntax.process_file (Path.explode "Pure.thy") #>
Theory.end_theory));
+
structure Pure = struct val thy = ML_Context.the_global_context () end;
+
Context.set_thread_data NONE;
-Thy_Info.register_theory Pure.thy;
+Thy_Info.register_thy Pure.thy;
(* ML toplevel pretty printing *)
@@ -51,7 +53,8 @@
(* ML toplevel use commands *)
-fun use name = Toplevel.program (fn () => Thy_Info.use name);
+fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
+
fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
--- a/src/Tools/Code/code_eval.ML Mon Jul 26 14:44:07 2010 +0200
+++ b/src/Tools/Code/code_eval.ML Mon Jul 26 18:25:19 2010 +0200
@@ -173,7 +173,8 @@
end
| process (code_body, _) _ (SOME file_name) thy =
let
- val preamble = "(* Generated from " ^ Path.implode (Thy_Load.thy_path (Context.theory_name thy))
+ val preamble =
+ "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy))
^ "; DO NOT EDIT! *)";
val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code_body);
in