# HG changeset patch
# User berghofe
# Date 909140136 -7200
# Node ID 31fc1d0e66d579a6199720402e8c3f99c371b5e9
# Parent  8a1be8e50d9fa3b3bfd3e4bc65c31e638d76fdbc
New example for using the datatype package:
Arithmetic and boolean expressions.

diff -r 8a1be8e50d9f -r 31fc1d0e66d5 src/HOL/Induct/ABexp.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/ABexp.ML	Fri Oct 23 12:55:36 1998 +0200
@@ -0,0 +1,16 @@
+(*  Title:      HOL/Induct/ABexp.ML
+    ID:         $Id$
+    Author:     Stefan Berghofer, TU Muenchen
+    Copyright   1998  TU Muenchen
+
+Arithmetic and boolean expressions
+*)
+
+(** substitution theorem for arithmetic and boolean expressions **)
+
+Goal
+  "eval_aexp env (subst_aexp (Var(v := a')) a) = eval_aexp (env(v := eval_aexp env a')) a &  \
+ \ eval_bexp env (subst_bexp (Var(v := a')) b) = eval_bexp (env(v := eval_aexp env a')) b";
+by (mutual_induct_tac ["a","b"] 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed "subst_aexp_bexp";
diff -r 8a1be8e50d9f -r 31fc1d0e66d5 src/HOL/Induct/ABexp.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/ABexp.thy	Fri Oct 23 12:55:36 1998 +0200
@@ -0,0 +1,60 @@
+(*  Title:      HOL/Induct/ABexp.thy
+    ID:         $Id$
+    Author:     Stefan Berghofer, TU Muenchen
+    Copyright   1998  TU Muenchen
+
+Arithmetic and boolean expressions
+*)
+
+ABexp = Main +
+
+datatype
+  'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp)
+          | Sum ('a aexp) ('a aexp)
+          | Diff ('a aexp) ('a aexp)
+          | Var 'a
+          | Num nat
+and
+  'a bexp = Less ('a aexp) ('a aexp)
+          | And ('a bexp) ('a bexp)
+          | Or ('a bexp) ('a bexp)
+
+
+(** evaluation of arithmetic and boolean expressions **)
+
+consts
+  eval_aexp :: "['a => nat, 'a aexp] => nat"
+  eval_bexp :: "['a => nat, 'a bexp] => bool"
+
+primrec
+  "eval_aexp env (If_then_else b a1 a2) =
+     (if eval_bexp env b then eval_aexp env a1 else eval_aexp env a2)"
+  "eval_aexp env (Sum a1 a2) = eval_aexp env a1 + eval_aexp env a2"
+  "eval_aexp env (Diff a1 a2) = eval_aexp env a1 - eval_aexp env a2"
+  "eval_aexp env (Var v) = env v"
+  "eval_aexp env (Num n) = n"
+
+  "eval_bexp env (Less a1 a2) = (eval_aexp env a1 < eval_aexp env a2)"
+  "eval_bexp env (And b1 b2) = (eval_bexp env b1 & eval_bexp env b2)"
+  "eval_bexp env (Or b1 b2) = (eval_bexp env b1 & eval_bexp env b2)"
+
+
+(** substitution on arithmetic and boolean expressions **)
+
+consts
+  subst_aexp :: "['a => 'b aexp, 'a aexp] => 'b aexp"
+  subst_bexp :: "['a => 'b aexp, 'a bexp] => 'b bexp"
+
+primrec
+  "subst_aexp f (If_then_else b a1 a2) =
+     If_then_else (subst_bexp f b) (subst_aexp f a1) (subst_aexp f a2)"
+  "subst_aexp f (Sum a1 a2) = Sum (subst_aexp f a1) (subst_aexp f a2)"
+  "subst_aexp f (Diff a1 a2) = Diff (subst_aexp f a1) (subst_aexp f a2)"
+  "subst_aexp f (Var v) = f v"
+  "subst_aexp f (Num n) = Num n"
+
+  "subst_bexp f (Less a1 a2) = Less (subst_aexp f a1) (subst_aexp f a2)"
+  "subst_bexp f (And b1 b2) = And (subst_bexp f b1) (subst_bexp f b2)"
+  "subst_bexp f (Or b1 b2) = Or (subst_bexp f b1) (subst_bexp f b2)"
+
+end