Theory Presburger_Formula
section ‹Concrete Atomic Presburger Formulas›
theory Presburger_Formula
imports
Abstract_Formula
"HOL-Library.Code_Target_Int"
"List-Index.List_Index"
begin
declare [[coercion "of_bool :: bool ⇒ nat"]]
declare [[coercion int]]
declare [[coercion_map map]]
declare [[coercion_enabled]]
fun len :: "nat ⇒ nat" where
"len 0 = 0"
| "len (Suc 0) = 1"
| "len n = Suc (len (n div 2))"
lemma len_eq0_iff: "len n = 0 ⟷ n = 0"
by (induct n rule: len.induct) auto
lemma len_mult2[simp]: "len (2 * x) = (if x = 0 then 0 else Suc (len x))"
proof (induct x rule: len.induct)
show "len (2 * Suc 0) = (if Suc 0 = 0 then 0 else Suc (len (Suc 0)))" by (simp add: numeral_eq_Suc)
qed auto
lemma len_mult2'[simp]: "len (x * 2) = (if x = 0 then 0 else Suc (len x))"
using len_mult2 [of x] by (simp add: ac_simps)
lemma len_Suc_mult2[simp]: "len (Suc (2 * x)) = Suc (len x)"
proof (induct x rule: len.induct)
show "len (Suc (2 * Suc 0)) = Suc (len (Suc 0))"
by (metis div_less One_nat_def div2_Suc_Suc len.simps(3) lessI mult.right_neutral numeral_2_eq_2)
qed auto
lemma len_le_iff: "len x ≤ l ⟷ x < 2 ^ l"
proof (induct x arbitrary: l rule: len.induct)
fix l show "(len (Suc 0) ≤ l) = (Suc 0 < 2 ^ l)"
proof (cases l)
case Suc then show ?thesis using le_less by fastforce
qed simp
next
fix v l assume "⋀l. (len (Suc (Suc v) div 2) ≤ l) = (Suc (Suc v) div 2 < 2 ^ l)"
then show "(len (Suc (Suc v)) ≤ l) = (Suc (Suc v) < 2 ^ l)"
by (cases l) (simp_all, linarith)
qed simp
lemma len_pow2[simp]: "len (2 ^ x) = Suc x"
by (induct x) auto
lemma len_div2[simp]: "len (x div 2) = len x - 1"
by (induct x rule: len.induct) auto
lemma less_pow2_len[simp]: "x < 2 ^ len x"
by (induct x rule: len.induct) auto
lemma len_alt: "len x = (LEAST i. x < 2 ^ i)"
proof (rule antisym)
show "len x ≤ (LEAST i. x < 2 ^ i)"
unfolding len_le_iff by (rule LeastI) (rule less_pow2_len)
qed (auto intro: Least_le)
lemma len_mono[simp]: "x ≤ y ⟹ len x ≤ len y"
unfolding len_le_iff using less_pow2_len[of y] by linarith
lemma len_div_pow2[simp]: "len (x div 2 ^ m) = len x - m"
by (induct m arbitrary: x) (auto simp: div_mult2_eq)
lemma len_mult_pow2[simp]: "len (x * 2 ^ m) = (if x = 0 then 0 else len x + m)"
by (induct m arbitrary: x) (auto simp: div_mult2_eq mult.assoc[symmetric] mult.commute[of _ 2])
lemma map_index'_Suc[simp]: "map_index' (Suc i) f xs = map_index' i (λi. f (Suc i)) xs"
by (induct xs arbitrary: i) auto
abbreviation (input) "zero n ≡ replicate n False"
abbreviation (input) "SUC ≡ λ_::unit. Suc"
definition "test_bit m n ≡ (m :: nat) div 2 ^ n mod 2 = 1"
lemma test_bit_eq_bit: ‹test_bit = bit›
by (simp add: fun_eq_iff test_bit_def bit_iff_odd_drop_bit mod_2_eq_odd flip: drop_bit_eq_div)
definition "downshift m ≡ (m :: nat) div 2"
definition "upshift m ≡ (m :: nat) * 2"
lemma set_bit_def: "set_bit n m ≡ m + (if ¬ test_bit m n then 2 ^ n else (0 :: nat))"
apply (rule eq_reflection)
apply (rule bit_eqI)
apply (subst disjunctive_add)
apply (auto simp add: bit_simps test_bit_eq_bit)
done
definition "cut_bits n m ≡ (m :: nat) mod 2 ^ n"
lemma cut_bits_eq_take_bit: ‹cut_bits = take_bit›
by (simp add: fun_eq_iff cut_bits_def take_bit_eq_mod)
typedef interp = "{(n :: nat, xs :: nat list). ∀x ∈ set xs. len x ≤ n}"
by (force intro: exI[of _ "[]"])
setup_lifting type_definition_interp
type_synonym atom = "bool list"
type_synonym "value" = "nat"