isabelle: src/HOLCF/IMP/Denotational.ML@53c76f9d95fd (annotated)

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
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	9	goalw thy [dlift_def] "dlift f`(Def x) = f`(Discr x)";
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	10	by(Simp_tac 1);
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
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	14	goalw thy [dlift_def] "cont(%f. dlift f)";
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	15	by(Simp_tac 1);
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
2846 53c76f9d95fd Optimized proofs. nipkow parents: 2841 diff changeset	19	goalw thy [dlift_def]
53c76f9d95fd Optimized proofs. nipkow parents: 2841 diff changeset	20	"(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	21	by(simp_tac (!simpset setloop (split_tac[expand_lift_case])) 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
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	25	goal thy "!!c. <c,s> -c-> t ==> D c`(Discr s) = (Def t)";
2798 f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	26	be evalc.induct 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 (ALLGOALS (rtac (fix_eq RS ssubst) THEN' Asm_full_simp_tac));
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
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	31	goal thy "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
2798 f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	32	by (com.induct_tac "c" 1);
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	33	by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	34	by (fast_tac ((HOL_cs addSIs evalc.intrs) addss !simpset) 1);
2846 53c76f9d95fd Optimized proofs. nipkow parents: 2841 diff changeset	35	by (fast_tac ((HOL_cs addSIs evalc.intrs) unsafe_addss !simpset) 1);
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	36	by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
2798 f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	37	by (fast_tac ((HOL_cs addIs evalc.intrs) unsafe_addss !simpset) 1);
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	38	by (Simp_tac 1);
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	39	br fix_ind 1;
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	40	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	41	by (Simp_tac 1);
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	42	by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
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);
f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	45	by (fast_tac ((HOL_cs addSIs evalc.intrs) unsafe_addss !simpset) 1);
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
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2798 diff changeset	49	goal thy "(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";

author	nipkow
	Thu, 27 Mar 1997 17:46:24 +0100
changeset 2846	53c76f9d95fd
parent 2841	c2508f4ab739
child 3221	90211fa9ee7e
permissions	-rw-r--r--