author  wenzelm 
Wed, 29 Oct 2014 11:19:27 +0100  
changeset 58813  625d04d4fd2a 
parent 57645  ee55e667dedc 
child 58889  5b7a9633cfa8 
permissions  rwrr 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

1 
(* Title: HOL/Quickcheck_Examples/Completeness.thy 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

2 
Author: Lukas Bulwahn 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

3 
Copyright 2012 TU Muenchen 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

4 
*) 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

5 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

6 
header {* Proving completeness of exhaustive generators *} 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

7 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

8 
theory Completeness 
57645  9 
imports Main 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

10 
begin 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

11 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

12 
subsection {* Preliminaries *} 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

13 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

14 
primrec is_some 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

15 
where 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

16 
"is_some (Some t) = True" 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

17 
 "is_some None = False" 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

18 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

19 
lemma is_some_is_not_None: 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

20 
"is_some x \<longleftrightarrow> x \<noteq> None" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

21 
by (cases x) simp_all 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

22 

58813  23 
setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

24 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

25 
subsection {* Defining the size of values *} 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

26 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

27 
hide_const size 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

28 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

29 
class size = 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

30 
fixes size :: "'a => nat" 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

31 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

32 
instantiation int :: size 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

33 
begin 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

34 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

35 
definition size_int :: "int => nat" 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

36 
where 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

37 
"size_int n = nat (abs n)" 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

38 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

39 
instance .. 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

40 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

41 
end 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

42 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

43 
instantiation natural :: size 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

44 
begin 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

45 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

46 
definition size_natural :: "natural => nat" 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

47 
where 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

48 
"size_natural = nat_of_natural" 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

49 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

50 
instance .. 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

51 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

52 
end 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

53 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

54 
instantiation nat :: size 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

55 
begin 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

56 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

57 
definition size_nat :: "nat => nat" 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

58 
where 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

59 
"size_nat n = n" 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

60 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

61 
instance .. 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

62 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

63 
end 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

64 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

65 
instantiation list :: (size) size 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

66 
begin 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

67 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

68 
primrec size_list :: "'a list => nat" 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

69 
where 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

70 
"size [] = 1" 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

71 
 "size (x # xs) = max (size x) (size xs) + 1" 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

72 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

73 
instance .. 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

74 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

75 
end 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

76 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

77 
subsection {* Completeness *} 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

78 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

79 
class complete = exhaustive + size + 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

80 
assumes 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

81 
complete: "(\<exists> v. size v \<le> n \<and> is_some (f v)) \<longleftrightarrow> is_some (exhaustive_class.exhaustive f (natural_of_nat n))" 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

82 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

83 
lemma complete_imp1: 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

84 
"size (v :: 'a :: complete) \<le> n \<Longrightarrow> is_some (f v) \<Longrightarrow> is_some (exhaustive_class.exhaustive f (natural_of_nat n))" 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

85 
by (metis complete) 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

86 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

87 
lemma complete_imp2: 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

88 
assumes "is_some (exhaustive_class.exhaustive f (natural_of_nat n))" 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

89 
obtains v where "size (v :: 'a :: complete) \<le> n" "is_some (f v)" 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

90 
using assms by (metis complete) 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

91 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

92 
subsubsection {* Instance Proofs *} 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

93 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

94 
declare exhaustive_int'.simps [simp del] 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

95 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

96 
lemma complete_exhaustive': 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

97 
"(\<exists> i. j <= i & i <= k & is_some (f i)) \<longleftrightarrow> is_some (Quickcheck_Exhaustive.exhaustive_int' f k j)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

98 
proof (induct rule: Quickcheck_Exhaustive.exhaustive_int'.induct[of _ f k j]) 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

99 
case (1 f d i) 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

100 
show ?case 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

101 
proof (cases "f i") 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

102 
case None 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

103 
from this 1 show ?thesis 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

104 
unfolding exhaustive_int'.simps[of _ _ i] Quickcheck_Exhaustive.orelse_def 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

105 
apply (auto simp add: add1_zle_eq dest: less_imp_le) 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

106 
apply auto 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

107 
done 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

108 
next 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

109 
case Some 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

110 
from this show ?thesis 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

111 
unfolding exhaustive_int'.simps[of _ _ i] Quickcheck_Exhaustive.orelse_def by auto 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

112 
qed 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

113 
qed 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

114 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

115 
instance int :: complete 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

116 
proof 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

117 
fix n f 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

118 
show "(\<exists>v. size (v :: int) \<le> n \<and> is_some (f v)) = is_some (exhaustive_class.exhaustive f (natural_of_nat n))" 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

119 
unfolding exhaustive_int_def complete_exhaustive'[symmetric] 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

120 
apply auto apply (rule_tac x="v" in exI) 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

121 
unfolding size_int_def by (metis abs_le_iff minus_le_iff nat_le_iff)+ 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

122 
qed 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

123 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

124 
declare exhaustive_natural'.simps[simp del] 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

125 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

126 
lemma complete_natural': 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

127 
"(\<exists>n. j \<le> n \<and> n \<le> k \<and> is_some (f n)) = 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

128 
is_some (Quickcheck_Exhaustive.exhaustive_natural' f k j)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

129 
proof (induct rule: exhaustive_natural'.induct[of _ f k j]) 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

130 
case (1 f k j) 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

131 
show "(\<exists>n\<ge>j. n \<le> k \<and> is_some (f n)) = is_some (Quickcheck_Exhaustive.exhaustive_natural' f k j)" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

132 
unfolding exhaustive_natural'.simps [of f k j] Quickcheck_Exhaustive.orelse_def 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

133 
apply (auto split: option.split) 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

134 
apply (auto simp add: less_eq_natural_def less_natural_def 1 [symmetric] dest: Suc_leD) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

135 
apply (metis is_some.simps(2) natural_eqI not_less_eq_eq order_antisym) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

136 
done 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

137 
qed 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

138 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

139 
instance natural :: complete 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

140 
proof 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

141 
fix n f 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

142 
show "(\<exists>v. size (v :: natural) \<le> n \<and> is_some (f v)) \<longleftrightarrow> is_some (exhaustive_class.exhaustive f (natural_of_nat n))" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

143 
unfolding exhaustive_natural_def complete_natural' [symmetric] 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

144 
by (auto simp add: size_natural_def less_eq_natural_def) 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

145 
qed 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

146 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

147 
instance nat :: complete 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

148 
proof 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

149 
fix n f 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

150 
show "(\<exists>v. size (v :: nat) \<le> n \<and> is_some (f v)) \<longleftrightarrow> is_some (exhaustive_class.exhaustive f (natural_of_nat n))" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

151 
unfolding exhaustive_nat_def complete[of n "%x. f (nat_of_natural x)", symmetric] 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

152 
apply auto 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

153 
apply (rule_tac x="natural_of_nat v" in exI) 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

154 
apply (auto simp add: size_natural_def size_nat_def) done 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

155 
qed 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

156 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

157 
instance list :: (complete) complete 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

158 
proof 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

159 
fix n f 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

160 
show "(\<exists> v. size (v :: 'a list) \<le> n \<and> is_some (f (v :: 'a list))) \<longleftrightarrow> is_some (exhaustive_class.exhaustive f (natural_of_nat n))" 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

161 
proof (induct n arbitrary: f) 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

162 
case 0 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

163 
{ fix v have "size (v :: 'a list) > 0" by (induct v) auto } 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

164 
from this show ?case by (simp add: list.exhaustive_list.simps) 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

165 
next 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

166 
case (Suc n) 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

167 
show ?case 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

168 
proof 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

169 
assume "\<exists>v. Completeness.size_class.size v \<le> Suc n \<and> is_some (f v)" 
47230  170 
then obtain v where v: "size v \<le> Suc n" "is_some (f v)" by blast 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

171 
show "is_some (exhaustive_class.exhaustive f (natural_of_nat (Suc n)))" 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

172 
proof (cases "v") 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

173 
case Nil 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

174 
from this v show ?thesis 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

175 
unfolding list.exhaustive_list.simps[of _ "natural_of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

176 
by (auto split: option.split simp add: less_natural_def) 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

177 
next 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

178 
case (Cons v' vs') 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

179 
from Cons v have size_v': "Completeness.size_class.size v' \<le> n" 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

180 
and "Completeness.size_class.size vs' \<le> n" by auto 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

181 
from Suc v Cons this have "is_some (exhaustive_class.exhaustive (\<lambda>xs. f (v' # xs)) (natural_of_nat n))" 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

182 
by metis 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

183 
from complete_imp1[OF size_v', of "%x. (exhaustive_class.exhaustive (\<lambda>xs. f (x # xs)) (natural_of_nat n))", OF this] 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

184 
show ?thesis 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

185 
unfolding list.exhaustive_list.simps[of _ "natural_of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

186 
by (auto split: option.split simp add: less_natural_def) 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

187 
qed 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

188 
next 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

189 
assume is_some: "is_some (exhaustive_class.exhaustive f (natural_of_nat (Suc n)))" 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

190 
show "\<exists>v. size v \<le> Suc n \<and> is_some (f v)" 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

191 
proof (cases "f []") 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

192 
case Some 
47230  193 
then show ?thesis 
47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

194 
by (metis Suc_eq_plus1 is_some.simps(1) le_add2 size_list.simps(1)) 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

195 
next 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

196 
case None 
47230  197 
with is_some have 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

198 
"is_some (exhaustive_class.exhaustive (\<lambda>x. exhaustive_class.exhaustive (\<lambda>xs. f (x # xs)) (natural_of_nat n)) (natural_of_nat n))" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

199 
unfolding list.exhaustive_list.simps[of _ "natural_of_nat (Suc n)"] Quickcheck_Exhaustive.orelse_def 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

200 
by (simp add: less_natural_def) 
47230  201 
then obtain v' where 
202 
v: "size v' \<le> n" 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

203 
"is_some (exhaustive_class.exhaustive (\<lambda>xs. f (v' # xs)) (natural_of_nat n))" 
47230  204 
by (rule complete_imp2) 
205 
with Suc[of "%xs. f (v' # xs)"] 

206 
obtain vs' where vs': "size vs' \<le> n" "is_some (f (v' # vs'))" 

47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

207 
by metis 
47230  208 
with v have "size (v' # vs') \<le> Suc n" by auto 
209 
with vs' v show ?thesis by metis 

47205
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

210 
qed 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

211 
qed 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

212 
qed 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

213 
qed 
34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

214 

34e8b7347dda
adding theory to prove completeness of the exhaustive generators
bulwahn
parents:
diff
changeset

215 
end 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47230
diff
changeset

216 