Theory QRLib

(*  Title:      Residues.thy
    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
*)

header {* Library for proof of QR *}

theory QRLib = NatIntLib:;

text{*Note. This is an old library. Parts of it have been supplanted
  by other library files.*}

(******************************************************************)
(*                                                                *)
(* Cardinality of some explicit finite sets                       *)
(*                                                                *)
(******************************************************************);

subsection {* Cardinality of explicit finite sets *}

lemma finite_surjI: "[| B ⊆ f ` A; finite A |] ==> finite B";
by (simp add: finite_subset finite_imageI)

lemma bdd_nat_set_l_finite: "finite { y::nat . y < x}";
apply (rule_tac N = "{y. y < x}" and n = x in bounded_nat_set_is_finite)
by auto

lemma bdd_nat_set_le_finite: "finite { y::nat . y ≤ x  }";
apply (subgoal_tac "{ y::nat . y ≤ x  } = { y::nat . y < Suc x}")
by (auto simp add: bdd_nat_set_l_finite)

lemma  bdd_int_set_l_finite: "finite { x::int . 0 ≤ x & x < n}";
apply (subgoal_tac " {(x :: int). 0 ≤ x & x < n} ⊆ 
    int ` {(x :: nat). x < nat n}");
apply (erule finite_surjI)
apply (auto simp add: bdd_nat_set_l_finite image_def)
apply (rule_tac x = "nat x" in exI, simp) 
done

lemma bdd_int_set_le_finite: "finite {x::int. 0 ≤ x & x ≤ n}";
apply (subgoal_tac "{x. 0 ≤ x & x ≤ n} = {x. 0 ≤ x & x < n + 1}")
apply (erule ssubst)
apply (rule bdd_int_set_l_finite)
by auto

lemma bdd_int_set_l_l_finite: "finite {x::int. 0 < x & x < n}";
apply (subgoal_tac "{x::int. 0 < x & x < n} ⊆ {x::int. 0 ≤ x & x < n}")
by (auto simp add: bdd_int_set_l_finite finite_subset);

lemma bdd_int_set_l_le_finite: "finite {x::int. 0 < x & x ≤ n}";
apply (subgoal_tac "{x::int. 0 < x & x ≤ n} ⊆ {x::int. 0 ≤ x & x ≤ n}")
by (auto simp add: bdd_int_set_le_finite finite_subset)

lemma card_bdd_nat_set_l: "card {y::nat . y < x} = x";
apply (induct_tac x, force)
proof -;
  fix n::nat;
  assume "card {y. y < n} = n"; 
  have "{y. y < Suc n} = insert n {y. y < n}";
    by auto
  then have "card {y. y < Suc n} = card (insert n {y. y < n})";
    by auto
  also have "... = Suc (card {y. y < n})";
    apply (rule card_insert_disjoint)
    by (auto simp add: bdd_nat_set_l_finite)
  finally show "card {y. y < Suc n} = Suc n"; 
    by (simp add: prems)
qed;

lemma card_bdd_nat_set_le: "card { y::nat. y ≤ x} = Suc x";
apply (subgoal_tac "{ y::nat. y ≤ x} = { y::nat. y < Suc x}")
by (auto simp add: card_bdd_nat_set_l)

lemma card_bdd_int_set_l: "0 ≤ (n::int) ==> card {y. 0 ≤ y & y < n} = nat n";
proof -;
  fix n::int;
  assume "0 ≤ n";
  have "finite {y. y < nat n}";
    by (rule bdd_nat_set_l_finite)
  moreover have "inj_on (%y. int y) {y. y < nat n}";
    by (auto simp add: inj_on_def)
  ultimately have "card (int ` {y. y < nat n}) = card {y. y < nat n}";
    by (rule card_image)
  also from prems have "int ` {y. y < nat n} = {y. 0 ≤ y & y < n}";
    apply (auto simp add: zless_nat_eq_int_zless image_def)
    apply (rule_tac x = "nat x" in exI)
    by (auto simp add: nat_0_le)
  also; have "card {y. y < nat n} = nat n" 
    by (rule card_bdd_nat_set_l)
  finally show "card {y. 0 ≤ y & y < n} = nat n"; .;
qed;

lemma card_bdd_int_set_le: "0 ≤ (n::int) ==> card {y. 0 ≤ y & y ≤ n} = 
  nat n + 1";
apply (subgoal_tac "{y. 0 ≤ y & y ≤ n} = {y. 0 ≤ y & y < n+1}")
apply (insert card_bdd_int_set_l [of "n+1"])
by (auto simp add: nat_add_distrib)

lemma card_bdd_int_set_l_le: "0 ≤ (n::int) ==> 
    card {x. 0 < x & x ≤ n} = nat n";
proof -;
  fix n::int;
  assume "0 ≤ n";
  have "finite {x. 0 ≤ x & x < n}";
    by (rule bdd_int_set_l_finite)
  moreover have "inj_on (%x. x+1) {x. 0 ≤ x & x < n}";
    by (auto simp add: inj_on_def)
  ultimately have "card ((%x. x+1) ` {x. 0 ≤ x & x < n}) = 
     card {x. 0 ≤ x & x < n}";
    by (rule card_image)
  also from prems have "... = nat n";
    by (rule card_bdd_int_set_l)
  also; have "(%x. x + 1) ` {x. 0 ≤ x & x < n} = {x. 0 < x & x<= n}";
    apply (auto simp add: image_def)
    apply (rule_tac x = "x - 1" in exI)
    by arith
  finally; show "card {x. 0 < x & x ≤ n} = nat n";.;
qed;

lemma card_bdd_int_set_l_l: "0 < (n::int) ==> 
    card {x. 0 < x & x < n} = nat n - 1";
  apply (subgoal_tac "{x. 0 < x & x < n} = {x. 0 < x & x ≤ n - 1}")
  apply (insert card_bdd_int_set_l_le [of "n - 1"])
  by (auto simp add: nat_diff_distrib)

lemma int_card_bdd_int_set_l_l: "0 < n ==> 
    int(card {x. 0 < x & x < n}) = n - 1";
  apply (auto simp add: card_bdd_int_set_l_l)
  apply (subgoal_tac "Suc 0 ≤ nat n")
  apply (auto simp add: zdiff_int [THEN sym])
  apply (subgoal_tac "0 < nat n", arith)
  by (simp add: zero_less_nat_eq)

lemma int_card_bdd_int_set_l_le: "0 ≤ n ==> 
    int(card {x. 0 < x & x ≤ n}) = n";
  by (auto simp add: card_bdd_int_set_l_le)

(*****************************************************************)
(*                                                               *)
(* Define the residue of a set, the standard residue, quadratic  *)
(* residues, and prove some basic properties.                    *)
(*                                                               *)
(*****************************************************************)

constdefs
  ResSet      :: "int => int set => bool"
  "ResSet m X == ∀y1 y2. (((y1 ∈ X) & (y2 ∈ X) & 
    [y1 = y2] (mod m)) --> y1 = y2)"

  StandardRes :: "int => int => int"
  "StandardRes m x == x mod m"

  QuadRes     :: "int => int => bool"
  "QuadRes m x == ∃y. ([(y ^ 2) = x] (mod m))"

  Legendre    :: "int => int => int"      
  "Legendre a p == (if ([a = 0] (mod p)) then 0
                     else if (QuadRes p a) then 1
                     else -1)"

  SR          :: "int => int set"
  "SR p == {x. (0 ≤ x) & (x < p)}"

  SRStar      :: "int => int set"
  "SRStar p == {x. (0 < x) & (x < p)}"

  MultInv :: "int => int => int" 
  "MultInv p x == x ^ nat (p - 2)";

(*****************************************************************)
(*                                                               *)
(* Some properties of MultInv                                    *)
(*                                                               *)
(*****************************************************************)

subsection {* A multiplicative inverse mod p *}

lemma MultInv_prop1: "[| 2 < p; [x = y] (mod p) |] ==> 
    [(MultInv p x) = (MultInv p y)] (mod p)";
  by (auto simp add: MultInv_def zcong_zpower)

lemma MultInv_prop2: "[| 2 < p; p ∈ zprime; ~([x = 0](mod p)) |] ==> 
  [(x * (MultInv p x)) = 1] (mod p)";
proof (simp add: MultInv_def zcong_eq_zdvd_prop);
  assume "2 < p" and "p ∈ zprime" and "~ p dvd x";
  have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)";
    by auto
  also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)";
    by (simp only: nat_add_distrib, auto)
  also have "p - 2 + 1 = p - 1" by arith
  finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)";
    by (rule ssubst, auto)
  also from prems have "[x ^ nat (p - 1) = 1] (mod p)";
    by (auto simp add: Little_Fermat) 
  finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)";.;
qed;

lemma MultInv_prop2a: "[| 2 < p; p ∈ zprime; ~([x = 0](mod p)) |] ==> 
    [(MultInv p x) * x = 1] (mod p)";
  by (auto simp add: MultInv_prop2 zmult_ac)

lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))";
  by (simp add: nat_diff_distrib)

lemma aux_2: "2 < p ==> 0 < nat (p - 2)";
  by auto

lemma MultInv_prop3: "[| 2 < p; p ∈ zprime; ~([x = 0](mod p)) |] ==> 
    ~([MultInv p x = 0](mod p))";
  apply (auto simp add: MultInv_def zcong_eq_zdvd_prop aux_1)
  apply (drule aux_2)
  apply (drule zpower_zdvd_prop2, auto)
done

lemma aux__1: "[| 2 < p; p ∈ zprime; ~([x = 0](mod p))|] ==> 
    [(MultInv p (MultInv p x)) = (x * (MultInv p x) * 
      (MultInv p (MultInv p x)))] (mod p)";
  apply (drule MultInv_prop2, auto)
  apply (drule_tac k = "MultInv p (MultInv p x)" in zcong_scalar, auto);
  apply (auto simp add: zcong_sym)
done

lemma aux__2: "[| 2 < p; p ∈ zprime; ~([x = 0](mod p))|] ==>
    [(x * (MultInv p x) * (MultInv p (MultInv p x))) = x] (mod p)";
  apply (frule MultInv_prop3, auto)
  apply (insert MultInv_prop2 [of p "MultInv p x"], auto)
  apply (drule MultInv_prop2, auto)
  apply (drule_tac k = x in zcong_scalar2, auto)
  apply (auto simp add: zmult_ac)
done

lemma MultInv_prop4: "[| 2 < p; p ∈ zprime; ~([x = 0](mod p)) |] ==> 
    [(MultInv p (MultInv p x)) = x] (mod p)";
  apply (frule aux__1, auto)
  apply (drule aux__2, auto)
  apply (drule zcong_trans, auto)
done

lemma MultInv_prop5: "[| 2 < p; p ∈ zprime; ~([x = 0](mod p)); 
    ~([y = 0](mod p)); [(MultInv p x) = (MultInv p y)] (mod p) |] ==> 
    [x = y] (mod p)";
  apply (drule_tac a = "MultInv p x" and b = "MultInv p y" and 
    m = p and k = x in zcong_scalar)
  apply (insert MultInv_prop2 [of p x], simp)
  apply (auto simp only: zcong_sym [of "MultInv p x * x"])
  apply (auto simp add:  zmult_ac)
  apply (drule zcong_trans, auto)
  apply (drule_tac a = "x * MultInv p y" and k = y in zcong_scalar, auto)
  apply (insert MultInv_prop2a [of p y], auto simp add: zmult_ac)
  apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x])
  apply (auto simp add: zcong_sym)
done

lemma MultInv_zcong_prop1: "[| 2 < p; [j = k] (mod p) |] ==> 
    [a * MultInv p j = a * MultInv p k] (mod p)";
  by (drule MultInv_prop1, auto simp add: zcong_scalar2)

lemma aux___1: "[j = a * MultInv p k] (mod p) ==> 
    [j * k = a * MultInv p k * k] (mod p)";
  by (auto simp add: zcong_scalar)

lemma aux___2: "[|2 < p; p ∈ zprime; ~([k = 0](mod p)); 
    [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)";
  apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2 
    [of "MultInv p k * k" 1 p "j * k" a])
  apply (auto simp add: zmult_ac)
done

lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k = 
     (MultInv p j) * a] (mod p)";
  by (auto simp add: zmult_assoc zcong_scalar2)

lemma aux___4: "[|2 < p; p ∈ zprime; ~([j = 0](mod p)); 
    [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |]
       ==> [k = a * (MultInv p j)] (mod p)";
  apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1 
    [of "MultInv p j * j" 1 p "MultInv p j * a" k])
  apply (auto simp add: zmult_ac zcong_sym)
done

lemma MultInv_zcong_prop2: "[| 2 < p; p ∈ zprime; ~([k = 0](mod p)); 
    ~([j = 0](mod p)); [j = a * MultInv p k] (mod p) |] ==> 
    [k = a * MultInv p j] (mod p)";
  apply (drule aux___1)
  apply (frule aux___2, auto)
  by (drule aux___3, drule aux___4, auto)

lemma MultInv_zcong_prop3: "[| 2 < p; p ∈ zprime; ~([a = 0](mod p)); 
    ~([k = 0](mod p)); ~([j = 0](mod p));
    [a * MultInv p j = a * MultInv p k] (mod p) |] ==> 
      [j = k] (mod p)";
  apply (auto simp add: zcong_eq_zdvd_prop [of a p])
  apply (frule zprime_imp_zrelprime, auto)
  apply (insert zcong_cancel2 [of p a "MultInv p j" "MultInv p k"], auto)
  apply (drule MultInv_prop5, auto)
done

(******************************************************************)
(*                                                                *)
(* Some useful properties of StandardRes                          *)
(*                                                                *)
(******************************************************************)

subsection {* Properties of StandardRes *}

lemma StandardRes_prop1: "[x = StandardRes m x] (mod m)";
  by (auto simp add: StandardRes_def zcong_zmod)

lemma StandardRes_prop2: "0 < m ==> (StandardRes m x1 = StandardRes m x2)
      = ([x1 = x2] (mod m))";
  by (auto simp add: StandardRes_def zcong_zmod_eq)

lemma StandardRes_prop3: "(~[x = 0] (mod p)) = (~(StandardRes p x = 0))";
  by (auto simp add: StandardRes_def zcong_def zdvd_iff_zmod_eq_0)

lemma StandardRes_prop4: "2 < m 
     ==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)";
  by (auto simp add: StandardRes_def zcong_zmod_eq 
                     zmod_zmult_distrib [of x y m])

lemma StandardRes_lbound: "0 < p ==> 0 ≤ StandardRes p x";
  by (auto simp add: StandardRes_def pos_mod_sign)

lemma StandardRes_ubound: "0 < p ==> StandardRes p x < p";
  by (auto simp add: StandardRes_def pos_mod_bound)

lemma StandardRes_eq_zcong: 
   "(StandardRes m x = 0) = ([x = 0](mod m))";
  by (auto simp add: StandardRes_def zcong_eq_zdvd_prop dvd_def) 

(******************************************************************)
(*                                                                *)
(* Some useful stuff relating StandardRes and SRStar and SR       *)
(*                                                                *)
(******************************************************************)

subsection {* Relations between StandardRes, SRStar, and SR *}

lemma SRStar_SR_prop: "x ∈ SRStar p ==> x ∈ SR p";
  by (auto simp add: SRStar_def SR_def)

lemma StandardRes_SR_prop: "x ∈ SR p ==> StandardRes p x = x";
  by (auto simp add: SR_def StandardRes_def mod_pos_pos_trivial)

lemma StandardRes_SRStar_prop1: "2 < p ==> (StandardRes p x ∈ SRStar p) 
     = (~[x = 0] (mod p))";
  apply (auto simp add: StandardRes_prop3 StandardRes_def
                        SRStar_def pos_mod_bound)
  apply (subgoal_tac "0 < p")
by (drule_tac a = x in pos_mod_sign, arith, simp)

lemma StandardRes_SRStar_prop1a: "x ∈ SRStar p ==> ~([x = 0] (mod p))";
  by (auto simp add: SRStar_def zcong_def zdvd_not_zless)

lemma StandardRes_SRStar_prop2: "[| 2 < p; p ∈ zprime; x ∈ SRStar p |] 
     ==> StandardRes p (MultInv p x) ∈ SRStar p";
  apply (frule_tac x = "(MultInv p x)" in StandardRes_SRStar_prop1, simp);
  apply (rule MultInv_prop3)
  apply (auto simp add: SRStar_def zcong_def zdvd_not_zless)
done

lemma StandardRes_SRStar_prop3: "x ∈ SRStar p ==> StandardRes p x = x";
  by (auto simp add: SRStar_SR_prop StandardRes_SR_prop)

lemma StandardRes_SRStar_prop4: "[| p ∈ zprime; 2 < p; x ∈ SRStar p |] 
     ==> StandardRes p x ∈ SRStar p";
  by (frule StandardRes_SRStar_prop3, auto)

lemma SRStar_mult_prop1: "[| p ∈ zprime; 2 < p; x ∈ SRStar p; y ∈ SRStar p|] 
     ==> (StandardRes p (x * y)):SRStar p";
  apply (frule_tac x = x in StandardRes_SRStar_prop4, auto)
  apply (frule_tac x = y in StandardRes_SRStar_prop4, auto)
  apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
done

lemma SRStar_mult_prop2: "[| p ∈ zprime; 2 < p; ~([a = 0](mod p)); 
     x ∈ SRStar p |] 
     ==> StandardRes p (a * MultInv p x) ∈ SRStar p";
  apply (frule_tac x = x in StandardRes_SRStar_prop2, auto)
  apply (frule_tac x = "MultInv p x" in StandardRes_SRStar_prop1)
  apply (auto simp add: StandardRes_SRStar_prop1 zcong_zmult_prop3)
done

lemma SRStar_card: "2 < p ==> int(card(SRStar p)) = p - 1";
  by (auto simp add: SRStar_def int_card_bdd_int_set_l_l)

lemma SRStar_finite: "2 < p ==> finite( SRStar p)";
  by (auto simp add: SRStar_def bdd_int_set_l_l_finite)

(******************************************************************)
(*                                                                *)
(* Some useful stuff about ResSet and StandardRes                 *)
(*                                                                *)
(******************************************************************)

subsection {* Properties relating ResSets with StandardRes *}

lemma aux: "x mod m = y mod m ==> [x = y] (mod m)";
  apply (subgoal_tac "x = y ==> [x = y](mod m)");
  apply (subgoal_tac "[x mod m = y mod m] (mod m) ==> [x = y] (mod m)");
  apply (auto simp add: zcong_zmod [of x y m])
done

lemma StandardRes_inj_on_ResSet: "ResSet m X ==> (inj_on (StandardRes m) X)";
  apply (auto simp add: ResSet_def StandardRes_def inj_on_def)
  apply (drule_tac m = m in aux, auto)
done

lemma StandardRes_Sum: "[| finite X; 0 < m |] 
     ==> [setsum f X = setsum (StandardRes m o f) X](mod m)"; 
  apply (rule_tac F = X in finite_induct)
  apply (auto intro!: zcong_zadd simp add: StandardRes_prop1)
done

lemma SR_pos: "0 < m ==> (StandardRes m ` X) ⊆ {x. 0 ≤ x & x < m}";
  by (auto simp add: StandardRes_ubound StandardRes_lbound)

lemma ResSet_finite: "0 < m ==> ResSet m X ==> finite X";
  apply (rule_tac f = "StandardRes m" in finite_imageD) 
  apply (rule_tac B = "{x. (0 :: int) ≤ x & x < m}" in finite_subset);
by (auto simp add: StandardRes_inj_on_ResSet bdd_int_set_l_finite SR_pos)

lemma mod_mod_is_mod: "[x = x mod m](mod m)";
  by (auto simp add: zcong_zmod)

lemma StandardRes_prod: "[| finite X; 0 < m |] 
     ==> [setprod f X = setprod (StandardRes m o f) X] (mod m)";
  apply (rule_tac F = X in finite_induct)
by (auto intro!: zcong_zmult simp add: StandardRes_prop1)

lemma ResSet_image: "[| 0 < m; ResSet m A; ∀x ∈ A. 
    ∀y ∈ A. ([f x = f y](mod m) --> x = y) |] ==> 
    ResSet m (f ` A)";
  by (auto simp add: ResSet_def)

(****************************************************************)
(*                                                              *)
(* Property for SRStar                                          *)
(*                                                              *)
(****************************************************************)

lemma ResSet_SRStar_prop: "ResSet p (SRStar p)";
  by (auto simp add: SRStar_def ResSet_def zcong_zless_imp_eq)

end;