src/LCF/ex/Ex1.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@58889
     1
section {*  Section 10.4 *}
wenzelm@4905
     2
wenzelm@17248
     3
theory Ex1
wenzelm@58974
     4
imports "../LCF"
wenzelm@17248
     5
begin
wenzelm@4905
     6
wenzelm@47025
     7
axiomatization
wenzelm@58977
     8
  P     :: "'a \<Rightarrow> tr" and
wenzelm@58977
     9
  G     :: "'a \<Rightarrow> 'a" and
wenzelm@58977
    10
  H     :: "'a \<Rightarrow> 'a" and
wenzelm@58977
    11
  K     :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
wenzelm@47025
    12
where
wenzelm@47025
    13
  P_strict:     "P(UU) = UU" and
wenzelm@58977
    14
  K:            "K = (\<lambda>h x. P(x) \<Rightarrow> x | h(h(G(x))))" and
wenzelm@17248
    15
  H:            "H = FIX(K)"
wenzelm@17248
    16
wenzelm@19755
    17
wenzelm@19755
    18
declare P_strict [simp] K [simp]
wenzelm@19755
    19
wenzelm@19755
    20
lemma H_unfold: "H = K(H)"
wenzelm@19755
    21
  apply (simplesubst H)
wenzelm@19755
    22
  apply (rule FIX_eq [symmetric])
wenzelm@19755
    23
  done
wenzelm@19755
    24
wenzelm@19755
    25
lemma H_strict [simp]: "H(UU)=UU"
wenzelm@19755
    26
  apply (simplesubst H_unfold)
wenzelm@19755
    27
  apply simp
wenzelm@19755
    28
  done
wenzelm@19755
    29
wenzelm@58977
    30
lemma H_idemp_lemma: "\<forall>x. H(FIX(K,x)) = FIX(K,x)"
wenzelm@58973
    31
  apply (induct K)
wenzelm@47025
    32
  apply simp
wenzelm@47025
    33
  apply (simp split: COND_cases_iff)
wenzelm@19755
    34
  apply (intro strip)
wenzelm@19755
    35
  apply (subst H_unfold)
wenzelm@47025
    36
  apply simp
wenzelm@19755
    37
  done
wenzelm@19755
    38
wenzelm@58977
    39
lemma H_idemp: "\<forall>x. H(H(x)) = H(x)"
wenzelm@19755
    40
  apply (rule H_idemp_lemma [folded H])
wenzelm@19755
    41
  done
wenzelm@4905
    42
wenzelm@4905
    43
end