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

58889 5b7a9633cfa8 modernized header uniformly as section; wenzelm parents: 47025 diff changeset	1	section {* 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
58974 cbc2ac19d783 simplifie sessions; wenzelm parents: 58973 diff changeset	4	imports "../LCF"
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	5	begin
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	6
47025 b2b8ae61d6ad modernized axiomatizations; wenzelm parents: 35762 diff changeset	7	axiomatization
58977 9576b510f6a2 more symbols; wenzelm parents: 58974 diff changeset	8	s :: "'a \<Rightarrow> 'a" and
9576b510f6a2 more symbols; wenzelm parents: 58974 diff changeset	9	p :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
47025 b2b8ae61d6ad modernized axiomatizations; wenzelm parents: 35762 diff changeset	10	where
b2b8ae61d6ad modernized axiomatizations; wenzelm parents: 35762 diff changeset	11	p_strict: "p(UU) = UU" and
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	12	p_s: "p(s(x),y) = s(p(x,y))"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	13
19755 90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	14	declare p_strict [simp] p_s [simp]
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	15
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	16	lemma example: "p(FIX(s),y) = FIX(s)"
58973 2a683fb686fd more Isar proof methods; wenzelm parents: 58889 diff changeset	17	apply (induct s)
47025 b2b8ae61d6ad modernized axiomatizations; wenzelm parents: 35762 diff changeset	18	apply simp
b2b8ae61d6ad modernized axiomatizations; wenzelm parents: 35762 diff changeset	19	apply simp
19755 90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	20	done
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	21
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	22	end

author	wenzelm
	Tue, 11 Nov 2014 15:55:31 +0100
changeset 58977	9576b510f6a2
parent 58974	cbc2ac19d783
child 60770	240563fbf41d
permissions	-rw-r--r--