Theory SortsExe
section "Executable Sorts"
theory SortsExe
imports Sorts
begin
type_synonym exeosig = "(class × class) list × (name × (class × sort list) list) list"
abbreviation (input) "execlasses ≡ fst"
abbreviation (input) "exetcsigs ≡ snd"
abbreviation alist_conds :: "('k::linorder × 'v) list ⇒ bool" where
"alist_conds al ≡ distinct (map fst al)"
definition exe_ars_conds :: "(name × (class × sort list) list) list ⇒ bool" where
"exe_ars_conds arss ⟷ alist_conds arss ∧ (∀ars ∈ snd ` set arss . alist_conds ars)"
fun exe_ars_conds' :: "(('k1::linorder) × (('k2::linorder) × 's list) list) list ⇒ bool" where
"exe_ars_conds' arss ⟷ alist_conds arss ∧ (∀ars ∈ snd ` set arss . alist_conds ars)"
lemma [code]: "exe_ars_conds arss ⟷ exe_ars_conds' arss"
by (simp add: exe_ars_conds_def)
definition exe_class_conds :: "(class × class) list ⇒ bool" where
"exe_class_conds cs ≡ distinct cs"
definition exe_osig_conds :: "exeosig ⇒ bool" where
"exe_osig_conds a ≡ exe_class_conds (execlasses a) ∧ exe_ars_conds (exetcsigs a)"
fun translate_ars :: "(name × (class × sort list) list) list ⇒ name ⇀ (class ⇀ sort list)" where
"translate_ars ars = map_of (map (apsnd map_of) ars)"
abbreviation "illformed_osig ≡ ({}, Map.empty(STR ''A'' ↦ Map.empty(STR ''A'' ↦ [{STR ''A''}])))"
lemma illformed_osig_not_wf_osig: "¬ wf_osig illformed_osig"
by (auto simp add: coregular_tcsigs_def complete_tcsigs_def consistent_length_tcsigs_def
all_normalized_and_ex_tcsigs_def sort_ex_def wf_sort_def)
fun translate_osig :: "exeosig ⇒ osig" where
"translate_osig (cs, arss) = (if exe_osig_conds (cs, arss)
then (set cs, translate_ars arss)
else illformed_osig)"
definition "exe_consistent_length_tcsigs arss ≡ (∀ars ∈ snd ` set arss .
∀ss⇩1 ∈ snd ` set ars. ∀ss⇩2 ∈ snd ` set ars. length ss⇩1 = length ss⇩2)"
lemma in_alist_imp_in_map_of: "distinct (map fst arss)
⟹ (name, ars) ∈ set arss ⟹ translate_ars arss name = Some (map_of ars)"
by (induction arss) (auto simp add: rev_image_eqI)
lemma "exe_ars_conds arss ⟹ ∃name . map_of (map (apsnd map_of) arss) name = Some ars
⟹ ∃name arsl . (name, arsl) ∈ set arss ∧ map_of arsl = ars"
by (force simp add: exe_ars_conds_def)
lemma "exe_ars_conds arss
⟹ (name, arsl) ∈ set arss ∧ map_of arsl = ars
⟹ map_of (map (apsnd map_of) arss) name = Some ars"
by (force simp add: exe_ars_conds_def)
lemma consistent_length_tcsigs_imp_exe_consistent_length_tcsigs:
"exe_ars_conds arss ⟹ consistent_length_tcsigs (translate_ars arss)
⟹ exe_consistent_length_tcsigs arss"
unfolding consistent_length_tcsigs_def exe_consistent_length_tcsigs_def
apply (clarsimp simp add: exe_ars_conds_def)
by (metis in_alist_imp_in_map_of map_of_is_SomeI ranI snd_conv translate_ars.simps)
lemma exe_consistent_length_tcsigs_imp_consistent_length_tcsigs:
assumes "exe_ars_conds arss" "exe_consistent_length_tcsigs arss"
shows "consistent_length_tcsigs (translate_ars arss)"
proof-
{
fix ars ss⇩1 ss⇩2
assume p: "ars ∈ ran (map_of (map (apsnd map_of) arss))" "ss⇩1 ∈ ran ars" "ss⇩2 ∈ ran ars"
from p(1) obtain name where "map_of (map (apsnd map_of) arss) name = Some ars"
by (meson in_range_if_ex_key)
from this obtain arsl where "(name, arsl) ∈ set arss" "map_of arsl = ars"
using assms(1) by (auto simp add: exe_ars_conds_def)
from this obtain c1 c2 where "ars c1 = Some ss⇩1" "ars c2 = Some ss⇩2"
by (metis in_range_if_ex_key p(2) p(3))
hence "(c1, ss⇩1) ∈ set arsl" "(c2, ss⇩2) ∈ set arsl"
by (simp_all add: ‹map_of arsl = ars› map_of_SomeD)
hence "length ss⇩1 = length ss⇩2"
using assms(2) ‹(name, arsl) ∈ set arss›
by (fastforce simp add: exe_consistent_length_tcsigs_def)
}
note 1 = this
show ?thesis
by (simp add: consistent_length_tcsigs_def exe_consistent_length_tcsigs_def) (use 1 in blast)
qed
lemma consistent_length_tcsigs_iff_exe_consistent_length_tcsigs:
"exe_ars_conds arss ⟹
consistent_length_tcsigs (translate_ars arss) ⟷ exe_consistent_length_tcsigs arss"
using consistent_length_tcsigs_imp_exe_consistent_length_tcsigs
exe_consistent_length_tcsigs_imp_consistent_length_tcsigs by blast
definition "exe_complete_tcsigs cs arss
≡ (∀ars ∈ snd ` set arss .
∀(c⇩1, c⇩2) ∈ set cs . c⇩1∈fst ` set ars ⟶ c⇩2∈fst ` set ars)"
lemma exe_complete_tcsigs_imp_complete_tcsigs:
assumes "exe_ars_conds arss" "exe_complete_tcsigs cs arss"
shows "complete_tcsigs (set cs) (translate_ars arss)"
proof-
{
fix ars a b y
assume p: "ars ∈ ran (map_of (map (apsnd map_of) arss))"
"(a, b) ∈ set cs" "ars a = Some y"
from p(1) obtain name where "map_of (map (apsnd map_of) arss) name = Some ars"
by (meson in_range_if_ex_key)
from this obtain arsl where "(name, arsl) ∈ set arss" "map_of arsl = ars"
using assms(1) by (auto simp add: exe_ars_conds_def)
hence "(a, y) ∈ set arsl"
by (simp add: map_of_SomeD p(3))
hence"∃y. ars b = Some y"
using assms(2) ‹(name, arsl) ∈ set arss›
apply (clarsimp simp add: exe_complete_tcsigs_def)
by (metis (no_types, lifting) ‹map_of arsl = ars› case_prodD domD domI dom_map_of_conv_image_fst
p(2) p(3) snd_conv)
}
note 1 = this
show ?thesis
by (simp add: complete_tcsigs_def exe_complete_tcsigs_def) (use 1 in blast)
qed
lemma complete_tcsigs_imp_exe_complete_tcsigs: "exe_ars_conds arss ⟹
complete_tcsigs (set cs) (translate_ars arss) ⟹ exe_complete_tcsigs cs arss"
unfolding complete_tcsigs_def exe_complete_tcsigs_def exe_ars_conds_def
by (metis (mono_tags, lifting) case_prod_unfold dom_map_of_conv_image_fst in_alist_imp_in_map_of
in_range_if_ex_key map_of_SomeD ran_distinct)
lemma exe_complete_tcsigs_iff_complete_tcsigs:
"exe_ars_conds arss ⟹
complete_tcsigs (set cs) (translate_ars arss) ⟷ exe_complete_tcsigs cs arss"
using exe_complete_tcsigs_imp_complete_tcsigs complete_tcsigs_imp_exe_complete_tcsigs
by blast
definition "exe_coregular_tcsigs (cs :: (class × class) list) arss
≡ (∀ars ∈ snd ` set arss .
∀c⇩1 ∈ fst ` set ars. ∀c⇩2 ∈ fst ` set ars.
(class_leq (set cs) c⇩1 c⇩2 ⟶
list_all2 (sort_leq (set cs)) (the (lookup (λx. x=c⇩1) ars)) (the (lookup (λx. x=c⇩2) ars))))"
lemma exe_coregular_tcsigs_imp_coregular_tcsigs:
assumes "exe_ars_conds arss" "exe_coregular_tcsigs cs arss"
shows "coregular_tcsigs (set cs) (translate_ars arss)"
proof-
{
fix ars c⇩1 c⇩2 ss1 ss2
assume p: "ars ∈ ran (map_of (map (apsnd map_of) arss))" "ars c⇩1 = Some ss1" "ars c⇩2 = Some ss2"
"class_leq (set cs) c⇩1 c⇩2"
from p(1) obtain name where "map_of (map (apsnd map_of) arss) name = Some ars"
by (meson in_range_if_ex_key)
from this obtain arsl where "(name, arsl) ∈ set arss" "map_of arsl = ars"
using assms(1) by (auto simp add: exe_ars_conds_def)
from this obtain c1 c2 where "ars c1 = Some ss1" "ars c2 = Some ss2" "class_leq (set cs) c1 c2"
using p(2) p(3) p(4) by blast
hence "(c1, ss1) ∈ set arsl" "(c2, ss2) ∈ set arsl"
by (simp_all add: ‹map_of arsl = ars› map_of_SomeD)
hence "lookup (λx. x=c1) arsl = Some ss1" "lookup (λx. x=c2) arsl = Some ss2"
by (metis ‹(name, arsl) ∈ set arss› assms(1) exe_ars_conds_def
image_eqI lookup_present_eq_key snd_conv)+
hence "list_all2 (sort_leq (set cs)) ss1 ss2"
using assms(2) ‹(name, arsl) ∈ set arss› ‹(c1, ss1) ∈ set arsl› ‹(c2, ss2) ∈ set arsl›
‹class_leq (set cs) c1 c2›
by (fastforce simp add: exe_coregular_tcsigs_def)
}
note 1 = this
show ?thesis
by (auto simp add: coregular_tcsigs_def exe_coregular_tcsigs_def) (use 1 in blast)
qed
lemma coregular_tcsigs_imp_exe_coregular_tcsigs:
assumes "exe_ars_conds arss" "coregular_tcsigs (set cs) (translate_ars arss)"
shows "exe_coregular_tcsigs cs arss"
proof-
{
fix name ars c1 ss1 c2 ss2
assume p: "(name, ars) ∈ set arss" "(c1, ss1) ∈ set ars" "(c2, ss2) ∈ set ars"
"class_leq (set cs) c1 c2"
have s1: "(lookup (λx. x = c1) ars) = Some ss1"
using assms(1) lookup_present_eq_key p(1) p(2) by (force simp add: exe_ars_conds_def)
have s2: "(lookup (λx. x = c2) ars) = Some ss2"
using assms(1) lookup_present_eq_key p(1) p(3) by (force simp add: exe_ars_conds_def)
have "list_all2 (sort_leq (set cs)) (the (lookup (λx. x = c1) ars)) (the (lookup (λx. x = c2) ars))"
using assms apply (simp add: coregular_tcsigs_def s1 s2 exe_ars_conds_def)
by (metis domIff in_alist_imp_in_map_of map_of_is_SomeI option.distinct(1) option.sel
p(1) p(2) p(3) p(4) ranI snd_conv translate_ars.simps)
}
note 1 = this
show ?thesis
by (auto simp add: coregular_tcsigs_def exe_coregular_tcsigs_def) (use 1 in blast)
qed
lemma coregular_tcsigs_iff_exe_coregular_tcsigs:
"exe_ars_conds arss ⟹ coregular_tcsigs (set cs) (translate_ars arss) ⟷ exe_coregular_tcsigs cs arss"
using coregular_tcsigs_imp_exe_coregular_tcsigs exe_coregular_tcsigs_imp_coregular_tcsigs by blast
lemma "wf_subclass sub ⟹ Field sub = Domain sub"
using refl_on_def by fastforce
definition [simp]: "exefield rel = List.union (map fst rel) (map snd rel)"
lemma Field_set_code: "Field (set rel) = set (exefield rel)"
by (induction rel) fastforce+
lemma class_ex_rec: "finite r ⟹ class_ex (insert (a,b) r) c = (a=c ∨ b=c ∨ class_ex r c)"
by (induction r rule: finite_induct) (auto simp add: class_ex_def)
definition [simp]: "execlass_ex rel c = List.member (exefield rel) c"
lemma execlass_ex_code: "class_ex (set rel) c = execlass_ex rel c"
by (metis Field_set_code class_ex_def execlass_ex_def in_set_member)
definition [simp]: "exesort_ex rel S = (∀x∈S . (List.member (exefield rel) x))"
lemma sort_ex_code: "sort_ex (set rel) S = exesort_ex rel S"
by (simp add: execlass_ex_code sort_ex_class_ex)
definition [simp]: "execlass_les cs c1 c2 = (List.member cs (c1,c2) ∧ ¬ List.member cs (c2,c1))"
lemma execlass_les_code: "class_les (set cs) c1 c2 = execlass_les cs c1 c2"
by (simp add: class_leq_def class_les_def member_def)
definition [simp]: "exenormalize_sort cs (s::sort)
= {c ∈ s . ¬ (∃c' ∈ s . execlass_les cs c' c)}"
definition [simp]: "exenormalized_sort cs s ≡ (exenormalize_sort cs s) = s"
lemma normalize_sort_code[code]: "normalize_sort (set cs) s = exenormalize_sort cs s"
by (auto simp add: normalize_sort_def List.member_def list_ex_iff class_leq_def class_les_def)
lemma normalized_sort_code[code]: "normalized_sort (set cs) s = exenormalized_sort cs s"
using exenormalized_sort_def normalize_sort_code by presburger
definition [simp]: "exewf_sort sub S ≡ exenormalized_sort sub S ∧ exesort_ex sub S"
lemma wf_sort_code:
assumes "exe_class_conds sub"
shows "wf_sort (set sub) S = exewf_sort sub S"
using normalized_sort_code sort_ex_code assms
by (simp add: sort_ex_code wf_sort_def)
declare exewf_sort_def[code del]
lemma [code]: "exewf_sort sub S ≡ (S = {} ∨ exenormalized_sort sub S ∧ exesort_ex sub S)"
by simp (smt ball_empty bot_set_def empty_Collect_eq)
definition "exe_all_normalized_and_ex_tcsigs cs arss
≡ (∀ars ∈ snd ` set arss . ∀ss ∈ snd ` set ars . ∀s ∈ set ss. exewf_sort cs s)"
lemma all_normalized_and_ex_tcsigs_imp_exe_all_normalized_and_ex_tcsigs:
assumes "exe_ars_conds arss" "all_normalized_and_ex_tcsigs (set cs) (translate_ars arss)"
shows "exe_all_normalized_and_ex_tcsigs cs arss"
proof-
have ac: "alist_conds arss"
using assms(1) exe_ars_conds_def by blast
{
fix s ars
assume a1: "(s, ars) ∈ set arss"
fix c Ss
assume a2: "(c,Ss) ∈ set ars"
fix S
assume a3: "S ∈ set Ss"
have "map_of ars ∈ ran (map_of (map (apsnd map_of) arss))"
using ac a1 by (metis in_alist_imp_in_map_of ranI translate_ars.simps)
moreover have "Ss ∈ ran (map_of ars)"
using a1 a2 assms(1) by (metis exe_ars_conds_def map_of_is_SomeI ranI ran_distinct)
ultimately have "wf_sort (set cs) S"
using assms(2) a1 a2 a3 by (auto simp add: all_normalized_and_ex_tcsigs_def )
}
thus ?thesis
using normalize_sort_code wf_sort_def
by (clarsimp simp add: all_normalized_and_ex_tcsigs_def exe_all_normalized_and_ex_tcsigs_def
exe_ars_conds_def wf_sort_def wf_sort_code normalize_sort_def sort_ex_code)
qed
lemma exe_all_normalized_and_ex_tcsigs_imp_all_normalized_and_ex_tcsigs:
assumes "exe_ars_conds arss" "exe_all_normalized_and_ex_tcsigs cs arss"
shows "all_normalized_and_ex_tcsigs (set cs) (translate_ars arss)"
proof-
{
fix ars ss s
assume p: "ars ∈ ran (map_of (map (apsnd map_of) arss))"
"ss ∈ ran ars" "s ∈ set ss"
from p(1) obtain name where "map_of (map (apsnd map_of) arss) name = Some ars"
by (meson in_range_if_ex_key)
from this obtain arsl where "(name, arsl) ∈ set arss" "map_of arsl = ars"
using assms(1) by (auto simp add: exe_ars_conds_def)
from this obtain c where c: "ars c = Some ss"
using in_range_if_ex_key p(2) by force
have "exewf_sort cs s"
by (metis (no_types, opaque_lifting) ‹(name, arsl) ∈ set arss› ‹map_of arsl = ars› assms(1) assms(2)
exe_all_normalized_and_ex_tcsigs_def exe_ars_conds_def image_iff p(2) p(3) ran_distinct snd_conv)
hence "wf_sort (set cs) s"
by (simp add: normalize_sort_code sort_ex_code wf_sort_def)
}
note 1 = this
show ?thesis
using 1 by (clarsimp simp add: wf_sort_def all_normalized_and_ex_tcsigs_def
exe_all_normalized_and_ex_tcsigs_def)
qed
lemma all_normalized_and_ex_tcsigs_iff_exe_all_normalized_and_ex_tcsigs:
"exe_ars_conds arss ⟹ all_normalized_and_ex_tcsigs (set cs) (translate_ars arss)
⟷ exe_all_normalized_and_ex_tcsigs cs arss"
using all_normalized_and_ex_tcsigs_imp_exe_all_normalized_and_ex_tcsigs exe_all_normalized_and_ex_tcsigs_imp_all_normalized_and_ex_tcsigs by blast
definition [simp]: "exe_wf_tcsigs (cs :: (class × class) list) arss ≡
exe_coregular_tcsigs cs arss
∧ exe_complete_tcsigs cs arss
∧ exe_consistent_length_tcsigs arss
∧ exe_all_normalized_and_ex_tcsigs cs arss"
lemma wf_tcsigs_iff_exe_wf_tcsigs:
"exe_ars_conds arss ⟹ wf_tcsigs (set cs) (translate_ars arss) ⟷ exe_wf_tcsigs cs arss"
using all_normalized_and_ex_tcsigs_iff_exe_all_normalized_and_ex_tcsigs
consistent_length_tcsigs_imp_exe_consistent_length_tcsigs
coregular_tcsigs_iff_exe_coregular_tcsigs exe_complete_tcsigs_iff_complete_tcsigs
exe_consistent_length_tcsigs_imp_consistent_length_tcsigs exe_wf_tcsigs_def wf_tcsigs_def
by blast
fun exe_antisym :: "('a × 'a) list ⇒ bool" where
"exe_antisym [] ⟷ True"
| "exe_antisym ((x,y)#r) ⟷ ((y,x)∈set r ⟶ x=y) ∧ exe_antisym r"
lemma exe_antisym_imp_antisym: "exe_antisym l ⟹ antisym (set l)"
by (induction l) (auto simp add: antisym_def)
lemma antisym_imp_exe_antisym: "antisym (set l) ⟹ exe_antisym l"
proof (induction l)
case Nil
then show ?case
by simp
next
case (Cons a l)
then show ?case
by (simp add: antisym_def) (metis exe_antisym.simps(2) surj_pair)
qed
lemma antisym_iff_exe_antisym: "antisym (set l) = exe_antisym l"
using antisym_imp_exe_antisym exe_antisym_imp_antisym by blast
definition "exe_wf_subclass cs = (trans (set cs) ∧ exe_antisym cs ∧ Refl (set cs))"
lemma wf_classes_iff_exe_wf_classes: "wf_subclass (set cs) ⟷ exe_wf_subclass cs"
by (simp add: antisym_iff_exe_antisym exe_wf_subclass_def)
definition [simp]: "exe_wf_osig oss ≡ exe_wf_subclass (execlasses oss)
∧ exe_wf_tcsigs (execlasses oss) (exetcsigs oss) ∧ exe_osig_conds oss"
lemma exe_wf_osig_imp_wf_osig: "exe_wf_osig oss ⟹ wf_osig (translate_osig oss)"
using exe_coregular_tcsigs_imp_coregular_tcsigs exe_complete_tcsigs_imp_complete_tcsigs
exe_complete_tcsigs_imp_complete_tcsigs exe_all_normalized_and_ex_tcsigs_imp_all_normalized_and_ex_tcsigs
exe_consistent_length_tcsigs_imp_consistent_length_tcsigs
by (cases oss) (auto simp add: exe_wf_subclass_def exe_antisym_imp_antisym exe_osig_conds_def)
lemma classes_translate: "exe_osig_conds oss ⟹ subclass (translate_osig oss) = set (execlasses oss)"
by (cases oss) simp_all
lemma tcsigs_translate: "exe_osig_conds oss
⟹ tcsigs (translate_osig oss) = translate_ars (exetcsigs oss)"
by (cases oss) simp_all
lemma wf_osig_translate_imp_exe_osig_conds:
"wf_osig (translate_osig oss) ⟹ exe_osig_conds oss"
using illformed_osig_not_wf_osig by (metis translate_osig.elims)
lemma wf_osig_imp_exe_wf_osig:
assumes "wf_osig (translate_osig oss)" shows "exe_wf_osig oss"
apply (cases "translate_osig oss")
using classes_translate tcsigs_translate assms wf_osig_translate_imp_exe_osig_conds
by (metis (full_types) exe_osig_conds_def exe_wf_osig_def subclass.simps tcsigs.simps
wf_classes_iff_exe_wf_classes wf_osig.simps wf_tcsigs_iff_exe_wf_tcsigs)
lemma wf_osig_iff_exe_wf_osig: "wf_osig (translate_osig oss) ⟷ exe_wf_osig oss"
using exe_wf_osig_imp_wf_osig wf_osig_imp_exe_wf_osig by blast
end