isabelle: src/LCF/ex/Ex4.thy@437ca370dbd7 (annotated)

4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	1
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	2	header {* 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)
90f80de04c46 removed obsolete ML files; wenzelm parents: 17248 diff changeset	13	apply (tactic {* induct_tac "f" 1 *})
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
	Mon, 09 Oct 2006 02:19:54 +0200
changeset 20901	437ca370dbd7
parent 19755	90f80de04c46
child 27208	5fe899199f85
permissions	-rw-r--r--