src/LCF/ex/Ex2.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 {* Example 3.8 *}
wenzelm@4905
     2
wenzelm@17248
     3
theory Ex2
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
  F     :: "'b \<Rightarrow> 'b" and
wenzelm@58977
    10
  G     :: "'a \<Rightarrow> 'a" and
wenzelm@58977
    11
  H     :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and
wenzelm@58977
    12
  K     :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'b)"
wenzelm@47025
    13
where
wenzelm@47025
    14
  F_strict:     "F(UU) = UU" and
wenzelm@58977
    15
  K:            "K = (\<lambda>h x y. P(x) \<Rightarrow> y | F(h(G(x),y)))" and
wenzelm@17248
    16
  H:            "H = FIX(K)"
wenzelm@17248
    17
wenzelm@19755
    18
declare F_strict [simp] K [simp]
wenzelm@19755
    19
wenzelm@58977
    20
lemma example: "\<forall>x. F(H(x::'a,y::'b)) = H(x,F(y))"
wenzelm@19755
    21
  apply (simplesubst H)
wenzelm@58977
    22
  apply (induct "K:: ('a\<Rightarrow>'b\<Rightarrow>'b) \<Rightarrow> ('a\<Rightarrow>'b\<Rightarrow>'b)")
wenzelm@47025
    23
  apply simp
wenzelm@47025
    24
  apply (simp split: COND_cases_iff)
wenzelm@19755
    25
  done
wenzelm@4905
    26
wenzelm@4905
    27
end