src/HOLCF/IMP/Denotational.ML
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 5618 721671c68324
child 12031 1b883fa9458e
permissions -rw-r--r--
` -> $
nipkow@2798
     1
(*  Title:      HOLCF/IMP/Denotational.ML
nipkow@2798
     2
    ID:         $Id$
nipkow@2798
     3
    Author:     Tobias Nipkow & Robert Sandner
nipkow@2798
     4
    Copyright   1996 TUM
nipkow@2798
     5
nipkow@2798
     6
Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL
nipkow@2798
     7
*)
nipkow@2798
     8
nipkow@10835
     9
Goalw [dlift_def] "dlift f$(Def x) = f$(Discr x)";
paulson@3457
    10
by (Simp_tac 1);
nipkow@2841
    11
qed "dlift_Def";
nipkow@2841
    12
Addsimps [dlift_Def];
nipkow@2798
    13
wenzelm@5068
    14
Goalw [dlift_def] "cont(%f. dlift f)";
paulson@3457
    15
by (Simp_tac 1);
nipkow@2841
    16
qed "cont_dlift";
nipkow@2841
    17
AddIffs [cont_dlift];
nipkow@2841
    18
wenzelm@5068
    19
Goalw [dlift_def]
nipkow@10835
    20
 "(dlift f$l = Def y) = (? x. l = Def x & f$(Discr x) = Def y)";
berghofe@5192
    21
by (simp_tac (simpset() addsplits [Lift1.lift.split]) 1);
nipkow@2846
    22
qed "dlift_is_Def";
nipkow@2846
    23
Addsimps [dlift_is_Def];
nipkow@2798
    24
nipkow@10835
    25
Goal "<c,s> -c-> t ==> D c$(Discr s) = (Def t)";
paulson@3457
    26
by (etac evalc.induct 1);
nipkow@2798
    27
      by (ALLGOALS Asm_simp_tac);
paulson@3457
    28
 by (ALLGOALS (stac fix_eq THEN' Asm_full_simp_tac));
nipkow@2798
    29
qed_spec_mp "eval_implies_D";
nipkow@2798
    30
nipkow@10835
    31
Goal "!s t. D c$(Discr s) = (Def t) --> <c,s> -c-> t";
berghofe@5192
    32
by (induct_tac "c" 1);
paulson@5618
    33
    by (Force_tac 1);
oheimb@5525
    34
   by (Force_tac 1);
oheimb@5525
    35
  by (Force_tac 1);
nipkow@4833
    36
 by (Simp_tac 1);
paulson@5618
    37
 by (Force_tac 1);
nipkow@2798
    38
by (Simp_tac 1);
paulson@3457
    39
by (rtac fix_ind 1);
paulson@5618
    40
  by (fast_tac (claset() addSIs adm_lemmas@[adm_chfindom,ax_flat_lift]) 1);
nipkow@2798
    41
 by (Simp_tac 1);
nipkow@4833
    42
by (Simp_tac 1);
paulson@5618
    43
by Safe_tac;
paulson@5618
    44
  by (Fast_tac 1);
paulson@5618
    45
 by (Force_tac 1);
nipkow@2798
    46
qed_spec_mp "D_implies_eval";
nipkow@2798
    47
nipkow@2798
    48
nipkow@10835
    49
Goal "(D c$(Discr s) = (Def t)) = (<c,s> -c-> t)";
paulson@5618
    50
by (fast_tac (claset() addSEs [D_implies_eval,eval_implies_D]) 1);
nipkow@2798
    51
qed "D_is_eval";