author  nipkow 
Mon, 13 Sep 2010 11:13:15 +0200  
changeset 39302  d7728f65b353 
parent 39198  f967a16dfcdd 
child 39650  2a35950ec495 
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] 
6e969ce3dfcc
added further inlining of boolean constants to the predicate compiler
bulwahn
parents:
36246
diff
changeset

10 
declare inf_bool_eq_raw[code_pred_inline] 
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 

35953  17 
setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *} 
18 

19 
section {* Pairs *} 

20 

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

23 
section {* Bounded quantifiers *} 

24 

25 
declare Ball_def[code_pred_inline] 

26 
declare Bex_def[code_pred_inline] 

27 

28 
section {* Set operations *} 

29 

30 
declare Collect_def[code_pred_inline] 

31 
declare mem_def[code_pred_inline] 

32 

33 
declare eq_reflection[OF empty_def, code_pred_inline] 

34 
declare insert_code[code_pred_def] 

35 

36 
declare subset_iff[code_pred_inline] 

37 

38 
declare Int_def[code_pred_inline] 

39 
declare eq_reflection[OF Un_def, code_pred_inline] 

40 
declare eq_reflection[OF UNION_def, code_pred_inline] 

41 

42 
lemma Diff[code_pred_inline]: 

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

44 
by (auto simp add: mem_def) 

45 

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

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

47 
"(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x > Q x))" 
6e969ce3dfcc
added further inlining of boolean constants to the predicate compiler
bulwahn
parents:
36246
diff
changeset

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

49 

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

52 
by (fastsimp simp add: mem_def) 

53 

54 
section {* Setup for Numerals *} 

55 

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

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

58 

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

60 

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

61 
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

62 

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

63 
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

64 

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 
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

66 
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

67 
"plus_eq_nat x y z = (x + y = z)" 
35953  68 

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

69 
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

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 
"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

72 

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 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

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 
"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

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 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

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 
"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

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 subtract 
35953  82 
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

83 
[code_inline]: "subtract x y = y  x" 
35953  84 

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

85 
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

86 
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

87 
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

88 
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

89 
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

90 
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

91 
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

92 
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

93 
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

94 
val ooi = Fun (Output, 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

95 
val plus_nat = Predicate_Compile_Core.functional_compilation @{const_name plus} iio 
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 minus_nat = Predicate_Compile_Core.functional_compilation @{const_name "minus"} iio 
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 
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

98 
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

99 
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

100 
in 
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 
absdummy (@{typ nat}, absdummy (@{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

102 
Const (@{const_name "If"}, @{typ bool} > T > T > T) $ 
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 
(@{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

104 
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

105 
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

106 
(@{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

107 
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

108 
fun enumerate_addups_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

109 
absdummy (@{typ nat}, Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * 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

110 
(absdummy (@{typ code_numeral}, @{term "Pair :: nat => nat => nat * 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

111 
(@{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

112 
(@{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

113 
@{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

114 
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

115 
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

116 
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

117 
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

118 
in 
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 
absdummy(@{typ nat}, absdummy (@{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

120 
Const (@{const_name If}, @{typ bool} > T > T > T) $ 
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 
(@{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

122 
(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

123 
@{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

124 
(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

125 
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

126 
in 
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 
Predicate_Compile_Core.force_modes_and_compilations @{const_name plus_eq_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

128 
[(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

129 
(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

130 
#> 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

131 
(@{term "plus :: nat => nat => nat"}, @{term "plus_eq_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

132 
#> Predicate_Compile_Core.force_modes_and_compilations @{const_name minus_eq_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

133 
[(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

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 "minus :: nat => nat => nat"}, @{term "minus_eq_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

136 
#> Predicate_Compile_Core.force_modes_and_functions @{const_name plus_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

137 
[(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

138 
(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

139 
#> 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

140 
(@{term "plus :: int => int => int"}, @{term "plus_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

141 
#> Predicate_Compile_Core.force_modes_and_functions @{const_name 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

142 
[(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

143 
(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

144 
#> 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

145 
(@{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

146 
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

147 
*} 
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 

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 
subsection {* Inductive definitions for ordering on naturals *} 
35953  150 

151 
inductive less_nat 

152 
where 

153 
"less_nat 0 (Suc y)" 

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

155 

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

156 
lemma less_nat[code_pred_inline]: 
35953  157 
"x < y = less_nat x y" 
158 
apply (rule iffI) 

159 
apply (induct x arbitrary: y) 

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

161 
apply (case_tac y) 

162 
apply (auto intro: less_nat.intros) 

163 
apply (induct rule: less_nat.induct) 

164 
apply auto 

165 
done 

166 

167 
inductive less_eq_nat 

168 
where 

169 
"less_eq_nat 0 y" 

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

171 

172 
lemma [code_pred_inline]: 

173 
"x <= y = less_eq_nat x y" 

174 
apply (rule iffI) 

175 
apply (induct x arbitrary: y) 

176 
apply (auto intro: less_eq_nat.intros) 

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

178 
apply (induct rule: less_eq_nat.induct) 

179 
apply auto done 

180 

181 
section {* Alternative list definitions *} 

182 

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

183 
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

184 

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

185 
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

186 
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

187 

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 
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

189 
"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

190 
"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

191 
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

192 

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 
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

194 
declare size_list_def[symmetric, code_pred_inline] 
35953  195 

196 
subsection {* Alternative rules for set *} 

197 

198 
lemma set_ConsI1 [code_pred_intro]: 

199 
"set (x # xs) x" 

200 
unfolding mem_def[symmetric, of _ x] 

201 
by auto 

202 

203 
lemma set_ConsI2 [code_pred_intro]: 

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

205 
unfolding mem_def[symmetric, of _ x] 

206 
by auto 

207 

208 
code_pred [skip_proof] set 

209 
proof  

210 
case set 

211 
from this show thesis 

212 
apply (case_tac xb) 

213 
apply auto 

214 
unfolding mem_def[symmetric, of _ xc] 

215 
apply auto 

216 
unfolding mem_def 

217 
apply fastsimp 

218 
done 

219 
qed 

220 

221 
subsection {* Alternative rules for list_all2 *} 

222 

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

224 
by auto 

225 

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

227 
by auto 

228 

229 
code_pred [skip_proof] list_all2 

230 
proof  

231 
case list_all2 

232 
from this show thesis 

233 
apply  

234 
apply (case_tac xb) 

235 
apply (case_tac xc) 

236 
apply auto 

237 
apply (case_tac xc) 

238 
apply auto 

239 
apply fastsimp 

240 
done 

241 
qed 

242 

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

243 
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

244 

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

245 
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

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

247 

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

248 
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

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

250 

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

251 
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

252 
unfolding less_nat[symmetric] by auto 
35953  253 

254 

255 
end 