src/HOLCF/IMP/Denotational.ML

Added "discrete" CPOs and modified IMP to use those rather than "lift"

(*  Title:      HOLCF/IMP/Denotational.ML
    ID:         $Id$
    Author:     Tobias Nipkow & Robert Sandner
    Copyright   1996 TUM

Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL
*)

goalw thy [dlift_def] "dlift f`(Def x) = f`(Discr x)";
by(Simp_tac 1);
qed "dlift_Def";
Addsimps [dlift_Def];

goalw thy [dlift_def] "cont(%f. dlift f)";
by(Simp_tac 1);
qed "cont_dlift";
AddIffs [cont_dlift];

goalw thy [dlift_def] "dlift f`l = Def y --> (? x. l = Def x)";
by(simp_tac (!simpset setloop (split_tac[expand_lift_case])) 1);
qed_spec_mp "dlift_DefD";


goal thy "!!c. <c,s> -c-> t ==> D c`(Discr s) = (Def t)";
be evalc.induct 1;
      by (ALLGOALS Asm_simp_tac);
 by (ALLGOALS (rtac (fix_eq RS ssubst) THEN' Asm_full_simp_tac));
qed_spec_mp "eval_implies_D";

goal thy "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
by (com.induct_tac "c" 1);
    by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
   by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
  by (Simp_tac 1);
  by (strip_tac 1);
  by (forward_tac [dlift_DefD] 1);
  be exE 1;
  by (rotate_tac ~1 1);
  by (Asm_full_simp_tac 1);
  by (fast_tac (HOL_cs addSIs evalc.intrs) 1);
 by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 by (fast_tac ((HOL_cs addIs evalc.intrs) unsafe_addss !simpset) 1);
by (Simp_tac 1);
br fix_ind 1;
  by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_flatdom,flat_lift])) 1);
 by (Simp_tac 1);
by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
by (safe_tac HOL_cs);
  (* case bexp s *)
  by (forward_tac [dlift_DefD] 1);
  be exE 1;
  by (rotate_tac ~1 1);
  by (Asm_full_simp_tac 1);
  by (fast_tac (HOL_cs addIs evalc.intrs) 1);
 (* case ~bexp s *)
 by (fast_tac ((HOL_cs addSIs evalc.intrs) unsafe_addss !simpset) 1);
qed_spec_mp "D_implies_eval";


goal thy "(D c`(Discr s) = (Def t)) = (<c,s> -c-> t)";
by (fast_tac (HOL_cs addSEs [D_implies_eval,eval_implies_D]) 1);
qed "D_is_eval";