isabelle: src/LCF/ex/Ex4.thy@1ffd7eaa778b (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)
27208 5fe899199f85 proper context for tactics derived from res_inst_tac; wenzelm parents: 19755 diff changeset	13	apply (tactic {* induct_tac @{context} "f" 1 *})
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
	Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421	1ffd7eaa778b
parent 27208	5fe899199f85
child 58889	5b7a9633cfa8
permissions	-rw-r--r--