类型定义为 0 到 7 nat 的 CARD
CARD of typedef of 0 to 7 nat
更新 2 (151015)
我在下面放了一些来源。它显示了我可能使用的框架。
在一些帮助下，我变得更加老练了。我现在知道了数字类型类型和数字类型常量之间的区别。符号都是一样的，我习惯于使用按术语而不是类型操作的函数。使用 CARD，这改变了一些范例。
就数字类型表示法而言，即使使用 show_consts，我看的是类型或术语也不明显。所以，我总是使用 show_sorts 和 show_consts。一个 0 元类型的构造函数类型，如 nat，永远不会被注释。知道这有帮助。
我说过某个定理在不导入的情况下无法被魔术证明Numeral_Type，但事实并非如此。
简洁的语法很重要，因此获得良好的类型推断也很重要。看起来我在使用数字类型时得到了很好的类型推断。
从回答中，我也第一次使用了虚拟类型，在这一点上，这似乎是一种更好的做事方式。
这是一些来源：
theory i151013c_numeral_has_type_enforcement
imports Complex_Main "~~/src/HOL/Library/Numeral_Type"
begin
declare [[show_sorts, show_consts]]
datatype ('a,'size) vD = vC "'a list"
definition CARD_foo :: "('a,'s::{finite,card_UNIV}) vD => ('a,'s) vD => nat"
where
"CARD_foo x y = card (UNIV :: 's set)"
notation (input) vC ("vC|_" [1000] 1000)
notation (output) vC ("vC|_" [1000] 999)
value "CARD_foo (vC|x::(nat,32) vD) vC|y = (32::nat)" (*True*)
value "CARD_foo (vC|x::(nat,65536) vD) vC|y = 65536" (*True*)
type_synonym nv3 = "(nat, 3) vD"
notation CARD_foo (infixl "*+*" 65)
value "vC|m *+* (vC|n::nv3) = 3" (*True*)
type_notation (input) vD ("< _ , _ >")
term "x::<'a,'s::{finite,card_UNIV}>"
term "vC|m *+* (vC|n::<'a,64>) = 64"
value "vC|m *+* (vC|n::<'a,64>) = 64" (*True*)
(*Next, Am I adding 2 types of type numeral? Or am I adding 2 constants of
type numeral, which produces a numeral type? The notation for numeral types
and numeral type constants is identical.*)
value "vC|[3] *+* (vC|y::<nat,2 + 3>)"
term "vC|[3] *+* (vC|y::<nat,2 + 3>)"
(*I guess 2 and 3 are types. In the output panel, 0-ary types, such as 'nat',
don't get annotated with anything, where nat constants do.*)
lemma "vC|[3] *+* (vC|y::<nat,2 + 3>) = 5"
by(simp add: CARD_foo_def)
(*Type error clash. Oh well. Just don't do that.*)
term "(vC|x::<'a,5>) *+* (vC|y::<'a,2 + 3>)"
definition vCARD :: "('a, 's::{finite,card_UNIV}) vD => nat" where
"vCARD x = CARD('s)"
declare vCARD_def [simp add]
lemma
"vCARD(x::<'a,'s::{finite,card_UNIV}>) =
vCARD(y::<'b,'s::{finite,card_UNIV}>)"
by(simp)
end
更新 (151014)
这里我向M.Eberl解释一下为什么我不使用数字类型，根据我所知道的和经历过的。
关于 typedef 的相关评论和过去的问题
不久前，我从 M.Eberl:
的回答中了解到 ~~/src/HOL/Library/Cardinality，以及 Numeral_Type
- Trying to generalize a bit vector that uses typedef, bool list, and nat length
该问题也与 typedef 有关。部分来自我当时的实验，我尽量远离 typedef, 并使用 datatype.
自带的魔法
即使在今天，由于抽象问题，我也开始遇到 sz8 typedef 无法与 value 一起使用的问题。回顾上面链接的答案后，它部分显示了要让 typedef 与 value 一起工作必须做些什么。我在包含的新资源中有一个 size8，它显示了我所做的。我认为 equal 函数存在问题，需要像上面的答案中所示那样修复它。
示例大小数据类型和矢量数据类型
现在，我对下面包含的第二个来源中的两个示例 datatype 发表一些评论。
大小类型的用例是矢量长度，其中矢量是列表。
大小类型强制执行二元运算，两个向量具有相同的长度。然后我只需要检查这两个向量的长度是否正确。
数字类型的问题是没有类型强制。我的示例函数具有以下签名，显示 datatype：
datatype ('a,'size) vD = vC "'a list" 'size
CARD_foo :: "(nat,'s::card_UNIV) vD => (nat,'s) vD => nat"
但我可以做到这一点：
term "CARD_foo (vC [] 10) (vC [] 11)"
其他评论在源中。我在最后有一个 typedef size8，目前我不知道如何解决它。
虽然数字类型没有类型强制，但我想我可以使用 CARD 来依赖类型大小，基于此：
theorem CARD_of_type_of_terms_of_same_type_are_equal:
"CARD_foo (vC n size1term) = CARD_foo (vC m size2term)"
unfolding CARD_foo_def
by(auto simp add: CARD_foo_def)
为了神奇地得到它，我不得不不导入 "~~/src/HOL/Library/Numeral_Type"。
感谢您的帮助。这是无价的，感谢您如何获得我最初要求的证明。它有助于在这里和那里学习有关 typedef.
的东西
新例子来源：
theory i151013b_2nd
imports Complex_Main (*"$GEZ/e/IsE"*)
"~~/src/HOL/Library/Cardinality" "~~/src/HOL/Library/Numeral_Type"
begin
declare [[show_sorts, show_consts]]
(*::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::*)
(*::¦ NUMERAL TYPE DOESN'T GUARANTEE TYPE ENFORCEMENT FOR A BINARY OP ¦:::*)
(*----------------------------*)
(*The size type as a datatype.*)
datatype sz8D = sz8C bool bool bool
(*-----------------------------------*)
(*Typdef 'n <= 7 would be preferable.*)
lemma UNIV_sz8D:
"UNIV =
{sz8C False False False, sz8C False False True, sz8C False True False,
sz8C False True True, sz8C True False False, sz8C True False True,
sz8C True True False, sz8C True True True}"
by(auto, metis (full_types) sz8D.exhaust)
lemma card_UNIV_sz8D [simp]: "card (UNIV :: sz8D set) = 8"
by(unfold UNIV_sz8D, auto)
instantiation sz8D :: card_UNIV
begin
definition "finite_UNIV = Phantom(sz8D) True"
definition "card_UNIV = Phantom(sz8D) 8"
instance
apply(default)
unfolding UNIV_sz8D finite_UNIV_sz8D_def card_UNIV_sz8D_def
by(auto)
end
(*-----------------------------------------*)
(*The vector type with an example function.*)
datatype ('a,'size) vD = vC "'a list" 'size
definition CARD_foo :: "(nat,'s::card_UNIV) vD => (nat,'s) vD => nat" where
"CARD_foo x y = card (UNIV :: 's set)"
thm CARD_foo_def
(*--------------------------------------------------------*)
(*sz8D: Size enforcement. Error if I mix other size types.*)
value "CARD_foo (vC [] (s::sz8D)) (vC [1] (t::sz8D))" (*outputs 8*)
value "CARD_foo (vC [] (sz8C False False False)) (vC [1] (t::sz8D))"
(*-------------------------------------*)
(*numeral: No enforcement of size type.*)
term "CARD_foo (vC [] 10) (vC [] 11)" (*
"CARD_foo (vC [] (10::'a::{card_UNIV,numeral}))
(vC [] (11::'a::{card_UNIV,numeral}))" :: "nat" *)
(*Can't eval the type to nat, even if they're the same*)
value "CARD_foo (vC [] 10) (vC [] 10)"
(*But here, CARDs are different anyway; no enforcement, no value.*)
value "CARD_foo (vC [] 10) (vC [] 11)" (*
"of_phantom card_UNIV_class.card_UNIV" :: "nat"*)
lemma "CARD_foo (vC [] 10) (vC [] 11) = z" oops (*
show_consts:
CARD_foo (vC [] (10::'a)) (vC [] (11::'a)) = z
'a :: {card_UNIV,numeral} *)
(*Can evaluate when there's not a conflict.*)
term "CARD(10)"
value "CARD(10)" (*outputs 10*)
lemma "CARD(10) = 10" by simp (*show_consts: 'UNIV :: 10 set'*)
value "CARD(11)" (*outputs 11*)
(*No eval if CARD('a) is used in a function.*)
definition fooID :: "'a::card_UNIV => nat" where
"fooID x = CARD('a)"
term "fooID(5)"
value "fooID(5)"
(*::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::*)
(*::¦ HOWEVER, BY FUNCTION UNIQUENESS, I SUPPOSE THERE'S NO AMBIGUITY ¦:::*)
(*[>) I have to drop down to only 'src/HOL/Library/Cardinality' to get this.
[>) For some reason, it won't unfold the definition.*)
theorem CARD_of_type_of_terms_of_same_type_are_equal:
"CARD_foo (vC n size_1term) = CARD_foo (vC m size_2term)"
unfolding CARD_foo_def
by(auto simp add: CARD_foo_def)
(*::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::*)
(*::¦ CAN'T USE TYPEDEF AFTERALL IF I CAN'T FIX THIS ¦::::::::::::::::::::*)
(*NOTE ABOUT PLUG'N'PLAY:
[>) See
[>) 'value' for 'CARD_foo' needs class 'equal'
[>) '[code abstract]' didn't work, so I used '[code]'.*)
typedef size8 = "{n::nat. n ≤ 7}"
morphisms size8_to_nat Abs_size8
by(blast)
definition nat_to_size8 :: "nat => size8" where
"nat_to_size8 n == if n ≤ 7 then Abs_size8 n else Abs_size8 0"
lemma nat_to_size8_code [code]:
"size8_to_nat (nat_to_size8 n) = (if n ≤ 7 then n else 0)"
unfolding nat_to_size8_def
by(simp add: Abs_size8_inverse)
setup_lifting type_definition_size8
instantiation size8 :: equal
begin
lift_definition equal_size8 :: "size8 => size8 => bool" is "λx y. x = y" .
instance
by(default, transfer, auto simp add: equal_size8_def)
end
instantiation size8 :: card_UNIV
begin
definition "finite_UNIV = Phantom(size8) True"
definition "card_UNIV = Phantom(size8) 8"
instance sorry
end
value "CARD_foo (vC [] (Abs_size8 0)) (vC [] (Abs_size8 0))" (*
Abstraction violation: constant Abs_size8 *)
end
原问题
我正在使用 typedef 来定义一些用作尺寸类型的类型，这样使用：CARD(sz8)。我可以使用 datatype，但它需要更长的时间才能自行设置。
我想我不明白如何用 typedef 为 sz8 生成的逆定理证明两个值是唯一的。
我有我的类型 sz8，我将其实例化为 card_UNIV。不完整的是我的定理 card_UNIV_sz8，即 "card (UNIV::sz8 set) = 8".
theory i151013a
imports Complex_Main "~~/src/HOL/Library/Cardinality"
"$GEZ/e/IsE"
begin
declare [[show_sorts, show_consts]]
typedef sz8 = "{n::nat. n ≤ 7}"
by(blast)
theorem UNIV_sz8:
"UNIV = {s::sz8. ∃n. n ≤ 7 ∧ s = Abs_sz8 n}"
using Rep_sz8 Rep_sz8_inverse
by(fastforce)
theorem foo1:
assumes "Abs_sz8 n ∈ {s::sz8. ∃n ≤ 7. s = Abs_sz8 n}"
shows "n ∈ {n. n ≤ 7}"
proof
fix n :: nat
note assms
obtain n1 where
f1: "n1 ≤ (7::nat) ∧ Abs_sz8 n = Abs_sz8 n1"
using Rep_sz8 Rep_sz8_inverse
by(fastforce)
hence "n = n1"
oops
find_theorems name: "sz8"
instance sz8 :: finite
apply default
unfolding UNIV_sz8
by(simp)
theorem card_UNIV_sz8 [simp]:
"card (UNIV::sz8 set) = 8"
unfolding UNIV_sz8
sorry
instantiation sz8 :: card_UNIV
begin
definition "finite_UNIV = Phantom(sz8) True"
definition "card_UNIV = Phantom(sz8) 8"
instance
apply default
unfolding finite_UNIV_sz8_def card_UNIV_sz8_def
by(simp_all)
end
end
您问题的答案
首先：我会回答你的问题，然后我会告诉你为什么你正在做的事情是不必要的。
您可以使用定理 sz8.Abs_sz8_inject 显示值的不同性，如果您这样做 find_theorems Abs_sz8:
(?x::nat) ∈ {n::nat. n ≤ (7::nat)} ⟹
(?y::nat) ∈ {n::nat. n ≤ (7::nat)} ⟹
(Abs_sz8 ?x = Abs_sz8 ?y) = (?x = ?y)
你可以证明你的定理，例如像这样：
lemma sz8_image: "x ∈ Abs_sz8 ` {0..7}"
by (cases x rule: sz8.Abs_sz8_cases) auto
theorem card_UNIV_sz8 [simp]: "card (UNIV::sz8 set) = 8"
proof -
from sz8_image have "UNIV = Abs_sz8 ` {0..7}" by blast
also from sz8.Abs_sz8_inject have "card … = card {0..(7::nat)}"
by (intro card_image inj_onI) simp_all
finally show ?thesis by simp
qed
你应该怎么做
看看理论~~/src/HOL/Library/Numeral_Type，其中~~代表伊莎贝尔根目录。
这为每个正整数 n 定义了一个类型 n，它恰好包含从 0 到 n - 1 的数字，甚至定义了许多类型类实例和模块化对他们算术。例如：
value "(2 - 5 :: 10) = 7"
> "True" :: "bool"
这可能正是您想要的，而且它已完全设置好；手工完成所有这些非常乏味，如果您需要 16 号类型，则必须重新做同样的事情。
更新：关于数字类型的更多信息
在您更新的问题中，您声称数字类型的类型检查不起作用。那是不正确的；问题仅仅是 vC [] 10 中的 10 没有意义。您的意图可能是指定该函数类型中的长度参数 'size 必须为 10.
但是，每个 数字类型都包含一个 10。例如，(10 :: 5) = 0 和 (10 :: 6) = 4。所以里面的10和11根本不会造成任何类型限制。
你要做的是在类型级别上约束'size：
datatype ('a,'size) vD = vC "'a list"
consts CARD_foo :: "(nat,'s::card_UNIV) vD => (nat,'s) vD => nat"
term "CARD_foo (vC [] :: (nat, 10) vD) (vC [] :: (nat, 11) vD)"
(* Type error *)
如果你真的想在价值层面上做一些类似于你试图做的事情，你可以使用以下技巧：
datatype ('a,'size) vD = vC "'a list" "'size itself"
consts CARD_foo :: "(nat,'s::card_UNIV) vD => (nat,'s) vD => nat"
term "CARD_foo (vC [] TYPE(10)) (vC [] TYPE(11))"
'a itself 基本上是一个包含值 TYPE('a) 的单例类型。我认为没有这些 itself 值的变体在长 运行 中可能更方便。
至于为什么你的 CARD_of_type_of_terms_of_same_type_are_equal 不起作用，我不能在没有看到所涉及的常量定义的情况下说，我很确定所有适用于你手工制作的 sz8 类型的东西都会使用数字类型。
归根结底，您始终可以将代码中所有地方的 sz8 替换为 8，一切都应该仍然有效。
更新 2 (151015)
我在下面放了一些来源。它显示了我可能使用的框架。
在一些帮助下，我变得更加老练了。我现在知道了数字类型类型和数字类型常量之间的区别。符号都是一样的，我习惯于使用按术语而不是类型操作的函数。使用 CARD，这改变了一些范例。
就数字类型表示法而言，即使使用 show_consts，我看的是类型或术语也不明显。所以，我总是使用 show_sorts 和 show_consts。一个 0 元类型的构造函数类型，如 nat，永远不会被注释。知道这有帮助。
我说过某个定理在不导入的情况下无法被魔术证明Numeral_Type，但事实并非如此。
简洁的语法很重要，因此获得良好的类型推断也很重要。看起来我在使用数字类型时得到了很好的类型推断。
从回答中，我也第一次使用了虚拟类型，在这一点上，这似乎是一种更好的做事方式。
这是一些来源：
theory i151013c_numeral_has_type_enforcement
imports Complex_Main "~~/src/HOL/Library/Numeral_Type"
begin
declare [[show_sorts, show_consts]]
datatype ('a,'size) vD = vC "'a list"
definition CARD_foo :: "('a,'s::{finite,card_UNIV}) vD => ('a,'s) vD => nat"
where
"CARD_foo x y = card (UNIV :: 's set)"
notation (input) vC ("vC|_" [1000] 1000)
notation (output) vC ("vC|_" [1000] 999)
value "CARD_foo (vC|x::(nat,32) vD) vC|y = (32::nat)" (*True*)
value "CARD_foo (vC|x::(nat,65536) vD) vC|y = 65536" (*True*)
type_synonym nv3 = "(nat, 3) vD"
notation CARD_foo (infixl "*+*" 65)
value "vC|m *+* (vC|n::nv3) = 3" (*True*)
type_notation (input) vD ("< _ , _ >")
term "x::<'a,'s::{finite,card_UNIV}>"
term "vC|m *+* (vC|n::<'a,64>) = 64"
value "vC|m *+* (vC|n::<'a,64>) = 64" (*True*)
(*Next, Am I adding 2 types of type numeral? Or am I adding 2 constants of
type numeral, which produces a numeral type? The notation for numeral types
and numeral type constants is identical.*)
value "vC|[3] *+* (vC|y::<nat,2 + 3>)"
term "vC|[3] *+* (vC|y::<nat,2 + 3>)"
(*I guess 2 and 3 are types. In the output panel, 0-ary types, such as 'nat',
don't get annotated with anything, where nat constants do.*)
lemma "vC|[3] *+* (vC|y::<nat,2 + 3>) = 5"
by(simp add: CARD_foo_def)
(*Type error clash. Oh well. Just don't do that.*)
term "(vC|x::<'a,5>) *+* (vC|y::<'a,2 + 3>)"
definition vCARD :: "('a, 's::{finite,card_UNIV}) vD => nat" where
"vCARD x = CARD('s)"
declare vCARD_def [simp add]
lemma
"vCARD(x::<'a,'s::{finite,card_UNIV}>) =
vCARD(y::<'b,'s::{finite,card_UNIV}>)"
by(simp)
end
更新 (151014)
这里我向M.Eberl解释一下为什么我不使用数字类型，根据我所知道的和经历过的。
关于 typedef 的相关评论和过去的问题
不久前，我从 M.Eberl:
的回答中了解到~~/src/HOL/Library/Cardinality，以及 Numeral_Type
- Trying to generalize a bit vector that uses typedef, bool list, and nat length
该问题也与 typedef 有关。部分来自我当时的实验，我尽量远离 typedef, 并使用 datatype.
即使在今天，由于抽象问题，我也开始遇到 sz8 typedef 无法与 value 一起使用的问题。回顾上面链接的答案后，它部分显示了要让 typedef 与 value 一起工作必须做些什么。我在包含的新资源中有一个 size8，它显示了我所做的。我认为 equal 函数存在问题，需要像上面的答案中所示那样修复它。
示例大小数据类型和矢量数据类型
现在，我对下面包含的第二个来源中的两个示例 datatype 发表一些评论。
大小类型的用例是矢量长度，其中矢量是列表。
大小类型强制执行二元运算，两个向量具有相同的长度。然后我只需要检查这两个向量的长度是否正确。
数字类型的问题是没有类型强制。我的示例函数具有以下签名，显示 datatype：
datatype ('a,'size) vD = vC "'a list" 'size
CARD_foo :: "(nat,'s::card_UNIV) vD => (nat,'s) vD => nat"
但我可以做到这一点：
term "CARD_foo (vC [] 10) (vC [] 11)"
其他评论在源中。我在最后有一个 typedef size8，目前我不知道如何解决它。
虽然数字类型没有类型强制，但我想我可以使用 CARD 来依赖类型大小，基于此：
theorem CARD_of_type_of_terms_of_same_type_are_equal:
"CARD_foo (vC n size1term) = CARD_foo (vC m size2term)"
unfolding CARD_foo_def
by(auto simp add: CARD_foo_def)
为了神奇地得到它，我不得不不导入 "~~/src/HOL/Library/Numeral_Type"。
感谢您的帮助。这是无价的，感谢您如何获得我最初要求的证明。它有助于在这里和那里学习有关 typedef.
新例子来源：
theory i151013b_2nd
imports Complex_Main (*"$GEZ/e/IsE"*)
"~~/src/HOL/Library/Cardinality" "~~/src/HOL/Library/Numeral_Type"
begin
declare [[show_sorts, show_consts]]
(*::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::*)
(*::¦ NUMERAL TYPE DOESN'T GUARANTEE TYPE ENFORCEMENT FOR A BINARY OP ¦:::*)
(*----------------------------*)
(*The size type as a datatype.*)
datatype sz8D = sz8C bool bool bool
(*-----------------------------------*)
(*Typdef 'n <= 7 would be preferable.*)
lemma UNIV_sz8D:
"UNIV =
{sz8C False False False, sz8C False False True, sz8C False True False,
sz8C False True True, sz8C True False False, sz8C True False True,
sz8C True True False, sz8C True True True}"
by(auto, metis (full_types) sz8D.exhaust)
lemma card_UNIV_sz8D [simp]: "card (UNIV :: sz8D set) = 8"
by(unfold UNIV_sz8D, auto)
instantiation sz8D :: card_UNIV
begin
definition "finite_UNIV = Phantom(sz8D) True"
definition "card_UNIV = Phantom(sz8D) 8"
instance
apply(default)
unfolding UNIV_sz8D finite_UNIV_sz8D_def card_UNIV_sz8D_def
by(auto)
end
(*-----------------------------------------*)
(*The vector type with an example function.*)
datatype ('a,'size) vD = vC "'a list" 'size
definition CARD_foo :: "(nat,'s::card_UNIV) vD => (nat,'s) vD => nat" where
"CARD_foo x y = card (UNIV :: 's set)"
thm CARD_foo_def
(*--------------------------------------------------------*)
(*sz8D: Size enforcement. Error if I mix other size types.*)
value "CARD_foo (vC [] (s::sz8D)) (vC [1] (t::sz8D))" (*outputs 8*)
value "CARD_foo (vC [] (sz8C False False False)) (vC [1] (t::sz8D))"
(*-------------------------------------*)
(*numeral: No enforcement of size type.*)
term "CARD_foo (vC [] 10) (vC [] 11)" (*
"CARD_foo (vC [] (10::'a::{card_UNIV,numeral}))
(vC [] (11::'a::{card_UNIV,numeral}))" :: "nat" *)
(*Can't eval the type to nat, even if they're the same*)
value "CARD_foo (vC [] 10) (vC [] 10)"
(*But here, CARDs are different anyway; no enforcement, no value.*)
value "CARD_foo (vC [] 10) (vC [] 11)" (*
"of_phantom card_UNIV_class.card_UNIV" :: "nat"*)
lemma "CARD_foo (vC [] 10) (vC [] 11) = z" oops (*
show_consts:
CARD_foo (vC [] (10::'a)) (vC [] (11::'a)) = z
'a :: {card_UNIV,numeral} *)
(*Can evaluate when there's not a conflict.*)
term "CARD(10)"
value "CARD(10)" (*outputs 10*)
lemma "CARD(10) = 10" by simp (*show_consts: 'UNIV :: 10 set'*)
value "CARD(11)" (*outputs 11*)
(*No eval if CARD('a) is used in a function.*)
definition fooID :: "'a::card_UNIV => nat" where
"fooID x = CARD('a)"
term "fooID(5)"
value "fooID(5)"
(*::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::*)
(*::¦ HOWEVER, BY FUNCTION UNIQUENESS, I SUPPOSE THERE'S NO AMBIGUITY ¦:::*)
(*[>) I have to drop down to only 'src/HOL/Library/Cardinality' to get this.
[>) For some reason, it won't unfold the definition.*)
theorem CARD_of_type_of_terms_of_same_type_are_equal:
"CARD_foo (vC n size_1term) = CARD_foo (vC m size_2term)"
unfolding CARD_foo_def
by(auto simp add: CARD_foo_def)
(*::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::*)
(*::¦ CAN'T USE TYPEDEF AFTERALL IF I CAN'T FIX THIS ¦::::::::::::::::::::*)
(*NOTE ABOUT PLUG'N'PLAY:
[>) See
[>) 'value' for 'CARD_foo' needs class 'equal'
[>) '[code abstract]' didn't work, so I used '[code]'.*)
typedef size8 = "{n::nat. n ≤ 7}"
morphisms size8_to_nat Abs_size8
by(blast)
definition nat_to_size8 :: "nat => size8" where
"nat_to_size8 n == if n ≤ 7 then Abs_size8 n else Abs_size8 0"
lemma nat_to_size8_code [code]:
"size8_to_nat (nat_to_size8 n) = (if n ≤ 7 then n else 0)"
unfolding nat_to_size8_def
by(simp add: Abs_size8_inverse)
setup_lifting type_definition_size8
instantiation size8 :: equal
begin
lift_definition equal_size8 :: "size8 => size8 => bool" is "λx y. x = y" .
instance
by(default, transfer, auto simp add: equal_size8_def)
end
instantiation size8 :: card_UNIV
begin
definition "finite_UNIV = Phantom(size8) True"
definition "card_UNIV = Phantom(size8) 8"
instance sorry
end
value "CARD_foo (vC [] (Abs_size8 0)) (vC [] (Abs_size8 0))" (*
Abstraction violation: constant Abs_size8 *)
end
原问题
我正在使用 typedef 来定义一些用作尺寸类型的类型，这样使用：CARD(sz8)。我可以使用 datatype，但它需要更长的时间才能自行设置。
我想我不明白如何用 typedef 为 sz8 生成的逆定理证明两个值是唯一的。
我有我的类型 sz8，我将其实例化为 card_UNIV。不完整的是我的定理 card_UNIV_sz8，即 "card (UNIV::sz8 set) = 8".
theory i151013a
imports Complex_Main "~~/src/HOL/Library/Cardinality"
"$GEZ/e/IsE"
begin
declare [[show_sorts, show_consts]]
typedef sz8 = "{n::nat. n ≤ 7}"
by(blast)
theorem UNIV_sz8:
"UNIV = {s::sz8. ∃n. n ≤ 7 ∧ s = Abs_sz8 n}"
using Rep_sz8 Rep_sz8_inverse
by(fastforce)
theorem foo1:
assumes "Abs_sz8 n ∈ {s::sz8. ∃n ≤ 7. s = Abs_sz8 n}"
shows "n ∈ {n. n ≤ 7}"
proof
fix n :: nat
note assms
obtain n1 where
f1: "n1 ≤ (7::nat) ∧ Abs_sz8 n = Abs_sz8 n1"
using Rep_sz8 Rep_sz8_inverse
by(fastforce)
hence "n = n1"
oops
find_theorems name: "sz8"
instance sz8 :: finite
apply default
unfolding UNIV_sz8
by(simp)
theorem card_UNIV_sz8 [simp]:
"card (UNIV::sz8 set) = 8"
unfolding UNIV_sz8
sorry
instantiation sz8 :: card_UNIV
begin
definition "finite_UNIV = Phantom(sz8) True"
definition "card_UNIV = Phantom(sz8) 8"
instance
apply default
unfolding finite_UNIV_sz8_def card_UNIV_sz8_def
by(simp_all)
end
end
您问题的答案
首先：我会回答你的问题，然后我会告诉你为什么你正在做的事情是不必要的。
您可以使用定理 sz8.Abs_sz8_inject 显示值的不同性，如果您这样做 find_theorems Abs_sz8:
(?x::nat) ∈ {n::nat. n ≤ (7::nat)} ⟹
(?y::nat) ∈ {n::nat. n ≤ (7::nat)} ⟹
(Abs_sz8 ?x = Abs_sz8 ?y) = (?x = ?y)
你可以证明你的定理，例如像这样：
lemma sz8_image: "x ∈ Abs_sz8 ` {0..7}"
by (cases x rule: sz8.Abs_sz8_cases) auto
theorem card_UNIV_sz8 [simp]: "card (UNIV::sz8 set) = 8"
proof -
from sz8_image have "UNIV = Abs_sz8 ` {0..7}" by blast
also from sz8.Abs_sz8_inject have "card … = card {0..(7::nat)}"
by (intro card_image inj_onI) simp_all
finally show ?thesis by simp
qed
你应该怎么做
看看理论~~/src/HOL/Library/Numeral_Type，其中~~代表伊莎贝尔根目录。
这为每个正整数 n 定义了一个类型 n，它恰好包含从 0 到 n - 1 的数字，甚至定义了许多类型类实例和模块化对他们算术。例如：
value "(2 - 5 :: 10) = 7"
> "True" :: "bool"
这可能正是您想要的，而且它已完全设置好；手工完成所有这些非常乏味，如果您需要 16 号类型，则必须重新做同样的事情。
更新：关于数字类型的更多信息
在您更新的问题中，您声称数字类型的类型检查不起作用。那是不正确的；问题仅仅是 vC [] 10 中的 10 没有意义。您的意图可能是指定该函数类型中的长度参数 'size 必须为 10.
但是，每个 数字类型都包含一个 10。例如，(10 :: 5) = 0 和 (10 :: 6) = 4。所以里面的10和11根本不会造成任何类型限制。
你要做的是在类型级别上约束'size：
datatype ('a,'size) vD = vC "'a list"
consts CARD_foo :: "(nat,'s::card_UNIV) vD => (nat,'s) vD => nat"
term "CARD_foo (vC [] :: (nat, 10) vD) (vC [] :: (nat, 11) vD)"
(* Type error *)
如果你真的想在价值层面上做一些类似于你试图做的事情，你可以使用以下技巧：
datatype ('a,'size) vD = vC "'a list" "'size itself"
consts CARD_foo :: "(nat,'s::card_UNIV) vD => (nat,'s) vD => nat"
term "CARD_foo (vC [] TYPE(10)) (vC [] TYPE(11))"
'a itself 基本上是一个包含值 TYPE('a) 的单例类型。我认为没有这些 itself 值的变体在长 运行 中可能更方便。
至于为什么你的 CARD_of_type_of_terms_of_same_type_are_equal 不起作用，我不能在没有看到所涉及的常量定义的情况下说，我很确定所有适用于你手工制作的 sz8 类型的东西都会使用数字类型。
归根结底，您始终可以将代码中所有地方的 sz8 替换为 8，一切都应该仍然有效。