isabelle: src/LCF/ex/Ex3.thy@aa4bc5a4be1d (annotated)

17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	1	header {* Addition with fixpoint of successor *}
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	2
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	3	theory Ex3
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	s :: "'a => 'a"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	9	p :: "'a => 'a => 'a"
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	10
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	11	axioms
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	12	p_strict: "p(UU) = UU"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	13	p_s: "p(s(x),y) = s(p(x,y))"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	14
19755 90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	15	declare p_strict [simp] p_s [simp]
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	16
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	17	lemma example: "p(FIX(s),y) = FIX(s)"
27208 5fe899199f85 proper context for tactics derived from res_inst_tac; wenzelm parents: 19755 diff changeset	18	apply (tactic {* induct_tac @{context} "s" 1 *})
19755 90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	19	apply (simp (no_asm))
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	20	apply (simp (no_asm))
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	21	done
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	22
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	23	end

author	wenzelm
	Tue, 18 May 2010 00:01:51 +0200
changeset 36972	aa4bc5a4be1d
parent 35762	af3ff2ba4c54
child 47025	b2b8ae61d6ad
permissions	-rw-r--r--