src/HOL/IMP/Expr.ML
author nipkow
Wed Nov 24 12:12:36 1999 +0100 (1999-11-24)
changeset 8029 05446a898852
parent 6141 a6922171b396
permissions -rw-r--r--
Basis now Main.
nipkow@1697
     1
(*  Title:      HOL/IMP/Expr.ML
nipkow@1697
     2
    ID:         $Id$
nipkow@1697
     3
    Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
nipkow@1697
     4
    Copyright   1994 TUM
nipkow@1697
     5
nipkow@1697
     6
Arithmetic expressions and Boolean expressions.
nipkow@1697
     7
Not used in the rest of the language, but included for completeness.
nipkow@1697
     8
*)
nipkow@1697
     9
paulson@6141
    10
val evala_elim_cases = 
paulson@6141
    11
    map evala.mk_cases
paulson@6141
    12
       ["(N(n),sigma) -a-> i", 
paulson@6141
    13
	"(X(x),sigma) -a-> i",
paulson@6141
    14
	"(Op1 f e,sigma) -a-> i", 
paulson@6141
    15
	"(Op2 f a1 a2,sigma)  -a-> i"];
nipkow@1697
    16
paulson@6141
    17
val evalb_elim_cases = 
paulson@6141
    18
    map evalb.mk_cases
paulson@6141
    19
       ["(true,sigma) -b-> x", 
paulson@6141
    20
	"(false,sigma) -b-> x",
paulson@6141
    21
	"(ROp f a0 a1,sigma) -b-> x", 
paulson@6141
    22
	"(noti(b),sigma) -b-> x",
paulson@6141
    23
	"(b0 andi b1,sigma) -b-> x", 
paulson@6141
    24
	"(b0 ori b1,sigma) -b-> x"];
nipkow@1697
    25
nipkow@1697
    26
val evalb_simps = map (fn s => prove_goal Expr.thy s
nipkow@1697
    27
    (fn _ => [fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases) 1]))
paulson@1729
    28
  ["((true,sigma) -b-> w) = (w=True)",
paulson@1729
    29
   "((false,sigma) -b-> w) = (w=False)",
paulson@1729
    30
   "((ROp f a0 a1,sigma) -b-> w) = \
paulson@1729
    31
\   (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))",
paulson@1729
    32
   "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))",
paulson@1729
    33
   "((b0 andi b1,sigma) -b-> w) = \
paulson@1729
    34
\   (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))",
paulson@1729
    35
   "((b0 ori b1,sigma) -b-> w) = \
paulson@1729
    36
\   (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"];
nipkow@1697
    37
wenzelm@5069
    38
Goal "!n. ((a,s) -a-> n) = (A a s = n)";
berghofe@5183
    39
by (induct_tac "a" 1);
paulson@5535
    40
by (auto_tac (claset() addSIs evala.intrs addSEs evala_elim_cases,
paulson@5535
    41
	      simpset()));
nipkow@1697
    42
qed_spec_mp "aexp_iff";
nipkow@1697
    43
wenzelm@5069
    44
Goal "!w. ((b,s) -b-> w) = (B b s = w)";
berghofe@5183
    45
by (induct_tac "b" 1);
paulson@5535
    46
by (auto_tac (claset(), 
paulson@5535
    47
	      simpset() addsimps aexp_iff::evalb_simps));
nipkow@1697
    48
qed_spec_mp "bexp_iff";