author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 41413  64cd30d6b0b8 
child 63549  b0d31c7def86 
permissions  rwrr 
17291  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  3 
begin 
2570  4 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
21404
diff
changeset

5 
axiomatization 
17291  6 
y :: "'a" 
2570  7 

19763  8 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19763
diff
changeset

9 
YS :: "'a stream" where 
19763  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  14 
"YYS = fix$(LAM z. y && y && z)" 
2570  15 

19742  16 
lemma YS_def2: "YS = y && YS" 
17 
apply (rule trans) 

18 
apply (rule fix_eq2) 

19763  19 
apply (rule YS_def [THEN eq_reflection]) 
19742  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) 

19763  27 
apply (rule YYS_def [THEN eq_reflection]) 
19742  28 
apply (rule beta_cfun) 
29 
apply simp 

30 
done 

31 

32 

33 
lemma lemma3: "YYS << y && YYS" 

19763  34 
apply (rule YYS_def [THEN eq_reflection, THEN def_fix_ind]) 
19742  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" 

40431  49 
apply (rule below_antisym) 
19742  50 
apply (rule lemma4) 
51 
apply (rule lemma3) 

52 
done 

53 

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  56 
apply (induct_tac n) 
35169  57 
apply (simp (no_asm)) 
19742  58 
apply (subst YS_def2) 
59 
apply (subst YYS_def2) 

35169  60 
apply simp 
19742  61 
apply (rule lemma5 [symmetric, THEN subst]) 
62 
apply (rule refl) 

63 
done 

64 

65 
(*  *) 

40945  66 
(* Zweite L"osung: Bernhard MÃ¶ller *) 
19742  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) 

35948  75 
apply simp 
19742  76 
apply (simp add: YS_def2 [symmetric]) 
77 
done 

78 

79 
lemma lemma7: "YS << YYS" 

19763  80 
apply (rule YS_def [THEN eq_reflection, THEN def_fix_ind]) 
19742  81 
apply simp_all 
82 
apply (subst lemma5 [symmetric]) 

83 
apply (erule monofun_cfun_arg) 

84 
done 

85 

86 
lemma wir_moel': "YS = YYS" 

40431  87 
apply (rule below_antisym) 
19742  88 
apply (rule lemma7) 
89 
apply (rule lemma6) 

90 
done 

17291  91 

2570  92 
end 