src/HOL/HOLCF/ex/Dagstuhl.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 40945 b8703f63bfb2
child 63549 b0d31c7def86
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
wenzelm@17291
     1
theory Dagstuhl
wenzelm@41413
     2
imports "~~/src/HOL/HOLCF/Library/Stream"
wenzelm@17291
     3
begin
oheimb@2570
     4
wenzelm@25135
     5
axiomatization
wenzelm@17291
     6
  y  :: "'a"
oheimb@2570
     7
wenzelm@19763
     8
definition
wenzelm@21404
     9
  YS :: "'a stream" where
wenzelm@19763
    10
  "YS = fix$(LAM x. y && x)"
wenzelm@21404
    11
wenzelm@21404
    12
definition
wenzelm@21404
    13
  YYS :: "'a stream" where
wenzelm@19763
    14
  "YYS = fix$(LAM z. y && y && z)"
oheimb@2570
    15
wenzelm@19742
    16
lemma YS_def2: "YS = y && YS"
wenzelm@19742
    17
  apply (rule trans)
wenzelm@19742
    18
  apply (rule fix_eq2)
wenzelm@19763
    19
  apply (rule YS_def [THEN eq_reflection])
wenzelm@19742
    20
  apply (rule beta_cfun)
wenzelm@19742
    21
  apply simp
wenzelm@19742
    22
  done
wenzelm@19742
    23
wenzelm@19742
    24
lemma YYS_def2: "YYS = y && y && YYS"
wenzelm@19742
    25
  apply (rule trans)
wenzelm@19742
    26
  apply (rule fix_eq2)
wenzelm@19763
    27
  apply (rule YYS_def [THEN eq_reflection])
wenzelm@19742
    28
  apply (rule beta_cfun)
wenzelm@19742
    29
  apply simp
wenzelm@19742
    30
  done
wenzelm@19742
    31
wenzelm@19742
    32
wenzelm@19742
    33
lemma lemma3: "YYS << y && YYS"
wenzelm@19763
    34
  apply (rule YYS_def [THEN eq_reflection, THEN def_fix_ind])
wenzelm@19742
    35
  apply simp_all
wenzelm@19742
    36
  apply (rule monofun_cfun_arg)
wenzelm@19742
    37
  apply (rule monofun_cfun_arg)
wenzelm@19742
    38
  apply assumption
wenzelm@19742
    39
  done
wenzelm@19742
    40
wenzelm@19742
    41
lemma lemma4: "y && YYS << YYS"
wenzelm@19742
    42
  apply (subst YYS_def2)
wenzelm@19742
    43
  back
wenzelm@19742
    44
  apply (rule monofun_cfun_arg)
wenzelm@19742
    45
  apply (rule lemma3)
wenzelm@19742
    46
  done
wenzelm@19742
    47
wenzelm@19742
    48
lemma lemma5: "y && YYS = YYS"
huffman@40431
    49
  apply (rule below_antisym)
wenzelm@19742
    50
  apply (rule lemma4)
wenzelm@19742
    51
  apply (rule lemma3)
wenzelm@19742
    52
  done
wenzelm@19742
    53
wenzelm@19742
    54
lemma wir_moel: "YS = YYS"
huffman@35642
    55
  apply (rule stream.take_lemma)
wenzelm@19742
    56
  apply (induct_tac n)
huffman@35169
    57
  apply (simp (no_asm))
wenzelm@19742
    58
  apply (subst YS_def2)
wenzelm@19742
    59
  apply (subst YYS_def2)
huffman@35169
    60
  apply simp
wenzelm@19742
    61
  apply (rule lemma5 [symmetric, THEN subst])
wenzelm@19742
    62
  apply (rule refl)
wenzelm@19742
    63
  done
wenzelm@19742
    64
wenzelm@19742
    65
(* ------------------------------------------------------------------------ *)
wenzelm@40945
    66
(* Zweite L"osung: Bernhard Möller                                          *)
wenzelm@19742
    67
(* statt Beweis von  wir_moel "uber take_lemma beidseitige Inclusion        *)
wenzelm@19742
    68
(* verwendet lemma5                                                         *)
wenzelm@19742
    69
(* ------------------------------------------------------------------------ *)
wenzelm@19742
    70
wenzelm@19742
    71
lemma lemma6: "YYS << YS"
wenzelm@19742
    72
  apply (unfold YYS_def)
wenzelm@19742
    73
  apply (rule fix_least)
wenzelm@19742
    74
  apply (subst beta_cfun)
huffman@35948
    75
  apply simp
wenzelm@19742
    76
  apply (simp add: YS_def2 [symmetric])
wenzelm@19742
    77
  done
wenzelm@19742
    78
wenzelm@19742
    79
lemma lemma7: "YS << YYS"
wenzelm@19763
    80
  apply (rule YS_def [THEN eq_reflection, THEN def_fix_ind])
wenzelm@19742
    81
  apply simp_all
wenzelm@19742
    82
  apply (subst lemma5 [symmetric])
wenzelm@19742
    83
  apply (erule monofun_cfun_arg)
wenzelm@19742
    84
  done
wenzelm@19742
    85
wenzelm@19742
    86
lemma wir_moel': "YS = YYS"
huffman@40431
    87
  apply (rule below_antisym)
wenzelm@19742
    88
  apply (rule lemma7)
wenzelm@19742
    89
  apply (rule lemma6)
wenzelm@19742
    90
  done
wenzelm@17291
    91
oheimb@2570
    92
end