src/HOL/IMP/Natural.ML
author nipkow
Wed Nov 24 12:12:36 1999 +0100 (1999-11-24)
changeset 8029 05446a898852
parent 6162 484adda70b65
child 9241 f961c1fdff50
permissions -rw-r--r--
Basis now Main.
nipkow@1700
     1
(*  Title:      HOL/IMP/Natural.ML
nipkow@1700
     2
    ID:         $Id$
nipkow@1700
     3
    Author:     Tobias Nipkow & Larry Paulson, TUM
nipkow@1700
     4
    Copyright   1996 TUM
nipkow@1700
     5
*)
nipkow@1700
     6
nipkow@1700
     7
open Natural;
nipkow@1700
     8
nipkow@1973
     9
AddIs evalc.intrs;
nipkow@1973
    10
paulson@6141
    11
val evalc_elim_cases = 
paulson@6141
    12
    map evalc.mk_cases
paulson@6141
    13
       ["<SKIP,s> -c-> t", 
paulson@6141
    14
	"<x:=a,s> -c-> t", 
paulson@6141
    15
	"<c1;c2, s> -c-> t",
paulson@6141
    16
	"<IF b THEN c1 ELSE c2, s> -c-> t"];
nipkow@1700
    17
paulson@6141
    18
val evalc_WHILE_case = evalc.mk_cases "<WHILE b DO c,s> -c-> t";
nipkow@1700
    19
nipkow@1973
    20
AddSEs evalc_elim_cases;
nipkow@1700
    21
nipkow@1700
    22
(* evaluation of com is deterministic *)
nipkow@5117
    23
Goal "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
paulson@1730
    24
by (etac evalc.induct 1);
paulson@1958
    25
by (thin_tac "<?c,s2> -c-> s1" 7);
paulson@4241
    26
(*blast_tac needs Unify.search_bound, trace_bound := 40*)
paulson@4241
    27
by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case])));
nipkow@1700
    28
qed_spec_mp "com_det";
nipkow@5789
    29
nipkow@5789
    30
(** An example due to Tony Hoare **)
nipkow@5789
    31
nipkow@5789
    32
Goal "[| !x. P x --> Q x; <w,s> -c-> t |] ==> \
nipkow@5789
    33
\ !c. w = While P c --> <While Q c,t> -c-> u --> <While Q c,s> -c-> u";
paulson@6162
    34
by (etac evalc.induct 1);
paulson@6162
    35
by (Auto_tac);
nipkow@5789
    36
val lemma1 = result() RS spec RS mp RS mp;
nipkow@5789
    37
nipkow@5789
    38
Goal "[| !x. P x --> Q x; <w,s> -c-> u |] ==> \
nipkow@5789
    39
\ !c. w = While Q c --> <While P c; While Q c,s> -c-> u";
paulson@6162
    40
by (etac evalc.induct 1);
paulson@6162
    41
by (ALLGOALS Asm_simp_tac);
paulson@6162
    42
by (Blast_tac 1);
paulson@6162
    43
by (case_tac "P s" 1);
paulson@6162
    44
by (Auto_tac);
nipkow@5789
    45
val lemma2 = result() RS spec RS mp;
nipkow@5789
    46
nipkow@5789
    47
Goal "!x. P x --> Q x ==> \
nipkow@5789
    48
\ (<While P c; While Q c, s> -c-> t) = (<While Q c, s> -c-> t)";
paulson@6162
    49
by (blast_tac (claset() addIs [lemma1,lemma2]) 1);
nipkow@5789
    50
qed "Hoare_example";