src/LCF/ex/Ex1.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>Section 10.4\<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 Ex1
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
  G     :: "'a \<Rightarrow> 'a" and
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
    10
  H     :: "'a \<Rightarrow> 'a" and
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
    11
  K     :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
47025
b2b8ae61d6ad modernized axiomatizations;
wenzelm
parents: 35762
diff changeset
    12
where
b2b8ae61d6ad modernized axiomatizations;
wenzelm
parents: 35762
diff changeset
    13
  P_strict:     "P(UU) = UU" and
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
    14
  K:            "K = (\<lambda>h x. P(x) \<Rightarrow> x | h(h(G(x))))" and
17248
81bf91654e73 converted to Isar theory format;
wenzelm
parents: 4905
diff changeset
    15
  H:            "H = FIX(K)"
81bf91654e73 converted to Isar theory format;
wenzelm
parents: 4905
diff changeset
    16
19755
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    17
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    18
declare P_strict [simp] K [simp]
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    19
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    20
lemma H_unfold: "H = K(H)"
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    21
  apply (simplesubst H)
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    22
  apply (rule FIX_eq [symmetric])
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    23
  done
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    24
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    25
lemma H_strict [simp]: "H(UU)=UU"
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    26
  apply (simplesubst H_unfold)
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    27
  apply simp
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    28
  done
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    29
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
    30
lemma H_idemp_lemma: "\<forall>x. H(FIX(K,x)) = FIX(K,x)"
58973
2a683fb686fd more Isar proof methods;
wenzelm
parents: 58889
diff changeset
    31
  apply (induct K)
47025
b2b8ae61d6ad modernized axiomatizations;
wenzelm
parents: 35762
diff changeset
    32
  apply simp
b2b8ae61d6ad modernized axiomatizations;
wenzelm
parents: 35762
diff changeset
    33
  apply (simp split: COND_cases_iff)
19755
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    34
  apply (intro strip)
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    35
  apply (subst H_unfold)
47025
b2b8ae61d6ad modernized axiomatizations;
wenzelm
parents: 35762
diff changeset
    36
  apply simp
19755
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    37
  done
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    38
58977
9576b510f6a2 more symbols;
wenzelm
parents: 58974
diff changeset
    39
lemma H_idemp: "\<forall>x. H(H(x)) = H(x)"
19755
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    40
  apply (rule H_idemp_lemma [folded H])
90f80de04c46 removed obsolete ML files;
wenzelm
parents: 17248
diff changeset
    41
  done
4905
be73ddff6c5a proper thy files;
wenzelm
parents:
diff changeset
    42
be73ddff6c5a proper thy files;
wenzelm
parents:
diff changeset
    43
end