Comment définir Sup pour un type de données inductif?

Question

Voici un système de types simple avec les types suivants: any, void, integer, real, set.

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

Types forment un demi-treillis avec supremum:

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 

Tout fonctionne comme prévu:

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

J'essaie de définir une fonction Sup pour les types:

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 

Le problème em est que l'expression suivante ne peut pas être évaluée:

value "Sup {IType, RType}" 

Je pense que cela est causé par le fait que ty type de données est infinie et donc un ensemble de ty est trop infini.

J'ai essayé de décrire UNIV :: ty set comme suit et prouver qu'il est finitude:

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) 

Mais je suis coincé. Je ne suis pas sûr que ce soit fini ou non. Les listes finies sont définies comme des types de données inductifs. Tous les types de données inductifs sont-ils finis?

MISE À JOUR:

Je prouvé que ty est dénombrable. Mais je ne sais pas si elle peut aider à définir Sup pour 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

Il est impossible de calculer suprema des ensembles infinis, sauf si vous savez quelque chose sur la structure de l'ensemble infini auquel vous appliquer la Sup opérateur. Il n'y a donc pas de solution universelle.

Vous pouvez bien sûr vérifier en utilisant des tests d'adhésion non-exécutables qui sont adaptés à la définition de votre commande. Vous pouvez regarder les théories DFA de Jinja et JinjaThreads (disponibles dans l'AFP) où les limites supérieures sont définies et calculées pour une hiérarchie de classes de type Java. Pour l'exécution, si vous êtes seulement intéressé par suprema sur les ensembles finis, vous pouvez dériver un equaiton de code spécial qui correspond au pattern sur le constructeur de code set. Par exemple, vous pouvez prouver une équation de code similaire à Sup_set_fold en théorie List. Ce théorème particulier exige aussi un élément mineur, et je n'ai pas assez étudié votre exemple pour voir où il y en a.