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
FinFun.FinFun
begin
lemma finite_set_Cons:
assumes A: "finite A" and B: "finite B"
shows "finite (set_Cons A B)"
proof -
have "set_Cons A B = case_prod (#) ` (A × B)" by (auto simp: set_Cons_def)
then show ?thesis
by (simp add: finite_imageI[OF finite_cartesian_product[OF A B],of "case_prod (#)"])
qed
lemma finite_listset:
assumes "∀A ∈ set As. finite A"
shows "finite (listset As)"
using assms
by (induct As) (auto simp: finite_set_Cons)
lemma listset_conv_nth:
"xs ∈ listset As = (length xs = length As ∧ (∀i < length As. xs ! i ∈ As ! i))"
proof (induct As arbitrary: xs)
case (Cons A As xs) then show ?case
by (cases xs) (auto simp: set_Cons_def nth_Cons nat.splits)
qed auto
lemma card_listset: assumes "⋀ A. A ∈ set As ⟹ finite A"
shows "card (listset As) = prod_list (map card As)"
using assms
proof (induct As)
case (Cons A As)
have sC: "set_Cons A B = case_prod (#) ` (A × B)" for B by (auto simp: set_Cons_def)
have IH: "prod_list (map card As) = card (listset As)" using Cons by auto
have "card A * card (listset As) = card (A × listset As)"
by (simp add: card_cartesian_product)
also have "… = card ((λ (a,as). Cons a as) ` (A × listset As))"
by (subst card_image, auto simp: inj_on_def)
finally
show ?case by (simp add: sC IH)
qed auto
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)"
shows "compute_nonempty_sorts Cs = {τ. ¬ empty_sort (map_of Cs) τ}" (is "_ = ?NE")
proof -
let ?TC = "𝒯(map_of Cs)"
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 "map_of Cs (f,args) = Some τ" by auto
hence fC: "f : args → τ in map_of Cs" by (simp add: fun_hastype_def)
from args ne empty_sortI have "∀ tau. ∃ t. tau ∈ set args ⟶ t : tau in ?TC" by force
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 empty_sortI obtain τ t where counter: "t : τ in ?TC" "τ ∉ ne" by force
thus False
proof (induct t τ)
case (Fun f ts τs τ)
from Fun(1) have "map_of Cs (f,τs) = Some τ" by (simp add: fun_hastype_def)
then 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)"
shows "decide_nonempty_sorts τs Cs = None ⟹ ∀ τ ∈ set τs. ¬ empty_sort (map_of Cs) τ"
"decide_nonempty_sorts τs Cs = Some τ ⟹ τ ∈ set τs ∧ empty_sort (map_of Cs) τ"
unfolding decide_nonempty_sorts_def Let_def compute_nonempty_sorts[OF assms]
find_None_iff find_Some_iff by auto
subsection ‹Deciding infiniteness of a sort and computing cardinalities›
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.
Moreover, we also compute for each sort the cardinality of the set of constructor ground
terms of that sort.›
context
includes finfun_syntax
begin
fun finfun_update_all :: "'a list ⇒ ('a ⇒ 'b) ⇒ ('a ⇒f 'b) ⇒ ('a ⇒f 'b)" where
"finfun_update_all [] g f = f"
| "finfun_update_all (x # xs) g f = (finfun_update_all xs g f)(x $:= g x)"
lemma finfun_update_all[simp]: "finfun_update_all xs g f $ x = (if x ∈ set xs then g x else f $ x)"
proof (induct xs)
case (Cons y xs)
thus ?case by (cases "x = y", auto)
qed auto
definition compute_card_of_sort :: "'τ ⇒ ('f × 'τ list)list ⇒ ('τ ⇒f nat) ⇒ nat" where
"compute_card_of_sort τ cs cards = (∑fσs←remdups cs. prod_list (map (($) cards) (snd fσs)))"
function compute_inf_card_main :: "'τ set ⇒ ('τ ⇒f nat) ⇒ ('τ × ('f × 'τ list)list) list ⇒ 'τ set × ('τ ⇒ nat)" where
"compute_inf_card_main m_inf cards ls = (
let (fin, ls') =
partition (λ (τ,fs). ∀ τs ∈ set (map snd fs). ∀ τ ∈ set τs. τ ∉ m_inf) ls
in if fin = [] then (m_inf, λ τ. cards $ τ) else
let new = map fst fin;
cards' = finfun_update_all new (λ τ. compute_card_of_sort τ (the (map_of ls τ)) cards) cards in
compute_inf_card_main (m_inf - set new) cards' ls')"
by pat_completeness auto
termination
proof (relation "measure (length o snd o snd)", goal_cases)
case (2 m_inf cards 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_card_main: fixes C :: "('f,'t)ssig"
assumes C_Cs: "C = map_of Cs'"
and Cs': "set Cs' = set (concat (map ((λ (τ, fs). map (λ f. (f,τ)) fs)) Cs))"
and arg_types_nonempty: "∀ f τs τ τ'. f : τs → τ in C ⟶ τ' ∈ set τs ⟶ ¬ empty_sort C τ'"
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)})"
and "set ls ⊆ set Cs"
and "fst ` (set Cs - set ls) ∩ m_inf = {}"
and "m_inf ⊆ fst ` set ls"
and "∀ τ. τ ∉ m_inf ⟶ cards $ τ = card_of_sort C τ ∧ finite_sort C τ"
and "∀ τ. τ ∈ m_inf ⟶ cards $ τ = 0"
shows "compute_inf_card_main m_inf cards ls = ({τ. ¬ bdd_above (size ` {t. t : τ in 𝒯(C)})},
λ τ. card_of_sort C τ)"
using assms(7-)
proof (induct m_inf cards ls rule: compute_inf_card_main.induct)
case (1 m_inf cards ls)
let ?terms = "λ τ. {t. t : τ in 𝒯(C)}"
let ?fin = "λ τ. bdd_above (size ` ?terms τ)"
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)}" 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)"
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 fun_hastype_def map_of_is_SomeI)
hence "∀σ. ∃ t. σ ∈ set σs ⟶ t : σ in 𝒯(C)"
by (auto dest!: arg_types_nonempty[rule_format] elim!: not_empty_sortE)
from choice[OF this] obtain t where "σ ∈ set σs ⟹ t σ : σ in 𝒯(C)" for σ by auto
hence "Fun f (map t σs) : τ in 𝒯(C)" 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
define cards' where "cards' = finfun_update_all (map fst fin) (λ τ. compute_card_of_sort τ (the (map_of ls τ)) cards) cards"
{
fix τ
assume asm: "τ ∈ fst ` set fin"
let ?TT = "?terms τ"
from asm obtain cs where tau_cs_fin: "(τ,cs) ∈ set fin" by auto
hence tau_ls: "(τ,cs) ∈ set ls" using part by auto
with dist(1) ‹set ls ⊆ set Cs›
have map: "map_of Cs τ = Some cs" "map_of ls τ = Some cs"
by (metis (no_types, opaque_lifting) eq_key_imp_eq_value map_of_SomeD subsetD weak_map_of_SomeI)+
from asm have cards': "cards' $ τ = compute_card_of_sort τ cs cards" unfolding cards'_def by (auto simp: map)
from part asm have tau_fin: "τ ∈ set (map fst fin)" by auto
{
fix f σs
have "f : σs → τ in C ⟷ ((f,σs),τ) ∈ set Cs'"
proof
assume "f : σs → τ in C"
hence "map_of Cs' (f,σs) = Some τ" unfolding C_Cs by (rule fun_hastypeD)
thus "((f,σs),τ) ∈ set Cs'" by (rule map_of_SomeD)
next
assume "((f, σs), τ) ∈ set Cs'"
hence "map_of Cs' (f, σs) = Some τ" using dist(2) by simp
thus "f : σs → τ in C" unfolding C_Cs by (rule fun_hastypeI)
qed
also have "… ⟷ (∃ cs. (τ, cs) ∈ set Cs ∧ (f,σs) ∈ set cs)"
unfolding Cs' by auto
also have "… ⟷ (∃ cs. map_of Cs τ = Some cs ∧ (f,σs) ∈ set cs)"
using dist(1) by simp
also have "… ⟷ (f,σs) ∈ set cs" unfolding map by auto
finally have "(f : σs → τ in C) = ((f, σs) ∈ set cs)" by auto
} note C_to_cs = this
define T where "T σ = ?terms σ" for σ
have to_ls: "{ts. ts :⇩l σs in 𝒯(C)} = listset (map T σs)" for σs
by (intro set_eqI, unfold listset_conv_nth, auto simp: T_def list_all2_conv_all_nth)
{
fix f σs σ
assume in_cs: "(f, σs) ∈ set cs" "σ ∈ set σs"
from tau_cs_fin part have "crit (τ,cs)" by auto
from this[unfolded crit_def split] in_cs have "σ ∉ m_inf" by auto
with 1(6) have "cards $ σ = card (T σ)" and "finite (T σ)"
by (auto simp: T_def card_of_sort finite_sort)
} note σs_infos = this
have "?TT = { Fun f ts | f ts σs. f : σs → τ in C ∧ ts :⇩l σs in 𝒯(C)}" (is "_ = ?FunApps")
proof (intro set_eqI)
fix t
{
assume "t : τ in 𝒯(C)"
hence "t ∈ ?FunApps" by (induct, auto)
}
moreover
{
assume "t ∈ ?FunApps"
hence "t : τ in 𝒯(C)" by (auto intro: Fun_hastypeI)
}
ultimately show "t ∈ ?TT ⟷ t ∈ ?FunApps" by auto
qed
also have "… = { Fun f ts | f ts σs. (f, σs) ∈ set cs ∧ ts :⇩l σs in 𝒯(C)}" unfolding C_to_cs ..
also have "… = (λ (f, ts). Fun f ts) ` (⋃ (f, σs) ∈ set cs. Pair f ` { ts. ts :⇩l σs in 𝒯(C)})" (is "_ = ?f ` ?A") by auto
finally have TTfA: "?TT = ?f ` ?A" .
have finPair: "finite (Pair f ` A) = finite A" for f :: 'f and A :: "('f, 'v) Term.term list set"
by (intro finite_image_iff inj_onI, auto)
have inj: "inj ?f" by (intro injI, auto)
from inj have card: "card ?TT = card ?A"
unfolding TTfA by (meson UNIV_I card_image inj_on_def)
also have "… = (∑i∈set cs. card (case i of (f, σs) ⇒ Pair f ` listset (map T σs)))" unfolding to_ls
proof (rule card_UN_disjoint[OF finite_set ballI ballI[OF ballI[OF impI]]], goal_cases)
case *: (1 fσs)
obtain f σs where fσs: "fσs = (f,σs)" by force
thus ?case using * σs_infos(2) by (cases fσs, auto intro!: finite_imageI finite_listset)
next
case *: (2 fσs gτs)
obtain f σs where fσs: "fσs = (f,σs)" by force
obtain g τs where gτs: "gτs = (g,τs)" by force
show ?case
proof (cases "g = f")
case False
thus ?thesis unfolding fσs gτs split by auto
next
case True
note fτs = gτs[unfolded True]
show ?thesis
proof (rule ccontr)
assume "¬ ?thesis"
from this[unfolded fσs fτs split]
obtain ts where ts: "ts ∈ listset (map T σs)" "ts ∈ listset (map T τs)" by auto
hence len: "length σs = length ts" "length τs = length ts" unfolding listset_conv_nth by auto
from *(3)[unfolded fσs fτs] have "σs ≠ τs" by auto
with len obtain i where i: "i < length ts" and diff: "σs ! i ≠ τs ! i"
by (metis nth_equalityI)
define ti where "ti = ts ! i"
define σi where "σi = σs ! i"
define τi where "τi = τs ! i"
note diff = diff[folded σi_def τi_def]
from ts i have "ti ∈ T σi" "ti ∈ T τi"
unfolding ti_def σi_def τi_def listset_conv_nth by auto
hence ti: "ti : σi in 𝒯(C)" "ti : τi in 𝒯(C)" unfolding T_def by auto
hence "σi = τi" by fastforce
with diff show False ..
qed
qed
qed
also have "… = (∑ fσs ∈set cs. card (listset (map T (snd fσs))))"
proof (rule sum.cong[OF refl], goal_cases)
case (1 fσs)
obtain f σs where id: "fσs = (f,σs)" by force
show ?case unfolding id split snd_conv
by (rule card_image, auto simp: inj_on_def)
qed
also have "… = (∑ fσs ∈set cs. prod_list (map card (map T (snd fσs))))"
by (rule sum.cong[OF refl], rule card_listset, insert σs_infos, auto)
also have "… = (∑ fσs ∈set cs. prod_list (map (($) cards) (snd fσs)))"
unfolding map_map o_def using σs_infos
by (intro sum.cong[OF refl] arg_cong[of _ _ prod_list], auto)
also have "… = sum_list (map (λ fσs. prod_list (map (($) cards) (snd fσs))) (remdups cs))"
by (rule sum.set_conv_list)
also have "… = cards' $ τ" unfolding cards' compute_card_of_sort_def ..
finally have cards': "card ?TT = cards' $ τ" by auto
from inj have "finite ?TT = finite ?A"
by (metis (no_types, lifting) TTfA finite_imageD finite_imageI subset_UNIV subset_inj_on)
also have "… = (∀ f σs. (f,σs) ∈ set cs ⟶ finite (Pair f ` {ts. ts :⇩l σs in 𝒯(C)}))"
by auto
finally have "finite ?TT = (∀ f σs. (f,σs) ∈ set cs ⟶ finite {ts. ts :⇩l σs in 𝒯(C)})"
unfolding finPair by auto
also have "… = True" unfolding to_ls using σs_infos(2) by (auto intro!: finite_listset)
finally have fin: "finite ?TT" by simp
from fin cards'
have "cards' $ τ = card (?terms τ)" "finite (?terms τ)" "?fin τ" by auto
} note fin = this
show ?case
proof (cases "fin = []")
case False
hence "compute_inf_card_main m_inf cards ls = compute_inf_card_main (m_inf - set (map fst fin)) cards' ls'"
unfolding compute_inf_card_main.simps[of m_inf] part[unfolded crit_def] cards'_def Let_def by auto
also have "… = ({τ. ¬ ?fin τ}, λ τ. card_of_sort C τ)"
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) ⊆ fst ` set ls'" using 1(5) part by force
show "∀τ. τ ∉ m_inf - set (map fst fin) ⟶ cards' $ τ = card_of_sort C τ ∧ finite_sort C τ"
proof (intro allI impI)
fix τ
assume nmem: "τ ∉ m_inf - set (map fst fin)"
show "cards' $ τ = card_of_sort C τ ∧ finite_sort C τ"
proof (cases "τ ∈ set (map fst fin)")
case False
with nmem have tau: "τ ∉ m_inf" by auto
with False 1(6)[rule_format, OF this] show ?thesis
unfolding cards'_def by auto
next
case True
with fin show ?thesis by (auto simp: card_of_sort finite_sort)
qed
qed
thus "∀τ. τ ∉ m_inf - set (map fst fin) ⟶ ?fin τ"
by (force simp: 1(2) intro: fin(3))
show "∀τ. τ ∈ m_inf - set (map fst fin) ⟶ cards' $ τ = 0" using 1(7) unfolding cards'_def
by auto
qed (auto simp: cards'_def)
finally show ?thesis .
next
case True
let ?cards = "λτ. cards $ τ"
have m_inf: "m_inf = {τ. ¬ ?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 fun_hastype_def .
have "∀ σ. ∃ t. σ ∈ set τs ⟶ t : σ in 𝒯(C)"
by (auto dest!: arg_types_nonempty[rule_format, OF c] elim!: not_empty_sortE)
from choice[OF this] obtain t where "⋀ σ. σ ∈ set τs ⟹ t σ : σ in 𝒯(C)" by auto
hence list: "map t τs :⇩l τs in 𝒯(C)" by (simp add: list_all2_conv_all_nth)
with c have "Fun c (map t τs) : τ in 𝒯(C)" by (intro Fun_hastypeI)
with * c list have "∃ c τs τ' ts. Fun c ts : τ in 𝒯(C) ∧ ts :⇩l τs in 𝒯(C) ∧ c : τs → τ in C ∧ τ' ∈ set τs ∧ τ' ∈ m_inf"
by blast
} note m_invD = this
{
fix n :: nat
have "τ ∈ m_inf ⟹ ∃ t. t : τ in 𝒯(C) ∧ 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)" "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)" and len: "length ts = length τs" by auto
from Suc(1)[OF *(4)] obtain t where t:"t : τ' in 𝒯(C)" and ns:"n ≤ size t" by auto
define ts' where "ts' = ts[i := t]"
have "ts' :⇩l τs in 𝒯(C)" 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)" 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) ∧ 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
from True have "compute_inf_card_main m_inf cards ls = (m_inf, ?cards)"
unfolding compute_inf_card_main.simps[of m_inf] part[unfolded crit_def] by auto
also have "?cards = (λ τ. card_of_sort C τ)"
proof (intro ext)
fix τ
show "cards $ τ = card_of_sort C τ"
proof (cases "τ ∈ m_inf")
case False
thus ?thesis using 1(6) by auto
next
case True
define TT where "TT = ?terms τ"
from True m_inf have "¬ bdd_above (size ` TT)" unfolding TT_def by auto
hence "infinite TT" by auto
hence "card TT = 0" by auto
thus ?thesis unfolding TT_def using True 1(7) by (auto simp: card_of_sort)
qed
qed
finally show ?thesis using m_inf by auto
qed
qed
definition compute_inf_card_sorts :: "(('f × 't list) × 't)list ⇒ 't set × ('t ⇒ nat)" where
"compute_inf_card_sorts Cs = (let
Cs' = map (λ τ. (τ, map fst (filter(λf. snd f = τ) Cs))) (remdups (map snd Cs))
in compute_inf_card_main (set (map fst Cs')) (K$ 0) Cs')"
lemma finite_imp_size_bdd_above: assumes "finite T"
shows "bdd_above (size ` T)"
proof -
from assms have "finite (size ` T)" by auto
thus ?thesis by simp
qed
lemma finite_sig_imp_finite_terms_of_bounded_size: assumes "finite (dom F)" and "finite (dom V)"
shows "finite {t. ∃ τ. size t ≤ n ∧ t : τ in 𝒯(F,V)}" (is "finite (?terms n)")
proof (induct n)
case (0)
have "t ∉ ?terms 0" for t by (cases t, auto)
hence id: "?terms 0 = {}" by auto
show ?case unfolding id by simp
next
case (Suc n)
let ?funsInter = "(λ (f, τs). (f, listset (map (λ _. (?terms n)) τs))) ` dom F"
define funsI where "funsI = ?funsInter"
let ?funs = "⋃ ((λ (f, tss). Fun f ` tss) ` funsI)"
{
fix t
assume "t ∈ ?terms (Suc n)"
then obtain τ where tτ: "t : τ in 𝒯(F,V)" and size: "size t ≤ Suc n" by auto
have "t ∈ Var ` dom V ∪ ?funs"
proof (cases t)
case (Var x)
thus ?thesis using tτ by auto
next
case t: (Fun f ts)
from tτ[unfolded t Fun_hastype] obtain τs where ts: "ts :⇩l τs in 𝒯(F,V)"
and f: "(f,τs) ∈ dom F" by auto
hence "(f, listset (map (λ _. (?terms n)) τs)) ∈ funsI" unfolding funsI_def by auto
moreover have "ts ∈ listset (map (λ _. (?terms n)) τs)"
unfolding listset_conv_nth length_map
proof (intro conjI allI impI)
show len: "length ts = length τs" using ts by (metis list_all2_lengthD)
fix i
assume i: "i < length τs"
with ts have i': "i < length ts" and type: "ts ! i : τs ! i in 𝒯(F,V)"
using list_all2_nthD2[OF ts] len by auto
from i' have "ts ! i ∈ set ts" by auto
from split_list[OF this] obtain bef aft where "ts = bef @ ts ! i # aft" by auto
from size[unfolded t] this have "size (Fun f (bef @ ts ! i # aft)) ≤ Suc n" by simp
hence "size (ts ! i) ≤ n" by simp
with type have "ts ! i ∈ ?terms n" by auto
with i show "ts ! i ∈ map (λ_. ?terms n) τs ! i" by auto
qed
ultimately show ?thesis unfolding t by blast
qed
}
hence "?terms (Suc n) ⊆ Var ` dom V ∪ ?funs" by blast
moreover have "finite (Var ` dom V ∪ ?funs)"
proof (intro finite_UnI finite_imageI assms finite_Union)
show "finite (funsI)" unfolding funsI_def
by (intro finite_imageI assms)
fix M
assume "M ∈ {Fun f ` tss |. (f, tss) ∈ funsI}"
from this obtain f tss where tss: "(f, tss) ∈ funsI" and M: "M = Fun f ` tss" by auto
from tss[unfolded funsI_def] obtain τs where
tss: "tss = listset (map (λ_. {t. size t ≤ n ∧ (∃τ. t : τ in 𝒯(F,V))}) τs)" and "τs ∈ snd ` dom F"
by force
have "finite tss" unfolding tss
by (intro finite_listset, insert Suc, auto)
thus "finite M" unfolding M
by (intro finite_imageI)
qed
ultimately show ?case by (rule finite_subset)
qed
lemma finite_sig_bdd_above_imp_finite: assumes "finite (dom F)" and "finite (dom V)"
and "bdd_above (size ` {t. t : τ in 𝒯(F,V)})"
shows "finite {t. t : τ in 𝒯(F,V)}"
proof -
from assms(3)[unfolded bdd_above_def] obtain n where
size: "∀s∈size ` {t. t : τ in 𝒯(F,V)}. s ≤ n " by auto
from finite_sig_imp_finite_terms_of_bounded_size[OF assms(1-2)]
have fin: "finite {t. ∃τ. size t ≤ n ∧ t : τ in 𝒯(F,V)}" by auto
have "finite {t. size t ≤ n ∧ t : τ in 𝒯(F,V)}"
by (rule finite_subset[OF _ fin], auto)
also have "{t. size t ≤ n ∧ t : τ in 𝒯(F,V)} = {t. t : τ in 𝒯(F,V)}"
using size by blast
finally show ?thesis by auto
qed
lemma finite_sig_bdd_above_iff_finite: assumes "finite (dom F)" and "finite (dom V)"
shows "bdd_above (size ` {t. t : τ in 𝒯(F,V)}) = finite {t. t : τ in 𝒯(F,V)}"
using finite_sig_bdd_above_imp_finite[OF assms] finite_imp_size_bdd_above
by metis
lemma compute_inf_card_sorts:
fixes C :: "('f,'t)ssig"
assumes C_Cs: "C = map_of Cs"
and arg_types_nonempty: "∀ f τs τ τ'. f : τs → τ in C ⟶ τ' ∈ set τs ⟶ ¬ empty_sort C τ'"
and dist: "distinct (map fst Cs)"
and result: "compute_inf_card_sorts Cs = (unb, cards)"
shows "unb = {τ. ¬ bdd_above (size ` {t. t : τ in 𝒯(C)})}" (is "_ = ?unb")
"cards = card_of_sort C" (is "_ = ?cards")
"unb = {τ. ¬finite_sort C τ}" (is "_ = ?inf")
proof -
let ?terms = "λ τ. {t. t : τ in 𝒯(C)}"
define taus where "taus = remdups (map snd Cs)"
define Cs' where "Cs' = map (λ τ. (τ, map fst (filter(λf. snd f = τ) Cs))) taus"
have "compute_inf_card_sorts Cs = compute_inf_card_main (set (map fst Cs')) (K$ 0) Cs'"
unfolding compute_inf_card_sorts_def taus_def Cs'_def Let_def by auto
also have "… = (?unb, ?cards)"
proof (rule compute_inf_card_main[OF C_Cs _ arg_types_nonempty _ 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
{ 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)
have emp: "empty_sort C τ"
proof (intro empty_sortI notI)
fix t
assume "t : τ in 𝒯(C)"
thus False using diff
proof induct
case (Fun f ss σs τ)
from Fun(1,4) show False unfolding fun_hastype_def by auto
qed auto
qed
}
note * = this
show "∀τ. τ ∉ set (map fst Cs') ⟶ bdd_above (size ` ?terms τ)"
"∀τ. τ ∉ set (map fst Cs') ⟶ (K$ 0) $ τ = card_of_sort C τ ∧ finite_sort C τ"
by (auto simp del: set_map dest!: *)
qed auto
finally show unb: "unb = ?unb" and cards: "cards = ?cards" unfolding result by auto
show "unb = ?inf" unfolding unb
proof (subst finite_sig_bdd_above_iff_finite)
show "finite (dom C)" unfolding C_Cs by (rule finite_dom_map_of)
show "finite (dom ∅)" by auto
qed (auto simp: finite_sort)
qed
end
abbreviation compute_inf_sorts :: "(('f × 't list) × 't)list ⇒ 't set" where
"compute_inf_sorts Cs ≡ fst (compute_inf_card_sorts Cs)"
lemma compute_inf_sorts:
assumes arg_types_nonempty: "∀ f τs τ τ'. f : τs → τ in map_of Cs ⟶ τ' ∈ set τs ⟶ ¬ empty_sort (map_of Cs) τ'"
and dist: "distinct (map fst Cs)"
shows
"compute_inf_sorts Cs = {τ. ¬ bdd_above (size ` {t. t : τ in 𝒯(map_of Cs)})}"
"compute_inf_sorts Cs = {τ. ¬ finite_sort (map_of Cs) τ}"
using compute_inf_card_sorts[OF refl assms]
by (cases "compute_inf_card_sorts Cs", auto)+
end