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;
wenzelm@4905
     1
wenzelm@58889
     2
section {* Prefixpoints *}
wenzelm@4905
     3
wenzelm@17248
     4
theory Ex4
wenzelm@58974
     5
imports "../LCF"
wenzelm@17248
     6
begin
wenzelm@17248
     7
wenzelm@19755
     8
lemma example:
wenzelm@58977
     9
  assumes asms: "f(p) << p"  "\<And>q. f(q) << q \<Longrightarrow> p << q"
wenzelm@19755
    10
  shows "FIX(f)=p"
wenzelm@19755
    11
  apply (unfold eq_def)
wenzelm@19755
    12
  apply (rule conjI)
wenzelm@58973
    13
  apply (induct f)
wenzelm@19755
    14
  apply (rule minimal)
wenzelm@19755
    15
  apply (intro strip)
wenzelm@19755
    16
  apply (rule less_trans)
wenzelm@19755
    17
  prefer 2
wenzelm@19755
    18
  apply (rule asms)
wenzelm@19755
    19
  apply (erule less_ap_term)
wenzelm@19755
    20
  apply (rule asms)
wenzelm@19755
    21
  apply (rule FIX_eq [THEN eq_imp_less1])
wenzelm@19755
    22
  done
wenzelm@19755
    23
wenzelm@17248
    24
end