2

disj_union我想提升到商类型 ( ) 的集合上有一个部分定义的运算符 (下面natq)。从道德上讲，我认为这应该没问题，因为总是可以在等价类中找到定义了运算符 [*] 的一些代表。但是，我无法完成提升定义保留等价性的证明，因为disj_union只是部分定义。在下面的理论文件中，我提出了一种我找到的定义disj_union运算符的方法，但我不喜欢它，因为它具有很多功能，abs而且Rep我认为它很难使用（对吗？）。

使用 Isabelle 中的商来定义这种事情的好方法是什么？

theory My_Theory imports 
  "~~/src/HOL/Library/Quotient_Set" 
begin

(* A ∪-operator that is defined only on disjoint operands. *)
definition "X ∩ Y = {} ⟹ disj_union X Y ≡ X ∪ Y"

(* Two sets are equivalent if they have the same cardinality. *)
definition "card_eq X Y ≡ finite X ∧ finite Y ∧ card X = card Y"

(* Quotient sets of naturals by this equivalence. *)
quotient_type natq = "nat set" / partial: card_eq
proof (intro part_equivpI)
  show "∃x. card_eq x x" by (metis card_eq_def finite.emptyI)
  show "symp card_eq" by (metis card_eq_def symp_def)
  show "transp card_eq" by (metis card_eq_def transp_def)
qed

(* I want to lift my disj_union operator to the natq type. 
   But I cannot complete the proof, because disj_union is
   only partially defined. *)
lift_definition natq_add :: "natq ⇒ natq ⇒ natq"
is "disj_union"
oops

(* Here is another attempt to define natq_add. I think it
   is correct, but it looks hard to prove things about, 
   because it uses abstraction and representation functions
   explicitly. *)
definition natq_add :: "natq ⇒ natq ⇒ natq"
where "natq_add X Y ≡ 
  let (X',Y') = SOME (X',Y'). 
  X' ∈ Rep_natq X ∧ Y' ∈ Rep_natq Y ∧ X' ∩ Y' = {} 
  in abs_natq (disj_union X' Y')"

end

[*] 这有点像如何只在绑定变量不冲突的条件下定义避免捕获替换；始终可以通过重命名为 alpha 等价类中的另一个代表来满足的条件。

4

2 回答 2

2

像这样的东西怎么样（只是一个想法）：

definition disj_union' :: "nat set ⇒ nat set ⇒ nat set"
where "disj_union' X Y ≡ 
  let (X',Y') = SOME (X',Y'). 
  card_eq X' X ∧ card_eq Y' Y ∧ X' ∩ Y' = {} 
  in disj_union X' Y'"

lift_definition natq_add :: "natq ⇒ natq ⇒ natq"
is "disj_union'" oops
于 2013-03-12T15:13:13.507 回答
0

为了记录，这是 Ondřej 的建议（嗯，对其进行了轻微修改，其中只有一个操作数被重命名，而不是两个）执行完成......

(* A version of disj_union that is always defined. *)
definition disj_union' :: "nat set ⇒ nat set ⇒ nat set"
where "disj_union' X Y ≡ 
  let Y' = SOME Y'. 
  card_eq Y' Y ∧ X ∩ Y' = {} 
  in disj_union X Y'"

(* Can always choose a natural that is not in a given finite subset of ℕ. *)
lemma nats_infinite:
  fixes A :: "nat set"
  assumes "finite A"
  shows "∃x. x ∉ A"
proof (rule ccontr, simp)
  assume "∀x. x ∈ A"
  hence "A = UNIV" by fast
  hence "finite UNIV" using assms by fast
  thus False by fast
qed

(* Can always choose n naturals that are not in a given finite subset of ℕ. *)
lemma nat_renaming:
  fixes x :: "nat set" and n :: nat
  assumes "finite x" 
  shows "∃z'. finite z' ∧ card z' = n ∧ x ∩ z' = {}"
using assms
apply (induct n)
apply (intro exI[of _ "{}"], simp)
apply (clarsimp)
apply (rule_tac x="insert (SOME y. y ∉ x ∪ z') z'" in exI)
apply (intro conjI, simp)
apply (rule someI2_ex, rule nats_infinite, simp, simp)+
done

lift_definition natq_add :: "natq ⇒ natq ⇒ natq"
is "disj_union'"
apply (unfold disj_union'_def card_eq_def)
apply (rule someI2_ex, simp add: nat_renaming)
apply (rule someI2_ex, simp add: nat_renaming)
apply (metis card.union_inter_neutral disj_union_def empty_iff finite_Un)
done
于 2013-03-13T10:43:18.523 回答