isabelle: src/LCF/ex/Ex3.thy@629f3a92863e (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)"
27208 5fe899199f85 proper context for tactics derived from res_inst_tac; wenzelm parents: 19755 diff changeset	21	apply (tactic {* induct_tac @{context} "s" 1 *})
19755 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	immler@in.tum.de
	Thu, 26 Feb 2009 10:13:43 +0100
changeset 30151	629f3a92863e
parent 27208	5fe899199f85
child 35762	af3ff2ba4c54
permissions	-rw-r--r--