src/HOL/IMP/Expr.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1973 8c94c9a5be10
child 4089 96fba19bcbe2
permissions -rw-r--r--
Dep. on Provers/nat_transitive
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
nipkow@1697
    10
open Expr;
nipkow@1697
    11
nipkow@1697
    12
val evala_elim_cases = map (evala.mk_cases aexp.simps)
paulson@1729
    13
   ["(N(n),sigma) -a-> i", "(X(x),sigma) -a-> i",
paulson@1729
    14
    "(Op1 f e,sigma) -a-> i", "(Op2 f a1 a2,sigma)  -a-> i"
nipkow@1697
    15
   ];
nipkow@1697
    16
nipkow@1697
    17
val evalb_elim_cases = map (evalb.mk_cases bexp.simps)
paulson@1729
    18
   ["(true,sigma) -b-> x", "(false,sigma) -b-> x",
paulson@1729
    19
    "(ROp f a0 a1,sigma) -b-> x", "(noti(b),sigma) -b-> x",
paulson@1729
    20
    "(b0 andi b1,sigma) -b-> x", "(b0 ori b1,sigma) -b-> x"
nipkow@1697
    21
   ];
nipkow@1697
    22
nipkow@1697
    23
val evalb_simps = map (fn s => prove_goal Expr.thy s
nipkow@1697
    24
    (fn _ => [fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases) 1]))
paulson@1729
    25
  ["((true,sigma) -b-> w) = (w=True)",
paulson@1729
    26
   "((false,sigma) -b-> w) = (w=False)",
paulson@1729
    27
   "((ROp f a0 a1,sigma) -b-> w) = \
paulson@1729
    28
\   (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))",
paulson@1729
    29
   "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))",
paulson@1729
    30
   "((b0 andi b1,sigma) -b-> w) = \
paulson@1729
    31
\   (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))",
paulson@1729
    32
   "((b0 ori b1,sigma) -b-> w) = \
paulson@1729
    33
\   (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"];
nipkow@1697
    34
paulson@1729
    35
goal Expr.thy "!n. ((a,s) -a-> n) = (n = A a s)";
nipkow@1697
    36
by (aexp.induct_tac "a" 1);                               (* struct. ind. *)
nipkow@1697
    37
by (ALLGOALS Simp_tac);                                   (* rewr. Den.   *)
nipkow@1973
    38
by (TRYALL (fast_tac (!claset addSIs (evala.intrs@prems)
nipkow@1697
    39
                             addSEs evala_elim_cases)));
nipkow@1697
    40
qed_spec_mp "aexp_iff";
nipkow@1697
    41
paulson@1729
    42
goal Expr.thy "!w. ((b,s) -b-> w) = (w = B b s)";
nipkow@1697
    43
by (bexp.induct_tac "b" 1);
nipkow@1697
    44
by (ALLGOALS(asm_simp_tac (!simpset addcongs [conj_cong]
nipkow@1697
    45
                                    addsimps (aexp_iff::evalb_simps))));
nipkow@1697
    46
qed_spec_mp "bexp_iff";