isabelle: src/LCF/ex/Ex2.thy@7d0962594902 (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 {* Example 3.8 *}
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	5
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	6	theory Ex2
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	F :: "'a => 'a"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	13	G :: "'a => 'a"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	14	H :: "'a => 'b => 'b"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	15	K :: "('a => 'b => 'b) => ('a => 'b => 'b)"
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	16
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	17	axioms
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	18	F_strict: "F(UU) = UU"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	19	K: "K = (%h x y. P(x) => y \| F(h(G(x),y)))"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	20	H: "H = FIX(K)"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	21
19755 90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	22	declare F_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 example: "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))"
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 (tactic {* induct_tac "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *})
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	27	apply (simp (no_asm))
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	28	apply (simp (no_asm_simp) split: COND_cases_iff)
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	29	done
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	30
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	31	end

author	urbanc
	Wed, 18 Oct 2006 23:15:16 +0200
changeset 21053	7d0962594902
parent 19755	90f80de04c46
child 27208	5fe899199f85
permissions	-rw-r--r--