isabelle: src/LCF/ex/Ex4.thy@322bcfce2b37 (annotated)

4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	1
60770 240563fbf41d isabelle update_cartouches; wenzelm parents: 58977 diff changeset	2	section \<open>Prefixpoints\<close>
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
58974 cbc2ac19d783 simplifie sessions; wenzelm parents: 58973 diff changeset	5	imports "../LCF"
17248 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:
58977 9576b510f6a2 more symbols; wenzelm parents: 58974 diff changeset	9	assumes asms: "f(p) << p" "\<And>q. f(q) << q \<Longrightarrow> p << q"
19755 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	Fabian Huch <huch@in.tum.de>
	Fri, 24 Nov 2023 17:24:22 +0100
changeset 79039	322bcfce2b37
parent 60770	240563fbf41d
permissions	-rw-r--r--