The HOLCF-based den. sem. of IMP.
authornipkow
Mon Mar 17 15:37:41 1997 +0100 (1997-03-17)
changeset 2798f84be65745b2
parent 2797 54ca927b831b
child 2799 1857b7e2e095
The HOLCF-based den. sem. of IMP.
src/HOLCF/IMP/Denotational.ML
src/HOLCF/IMP/Denotational.thy
src/HOLCF/IMP/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/IMP/Denotational.ML	Mon Mar 17 15:37:41 1997 +0100
     1.3 @@ -0,0 +1,81 @@
     1.4 +(*  Title:      HOLCF/IMP/Denotational.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow & Robert Sandner
     1.7 +    Copyright   1996 TUM
     1.8 +
     1.9 +Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL
    1.10 +*)
    1.11 +
    1.12 +Addsimps [flift1_def];
    1.13 +
    1.14 +val prems = goal Lift.thy "[| f`UU = UU; f`x = Def b |] ==> EX a. x = Def a";
    1.15 +by (cut_facts_tac prems 1);
    1.16 +by (res_inst_tac [("x","x")] Lift_cases 1);
    1.17 + by (fast_tac (HOL_cs addSEs [DefE2]) 1);
    1.18 +by (fast_tac HOL_cs 1);
    1.19 +qed "strict_Def";
    1.20 +
    1.21 +
    1.22 +goal thy "D(WHILE b DO c) = D(IF b THEN c;WHILE b DO c ELSE SKIP)";
    1.23 +by(Simp_tac 1);
    1.24 +by(EVERY[stac fix_eq 1, Simp_tac 1, IF_UNSOLVED	no_tac]);
    1.25 +qed "D_While_If";
    1.26 +
    1.27 +
    1.28 +goal thy "D c`UU =UU";
    1.29 +by (com.induct_tac "c" 1);
    1.30 +    by (ALLGOALS Asm_simp_tac);
    1.31 +by (stac fix_eq 1);
    1.32 +by (Asm_simp_tac 1);
    1.33 +qed "D_strict";
    1.34 +
    1.35 +
    1.36 +goal thy "!!c. <c,s> -c-> t ==> D c`(Def s) = (Def t)";
    1.37 +be evalc.induct 1;
    1.38 +      by (ALLGOALS Asm_simp_tac);
    1.39 + by (ALLGOALS (rtac (fix_eq RS ssubst) THEN' Asm_full_simp_tac));
    1.40 +qed_spec_mp "eval_implies_D";
    1.41 +
    1.42 +goal thy "!s t. D c`(Def s) = (Def t) --> <c,s> -c-> t";
    1.43 +by (com.induct_tac "c" 1);
    1.44 +    by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
    1.45 +   by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
    1.46 +  by (Simp_tac 1);
    1.47 +  by (strip_tac 1);
    1.48 +  by (forward_tac [D_strict RS strict_Def] 1);
    1.49 +  be exE 1;
    1.50 +  by (rotate_tac ~1 1);
    1.51 +  by (Asm_full_simp_tac 1);
    1.52 +  by (fast_tac (HOL_cs addSIs evalc.intrs) 1);
    1.53 + by (REPEAT (rtac allI 1));
    1.54 + by (case_tac "bexp s" 1);
    1.55 +  by (fast_tac ((HOL_cs addSIs evalc.intrs) unsafe_addss !simpset) 1);
    1.56 + by (fast_tac ((HOL_cs addIs evalc.intrs) unsafe_addss !simpset) 1);
    1.57 +by(res_inst_tac [("Q","D (WHILE bexp DO com)`UU = UU")] conjunct1 1);
    1.58 +by (Simp_tac 1);
    1.59 +br fix_ind 1;
    1.60 +  by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_flatdom,flat_lift])) 1);
    1.61 + by (Simp_tac 1);
    1.62 +br conjI 1;
    1.63 + by (REPEAT (rtac allI 1));
    1.64 + by (case_tac "bexp s" 1);
    1.65 +  (* case bexp s *)
    1.66 +  by (Asm_simp_tac 1);
    1.67 +  by (strip_tac 1);
    1.68 +  be conjE 1;
    1.69 +  bd strict_Def 1;
    1.70 +   ba 1;
    1.71 +  be exE 1;
    1.72 +  by (rotate_tac ~1 1);
    1.73 +  by (Asm_full_simp_tac 1);
    1.74 +  by (fast_tac (HOL_cs addIs evalc.intrs) 1);
    1.75 + (* case ~bexp s *)
    1.76 + by (fast_tac ((HOL_cs addSIs evalc.intrs) unsafe_addss !simpset) 1);
    1.77 +(* induction step for strictness *)
    1.78 +by (Asm_full_simp_tac 1);
    1.79 +qed_spec_mp "D_implies_eval";
    1.80 +
    1.81 +
    1.82 +goal thy "(D c`(Def s) = (Def t)) = (<c,s> -c-> t)";
    1.83 +by (fast_tac (HOL_cs addSEs [D_implies_eval,eval_implies_D]) 1);
    1.84 +qed "D_is_eval";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOLCF/IMP/Denotational.thy	Mon Mar 17 15:37:41 1997 +0100
     2.3 @@ -0,0 +1,22 @@
     2.4 +(*  Title:      HOL/IMP/Den2.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Tobias Nipkow & Robert Sandner, TUM
     2.7 +    Copyright   1996 TUM
     2.8 +
     2.9 +Denotational semantics of commands in HOLCF
    2.10 +*)
    2.11 +
    2.12 +Denotational = HOLCF + Natural +
    2.13 +
    2.14 +consts D :: "com => state lift -> state lift"
    2.15 +
    2.16 +primrec D com
    2.17 +  "D(SKIP) = (LAM s. s)"
    2.18 +  "D(X := a) = flift1(%s. Def(s[a(s)/X]))"
    2.19 +  "D(c0 ; c1) = ((D c1) oo (D c0))"
    2.20 +  "D(IF b THEN c1 ELSE c2) =
    2.21 +	flift1(%s . if b s then (D c1)`(Def s) else (D c2)`(Def s))"
    2.22 +  "D(WHILE b DO c) =
    2.23 +	fix`(LAM w. flift1(%s. if b s then w`((D c)`(Def s)) else Def s))"
    2.24 +
    2.25 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOLCF/IMP/ROOT.ML	Mon Mar 17 15:37:41 1997 +0100
     3.3 @@ -0,0 +1,18 @@
     3.4 +(*  Title:      HOLCF/IMP/ROOT.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Tobias Nipkow
     3.7 +    Copyright   1997  TU Muenchen
     3.8 +*)
     3.9 +
    3.10 +(*Load theories from ../meta_theory without generating HTML files
    3.11 +  (has already been done by HOL/IMP/ROOT.ML)*)
    3.12 +val old_make_html = !make_html;
    3.13 +make_html := false;
    3.14 +loadpath := ["../../HOL/IMP"];
    3.15 +
    3.16 +use_thy "Natural";
    3.17 +
    3.18 +make_html := old_make_html;
    3.19 +loadpath := ["."];
    3.20 +
    3.21 +use_thy "Denotational";