author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45214  66ba67adafab 
child 50055  94041d602ecb 
permissions  rwrr 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

1 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

2 
(* Author: Lukas Bulwahn, TU Muenchen *) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

3 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

4 
header {* Lazy sequences *} 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

5 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

6 
theory Lazy_Sequence 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

7 
imports List Code_Numeral 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

8 
begin 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

9 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

10 
datatype 'a lazy_sequence = Empty  Insert 'a "'a lazy_sequence" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

11 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

12 
definition Lazy_Sequence :: "(unit => ('a * 'a lazy_sequence) option) => 'a lazy_sequence" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

13 
where 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

14 
"Lazy_Sequence f = (case f () of None => Empty  Some (x, xq) => Insert x xq)" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

15 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

16 
code_datatype Lazy_Sequence 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

17 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

18 
primrec yield :: "'a lazy_sequence => ('a * 'a lazy_sequence) option" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

19 
where 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

20 
"yield Empty = None" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

21 
 "yield (Insert x xq) = Some (x, xq)" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

22 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

23 
lemma [simp]: "yield xq = Some (x, xq') ==> size xq' < size xq" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

24 
by (cases xq) auto 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

25 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

26 
lemma yield_Seq [code]: 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

27 
"yield (Lazy_Sequence f) = f ()" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

28 
unfolding Lazy_Sequence_def by (cases "f ()") auto 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

29 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

30 
lemma Seq_yield: 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

31 
"Lazy_Sequence (%u. yield f) = f" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

32 
unfolding Lazy_Sequence_def by (cases f) auto 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

33 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

34 
lemma lazy_sequence_size_code [code]: 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

35 
"lazy_sequence_size s xq = (case yield xq of None => 0  Some (x, xq') => s x + lazy_sequence_size s xq' + 1)" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

36 
by (cases xq) auto 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

37 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

38 
lemma size_code [code]: 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

39 
"size xq = (case yield xq of None => 0  Some (x, xq') => size xq' + 1)" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

40 
by (cases xq) auto 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

41 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36902
diff
changeset

42 
lemma [code]: "HOL.equal xq yq = (case (yield xq, yield yq) of 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36902
diff
changeset

43 
(None, None) => True  (Some (x, xq'), Some (y, yq')) => (HOL.equal x y) \<and> (HOL.equal xq yq)  _ => False)" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36902
diff
changeset

44 
apply (cases xq) apply (cases yq) apply (auto simp add: equal_eq) 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36902
diff
changeset

45 
apply (cases yq) apply (auto simp add: equal_eq) done 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36902
diff
changeset

46 

97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36902
diff
changeset

47 
lemma [code nbe]: 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36902
diff
changeset

48 
"HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36902
diff
changeset

49 
by (fact equal_refl) 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

50 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

51 
lemma seq_case [code]: 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

52 
"lazy_sequence_case f g xq = (case (yield xq) of None => f  Some (x, xq') => g x xq')" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

53 
by (cases xq) auto 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

54 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

55 
lemma [code]: "lazy_sequence_rec f g xq = (case (yield xq) of None => f  Some (x, xq') => g x xq' (lazy_sequence_rec f g xq'))" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

56 
by (cases xq) auto 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

57 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

58 
definition empty :: "'a lazy_sequence" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

59 
where 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

60 
[code]: "empty = Lazy_Sequence (%u. None)" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

61 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

62 
definition single :: "'a => 'a lazy_sequence" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

63 
where 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

64 
[code]: "single x = Lazy_Sequence (%u. Some (x, empty))" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

65 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

66 
primrec append :: "'a lazy_sequence => 'a lazy_sequence => 'a lazy_sequence" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

67 
where 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

68 
"append Empty yq = yq" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

69 
 "append (Insert x xq) yq = Insert x (append xq yq)" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

70 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

71 
lemma [code]: 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

72 
"append xq yq = Lazy_Sequence (%u. case yield xq of 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

73 
None => yield yq 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

74 
 Some (x, xq') => Some (x, append xq' yq))" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

75 
unfolding Lazy_Sequence_def 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

76 
apply (cases "xq") 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

77 
apply auto 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

78 
apply (cases "yq") 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

79 
apply auto 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

80 
done 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

81 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

82 
primrec flat :: "'a lazy_sequence lazy_sequence => 'a lazy_sequence" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

83 
where 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

84 
"flat Empty = Empty" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

85 
 "flat (Insert xq xqq) = append xq (flat xqq)" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

86 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

87 
lemma [code]: 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

88 
"flat xqq = Lazy_Sequence (%u. case yield xqq of 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

89 
None => None 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

90 
 Some (xq, xqq') => yield (append xq (flat xqq')))" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

91 
apply (cases "xqq") 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

92 
apply (auto simp add: Seq_yield) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

93 
unfolding Lazy_Sequence_def 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

94 
by auto 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

95 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

96 
primrec map :: "('a => 'b) => 'a lazy_sequence => 'b lazy_sequence" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

97 
where 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

98 
"map f Empty = Empty" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

99 
 "map f (Insert x xq) = Insert (f x) (map f xq)" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

100 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

101 
lemma [code]: 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

102 
"map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (f x, map f xq')) (yield xq))" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

103 
apply (cases xq) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

104 
apply (auto simp add: Seq_yield) 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

105 
unfolding Lazy_Sequence_def 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

106 
apply auto 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

107 
done 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

108 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

109 
definition bind :: "'a lazy_sequence => ('a => 'b lazy_sequence) => 'b lazy_sequence" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

110 
where 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

111 
[code]: "bind xq f = flat (map f xq)" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

112 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

113 
definition if_seq :: "bool => unit lazy_sequence" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

114 
where 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

115 
"if_seq b = (if b then single () else empty)" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

116 

36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36030
diff
changeset

117 
function iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a Lazy_Sequence.lazy_sequence" 
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36030
diff
changeset

118 
where 
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36030
diff
changeset

119 
"iterate_upto f n m = Lazy_Sequence.Lazy_Sequence (%u. if n > m then None else Some (f n, iterate_upto f (n + 1) m))" 
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36030
diff
changeset

120 
by pat_completeness auto 
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36030
diff
changeset

121 

0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36030
diff
changeset

122 
termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1  n))") auto 
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36030
diff
changeset

123 

34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

124 
definition not_seq :: "unit lazy_sequence => unit lazy_sequence" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

125 
where 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

126 
"not_seq xq = (case yield xq of None => single ()  Some ((), xq) => empty)" 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

127 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

128 
subsection {* Code setup *} 
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

129 

36533  130 
fun anamorph :: "('a \<Rightarrow> ('b \<times> 'a) option) \<Rightarrow> code_numeral \<Rightarrow> 'a \<Rightarrow> 'b list \<times> 'a" where 
131 
"anamorph f k x = (if k = 0 then ([], x) 

132 
else case f x of None \<Rightarrow> ([], x)  Some (v, y) \<Rightarrow> 

133 
let (vs, z) = anamorph f (k  1) y 

134 
in (v # vs, z))" 

34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

135 

36533  136 
definition yieldn :: "code_numeral \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a list \<times> 'a lazy_sequence" where 
137 
"yieldn = anamorph yield" 

34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

138 

36533  139 
code_reflect Lazy_Sequence 
140 
datatypes lazy_sequence = Lazy_Sequence 

141 
functions map yield yieldn 

34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

142 

40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

143 
subsection {* Generator Sequences *} 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

144 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

145 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

146 
subsubsection {* General lazy sequence operation *} 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

147 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

148 
definition product :: "'a Lazy_Sequence.lazy_sequence \<Rightarrow> 'b Lazy_Sequence.lazy_sequence \<Rightarrow> ('a * 'b) Lazy_Sequence.lazy_sequence" 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

149 
where 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

150 
"product s1 s2 = Lazy_Sequence.bind s1 (%a. Lazy_Sequence.bind s2 (%b. Lazy_Sequence.single (a, b)))" 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

151 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

152 

40056  153 
subsubsection {* Small lazy typeclasses *} 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

154 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

155 
class small_lazy = 
45214  156 
fixes small_lazy :: "code_numeral \<Rightarrow> 'a Lazy_Sequence.lazy_sequence" 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

157 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

158 
instantiation unit :: small_lazy 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

159 
begin 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

160 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

161 
definition "small_lazy d = Lazy_Sequence.single ()" 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

162 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

163 
instance .. 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

164 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

165 
end 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

166 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

167 
instantiation int :: small_lazy 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

168 
begin 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

169 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

170 
text {* maybe optimise this expression > append (single x) xs == cons x xs 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

171 
Performance difference? *} 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

172 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

173 
function small_lazy' :: "int => int => int Lazy_Sequence.lazy_sequence" 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

174 
where "small_lazy' d i = (if d < i then Lazy_Sequence.empty else 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

175 
Lazy_Sequence.append (Lazy_Sequence.single i) (small_lazy' d (i + 1)))" 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

176 
by pat_completeness auto 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

177 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

178 
termination 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

179 
by (relation "measure (%(d, i). nat (d + 1  i))") auto 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

180 

45214  181 
definition "small_lazy d = small_lazy' (Code_Numeral.int_of d) ( (Code_Numeral.int_of d))" 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

182 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

183 
instance .. 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

184 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

185 
end 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

186 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

187 
instantiation prod :: (small_lazy, small_lazy) small_lazy 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

188 
begin 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

189 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

190 
definition 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

191 
"small_lazy d = product (small_lazy d) (small_lazy d)" 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

192 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

193 
instance .. 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

194 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

195 
end 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

196 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

197 
instantiation list :: (small_lazy) small_lazy 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

198 
begin 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

199 

45214  200 
fun small_lazy_list :: "code_numeral => 'a list Lazy_Sequence.lazy_sequence" 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

201 
where 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

202 
"small_lazy_list d = Lazy_Sequence.append (Lazy_Sequence.single []) (if d > 0 then Lazy_Sequence.bind (product (small_lazy (d  1)) (small_lazy (d  1))) (%(x, xs). Lazy_Sequence.single (x # xs)) else Lazy_Sequence.empty)" 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

203 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

204 
instance .. 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

205 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

206 
end 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

207 

36902
c6bae4456741
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents:
36533
diff
changeset

208 
subsection {* With Hit Bound Value *} 
36030  209 
text {* assuming in negative context *} 
210 

42163
392fd6c4669c
renewing specifications in HOL: replacing types by type_synonym
bulwahn
parents:
40056
diff
changeset

211 
type_synonym 'a hit_bound_lazy_sequence = "'a option lazy_sequence" 
36030  212 

213 
definition hit_bound :: "'a hit_bound_lazy_sequence" 

214 
where 

215 
[code]: "hit_bound = Lazy_Sequence (%u. Some (None, empty))" 

216 

217 
definition hb_single :: "'a => 'a hit_bound_lazy_sequence" 

218 
where 

219 
[code]: "hb_single x = Lazy_Sequence (%u. Some (Some x, empty))" 

220 

221 
primrec hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence => 'a hit_bound_lazy_sequence" 

222 
where 

223 
"hb_flat Empty = Empty" 

224 
 "hb_flat (Insert xq xqq) = append (case xq of None => hit_bound  Some xq => xq) (hb_flat xqq)" 

225 

226 
lemma [code]: 

227 
"hb_flat xqq = Lazy_Sequence (%u. case yield xqq of 

228 
None => None 

229 
 Some (xq, xqq') => yield (append (case xq of None => hit_bound  Some xq => xq) (hb_flat xqq')))" 

230 
apply (cases "xqq") 

231 
apply (auto simp add: Seq_yield) 

232 
unfolding Lazy_Sequence_def 

233 
by auto 

234 

235 
primrec hb_map :: "('a => 'b) => 'a hit_bound_lazy_sequence => 'b hit_bound_lazy_sequence" 

236 
where 

237 
"hb_map f Empty = Empty" 

238 
 "hb_map f (Insert x xq) = Insert (Option.map f x) (hb_map f xq)" 

239 

240 
lemma [code]: 

241 
"hb_map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (Option.map f x, hb_map f xq')) (yield xq))" 

242 
apply (cases xq) 

243 
apply (auto simp add: Seq_yield) 

244 
unfolding Lazy_Sequence_def 

245 
apply auto 

246 
done 

247 

248 
definition hb_bind :: "'a hit_bound_lazy_sequence => ('a => 'b hit_bound_lazy_sequence) => 'b hit_bound_lazy_sequence" 

249 
where 

250 
[code]: "hb_bind xq f = hb_flat (hb_map f xq)" 

251 

252 
definition hb_if_seq :: "bool => unit hit_bound_lazy_sequence" 

253 
where 

254 
"hb_if_seq b = (if b then hb_single () else empty)" 

255 

256 
definition hb_not_seq :: "unit hit_bound_lazy_sequence => unit lazy_sequence" 

257 
where 

258 
"hb_not_seq xq = (case yield xq of None => single ()  Some (x, xq) => empty)" 

259 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36049
diff
changeset

260 
hide_type (open) lazy_sequence 
40051
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

261 
hide_const (open) Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

262 
iterate_upto not_seq product 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

263 

b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

264 
hide_fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def 
b6acda4d1c29
added generator_dseq compilation for a sound depthlimited compilation with small value generators
bulwahn
parents:
38857
diff
changeset

265 
iterate_upto.simps product_def if_seq_def not_seq_def 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

266 

2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
diff
changeset

267 
end 