src/HOLCF/IMP/Denotational.ML
author nipkow
Mon, 17 Mar 1997 15:37:41 +0100
changeset 2798 f84be65745b2
child 2841 c2508f4ab739
permissions -rw-r--r--
The HOLCF-based den. sem. of IMP.
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
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     9
Addsimps [flift1_def];
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    10
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    11
val prems = goal Lift.thy "[| f`UU = UU; f`x = Def b |] ==> EX a. x = Def a";
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    12
by (cut_facts_tac prems 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    13
by (res_inst_tac [("x","x")] Lift_cases 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    14
 by (fast_tac (HOL_cs addSEs [DefE2]) 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    15
by (fast_tac HOL_cs 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    16
qed "strict_Def";
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    17
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    18
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    19
goal thy "D(WHILE b DO c) = D(IF b THEN c;WHILE b DO c ELSE SKIP)";
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    20
by(Simp_tac 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    21
by(EVERY[stac fix_eq 1, Simp_tac 1, IF_UNSOLVED	no_tac]);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    22
qed "D_While_If";
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    23
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    24
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    25
goal thy "D c`UU =UU";
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    26
by (com.induct_tac "c" 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 (stac fix_eq 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    29
by (Asm_simp_tac 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    30
qed "D_strict";
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    31
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    32
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    33
goal thy "!!c. <c,s> -c-> t ==> D c`(Def s) = (Def t)";
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    34
be evalc.induct 1;
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    35
      by (ALLGOALS Asm_simp_tac);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    36
 by (ALLGOALS (rtac (fix_eq RS ssubst) THEN' Asm_full_simp_tac));
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    37
qed_spec_mp "eval_implies_D";
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    38
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    39
goal thy "!s t. D c`(Def s) = (Def t) --> <c,s> -c-> t";
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    40
by (com.induct_tac "c" 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    41
    by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    42
   by (fast_tac ((HOL_cs addSIs evalc.intrs) 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
  by (strip_tac 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    45
  by (forward_tac [D_strict RS strict_Def] 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    46
  be exE 1;
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    47
  by (rotate_tac ~1 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    48
  by (Asm_full_simp_tac 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    49
  by (fast_tac (HOL_cs addSIs evalc.intrs) 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    50
 by (REPEAT (rtac allI 1));
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    51
 by (case_tac "bexp s" 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    52
  by (fast_tac ((HOL_cs addSIs evalc.intrs) unsafe_addss !simpset) 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    53
 by (fast_tac ((HOL_cs addIs evalc.intrs) unsafe_addss !simpset) 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    54
by(res_inst_tac [("Q","D (WHILE bexp DO com)`UU = UU")] conjunct1 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    55
by (Simp_tac 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    56
br fix_ind 1;
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    57
  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
    58
 by (Simp_tac 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    59
br conjI 1;
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    60
 by (REPEAT (rtac allI 1));
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    61
 by (case_tac "bexp s" 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    62
  (* case bexp s *)
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    63
  by (Asm_simp_tac 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    64
  by (strip_tac 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    65
  be conjE 1;
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    66
  bd strict_Def 1;
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    67
   ba 1;
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    68
  be exE 1;
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    69
  by (rotate_tac ~1 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    70
  by (Asm_full_simp_tac 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    71
  by (fast_tac (HOL_cs addIs evalc.intrs) 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    72
 (* case ~bexp s *)
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    73
 by (fast_tac ((HOL_cs addSIs evalc.intrs) unsafe_addss !simpset) 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    74
(* induction step for strictness *)
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    75
by (Asm_full_simp_tac 1);
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    76
qed_spec_mp "D_implies_eval";
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    77
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    78
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    79
goal thy "(D c`(Def s) = (Def t)) = (<c,s> -c-> t)";
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    80
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
    81
qed "D_is_eval";