isabelle: src/LCF/ex/Ex1.thy@b22e44496dc2 (annotated)

4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	1
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	2	(* $Id$ *)
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	3
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	4	header {* Section 10.4 *}
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	5
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	6	theory Ex1
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	7	imports LCF
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	8	begin
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	9
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	10	consts
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	11	P :: "'a => tr"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	12	G :: "'a => 'a"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	13	H :: "'a => 'a"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	14	K :: "('a => 'a) => ('a => 'a)"
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	15
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	16	axioms
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	17	P_strict: "P(UU) = UU"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	18	K: "K = (%h x. P(x) => x \| h(h(G(x))))"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	19	H: "H = FIX(K)"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	20
19755 90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	21
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	22	declare P_strict [simp] K [simp]
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	23
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	24	lemma H_unfold: "H = K(H)"
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	25	apply (simplesubst H)
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	26	apply (rule FIX_eq [symmetric])
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	27	done
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	28
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	29	lemma H_strict [simp]: "H(UU)=UU"
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	30	apply (simplesubst H_unfold)
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	31	apply simp
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	32	done
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	33
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	34	lemma H_idemp_lemma: "ALL x. H(FIX(K,x)) = FIX(K,x)"
27208 5fe899199f85 proper context for tactics derived from res_inst_tac; wenzelm parents: 19755 diff changeset	35	apply (tactic {* induct_tac @{context} "K" 1 *})
19755 90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	36	apply (simp (no_asm))
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	37	apply (simp (no_asm) split: COND_cases_iff)
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	38	apply (intro strip)
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	39	apply (subst H_unfold)
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	40	apply (simp (no_asm_simp))
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	41	done
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	42
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	43	lemma H_idemp: "ALL x. H(H(x)) = H(x)"
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	44	apply (rule H_idemp_lemma [folded H])
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	45	done
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	46
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	47	end

author	haftmann
	Tue, 20 Oct 2009 16:13:01 +0200
changeset 33037	b22e44496dc2
parent 27208	5fe899199f85
child 35762	af3ff2ba4c54
permissions	-rw-r--r--