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;
     1 theory Dagstuhl
     2 imports "~~/src/HOL/HOLCF/Library/Stream"
     3 begin
     4 
     5 axiomatization
     6   y  :: "'a"
     7 
     8 definition
     9   YS :: "'a stream" where
    10   "YS = fix$(LAM x. y && x)"
    11 
    12 definition
    13   YYS :: "'a stream" where
    14   "YYS = fix$(LAM z. y && y && z)"
    15 
    16 lemma YS_def2: "YS = y && YS"
    17   apply (rule trans)
    18   apply (rule fix_eq2)
    19   apply (rule YS_def [THEN eq_reflection])
    20   apply (rule beta_cfun)
    21   apply simp
    22   done
    23 
    24 lemma YYS_def2: "YYS = y && y && YYS"
    25   apply (rule trans)
    26   apply (rule fix_eq2)
    27   apply (rule YYS_def [THEN eq_reflection])
    28   apply (rule beta_cfun)
    29   apply simp
    30   done
    31 
    32 
    33 lemma lemma3: "YYS << y && YYS"
    34   apply (rule YYS_def [THEN eq_reflection, THEN def_fix_ind])
    35   apply simp_all
    36   apply (rule monofun_cfun_arg)
    37   apply (rule monofun_cfun_arg)
    38   apply assumption
    39   done
    40 
    41 lemma lemma4: "y && YYS << YYS"
    42   apply (subst YYS_def2)
    43   back
    44   apply (rule monofun_cfun_arg)
    45   apply (rule lemma3)
    46   done
    47 
    48 lemma lemma5: "y && YYS = YYS"
    49   apply (rule below_antisym)
    50   apply (rule lemma4)
    51   apply (rule lemma3)
    52   done
    53 
    54 lemma wir_moel: "YS = YYS"
    55   apply (rule stream.take_lemma)
    56   apply (induct_tac n)
    57   apply (simp (no_asm))
    58   apply (subst YS_def2)
    59   apply (subst YYS_def2)
    60   apply simp
    61   apply (rule lemma5 [symmetric, THEN subst])
    62   apply (rule refl)
    63   done
    64 
    65 (* ------------------------------------------------------------------------ *)
    66 (* Zweite L"osung: Bernhard Möller                                          *)
    67 (* statt Beweis von  wir_moel "uber take_lemma beidseitige Inclusion        *)
    68 (* verwendet lemma5                                                         *)
    69 (* ------------------------------------------------------------------------ *)
    70 
    71 lemma lemma6: "YYS << YS"
    72   apply (unfold YYS_def)
    73   apply (rule fix_least)
    74   apply (subst beta_cfun)
    75   apply simp
    76   apply (simp add: YS_def2 [symmetric])
    77   done
    78 
    79 lemma lemma7: "YS << YYS"
    80   apply (rule YS_def [THEN eq_reflection, THEN def_fix_ind])
    81   apply simp_all
    82   apply (subst lemma5 [symmetric])
    83   apply (erule monofun_cfun_arg)
    84   done
    85 
    86 lemma wir_moel': "YS = YYS"
    87   apply (rule below_antisym)
    88   apply (rule lemma7)
    89   apply (rule lemma6)
    90   done
    91 
    92 end