author  nipkow 
Mon, 12 Sep 2011 07:55:43 +0200  
changeset 44890  22f665a2e91c 
parent 44241  7943b69f0188 
child 44928  7ef6505bde7f 
permissions  rwrr 
35953  1 
theory Predicate_Compile_Alternative_Defs 
36053
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

2 
imports Main 
35953  3 
begin 
4 

5 
section {* Common constants *} 

6 

7 
declare HOL.if_bool_eq_disj[code_pred_inline] 

8 

36253
6e969ce3dfcc
added further inlining of boolean constants to the predicate compiler
bulwahn
parents:
36246
diff
changeset

9 
declare bool_diff_def[code_pred_inline] 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40548
diff
changeset

10 
declare inf_bool_def_raw[code_pred_inline] 
36253
6e969ce3dfcc
added further inlining of boolean constants to the predicate compiler
bulwahn
parents:
36246
diff
changeset

11 
declare less_bool_def_raw[code_pred_inline] 
6e969ce3dfcc
added further inlining of boolean constants to the predicate compiler
bulwahn
parents:
36246
diff
changeset

12 
declare le_bool_def_raw[code_pred_inline] 
6e969ce3dfcc
added further inlining of boolean constants to the predicate compiler
bulwahn
parents:
36246
diff
changeset

13 

6e969ce3dfcc
added further inlining of boolean constants to the predicate compiler
bulwahn
parents:
36246
diff
changeset

14 
lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

15 
by (rule eq_reflection) (auto simp add: fun_eq_iff min_def le_bool_def) 
36253
6e969ce3dfcc
added further inlining of boolean constants to the predicate compiler
bulwahn
parents:
36246
diff
changeset

16 

39650
2a35950ec495
handling equivalences smarter in the predicate compiler
bulwahn
parents:
39302
diff
changeset

17 
lemma [code_pred_inline]: 
2a35950ec495
handling equivalences smarter in the predicate compiler
bulwahn
parents:
39302
diff
changeset

18 
"((A::bool) ~= (B::bool)) = ((A & ~ B)  (B & ~ A))" 
2a35950ec495
handling equivalences smarter in the predicate compiler
bulwahn
parents:
39302
diff
changeset

19 
by fast 
2a35950ec495
handling equivalences smarter in the predicate compiler
bulwahn
parents:
39302
diff
changeset

20 

35953  21 
setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *} 
22 

23 
section {* Pairs *} 

24 

37591  25 
setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name prod_case}] *} 
35953  26 

27 
section {* Bounded quantifiers *} 

28 

29 
declare Ball_def[code_pred_inline] 

30 
declare Bex_def[code_pred_inline] 

31 

32 
section {* Set operations *} 

33 

34 
declare Collect_def[code_pred_inline] 

35 
declare mem_def[code_pred_inline] 

36 

37 
declare eq_reflection[OF empty_def, code_pred_inline] 

38 
declare insert_code[code_pred_def] 

39 

40 
declare subset_iff[code_pred_inline] 

41 

42 
declare Int_def[code_pred_inline] 

43 
declare eq_reflection[OF Un_def, code_pred_inline] 

44 
declare eq_reflection[OF UNION_def, code_pred_inline] 

45 

46 
lemma Diff[code_pred_inline]: 

47 
"(A  B) = (%x. A x \<and> \<not> B x)" 

48 
by (auto simp add: mem_def) 

49 

36253
6e969ce3dfcc
added further inlining of boolean constants to the predicate compiler
bulwahn
parents:
36246
diff
changeset

50 
lemma subset_eq[code_pred_inline]: 
6e969ce3dfcc
added further inlining of boolean constants to the predicate compiler
bulwahn
parents:
36246
diff
changeset

51 
"(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x > Q x))" 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44241
diff
changeset

52 
by (rule eq_reflection) (fastforce simp add: mem_def) 
36253
6e969ce3dfcc
added further inlining of boolean constants to the predicate compiler
bulwahn
parents:
36246
diff
changeset

53 

35953  54 
lemma set_equality[code_pred_inline]: 
55 
"(A = B) = ((\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x))" 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44241
diff
changeset

56 
by (fastforce simp add: mem_def) 
35953  57 

58 
section {* Setup for Numerals *} 

59 

60 
setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *} 

61 
setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *} 

62 

63 
setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *} 

64 

36053
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

65 
section {* Arithmetic operations *} 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

66 

29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

67 
subsection {* Arithmetic on naturals and integers *} 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

68 

29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

69 
definition plus_eq_nat :: "nat => nat => nat => bool" 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

70 
where 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

71 
"plus_eq_nat x y z = (x + y = z)" 
35953  72 

36053
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

73 
definition minus_eq_nat :: "nat => nat => nat => bool" 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

74 
where 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

75 
"minus_eq_nat x y z = (x  y = z)" 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

76 

29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

77 
definition plus_eq_int :: "int => int => int => bool" 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

78 
where 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

79 
"plus_eq_int x y z = (x + y = z)" 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

80 

29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

81 
definition minus_eq_int :: "int => int => int => bool" 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

82 
where 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

83 
"minus_eq_int x y z = (x  y = z)" 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

84 

29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

85 
definition subtract 
35953  86 
where 
36053
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

87 
[code_inline]: "subtract x y = y  x" 
35953  88 

36053
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

89 
setup {* 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

90 
let 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

91 
val Fun = Predicate_Compile_Aux.Fun 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

92 
val Input = Predicate_Compile_Aux.Input 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

93 
val Output = Predicate_Compile_Aux.Output 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

94 
val Bool = Predicate_Compile_Aux.Bool 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

95 
val iio = Fun (Input, Fun (Input, Fun (Output, Bool))) 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

96 
val ioi = Fun (Input, Fun (Output, Fun (Input, Bool))) 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

97 
val oii = Fun (Output, Fun (Input, Fun (Input, Bool))) 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

98 
val ooi = Fun (Output, Fun (Output, Fun (Input, Bool))) 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39650
diff
changeset

99 
val plus_nat = Core_Data.functional_compilation @{const_name plus} iio 
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39650
diff
changeset

100 
val minus_nat = Core_Data.functional_compilation @{const_name "minus"} iio 
36053
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

101 
fun subtract_nat compfuns (_ : typ) = 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

102 
let 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

103 
val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat} 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

104 
in 
44241  105 
absdummy @{typ nat} (absdummy @{typ nat} 
106 
(Const (@{const_name "If"}, @{typ bool} > T > T > T) $ 

36053
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

107 
(@{term "op > :: nat => nat => bool"} $ Bound 1 $ Bound 0) $ 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

108 
Predicate_Compile_Aux.mk_bot compfuns @{typ nat} $ 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

109 
Predicate_Compile_Aux.mk_single compfuns 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

110 
(@{term "op  :: nat => nat => nat"} $ Bound 0 $ Bound 1))) 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

111 
end 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

112 
fun enumerate_addups_nat compfuns (_ : typ) = 
44241  113 
absdummy @{typ nat} (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"} 
114 
(absdummy @{typ code_numeral} (@{term "Pair :: nat => nat => nat * nat"} $ 

36053
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

115 
(@{term "Code_Numeral.nat_of"} $ Bound 0) $ 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

116 
(@{term "op  :: nat => nat => nat"} $ Bound 1 $ (@{term "Code_Numeral.nat_of"} $ Bound 0))), 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

117 
@{term "0 :: code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 0)) 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

118 
fun enumerate_nats compfuns (_ : typ) = 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

119 
let 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

120 
val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns @{term "0 :: nat"}) 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

121 
val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat} 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

122 
in 
44241  123 
absdummy @{typ nat} (absdummy @{typ nat} 
124 
(Const (@{const_name If}, @{typ bool} > T > T > T) $ 

36053
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

125 
(@{term "op = :: nat => nat => bool"} $ Bound 0 $ @{term "0::nat"}) $ 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

126 
(Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ nat} (@{term "Code_Numeral.nat_of"}, 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

127 
@{term "0::code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 1)) $ 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

128 
(single_const $ (@{term "op + :: nat => nat => nat"} $ Bound 1 $ Bound 0)))) 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

129 
end 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

130 
in 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39650
diff
changeset

131 
Core_Data.force_modes_and_compilations @{const_name plus_eq_nat} 
36053
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

132 
[(iio, (plus_nat, false)), (oii, (subtract_nat, false)), (ioi, (subtract_nat, false)), 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

133 
(ooi, (enumerate_addups_nat, false))] 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

134 
#> Predicate_Compile_Fun.add_function_predicate_translation 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

135 
(@{term "plus :: nat => nat => nat"}, @{term "plus_eq_nat"}) 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39650
diff
changeset

136 
#> Core_Data.force_modes_and_compilations @{const_name minus_eq_nat} 
36053
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

137 
[(iio, (minus_nat, false)), (oii, (enumerate_nats, false))] 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

138 
#> Predicate_Compile_Fun.add_function_predicate_translation 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

139 
(@{term "minus :: nat => nat => nat"}, @{term "minus_eq_nat"}) 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39650
diff
changeset

140 
#> Core_Data.force_modes_and_functions @{const_name plus_eq_int} 
36053
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

141 
[(iio, (@{const_name plus}, false)), (ioi, (@{const_name subtract}, false)), 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

142 
(oii, (@{const_name subtract}, false))] 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

143 
#> Predicate_Compile_Fun.add_function_predicate_translation 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

144 
(@{term "plus :: int => int => int"}, @{term "plus_eq_int"}) 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39650
diff
changeset

145 
#> Core_Data.force_modes_and_functions @{const_name minus_eq_int} 
36053
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

146 
[(iio, (@{const_name minus}, false)), (oii, (@{const_name plus}, false)), 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

147 
(ioi, (@{const_name minus}, false))] 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

148 
#> Predicate_Compile_Fun.add_function_predicate_translation 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

149 
(@{term "minus :: int => int => int"}, @{term "minus_eq_int"}) 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

150 
end 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

151 
*} 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

152 

29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

153 
subsection {* Inductive definitions for ordering on naturals *} 
35953  154 

155 
inductive less_nat 

156 
where 

157 
"less_nat 0 (Suc y)" 

158 
 "less_nat x y ==> less_nat (Suc x) (Suc y)" 

159 

36246
43fecedff8cf
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents:
36053
diff
changeset

160 
lemma less_nat[code_pred_inline]: 
35953  161 
"x < y = less_nat x y" 
162 
apply (rule iffI) 

163 
apply (induct x arbitrary: y) 

164 
apply (case_tac y) apply (auto intro: less_nat.intros) 

165 
apply (case_tac y) 

166 
apply (auto intro: less_nat.intros) 

167 
apply (induct rule: less_nat.induct) 

168 
apply auto 

169 
done 

170 

171 
inductive less_eq_nat 

172 
where 

173 
"less_eq_nat 0 y" 

174 
 "less_eq_nat x y ==> less_eq_nat (Suc x) (Suc y)" 

175 

176 
lemma [code_pred_inline]: 

177 
"x <= y = less_eq_nat x y" 

178 
apply (rule iffI) 

179 
apply (induct x arbitrary: y) 

180 
apply (auto intro: less_eq_nat.intros) 

181 
apply (case_tac y) apply (auto intro: less_eq_nat.intros) 

182 
apply (induct rule: less_eq_nat.induct) 

183 
apply auto done 

184 

185 
section {* Alternative list definitions *} 

186 

36053
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

187 
subsection {* Alternative rules for length *} 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

188 

29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

189 
definition size_list :: "'a list => nat" 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

190 
where "size_list = size" 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

191 

29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

192 
lemma size_list_simps: 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

193 
"size_list [] = 0" 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

194 
"size_list (x # xs) = Suc (size_list xs)" 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

195 
by (auto simp add: size_list_def) 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

196 

29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

197 
declare size_list_simps[code_pred_def] 
29e242e9e9a3
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents:
35953
diff
changeset

198 
declare size_list_def[symmetric, code_pred_inline] 
35953  199 

200 
subsection {* Alternative rules for set *} 

201 

202 
lemma set_ConsI1 [code_pred_intro]: 

203 
"set (x # xs) x" 

204 
unfolding mem_def[symmetric, of _ x] 

205 
by auto 

206 

207 
lemma set_ConsI2 [code_pred_intro]: 

208 
"set xs x ==> set (x' # xs) x" 

209 
unfolding mem_def[symmetric, of _ x] 

210 
by auto 

211 

212 
code_pred [skip_proof] set 

213 
proof  

214 
case set 

215 
from this show thesis 

216 
apply (case_tac xb) 

217 
apply auto 

218 
unfolding mem_def[symmetric, of _ xc] 

219 
apply auto 

220 
unfolding mem_def 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44241
diff
changeset

221 
apply fastforce 
35953  222 
done 
223 
qed 

224 

225 
subsection {* Alternative rules for list_all2 *} 

226 

227 
lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []" 

228 
by auto 

229 

230 
lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)" 

231 
by auto 

232 

233 
code_pred [skip_proof] list_all2 

234 
proof  

235 
case list_all2 

236 
from this show thesis 

237 
apply  

238 
apply (case_tac xb) 

239 
apply (case_tac xc) 

240 
apply auto 

241 
apply (case_tac xc) 

242 
apply auto 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44241
diff
changeset

243 
apply fastforce 
35953  244 
done 
245 
qed 

246 

40548
54eb5fd36e5e
ignoring the constant STR in the predicate compiler
bulwahn
parents:
40054
diff
changeset

247 
section {* Setup for String.literal *} 
54eb5fd36e5e
ignoring the constant STR in the predicate compiler
bulwahn
parents:
40054
diff
changeset

248 

54eb5fd36e5e
ignoring the constant STR in the predicate compiler
bulwahn
parents:
40054
diff
changeset

249 
setup {* Predicate_Compile_Data.ignore_consts [@{const_name "STR"}] *} 
54eb5fd36e5e
ignoring the constant STR in the predicate compiler
bulwahn
parents:
40054
diff
changeset

250 

36246
43fecedff8cf
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents:
36053
diff
changeset

251 
section {* Simplification rules for optimisation *} 
43fecedff8cf
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents:
36053
diff
changeset

252 

43fecedff8cf
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents:
36053
diff
changeset

253 
lemma [code_pred_simp]: "\<not> False == True" 
43fecedff8cf
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents:
36053
diff
changeset

254 
by auto 
43fecedff8cf
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents:
36053
diff
changeset

255 

43fecedff8cf
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents:
36053
diff
changeset

256 
lemma [code_pred_simp]: "\<not> True == False" 
43fecedff8cf
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents:
36053
diff
changeset

257 
by auto 
43fecedff8cf
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents:
36053
diff
changeset

258 

43fecedff8cf
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents:
36053
diff
changeset

259 
lemma less_nat_k_0 [code_pred_simp]: "less_nat k 0 == False" 
43fecedff8cf
added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents:
36053
diff
changeset

260 
unfolding less_nat[symmetric] by auto 
35953  261 

262 

263 
end 