isabelle: src/HOLCF/IMP/Denotational.ML@c326808da921 (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
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4833 diff changeset	9	Goalw [dlift_def] "dlift f`(Def x) = f`(Discr x)";
3457 a8ab7c64817c Ran expandshort paulson parents: 3325 diff changeset	10	by (Simp_tac 1);
2841 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
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4833 diff changeset	14	Goalw [dlift_def] "cont(%f. dlift f)";
3457 a8ab7c64817c Ran expandshort paulson parents: 3325 diff changeset	15	by (Simp_tac 1);
2841 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
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4833 diff changeset	19	Goalw [dlift_def]
2846 53c76f9d95fd Optimized proofs. nipkow parents: 2841 diff changeset	20	"(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
5192 704dd3a6d47d Adapted to new datatype package. berghofe parents: 5143 diff changeset	21	by (simp_tac (simpset() addsplits [Lift1.lift.split]) 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
5143 b94cd208f073 Removal of leading "\!\!..." from most Goal commands paulson parents: 5068 diff changeset	25	Goal "<c,s> -c-> t ==> D c`(Discr s) = (Def t)";
3457 a8ab7c64817c Ran expandshort paulson parents: 3325 diff changeset	26	by (etac evalc.induct 1);
2798 f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	27	by (ALLGOALS Asm_simp_tac);
3457 a8ab7c64817c Ran expandshort paulson parents: 3325 diff changeset	28	by (ALLGOALS (stac fix_eq THEN' Asm_full_simp_tac));
2798 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
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4833 diff changeset	31	Goal "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
5192 704dd3a6d47d Adapted to new datatype package. berghofe parents: 5143 diff changeset	32	by (induct_tac "c" 1);
5618 721671c68324 tidied paulson parents: 5525 diff changeset	33	by (Force_tac 1);
5525 896f8234b864 improved addbefore and addSbefore oheimb parents: 5192 diff changeset	34	by (Force_tac 1);
896f8234b864 improved addbefore and addSbefore oheimb parents: 5192 diff changeset	35	by (Force_tac 1);
4833 2e53109d4bc8 Renamed expand_const -> split_const nipkow parents: 4098 diff changeset	36	by (Simp_tac 1);
5618 721671c68324 tidied paulson parents: 5525 diff changeset	37	by (Force_tac 1);
2798 f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	38	by (Simp_tac 1);
3457 a8ab7c64817c Ran expandshort paulson parents: 3325 diff changeset	39	by (rtac fix_ind 1);
5618 721671c68324 tidied paulson parents: 5525 diff changeset	40	by (fast_tac (claset() addSIs adm_lemmas@[adm_chfindom,ax_flat_lift]) 1);
2798 f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	41	by (Simp_tac 1);
4833 2e53109d4bc8 Renamed expand_const -> split_const nipkow parents: 4098 diff changeset	42	by (Simp_tac 1);
5618 721671c68324 tidied paulson parents: 5525 diff changeset	43	by Safe_tac;
721671c68324 tidied paulson parents: 5525 diff changeset	44	by (Fast_tac 1);
721671c68324 tidied paulson parents: 5525 diff changeset	45	by (Force_tac 1);
2798 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
5068 fb28eaa07e01 isatool fixgoal; wenzelm parents: 4833 diff changeset	49	Goal "(D c`(Discr s) = (Def t)) = (<c,s> -c-> t)";
5618 721671c68324 tidied paulson parents: 5525 diff changeset	50	by (fast_tac (claset() addSEs [D_implies_eval,eval_implies_D]) 1);
2798 f84be65745b2 The HOLCF-based den. sem. of IMP. nipkow parents: diff changeset	51	qed "D_is_eval";

author	wenzelm
	Wed, 29 Sep 1999 13:49:49 +0200
changeset 7634	c326808da921
parent 5618	721671c68324
child 10835	f4745d77e620
permissions	-rw-r--r--