src/HOL/IMP/Denotation.ML
author nipkow
Wed Nov 24 12:12:36 1999 +0100 (1999-11-24)
changeset 8029 05446a898852
parent 5223 4cb05273f764
child 10186 499637e8f2c6
permissions -rw-r--r--
Basis now Main.
     1 (*  Title:      HOL/IMP/Denotation.ML
     2     ID:         $Id$
     3     Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
     4     Copyright   1994 TUM
     5 *)
     6 
     7 (**** mono (Gamma(b,c)) ****)
     8 
     9 qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def]
    10         "mono (Gamma b c)"
    11      (fn _ => [Fast_tac 1]);
    12 
    13 
    14 Goal "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)";
    15 by (Simp_tac 1);
    16 by (EVERY[stac (Gamma_mono RS lfp_Tarski) 1,
    17           stac (Gamma_def RS meta_eq_to_obj_eq RS fun_cong) 1,
    18           Simp_tac 1,
    19           IF_UNSOLVED no_tac]);
    20 qed "C_While_If";
    21 
    22 
    23 (* Operational Semantics implies Denotational Semantics *)
    24 
    25 Goal "<c,s> -c-> t ==> (s,t) : C(c)";
    26 
    27 (* start with rule induction *)
    28 by (etac evalc.induct 1);
    29 by Auto_tac;
    30 (* while *)
    31 by (rewtac Gamma_def);
    32 by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
    33 by (Fast_tac 1);
    34 by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
    35 by (Fast_tac 1);
    36 
    37 qed "com1";
    38 
    39 (* Denotational Semantics implies Operational Semantics *)
    40 
    41 Goal "!s t. (s,t):C(c) --> <c,s> -c-> t";
    42 by (induct_tac "c" 1);
    43 
    44 by (ALLGOALS Full_simp_tac);
    45 by (ALLGOALS (TRY o Fast_tac));
    46 
    47 (* while *)
    48 by (strip_tac 1);
    49 by (etac (Gamma_mono RSN (2,induct)) 1);
    50 by (rewtac Gamma_def);  
    51 by (Fast_tac 1);
    52 
    53 qed_spec_mp "com2";
    54 
    55 
    56 (**** Proof of Equivalence ****)
    57 
    58 Goal "(s,t) : C(c)  =  (<c,s> -c-> t)";
    59 by (fast_tac (claset() addEs [com2] addDs [com1]) 1);
    60 qed "denotational_is_natural";