--- a/src/HOL/Bali/Term.thy Wed Oct 30 12:44:18 2002 +0100
+++ b/src/HOL/Bali/Term.thy Thu Oct 31 18:27:10 2002 +0100
@@ -30,7 +30,6 @@
simplifications:
\begin{itemize}
\item expression statement allowed for any expression
-\item no unary, binary, etc, operators
\item This is modeled as a special non-assignable local variable
\item Super is modeled as a general expression with the same value as This
\item access to field x in current class via This.x
@@ -73,7 +72,8 @@
| Std xname --{* intermediate standard exception, see Eval.thy *}
datatype error
- = AccessViolation --{* Access to a member that isn't permitted *}
+ = AccessViolation --{* Access to a member that isn't permitted *}
+ | CrossMethodJump --{* Method exits with a break or continue *}
datatype abrupt --{* abrupt completion *}
= Xcpt xcpt --{* exception *}
@@ -206,7 +206,7 @@
| Comp stmt stmt ("_;; _" [ 66,65]65)
| If_ expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70)
| Loop label expr stmt ("_\<bullet> While'(_') _" [ 99,80,79]70)
- | Do jump --{* break, continue, return *}
+ | Jmp jump --{* break, continue, return *}
| Throw expr
| TryC stmt qtname vname stmt ("Try _ Catch'(_ _') _" [79,99,80,79]70)
--{* @{term "Try c1 Catch(C vn) c2"} *}
@@ -258,8 +258,8 @@
"this" == "Acc (LVar This)"
"!!v" == "Acc (LVar (EName (VNam v)))"
"v:==e" == "Expr (Ass (LVar (EName (VNam v))) e)"
- "Return e" == "Expr (Ass (LVar (EName Res)) e);; Do Ret"
- --{* \tt Res := e;; Do Ret *}
+ "Return e" == "Expr (Ass (LVar (EName Res)) e);; Jmp Ret"
+ --{* \tt Res := e;; Jmp Ret *}
"StatRef rt" == "Cast (RefT rt) (Lit Null)"
constdefs
@@ -273,8 +273,39 @@
declare is_stmt_rews [simp]
+text {*
+ Here is some syntactic stuff to handle the injections of statements,
+ expressions, variables and expression lists into general terms.
+*}
+
+syntax
+ expr_inj_term:: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 1000)
+ stmt_inj_term:: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 1000)
+ var_inj_term:: "var \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>v" 1000)
+ lst_inj_term:: "expr list \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>l" 1000)
+
+translations
+ "\<langle>e\<rangle>\<^sub>e" \<rightharpoonup> "In1l e"
+ "\<langle>c\<rangle>\<^sub>s" \<rightharpoonup> "In1r c"
+ "\<langle>v\<rangle>\<^sub>v" \<rightharpoonup> "In2 v"
+ "\<langle>es\<rangle>\<^sub>l" \<rightharpoonup> "In3 es"
+
+text {* It seems to be more elegant to have an overloaded injection like the
+following.
+*}
+
axclass inj_term < "type"
-consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 83)
+consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 1000)
+
+text {* How this overloaded injections work can be seen in the theory
+@{text DefiniteAssignment}. Other big inductive relations on
+terms defined in theories @{text WellType}, @{text Eval}, @{text Evaln} and
+@{text AxSem} don't follow this convention right now, but introduce subtle
+syntactic sugar in the relations themselves to make a distinction on
+expressions, statements and so on. So unfortunately you will encounter a
+mixture of dealing with these injections. The translations above are used
+as bridge between the different conventions.
+*}
instance stmt::inj_term ..
@@ -284,6 +315,9 @@
lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
by (simp add: stmt_inj_term_def)
+lemma stmt_inj_term [iff]: "\<langle>x::stmt\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
+ by (simp add: stmt_inj_term_simp)
+
instance expr::inj_term ..
defs (overloaded)
@@ -292,6 +326,9 @@
lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
by (simp add: expr_inj_term_def)
+lemma expr_inj_term [iff]: "\<langle>x::expr\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
+ by (simp add: expr_inj_term_simp)
+
instance var::inj_term ..
defs (overloaded)
@@ -300,6 +337,9 @@
lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
by (simp add: var_inj_term_def)
+lemma var_inj_term [iff]: "\<langle>x::var\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
+ by (simp add: var_inj_term_simp)
+
instance "list":: (type) inj_term ..
defs (overloaded)
@@ -308,4 +348,93 @@
lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
by (simp add: expr_list_inj_term_def)
+lemma expr_list_inj_term [iff]: "\<langle>x::expr list\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
+ by (simp add: expr_list_inj_term_simp)
+
+lemmas inj_term_simps = stmt_inj_term_simp expr_inj_term_simp var_inj_term_simp
+ expr_list_inj_term_simp
+lemmas inj_term_sym_simps = stmt_inj_term_simp [THEN sym]
+ expr_inj_term_simp [THEN sym]
+ var_inj_term_simp [THEN sym]
+ expr_list_inj_term_simp [THEN sym]
+
+lemma stmt_expr_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::expr\<rangle>"
+ by (simp add: inj_term_simps)
+lemma expr_stmt_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
+ by (simp add: inj_term_simps)
+lemma stmt_var_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::var\<rangle>"
+ by (simp add: inj_term_simps)
+lemma var_stmt_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
+ by (simp add: inj_term_simps)
+lemma stmt_elist_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
+ by (simp add: inj_term_simps)
+lemma elist_stmt_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
+ by (simp add: inj_term_simps)
+lemma expr_var_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::var\<rangle>"
+ by (simp add: inj_term_simps)
+lemma var_expr_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::expr\<rangle>"
+ by (simp add: inj_term_simps)
+lemma expr_elist_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
+ by (simp add: inj_term_simps)
+lemma elist_expr_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::expr\<rangle>"
+ by (simp add: inj_term_simps)
+lemma var_elist_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
+ by (simp add: inj_term_simps)
+lemma elist_var_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::var\<rangle>"
+ by (simp add: inj_term_simps)
+
+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)"
+
+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))"
+
+-- "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 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))"
+
+constdefs need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool"
+"need_second_arg binop v1 \<equiv> \<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*}
+
+lemma need_second_arg_CondAnd [simp]: "need_second_arg CondAnd (Bool b) = b"
+by (simp add: need_second_arg_def)
+
+lemma need_second_arg_CondOr [simp]: "need_second_arg CondOr (Bool b) = (\<not> b)"
+by (simp add: need_second_arg_def)
+
+lemma need_second_arg_strict[simp]:
+ "\<lbrakk>binop\<noteq>CondAnd; binop\<noteq>CondOr\<rbrakk> \<Longrightarrow> need_second_arg binop b"
+by (cases binop)
+ (simp_all add: need_second_arg_def)
end
\ No newline at end of file