src/HOL/Induct/ABexp.thy
author wenzelm
Sat, 03 Feb 2001 17:40:16 +0100
changeset 11046 b5f5942781a0
parent 5802 614f2f30781a
child 11649 dfb59b9954a6
permissions -rw-r--r--
Induct: converted some theories to new-style format;
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
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
     7
header {* Arithmetic and boolean expressions *}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
     8
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
     9
theory ABexp = Main:
5737
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    10
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    11
datatype 'a aexp =
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    12
    IF "'a bexp"  "'a aexp"  "'a aexp"
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    13
  | Sum "'a aexp"  "'a aexp"
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    14
  | Diff "'a aexp"  "'a aexp"
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    15
  | Var 'a
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    16
  | Num nat
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    17
and 'a bexp =
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    18
    Less "'a aexp"  "'a aexp"
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    19
  | And "'a bexp"  "'a bexp"
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    20
  | Neg "'a bexp"
5737
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
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    23
text {* \medskip Evaluation of arithmetic and boolean expressions *}
5737
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
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    26
  evala :: "('a => nat) => 'a aexp => nat"
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    27
  evalb :: "('a => nat) => 'a bexp => bool"
5737
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
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    30
  "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
5802
614f2f30781a Shortened names and added new thm.
nipkow
parents: 5737
diff changeset
    31
  "evala env (Sum a1 a2) = evala env a1 + evala env a2"
614f2f30781a Shortened names and added new thm.
nipkow
parents: 5737
diff changeset
    32
  "evala env (Diff a1 a2) = evala env a1 - evala env a2"
614f2f30781a Shortened names and added new thm.
nipkow
parents: 5737
diff changeset
    33
  "evala env (Var v) = env v"
614f2f30781a Shortened names and added new thm.
nipkow
parents: 5737
diff changeset
    34
  "evala env (Num n) = n"
5737
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    35
5802
614f2f30781a Shortened names and added new thm.
nipkow
parents: 5737
diff changeset
    36
  "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    37
  "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    38
  "evalb env (Neg b) = (\<not> evalb env b)"
5737
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    39
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    40
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    41
text {* \medskip Substitution on arithmetic and boolean expressions *}
5737
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    42
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    43
consts
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    44
  substa :: "('a => 'b aexp) => 'a aexp => 'b aexp"
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    45
  substb :: "('a => 'b aexp) => 'a bexp => 'b bexp"
5737
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    46
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    47
primrec
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    48
  "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
5802
614f2f30781a Shortened names and added new thm.
nipkow
parents: 5737
diff changeset
    49
  "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
614f2f30781a Shortened names and added new thm.
nipkow
parents: 5737
diff changeset
    50
  "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
614f2f30781a Shortened names and added new thm.
nipkow
parents: 5737
diff changeset
    51
  "substa f (Var v) = f v"
614f2f30781a Shortened names and added new thm.
nipkow
parents: 5737
diff changeset
    52
  "substa f (Num n) = Num n"
5737
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    53
5802
614f2f30781a Shortened names and added new thm.
nipkow
parents: 5737
diff changeset
    54
  "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
614f2f30781a Shortened names and added new thm.
nipkow
parents: 5737
diff changeset
    55
  "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
614f2f30781a Shortened names and added new thm.
nipkow
parents: 5737
diff changeset
    56
  "substb f (Neg b) = Neg (substb f b)"
5737
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    57
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    58
lemma subst1_aexp_bexp:
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    59
  "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a \<and>
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    60
  evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    61
    --  {* one variable *}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    62
  apply (induct a and b)
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    63
         apply simp_all
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    64
  done
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    65
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    66
lemma subst_all_aexp_bexp:
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    67
  "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a \<and>
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    68
  evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    69
    -- {* all variables *}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    70
  apply (induct a and b)
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    71
         apply auto
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    72
  done
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 5802
diff changeset
    73
5737
31fc1d0e66d5 New example for using the datatype package:
berghofe
parents:
diff changeset
    74
end