isabelle: src/HOLCF/ex/Dagstuhl.thy@2e9bdc6fbedf (annotated)

17291 94f6113fe9ed converted to Isar theory format; wenzelm parents: 10835 diff changeset	1	theory Dagstuhl
94f6113fe9ed converted to Isar theory format; wenzelm parents: 10835 diff changeset	2	imports Stream
94f6113fe9ed converted to Isar theory format; wenzelm parents: 10835 diff changeset	3	begin
2570 24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	4
25135 4f8176c940cf modernized specifications ('definition', 'axiomatization'); wenzelm parents: 21404 diff changeset	5	axiomatization
17291 94f6113fe9ed converted to Isar theory format; wenzelm parents: 10835 diff changeset	6	y :: "'a"
2570 24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	7
19763 ec18656a2c10 tuned; wenzelm parents: 19742 diff changeset	8	definition
21404 eb85850d3eb7 more robust syntax for definition/abbreviation/notation; wenzelm parents: 19763 diff changeset	9	YS :: "'a stream" where
19763 ec18656a2c10 tuned; wenzelm parents: 19742 diff changeset	10	"YS = fix$(LAM x. y && x)"
21404 eb85850d3eb7 more robust syntax for definition/abbreviation/notation; wenzelm parents: 19763 diff changeset	11
eb85850d3eb7 more robust syntax for definition/abbreviation/notation; wenzelm parents: 19763 diff changeset	12	definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation; wenzelm parents: 19763 diff changeset	13	YYS :: "'a stream" where
19763 ec18656a2c10 tuned; wenzelm parents: 19742 diff changeset	14	"YYS = fix$(LAM z. y && y && z)"
2570 24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	15
19742 86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	16	lemma YS_def2: "YS = y && YS"
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	17	apply (rule trans)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	18	apply (rule fix_eq2)
19763 ec18656a2c10 tuned; wenzelm parents: 19742 diff changeset	19	apply (rule YS_def [THEN eq_reflection])
19742 86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	20	apply (rule beta_cfun)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	21	apply simp
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	22	done
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	23
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	24	lemma YYS_def2: "YYS = y && y && YYS"
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	25	apply (rule trans)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	26	apply (rule fix_eq2)
19763 ec18656a2c10 tuned; wenzelm parents: 19742 diff changeset	27	apply (rule YYS_def [THEN eq_reflection])
19742 86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	28	apply (rule beta_cfun)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	29	apply simp
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	30	done
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	31
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	32
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	33	lemma lemma3: "YYS << y && YYS"
19763 ec18656a2c10 tuned; wenzelm parents: 19742 diff changeset	34	apply (rule YYS_def [THEN eq_reflection, THEN def_fix_ind])
19742 86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	35	apply simp_all
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	36	apply (rule monofun_cfun_arg)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	37	apply (rule monofun_cfun_arg)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	38	apply assumption
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	39	done
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	40
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	41	lemma lemma4: "y && YYS << YYS"
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	42	apply (subst YYS_def2)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	43	back
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	44	apply (rule monofun_cfun_arg)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	45	apply (rule lemma3)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	46	done
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	47
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	48	lemma lemma5: "y && YYS = YYS"
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	49	apply (rule antisym_less)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	50	apply (rule lemma4)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	51	apply (rule lemma3)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	52	done
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	53
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	54	lemma wir_moel: "YS = YYS"
35642 f478d5a9d238 generate separate qualified theorem name for each type's reach and take_lemma huffman parents: 35174 diff changeset	55	apply (rule stream.take_lemma)
19742 86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	56	apply (induct_tac n)
35169 31cbcb019003 fix warnings about duplicate simp rules huffman parents: 25135 diff changeset	57	apply (simp (no_asm))
19742 86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	58	apply (subst YS_def2)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	59	apply (subst YYS_def2)
35169 31cbcb019003 fix warnings about duplicate simp rules huffman parents: 25135 diff changeset	60	apply simp
19742 86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	61	apply (rule lemma5 [symmetric, THEN subst])
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	62	apply (rule refl)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	63	done
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	64
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	65	(* ------------------------------------------------------------------------ *)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	66	(* Zweite L"osung: Bernhard M�ller *)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	67	(* statt Beweis von wir_moel "uber take_lemma beidseitige Inclusion *)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	68	(* verwendet lemma5 *)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	69	(* ------------------------------------------------------------------------ *)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	70
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	71	lemma lemma6: "YYS << YS"
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	72	apply (unfold YYS_def)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	73	apply (rule fix_least)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	74	apply (subst beta_cfun)
35948 5e7909f0346b remove ancient continuity tactic huffman parents: 35642 diff changeset	75	apply simp
19742 86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	76	apply (simp add: YS_def2 [symmetric])
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	77	done
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	78
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	79	lemma lemma7: "YS << YYS"
19763 ec18656a2c10 tuned; wenzelm parents: 19742 diff changeset	80	apply (rule YS_def [THEN eq_reflection, THEN def_fix_ind])
19742 86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	81	apply simp_all
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	82	apply (subst lemma5 [symmetric])
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	83	apply (erule monofun_cfun_arg)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	84	done
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	85
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	86	lemma wir_moel': "YS = YYS"
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	87	apply (rule antisym_less)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	88	apply (rule lemma7)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	89	apply (rule lemma6)
86f21beabafc removed legacy ML scripts; wenzelm parents: 17291 diff changeset	90	done
17291 94f6113fe9ed converted to Isar theory format; wenzelm parents: 10835 diff changeset	91
2570 24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	92	end

author	blanchet
	Fri, 03 Sep 2010 13:45:12 +0200
changeset 39111	2e9bdc6fbedf
parent 35948	5e7909f0346b
child 40431	682d6c455670
permissions	-rw-r--r--