src/HOL/Bali/Term.thy
changeset 13688 a0b16d42d489
parent 13384 a34e38154413
child 13690 ac335b2f4a39
     1.1 --- a/src/HOL/Bali/Term.thy	Wed Oct 30 12:44:18 2002 +0100
     1.2 +++ b/src/HOL/Bali/Term.thy	Thu Oct 31 18:27:10 2002 +0100
     1.3 @@ -30,7 +30,6 @@
     1.4  simplifications:
     1.5  \begin{itemize}
     1.6  \item expression statement allowed for any expression
     1.7 -\item no unary, binary, etc, operators
     1.8  \item This  is modeled as a special non-assignable local variable
     1.9  \item Super is modeled as a general expression with the same value as This
    1.10  \item access to field x in current class via This.x
    1.11 @@ -73,7 +72,8 @@
    1.12  	| Std xname  --{* intermediate standard exception, see Eval.thy *}
    1.13  
    1.14  datatype error
    1.15 -       = AccessViolation --{* Access to a member that isn't permitted *}
    1.16 +       =  AccessViolation  --{* Access to a member that isn't permitted *}
    1.17 +        | CrossMethodJump  --{* Method exits with a break or continue *}
    1.18  
    1.19  datatype abrupt       --{* abrupt completion *} 
    1.20          = Xcpt xcpt   --{* exception *}
    1.21 @@ -206,7 +206,7 @@
    1.22  	| Comp  stmt stmt       ("_;; _"                  [      66,65]65)
    1.23  	| If_   expr stmt stmt  ("If'(_') _ Else _"       [   80,79,79]70)
    1.24  	| Loop  label expr stmt ("_\<bullet> While'(_') _"        [   99,80,79]70)
    1.25 -        | Do jump               --{* break, continue, return *}
    1.26 +        | Jmp jump              --{* break, continue, return *}
    1.27  	| Throw expr
    1.28          | TryC  stmt qtname vname stmt ("Try _ Catch'(_ _') _"  [79,99,80,79]70)
    1.29               --{* @{term "Try c1 Catch(C vn) c2"} *} 
    1.30 @@ -258,8 +258,8 @@
    1.31   "this"       == "Acc (LVar This)"
    1.32   "!!v"        == "Acc (LVar (EName (VNam v)))"
    1.33   "v:==e"      == "Expr (Ass (LVar (EName (VNam  v))) e)"
    1.34 - "Return e"   == "Expr (Ass (LVar (EName Res)) e);; Do Ret" 
    1.35 -                  --{* \tt Res := e;; Do Ret *}
    1.36 + "Return e"   == "Expr (Ass (LVar (EName Res)) e);; Jmp Ret" 
    1.37 +                  --{* \tt Res := e;; Jmp Ret *}
    1.38   "StatRef rt" == "Cast (RefT rt) (Lit Null)"
    1.39    
    1.40  constdefs
    1.41 @@ -273,8 +273,39 @@
    1.42  
    1.43  declare is_stmt_rews [simp]
    1.44  
    1.45 +text {*
    1.46 +  Here is some syntactic stuff to handle the injections of statements,
    1.47 +  expressions, variables and expression lists into general terms.
    1.48 +*}
    1.49 +
    1.50 +syntax 
    1.51 +  expr_inj_term:: "expr \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>e" 1000)
    1.52 +  stmt_inj_term:: "stmt \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>s" 1000)
    1.53 +  var_inj_term::  "var \<Rightarrow> term"  ("\<langle>_\<rangle>\<^sub>v" 1000)
    1.54 +  lst_inj_term:: "expr list \<Rightarrow> term" ("\<langle>_\<rangle>\<^sub>l" 1000)
    1.55 +
    1.56 +translations 
    1.57 +  "\<langle>e\<rangle>\<^sub>e" \<rightharpoonup> "In1l e"
    1.58 +  "\<langle>c\<rangle>\<^sub>s" \<rightharpoonup> "In1r c"
    1.59 +  "\<langle>v\<rangle>\<^sub>v" \<rightharpoonup> "In2 v"
    1.60 +  "\<langle>es\<rangle>\<^sub>l" \<rightharpoonup> "In3 es"
    1.61 +
    1.62 +text {* It seems to be more elegant to have an overloaded injection like the
    1.63 +following.
    1.64 +*}
    1.65 +
    1.66  axclass inj_term < "type"
    1.67 -consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 83)
    1.68 +consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 1000)
    1.69 +
    1.70 +text {* How this overloaded injections work can be seen in the theory 
    1.71 +@{text DefiniteAssignment}. Other big inductive relations on
    1.72 +terms defined in theories @{text WellType}, @{text Eval}, @{text Evaln} and
    1.73 +@{text AxSem} don't follow this convention right now, but introduce subtle 
    1.74 +syntactic sugar in the relations themselves to make a distinction on 
    1.75 +expressions, statements and so on. So unfortunately you will encounter a 
    1.76 +mixture of dealing with these injections. The translations above are used
    1.77 +as bridge between the different conventions.  
    1.78 +*}
    1.79  
    1.80  instance stmt::inj_term ..
    1.81  
    1.82 @@ -284,6 +315,9 @@
    1.83  lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
    1.84  by (simp add: stmt_inj_term_def)
    1.85  
    1.86 +lemma  stmt_inj_term [iff]: "\<langle>x::stmt\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
    1.87 +  by (simp add: stmt_inj_term_simp)
    1.88 +
    1.89  instance expr::inj_term ..
    1.90  
    1.91  defs (overloaded)
    1.92 @@ -292,6 +326,9 @@
    1.93  lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
    1.94  by (simp add: expr_inj_term_def)
    1.95  
    1.96 +lemma expr_inj_term [iff]: "\<langle>x::expr\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
    1.97 +  by (simp add: expr_inj_term_simp)
    1.98 +
    1.99  instance var::inj_term ..
   1.100  
   1.101  defs (overloaded)
   1.102 @@ -300,6 +337,9 @@
   1.103  lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
   1.104  by (simp add: var_inj_term_def)
   1.105  
   1.106 +lemma var_inj_term [iff]: "\<langle>x::var\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
   1.107 +  by (simp add: var_inj_term_simp)
   1.108 +
   1.109  instance "list":: (type) inj_term ..
   1.110  
   1.111  defs (overloaded)
   1.112 @@ -308,4 +348,93 @@
   1.113  lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
   1.114  by (simp add: expr_list_inj_term_def)
   1.115  
   1.116 +lemma expr_list_inj_term [iff]: "\<langle>x::expr list\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
   1.117 +  by (simp add: expr_list_inj_term_simp)
   1.118 +
   1.119 +lemmas inj_term_simps = stmt_inj_term_simp expr_inj_term_simp var_inj_term_simp
   1.120 +                        expr_list_inj_term_simp
   1.121 +lemmas inj_term_sym_simps = stmt_inj_term_simp [THEN sym] 
   1.122 +                            expr_inj_term_simp [THEN sym]
   1.123 +                            var_inj_term_simp [THEN sym]
   1.124 +                            expr_list_inj_term_simp [THEN sym]
   1.125 +
   1.126 +lemma stmt_expr_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::expr\<rangle>"
   1.127 +  by (simp add: inj_term_simps)
   1.128 +lemma expr_stmt_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
   1.129 +  by (simp add: inj_term_simps)
   1.130 +lemma stmt_var_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::var\<rangle>"
   1.131 +  by (simp add: inj_term_simps)
   1.132 +lemma var_stmt_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
   1.133 +  by (simp add: inj_term_simps)
   1.134 +lemma stmt_elist_inj_term [iff]: "\<langle>t::stmt\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
   1.135 +  by (simp add: inj_term_simps)
   1.136 +lemma elist_stmt_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::stmt\<rangle>"
   1.137 +  by (simp add: inj_term_simps)
   1.138 +lemma expr_var_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::var\<rangle>"
   1.139 +  by (simp add: inj_term_simps)
   1.140 +lemma var_expr_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::expr\<rangle>"
   1.141 +  by (simp add: inj_term_simps)
   1.142 +lemma expr_elist_inj_term [iff]: "\<langle>t::expr\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
   1.143 +  by (simp add: inj_term_simps)
   1.144 +lemma elist_expr_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::expr\<rangle>"
   1.145 +  by (simp add: inj_term_simps)
   1.146 +lemma var_elist_inj_term [iff]: "\<langle>t::var\<rangle> \<noteq> \<langle>w::expr list\<rangle>"
   1.147 +  by (simp add: inj_term_simps)
   1.148 +lemma elist_var_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::var\<rangle>"
   1.149 +  by (simp add: inj_term_simps)
   1.150 +
   1.151 +section {* Evaluation of unary operations *}
   1.152 +consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
   1.153 +primrec
   1.154 +"eval_unop UPlus   v = Intg (the_Intg v)"
   1.155 +"eval_unop UMinus  v = Intg (- (the_Intg v))"
   1.156 +"eval_unop UBitNot v = Intg 42"                -- "FIXME: Not yet implemented"
   1.157 +"eval_unop UNot    v = Bool (\<not> the_Bool v)"
   1.158 +
   1.159 +section {* Evaluation of binary operations *}
   1.160 +consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
   1.161 +primrec
   1.162 +"eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
   1.163 +"eval_binop Div     v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
   1.164 +"eval_binop Mod     v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
   1.165 +"eval_binop Plus    v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
   1.166 +"eval_binop Minus   v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
   1.167 +
   1.168 +-- "Be aware of the explicit coercion of the shift distance to nat"
   1.169 +"eval_binop LShift  v1 v2 = Intg ((the_Intg v1) *   (2^(nat (the_Intg v2))))"
   1.170 +"eval_binop RShift  v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
   1.171 +"eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
   1.172 +
   1.173 +"eval_binop Less    v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
   1.174 +"eval_binop Le      v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
   1.175 +"eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
   1.176 +"eval_binop Ge      v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
   1.177 +
   1.178 +"eval_binop Eq      v1 v2 = Bool (v1=v2)"
   1.179 +"eval_binop Neq     v1 v2 = Bool (v1\<noteq>v2)"
   1.180 +"eval_binop BitAnd  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
   1.181 +"eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
   1.182 +"eval_binop BitXor  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
   1.183 +"eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
   1.184 +"eval_binop BitOr   v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
   1.185 +"eval_binop Or      v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
   1.186 +"eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
   1.187 +"eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
   1.188 +
   1.189 +constdefs need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool"
   1.190 +"need_second_arg binop v1 \<equiv> \<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
   1.191 +                               (binop=CondOr  \<and> the_Bool v1))"
   1.192 +text {* @{term CondAnd} and @{term CondOr} only evalulate the second argument
   1.193 + if the value isn't already determined by the first argument*}
   1.194 +
   1.195 +lemma need_second_arg_CondAnd [simp]: "need_second_arg CondAnd (Bool b) = b" 
   1.196 +by (simp add: need_second_arg_def)
   1.197 +
   1.198 +lemma need_second_arg_CondOr [simp]: "need_second_arg CondOr (Bool b) = (\<not> b)" 
   1.199 +by (simp add: need_second_arg_def)
   1.200 +
   1.201 +lemma need_second_arg_strict[simp]: 
   1.202 + "\<lbrakk>binop\<noteq>CondAnd; binop\<noteq>CondOr\<rbrakk> \<Longrightarrow> need_second_arg binop b"
   1.203 +by (cases binop) 
   1.204 +   (simp_all add: need_second_arg_def)
   1.205  end
   1.206 \ No newline at end of file