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