src/HOLCF/IMP/Denotational.ML
author slotosch
Sun, 25 May 1997 16:57:19 +0200
changeset 3325 4e4ee8a101be
parent 3324 6b26b886ff69
child 3457 a8ab7c64817c
permissions -rw-r--r--
*** empty log message ***
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
2846
53c76f9d95fd Optimized proofs.
nipkow
parents: 2841
diff changeset
    19
goalw thy [dlift_def]
53c76f9d95fd Optimized proofs.
nipkow
parents: 2841
diff changeset
    20
 "(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    21
by(simp_tac (!simpset setloop (split_tac[expand_lift_case])) 1);
2846
53c76f9d95fd Optimized proofs.
nipkow
parents: 2841
diff changeset
    22
qed "dlift_is_Def";
53c76f9d95fd Optimized proofs.
nipkow
parents: 2841
diff changeset
    23
Addsimps [dlift_is_Def];
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    24
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    25
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
    26
be evalc.induct 1;
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    27
      by (ALLGOALS Asm_simp_tac);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    28
 by (ALLGOALS (rtac (fix_eq RS ssubst) THEN' Asm_full_simp_tac));
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    29
qed_spec_mp "eval_implies_D";
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    30
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    31
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
    32
by (com.induct_tac "c" 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 (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
3221
90211fa9ee7e renamed unsafe_addss to addss
oheimb
parents: 2846
diff changeset
    35
  by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    36
 by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
3221
90211fa9ee7e renamed unsafe_addss to addss
oheimb
parents: 2846
diff changeset
    37
 by (fast_tac ((HOL_cs addIs evalc.intrs) addss !simpset) 1);
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    38
by (Simp_tac 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    39
br fix_ind 1;
3325
4e4ee8a101be *** empty log message ***
slotosch
parents: 3324
diff changeset
    40
  by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,ax_flat_lift])) 1);
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    41
 by (Simp_tac 1);
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    42
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
    43
by (safe_tac HOL_cs);
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    44
  by (fast_tac (HOL_cs addIs evalc.intrs) 1);
3221
90211fa9ee7e renamed unsafe_addss to addss
oheimb
parents: 2846
diff changeset
    45
 by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    46
qed_spec_mp "D_implies_eval";
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    47
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    48
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents: 2798
diff changeset
    49
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
    50
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
    51
qed "D_is_eval";