isabelle: src/LCF/ex/Ex2.thy@b48aa3492f0b (annotated)

17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	1	header {* Example 3.8 *}
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	2
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	3	theory Ex2
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	4	imports LCF
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	5	begin
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	6
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	7	consts
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	8	P :: "'a => tr"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	9	F :: "'a => 'a"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	10	G :: "'a => 'a"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	11	H :: "'a => 'b => 'b"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	12	K :: "('a => 'b => 'b) => ('a => 'b => 'b)"
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	13
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	14	axioms
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	15	F_strict: "F(UU) = UU"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	16	K: "K = (%h x y. P(x) => y \| F(h(G(x),y)))"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	17	H: "H = FIX(K)"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	18
19755 90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	19	declare F_strict [simp] K [simp]
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	20
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	21	lemma example: "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))"
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	22	apply (simplesubst H)
27208 5fe899199f85 proper context for tactics derived from res_inst_tac; wenzelm parents: 19755 diff changeset	23	apply (tactic {* induct_tac @{context} "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *})
19755 90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	24	apply (simp (no_asm))
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	25	apply (simp (no_asm_simp) split: COND_cases_iff)
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	26	done
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	27
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	28	end

author	blanchet
	Fri, 27 May 2011 10:30:07 +0200
changeset 43007	b48aa3492f0b
parent 35762	af3ff2ba4c54
child 47025	b2b8ae61d6ad
permissions	-rw-r--r--