isabelle: src/LCF/ex/Ex2.thy@c2ab1a970e82 (annotated)

60770 240563fbf41d isabelle update_cartouches; wenzelm parents: 58977 diff changeset	1	section \<open>Example 3.8\<close>
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	2
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	3	theory Ex2
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	P :: "'a \<Rightarrow> tr" and
9576b510f6a2 more symbols; wenzelm parents: 58974 diff changeset	9	F :: "'b \<Rightarrow> 'b" and
9576b510f6a2 more symbols; wenzelm parents: 58974 diff changeset	10	G :: "'a \<Rightarrow> 'a" and
9576b510f6a2 more symbols; wenzelm parents: 58974 diff changeset	11	H :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and
9576b510f6a2 more symbols; wenzelm parents: 58974 diff changeset	12	K :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'b)"
47025 b2b8ae61d6ad modernized axiomatizations; wenzelm parents: 35762 diff changeset	13	where
b2b8ae61d6ad modernized axiomatizations; wenzelm parents: 35762 diff changeset	14	F_strict: "F(UU) = UU" and
58977 9576b510f6a2 more symbols; wenzelm parents: 58974 diff changeset	15	K: "K = (\<lambda>h x y. P(x) \<Rightarrow> y \| F(h(G(x),y)))" and
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	16	H: "H = FIX(K)"
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 F_strict [simp] K [simp]
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	19
58977 9576b510f6a2 more symbols; wenzelm parents: 58974 diff changeset	20	lemma example: "\<forall>x. F(H(x::'a,y::'b)) = H(x,F(y))"
19755 90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	21	apply (simplesubst H)
58977 9576b510f6a2 more symbols; wenzelm parents: 58974 diff changeset	22	apply (induct "K:: ('a\<Rightarrow>'b\<Rightarrow>'b) \<Rightarrow> ('a\<Rightarrow>'b\<Rightarrow>'b)")
47025 b2b8ae61d6ad modernized axiomatizations; wenzelm parents: 35762 diff changeset	23	apply simp
b2b8ae61d6ad modernized axiomatizations; wenzelm parents: 35762 diff changeset	24	apply (simp split: COND_cases_iff)
19755 90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	25	done
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	26
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	27	end

author	wenzelm
	Sat, 27 Feb 2021 21:36:58 +0100
changeset 73323	c2ab1a970e82
parent 60770	240563fbf41d
permissions	-rw-r--r--