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