src/LCF/ex/Ex4.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 27208 5fe899199f85
child 58973 2a683fb686fd
permissions -rw-r--r--
modernized header uniformly as section;
     1 
     2 section {* Prefixpoints *}
     3 
     4 theory Ex4
     5 imports LCF
     6 begin
     7 
     8 lemma example:
     9   assumes asms: "f(p) << p"  "!!q. f(q) << q ==> p << q"
    10   shows "FIX(f)=p"
    11   apply (unfold eq_def)
    12   apply (rule conjI)
    13   apply (tactic {* induct_tac @{context} "f" 1 *})
    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