src/HOL/Induct/ABexp.thy
author berghofe
Fri, 23 Oct 1998 12:55:36 +0200
changeset 5737 31fc1d0e66d5
child 5802 614f2f30781a
permissions -rw-r--r--
New example for using the datatype package: Arithmetic and boolean expressions.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5737
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/Induct/ABexp.thy
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
     2
    ID:         $Id$
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
     3
    Author:     Stefan Berghofer, TU Muenchen
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
     4
    Copyright   1998  TU Muenchen
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
     5
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
     6
Arithmetic and boolean expressions
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
     7
*)
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
     8
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
     9
ABexp = Main +
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    10
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    11
datatype
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    12
  'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp)
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    13
          | Sum ('a aexp) ('a aexp)
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    14
          | Diff ('a aexp) ('a aexp)
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    15
          | Var 'a
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    16
          | Num nat
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    17
and
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    18
  'a bexp = Less ('a aexp) ('a aexp)
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    19
          | And ('a bexp) ('a bexp)
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    20
          | Or ('a bexp) ('a bexp)
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    21
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    22
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    23
(** evaluation of arithmetic and boolean expressions **)
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    24
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    25
consts
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    26
  eval_aexp :: "['a => nat, 'a aexp] => nat"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    27
  eval_bexp :: "['a => nat, 'a bexp] => bool"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    28
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    29
primrec
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    30
  "eval_aexp env (If_then_else b a1 a2) =
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    31
     (if eval_bexp env b then eval_aexp env a1 else eval_aexp env a2)"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    32
  "eval_aexp env (Sum a1 a2) = eval_aexp env a1 + eval_aexp env a2"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    33
  "eval_aexp env (Diff a1 a2) = eval_aexp env a1 - eval_aexp env a2"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    34
  "eval_aexp env (Var v) = env v"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    35
  "eval_aexp env (Num n) = n"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    36
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    37
  "eval_bexp env (Less a1 a2) = (eval_aexp env a1 < eval_aexp env a2)"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    38
  "eval_bexp env (And b1 b2) = (eval_bexp env b1 & eval_bexp env b2)"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    39
  "eval_bexp env (Or b1 b2) = (eval_bexp env b1 & eval_bexp env b2)"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    40
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    41
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    42
(** substitution on arithmetic and boolean expressions **)
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    43
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    44
consts
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    45
  subst_aexp :: "['a => 'b aexp, 'a aexp] => 'b aexp"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    46
  subst_bexp :: "['a => 'b aexp, 'a bexp] => 'b bexp"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    47
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    48
primrec
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    49
  "subst_aexp f (If_then_else b a1 a2) =
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    50
     If_then_else (subst_bexp f b) (subst_aexp f a1) (subst_aexp f a2)"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    51
  "subst_aexp f (Sum a1 a2) = Sum (subst_aexp f a1) (subst_aexp f a2)"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    52
  "subst_aexp f (Diff a1 a2) = Diff (subst_aexp f a1) (subst_aexp f a2)"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    53
  "subst_aexp f (Var v) = f v"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    54
  "subst_aexp f (Num n) = Num n"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    55
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    56
  "subst_bexp f (Less a1 a2) = Less (subst_aexp f a1) (subst_aexp f a2)"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    57
  "subst_bexp f (And b1 b2) = And (subst_bexp f b1) (subst_bexp f b2)"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    58
  "subst_bexp f (Or b1 b2) = Or (subst_bexp f b1) (subst_bexp f b2)"
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    59
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    60
end