如何爲一個歸納數據類型定義Sup？

Question

這裏是一個簡單的類型系統，具有以下類型：any，void，integer，real，set。

datatype ty = 
    AType 
| VType 
| IType 
| RType 
| SType ty 

類型形成確半格：

notation sup (infixl "⊔" 65) 

instantiation ty :: semilattice_sup 
begin 

inductive less_ty where 
    "τ ≠ VType ⟹ VType < τ" 
| "τ ≠ AType ⟹ τ < AType" 
| "IType < RType" 
| "τ < σ ⟹ SType τ < SType σ" 

inductive_cases VType_less [elim!]: "VType < τ" 
inductive_cases less_AType [elim!]: "τ < AType" 
inductive_cases IType_less_RType [elim!]: "IType < RType" 
inductive_cases SType_less_SType [elim!]: "SType τ < SType σ" 
inductive_cases less_SType [elim!]: "τ < SType σ" 
inductive_cases SType_less [elim!]: "SType τ < σ" 

fun less_ty_fun where 
    "less_ty_fun VType τ = (τ ≠ VType)" 
| "less_ty_fun τ VType = False" 
| "less_ty_fun AType τ = False" 
| "less_ty_fun τ AType = (τ ≠ AType)" 
| "less_ty_fun IType RType = True" 
| "less_ty_fun (SType τ) (SType σ) = (τ < σ)" 
| "less_ty_fun _ _ = False" 

lemma less_ty_code [code]: 
    "τ < σ = less_ty_fun τ σ" 
    for τ σ :: ty 
    apply (rule iffI) 
    apply (induct rule: less_ty.induct) 
    apply simp 
    using less_ty_fun.simps(10) ty.exhaust apply force 
    apply simp 
    apply simp 
    apply (erule less_ty_fun.elims; simp add: less_ty.intros) 
    done 

definition "τ ≤ σ ≡ τ = σ ∨ τ < σ" for τ σ :: ty 

fun sup_ty where 
    "VType ⊔ τ = τ" 
| "τ ⊔ VType = τ" 
| "AType ⊔ τ = AType" 
| "τ ⊔ AType = AType" 
| "IType ⊔ IType = IType" 
| "IType ⊔ RType = RType" 
| "RType ⊔ IType = RType" 
| "RType ⊔ RType = RType" 
| "SType τ ⊔ SType σ = SType (τ ⊔ σ)" 
| "SType _ ⊔ _ = AType" 
| "_ ⊔ SType _ = AType" 

lemma less_le_not_le_ty: 
    "τ < σ ⟷ τ ≤ σ ∧ ¬ σ ≤ τ" for τ σ :: ty 
    apply (rule iffI; auto simp add: less_eq_ty_def) 
    apply (induct τ arbitrary: σ; auto) 
    using less_ty.cases apply fastforce 
    using less_ty.cases apply fastforce 
    using less_ty.cases apply fastforce 
    apply (induct rule: less_ty.induct) 
    using less_ty.cases apply blast+ 
    done 

lemma order_refl_ty [iff]: "τ ≤ τ" for τ :: ty 
    by (simp add: less_eq_ty_def) 

lemma order_trans_ty: 
    "τ ≤ σ ⟹ σ ≤ ρ ⟹ τ ≤ ρ" for τ σ ρ :: ty 
    apply (auto simp add: less_eq_ty_def) 
    apply (erule notE) 
    apply (induct τ arbitrary: σ ρ) 
    using less_ty.cases apply blast 
    apply (metis less_le_not_le_ty less_ty.intros(1)) 
    apply (metis less_ty.simps ty.distinct(1) ty.distinct(19) ty.distinct(3) ty.distinct(7) ty.simps(13) ty.simps(19)) 
    apply (metis less_ty.simps ty.distinct(1) ty.distinct(19) ty.distinct(3) ty.distinct(7) ty.simps(13)) 
    apply (metis less_ty.simps ty.distinct(1) ty.distinct(17) ty.distinct(3) ty.distinct(7) ty.inject ty.simps(15)) 
    done 

lemma antisym_ty: 
    "τ ≤ σ ⟹ σ ≤ τ ⟹ τ = σ" for τ σ :: ty 
    by (simp add: less_eq_ty_def; auto simp add: less_le_not_le_ty) 

lemma sup_ge1_ty_IType: 
    "IType = IType ⊔ σ ∨ IType < IType ⊔ σ" 
    by (cases σ; simp add: less_ty.intros) 

lemma sup_ge1_ty_RType: 
    "RType = RType ⊔ σ ∨ RType < RType ⊔ σ" 
    by (cases σ; simp add: less_ty.intros) 

lemma sup_ge1_ty_SType: 
    "(⋀σ. τ = τ ⊔ σ ∨ τ < τ ⊔ σ) ⟹ 
    SType τ = SType τ ⊔ σ ∨ SType τ < SType τ ⊔ σ" 
    apply (cases σ; simp add: less_ty.intros) 
    using less_ty.intros(4) by auto 

lemma sup_ge1_ty: "τ ≤ τ ⊔ σ" for τ σ :: ty 
    apply (induct τ arbitrary: σ; simp add: less_eq_ty_def) 
    apply (metis sup_ty.simps(2) sup_ty.simps(6) sup_ty.simps(7) sup_ty.simps(8) sup_ty.simps(9) ty.exhaust) 
    apply (metis less_ty.intros(1)) 
    using sup_ge1_ty_IType apply auto[1] 
    using sup_ge1_ty_RType apply auto[1] 
    using sup_ge1_ty_SType apply auto[1] 
    done 

lemma sup_commut_ty_AType: "AType ⊔ σ = σ ⊔ AType" by (cases σ; simp) 
lemma sup_commut_ty_VType: "VType ⊔ σ = σ ⊔ VType" by (cases σ; simp) 
lemma sup_commut_ty_IType: "IType ⊔ σ = σ ⊔ IType" by (cases σ; simp) 
lemma sup_commut_ty_RType: "RType ⊔ σ = σ ⊔ RType" by (cases σ; simp) 
lemma sup_commut_ty_SType: "(⋀σ. τ ⊔ σ = σ ⊔ τ) ⟹ SType τ ⊔ σ = σ ⊔ SType τ" by (cases σ; simp) 

lemma sup_commut_ty: 
    "τ ⊔ σ = σ ⊔ τ" 
    for τ σ :: ty 
    apply (induct τ arbitrary: σ) 
    using sup_commut_ty_AType apply auto[1] 
    using sup_commut_ty_VType apply auto[1] 
    using sup_commut_ty_IType apply auto[1] 
    using sup_commut_ty_RType apply auto[1] 
    using sup_commut_ty_SType apply auto[1] 
    done 

lemma sup_ty_idem: "τ ⊔ τ = τ" for τ :: ty by (induct τ; simp) 

lemma sup_ty_strict_order: 
    "σ < τ ⟹ τ ⊔ σ = τ" 
    for τ σ :: ty 
    apply (induct rule: less_ty.induct) 
    using sup_commut_ty sup_ty.simps(1) apply auto[1] 
    apply (meson antisym_ty less_eq_ty_def less_ty.simps sup_ge1_ty) 
    apply simp 
    apply simp 
    done 

lemma sup_less_eq_set: 
    "(⋀τ σ. τ < ρ ⟹ σ < ρ ⟹ τ ⊔ σ ≤ ρ) ⟹ 
    τ < SType ρ ⟹ 
    σ < SType ρ ⟹ 
    τ ⊔ σ ≤ SType ρ" 
    apply (cases τ; cases σ; auto) 
    apply (simp add: less_eq_ty_def less_ty.intros(1) sup_ty_idem) 
    apply (simp add: less_eq_ty_def less_ty.intros(4)) 
    apply (simp add: less_eq_ty_def less_ty.intros(4)) 
    apply (metis (mono_tags) less_eq_ty_def less_ty.intros(4)) 
    done 

lemma sup_ty_strict_order2_RType: 
    "τ < RType ⟹ σ < RType ⟹ τ ⊔ σ ≤ RType" 
    apply (cases τ; auto) 
    apply (simp add: less_ty_code) 
    apply (simp add: less_eq_ty_def) 
    apply (metis less_eq_ty_def less_ty.simps sup_ty.simps(13) sup_ty.simps(3) ty.distinct(19) ty.distinct(5)) 
    apply (simp add: less_ty_code) 
    done 

lemma sup_ty_strict_order2: 
    "τ < ρ ⟹ σ < ρ ⟹ τ ⊔ σ ≤ ρ" for τ σ ρ :: ty 
    apply (induct ρ arbitrary: τ σ) 
    using less_eq_ty_def less_ty.intros(2) apply blast 
    using less_ty.cases apply blast 
    using less_le_not_le_ty less_ty.cases apply fastforce 
    apply (simp add: sup_ty_strict_order2_RType) 
    apply (simp add: sup_less_eq_set) 
    done 

lemma sup_least_ty: 
    "τ ≤ ρ ⟹ σ ≤ ρ ⟹ τ ⊔ σ ≤ ρ" for τ σ ρ :: ty 
    apply (simp add: less_eq_ty_def) 
    apply (elim disjE) 
    using sup_ty_idem apply auto[1] 
    apply (simp add: sup_ty_strict_order) 
    apply (simp add: sup_ty_strict_order sup_commut_ty) 
    using less_eq_ty_def sup_ty_strict_order2 apply auto 
    done 

instance 
    apply (standard) 
    apply (simp add: less_le_not_le_ty) 
    apply simp 
    using order_trans_ty apply blast 
    apply (simp add: antisym_ty) 
    apply (simp add: sup_ge1_ty) 
    apply (simp add: sup_commut_ty sup_ge1_ty) 
    apply (simp add: sup_least_ty) 
    done 

end 

一切正常：

value "IType ⊔ RType" 
value "SType IType ⊔ SType RType" 
value "SType IType ⊔ SType (SType RType)" 
value "SType (SType IType) ⊔ SType (SType RType)" 

我嘗試定義類型的一個Sup功能：

interpretation ty_abel_semigroup: abel_semigroup "sup :: ty ⇒ ty ⇒ ty" .. 

interpretation ty_comm_monoid_set: comm_monoid_set "sup :: ty ⇒ ty ⇒ ty" VType 
    apply (standard) 
    using sup_commut_ty sup_ty.simps(1) by auto 

instantiation ty :: Sup 
begin 
definition Sup_ty where "Sup_ty ≡ ty_comm_monoid_set.F id" 
instance .. 
end 

問題EM是下面的表達式無法計算：

value "Sup {IType, RType}" 

我覺得這是一個事實，即ty數據類型是無限的，所以一組ty是無限的太引起的。

我試圖描述UNIV :: ty set如下，並證明它的有限性：

lemma UNIV_ty: "UNIV = {VType, AType, IType, RType} ∪ (SType ` UNIV)" 
    apply (auto intro: ty.induct) 
    by (metis range_eqI ty.exhaust) 

instance ty :: finite 
    apply (standard) 

但我卡住了。我不確定它是否有限。有限列表也被定義爲歸納數據類型。所有的歸納數據類型都是有限的嗎？

UPDATE：

我證明了ty是可數。但我不知道它是否能夠幫助確定Sup爲ty ...

fun ty_to_nat :: "ty ⇒ nat" where 
    "ty_to_nat VType = 0" 
| "ty_to_nat AType = 1" 
| "ty_to_nat IType = 2" 
| "ty_to_nat RType = 3" 
| "ty_to_nat (SType t) = 4 + ty_to_nat t" 

lemma ty_to_nat_inj_AType: "ty_to_nat AType = ty_to_nat y ⟹ AType = y" 
    by (induct y; simp) 
lemma ty_to_nat_inj_VType: "ty_to_nat VType = ty_to_nat y ⟹ VType = y" 
    by (induct y; simp) 
lemma ty_to_nat_inj_IType: "ty_to_nat IType = ty_to_nat y ⟹ IType = y" 
    by (induct y; simp) 
lemma ty_to_nat_inj_RType: "ty_to_nat RType = ty_to_nat y ⟹ RType = y" 
    by (induct y; simp) 
lemma ty_to_nat_inj_SType: 
    "(⋀y. ty_to_nat x = ty_to_nat y ⟹ x = y) ⟹ 
    ty_to_nat (SType x) = ty_to_nat y ⟹ SType x = y" 
    by (induct y; simp) 

lemma ty_to_nat_inj: 
    "ty_to_nat x = ty_to_nat y ⟹ x = y" 
    apply (induct x arbitrary: y) 
    using ty_to_nat_inj_AType apply auto[1] 
    using ty_to_nat_inj_VType apply auto[1] 
    using ty_to_nat_inj_IType apply auto[1] 
    using ty_to_nat_inj_RType apply auto[1] 
    using ty_to_nat_inj_SType apply auto[1] 
    done 

instance ty :: countable 
    apply (standard) 
    apply (rule exI[of _ "ty_to_nat"]) 
    apply (simp add: injI ty_to_nat_inj) 
    done 

Answer 1

這是不可能計算的無限集合是最高的，除非你知道一些關於無窮集合的結構應用到Sup運營商。所以沒有通用的解決方案。

您當然可以使用針對您的訂單定義進行定製的不可執行成員資格測試進行檢查。您可能需要查看Jinja和JinjaThreads（可在法新社獲得）的DFA理論，其中爲類似Java的類層次結構定義並計算了最小上界。

若要執行，如果您只對有限集合上的上限感興趣，則可以派生出一個特殊的代碼方程式，它在set代碼構造函數上與模式匹配。例如，您可以在理論List中證明類似於Sup_set_fold的代碼方程。這個特定的定理也需要至少一個元素，並且我還沒有研究過你的例子來看看是否有這樣的情況。