Theory Perron_Frobenius.Cancel_Card_Constraint

(* Author: R. Thiemann *)
section ‹Elimination of CARD('n)›

text ‹In the following theory we provide a method which modifies theorems
  of the form $P[CARD('n)]$ into $n != 0 \Longrightarrow P[n]$, so that they can more
  easily be applied.
  
  Known issues: there might be problems with nested meta-implications and meta-quantification.›

theory Cancel_Card_Constraint
imports 
  "HOL-Types_To_Sets.Types_To_Sets"
  "HOL-Library.Cardinality"
begin

lemma n_zero_nonempty: "n ≠ 0 ⟹ {0 ..< n :: nat} ≠ {}" by auto

lemma type_impl_card_n: assumes "∃(Rep :: 'a ⇒ nat) Abs. type_definition Rep Abs {0 ..< n :: nat}"
  shows "class.finite (TYPE('a)) ∧ CARD('a) = n"
proof -
  from assms obtain rep :: "'a ⇒ nat" and abs :: "nat ⇒ 'a" where t: "type_definition rep abs {0 ..< n}" by auto
  have "card (UNIV :: 'a set) = card {0 ..< n}" using t by (rule type_definition.card)
  also have "… = n" by auto
  finally have bn: "CARD ('a) = n" .
  have "finite (abs ` {0 ..< n})" by auto
  also have "abs ` {0 ..< n} = UNIV" using t by (rule type_definition.Abs_image)
  finally have "class.finite (TYPE('a))" unfolding class.finite_def .
  with bn show ?thesis by blast
qed  

ML_file ‹cancel_card_constraint.ML›


(* below you find an example what the attribute cancel_card_constraint can do and how
   it works internally *)

(*
(* input: some type based lemma with CARD inside, like t0 *)
consts P :: "nat ⇒ nat ⇒ bool" 
axiomatization where t0: "P (CARD ('a :: finite)) (CARD('a) * m)"

(* t0 is converted into a property without the cardinality constraint via the new attribute *)
lemma t_1_to_6: "n ≠ 0 ⟹ P n (n * m)"
  by (rule t0[cancel_card_constraint])

(* The internal steps are as follows. *)

(* 1st step: pull out CARD and introduce new variable n *)
lemma t1: "CARD('a :: finite) = n ⟹ P n (n * m)" 
  using t0[where 'a = 'a] by blast

(* 2nd step: get rid of sorts *)
lemma t2: "class.finite TYPE('a) ⟹ CARD('a) = n ⟹ P n (n * m)"
  by (rule t1[internalize_sort "?'a::finite"])

(* 3rd step: restructure thm so that first two assumptions are merged into one *)
lemma t3: "class.finite TYPE('a) ∧ CARD('a) = n ⟹ P n (n * m)" 
  using t2 by blast

(* 4th step: choose an appropriate carrier set *)
lemma t4: "∃Rep Abs. type_definition Rep Abs {0..<n} ⟹ P n (n * m)"
  by (rule t3[OF type_impl_card_n])

(* 5th step: cancel type definition *)
lemma t5: "{0..<n} ≠ {} ⟹ P n (n * m)"
  by (rule t4[cancel_type_definition])

(* 6th step: simplify non-empty assumption to obtain final theorem *)
lemma t6: "n ≠ 0 ⟹ P n (n * m)" 
  by (rule t5[OF n_zero_nonempty])
*)

end