src/HOLCF/IMP/Denotational.ML
author wenzelm
Tue, 28 Jul 1998 17:05:34 +0200
changeset 5210 54aaa779b6b4
parent 5192 704dd3a6d47d
child 5525 896f8234b864
permissions -rw-r--r--
removed global_names flag;
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
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
     9
Goalw [dlift_def] "dlift f`(Def x) = f`(Discr x)";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3325
diff changeset
    10
by (Simp_tac 1);
2841
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
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    14
Goalw [dlift_def] "cont(%f. dlift f)";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3325
diff changeset
    15
by (Simp_tac 1);
2841
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
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    19
Goalw [dlift_def]
2846
53c76f9d95fd Optimized proofs.
nipkow
parents: 2841
diff changeset
    20
 "(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 5143
diff changeset
    21
by (simp_tac (simpset() addsplits [Lift1.lift.split]) 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
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5068
diff changeset
    25
Goal "<c,s> -c-> t ==> D c`(Discr s) = (Def t)";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3325
diff changeset
    26
by (etac evalc.induct 1);
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    27
      by (ALLGOALS Asm_simp_tac);
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3325
diff changeset
    28
 by (ALLGOALS (stac fix_eq THEN' Asm_full_simp_tac));
2798
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
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    31
Goal "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 5143
diff changeset
    32
by (induct_tac "c" 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
    33
    by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
    34
   by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
    35
  by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4098
diff changeset
    36
 by (Simp_tac 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3457
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);
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3325
diff changeset
    39
by (rtac fix_ind 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3325
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);
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4098
diff changeset
    42
by (Simp_tac 1);
2841
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);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3457
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
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    49
Goal "(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";