src/HOL/IMP/Denotation.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24 ago)
changeset 4477 b3e5857d8d99
parent 4089 96fba19bcbe2
child 5069 3ea049f7979d
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
clasohm@1465
     1
(*  Title:      HOL/IMP/Denotation.ML
clasohm@924
     2
    ID:         $Id$
nipkow@1696
     3
    Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
clasohm@924
     4
    Copyright   1994 TUM
clasohm@924
     5
*)
clasohm@924
     6
clasohm@924
     7
open Denotation;
clasohm@924
     8
nipkow@1696
     9
clasohm@924
    10
(**** mono (Gamma(b,c)) ****)
clasohm@924
    11
clasohm@924
    12
qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def]
clasohm@1465
    13
        "mono (Gamma b c)"
nipkow@1973
    14
     (fn _ => [Fast_tac 1]);
nipkow@1481
    15
nipkow@1696
    16
nipkow@1696
    17
goal Denotation.thy "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)";
paulson@2031
    18
by (Simp_tac 1);
paulson@2031
    19
by (EVERY[stac (Gamma_mono RS lfp_Tarski) 1,
nipkow@1696
    20
          stac (Gamma_def RS meta_eq_to_obj_eq RS fun_cong) 1,
paulson@2031
    21
          Simp_tac 1,
paulson@2031
    22
          IF_UNSOLVED no_tac]);
nipkow@1481
    23
qed "C_While_If";
nipkow@1481
    24
nipkow@1696
    25
nipkow@1696
    26
(* Operational Semantics implies Denotational Semantics *)
nipkow@1696
    27
paulson@1731
    28
goal Denotation.thy "!!c s t. <c,s> -c-> t ==> (s,t) : C(c)";
nipkow@1696
    29
nipkow@1696
    30
(* start with rule induction *)
paulson@1731
    31
by (etac evalc.induct 1);
paulson@4477
    32
by Auto_tac;
nipkow@1696
    33
(* while *)
paulson@2031
    34
by (rewtac Gamma_def);
paulson@2036
    35
by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
nipkow@1973
    36
by (Fast_tac 1);
paulson@2036
    37
by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
nipkow@1973
    38
by (Fast_tac 1);
nipkow@1696
    39
paulson@1731
    40
qed "com1";
nipkow@1696
    41
nipkow@1696
    42
(* Denotational Semantics implies Operational Semantics *)
nipkow@1696
    43
nipkow@1696
    44
goal Denotation.thy "!s t. (s,t):C(c) --> <c,s> -c-> t";
nipkow@1696
    45
by (com.induct_tac "c" 1);
nipkow@1973
    46
paulson@2031
    47
by (ALLGOALS Full_simp_tac);
paulson@2031
    48
by (ALLGOALS (TRY o Fast_tac));
nipkow@1696
    49
nipkow@1696
    50
(* while *)
nipkow@1696
    51
by (strip_tac 1);
nipkow@1696
    52
by (etac (Gamma_mono RSN (2,induct)) 1);
nipkow@1696
    53
by (rewtac Gamma_def);  
nipkow@1973
    54
by (Fast_tac 1);
nipkow@1696
    55
nipkow@1696
    56
qed_spec_mp "com2";
nipkow@1696
    57
nipkow@1696
    58
nipkow@1696
    59
(**** Proof of Equivalence ****)
nipkow@1696
    60
nipkow@1696
    61
goal Denotation.thy "(s,t) : C(c)  =  (<c,s> -c-> t)";
wenzelm@4089
    62
by (fast_tac (claset() addEs [com2] addDs [com1]) 1);
nipkow@1696
    63
qed "denotational_is_natural";