Theory With_Type_Example

section ‹‹With_Type_Example› -- Some contrieved simple examples›

theory With_Type_Example
  imports With_Type "HOL-Computational_Algebra.Factorial_Ring" Mersenne_Primes.Lucas_Lehmer_Code
begin

unbundle lifting_syntax and no m_inv_syntax


subsection ‹Semigroups (class with one parameter)›


definition ‹WITH_TYPE_CLASS_semigroup_add S plus ⟷ (∀a∈S. ∀b∈S. plus a b ∈ S) ∧ (∀a∈S. ∀b∈S. ∀c∈S. plus (plus a b) c = plus a (plus b c))›
  for S :: ‹'rep set› and plus :: ‹'rep ⇒ 'rep ⇒ 'rep›
definition ‹WITH_TYPE_REL_semigroup_add r = (r ===> r ===> r)›
  for r :: ‹'rep ⇒ 'abs ⇒ bool› and rep_ops :: ‹'rep ⇒ 'rep ⇒ 'rep› and abs_ops :: ‹'abs ⇒ 'abs ⇒ 'abs›

lemma with_type_wellformed_semigroup_add[with_type_intros]:
  ‹with_type_wellformed WITH_TYPE_CLASS_semigroup_add S WITH_TYPE_REL_semigroup_add›
  by (simp add: with_type_wellformed_def WITH_TYPE_CLASS_semigroup_add_def WITH_TYPE_REL_semigroup_add_def
      fun.Domainp_rel Domainp_pred_fun_eq bi_unique_alt_def)

lemma with_type_transfer_semigroup_add:
  assumes [transfer_rule]: ‹bi_unique r› ‹right_total r›
  shows ‹(WITH_TYPE_REL_semigroup_add r ===> (⟷))
         (WITH_TYPE_CLASS_semigroup_add (Collect (Domainp r))) class.semigroup_add›
proof -
  define f where ‹f y = (SOME x. r x y)› for y
  have rf: ‹r x y ⟷ x = f y› for x y
    unfolding f_def
    apply (rule someI2_ex)
    using assms
    by (auto intro!: simp: right_total_def bi_unique_def)
  have inj: ‹inj f›
    using ‹bi_unique r›
    by (auto intro!: injI simp: bi_unique_def rf)
  have aux1: ‹∀ya yb. x (f ya) (f yb) = f (y ya yb) ⟹
       ∀a. (∃y. a = f y) ⟶ (∀b. (∃y. b = f y) ⟶ (∀c. (∃y. c = f y) ⟶ x (x a b) c = x a (x b c))) ⟹ 
       y (y a b) c = y a (y b c)› for x y a b c
    by (metis inj injD)
  show ?thesis
    unfolding WITH_TYPE_REL_semigroup_add_def rel_fun_def
    unfolding WITH_TYPE_CLASS_semigroup_add_def Domainp_iff rf
    by (auto intro!: simp: class.semigroup_add_def aux1)
qed

setup ‹
With_Type.add_with_type_info_global {
  class = \<^class>‹semigroup_add›,
  param_names = ["plus"],
  rep_class = \<^const_name>‹WITH_TYPE_CLASS_semigroup_add›,
  rep_rel = \<^const_name>‹WITH_TYPE_REL_semigroup_add›,
  with_type_wellformed = @{thm with_type_wellformed_semigroup_add},
  transfer = SOME @{thm with_type_transfer_semigroup_add},
  rep_rel_itself = NONE
}
›

subsubsection ‹Example›

definition carrier :: ‹int set› where ‹carrier = {0,1,2}›
definition carrier_plus :: ‹int ⇒ int ⇒ int› where ‹carrier_plus i j = (i + j) mod 3›

lemma carrier_nonempty[iff]: ‹carrier ≠ {}›
  by (simp add: carrier_def)

lemma carrier_semigroup[with_type_intros]: ‹WITH_TYPE_CLASS_semigroup_add carrier carrier_plus›
  by (auto simp: WITH_TYPE_CLASS_semigroup_add_def
        carrier_def carrier_plus_def)

text ‹This proof uses both properties of the specific carrier (existence of two different elements)
  and of semigroups in general (associativity)›
lemma example_semigroup:
  shows ‹let 't::semigroup_add = carrier with carrier_plus in ∀x y.
    (plus_t x y = plus_t y x ∧ plus_t x (plus_t x x) = plus_t (plus_t x x) x)›
proof (with_type_intro)
  show ‹carrier ≠ {}› by simp
  fix Rep :: ‹'t ⇒ int› and T and plus_t
  assume ‹bij_betw Rep UNIV carrier›
  then interpret type_definition Rep ‹inv Rep› carrier
    using type_definition_bij_betw_iff by blast
  define r where ‹r = (λx y. x = Rep y)›
  have [transfer_rule]: ‹bi_unique r›
    by (simp add: Rep_inject bi_unique_def r_def)
  have [transfer_rule]: ‹right_total r›
    by (simp add: r_def right_total_def)
  assume ‹WITH_TYPE_REL_semigroup_add (λx y. x = Rep y) carrier_plus plus_t›
  then have transfer_carrier[transfer_rule]: ‹(r ===> r ===> r) carrier_plus plus_t›
    by (simp add: r_def WITH_TYPE_REL_semigroup_add_def)
  have [transfer_rule]: ‹((r ===> r ===> r) ===> (⟷)) (WITH_TYPE_CLASS_semigroup_add (Collect (Domainp r))) class.semigroup_add›
  proof (intro rel_funI)
    fix x y
    assume xy[transfer_rule]: ‹(r ===> r ===> r) x y›
    have aux1: ‹∀a. Domainp r a ⟶ (∀b. Domainp r b ⟶ (∀c. Domainp r c ⟶ x (x a b) c = x a (x b c))) ⟹
       r a b ⟹ r ba bb ⟹ r c bc ⟹ x (x a ba) c = x a (x ba c)› for a b ba bb c bc
      by blast
    have aux2: ‹r a b ⟹ r ba bb ⟹ Domainp r (x a ba)› for a b ba bb
      by (metis DomainPI rel_funD xy)
    show ‹WITH_TYPE_CLASS_semigroup_add (Collect (Domainp r)) x ⟷ class.semigroup_add y›
      unfolding class.semigroup_add_def
      apply transfer
      by (auto intro!: aux1 aux2 simp: WITH_TYPE_CLASS_semigroup_add_def)
  qed
  have dom_r: ‹Collect (Domainp r) = carrier›
    by (auto elim!: Rep_cases simp: Rep r_def Domainp_iff)
  interpret semigroup_add plus_t
    apply transfer
    using carrier_semigroup dom_r by auto

  have 1: ‹plus_t x y = plus_t y x› for x y
    apply transfer
    apply (simp add: carrier_plus_def)
    by presburger

  have 2: ‹plus_t x (plus_t x x) = plus_t (plus_t x x) x› for x
    by (simp add: add_assoc)

  from 1 2
  show ‹∀x y. plus_t x y = plus_t y x ∧ plus_t x (plus_t x x) = plus_t (plus_t x x) x›
    by simp
qed

text ‹Some hypothetical lemma where we use the existence of a commutative semigroup to 
  derive that 2147483647 is prime. (The lemma is true since 2147483647 is prime,
  but otherwise this is completely fictional.)›
lemma artificial_lemma: ‹(∃p (x::_::semigroup_add) y. p x y = p y x) ⟹ prime (2147483647 :: nat)›
proof - ― ‹This proof can be ignored. We just didn't want to have a "sorry" in the theory file›
  have "prime (2 ^ 31 - 1 :: nat)"
    by (subst lucas_lehmer_correct') eval
  also have ‹… = 2147483647›
    by eval
  finally show ‹prime (2147483647 :: nat)›
    by -
qed

lemma prime_2147483647: ‹prime (2147483647 :: nat)›
proof -
  from example_semigroup
  have ‹let 't::semigroup_add = carrier with carrier_plus in
        prime (2147483647 :: nat)›
  proof with_type_mp
    with_type_case
    show ‹prime (2147483647 :: nat)›
      apply (rule artificial_lemma)
      using with_type_mp.premise by auto
  qed
  from this[cancel_with_type]
  show ?thesis
    by -
qed


subsection ‹Abelian groups (class with several parameters)›

text ‹Here we do exactly the same as for semigroups, except that now we use an abelian group.
  This shows the additional subtleties that arise when a class has more than one parameter.›

notation rel_prod (infixr ‹***› 80)

definition ‹WITH_TYPE_CLASS_ab_group_add S = (λ(plus,zero,minus,uminus). zero ∈ S
 ∧ (∀a∈S. ∀b∈S. plus a b ∈ S) ∧ (∀a∈S. ∀b∈S. minus a b ∈ S) ∧ (∀a∈S. uminus a ∈ S)
 ∧ (∀a∈S. ∀b∈S. ∀c∈S. plus (plus a b) c= plus a (plus b c)) ∧ (∀a∈S. ∀b∈S. plus a b = plus b a)
 ∧ (∀a∈S. plus zero a = a) ∧ (∀a∈S. plus (uminus a) a = zero) ∧ (∀a∈S. ∀b∈S. minus a b = plus a (uminus b)))›
  for S :: ‹'rep set›
definition ‹WITH_TYPE_REL_ab_group_add r = (r ===> r ===> r) *** r *** (r ===> r ===> r) *** (r ===> r)›
  for r :: ‹'rep ⇒ 'abs ⇒ bool› and rep_ops :: ‹'rep ⇒ 'rep ⇒ 'rep› and abs_ops :: ‹'abs ⇒ 'abs ⇒ 'abs›

lemma with_type_wellformed_ab_group_add[with_type_intros]:
  ‹with_type_wellformed WITH_TYPE_CLASS_ab_group_add S WITH_TYPE_REL_ab_group_add›
  by (simp add: with_type_wellformed_def WITH_TYPE_CLASS_ab_group_add_def WITH_TYPE_REL_ab_group_add_def
      fun.Domainp_rel Domainp_pred_fun_eq bi_unique_alt_def prod.Domainp_rel DomainPI)

lemma with_type_transfer_ab_group_add:
  assumes [transfer_rule]: ‹bi_unique r› ‹right_total r›
  shows ‹(WITH_TYPE_REL_ab_group_add r ===> (⟷))
         (WITH_TYPE_CLASS_ab_group_add (Collect (Domainp r))) (λ(p,z,m,u). class.ab_group_add p z m u)›
proof -
  define f where ‹f y = (SOME x. r x y)› for y
  have rf: ‹r x y ⟷ x = f y› for x y
    unfolding f_def
    apply (rule someI2_ex)
    using assms
    by (auto intro!: simp: right_total_def bi_unique_def)
  have inj: ‹inj f›
    using ‹bi_unique r›
    by (auto intro!: injI simp: bi_unique_def rf)
  show ?thesis
    unfolding WITH_TYPE_REL_ab_group_add_def rel_fun_def
    unfolding WITH_TYPE_CLASS_ab_group_add_def
    unfolding Domainp_iff rf
    using inj
    apply (simp add: class.ab_group_add_def class.comm_monoid_add_def
        class.ab_semigroup_add_def class.semigroup_add_def class.ab_semigroup_add_axioms_def
        class.comm_monoid_add_axioms_def class.ab_group_add_axioms_def inj_def)
    apply safe
    by metis+
qed


setup ‹
With_Type.add_with_type_info_global {
  class = \<^class>‹ab_group_add›,
  param_names = ["plus", "zero", "minus", "uminus"],
  rep_class = \<^const_name>‹WITH_TYPE_CLASS_ab_group_add›,
  rep_rel = \<^const_name>‹WITH_TYPE_REL_ab_group_add›,
  with_type_wellformed = @{thm with_type_wellformed_ab_group_add},
  transfer = SOME @{thm with_type_transfer_ab_group_add},
  rep_rel_itself = NONE
}
›

subsubsection ‹Example›

definition carrier_group where ‹carrier_group = (carrier_plus, 0::int, (λ i j. (i - j) mod 3), (λi. (- i) mod 3))›

lemma carrier_ab_group_add[with_type_intros]: ‹WITH_TYPE_CLASS_ab_group_add carrier carrier_group›
  by (auto simp: WITH_TYPE_CLASS_ab_group_add_def carrier_plus_def
        carrier_def carrier_group_def)

declare [[show_sorts=false]]
lemma example_ab_group:
  shows ‹let 't::ab_group_add = carrier with carrier_group in ∀x y.
    (plus_t x y = plus_t y x ∧ plus_t x (plus_t x x) = plus_t (plus_t x x) x)›
proof with_type_intro
  show ‹carrier ≠ {}› by simp
  fix Rep :: ‹'t ⇒ int› and t_ops
  assume wt: ‹WITH_TYPE_REL_ab_group_add (λx y. x = Rep y) carrier_group t_ops›
  define plus zero minus uminus where ‹plus = fst t_ops›
    and ‹zero = fst (snd t_ops)›
    and ‹minus = fst (snd (snd t_ops))›
    and ‹uminus = snd (snd (snd t_ops))›

  assume ‹bij_betw Rep UNIV carrier›
  then interpret type_definition Rep ‹inv Rep› carrier
    by (simp add: type_definition_bij_betw_iff)

  define r where ‹r = (λx y. x = Rep y)›
  have [transfer_rule]: ‹bi_unique r›
    by (simp add: Rep_inject bi_unique_def r_def)
  have [transfer_rule]: ‹right_total r›
    by (simp add: r_def right_total_def)
  from wt have transfer_carrier[transfer_rule]: ‹((r ===> r ===> r) *** r *** (r ===> r ===> r) *** (r ===> r)) carrier_group t_ops›
    by (simp add: r_def WITH_TYPE_REL_ab_group_add_def)
  have transfer_plus[transfer_rule]: ‹(r ===> r ===> r) carrier_plus plus›
    apply (subst asm_rl[of ‹carrier_plus = fst (carrier_group)›])
     apply (simp add: carrier_group_def)
    unfolding plus_def
    by transfer_prover
  have dom_r: ‹Collect (Domainp r) = carrier›
    by (auto elim!: Rep_cases simp: Rep r_def Domainp_iff)
  
  from with_type_transfer_ab_group_add[OF ‹bi_unique r› ‹right_total r›]
  have [transfer_rule]: ‹((r ===> r ===> r) ===> r ===> (r ===> r ===> r) ===> (r ===> r) ===> (⟷))
                         (λp z m u. WITH_TYPE_CLASS_ab_group_add carrier (p,z,m,u)) class.ab_group_add›
    unfolding dom_r WITH_TYPE_REL_ab_group_add_def
    by (auto intro!: simp: rel_fun_def)

  interpret ab_group_add plus zero minus uminus
    unfolding zero_def plus_def minus_def uminus_def
    apply transfer
    using carrier_ab_group_add dom_r
    by (auto intro!: simp: Let_def case_prod_beta)

  have 1: ‹plus x y = plus y x› for x y
    ― ‹We could prove this simply with ‹by (simp add: add_commute)›, but we use the approach of
      going to the concrete type for demonstration.›
    apply transfer
    apply (simp add: carrier_plus_def)
    by presburger

  have 2: ‹plus x (plus x x) = plus (plus x x) x› for x
    by (simp add: add_assoc)

  from 1 2
  show ‹∀x y. plus x y = plus y x ∧ plus x (plus x x) = plus (plus x x) x›
    by (simp add: plus_def case_prod_beta)
qed

lemma artificial_lemma': ‹(∃p (x::_::group_add) y. p x y = p y x) ⟹ prime (2305843009213693951 :: nat)›
proof - ― ‹This proof can be ignored. We just didn't want to have a "sorry" in the theory file›
  have "prime (2 ^ 61 - 1 :: nat)"
    by (subst lucas_lehmer_correct') eval
  also have ‹… = 2305843009213693951›
    by eval
  finally show ‹prime (2305843009213693951 :: nat)›
    by -
qed

lemma prime_2305843009213693951: ‹prime (2305843009213693951 :: nat)›
proof -
  from example_ab_group
  have ‹let 't::ab_group_add = carrier with carrier_group in prime (2305843009213693951 :: nat)›
  proof with_type_mp
    with_type_case
    show ‹prime (2305843009213693951 :: nat)›
      apply (rule artificial_lemma')
      using with_type_mp.premise by auto
  qed
  from this[cancel_with_type]
  show ?thesis
    by -
qed


end