isabelle: src/LCF/ex/Ex4.thy@2a683fb686fd (annotated)

4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	1
58889 5b7a9633cfa8 modernized header uniformly as section; wenzelm parents: 27208 diff changeset	2	section {* Prefixpoints *}
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	3
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	4	theory Ex4
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	5	imports LCF
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	6	begin
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	7
19755 90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	8	lemma example:
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	9	assumes asms: "f(p) << p" "!!q. f(q) << q ==> p << q"
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	10	shows "FIX(f)=p"
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	11	apply (unfold eq_def)
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	12	apply (rule conjI)
58973 2a683fb686fd more Isar proof methods; wenzelm parents: 58889 diff changeset	13	apply (induct f)
19755 90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	14	apply (rule minimal)
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	15	apply (intro strip)
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	16	apply (rule less_trans)
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	17	prefer 2
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	18	apply (rule asms)
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	19	apply (erule less_ap_term)
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	20	apply (rule asms)
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	21	apply (rule FIX_eq [THEN eq_imp_less1])
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	22	done
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	23
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	24	end

author	wenzelm
	Tue, 11 Nov 2014 11:47:53 +0100
changeset 58973	2a683fb686fd
parent 58889	5b7a9633cfa8
child 58974	cbc2ac19d783
permissions	-rw-r--r--