src/HOL/HOLCF/ex/Dagstuhl.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 41413 64cd30d6b0b8
child 63549 b0d31c7def86
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
     1
theory Dagstuhl
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 40945
diff changeset
     2
imports "~~/src/HOL/HOLCF/Library/Stream"
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
     3
begin
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     4
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 21404
diff changeset
     5
axiomatization
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
     6
  y  :: "'a"
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     7
19763
wenzelm
parents: 19742
diff changeset
     8
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19763
diff changeset
     9
  YS :: "'a stream" where
19763
wenzelm
parents: 19742
diff changeset
    10
  "YS = fix$(LAM x. y && x)"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19763
diff changeset
    11
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19763
diff changeset
    12
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19763
diff changeset
    13
  YYS :: "'a stream" where
19763
wenzelm
parents: 19742
diff changeset
    14
  "YYS = fix$(LAM z. y && y && z)"
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    15
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    16
lemma YS_def2: "YS = y && YS"
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    17
  apply (rule trans)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    18
  apply (rule fix_eq2)
19763
wenzelm
parents: 19742
diff changeset
    19
  apply (rule YS_def [THEN eq_reflection])
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    20
  apply (rule beta_cfun)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    21
  apply simp
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    22
  done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    23
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    24
lemma YYS_def2: "YYS = y && y && YYS"
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    25
  apply (rule trans)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    26
  apply (rule fix_eq2)
19763
wenzelm
parents: 19742
diff changeset
    27
  apply (rule YYS_def [THEN eq_reflection])
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    28
  apply (rule beta_cfun)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    29
  apply simp
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    30
  done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    31
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    32
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    33
lemma lemma3: "YYS << y && YYS"
19763
wenzelm
parents: 19742
diff changeset
    34
  apply (rule YYS_def [THEN eq_reflection, THEN def_fix_ind])
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    35
  apply simp_all
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    36
  apply (rule monofun_cfun_arg)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    37
  apply (rule monofun_cfun_arg)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    38
  apply assumption
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    39
  done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    40
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    41
lemma lemma4: "y && YYS << YYS"
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    42
  apply (subst YYS_def2)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    43
  back
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    44
  apply (rule monofun_cfun_arg)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    45
  apply (rule lemma3)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    46
  done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    47
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    48
lemma lemma5: "y && YYS = YYS"
40431
682d6c455670 discontinue a bunch of legacy theorem names
huffman
parents: 35948
diff changeset
    49
  apply (rule below_antisym)
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    50
  apply (rule lemma4)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    51
  apply (rule lemma3)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    52
  done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    53
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    54
lemma wir_moel: "YS = YYS"
35642
f478d5a9d238 generate separate qualified theorem name for each type's reach and take_lemma
huffman
parents: 35174
diff changeset
    55
  apply (rule stream.take_lemma)
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    56
  apply (induct_tac n)
35169
31cbcb019003 fix warnings about duplicate simp rules
huffman
parents: 25135
diff changeset
    57
  apply (simp (no_asm))
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    58
  apply (subst YS_def2)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    59
  apply (subst YYS_def2)
35169
31cbcb019003 fix warnings about duplicate simp rules
huffman
parents: 25135
diff changeset
    60
  apply simp
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    61
  apply (rule lemma5 [symmetric, THEN subst])
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    62
  apply (rule refl)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    63
  done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    64
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    65
(* ------------------------------------------------------------------------ *)
40945
b8703f63bfb2 recoded latin1 as utf8;
wenzelm
parents: 40774
diff changeset
    66
(* Zweite L"osung: Bernhard Möller                                          *)
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    67
(* statt Beweis von  wir_moel "uber take_lemma beidseitige Inclusion        *)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    68
(* verwendet lemma5                                                         *)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    69
(* ------------------------------------------------------------------------ *)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    70
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    71
lemma lemma6: "YYS << YS"
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    72
  apply (unfold YYS_def)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    73
  apply (rule fix_least)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    74
  apply (subst beta_cfun)
35948
5e7909f0346b remove ancient continuity tactic
huffman
parents: 35642
diff changeset
    75
  apply simp
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    76
  apply (simp add: YS_def2 [symmetric])
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    77
  done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    78
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    79
lemma lemma7: "YS << YYS"
19763
wenzelm
parents: 19742
diff changeset
    80
  apply (rule YS_def [THEN eq_reflection, THEN def_fix_ind])
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    81
  apply simp_all
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    82
  apply (subst lemma5 [symmetric])
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    83
  apply (erule monofun_cfun_arg)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    84
  done
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    85
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    86
lemma wir_moel': "YS = YYS"
40431
682d6c455670 discontinue a bunch of legacy theorem names
huffman
parents: 35948
diff changeset
    87
  apply (rule below_antisym)
19742
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    88
  apply (rule lemma7)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    89
  apply (rule lemma6)
86f21beabafc removed legacy ML scripts;
wenzelm
parents: 17291
diff changeset
    90
  done
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 10835
diff changeset
    91
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    92
end