(* 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