src/HOL/Bali/Term.thy
changeset 37956 ee939247b2fb
parent 35431 8758fe1fc9f8
child 41778 5f79a9e42507
     1.1 --- a/src/HOL/Bali/Term.thy	Mon Jul 26 13:50:52 2010 +0200
     1.2 +++ b/src/HOL/Bali/Term.thy	Mon Jul 26 17:41:26 2010 +0200
     1.3 @@ -258,8 +258,9 @@
     1.4    StatRef :: "ref_ty \<Rightarrow> expr"
     1.5    where "StatRef rt == Cast (RefT rt) (Lit Null)"
     1.6    
     1.7 -definition is_stmt :: "term \<Rightarrow> bool" where
     1.8 - "is_stmt t \<equiv> \<exists>c. t=In1r c"
     1.9 +definition
    1.10 +  is_stmt :: "term \<Rightarrow> bool"
    1.11 +  where "is_stmt t = (\<exists>c. t=In1r c)"
    1.12  
    1.13  ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def}) *}
    1.14  
    1.15 @@ -307,7 +308,7 @@
    1.16  begin
    1.17  
    1.18  definition
    1.19 -  stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
    1.20 +  stmt_inj_term_def: "\<langle>c::stmt\<rangle> = In1r c"
    1.21  
    1.22  instance ..
    1.23  
    1.24 @@ -323,7 +324,7 @@
    1.25  begin
    1.26  
    1.27  definition
    1.28 -  expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
    1.29 +  expr_inj_term_def: "\<langle>e::expr\<rangle> = In1l e"
    1.30  
    1.31  instance ..
    1.32  
    1.33 @@ -339,7 +340,7 @@
    1.34  begin
    1.35  
    1.36  definition
    1.37 -  var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
    1.38 +  var_inj_term_def: "\<langle>v::var\<rangle> = In2 v"
    1.39  
    1.40  instance ..
    1.41  
    1.42 @@ -368,7 +369,7 @@
    1.43  begin
    1.44  
    1.45  definition
    1.46 -  "\<langle>es::'a list\<rangle> \<equiv> In3 (map expr_of es)"
    1.47 +  "\<langle>es::'a list\<rangle> = In3 (map expr_of es)"
    1.48  
    1.49  instance ..
    1.50  
    1.51 @@ -425,46 +426,47 @@
    1.52    done
    1.53  
    1.54  section {* Evaluation of unary operations *}
    1.55 -consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
    1.56 -primrec
    1.57 -"eval_unop UPlus   v = Intg (the_Intg v)"
    1.58 -"eval_unop UMinus  v = Intg (- (the_Intg v))"
    1.59 -"eval_unop UBitNot v = Intg 42"                -- "FIXME: Not yet implemented"
    1.60 -"eval_unop UNot    v = Bool (\<not> the_Bool v)"
    1.61 +primrec eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
    1.62 +where
    1.63 +  "eval_unop UPlus v = Intg (the_Intg v)"
    1.64 +| "eval_unop UMinus v = Intg (- (the_Intg v))"
    1.65 +| "eval_unop UBitNot v = Intg 42"                -- "FIXME: Not yet implemented"
    1.66 +| "eval_unop UNot v = Bool (\<not> the_Bool v)"
    1.67  
    1.68  section {* Evaluation of binary operations *}
    1.69 -consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
    1.70 -primrec
    1.71 -"eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
    1.72 -"eval_binop Div     v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
    1.73 -"eval_binop Mod     v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
    1.74 -"eval_binop Plus    v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
    1.75 -"eval_binop Minus   v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
    1.76 +primrec eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
    1.77 +where
    1.78 +  "eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
    1.79 +| "eval_binop Div     v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
    1.80 +| "eval_binop Mod     v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
    1.81 +| "eval_binop Plus    v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
    1.82 +| "eval_binop Minus   v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
    1.83  
    1.84  -- "Be aware of the explicit coercion of the shift distance to nat"
    1.85 -"eval_binop LShift  v1 v2 = Intg ((the_Intg v1) *   (2^(nat (the_Intg v2))))"
    1.86 -"eval_binop RShift  v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
    1.87 -"eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
    1.88 +| "eval_binop LShift  v1 v2 = Intg ((the_Intg v1) *   (2^(nat (the_Intg v2))))"
    1.89 +| "eval_binop RShift  v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
    1.90 +| "eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
    1.91  
    1.92 -"eval_binop Less    v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
    1.93 -"eval_binop Le      v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
    1.94 -"eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
    1.95 -"eval_binop Ge      v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
    1.96 +| "eval_binop Less    v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
    1.97 +| "eval_binop Le      v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
    1.98 +| "eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
    1.99 +| "eval_binop Ge      v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
   1.100  
   1.101 -"eval_binop Eq      v1 v2 = Bool (v1=v2)"
   1.102 -"eval_binop Neq     v1 v2 = Bool (v1\<noteq>v2)"
   1.103 -"eval_binop BitAnd  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
   1.104 -"eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
   1.105 -"eval_binop BitXor  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
   1.106 -"eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
   1.107 -"eval_binop BitOr   v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
   1.108 -"eval_binop Or      v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
   1.109 -"eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
   1.110 -"eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
   1.111 +| "eval_binop Eq      v1 v2 = Bool (v1=v2)"
   1.112 +| "eval_binop Neq     v1 v2 = Bool (v1\<noteq>v2)"
   1.113 +| "eval_binop BitAnd  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
   1.114 +| "eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
   1.115 +| "eval_binop BitXor  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
   1.116 +| "eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
   1.117 +| "eval_binop BitOr   v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
   1.118 +| "eval_binop Or      v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
   1.119 +| "eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
   1.120 +| "eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
   1.121  
   1.122 -definition need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool" where
   1.123 -"need_second_arg binop v1 \<equiv> \<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
   1.124 -                               (binop=CondOr  \<and> the_Bool v1))"
   1.125 +definition
   1.126 +  need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool" where
   1.127 +  "need_second_arg binop v1 = (\<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
   1.128 +                                 (binop=CondOr  \<and> the_Bool v1)))"
   1.129  text {* @{term CondAnd} and @{term CondOr} only evalulate the second argument
   1.130   if the value isn't already determined by the first argument*}
   1.131