1088 setup "Presburger.setup" |
1088 setup "Presburger.setup" |
1089 |
1089 |
1090 text {* Code generator setup *} |
1090 text {* Code generator setup *} |
1091 |
1091 |
1092 text {* |
1092 text {* |
1093 Presburger arithmetic is neccesary to prove some |
1093 Presburger arithmetic is necessary (at least convenient) to prove some |
1094 of the following code lemmas on integer numerals. |
1094 of the following code lemmas on integer numerals. |
1095 *} |
1095 *} |
1096 |
1096 |
1097 lemma eq_number_of [code func]: |
1097 lemma eq_number_of [code func]: |
1098 "Code_Generator.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> Code_Generator.eq k l" |
1098 "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l" |
1099 unfolding number_of_is_id .. |
1099 unfolding number_of_is_id .. |
1100 |
1100 |
1101 lemma less_eq_number_of [code func]: |
1101 lemma less_eq_number_of [code func]: |
1102 "((number_of k)\<Colon>int) <= number_of l \<longleftrightarrow> k <= l" |
1102 "((number_of k)\<Colon>int) <= number_of l \<longleftrightarrow> k <= l" |
1103 unfolding number_of_is_id .. |
1103 unfolding number_of_is_id .. |
1104 |
1104 |
1105 lemma eq_Pls_Pls: |
1105 lemma eq_Pls_Pls: |
1106 "Code_Generator.eq Numeral.Pls Numeral.Pls" |
1106 "Numeral.Pls = Numeral.Pls" .. |
1107 unfolding eq_def .. |
|
1108 |
1107 |
1109 lemma eq_Pls_Min: |
1108 lemma eq_Pls_Min: |
1110 "\<not> Code_Generator.eq Numeral.Pls Numeral.Min" |
1109 "Numeral.Pls \<noteq> Numeral.Min" |
1111 unfolding eq_def Pls_def Min_def by auto |
1110 unfolding Pls_def Min_def by auto |
1112 |
1111 |
1113 lemma eq_Pls_Bit0: |
1112 lemma eq_Pls_Bit0: |
1114 "Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> Code_Generator.eq Numeral.Pls k" |
1113 "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k" |
1115 unfolding eq_def Pls_def Bit_def bit.cases by auto |
1114 unfolding Pls_def Bit_def bit.cases by auto |
1116 |
1115 |
1117 lemma eq_Pls_Bit1: |
1116 lemma eq_Pls_Bit1: |
1118 "\<not> Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B1)" |
1117 "Numeral.Pls \<noteq> Numeral.Bit k bit.B1" |
1119 unfolding eq_def Pls_def Bit_def bit.cases by arith |
1118 unfolding Pls_def Bit_def bit.cases by arith |
1120 |
1119 |
1121 lemma eq_Min_Pls: |
1120 lemma eq_Min_Pls: |
1122 "\<not> Code_Generator.eq Numeral.Min Numeral.Pls" |
1121 "Numeral.Min \<noteq> Numeral.Pls" |
1123 unfolding eq_def Pls_def Min_def by auto |
1122 unfolding Pls_def Min_def by auto |
1124 |
1123 |
1125 lemma eq_Min_Min: |
1124 lemma eq_Min_Min: |
1126 "Code_Generator.eq Numeral.Min Numeral.Min" |
1125 "Numeral.Min = Numeral.Min" .. |
1127 unfolding eq_def .. |
|
1128 |
1126 |
1129 lemma eq_Min_Bit0: |
1127 lemma eq_Min_Bit0: |
1130 "\<not> Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B0)" |
1128 "Numeral.Min \<noteq> Numeral.Bit k bit.B0" |
1131 unfolding eq_def Min_def Bit_def bit.cases by arith |
1129 unfolding Min_def Bit_def bit.cases by arith |
1132 |
1130 |
1133 lemma eq_Min_Bit1: |
1131 lemma eq_Min_Bit1: |
1134 "Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> Code_Generator.eq Numeral.Min k" |
1132 "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k" |
1135 unfolding eq_def Min_def Bit_def bit.cases by auto |
1133 unfolding Min_def Bit_def bit.cases by auto |
1136 |
1134 |
1137 lemma eq_Bit0_Pls: |
1135 lemma eq_Bit0_Pls: |
1138 "Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> Code_Generator.eq Numeral.Pls k" |
1136 "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k" |
1139 unfolding eq_def Pls_def Bit_def bit.cases by auto |
1137 unfolding Pls_def Bit_def bit.cases by auto |
1140 |
1138 |
1141 lemma eq_Bit1_Pls: |
1139 lemma eq_Bit1_Pls: |
1142 "\<not> Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Pls" |
1140 "Numeral.Bit k bit.B1 \<noteq> Numeral.Pls" |
1143 unfolding eq_def Pls_def Bit_def bit.cases by arith |
1141 unfolding Pls_def Bit_def bit.cases by arith |
1144 |
1142 |
1145 lemma eq_Bit0_Min: |
1143 lemma eq_Bit0_Min: |
1146 "\<not> Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Min" |
1144 "Numeral.Bit k bit.B0 \<noteq> Numeral.Min" |
1147 unfolding eq_def Min_def Bit_def bit.cases by arith |
1145 unfolding Min_def Bit_def bit.cases by arith |
1148 |
1146 |
1149 lemma eq_Bit1_Min: |
1147 lemma eq_Bit1_Min: |
1150 "Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> Code_Generator.eq Numeral.Min k" |
1148 "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k" |
1151 unfolding eq_def Min_def Bit_def bit.cases by auto |
1149 unfolding Min_def Bit_def bit.cases by auto |
1152 |
1150 |
1153 lemma eq_Bit_Bit: |
1151 lemma eq_Bit_Bit: |
1154 "Code_Generator.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow> |
1152 "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow> |
1155 Code_Generator.eq v1 v2 \<and> Code_Generator.eq k1 k2" |
1153 v1 = v2 \<and> k1 = k2" |
1156 unfolding eq_def Bit_def |
1154 unfolding Bit_def |
1157 apply (cases v1) |
1155 apply (cases v1) |
1158 apply (cases v2) |
1156 apply (cases v2) |
1159 apply auto |
1157 apply auto |
1160 apply arith |
1158 apply arith |
1161 apply (cases v2) |
1159 apply (cases v2) |