src/HOLCF/ex/Dagstuhl.thy
 author huffman Sun Mar 07 16:39:31 2010 -0800 (2010-03-07) changeset 35642 f478d5a9d238 parent 35174 e15040ae75d7 child 35948 5e7909f0346b permissions -rw-r--r--
generate separate qualified theorem name for each type's reach and take_lemma
```     1 theory Dagstuhl
```
```     2 imports 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 antisym_less)
```
```    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 (tactic "cont_tacR 1")
```
```    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 antisym_less)
```
```    88   apply (rule lemma7)
```
```    89   apply (rule lemma6)
```
```    90   done
```
```    91
```
```    92 end
```