src/LCF/ex/Ex4.thy
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 58977 9576b510f6a2
child 60770 240563fbf41d
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
     1 
     2 section {* Prefixpoints *}
     3 
     4 theory Ex4
     5 imports "../LCF"
     6 begin
     7 
     8 lemma example:
     9   assumes asms: "f(p) << p"  "\<And>q. f(q) << q \<Longrightarrow> p << q"
    10   shows "FIX(f)=p"
    11   apply (unfold eq_def)
    12   apply (rule conjI)
    13   apply (induct f)
    14   apply (rule minimal)
    15   apply (intro strip)
    16   apply (rule less_trans)
    17   prefer 2
    18   apply (rule asms)
    19   apply (erule less_ap_term)
    20   apply (rule asms)
    21   apply (rule FIX_eq [THEN eq_imp_less1])
    22   done
    23 
    24 end