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.
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
(**** mono (Gamma(b,c)) ****)
clasohm@924
     8
clasohm@924
     9
qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def]
clasohm@1465
    10
        "mono (Gamma b c)"
nipkow@1973
    11
     (fn _ => [Fast_tac 1]);
nipkow@1481
    12
nipkow@1696
    13
wenzelm@5069
    14
Goal "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)";
paulson@2031
    15
by (Simp_tac 1);
paulson@2031
    16
by (EVERY[stac (Gamma_mono RS lfp_Tarski) 1,
nipkow@1696
    17
          stac (Gamma_def RS meta_eq_to_obj_eq RS fun_cong) 1,
paulson@2031
    18
          Simp_tac 1,
paulson@2031
    19
          IF_UNSOLVED no_tac]);
nipkow@1481
    20
qed "C_While_If";
nipkow@1481
    21
nipkow@1696
    22
nipkow@1696
    23
(* Operational Semantics implies Denotational Semantics *)
nipkow@1696
    24
nipkow@5117
    25
Goal "<c,s> -c-> t ==> (s,t) : C(c)";
nipkow@1696
    26
nipkow@1696
    27
(* start with rule induction *)
paulson@1731
    28
by (etac evalc.induct 1);
paulson@4477
    29
by Auto_tac;
nipkow@1696
    30
(* while *)
paulson@2031
    31
by (rewtac Gamma_def);
paulson@2036
    32
by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
nipkow@1973
    33
by (Fast_tac 1);
paulson@2036
    34
by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
nipkow@1973
    35
by (Fast_tac 1);
nipkow@1696
    36
paulson@1731
    37
qed "com1";
nipkow@1696
    38
nipkow@1696
    39
(* Denotational Semantics implies Operational Semantics *)
nipkow@1696
    40
wenzelm@5069
    41
Goal "!s t. (s,t):C(c) --> <c,s> -c-> t";
berghofe@5183
    42
by (induct_tac "c" 1);
nipkow@1973
    43
paulson@2031
    44
by (ALLGOALS Full_simp_tac);
paulson@2031
    45
by (ALLGOALS (TRY o Fast_tac));
nipkow@1696
    46
nipkow@1696
    47
(* while *)
nipkow@1696
    48
by (strip_tac 1);
nipkow@1696
    49
by (etac (Gamma_mono RSN (2,induct)) 1);
nipkow@1696
    50
by (rewtac Gamma_def);  
nipkow@1973
    51
by (Fast_tac 1);
nipkow@1696
    52
nipkow@1696
    53
qed_spec_mp "com2";
nipkow@1696
    54
nipkow@1696
    55
nipkow@1696
    56
(**** Proof of Equivalence ****)
nipkow@1696
    57
wenzelm@5069
    58
Goal "(s,t) : C(c)  =  (<c,s> -c-> t)";
wenzelm@4089
    59
by (fast_tac (claset() addEs [com2] addDs [com1]) 1);
nipkow@1696
    60
qed "denotational_is_natural";