src/HOLCF/IMP/Denotational.ML
author nipkow
Wed, 26 Mar 1997 17:58:48 +0100
changeset 2841 c2508f4ab739
parent 2798 f84be65745b2
child 2846 53c76f9d95fd
permissions -rw-r--r--
Added "discrete" CPOs and modified IMP to use those rather than "lift"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     1
(*  Title:      HOLCF/IMP/Denotational.ML
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow & Robert Sandner
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     4
    Copyright   1996 TUM
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     5
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     6
Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     7
*)
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     8
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
     9
goalw thy [dlift_def] "dlift f`(Def x) = f`(Discr x)";
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    10
by(Simp_tac 1);
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    11
qed "dlift_Def";
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    12
Addsimps [dlift_Def];
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    13
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    14
goalw thy [dlift_def] "cont(%f. dlift f)";
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    15
by(Simp_tac 1);
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    16
qed "cont_dlift";
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    17
AddIffs [cont_dlift];
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    18
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    19
goalw thy [dlift_def] "dlift f`l = Def y --> (? x. l = Def x)";
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    20
by(simp_tac (!simpset setloop (split_tac[expand_lift_case])) 1);
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    21
qed_spec_mp "dlift_DefD";
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    22
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    23
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    24
goal thy "!!c. <c,s> -c-> t ==> D c`(Discr s) = (Def t)";
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    25
be evalc.induct 1;
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    26
      by (ALLGOALS Asm_simp_tac);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    27
 by (ALLGOALS (rtac (fix_eq RS ssubst) THEN' Asm_full_simp_tac));
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    28
qed_spec_mp "eval_implies_D";
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    29
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    30
goal thy "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    31
by (com.induct_tac "c" 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    32
    by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    33
   by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    34
  by (Simp_tac 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    35
  by (strip_tac 1);
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    36
  by (forward_tac [dlift_DefD] 1);
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    37
  be exE 1;
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    38
  by (rotate_tac ~1 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    39
  by (Asm_full_simp_tac 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    40
  by (fast_tac (HOL_cs addSIs evalc.intrs) 1);
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    41
 by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    42
 by (fast_tac ((HOL_cs addIs evalc.intrs) unsafe_addss !simpset) 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    43
by (Simp_tac 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    44
br fix_ind 1;
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    45
  by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_flatdom,flat_lift])) 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    46
 by (Simp_tac 1);
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    47
by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    48
by (safe_tac HOL_cs);
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    49
  (* case bexp s *)
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    50
  by (forward_tac [dlift_DefD] 1);
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    51
  be exE 1;
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    52
  by (rotate_tac ~1 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    53
  by (Asm_full_simp_tac 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    54
  by (fast_tac (HOL_cs addIs evalc.intrs) 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    55
 (* case ~bexp s *)
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    56
 by (fast_tac ((HOL_cs addSIs evalc.intrs) unsafe_addss !simpset) 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    57
qed_spec_mp "D_implies_eval";
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    58
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    59
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    60
goal thy "(D c`(Discr s) = (Def t)) = (<c,s> -c-> t)";
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    61
by (fast_tac (HOL_cs addSEs [D_implies_eval,eval_implies_D]) 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    62
qed "D_is_eval";