2

disj_union商型 ( ) にリフトしたいセットに部分的に定義された演算子 (以下) がありますnatq。道徳的には、これは問題ないと思います。なぜなら、演算子が定義されている代表を等価クラスで見つけることが常に可能だからです[*]。disj_unionただし、は部分的にしか定義されていないため、リフトされた定義が等価性を保持するという証明を完成させることはできません。以下の私の理論ファイルでは、演算子を定義するために見つけた 1 つの方法を提案していますが、多くのand関数disj_unionを備えているので気に入らず、操作が難しいと思います (右?)。absRep

イザベルで商を使ってこの種のものを定義する良い方法は何ですか?

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

[*] これは、バインドされた変数が衝突しないという条件でのみキャプチャ回避置換が定義される方法に少し似ています。アルファ等価クラスの別の代表者に名前を変更することで常に満たすことができる条件。

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の提案です（まあ、オペランドの1つだけが名前変更され、両方ではなく名前が変更されているというわずかな修正）が完了まで実行されました...

(* 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 に答える