Theory Compute_Nonempty_Infinite_Sorts
section ‹Computing Nonempty and Infinite sorts›
text ‹This theory provides two algorithms, which both take a description of a set of sorts with
their constructors. The first algorithm computes the set of sorts that are nonempty, i.e., those
sorts that are inhabited by ground terms;
and the second algorithm computes the set of sorts that are infinite,
i.e., where one can build arbitrary large ground terms.›
theory Compute_Nonempty_Infinite_Sorts
imports
Sorted_Terms.Sorted_Terms
LP_Duality.Minimum_Maximum
Matrix.Utility
begin
subsection ‹Deciding the nonemptyness of all sorts under consideration›
function compute_nonempty_main :: "'τ set ⇒ (('f × 'τ list) × 'τ) list ⇒ 'τ set" where
"compute_nonempty_main ne ls = (let rem_ls = filter (λ f. snd f ∉ ne) ls in
case partition (λ ((_,args),_). set args ⊆ ne) rem_ls of
(new, rem) ⇒ if new = [] then ne else compute_nonempty_main (ne ∪ set (map snd new)) rem)"
by pat_completeness auto
termination
proof (relation "measure (length o snd)", goal_cases)
case (2 ne ls rem_ls new rem)
have "length new + length rem = length rem_ls"
using 2(2) sum_length_filter_compl[of _ rem_ls] by (auto simp: o_def)
with 2(3) have "length rem < length rem_ls" by (cases new, auto)
also have "… ≤ length ls" using 2(1) by auto
finally show ?case by simp
qed simp
declare compute_nonempty_main.simps[simp del]
definition compute_nonempty_sorts :: "(('f × 'τ list) × 'τ) list ⇒ 'τ set" where
"compute_nonempty_sorts Cs = compute_nonempty_main {} Cs"
lemma compute_nonempty_sorts:
assumes "distinct (map fst Cs)"
and "map_of Cs = C"
shows "compute_nonempty_sorts Cs = {τ. ∃ t :: ('f,'v)term. t : τ in 𝒯(C,∅)}" (is "_ = ?NE")
proof -
let ?TC = "𝒯(C,(∅ :: 'v ⇒ _))"
have "ne ⊆ ?NE ⟹ set ls ⊆ set Cs ⟹ snd ` (set Cs - set ls) ⊆ ne ⟹
compute_nonempty_main ne ls = ?NE" for ne ls
proof (induct ne ls rule: compute_nonempty_main.induct)
case (1 ne ls)
note ne = 1(2)
define rem_ls where "rem_ls = filter (λ f. snd f ∉ ne) ls"
have rem_ls: "set rem_ls ⊆ set Cs"
"snd ` (set Cs - set rem_ls) ⊆ ne"
using 1(2-) by (auto simp: rem_ls_def)
obtain new rem where part: "partition (λ((f, args), target). set args ⊆ ne) rem_ls = (new,rem)" by force
have [simp]: "compute_nonempty_main ne ls = (if new = [] then ne else compute_nonempty_main (ne ∪ set (map snd new)) rem)"
unfolding compute_nonempty_main.simps[of ne ls] Let_def rem_ls_def[symmetric] part by auto
have new: "set (map snd new) ⊆ ?NE"
proof
fix τ
assume "τ ∈ set (map snd new)"
then obtain f args where "((f,args),τ) ∈ set rem_ls" and args: "set args ⊆ ne" using part by auto
with rem_ls have "((f,args),τ) ∈ set Cs" by auto
with assms have "C (f,args) = Some τ" by auto
hence fC: "f : args → τ in C" by (simp add: hastype_in_ssig_def)
from args ne have "∀ tau. ∃ t. tau ∈ set args ⟶ t : tau in ?TC" by auto
from choice[OF this] obtain ts where "⋀ tau. tau ∈ set args ⟹ ts tau : tau in ?TC" by auto
hence "Fun f (map ts args) : τ in ?TC"
apply (intro Fun_hastypeI[OF fC])
by (simp add: list_all2_conv_all_nth)
thus "τ ∈ ?NE" by auto
qed
show ?case
proof (cases "new = []")
case False
note IH = 1(1)[OF rem_ls_def part[symmetric] False]
have "compute_nonempty_main ne ls = compute_nonempty_main (ne ∪ set (map snd new)) rem" using False by simp
also have "… = ?NE"
proof (rule IH)
show "ne ∪ set (map snd new) ⊆ ?NE" using new ne by auto
show "set rem ⊆ set Cs" using rem_ls part by auto
show "snd ` (set Cs - set rem) ⊆ ne ∪ set (map snd new)"
proof
fix τ
assume "τ ∈ snd ` (set Cs - set rem)"
then obtain f args where in_ls: "((f,args),τ) ∈ set Cs" and nrem: "((f,args),τ) ∉ set rem" by force
thus "τ ∈ ne ∪ set (map snd new)" using new part rem_ls by force
qed
qed
finally show ?thesis .
next
case True
have "compute_nonempty_main ne ls = ne" using True by simp
also have "… = ?NE"
proof (rule ccontr)
assume "¬ ?thesis"
with ne obtain τ t where counter: "t : τ in ?TC" "τ ∉ ne" by auto
thus False
proof (induct t τ)
case (Fun f ts τs τ)
from Fun(1) have "C (f,τs) = Some τ" by (simp add: hastype_in_ssig_def)
with assms(2) have mem: "((f,τs),τ) ∈ set Cs" by (meson map_of_SomeD)
from Fun(3) have τs: "set τs ⊆ ne" by (induct, auto)
from rem_ls mem Fun(4) have "((f,τs),τ) ∈ set rem_ls" by auto
with τs have "((f,τs),τ) ∈ set new" using part by auto
with True show ?case by auto
qed auto
qed
finally show ?thesis .
qed
qed
from this[of "{}" Cs] show ?thesis unfolding compute_nonempty_sorts_def by auto
qed
definition decide_nonempty_sorts :: "'t list ⇒ (('f × 't list) × 't)list ⇒ 't option" where
"decide_nonempty_sorts τs Cs = (let ne = compute_nonempty_sorts Cs in
find (λ τ. τ ∉ ne) τs)"
lemma decide_nonempty_sorts:
assumes "distinct (map fst Cs)"
and "map_of Cs = C"
shows "decide_nonempty_sorts τs Cs = None ⟹ ∀ τ ∈ set τs. ∃ t :: ('f,'v)term. t : τ in 𝒯(C,∅)"
"decide_nonempty_sorts τs Cs = Some τ ⟹ τ ∈ set τs ∧ ¬ (∃ t :: ('f,'v)term. t : τ in 𝒯(C,∅))"
unfolding decide_nonempty_sorts_def Let_def compute_nonempty_sorts[OF assms, where ?'v = 'v]
find_None_iff find_Some_iff by auto
subsection ‹Deciding infiniteness of a sort›
text ‹We provide an algorithm, that given a list of sorts with constructors, computes the
set of those sorts that are infinite. Here a sort is defined as infinite iff
there is no upper bound on the size of the ground terms of that sort.›
function compute_inf_main :: "'τ set ⇒ ('τ × ('f × 'τ list)list) list ⇒ 'τ set" where
"compute_inf_main m_inf ls = (
let (fin, ls') =
partition (λ (τ,fs). ∀ τs ∈ set (map snd fs). ∀ τ ∈ set τs. τ ∉ m_inf) ls
in if fin = [] then m_inf else compute_inf_main (m_inf - set (map fst fin)) ls')"
by pat_completeness auto
termination
proof (relation "measure (length o snd)", goal_cases)
case (2 m_inf ls pair fin ls')
have "length fin + length ls' = length ls"
using 2 sum_length_filter_compl[of _ ls] by (auto simp: o_def)
with 2(3) have "length ls' < length ls" by (cases fin, auto)
thus ?case by auto
qed simp
lemma compute_inf_main: fixes E :: "'v ⇀ 't" and C :: "('f,'t)ssig"
assumes E: "E = ∅"
and C_Cs: "C = map_of Cs'"
and Cs': "set Cs' = set (concat (map ((λ (τ, fs). map (λ f. (f,τ)) fs)) Cs))"
and arg_types_inhabitet: "∀ f τs τ τ'. f : τs → τ in C ⟶ τ' ∈ set τs ⟶ (∃ t. t : τ' in 𝒯(C,E))"
and dist: "distinct (map fst Cs)" "distinct (map fst Cs')"
and inhabitet: "∀ τ fs. (τ,fs) ∈ set Cs ⟶ set fs ≠ {}"
and "∀ τ. τ ∉ m_inf ⟶ bdd_above (size ` {t. t : τ in 𝒯(C,E)})"
and "set ls ⊆ set Cs"
and "fst ` (set Cs - set ls) ∩ m_inf = {}"
and "m_inf ⊆ fst ` set ls"
shows "compute_inf_main m_inf ls = {τ. ¬ bdd_above (size ` {t. t : τ in 𝒯(C,E)})}"
using assms(8-)
proof (induct m_inf ls rule: compute_inf_main.induct)
case (1 m_inf ls)
let ?fin = "λ τ. bdd_above (size ` {t. t : τ in 𝒯(C,E)})"
define crit where "crit = (λ (τ :: 't,fs :: ('f × 't list) list). ∀ τs ∈ set (map snd fs). ∀ τ ∈ set τs. τ ∉ m_inf)"
define S where "S τ' = size ` {t. t : τ' in 𝒯(C,E)}" for τ'
define M where "M τ' = Maximum (S τ')" for τ'
define M' where "M' σs = sum_list (map M σs) + (1 + length σs)" for σs
define L where "L = [ σs . (τ,cs) <- Cs, (f,σs) <- cs]"
define N where "N = max_list (map M' L)"
obtain fin ls' where part: "partition crit ls = (fin, ls')" by force
{
fix τ cs
assume inCs: "(τ,cs) ∈ set Cs"
have nonempty:"∃ t. t : τ in 𝒯(C,E)"
proof -
from inhabitet[rule_format, OF inCs] obtain f σs where "(f,σs) ∈ set cs" by (cases cs,auto )
with inCs have "((f,σs),τ) ∈ set Cs'" unfolding Cs' by auto
hence fC: "f : σs → τ in C" using dist(2) unfolding C_Cs
by (meson hastype_in_ssig_def map_of_is_SomeI)
hence "∀σ. ∃ t. σ ∈ set σs ⟶ t : σ in 𝒯(C,E)" using arg_types_inhabitet[rule_format, of f σs τ] by auto
from choice[OF this] obtain t where "σ ∈ set σs ⟹ t σ : σ in 𝒯(C,E)" for σ by auto
hence "Fun f (map t σs) : τ in 𝒯(C,E)" using list_all2_conv_all_nth
apply (intro Fun_hastypeI[OF fC]) by (simp add: list_all2_conv_all_nth)
then show ?thesis by auto
qed
} note inhabited = this
{
fix τ
assume asm: "τ ∈ fst ` set fin"
hence "?fin τ"
proof(cases "τ ∈ m_inf")
case True
then obtain fs where taufs:"(τ, fs) ∈ set fin" using asm by auto
{
fix τ' and t and args
assume *: "τ' ∈ set args" "args ∈ snd ` set fs" "t : τ' in 𝒯(C,E)"
from * have "τ' ∉ m_inf" using taufs unfolding compute_inf_main.simps[of m_inf]
using crit_def part by fastforce
hence "?fin τ'" using crit_def part 1(2) by auto
hence hM: "bdd_above (S τ')" unfolding S_def .
from *(3) have "size t ∈ S τ'" unfolding S_def by auto
from this hM have "size t ≤ M τ'" unfolding M_def by (metis bdd_above_Maximum_nat)
} note arg_type_bounds = this
{
fix t
assume t: "t : τ in 𝒯(C,E)"
then obtain f ts where tF: "t = Fun f ts" unfolding E by (induct, auto)
from t[unfolded tF Fun_hastype]
obtain σs where f: "f : σs → τ in C" and args: "ts :⇩l σs in 𝒯(C,E)" by auto
from part[simplified] asm 1(3) obtain cs where inCs: "(τ,cs) ∈ set Cs" and crit: "crit (τ,cs)" by auto
{
from f[unfolded hastype_in_ssig_def C_Cs]
have "map_of Cs' (f, σs) = Some τ" by auto
hence "((f,σs), τ) ∈ set Cs'" by (metis map_of_SomeD)
from this[unfolded Cs', simplified] obtain cs' where 2: "(τ,cs') ∈ set Cs" and mem: "(f,σs) ∈ set cs'" by auto
from inCs 2 dist have "cs' = cs" by (metis eq_key_imp_eq_value)
with mem have mem: "(f,σs) ∈ set cs" by auto
} note mem = this
from mem inCs have inL: "σs ∈ set L" unfolding L_def by force
{
fix σ ti
assume "σ ∈ set σs" and ti: "ti : σ in 𝒯(C,E)"
with mem crit have "σ ∉ m_inf" unfolding crit_def by auto
hence "?fin σ" using 1(2) by auto
hence hM: "bdd_above (S σ)" unfolding S_def .
from ti have "size ti ∈ S σ" unfolding S_def by auto
from this hM have "size ti ≤ M σ" unfolding M_def by (metis bdd_above_Maximum_nat)
} note arg_bound = this
have len: "length σs = length ts" using args by (auto simp: list_all2_conv_all_nth)
have "size t = sum_list (map size ts) + (1 + length ts)" unfolding tF by (simp add: size_list_conv_sum_list)
also have "… ≤ sum_list (map M σs) + (1 + length ts)" unfolding tF args
proof -
have id1: "map size ts = map (λ i. size (ts ! i)) [0 ..< length ts]" by (intro nth_equalityI, auto)
have id2: "map M σs = map (λ i. M (σs ! i)) [0 ..< length ts]" using len by (intro nth_equalityI, auto)
have "sum_list (map size ts) ≤ sum_list (map M σs)" unfolding id1 id2
apply (rule sum_list_mono) using arg_bound args
by (auto, simp add: list_all2_conv_all_nth)
thus ?thesis by auto
qed
also have "… = sum_list (map M σs) + (1 + length σs)" using args unfolding M_def using list_all2_lengthD by auto
also have "… = M' σs" unfolding M'_def by auto
also have "… ≤ max_list (map M' L)"
by (rule max_list, insert inL, auto)
also have "… = N" unfolding N_def ..
finally have "size t ≤ N" .
}
hence "⋀ s. s ∈ S τ ⟹ s ≤ N" unfolding S_def by auto
hence "finite (S τ)"
using finite_nat_set_iff_bounded_le by auto
moreover
have nonempty:"∃ t. t : τ in 𝒯(C,E)"
proof -
from part[simplified] asm 1(3) obtain cs where inCs: "(τ,cs) ∈ set Cs" by auto
thus ?thesis using inhabited by auto
qed
hence "S τ ≠ {}" unfolding S_def by auto
ultimately show ?thesis unfolding S_def[symmetric] by (metis Max_ge bdd_above_def)
next
case False
then show ?thesis using 1(2) by simp
qed
} note fin = this
show ?case
proof (cases "fin = []")
case False
hence "compute_inf_main m_inf ls = compute_inf_main (m_inf - set (map fst fin)) ls'"
unfolding compute_inf_main.simps[of m_inf] part[unfolded crit_def] by auto
also have "… = {τ. ¬ ?fin τ}"
proof (rule 1(1)[OF refl part[unfolded crit_def, symmetric] False])
show "set ls' ⊆ set Cs" using 1(3) part by auto
show "fst ` (set Cs - set ls') ∩ (m_inf - set (map fst fin)) = {}" using 1(3-4) part by force
show "∀τ. τ ∉ m_inf - set (map fst fin) ⟶ ?fin τ" using 1(2) fin by force
show "m_inf - set (map fst fin) ⊆ fst ` set ls'" using 1(5) part by force
qed
finally show ?thesis .
next
case True
hence "compute_inf_main m_inf ls = m_inf"
unfolding compute_inf_main.simps[of m_inf] part[unfolded crit_def] by auto
also have "… = {τ. ¬ ?fin τ}"
proof
show "{τ. ¬ ?fin τ} ⊆ m_inf" using fin 1(2) by auto
{
fix τ
assume "τ ∈ m_inf"
with 1(5) obtain cs where mem: "(τ,cs) ∈ set ls" by auto
from part True have ls': "ls' = ls" by (induct ls arbitrary: ls', auto)
from partition_P[OF part, unfolded ls']
have "⋀ e. e ∈ set ls ⟹ ¬ crit e" by auto
from this[OF mem, unfolded crit_def split]
obtain c τs τ' where *: "(c,τs) ∈ set cs" "τ' ∈ set τs" "τ' ∈ m_inf" by auto
from mem 1(2-) have "(τ,cs) ∈ set Cs" by auto
with * have "((c,τs),τ) ∈ set Cs'" unfolding Cs' by force
with dist(2) have "map_of Cs' ((c,τs)) = Some τ" by simp
from this[folded C_Cs] have c: "c : τs → τ in C" unfolding hastype_in_ssig_def .
from arg_types_inhabitet this have "∀ σ. ∃ t. σ ∈ set τs ⟶ t : σ in 𝒯(C,E)" by auto
from choice[OF this] obtain t where "⋀ σ. σ ∈ set τs ⟹ t σ : σ in 𝒯(C,E)" by auto
hence list: "map t τs :⇩l τs in 𝒯(C,E)" by (simp add: list_all2_conv_all_nth)
with c have "Fun c (map t τs) : τ in 𝒯(C,E)" by (intro Fun_hastypeI)
with * c list have "∃ c τs τ' ts. Fun c ts : τ in 𝒯(C,E) ∧ ts :⇩l τs in 𝒯(C,E) ∧ c : τs → τ in C ∧ τ' ∈ set τs ∧ τ' ∈ m_inf"
by blast
} note m_invD = this
{
fix n :: nat
have "τ ∈ m_inf ⟹ ∃ t. t : τ in 𝒯(C,E) ∧ size t ≥ n" for τ
proof (induct n arbitrary: τ)
case (0 τ)
from m_invD[OF 0] show ?case by blast
next
case (Suc n τ)
from m_invD[OF Suc(2)] obtain c τs τ' ts
where *: "ts :⇩l τs in 𝒯(C,E)" "c : τs → τ in C" "τ' ∈ set τs" "τ' ∈ m_inf"
by auto
from *(1)[unfolded list_all2_conv_all_nth] *(3)[unfolded set_conv_nth]
obtain i where i: "i < length τs" and tsi:"ts ! i : τ' in 𝒯(C,E)" and len: "length ts = length τs" by auto
from Suc(1)[OF *(4)] obtain t where t:"t : τ' in 𝒯(C,E)" and ns:"n ≤ size t" by auto
define ts' where "ts' = ts[i := t]"
have "ts' :⇩l τs in 𝒯(C,E)" using list_all2_conv_all_nth unfolding ts'_def
by (metis "*"(1) tsi has_same_type i list_all2_update_cong list_update_same_conv t(1))
hence **:"Fun c ts' : τ in 𝒯(C,E)" apply (intro Fun_hastypeI[OF *(2)]) by fastforce
have "t ∈ set ts'" unfolding ts'_def using t
by (simp add: i len set_update_memI)
hence "size (Fun c ts') ≥ Suc n" using *
by (simp add: size_list_estimation' ns)
thus ?case using ** by blast
qed
} note main = this
show "m_inf ⊆ {τ. ¬ ?fin τ}"
proof (standard, standard)
fix τ
assume asm: "τ ∈ m_inf"
have "∃t. t : τ in 𝒯(C,E) ∧ n < size t" for n using main[OF asm, of "Suc n"] by auto
thus "¬ ?fin τ"
by (metis bdd_above_Maximum_nat imageI mem_Collect_eq order.strict_iff)
qed
qed
finally show ?thesis .
qed
qed
definition compute_inf_sorts :: "(('f × 't list) × 't)list ⇒ 't set" where
"compute_inf_sorts Cs = (let
Cs' = map (λ τ. (τ, map fst (filter(λf. snd f = τ) Cs))) (remdups (map snd Cs))
in compute_inf_main (set (map fst Cs')) Cs')"
lemma compute_inf_sorts:
fixes E :: "'v ⇀ 't" and C :: "('f,'t)ssig"
assumes E: "E = ∅"
and C_Cs: "C = map_of Cs"
and arg_types_inhabitet: "∀ f τs τ τ'. f : τs → τ in C ⟶ τ' ∈ set τs ⟶ (∃ t. t : τ' in 𝒯(C,E))"
and dist: "distinct (map fst Cs)"
shows "compute_inf_sorts Cs = {τ. ¬ bdd_above (size ` {t. t : τ in 𝒯(C,E)})}"
proof -
define taus where "taus = remdups (map snd Cs)"
define Cs' where "Cs' = map (λ τ. (τ, map fst (filter(λf. snd f = τ) Cs))) taus"
have "compute_inf_sorts Cs = compute_inf_main (set (map fst Cs')) Cs'"
unfolding compute_inf_sorts_def taus_def Cs'_def Let_def by auto
also have "… = {τ. ¬ bdd_above (size ` {t. t : τ in 𝒯(C,E)})}"
proof (rule compute_inf_main[OF E C_Cs _ arg_types_inhabitet _ dist _ _ subset_refl])
have "distinct taus" unfolding taus_def by auto
thus "distinct (map fst Cs')" unfolding Cs'_def map_map o_def fst_conv by auto
show "set Cs = set (concat (map (λ(τ, fs). map (λf. (f, τ)) fs) Cs'))"
unfolding Cs'_def taus_def by force
show "∀τ fs. (τ, fs) ∈ set Cs' ⟶ set fs ≠ {}"
unfolding Cs'_def taus_def by (force simp: filter_empty_conv)
show "fst ` (set Cs' - set Cs') ∩ set (map fst Cs') = {}" by auto
show "set (map fst Cs') ⊆ fst ` set Cs'" by auto
show "∀τ. τ ∉ set (map fst Cs') ⟶ bdd_above (size ` {t. t : τ in 𝒯(C,E)})"
proof (intro allI impI)
fix τ
assume "τ ∉ set (map fst Cs')"
hence "τ ∉ snd ` set Cs" unfolding Cs'_def taus_def by auto
hence diff: "C f ≠ Some τ" for f unfolding C_Cs
by (metis Some_eq_map_of_iff dist imageI snd_conv)
{
fix t
assume "t : τ in 𝒯(C,E)"
hence False using diff unfolding E
proof induct
case (Fun f ss σs τ)
from Fun(1,4) show False unfolding hastype_in_ssig_def by auto
qed auto
}
hence id: "{t. t : τ in 𝒯(C,E)} = {}" by auto
show "bdd_above (size ` {t. t : τ in 𝒯(C,E)})" unfolding id by auto
qed
qed
finally show ?thesis .
qed
end