Fixed markup error in comment.
authorschirmer
Thu Jul 11 09:36:41 2002 +0200 (2002-07-11)
changeset 13345bd611943cbc2
parent 13344 c8eb3fbf4c0c
child 13346 6918b6d5192b
Fixed markup error in comment.
src/HOL/Bali/Term.thy
     1.1 --- a/src/HOL/Bali/Term.thy	Thu Jul 11 09:31:01 2002 +0200
     1.2 +++ b/src/HOL/Bali/Term.thy	Thu Jul 11 09:36:41 2002 +0200
     1.3 @@ -106,33 +106,37 @@
     1.4    "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
     1.5  
     1.6  -- "function codes for unary operations"
     1.7 -datatype unop =  UPlus    -- "+ unary plus" 
     1.8 -               | UMinus   -- "- unary minus"
     1.9 -               | UBitNot  -- "~ bitwise NOT"
    1.10 -               | UNot     -- "! logical complement"
    1.11 +datatype unop =  UPlus    -- {*{\tt +} unary plus*} 
    1.12 +               | UMinus   -- {*{\tt -} unary minus*}
    1.13 +               | UBitNot  -- {*{\tt ~} bitwise NOT*}
    1.14 +               | UNot     -- {*{\tt !} logical complement*}
    1.15  
    1.16  -- "function codes for binary operations"
    1.17 -datatype binop = Mul     -- "*   multiplication"
    1.18 -               | Div     -- "/   division"
    1.19 -               | Mod     -- "%   remainder"
    1.20 -               | Plus    -- "+   addition"
    1.21 -               | Minus   -- "-   subtraction"
    1.22 -               | LShift  -- "<<  left shift"
    1.23 -               | RShift  -- ">>  signed right shift"
    1.24 -               | RShiftU -- ">>> unsigned right shift"
    1.25 -               | Less    -- "<   less than"
    1.26 -               | Le      -- "<=  less than or equal"
    1.27 -               | Greater -- ">   greater than"
    1.28 -               | Ge      -- ">=  greater than or equal"
    1.29 -               | Eq      -- "==  equal"
    1.30 -               | Neq     -- "!=  not equal"
    1.31 -               | BitAnd  -- "&   bitwise AND"
    1.32 -               | And     -- "&   boolean AND"
    1.33 -               | BitXor  -- "^   bitwise Xor"
    1.34 -               | Xor     -- "^   boolean Xor"
    1.35 -               | BitOr   -- "|   bitwise Or"
    1.36 -               | Or      -- "|   boolean Or"
    1.37 -
    1.38 +datatype binop = Mul     -- {*{\tt * }   multiplication*}
    1.39 +               | Div     -- {*{\tt /}   division*}
    1.40 +               | Mod     -- {*{\tt %}   remainder*}
    1.41 +               | Plus    -- {*{\tt +}   addition*}
    1.42 +               | Minus   -- {*{\tt -}   subtraction*}
    1.43 +               | LShift  -- {*{\tt <<}  left shift*}
    1.44 +               | RShift  -- {*{\tt >>}  signed right shift*}
    1.45 +               | RShiftU -- {*{\tt >>>} unsigned right shift*}
    1.46 +               | Less    -- {*{\tt <}   less than*}
    1.47 +               | Le      -- {*{\tt <=}  less than or equal*}
    1.48 +               | Greater -- {*{\tt >}   greater than*}
    1.49 +               | Ge      -- {*{\tt >=}  greater than or equal*}
    1.50 +               | Eq      -- {*{\tt ==}  equal*}
    1.51 +               | Neq     -- {*{\tt !=}  not equal*}
    1.52 +               | BitAnd  -- {*{\tt &}   bitwise AND*}
    1.53 +               | And     -- {*{\tt &}   boolean AND*}
    1.54 +               | BitXor  -- {*{\tt ^}   bitwise Xor*}
    1.55 +               | Xor     -- {*{\tt ^}   boolean Xor*}
    1.56 +               | BitOr   -- {*{\tt |}   bitwise Or*}
    1.57 +               | Or      -- {*{\tt |}   boolean Or*}
    1.58 +text{* The boolean operators {\tt &} and {\tt |} strictly evaluate both
    1.59 +of their arguments. The lazy operators {\tt &&} and {\tt ||} are modeled
    1.60 +as instances of the @{text Cond} expression: {\tt a && b = a?b:false} and
    1.61 +  {\tt a || b = a?true:b}
    1.62 +*}
    1.63  datatype var
    1.64  	= LVar                  lname(* local variable (incl. parameters) *)
    1.65          | FVar qtname qtname bool expr vname
    1.66 @@ -233,4 +237,40 @@
    1.67  *}
    1.68  
    1.69  declare is_stmt_rews [simp]
    1.70 +
    1.71 +axclass inj_term < "type"
    1.72 +consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 83)
    1.73 +
    1.74 +instance stmt::inj_term ..
    1.75 +
    1.76 +defs (overloaded)
    1.77 +stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
    1.78 +
    1.79 +lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
    1.80 +by (simp add: stmt_inj_term_def)
    1.81 +
    1.82 +instance expr::inj_term ..
    1.83 +
    1.84 +defs (overloaded)
    1.85 +expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
    1.86 +
    1.87 +lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
    1.88 +by (simp add: expr_inj_term_def)
    1.89 +
    1.90 +instance var::inj_term ..
    1.91 +
    1.92 +defs (overloaded)
    1.93 +var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
    1.94 +
    1.95 +lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
    1.96 +by (simp add: var_inj_term_def)
    1.97 +
    1.98 +instance "list":: (type) inj_term ..
    1.99 +
   1.100 +defs (overloaded)
   1.101 +expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
   1.102 +
   1.103 +lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
   1.104 +by (simp add: expr_list_inj_term_def)
   1.105 +
   1.106  end
   1.107 \ No newline at end of file