src/LCF/ex/Ex2.thy
author wenzelm
Mon, 24 Oct 2016 14:05:22 +0200
changeset 64371 213cf4215b40
parent 60770 240563fbf41d
permissions -rw-r--r--
more robust;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58977
diff changeset
     1
section \<open>Example 3.8\<close>
4905
be73ddff6c5a proper thy files;
wenzelm
parents:
diff changeset
     2
17248
81bf91654e73 converted to Isar theory format;
wenzelm
parents: 4905
diff changeset
     3
theory Ex2
58974
cbc2ac19d783 simplifie sessions;
wenzelm
parents: 58973
diff changeset
     4
imports "../LCF"
17248
81bf91654e73 converted to Isar theory format;
wenzelm
parents: 4905
diff changeset
     5
begin
4905
be73ddff6c5a proper thy files;
wenzelm
parents:
diff changeset
     6
47025
b2b8ae61d6ad modernized axiomatizations;
wenzelm
parents: 35762
diff changeset
     7
axiomatization
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
     8
  P     :: "'a \<Rightarrow> tr" and
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
     9
  F     :: "'b \<Rightarrow> 'b" and
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
    10
  G     :: "'a \<Rightarrow> 'a" and
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
    11
  H     :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
    12
  K     :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'b)"
47025
b2b8ae61d6ad modernized axiomatizations;
wenzelm
parents: 35762
diff changeset
    13
where
b2b8ae61d6ad modernized axiomatizations;
wenzelm
parents: 35762
diff changeset
    14
  F_strict:     "F(UU) = UU" and
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
    15
  K:            "K = (\<lambda>h x y. P(x) \<Rightarrow> y | F(h(G(x),y)))" and
17248
81bf91654e73 converted to Isar theory format;
wenzelm
parents: 4905
diff changeset
    16
  H:            "H = FIX(K)"
81bf91654e73 converted to Isar theory format;
wenzelm
parents: 4905
diff changeset
    17
19755
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    18
declare F_strict [simp] K [simp]
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    19
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
    20
lemma example: "\<forall>x. F(H(x::'a,y::'b)) = H(x,F(y))"
19755
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    21
  apply (simplesubst H)
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
    22
  apply (induct "K:: ('a\<Rightarrow>'b\<Rightarrow>'b) \<Rightarrow> ('a\<Rightarrow>'b\<Rightarrow>'b)")
47025
b2b8ae61d6ad modernized axiomatizations;
wenzelm
parents: 35762
diff changeset
    23
  apply simp
b2b8ae61d6ad modernized axiomatizations;
wenzelm
parents: 35762
diff changeset
    24
  apply (simp split: COND_cases_iff)
19755
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    25
  done
4905
be73ddff6c5a proper thy files;
wenzelm
parents:
diff changeset
    26
be73ddff6c5a proper thy files;
wenzelm
parents:
diff changeset
    27
end