부분 정의를 몫 유형으로 올림

Question

몫 유형 (natq)으로 옮기고 싶은 부분에 부분적으로 정의 된 연산자 (disj_union)가 있습니다. 도덕적으로,이 은이어야한다고 생각합니다. 동등한 클래스 에서 찾을 수 있기 때문에 연산자가 정의 된 대표자 인입니다. 그러나 disj_union은 부분적으로 만 정의 되었기 때문에 해제 된 정의가 동등성을 유지한다는 증거를 완성 할 수 없습니다. 아래의 이론 파일에서는 disj_union 연산자를 정의하는 한 가지 방법을 제안합니다.하지만 abs 및 Rep 함수가 많이 포함되어 있기 때문에 마음에 들지 않습니다. 제대로 작동하지 않을 것이라고 생각합니다. .

이사벨에서 몫을 사용하여 이런 종류의 것을 정의하는 좋은 방법은 무엇입니까?

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 

[*] 이것은 캡처 회피 교체 만 충돌하지 않는 변수 구속 조건을 정의하는 방법과 같은 좀; 알파 등가 클래스에서 다른 대표로 이름을 바꾸면 항상 만족할 수있는 조건입니다. 이 같은 (그냥 생각)에 대해 어떻게

Answer 1

:

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 

Answer 2

기록을 보려면 여기를 잘 피연산자 중 하나의 이름이 변경되는 약간의 개정 그이, 둘 (드레이의 제안입니다) 완료까지 수행 ...

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