isabelle: src/HOL/HOLCF/ex/Dnat.thy@b7cfe12acf2e (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 40774 diff changeset	1	(* Title: HOL/HOLCF/ex/Dnat.thy
2570 24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	2	Author: Franz Regensburger
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	3
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	4	Theory for the domain of natural numbers dnat = one ++ dnat
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	5	*)
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	6
27108 e447b3107696 whitespace tuning haftmann parents: 21404 diff changeset	7	theory Dnat
e447b3107696 whitespace tuning haftmann parents: 21404 diff changeset	8	imports HOLCF
e447b3107696 whitespace tuning haftmann parents: 21404 diff changeset	9	begin
2570 24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	10
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	11	domain dnat = dzero \| dsucc (dpred :: dnat)
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	12
19763 ec18656a2c10 tuned; wenzelm parents: 19550 diff changeset	13	definition
21404 eb85850d3eb7 more robust syntax for definition/abbreviation/notation; wenzelm parents: 19764 diff changeset	14	iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" where
19763 ec18656a2c10 tuned; wenzelm parents: 19550 diff changeset	15	"iterator = fix $ (LAM h n f x.
12035 f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	16	case n of dzero => x
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	17	\| dsucc $ m => f $ (h $ m $ f $ x))"
2570 24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	18
12035 f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	19	text {*
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	20	\medskip Expand fixed point properties.
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	21	*}
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	22
19764 372065f34795 removed obsolete ML files; wenzelm parents: 19763 diff changeset	23	lemma iterator_def2:
372065f34795 removed obsolete ML files; wenzelm parents: 19763 diff changeset	24	"iterator = (LAM n f x. case n of dzero => x \| dsucc$m => f$(iterator$m$f$x))"
372065f34795 removed obsolete ML files; wenzelm parents: 19763 diff changeset	25	apply (rule trans)
372065f34795 removed obsolete ML files; wenzelm parents: 19763 diff changeset	26	apply (rule fix_eq2)
372065f34795 removed obsolete ML files; wenzelm parents: 19763 diff changeset	27	apply (rule iterator_def [THEN eq_reflection])
372065f34795 removed obsolete ML files; wenzelm parents: 19763 diff changeset	28	apply (rule beta_cfun)
372065f34795 removed obsolete ML files; wenzelm parents: 19763 diff changeset	29	apply simp
372065f34795 removed obsolete ML files; wenzelm parents: 19763 diff changeset	30	done
12035 f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	31
19764 372065f34795 removed obsolete ML files; wenzelm parents: 19763 diff changeset	32	text {* \medskip Recursive properties. *}
12035 f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	33
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	34	lemma iterator1: "iterator $ UU $ f $ x = UU"
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	35	apply (subst iterator_def2)
35169 31cbcb019003 fix warnings about duplicate simp rules huffman parents: 27108 diff changeset	36	apply simp
12035 f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	37	done
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	38
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	39	lemma iterator2: "iterator $ dzero $ f $ x = x"
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	40	apply (subst iterator_def2)
35169 31cbcb019003 fix warnings about duplicate simp rules huffman parents: 27108 diff changeset	41	apply simp
12035 f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	42	done
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	43
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	44	lemma iterator3: "n ~= UU ==> iterator $ (dsucc $ n) $ f $ x = f $ (iterator $ n $ f $ x)"
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	45	apply (rule trans)
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	46	apply (subst iterator_def2)
35169 31cbcb019003 fix warnings about duplicate simp rules huffman parents: 27108 diff changeset	47	apply simp
12035 f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	48	apply (rule refl)
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	49	done
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	50
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	51	lemmas iterator_rews = iterator1 iterator2 iterator3
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	52
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	53	lemma dnat_flat: "ALL x y::dnat. x<<y --> x=UU \| x=y"
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	54	apply (rule allI)
35781 b7738ab762b1 renamed some lemmas generated by the domain package huffman parents: 35532 diff changeset	55	apply (induct_tac x)
12035 f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	56	apply fast
f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	57	apply (rule allI)
35532 60647586b173 adapt to changed variable name in casedist theorem huffman parents: 35443 diff changeset	58	apply (case_tac y)
19550 ae77a20f6995 update to reflect changes in inverts/injects lemmas huffman parents: 16417 diff changeset	59	apply simp
12035 f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	60	apply simp
35169 31cbcb019003 fix warnings about duplicate simp rules huffman parents: 27108 diff changeset	61	apply simp
12035 f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	62	apply (rule allI)
35532 60647586b173 adapt to changed variable name in casedist theorem huffman parents: 35443 diff changeset	63	apply (case_tac y)
45049 13efaee97111 discontinued HOLCF legacy theorem names huffman parents: 42151 diff changeset	64	apply (fast intro!: bottomI)
35443 2e0f9516947e change domain package's treatment of variable names in theorems to be like datatype package huffman parents: 35169 diff changeset	65	apply (thin_tac "ALL y. dnat << y --> dnat = UU \| dnat = y")
35169 31cbcb019003 fix warnings about duplicate simp rules huffman parents: 27108 diff changeset	66	apply simp
31cbcb019003 fix warnings about duplicate simp rules huffman parents: 27108 diff changeset	67	apply (simp (no_asm_simp))
35443 2e0f9516947e change domain package's treatment of variable names in theorems to be like datatype package huffman parents: 35169 diff changeset	68	apply (drule_tac x="dnata" in spec)
19550 ae77a20f6995 update to reflect changes in inverts/injects lemmas huffman parents: 16417 diff changeset	69	apply simp
12035 f2ee4b5d02f2 converted theory Dnat; wenzelm parents: 10835 diff changeset	70	done
2570 24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	71
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	72	end

author	wenzelm
	Mon, 19 Jan 2015 20:39:01 +0100
changeset 59409	b7cfe12acf2e
parent 45049	13efaee97111
child 62175	8ffc4d0e652d
permissions	-rw-r--r--