isabelle: src/LCF/ex/Ex3.thy@27ea2ba48fa3 (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 {* Addition with fixpoint of successor *}
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	5
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	6	theory Ex3
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	s :: "'a => 'a"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	12	p :: "'a => 'a => 'a"
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	p_strict: "p(UU) = UU"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	16	p_s: "p(s(x),y) = s(p(x,y))"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	17
19755 90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	18	declare p_strict [simp] p_s [simp]
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	19
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	20	lemma example: "p(FIX(s),y) = FIX(s)"
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	21	apply (tactic {* induct_tac "s" 1 *})
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	22	apply (simp (no_asm))
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	23	apply (simp (no_asm))
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	24	done
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	25
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	26	end

author	wenzelm
	Thu, 31 Aug 2006 22:55:49 +0200
changeset 20451	27ea2ba48fa3
parent 19755	90f80de04c46
child 27208	5fe899199f85
permissions	-rw-r--r--