https://vim-jp.slack.com/archives/C01844Y1FD2/p1693376299215649

Sceratch.thy

theory Scratch
  imports Main
begin

no_notation relcomp (infixr "O" 75)


(* oreo 型の内部表現 *)
datatype oreo0 = O0 | Ore0 oreo0 | Reo0 oreo0

(* oreo 型の内部表現を整数へ変換 *)
fun to_int :: "oreo0 ⇒ int"
  where "to_int O0 = 0"
      | "to_int (Ore0 x) = (to_int x) + 1"
      | "to_int (Reo0 x) = (to_int x) - 1"

(* 整数を oreo 型の内部表現へ変換 *)
definition of_int :: "int ⇒ oreo0"
  where "of_int i ≡ if i < 0 then (Reo0 ^^ (THE n. i = - (int n))) O0 else (Ore0 ^^ (THE n. i = int n)) O0"

(* Ore O が 1 であることを証明 *)
lemma to_int_OreO_eq_1: "to_int (Ore0 O0) = 1" by simp

(* to_int と of_int の順の関数合成が恒等関数であることを証明。 *)
lemma to_int_comp_of_int: "to_int ∘ of_int = id"
unfolding of_int_def proof standard
  fix x
  show " (to_int ∘ (λi. if i < 0 then (Reo0 ^^ (THE n. i = - int n)) O0 else (Ore0 ^^ (THE n. i = int n)) O0)) x = id x " proof auto
    assume "x < 0"
    then obtain n where 1: "x = - int n" using neg_int_cases by auto
    hence 2: "⋀m. x = - int m ⟹ m = n" by simp
    show "to_int ((Reo0 ^^ (THE n. x = - int n)) O0) = x" using 1 2 proof auto
      show "to_int ((Reo0 ^^ n) O0) = - int n" proof (induct n)
        case 0
        thus ?case by simp
      next
        case (Suc n)
        thus ?case by simp
      qed
    qed
  next
    assume "¬ x < 0"
    then obtain n where 1: "x = int n" using split_nat by auto
    hence 2: "⋀m. x = int m ⟹ m = n" by simp
    show "to_int ((Ore0 ^^ (THE n. x = int n)) O0) = x" using 1 2 proof auto
      show "to_int ((Ore0 ^^ n) O0) = int n" proof (induct n)
        case 0
        thus ?case by simp
      next
        case (Suc n)
        thus ?case by simp
      qed
    qed
  qed
qed

lemma to_int_of_int: "to_int (of_int x) = x" using to_int_comp_of_int by (simp add: pointfree_idE)

(* to_int の値が同じすべての組 (x, y) からなる関係。 *)
definition oreorel :: "oreo0 ⇒ oreo0 ⇒ bool"
  where "oreorel x y ≡ to_int x = to_int y"

(* 単項マイナス演算子の内部表現。 *)
fun uminus_oreo0 :: "oreo0 ⇒ oreo0"
  where "uminus_oreo0 O0 = O0"
      | "uminus_oreo0 (Ore0 x) = Reo0 (uminus_oreo0 x)"
      | "uminus_oreo0 (Reo0 x) = Ore0 (uminus_oreo0 x)"

(* xに単項マイナス演算子の内部表現を適用して整数表現にしたものは、その加法的逆元に等しいことを証明。 *)
lemma to_int_uminus_oreo0: "to_int (uminus_oreo0 x) = - to_int x"
  by (induct x; auto)

(* Reo Ore O と O を同一視する型を作る。 *)
quotient_type oreo = "oreo0" / "oreorel"
  morphisms Rep_oreo0 Abs_oreo0
proof (rule Equiv_Relations.equivpI)
  show "reflp oreorel" unfolding oreorel_def by (rule reflpI, simp)
next
  show "symp oreorel" unfolding oreorel_def by (rule sympI, simp)
next
  show "transp oreorel" unfolding oreorel_def by (rule transpI, simp)
qed

(* Ore (Ore O) や O、 Reo Re のように書ける記法を導入する *)
definition O :: "oreo" where "O ≡ Abs_oreo0 O0"
abbreviation Re :: "oreo" where "Re ≡ O"
definition Ore :: "oreo ⇒ oreo" where "Ore ≡ Abs_oreo0 ∘ Ore0 ∘ Rep_oreo0"
definition Reo :: "oreo ⇒ oreo" where "Reo ≡ Abs_oreo0 ∘ Reo0 ∘ Rep_oreo0"

(* oreo 型から単位的環を構成する。 *)
instantiation oreo :: ring_1
begin

(* 単項マイナス演算子に相当する関数。 *)
lift_definition uminus_oreo :: "oreo ⇒ oreo" is "uminus_oreo0"
unfolding oreorel_def proof -
  fix oreo1 oreo2
  assume "to_int oreo1 = to_int oreo2"
  thus "to_int (uminus_oreo0 oreo1) = to_int (uminus_oreo0 oreo2)" unfolding to_int_uminus_oreo0 by simp
qed

(* oreo 型の単位元の定義。 *)
definition one_oreo :: "oreo"
  where "one_oreo ≡ Ore O"

(* Ore O を簡約すると Ore0 O0 を内部表現にしたものと一致することを証明。 *)
lemma OreO_eq: "Ore O = Abs_oreo0 (Ore0 O0)"
  by (metis O_def Ore_def Quotient_oreo Quotient_rel_abs Quotient_rep_abs_fold_unmap comp_def oreorel_def to_int.simps(2))

(* oreo 型の乗法の定義。 *)
lift_definition times_oreo :: "oreo ⇒ oreo ⇒ oreo"
  is "λx y. of_int ((to_int x) * (to_int y))"
unfolding oreorel_def proof -
  fix oreo1 oreo2 oreo3 oreo4
  assume 1: "to_int oreo1 = to_int oreo2"
  assume 2: "to_int oreo3 = to_int oreo4"
  show "to_int (of_int (to_int oreo1 * to_int oreo3)) = to_int (of_int (to_int oreo2 * to_int oreo4))" unfolding 1 2 by simp
qed

(* oreo 型の零元の定義。 *)
definition zero_oreo :: "oreo"
  where "zero_oreo ≡ O"

(* oreo 型の減法の定義。 *)
lift_definition minus_oreo :: "oreo ⇒ oreo ⇒ oreo"
  is "λx y. of_int ((to_int x) - (to_int y))"
unfolding oreorel_def proof -
  fix oreo1 oreo2 oreo3 oreo4
  assume 1: "to_int oreo1 = to_int oreo2"
  assume 2: "to_int oreo3 = to_int oreo4"
  show "to_int (of_int (to_int oreo1 - to_int oreo3)) = to_int (of_int (to_int oreo2 - to_int oreo4))" unfolding 1 2 by simp
qed

(* oreo 型の加法の定義。 *)
lift_definition plus_oreo :: "oreo ⇒ oreo ⇒ oreo"
  is "λx y. of_int ((to_int x) + (to_int y))"
unfolding oreorel_def proof -
  fix oreo1 oreo2 oreo3 oreo4
  assume 1: "to_int oreo1 = to_int oreo2"
  assume 2: "to_int oreo3 = to_int oreo4"
  show "to_int (of_int (to_int oreo1 + to_int oreo3)) = to_int (of_int (to_int oreo2 + to_int oreo4))" unfolding 1 2 by simp
qed

(* 単位的環の公理を満たすことを証明。 *)
instance proof
  fix a b c :: oreo
  show "a * b * c = a * (b * c)" unfolding times_oreo_def
    by (smt (verit, del_insts) Quotient3_abs_rep Quotient3_oreo mult.commute mult.left_commute times_oreo.abs_eq times_oreo_def to_int_of_int)
next
  fix a :: oreo
  show "1 * a = a" unfolding times_oreo_def one_oreo_def OreO_eq proof auto
    show "Abs_oreo0 (of_int (to_int (Rep_oreo0 (Abs_oreo0 (Ore0 O0))) * to_int (Rep_oreo0 a))) = a"
      by (smt (verit) Quotient3_abs_rep Quotient3_oreo Quotient_oreo Quotient_total_abs_eq_iff equivp_reflp2 mult_cancel_right2 oreo_equivp oreorel_def pointfree_idE to_int_OreO_eq_1 to_int_comp_of_int)
  qed
next
  fix a :: oreo
  show "a * 1 = a" unfolding times_oreo_def one_oreo_def OreO_eq proof auto
    show "Abs_oreo0 (of_int (to_int (Rep_oreo0 a) * to_int (Rep_oreo0 (Abs_oreo0 (Ore0 O0))))) = a"
      by (metis Quotient3_abs_rep Quotient3_oreo mult_cancel_left2 oreo.abs_eq_iff oreorel_def pointfree_idE to_int_OreO_eq_1 to_int_comp_of_int)
  qed
next
  fix a b c :: oreo
  show "a + b + c = a + (b + c)" unfolding plus_oreo_def
    by (smt (verit) Quotient3_abs_rep Quotient3_oreo plus_oreo.abs_eq plus_oreo_def to_int_of_int)
next
  fix a b :: oreo
  show "a + b = b + a" unfolding plus_oreo_def proof auto
    show "Abs_oreo0 (of_int (to_int (Rep_oreo0 a) + to_int (Rep_oreo0 b))) = Abs_oreo0 (of_int (to_int (Rep_oreo0 b) + to_int (Rep_oreo0 a)))" by (subst add.commute, rule refl)
  qed
next
  fix a :: oreo
  show "0 + a = a" unfolding plus_oreo_def zero_oreo_def O_def proof auto
    show "Abs_oreo0 (of_int (to_int (Rep_oreo0 (Abs_oreo0 O0)) + to_int (Rep_oreo0 a))) = a" 
      by (smt (verit) Quotient_oreo Quotient_rel_abs2 Quotient_rep_abs_fold_unmap oreorel_def pointfree_idE to_int.simps(1) to_int_comp_of_int)
  qed
next
  fix a :: oreo
  show "- a + a = 0" unfolding plus_oreo_def zero_oreo_def O_def proof auto
    show "Abs_oreo0 (of_int (to_int (Rep_oreo0 (- a)) + to_int (Rep_oreo0 a))) = Abs_oreo0 O0"
      by (smt (verit, ccfv_SIG) Quotient_oreo Quotient_rep_abs_fold_unmap Quotient_total_abs_eq_iff equivp_reflp2 map_fun_apply oreo_equivp oreorel_def to_int.simps(1) to_int_of_int to_int_uminus_oreo0 uminus_oreo_def)
  qed
next
  fix a b :: oreo
  show "a - b = a + - b" unfolding minus_oreo_def plus_oreo_def proof auto
    show "Abs_oreo0 (of_int (to_int (Rep_oreo0 a) - to_int (Rep_oreo0 b))) = Abs_oreo0 (of_int (to_int (Rep_oreo0 a) + to_int (Rep_oreo0 (- b))))"
      by (smt (verit, ccfv_SIG) Quotient_oreo Quotient_rep_abs_fold_unmap map_fun_apply oreorel_def to_int_uminus_oreo0 uminus_oreo_def)
  qed
next
  fix a b c :: oreo
  show "(a + b) * c = a * c + b * c" unfolding plus_oreo_def times_oreo_def proof auto
    show "Abs_oreo0 (of_int (to_int (Rep_oreo0 (Abs_oreo0 (of_int (to_int (Rep_oreo0 a) + to_int (Rep_oreo0 b))))) * to_int (Rep_oreo0 c)))
       = Abs_oreo0 (of_int (to_int (Rep_oreo0 (Abs_oreo0 (of_int (to_int (Rep_oreo0 a) * to_int (Rep_oreo0 c))))) + to_int (Rep_oreo0 (Abs_oreo0 (of_int (to_int (Rep_oreo0 b) * to_int (Rep_oreo0 c)))))))"
      by (metis Quotient_oreo Quotient_rep_abs_fold_unmap int_distrib(1) oreorel_def to_int_of_int)
  qed
next
  fix a b c :: oreo
  show "a * (b + c) = a * b + a * c" unfolding plus_oreo_def times_oreo_def proof auto
    show "Abs_oreo0 (of_int (to_int (Rep_oreo0 a) * to_int (Rep_oreo0 (Abs_oreo0 (of_int (to_int (Rep_oreo0 b) + to_int (Rep_oreo0 c)))))))
      = Abs_oreo0 (of_int (to_int (Rep_oreo0 (Abs_oreo0 (of_int (to_int (Rep_oreo0 a) * to_int (Rep_oreo0 b))))) + to_int (Rep_oreo0 (Abs_oreo0 (of_int (to_int (Rep_oreo0 a) * to_int (Rep_oreo0 c)))))))"
      by (metis Quotient_oreo Quotient_rep_abs_fold_unmap int_distrib(2) oreorel_def to_int_of_int)
  qed
next
  show "0 ≠ (1 :: oreo)" unfolding zero_oreo_def one_oreo_def O_def Ore_def proof auto
    show "Abs_oreo0 O0 = Abs_oreo0 (Ore0 (Rep_oreo0 (Abs_oreo0 O0))) ⟹ False"
      by (smt (verit, ccfv_SIG) O_def OreO_eq Ore_def Quotient_oreo Quotient_total_abs_eq_iff comp_def equivp_reflp2 oreo_equivp oreorel_def to_int.simps(1) to_int_OreO_eq_1)
  qed
qed



end