Page MenuHomeIsabelle/Phabricator
Files F1601020

No OneTemporary
Actions

View Options

diff --git a/thys/Conditional_Transfer_Rule/CTR/Tests/CTR_TEST_PROCESS_CTR_RELATOR.ML b/thys/Conditional_Transfer_Rule/CTR/Tests/CTR_TEST_PROCESS_CTR_RELATOR.ML
--- a/thys/Conditional_Transfer_Rule/CTR/Tests/CTR_TEST_PROCESS_CTR_RELATOR.ML
+++ b/thys/Conditional_Transfer_Rule/CTR/Tests/CTR_TEST_PROCESS_CTR_RELATOR.ML
@@ -1,185 +1,187 @@
(* Title: CTR/Tests/CTR_TEST_PROCESS_CTR_RELATOR.ML
Author: Mihails Milehins
Copyright 2021 (C) Mihails Milehins
*)
signature CTR_TEST_PROCESS_CTR_RELATOR =
sig
type process_ctr_relator_in_type
val test_suite : Proof.context -> unit -> unit
end;
structure ctr_test_process_ctr_relator : CTR_TEST_PROCESS_CTR_RELATOR =
struct
(**** Background ****)
open SpecCheck;
structure Prop = SpecCheck_Property;
structure Show = SpecCheck_Show;
(**** Auxiliary ****)
fun mk_msg_ctr_relator msg = "ctr_relator: " ^ msg;
(*** Data ***)
type process_ctr_relator_in_type = string * Proof.context;
(**** Visualization ****)
+(*FIXME: complete the migration to SpecCheck.Show*)
+
fun show_ctr_relator_in (process_ctr_relator_in : process_ctr_relator_in_type) =
let
val (c, _) = process_ctr_relator_in
val name_c = "constant name: " ^ c
val ctxt_c = "lthy: unknown context"
val out_c = [name_c, ctxt_c] |> String.concatWith "\n"
in Pretty.str out_c end;
(**** Tests ****)
(*** Wrapper ***)
fun process_ctr_relator ((c, ctxt) : process_ctr_relator_in_type) =
CTR_Relators.process_ctr_relator c ctxt;
(*** Exceptions ***)
fun test_exc_template ctxt c err_msg_end_c test_name_c =
let
val args = (c, ctxt)
val err_msg = mk_msg_ctr_relator err_msg_end_c
val exn_prop = Prop.expect_failure (ERROR err_msg) process_ctr_relator
in
check_list_unit
show_ctr_relator_in
[args]
test_name_c
exn_prop
end;
fun test_exc_not_const ctxt _ = test_exc_template
ctxt "a + b" "the input must be a constant term" "not a constant";
fun test_exc_not_body_bool ctxt _ = test_exc_template
ctxt
"Cons"
"the body of the type of the input must be bool"
"not bool body";
fun test_exc_not_binders_2 ctxt _ = test_exc_template
ctxt
"Ex"
"the type of the input must have more than two binders"
"not two binders";
fun test_exc_not_binders_binrelT ctxt _ = test_exc_template
ctxt
"not_binders_binrelT"
(
"all of the binders associated with the type of the input" ^
"except the last two must be the binary relation types"
)
"not binary relation types";
fun test_exc_no_dup_binrelT ctxt _ = test_exc_template
ctxt
"no_dup_binrelT"
(
"the types of the binders of the binary relations associated " ^
"with the type of the input must have no duplicates"
)
"no duplicates in the binary relation types";
fun test_exc_not_binders_binrelT_ftv_stv ctxt _ = test_exc_template
ctxt
"not_binders_binrelT_ftv_stv"
(
"the types of the binders of the binary relation types associated " ^
"with the input type must be either free type variables or " ^
"schematic type variables"
)
"not binrel type ftv or stv";
fun test_exc_not_type_constructor_lhs ctxt _ = test_exc_template
ctxt
"not_type_constructor_lhs"
(
"the last two binders of the input type must be " ^
"the results of an application of a type constructor"
)
"not type constructor lhs";
fun test_exc_not_type_constructor_rhs ctxt _ = test_exc_template
ctxt
"not_type_constructor_rhs"
(
"the last two binders of the input type must be " ^
"the results of an application of a type constructor"
)
"not type constructor rhs";
fun test_exc_not_identical_type_constructors_lhs ctxt _ = test_exc_template
ctxt
"not_identical_type_constructors_lhs"
(
"the sequences of the input types to the type constructors that are " ^
"associated with the last two binders of the input type must be " ^
"identical to the sequences of the types formed by concatenating the " ^
"type variables associated with the left hand side and the right " ^
"hand side of the binary relation types, respectively"
)
"not identical type constructors lhs";
fun test_exc_not_identical_type_constructors_rhs ctxt _ = test_exc_template
ctxt
"not_identical_type_constructors_rhs"
(
"the sequences of the input types to the type constructors that are " ^
"associated with the last two binders of the input type must be " ^
"identical to the sequences of the types formed by concatenating the " ^
"type variables associated with the left hand side and the right " ^
"hand side of the binary relation types, respectively"
)
"not identical type constructors rhs";
(**** Test Suite ****)
fun test_suite ctxt s =
[
test_exc_not_const,
test_exc_not_body_bool,
test_exc_not_binders_2,
test_exc_not_binders_binrelT,
test_exc_no_dup_binrelT,
test_exc_not_binders_binrelT_ftv_stv,
test_exc_not_type_constructor_lhs,
test_exc_not_type_constructor_rhs,
test_exc_not_identical_type_constructors_lhs,
test_exc_not_identical_type_constructors_rhs
]
|> map (fn f => f ctxt s)
|> Lecker.test_group ctxt s;
end;
\ No newline at end of file
diff --git a/thys/Conditional_Transfer_Rule/CTR/Tests/CTR_TEST_PROCESS_RELATIVIZATION.ML b/thys/Conditional_Transfer_Rule/CTR/Tests/CTR_TEST_PROCESS_RELATIVIZATION.ML
--- a/thys/Conditional_Transfer_Rule/CTR/Tests/CTR_TEST_PROCESS_RELATIVIZATION.ML
+++ b/thys/Conditional_Transfer_Rule/CTR/Tests/CTR_TEST_PROCESS_RELATIVIZATION.ML
@@ -1,304 +1,306 @@
(* Title: CTR/Tests/CTR_TEST_PROCESS_RELATIVIZATION.ML
Author: Mihails Milehins
Copyright 2021 (C) Mihails Milehins
*)
signature CTR_TEST_PROCESS_RELATIVIZATION =
sig
type process_relativization_in_type
val test_suite : Proof.context -> unit -> unit
end;
structure ctr_test_process_relativization : CTR_TEST_PROCESS_RELATIVIZATION =
struct
(**** Background ****)
open SpecCheck;
structure Prop = SpecCheck_Property;
structure Show = SpecCheck_Show;
(**** Auxiliary ****)
fun mk_msg_ctr_error msg = "ctr: " ^ msg
(*** Data ***)
type process_relativization_in_type =
(
(string * thm list option) option *
Element.context list *
(string * string) list *
((binding option * thm) * mixfix)
) * Proof.context;
(*** Relation ***)
local
fun map_const_name (oldc, newc) (Const (c, T)) =
if oldc = c then Const (newc, T) else Const (c, T)
| map_const_name eqc (Abs (c, T, t)) = Abs (c, T, map_const_name eqc t)
| map_const_name eqc (t $ u) = map_const_name eqc t $ map_const_name eqc u
| map_const_name _ t = t
in
fun process_relativization_test_eq
(PPRelativization args1, PPRelativization args2) =
let
val act_lthy = #2 args1
val exp_lthy = #2 args2
val (act_ow_def_t, act_tr_t) = args1
|> #1
|>> Local_Defs.meta_rewrite_rule act_lthy
|> apply2 Thm.full_prop_of
val (exp_ow_def_t, exp_tr_t) = args2
|> #1
|>> Local_Defs.meta_rewrite_rule act_lthy
|> apply2 Thm.full_prop_of
val act_ow_def_lhst = act_ow_def_t |> Logic.dest_equals |> #1
val exp_ow_def_lhst = exp_ow_def_t |> Logic.dest_equals |> #1
val thy = Proof_Context.theory_of exp_lthy
val mapc =
(
act_ow_def_lhst |> head_of |> dest_Const |> #1,
exp_ow_def_lhst |> head_of |> dest_Const |> #1
)
val act_ow_def_t' = map_const_name mapc act_ow_def_t
val act_tr_t' = map_const_name mapc act_tr_t
val act_ow_def_eq = Pattern.equiv thy (act_ow_def_t', exp_ow_def_t)
val tr_eq = Pattern.equiv thy (act_tr_t', exp_tr_t)
val _ = act_ow_def_eq |> Bool.toString |> writeln
in act_ow_def_eq andalso tr_eq end
| process_relativization_test_eq
(PPParametricity args1, PPParametricity args2) =
(*careful: not needed; hence, a usable implementation is not provided*)
Thm.eq_thm (fst args1, fst args2)
| process_relativization_test_eq (_, _) = false;
end;
(**** Visualization ****)
+(*FIXME: complete the migration to SpecCheck.Show*)
+
fun string_of_elem_ctxt_fixes args = "fixes: " ^
(
args
|> map (fn (x, y, _) => (x, y))
|> ML_Syntax.print_list
(ML_Syntax.print_pair Binding.print (ML_Syntax.print_option I))
);
fun string_of_elem_ctxt_assumes ctxt args =
let
val string_of_fst = ML_Syntax.print_pair
Binding.print
(ML_Syntax.print_list (Token.pretty_src ctxt #> Pretty.string_of))
val string_of_snd =
ML_Syntax.print_list (ML_Syntax.print_pair I (ML_Syntax.print_list I))
in
"assumes: " ^
ML_Syntax.print_list (ML_Syntax.print_pair string_of_fst string_of_snd) args
end;
fun string_of_elem_ctxt_constrains _ = "constrains: unknown constrains";
fun string_of_elem_ctxt_defines _ = "defines: unknown defines";
fun string_of_elem_ctxt_notes _ = "notes: unknown notes";
fun string_of_elem_ctxt_lazy_notes _ = "lazy notes: unknown lazy notes";
fun string_of_elem_ctxt _ (Element.Fixes args : Element.context) =
string_of_elem_ctxt_fixes args
| string_of_elem_ctxt _ (Element.Constrains args) =
string_of_elem_ctxt_constrains args
| string_of_elem_ctxt ctxt (Element.Assumes args) =
string_of_elem_ctxt_assumes ctxt args
| string_of_elem_ctxt _ (Element.Defines args) =
string_of_elem_ctxt_defines args
| string_of_elem_ctxt _ (Element.Notes args) =
string_of_elem_ctxt_notes args
| string_of_elem_ctxt _ (Element.Lazy_Notes args) =
string_of_elem_ctxt_lazy_notes args
fun show_relativization_in
ctxt
(process_relativization_in : process_relativization_in_type) =
let
val ((synthesis_opt, elems, type_specs, thm_spec), lthy) =
process_relativization_in
val synthesis_opt_c =
let val synthesis_c = "synthesis: "
in
case synthesis_opt of
SOME synthesis =>
(
case #2 synthesis of
SOME _ => synthesis_c ^ "user-defined simpset"
| NONE => synthesis_c ^ "default simpset"
)
| NONE => synthesis_c ^ "none"
end
val elems_c = "elements:" ^
(
if null elems
then " none"
else "\n" ^
(
elems
|> map (string_of_elem_ctxt ctxt)
|> map (fn c => "\t" ^ c)
|> String.concatWith "\n"
)
)
val type_specs_c = "type_specs: " ^
ML_Syntax.print_list (ML_Syntax.print_pair I I) type_specs
val thm_spec_c =
"definition: " ^ (thm_spec |> #1 |> #2 |> Thm.string_of_thm lthy)
val lthy_c = "lthy: unknown local theory"
val out_c = [synthesis_opt_c, elems_c, type_specs_c, thm_spec_c, lthy_c]
|> String.concatWith "\n"
in Pretty.str out_c end;
fun show_relativization ctxt =
Show.zip (show_relativization_in ctxt) (Pretty.str o string_of_pp_out)
(**** Tests ****)
(*** Wrapper ***)
fun process_relativization
(
((synthesis, assms, type_specs, thm_spec), lthy) :
process_relativization_in_type
) = CTR.process_relativization synthesis assms type_specs thm_spec lthy;
(*** Valid inputs ***)
fun test_eq_trivial ctxt _ =
let
(*input*)
val {synthesis, elems, type_specs, thm_specs, ...} =
ctr_test_data_of_proof ctxt "mono_with" |> the
val process_relativization_in : process_relativization_in_type =
((synthesis, elems, type_specs, the_single thm_specs), ctxt)
(*output*)
val process_relativization_out =
PPRelativization ((@{thm mono_ow_def}, @{thm mono_ow_transfer'}), ctxt)
in
check_list_unit
(show_relativization ctxt)
[(process_relativization_in, process_relativization_out)]
"equality"
(
Prop.prop
(
fn (val_in, exp_out) =>
process_relativization_test_eq
(process_relativization val_in, exp_out)
)
)
end;
(*** Exceptions ***)
fun test_exc_template ctxt input_name_c err_msg_end_c test_name_c =
let
val {synthesis, elems, type_specs, thm_specs, ...} =
ctr_test_data_of_proof ctxt input_name_c |> the
val args = ((synthesis, elems, type_specs, the_single thm_specs), ctxt)
val err_msg = mk_msg_ctr_error err_msg_end_c
val exn_prop = Prop.expect_failure (ERROR err_msg) process_relativization
in
check_list_unit
(show_relativization_in ctxt)
[args]
test_name_c
exn_prop
end;
fun test_exc_def ctxt _ =
let
val err_msg_end_c =
(
Syntax.string_of_term ctxt (Thm.full_prop_of @{thm exI}) ^
" is not a definition"
)
in test_exc_template ctxt "exI" err_msg_end_c "not a definition" end;
fun test_exc_binrel ctxt _ =
let val err_msg_end_c = "trp: trp must consist of (stv, binary relation) pairs"
in test_exc_template ctxt "binrel" err_msg_end_c "binary relation" end;
fun test_exc_binrel_ftv ctxt _ =
let
val err_msg_end_c =
"trp: the user-specified binary relations must " ^
"be defined over type variables"
in test_exc_template ctxt "binrel_ftv" err_msg_end_c "binary relation ftv" end;
fun test_exc_dup_stvs ctxt _ =
let val err_msg_end_c = "trp: duplicate stvs"
in test_exc_template ctxt "dup_stvs" err_msg_end_c "duplicate stv" end;
fun test_exc_dup_binrel_ftvs ctxt _ =
let
val err_msg_end_c =
"trp: duplicate ftvs in the specification of the binary relations"
in
test_exc_template
ctxt "dup_binrel_ftvs" err_msg_end_c "duplicate binrel ftvs"
end;
fun test_exc_no_relator ctxt _ =
let val err_msg_end_c = "no relator found for the type constructor CTR_Tests.K"
in test_exc_template ctxt "no_relator" err_msg_end_c "no relator" end;
fun test_exc_invalid_relator ctxt _ =
let
val err_msg_end_c =
(
"the relator found for the type constructor CTR_Tests.L " ^
"is not suitable (is there is a mismatch of type variables?)"
)
in
test_exc_template ctxt "invalid_relator" err_msg_end_c "invalid relator"
end;
(**** Test Suite ****)
fun test_suite ctxt s =
[
test_eq_trivial,
test_exc_def,
test_exc_binrel,
test_exc_binrel_ftv,
test_exc_dup_stvs,
test_exc_dup_binrel_ftvs,
test_exc_no_relator,
test_exc_invalid_relator
]
|> map (fn f => f ctxt s)
|> Lecker.test_group ctxt s;
end;
\ No newline at end of file
diff --git a/thys/Conditional_Transfer_Rule/CTR/Tests/CTR_Tests.thy b/thys/Conditional_Transfer_Rule/CTR/Tests/CTR_Tests.thy
--- a/thys/Conditional_Transfer_Rule/CTR/Tests/CTR_Tests.thy
+++ b/thys/Conditional_Transfer_Rule/CTR/Tests/CTR_Tests.thy
@@ -1,251 +1,250 @@
(* Title: CTR/Tests/CTR_Tests.thy
Author: Mihails Milehins
Copyright 2021 (C) Mihails Milehins
A test suite for the sub-framework CTR.
*)
section\<open>A test suite for CTR\<close>
theory CTR_Tests
imports
"../CTR"
"../../IML_UT/IML_UT"
- SpecCheck.SpecCheck_Dynamic
Complex_Main
keywords "ctr_test" :: thy_defn
begin
subsection\<open>Background\<close>
ML\<open>
type ctr_test_data =
{
ctr_type : string,
synthesis : (string * thm list option) option,
elems: (string, string, Facts.ref) Element.ctxt list,
type_specs : (string * string) list,
thm_specs : ((binding option * thm) * mixfix) list
};
structure CTRTestData = Generic_Data
(
type T = ctr_test_data Symtab.table
val empty = Symtab.empty
val merge = Symtab.merge (K true)
);
val get_ctr_test_data_generic = CTRTestData.get;
val get_ctr_test_data_proof = Context.Proof #> get_ctr_test_data_generic;
val get_ctr_test_data_global = Context.Theory #> get_ctr_test_data_generic;
fun test_data_of_generic context = context
|> get_ctr_test_data_generic
|> Symtab.lookup;
val ctr_test_data_of_proof = Context.Proof #> test_data_of_generic;
(*oversimplified: to be used with care*)
fun update_ctr_test_data k ctr_test_data =
Local_Theory.declaration
{pervasive=true, syntax=false}
(fn _ => (k, ctr_test_data) |> Symtab.update |> CTRTestData.map);
fun process_ctr_test_data (k, args) (lthy : local_theory) =
let
fun preprocess_thm_specs lthy =
map (apfst (apsnd (singleton (Attrib.eval_thms lthy))))
fun process_ctrs_impl (CTR.ALG_PP _) (lthy : local_theory) = lthy
| process_ctrs_impl
(CTR.ALG_RP (((synthesis, elems), type_specs), thm_specs))
(lthy : local_theory) =
let
val thm_specs' = preprocess_thm_specs lthy thm_specs
val synthesis' = Option.map
(apsnd (Option.map ((single #> Attrib.eval_thms lthy))))
synthesis
val data : ctr_test_data =
{
ctr_type = "relativization",
synthesis = synthesis',
elems = elems,
type_specs = type_specs,
thm_specs = thm_specs'
}
in update_ctr_test_data k data lthy end
in process_ctrs_impl args lthy end;
val ctr_test_parser = Parse.string -- CTR.ctr_parser;
val _ =
Outer_Syntax.local_theory
\<^command_keyword>\<open>ctr_test\<close>
"test setup for the command ctr"
(ctr_test_parser >> process_ctr_test_data);
\<close>
ud \<open>order.mono\<close>
ud mono' \<open>mono\<close>
definition mono_ow ::
"'a set \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
where "mono_ow UB leb lea f \<equiv> \<forall>x\<in>UB. \<forall>y\<in>UB. lea x y \<longrightarrow> leb (f x) (f y)"
typedef 'a K = \<open>{xs::'a list. length xs = 2}\<close>
by (simp add: Ex_list_of_length)
definition KK :: "'a K \<Rightarrow> 'a K \<Rightarrow> bool"
where "KK k1 k2 \<equiv> k1 = k2"
typedef 'a L = \<open>{xs::'a list. length xs = 2}\<close>
by (simp add: Ex_list_of_length)
definition LL :: "'a L \<Rightarrow> 'a L \<Rightarrow> bool"
where "LL k1 k2 \<equiv> k1 = k2"
definition rel_L ::
"('a::group_add \<Rightarrow> 'b::group_add \<Rightarrow> bool) \<Rightarrow>
'a::group_add L \<Rightarrow>
'b::group_add L \<Rightarrow>
bool"
where "rel_L A b c = True"
ctr_relator rel_L
definition not_binders_binrelT ::
"('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
where "not_binders_binrelT R1 R2 a b = True"
definition no_dup_binrelT ::
"('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
where "no_dup_binrelT R1 R2 a b = True"
definition not_binders_binrelT_ftv_stv ::
"('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
where "not_binders_binrelT_ftv_stv R1 R2 a b = True"
definition not_type_constructor_lhs ::
"('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a K \<Rightarrow> bool"
where "not_type_constructor_lhs R1 R2 a b = True"
definition not_type_constructor_rhs ::
"('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a K \<Rightarrow> 'e \<Rightarrow> bool"
where "not_type_constructor_rhs R1 R2 a b = True"
definition not_identical_type_constructors ::
"('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a K \<Rightarrow> 'e L \<Rightarrow> bool"
where "not_identical_type_constructors R1 R2 a b = True"
definition not_identical_type_constructors_lhs ::
"('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a K \<Rightarrow> 'b K \<Rightarrow> bool"
where "not_identical_type_constructors_lhs R1 R2 a b = True"
definition not_identical_type_constructors_rhs ::
"('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a K \<Rightarrow> 'c K \<Rightarrow> bool"
where "not_identical_type_constructors_rhs R1 a b = True"
subsection\<open>Test data\<close>
lemma mono_ow_transfer':
includes lifting_syntax
assumes [transfer_domain_rule, transfer_rule]: "Domainp B = (\<lambda>x. x \<in> UB)"
and [transfer_rule]: "right_total B"
shows
"((A ===> A ===> (=)) ===> (B ===> B ===> (=)) ===> (B ===> A) ===> (=))
(mono_ow UB) mono.with"
unfolding mono_ow_def mono.with_def
by (transfer_prover_start, transfer_step+) simp
ctr_test "mono_with" relativization
synthesis ctr_simps_Collect_mem_eq
assumes [transfer_domain_rule, transfer_rule]:
"Domainp (B::'c\<Rightarrow>'d\<Rightarrow>bool) = (\<lambda>x. x \<in> UB)"
and [transfer_rule]: "right_total B"
trp (?'b \<open>A::'a\<Rightarrow>'b\<Rightarrow>bool\<close>) and (?'a B)
in mono_ow': mono.with_def
ctr_test "exI" relativization
in mono_ow'': exI
ctr_test "binrel" relativization
synthesis ctr_simps_Collect_mem_eq
assumes [transfer_domain_rule, transfer_rule]:
"Domainp (B::'c\<Rightarrow>'d\<Rightarrow>bool) = (\<lambda>x. x \<in> UB)"
and [transfer_rule]: "right_total B"
trp (?'b A) and (?'a B)
in mono_ow': mono.with_def
ctr_test "binrel_ftv" relativization
synthesis ctr_simps_Collect_mem_eq
assumes [transfer_domain_rule, transfer_rule]:
"Domainp (B::'c\<Rightarrow>'d\<Rightarrow>bool) = (\<lambda>x. x \<in> UB)"
and [transfer_rule]: "right_total B"
trp (?'b \<open>A::nat\<Rightarrow>'b\<Rightarrow>bool\<close>) and (?'a B)
in mono_ow': mono.with_def
ctr_test "dup_stvs" relativization
synthesis ctr_simps_Collect_mem_eq
assumes [transfer_domain_rule, transfer_rule]:
"Domainp (B::'c\<Rightarrow>'d\<Rightarrow>bool) = (\<lambda>x. x \<in> UB)"
and [transfer_rule]: "right_total B"
trp (?'b \<open>A::'a\<Rightarrow>'b\<Rightarrow>bool\<close>) and (?'b B)
in mono_ow': mono.with_def
ctr_test "dup_binrel_ftvs" relativization
synthesis ctr_simps_Collect_mem_eq
assumes [transfer_domain_rule, transfer_rule]:
"Domainp (B::'c\<Rightarrow>'d\<Rightarrow>bool) = (\<lambda>x. x \<in> UB)"
and [transfer_rule]: "right_total B"
trp (?'b \<open>A::'a\<Rightarrow>'d\<Rightarrow>bool\<close>) and (?'a B)
in mono_ow': mono.with_def
ctr_test "no_relator" relativization
synthesis ctr_simps_Collect_mem_eq
assumes [transfer_domain_rule, transfer_rule]:
"Domainp (B::'c\<Rightarrow>'d\<Rightarrow>bool) = (\<lambda>x. x \<in> UB)"
and [transfer_rule]: "right_total B"
trp (?'b \<open>A::'a\<Rightarrow>'b\<Rightarrow>bool\<close>) and (?'a B)
in KK_def
ctr_test "invalid_relator" relativization
synthesis ctr_simps_Collect_mem_eq
assumes [transfer_domain_rule, transfer_rule]:
"Domainp (B::'c\<Rightarrow>'d\<Rightarrow>bool) = (\<lambda>x. x \<in> UB)"
and [transfer_rule]: "right_total B"
trp (?'b \<open>A::'a\<Rightarrow>'b\<Rightarrow>bool\<close>) and (?'a B)
in LL_def
subsection\<open>Tests\<close>
subsubsection\<open>\<open>process_relativization\<close>\<close>
ML_file\<open>CTR_TEST_PROCESS_RELATIVIZATION.ML\<close>
context
includes lifting_syntax
begin
ML\<open>
Lecker.test_group @{context} () [ctr_test_process_relativization.test_suite]
\<close>
end
subsubsection\<open>\<open>process_ctr_relator\<close>\<close>
ML_file\<open>CTR_TEST_PROCESS_CTR_RELATOR.ML\<close>
context
includes lifting_syntax
begin
ML\<open>
Lecker.test_group @{context} () [ctr_test_process_ctr_relator.test_suite]
\<close>
end
end
\ No newline at end of file
diff --git a/thys/Conditional_Transfer_Rule/IML_UT/IML_UT.thy b/thys/Conditional_Transfer_Rule/IML_UT/IML_UT.thy
--- a/thys/Conditional_Transfer_Rule/IML_UT/IML_UT.thy
+++ b/thys/Conditional_Transfer_Rule/IML_UT/IML_UT.thy
@@ -1,26 +1,26 @@
(* Title: IML_UT/IML_UT.thy
Author: Mihails Milehins
Copyright 2021 (C) Mihails Milehins
A minor extension of SpecCheck: courtesy of Kevin Kappelmann.
*)
section\<open>\<open>IML_UT\<close>\<close>
theory IML_UT
- imports SpecCheck.SpecCheck_Dynamic
+ imports SpecCheck.SpecCheck
begin
ML\<open>
open SpecCheck;
structure Prop = SpecCheck_Property;
structure Show = SpecCheck_Show;
fun style_error show_opt =
SpecCheck_Output_Style_Custom.style_custom writeln error show_opt
fun check_list_unit show ts name prop ctxt _ =
check_list_style style_error (SOME show) ts name prop ctxt
|> K ();
\<close>
end
\ No newline at end of file
diff --git a/thys/Conditional_Transfer_Rule/UD/Tests/UD_TEST_UNOVERLOAD_DEFINITION.ML b/thys/Conditional_Transfer_Rule/UD/Tests/UD_TEST_UNOVERLOAD_DEFINITION.ML
--- a/thys/Conditional_Transfer_Rule/UD/Tests/UD_TEST_UNOVERLOAD_DEFINITION.ML
+++ b/thys/Conditional_Transfer_Rule/UD/Tests/UD_TEST_UNOVERLOAD_DEFINITION.ML
@@ -1,275 +1,277 @@
(* Title: UD/Tests/UD_TEST_UNOVERLOAD_DEFINITION.ML
Author: Mihails Milehins
Copyright 2021 (C) Mihails Milehins
*)
signature UD_TEST_UNOVERLOAD_DEFINITION =
sig
type unoverload_definition_in_type
val test_suite : Proof.context -> unit -> unit
end;
structure ud_test_unoverload_definition : UD_TEST_UNOVERLOAD_DEFINITION =
struct
(**** Background ****)
open SpecCheck;
structure Prop = SpecCheck_Property;
structure Show = SpecCheck_Show;
(**** Auxiliary ****)
fun mk_msg_unoverload_definition_error msg = "ud: " ^ msg
(*** Data ***)
type unoverload_definition_in_type =
(binding * mixfix) * (string * typ) * theory;
(*** Relation ***)
fun ud_test_eq_thm thy (act_c, exp_c) (act_ud_out, exp_ud_out) =
let
fun rel (act_thm, exp_thm) =
let
fun replace_const (Const (c, T)) =
if c = exp_c then Const (act_c, T) else Const (c, T)
| replace_const (t $ u) = replace_const t $ replace_const u
| replace_const (Abs (c, T, t)) = Abs (c, T, replace_const t)
| replace_const x = x
val act_t = Thm.full_prop_of act_thm
val exp_t = exp_thm |> Thm.full_prop_of |> replace_const
in Pattern.equiv thy (act_t, exp_t) end;
fun ud_test_eq_thm_impl ((UD.trivial act_thm), (UD.trivial exp_thm)) =
rel (act_thm, exp_thm)
| ud_test_eq_thm_impl ((UD.nontrivial act_thms), (UD.nontrivial exp_thms)) =
let
val (act_with_def_thm, act_with_thm) = act_thms
val (exp_with_def_thm, exp_with_thm) = exp_thms
in
rel (act_with_def_thm, exp_with_def_thm)
andalso rel (act_with_thm, exp_with_thm)
end
| ud_test_eq_thm_impl (_, _) = false
in ud_test_eq_thm_impl (fst act_ud_out, fst exp_ud_out) end;
(**** Visualization ****)
+(*FIXME: complete the migration to SpecCheck.Show*)
+
fun show_unoverload_definition_in
(unoverload_definition_in : unoverload_definition_in_type) =
let
val ((b, _), (c, T), thy) = unoverload_definition_in
val b_c = "binding: " ^ Binding.name_of b
val const_c =
"constant: " ^
c ^
" :: " ^
Syntax.string_of_typ (Proof_Context.init_global thy) T
val thy_c = "thy: unknown theory"
val out_c = [b_c, const_c, thy_c] |> String.concatWith "\n"
in Pretty.str out_c end;
fun show_unoverload_definition_out (ud_thm_out, thy) =
let
val ctxt = Proof_Context.init_global thy
val ud_thm_c =
let
val with_thm_c = "with_thm: "
val with_def_thm_c = "with_def_thm: "
in
case ud_thm_out of
UD.trivial with_thm => with_thm_c ^ Thm.string_of_thm ctxt with_thm
| UD.nontrivial (with_def_thm, with_thm) =>
with_def_thm_c ^
Thm.string_of_thm ctxt with_def_thm ^
"\n" ^
with_thm_c ^
Thm.string_of_thm ctxt with_thm
end
val thy_c = "thy: unknown theory"
val out_c = [ud_thm_c, thy_c] |> String.concatWith "\n"
in Pretty.str out_c end;
val show_unoverload_definition =
Show.zip show_unoverload_definition_in show_unoverload_definition_out;
(**** Tests ****)
(*** Wrapper ***)
fun unoverload_definition
(((b, mixfix), (c, T), thy) : unoverload_definition_in_type) =
UD.unoverload_definition (b, mixfix) (c, T) thy;
(*** Valid inputs ***)
fun test_eq_trivial thy _ =
let
(*input*)
val act_c = "UD_Tests.closed'.with"
val exp_c = ""
val b = Binding.name "closed'"
val aT = TVar (("'a", 0), \<^sort>\<open>topological_space\<close>)
val T = HOLogic.mk_setT aT --> HOLogic.boolT
val closed_c = "Topological_Spaces.topological_space_class.closed"
val ud_in = ((b, NoSyn), (closed_c, T), thy)
(*output*)
val ud_out = (UD.trivial (@{thm closed_with}), thy)
in
check_list_unit
show_unoverload_definition
[(ud_in, ud_out)]
"trivial equality"
(
Prop.prop
(
fn (ud_in, ud_out) => ud_test_eq_thm
thy (act_c, exp_c) (unoverload_definition ud_in, ud_out)
)
)
end;
fun test_eq_nontrivial thy _ =
let
(*input*)
val act_c = "UD_Tests.closure.with"
val exp_c = "UD_Tests.closure_with"
val b = Binding.name "closure"
val aT = TVar (("'a", 0), \<^sort>\<open>topological_space\<close>)
val T = (HOLogic.mk_setT aT --> HOLogic.mk_setT aT)
val closure_c = "UD_Tests.closure"
val ud_in = ((b, NoSyn), (closure_c, T), thy)
(*output*)
val ud_out =
(UD.nontrivial (@{thm closure_with_def}, @{thm closure_with}), thy)
in
check_list_unit
show_unoverload_definition
[(ud_in, ud_out)]
"nontrivial equality"
(
Prop.prop
(
fn (ud_in, ud_out) => ud_test_eq_thm
thy (act_c, exp_c) (unoverload_definition ud_in, ud_out)
)
)
end;
(*** Exceptions ***)
fun test_exc_extra_type_variables thy _ =
let
val aT = TVar (("'a", 0), \<^sort>\<open>type\<close>)
val Sup_class_c = "Complete_Lattices.Sup_class"
val args : unoverload_definition_in_type =
(
(Binding.empty, NoSyn),
(Sup_class_c, Term.itselfT aT --> \<^typ>\<open>prop\<close>),
thy
)
val err_msg = mk_msg_unoverload_definition_error
"specification depends on extra type variables"
val exn_prop = Prop.expect_failure (ERROR err_msg) unoverload_definition
in
check_list_unit
show_unoverload_definition_in
[args]
"extra type variables"
exn_prop
end;
fun test_exc_ud_ex thy _ =
let
val aT = TVar (("'a", 0), \<^sort>\<open>type\<close>)
val T =
(HOLogic.mk_setT aT --> HOLogic.boolT) -->
HOLogic.mk_setT aT -->
HOLogic.boolT
val ts_c = "Topological_Spaces.topological_space.closed"
val args : unoverload_definition_in_type =
((Binding.empty, NoSyn), (ts_c, T), thy)
val err_msg = mk_msg_unoverload_definition_error
"unoverloaded constant already exists"
val exn_prop = Prop.expect_failure (ERROR err_msg) unoverload_definition
in
check_list_unit
show_unoverload_definition_in
[args]
"constant already exists"
exn_prop
end;
fun test_exc_no_cids thy _ =
let
val aT = TVar (("'a", 0), \<^sort>\<open>type\<close>)
val T =
(HOLogic.mk_setT aT --> HOLogic.boolT) -->
HOLogic.mk_setT aT -->
HOLogic.boolT
val implies_c = "HOL.implies"
val args : unoverload_definition_in_type =
((Binding.empty, NoSyn), (implies_c, T), thy)
val err_msg = mk_msg_unoverload_definition_error
"no suitable constant-instance definitions"
val exn_prop = Prop.expect_failure (ERROR err_msg) unoverload_definition
in
check_list_unit
show_unoverload_definition_in
[args]
"no suitable CIs"
exn_prop
end;
(**** Test Suite ****)
fun test_suite ctxt s =
let val thy = Proof_Context.theory_of ctxt
in
[
test_eq_trivial,
test_eq_nontrivial,
test_exc_extra_type_variables,
test_exc_ud_ex,
test_exc_no_cids
]
|> map (fn f => f thy s)
|> Lecker.test_group ctxt s
end;
end;
\ No newline at end of file
diff --git a/thys/Conditional_Transfer_Rule/UD/Tests/UD_Tests.thy b/thys/Conditional_Transfer_Rule/UD/Tests/UD_Tests.thy
--- a/thys/Conditional_Transfer_Rule/UD/Tests/UD_Tests.thy
+++ b/thys/Conditional_Transfer_Rule/UD/Tests/UD_Tests.thy
@@ -1,53 +1,52 @@
(* Title: UD/Tests/UD_Tests.thy
Author: Mihails Milehins
Copyright 2021 (C) Mihails Milehins
A test suite for the framework UD.
*)
section\<open>Test suite for UD\<close>
theory UD_Tests
imports
"../UD"
"../../IML_UT/IML_UT"
- SpecCheck.SpecCheck_Dynamic
Complex_Main
begin
subsection\<open>Background\<close>
(*
The following two definitions were copied from
HOL-Analysis.Elementary_Topology with minor amendments
to avoid unnecessary dependencies
*)
definition (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool"
where "islimpt x S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
definition closure :: "('a::topological_space) set \<Rightarrow> 'a set"
where "closure S = S \<union> {x. islimpt x S}"
ud \<open>topological_space.closed\<close>
ud \<open>islimpt\<close>
lemma closed_with: "closed \<equiv> closed.with open"
unfolding closed_def closed.with_def .
definition closure_with :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"
where "closure_with \<tau> \<equiv> \<lambda>S. S \<union> {x. islimpt.with \<tau> x S}"
lemma closure_with: "closure \<equiv> closure_with open"
unfolding closure_def islimpt.with closure_with_def .
subsection\<open>Tests\<close>
ML_file\<open>UD_TEST_UNOVERLOAD_DEFINITION.ML\<close>
ML\<open>
Lecker.test_group @{context} () [ud_test_unoverload_definition.test_suite]
\<close>
end
\ No newline at end of file
diff --git a/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_AMEND_CTXT_DATA.ML b/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_AMEND_CTXT_DATA.ML
--- a/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_AMEND_CTXT_DATA.ML
+++ b/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_AMEND_CTXT_DATA.ML
@@ -1,541 +1,543 @@
(* Title: ETTS/Tests/ETTS_TEST_AMEND_CTXT_DATA.ML
Author: Mihails Milehins
Copyright 2021 (C) Mihails Milehins
*)
signature ETTS_TEST_AMEND_CTXT_DATA =
sig
val test_suite : Proof.context -> unit -> unit
end;
structure etts_test_amend_ctxt_data : ETTS_TEST_AMEND_CTXT_DATA =
struct
(**** Background ****)
open SpecCheck;
structure Prop = SpecCheck_Property;
structure Show = SpecCheck_Show;
(**** Auxiliary ****)
fun mk_msg_tts_ctxt_error msg = "tts_context: " ^ msg
(*
approximate comparison of Token.src values: should not be made public
and should be used with great care
*)
local
val eq_eps_src_msg = "eq_eps_src: comparison is not possible"
in
fun eq_eps_src (src, src') =
let
val eq_name = Token.name_of_src src = Token.name_of_src src'
val eq_args = Token.args_of_src src ~~ Token.args_of_src src'
|> map eq_eps_token
|> List.all I
in eq_name andalso eq_args end
and eq_eps_token (token : Token.T, token' : Token.T) =
let
val eq_kind = Token.kind_of token = Token.kind_of token'
val eq_content = Token.content_of token = Token.content_of token'
val eq_source = Token.source_of token = Token.source_of token'
val eq_range =
Input.range_of (Token.input_of token) =
Input.range_of (Token.input_of token')
val eq_slot = (Token.get_value token, Token.get_value token')
|> eq_option eq_eps_value
in
eq_kind
andalso eq_content
andalso eq_source
andalso eq_range
andalso eq_slot
end
and eq_eps_value (Token.Source src, Token.Source src') = eq_eps_src (src, src')
| eq_eps_value (Token.Literal ltrl, Token.Literal ltrl') = ltrl = ltrl'
| eq_eps_value (Token.Name _, Token.Name _) = error eq_eps_src_msg
| eq_eps_value (Token.Typ T, Token.Typ T') = T = T'
| eq_eps_value (Token.Term t, Token.Term t') = t = t'
| eq_eps_value (Token.Fact (c_opt, thms), Token.Fact (c_opt', thms')) =
let
val eq_c = c_opt = c_opt'
val eq_thms = eq_list Thm.eq_thm (thms, thms')
in eq_c andalso eq_thms end
| eq_eps_value (Token.Attribute _, Token.Attribute _) =
error eq_eps_src_msg
| eq_eps_value (Token.Declaration _, Token.Declaration _) =
error eq_eps_src_msg
| eq_eps_value (Token.Files _, Token.Files _) =
error eq_eps_src_msg;
end;
(*
approximate comparison of ctxt_def_type: should not be made public
and used with great care
*)
fun eq_tts_ctxt_data
(
ctxt_data : ETTS_Context.ctxt_def_type,
ctxt_data' : ETTS_Context.ctxt_def_type
) =
let
fun eq_subst_thm (rsrc, rsrc') = fst rsrc = fst rsrc'
andalso eq_list eq_eps_src (snd rsrc, snd rsrc')
val _ = (#mpespc_opt ctxt_data, #mpespc_opt ctxt_data')
|> apply2 is_none
|> (fn (x, y) => x = true andalso y = true)
orelse error "eq_tts_ctxt_data: comparison is not possible"
val eq_rispec = #rispec ctxt_data = #rispec ctxt_data'
val eq_sbtspec = #sbtspec ctxt_data = #sbtspec ctxt_data'
val eq_subst_thms =
eq_list eq_subst_thm (#subst_thms ctxt_data, #subst_thms ctxt_data')
val eq_sbrr_opt = (#sbrr_opt ctxt_data, #sbrr_opt ctxt_data')
|> eq_option eq_subst_thm
val eq_attrbs = eq_list eq_eps_src (#attrbs ctxt_data, #attrbs ctxt_data')
in
eq_rispec
andalso eq_sbtspec
andalso eq_subst_thms
andalso eq_sbrr_opt
andalso eq_attrbs
end;
(**** Visualization ****)
+(*FIXME: complete the migration to SpecCheck.Show*)
+
fun show_amend_context_in (args, ctxt) =
let
val c =
"ctxt : unknown context\n" ^
ETTS_Context.string_of_amend_context_data_args ctxt args
in Pretty.str c end;
fun show_amend_context_out (ctxt_data, ctxt) =
Pretty.str (ETTS_Context.string_of_tts_ctxt_data ctxt ctxt_data)
val show_amend_context = Show.zip show_amend_context_in show_amend_context_out
(**** Tests ****)
(*** Wrapper ***)
val test_amend_context_data = uncurry ETTS_Context.amend_context_data;
(*** Valid inputs ***)
fun test_eq_tts_context (ctxt : Proof.context) _ =
let
(*input*)
val risstv1_c = "?'a"
val U1_c = "UA::'ao set"
val risstv2_c = "?'b"
val U2_c = "UB::'bo set"
val rispec = [(risstv1_c, U1_c), (risstv2_c, U2_c)]
val tbt_1 = "(\<le>)::?'a::ord\<Rightarrow>?'a::ord\<Rightarrow>bool"
val sbt_1 = "(\<le>\<^sub>o\<^sub>w)"
val tbt_2 = "(<)::?'b::ord\<Rightarrow>?'b::ord\<Rightarrow>bool"
val sbt_2 = "(<\<^sub>o\<^sub>w)"
val sbtspec = [(tbt_1, sbt_1), (tbt_2, sbt_2)]
val args : ETTS_Context.amend_ctxt_data_input_type =
(((((rispec, sbtspec), NONE), []), NONE), [])
(*output*)
val s_a_ix : indexname = ("'a", 0)
val s_a_T = TVar (s_a_ix, \<^sort>\<open>ord\<close>)
val aT = TFree ("'ao", \<^sort>\<open>type\<close>)
val U1 = Free ("UA", HOLogic.mk_setT aT)
val s_b_ix : indexname = ("'b", 0)
val s_b_T = TVar (s_b_ix, \<^sort>\<open>ord\<close>)
val bT = TFree ("'bo", \<^sort>\<open>type\<close>)
val U2 = Free ("UB", HOLogic.mk_setT bT)
val less_eqt =
Const (\<^const_name>\<open>less_eq\<close>, s_a_T --> s_a_T --> HOLogic.boolT)
val lesst =
Const (\<^const_name>\<open>less\<close>, s_b_T --> s_b_T --> HOLogic.boolT)
val leqt = Free ("le", aT --> aT --> HOLogic.boolT)
val lst = Free ("ls", bT --> bT --> HOLogic.boolT)
val rispec = [(s_a_ix, U1), (s_b_ix, U2)]
val sbtspec = [(less_eqt, leqt), (lesst, lst)]
val subst_thms = []
val sbrr_opt = NONE
val mpespc_opt = NONE
val attrbs = []
val tts_ctxt_data_out : ETTS_Context.ctxt_def_type =
{
rispec = rispec,
sbtspec = sbtspec,
subst_thms = subst_thms,
sbrr_opt = sbrr_opt,
mpespc_opt = mpespc_opt,
attrbs = attrbs
}
in
check_list_unit
show_amend_context
[((args, ctxt), (tts_ctxt_data_out, ctxt))]
"equality"
(
Prop.prop
(
fn (val_in, val_out) =>
eq_fst eq_tts_ctxt_data (test_amend_context_data val_in, val_out)
)
)
end;
(*** Exceptions ***)
(** General **)
fun test_exc_tts_context_tts_context thy _ =
let
val ctxt = Proof_Context.init_global thy;
val risstv1_c = "?'a"
val U1_c = "U1::'a set"
val rispec1 = [(risstv1_c, U1_c)]
val args1 : ETTS_Context.amend_ctxt_data_input_type =
(((((rispec1, []), NONE), []), NONE), [])
val ctxt' = ETTS_Context.amend_context_data args1 ctxt |> snd
val risstv2_c = "?'b"
val U2_c = "U2::'b set"
val rispec2 = [(risstv2_c, U2_c)]
val args2 : ETTS_Context.amend_ctxt_data_input_type =
(((((rispec2, []), NONE), []), NONE), [])
val err_msg = mk_msg_tts_ctxt_error "nested tts contexts"
val exn_prop = Prop.expect_failure (ERROR err_msg) test_amend_context_data
in
check_list_unit
(show_amend_context_in)
[(args2, ctxt')]
"nested tts contexts"
exn_prop
end;
(** tts **)
fun test_exc_rispec_empty thy _ =
let
val ctxt = Proof_Context.init_global thy;
val args = ((((([], []), NONE), []), NONE), [])
val err_msg = mk_msg_tts_ctxt_error "rispec must not be empty"
val exn_prop = Prop.expect_failure (ERROR err_msg) test_amend_context_data
in
check_list_unit
(show_amend_context_in)
[(args, ctxt)]
"rispec empty"
exn_prop
end;
fun test_exc_rispec_not_set thy _ =
let
val ctxt = Proof_Context.init_global thy;
val risstv1_c = "?'a"
val U1_c = "U1::('b list) set"
val risstv2_c = "?'b"
val U2_c = "U2::'a set"
val rispec = [(risstv1_c, U1_c), (risstv2_c, U2_c)]
val args = (((((rispec, []), NONE), []), NONE), [])
val err_msg = mk_msg_tts_ctxt_error
"risset must be terms of the type of the form ?'a set or 'a set"
val exn_prop = Prop.expect_failure (ERROR err_msg) test_amend_context_data
in
check_list_unit
(show_amend_context_in)
[(args, ctxt)]
"risset are not all sets"
exn_prop
end;
fun test_exc_rispec_duplicate_risstvs thy _ =
let
val ctxt = Proof_Context.init_global thy;
val risstv1_c = "?'a"
val U1_c = "U1::'a set"
val risstv2_c = "?'b"
val U2_c = "U2::'b set"
val risstv3_c = "?'a"
val U3_c = "U3::'c set"
val rispec = [(risstv1_c, U1_c), (risstv2_c, U2_c), (risstv3_c, U3_c)]
val args = (((((rispec, []), NONE), []), NONE), [])
val err_msg = "tts_context: risstvs must be distinct"
val exn_prop = Prop.expect_failure (ERROR err_msg) test_amend_context_data
in
check_list_unit
(show_amend_context_in)
[(args, ctxt)]
"duplicate risstvs"
exn_prop
end;
fun test_exc_rispec_not_ds_dtv thy _ =
let
val ctxt = Proof_Context.init_global thy;
val risstv1_c = "?'a"
val U1_c = "U1::'a set"
val risstv2_c = "?'b"
val U2_c = "U2::'b::{group_add, finite} set"
val risstv3_c = "?'c"
val U3_c = "U3::'c::{group_add, order} set"
val risstv4_c = "?'d"
val U4_c = "U4::'b::{group_add, order} set"
val rispec =
[(risstv1_c, U1_c), (risstv2_c, U2_c), (risstv3_c, U3_c), (risstv4_c, U4_c)]
val args = (((((rispec, []), NONE), []), NONE), [])
val err_msg =
"tts_context: risset: type variables with distinct sorts must be distinct"
val exn_prop = Prop.expect_failure (ERROR err_msg) test_amend_context_data
in
check_list_unit
(show_amend_context_in)
[(args, ctxt)]
"not distinct sorts \<longrightarrow> distinct types variables"
exn_prop
end;
fun test_exc_rispec_not_dt_dv thy _ =
let
val ctxt = Proof_Context.init_global thy;
val risstv1_c = "?'a"
val U1_c = "U1::'a set"
val risstv2_c = "?'b"
val U2_c = "U2::'b::{group_add, finite} set"
val risstv3_c = "?'c"
val U3_c = "U3::'c::{group_add, order} set"
val risstv4_c = "?'d"
val U4_c = "U2::'c::{group_add, order} set"
val rispec =
[
(risstv1_c, U1_c),
(risstv2_c, U2_c),
(risstv3_c, U3_c),
(risstv4_c, U4_c)
]
val args = (((((rispec, []), NONE), []), NONE), [])
val err_msg =
"tts_context: risset: variables with distinct types must be distinct"
val exn_prop = Prop.expect_failure (ERROR err_msg) test_amend_context_data
in
check_list_unit
(show_amend_context_in)
[(args, ctxt)]
"not distinct types \<longrightarrow> distinct variables"
exn_prop
end;
(** sbterms **)
fun test_exc_distinct_sorts ctxt _ =
let
val risstv1_c = "?'a"
val U1_c = "UA::'ao set"
val risstv2_c = "?'b"
val U2_c = "UB::'bo set"
val rispec = [(risstv1_c, U1_c), (risstv2_c, U2_c)]
val tbt_1 = "(<)::?'a::ord\<Rightarrow>?'a::ord\<Rightarrow>bool"
val sbt_1 = "(<\<^sub>o\<^sub>w)"
val tbt_2 = "?a::?'a::order\<Rightarrow>?'a::order\<Rightarrow>bool"
val sbt_2 = "f"
val sbtspec = [(tbt_1, sbt_1), (tbt_2, sbt_2)]
val args = (((((rispec, sbtspec), NONE), []), NONE), [])
val err_msg = mk_msg_tts_ctxt_error
"tbts: a single stv should not have two distinct sorts associated with it"
val exn_prop = Prop.expect_failure (ERROR err_msg) test_amend_context_data
in
check_list_unit
(show_amend_context_in)
[(args, ctxt)]
"tbts: an stv with distinct sorts"
exn_prop
end;
fun test_exc_sbts_no_tis ctxt _ =
let
val risstv1_c = "?'a"
val U1_c = "UA::'ao set"
val risstv2_c = "?'b"
val U2_c = "UB::'bo set"
val rispec = [(risstv1_c, U1_c), (risstv2_c, U2_c)]
val tbt_1 = "(<)::?'a::ord\<Rightarrow>?'a::ord\<Rightarrow>bool"
val sbt_1 = "(<\<^sub>o\<^sub>w)"
val tbt_2 = "(\<le>)::?'a::ord\<Rightarrow>?'a::ord\<Rightarrow>bool"
val sbt_2 = "(\<le>\<^sub>o\<^sub>w)"
val sbtspec = [(tbt_1, sbt_1), (tbt_2, sbt_2)]
val args = (((((rispec, sbtspec), NONE), []), NONE), [])
val err_msg = mk_msg_tts_ctxt_error
"\n\t-the types of the sbts must be equivalent " ^
"to the types of the tbts up to renaming of the type variables\n" ^
"\t-to each type variable that occurs among the tbts must correspond " ^
"exactly one type variable among all type " ^
"variables that occur among all of the sbts"
val exn_prop = Prop.expect_failure (ERROR err_msg) test_amend_context_data
in
check_list_unit
(show_amend_context_in)
[(args, ctxt)]
"sbts are not type instances of tbts"
exn_prop
end;
fun test_exc_tbt_fixed ctxt _ =
let
val risstv1_c = "?'a"
val U1_c = "UA::'ao set"
val risstv2_c = "?'b"
val U2_c = "UB::'bo set"
val rispec = [(risstv1_c, U1_c), (risstv2_c, U2_c)]
val tbt_1 = "(<)::?'a::ord\<Rightarrow>?'a::ord\<Rightarrow>bool"
val sbt_1 = "(<\<^sub>o\<^sub>w)"
val tbt_2 = "g::?'a::ord\<Rightarrow>?'a::ord\<Rightarrow>bool"
val sbt_2 = "(<\<^sub>o\<^sub>w)"
val sbtspec = [(tbt_1, sbt_1), (tbt_2, sbt_2)]
val args = (((((rispec, sbtspec), NONE), []), NONE), [])
val err_msg = mk_msg_tts_ctxt_error
"tbts must consist of constants and schematic variables"
val exn_prop = Prop.expect_failure (ERROR err_msg) test_amend_context_data
in
check_list_unit
(show_amend_context_in)
[(args, ctxt)]
"tbts are not constants and schematic variables"
exn_prop
end;
fun test_exc_sbts_not_registered ctxt _ =
let
val risstv1_c = "?'a"
val U1_c = "UA::'ao set"
val risstv2_c = "?'b"
val U2_c = "UB::'bo set"
val rispec = [(risstv1_c, U1_c), (risstv2_c, U2_c)]
val tbt_1 = "(<)::?'a::ord\<Rightarrow>?'a::ord\<Rightarrow>bool"
val sbt_1 = "(<\<^sub>o\<^sub>w)"
val tbt_2 = "(\<le>)::?'a::ord\<Rightarrow>?'a::ord\<Rightarrow>bool"
val sbt_2 = "g::'bo::type\<Rightarrow>'bo::type\<Rightarrow>bool"
val sbtspec = [(tbt_1, sbt_1), (tbt_2, sbt_2)]
val args = (((((rispec, sbtspec), NONE), []), NONE), [])
val err_msg = mk_msg_tts_ctxt_error
"sbts must be registered using the command tts_register_sbts"
val exn_prop = Prop.expect_failure (ERROR err_msg) test_amend_context_data
in
check_list_unit
(show_amend_context_in)
[(args, ctxt)]
"sbts must be registered"
exn_prop
end;
fun test_exc_tbts_not_distinct ctxt _ =
let
val risstv1_c = "?'a"
val U1_c = "UA::'ao set"
val risstv2_c = "?'b"
val U2_c = "UB::'bo set"
val rispec = [(risstv1_c, U1_c), (risstv2_c, U2_c)]
val tbt_1 = "(\<le>)::?'a::ord\<Rightarrow>?'a::ord\<Rightarrow>bool"
val sbt_1 = "(<\<^sub>o\<^sub>w)"
val tbt_2 = "(\<le>)::?'a::ord\<Rightarrow>?'a::ord\<Rightarrow>bool"
val sbt_2 = "(<\<^sub>o\<^sub>w)"
val sbtspec = [(tbt_1, sbt_1), (tbt_2, sbt_2)]
val args = (((((rispec, sbtspec), NONE), []), NONE), [])
val err_msg = mk_msg_tts_ctxt_error "tbts must be distinct"
val exn_prop = Prop.expect_failure (ERROR err_msg) test_amend_context_data
in
check_list_unit
(show_amend_context_in)
[(args, ctxt)]
"tbts must be distinct"
exn_prop
end;
fun test_exc_sbterms_subset_rispec (ctxt : Proof.context) _ =
let
(* input *)
val risstv1_c = "?'a"
val U1_c = "UA::'ao set"
val rispec = [(risstv1_c, U1_c)]
val tbt_1 = "(\<le>)::?'a::ord\<Rightarrow>?'a::ord\<Rightarrow>bool"
val sbt_1 = "(\<le>\<^sub>o\<^sub>w)"
val tbt_2 = "(<)::?'b::ord\<Rightarrow>?'b::ord\<Rightarrow>bool"
val sbt_2 = "(<\<^sub>o\<^sub>w)"
val sbtspec = [(tbt_1, sbt_1), (tbt_2, sbt_2)]
val args : ETTS_Context.amend_ctxt_data_input_type =
(((((rispec, sbtspec), NONE), []), NONE), [])
val err_msg = mk_msg_tts_ctxt_error
"the collection of the (stv, ftv) pairs associated with the sbterms " ^
"must form a subset of the collection of the (stv, ftv) pairs " ^
"associated with the RI specification, provided that only the pairs " ^
"(stv, ftv) associated with the sbterms such that ftv occurs in a " ^
"premise of a theorem associated with an sbterm are taken into account"
val exn_prop = Prop.expect_failure (ERROR err_msg) test_amend_context_data
in
check_list_unit
(show_amend_context_in)
[(args, ctxt)]
"stv-ftv subset"
exn_prop
end;
(**** Test Suite ****)
fun test_suite ctxt s =
let val thy = Proof_Context.theory_of ctxt
in
[
test_eq_tts_context ctxt s,
test_exc_tts_context_tts_context thy s,
test_exc_rispec_empty thy s,
test_exc_rispec_not_set thy s,
test_exc_rispec_duplicate_risstvs thy s,
test_exc_rispec_not_ds_dtv thy s,
test_exc_rispec_not_dt_dv thy s,
test_exc_distinct_sorts ctxt s,
test_exc_sbts_no_tis ctxt s,
test_exc_tbt_fixed ctxt s,
test_exc_sbts_not_registered ctxt s,
test_exc_tbts_not_distinct ctxt s,
test_exc_sbterms_subset_rispec ctxt s
]
|> Lecker.test_group ctxt s
end;
end;
\ No newline at end of file
diff --git a/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_TTS_ALGORITHM.ML b/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_TTS_ALGORITHM.ML
--- a/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_TTS_ALGORITHM.ML
+++ b/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_TTS_ALGORITHM.ML
@@ -1,410 +1,412 @@
(* Title: ETTS/Tests/ETTS_TEST_TTS_ALGORITHM.ML
Author: Mihails Milehins
Copyright 2021 (C) Mihails Milehins
*)
signature ETTS_TEST_TTS_ALGORITHM =
sig
type tts_algorithm_in_type
val test_suite : Proof.context -> unit -> unit
end;
structure etts_test_tts_algorithm : ETTS_TEST_TTS_ALGORITHM =
struct
(**** Background ****)
open SpecCheck;
structure Prop = SpecCheck_Property;
structure Show = SpecCheck_Show;
(**** Auxiliary ****)
fun mk_msg_tts_algorithm_error msg = "tts_algorithm: " ^ msg
(*** Data ***)
type tts_algorithm_in_type =
Proof.context *
ETTS_Algorithm.etts_output_type *
int list *
(indexname * term) list *
(term * term) list *
(Facts.ref * Token.src list) option *
(Facts.ref * Token.src list) list *
(term list * (Proof.context -> tactic)) option *
Token.src list *
thm;
(*** String I/O ***)
fun string_of_writer writer = writer
|> ML_Syntax.print_list Int.toString
|> curry op^ "writer: "
(*** Relation for the outputs ***)
fun rel_tts_algorithm_out
(
act_out : (thm * int list) * Proof.context,
exp_out : (thm * int list) * Proof.context
) =
let
val ((thm_act_out, writer_act_out), _) = act_out
val ((thm_exp_out, writer_exp_out), _) = exp_out
val t_act_out = Thm.full_prop_of thm_act_out
val t_exp_out = Thm.full_prop_of thm_exp_out
in
t_act_out aconv t_exp_out
andalso writer_act_out = writer_exp_out
end;
(**** Visualization ****)
+(*FIXME: complete the migration to SpecCheck.Show*)
+
fun string_of_rispec ctxt =
ML_Syntax.print_pair (Term.string_of_vname) (Syntax.string_of_term ctxt)
|> ML_Syntax.print_list;
fun string_of_sbtspec ctxt =
let val string_of_term = Syntax.string_of_term ctxt
in
ML_Syntax.print_pair string_of_term string_of_term
|> ML_Syntax.print_list
end;
fun show_tts_algorithm_in (tts_algorithm_in : tts_algorithm_in_type) =
let
val
(
ctxt,
tts_output_type,
writer,
rispec,
sbtspec,
sbrr_opt,
subst_thms,
mpespc_opt,
attrbs,
thm
) = tts_algorithm_in
val ctxt_c = "ctxt: unknown context"
val tts_output_type_c =
ETTS_Algorithm.string_of_etts_output_type tts_output_type
val writer_c = string_of_writer writer
val rispec_c = rispec |> string_of_rispec ctxt |> curry op^ "rispec: "
val sbtspec_c = sbtspec |> string_of_sbtspec ctxt |> curry op^ "sbtspec: "
val sbrr_opt_c = sbrr_opt
|> ETTS_Context.string_of_sbrr_opt
|> curry op^ "sbrr_opt: "
val subst_thms_c = subst_thms
|> ETTS_Context.string_of_subst_thms
|> curry op^ "subst_thms: "
val mpespc_opt_c = mpespc_opt
|> ETTS_Context.string_of_mpespc_opt ctxt
|> curry op^ "mpespc_opt: "
val attrbs_c = attrbs |> string_of_token_src_list |> curry op^ "attrbs: "
val thm_c = thm |> Thm.string_of_thm ctxt |> curry op^ "in_thm: "
val out_c =
[
ctxt_c,
tts_output_type_c,
writer_c,
rispec_c,
sbtspec_c,
sbrr_opt_c,
subst_thms_c,
mpespc_opt_c,
attrbs_c,
thm_c
]
|> String.concatWith "\n"
in Pretty.str out_c end;
fun show_tts_algorithm_out
(((thm, writer), ctxt) : (thm * int list) * Proof.context) =
let
val ctxt_c = "ctxt: unknown context"
val thm_c = Thm.string_of_thm ctxt thm
val writer_c = ML_Syntax.print_list Int.toString writer
val out_c = [ctxt_c, thm_c, writer_c] |> String.concatWith "\n"
in Pretty.str out_c end;
val show_tts_algorithm = Show.zip show_tts_algorithm_in show_tts_algorithm_out
(**** Tests ****)
(*** Wrapper ***)
fun tts_algorithm (tts_algorithm_in : tts_algorithm_in_type) =
let
val
(
ctxt,
tts_output_type,
writer,
rispec,
sbtspec,
sbrr_opt,
subst_thms,
mpespc_opt,
attrbs,
thm
) = tts_algorithm_in
val tts_algorithm_out =
ETTS_Algorithm.etts_algorithm
ctxt
tts_output_type
writer
rispec
sbtspec
sbrr_opt
subst_thms
mpespc_opt
attrbs
thm
in tts_algorithm_out end;
(*** Valid inputs ***)
fun test_eq_tts_algorithm (ctxt : Proof.context) _ =
let
(*input*)
val tts_ctxt_data = ETTS_Context.get_tts_ctxt_data ctxt
val rispec = #rispec tts_ctxt_data
val sbtspec = #sbtspec tts_ctxt_data
val sbrr_opt = #sbrr_opt tts_ctxt_data
val subst_thms = #subst_thms tts_ctxt_data
val mpespc_opt = #mpespc_opt tts_ctxt_data
val attrbs = #attrbs tts_ctxt_data
val tts_output_type = ETTS_Algorithm.default
val writer_in = [1, 1, 1, 1]
val in_thm = @{thm tta_semigroup_hom.tta_left_ideal_closed}
val tts_algorithm_in : tts_algorithm_in_type =
(
ctxt,
tts_output_type,
writer_in,
rispec,
sbtspec,
sbrr_opt,
subst_thms,
mpespc_opt,
attrbs,
in_thm
)
(*output*)
val writer_out = [1, 3, 1, 1]
val exp_tts_algorithm_out =
((@{thm tta_left_ideal_ow_closed}, writer_out), ctxt)
in
check_list_unit
show_tts_algorithm
[(tts_algorithm_in, exp_tts_algorithm_out)]
"equality"
(
Prop.prop
(
fn (val_in, val_out) =>
rel_tts_algorithm_out (tts_algorithm val_in, val_out)
)
)
end;
(*** Exceptions ***)
fun test_exc_ftvs ctxt _ =
let
val tts_ctxt_data = ETTS_Context.get_tts_ctxt_data ctxt
val rispec = #rispec tts_ctxt_data
val sbtspec = #sbtspec tts_ctxt_data
val sbrr_opt = #sbrr_opt tts_ctxt_data
val subst_thms = #subst_thms tts_ctxt_data
val mpespc_opt = #mpespc_opt tts_ctxt_data
val attrbs = #attrbs tts_ctxt_data
val tts_output_type = ETTS_Algorithm.default
val writer_in = [1, 1, 1, 1]
val in_thm = @{thm exI'[where 'a='a]}
val tts_algorithm_in : tts_algorithm_in_type =
(
ctxt,
tts_output_type,
writer_in,
rispec,
sbtspec,
sbrr_opt,
subst_thms,
mpespc_opt,
attrbs,
in_thm
)
val err_msg = mk_msg_tts_algorithm_error
"fixed type variables must not occur in the type-based theorems"
val exn_prop = Prop.expect_failure (ERROR err_msg) tts_algorithm
in
check_list_unit
show_tts_algorithm_in
[tts_algorithm_in]
"fixed type variables"
exn_prop
end;
fun test_exc_fvs ctxt _ =
let
val tts_ctxt_data = ETTS_Context.get_tts_ctxt_data ctxt
val rispec = #rispec tts_ctxt_data
val sbtspec = #sbtspec tts_ctxt_data
val sbrr_opt = #sbrr_opt tts_ctxt_data
val subst_thms = #subst_thms tts_ctxt_data
val mpespc_opt = #mpespc_opt tts_ctxt_data
val attrbs = #attrbs tts_ctxt_data
val tts_output_type = ETTS_Algorithm.default
val writer_in = [1, 1, 1, 1]
val aT = TVar (("'a", 0), \<^sort>\<open>type\<close>)
val xv = ("x", 0)
val xt = Free ("x", aT) |> Thm.cterm_of ctxt
val in_thm = Drule.instantiate_normalize
(TVars.empty, Vars.make [((xv, aT), xt)]) @{thm exI'}
val tts_algorithm_in : tts_algorithm_in_type =
(
ctxt,
tts_output_type,
writer_in,
rispec,
sbtspec,
sbrr_opt,
subst_thms,
mpespc_opt,
attrbs,
in_thm
)
val err_msg = mk_msg_tts_algorithm_error
"fixed variables must not occur in the type-based theorems"
val exn_prop = Prop.expect_failure (ERROR err_msg) tts_algorithm
in
check_list_unit
show_tts_algorithm_in
[tts_algorithm_in]
"fixed variables"
exn_prop
end;
fun test_exc_not_risstv_subset ctxt _ =
let
val tts_ctxt_data = ETTS_Context.get_tts_ctxt_data ctxt
val rispec = #rispec tts_ctxt_data
val sbtspec = #sbtspec tts_ctxt_data
val sbrr_opt = #sbrr_opt tts_ctxt_data
val subst_thms = #subst_thms tts_ctxt_data
val mpespc_opt = #mpespc_opt tts_ctxt_data
val attrbs = #attrbs tts_ctxt_data
val tts_output_type = ETTS_Algorithm.default
val writer_in = [1, 1, 1, 1]
val in_thm = @{thm tta_semigroup.tta_assoc}
val tts_algorithm_in : tts_algorithm_in_type =
(
ctxt,
tts_output_type,
writer_in,
rispec,
sbtspec,
sbrr_opt,
subst_thms,
mpespc_opt,
attrbs,
in_thm
)
val err_msg = mk_msg_tts_algorithm_error
"risstv must be a subset of the schematic type " ^
"variables that occur in the type-based theorems"
val exn_prop = Prop.expect_failure (ERROR err_msg) tts_algorithm
in
check_list_unit
show_tts_algorithm_in
[tts_algorithm_in]
"risstv is not a subset of the stvs of the type-based theorems"
exn_prop
end;
fun test_not_tts_context thy _ =
let
val ctxt = Proof_Context.init_global thy
val tts_ctxt_data = ETTS_Context.get_tts_ctxt_data ctxt
val rispec = #rispec tts_ctxt_data
val sbtspec = #sbtspec tts_ctxt_data
val sbrr_opt = #sbrr_opt tts_ctxt_data
val subst_thms = #subst_thms tts_ctxt_data
val mpespc_opt = #mpespc_opt tts_ctxt_data
val attrbs = #attrbs tts_ctxt_data
val tts_output_type = ETTS_Algorithm.default
val writer_in = [1, 1, 1, 1]
val in_thm = @{thm tta_semigroup_hom.tta_left_ideal_closed}
val tts_algorithm_in : tts_algorithm_in_type =
(
ctxt,
tts_output_type,
writer_in,
rispec,
sbtspec,
sbrr_opt,
subst_thms,
mpespc_opt,
attrbs,
in_thm
)
val err_msg = mk_msg_tts_algorithm_error
"ERA can only be invoked from an appropriately parameterized tts context"
val exn_prop = Prop.expect_failure (ERROR err_msg) tts_algorithm
in
check_list_unit
show_tts_algorithm_in
[tts_algorithm_in]
"not tts context"
exn_prop
end;
(**** Test Suite ****)
fun test_suite ctxt s =
let val thy = Proof_Context.theory_of ctxt
in
[
test_eq_tts_algorithm ctxt s,
test_exc_ftvs ctxt s,
test_exc_fvs ctxt s,
test_exc_not_risstv_subset ctxt s,
test_not_tts_context thy s
]
|> Lecker.test_group ctxt s
end;
end;
\ No newline at end of file
diff --git a/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_TTS_REGISTER_SBTS.ML b/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_TTS_REGISTER_SBTS.ML
--- a/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_TTS_REGISTER_SBTS.ML
+++ b/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_TTS_REGISTER_SBTS.ML
@@ -1,127 +1,129 @@
(* Title: ETTS/Tests/ETTS_TEST_TTS_REGISTER_SBTS.ML
Author: Mihails Milehins
Copyright 2021 (C) Mihails Milehins
*)
signature ETTS_TEST_TTS_REGISTER_SBTS =
sig
type tts_register_sbts_in_type
val test_suite : Proof.context -> unit -> unit
end;
structure etts_test_tts_register_sbts : ETTS_TEST_TTS_REGISTER_SBTS =
struct
(**** Background ****)
open SpecCheck;
structure Prop = SpecCheck_Property;
structure Show = SpecCheck_Show;
(**** Auxiliary ****)
fun mk_msg_tts_register_sbts_error msg = "tts_register_sbts: " ^ msg
(*** Data ***)
type tts_register_sbts_in_type =
(string * string list) * Proof.context
(**** Visualization ****)
+(*FIXME: complete the migration to SpecCheck.Show*)
+
fun show_tts_register_sbts_in
(tts_register_sbts_in : tts_register_sbts_in_type) =
let
val ((sbt, risset), _) = tts_register_sbts_in
val ctxt_c = "ctxt: unknown context"
val sbt_c = "sbt: " ^ sbt
val risset_c = "risset: " ^ ML_Syntax.print_list I risset
val out_c = [ctxt_c, sbt_c, risset_c] |> String.concatWith "\n"
in Pretty.str out_c end;
(**** Tests ****)
(*** Wrapper ***)
fun tts_register_sbts ((args, ctxt) : tts_register_sbts_in_type) =
ETTS_Substitution.process_tts_register_sbts args ctxt;
(*** Exceptions ***)
fun test_exc_fvs ctxt _ =
let
val sbt = "g::'q"
val UA_c = "UA::'a set"
val UB_c = "UB::'b set"
val rissest = [UA_c, UB_c]
val tts_register_sbts_in : tts_register_sbts_in_type =
((sbt, rissest), ctxt)
val err_msg = mk_msg_tts_register_sbts_error
"all fixed variables that occur in the sbterm " ^
"must be fixed in the context"
val exn_prop = Prop.expect_failure (ERROR err_msg) tts_register_sbts
in
check_list_unit
(show_tts_register_sbts_in)
[tts_register_sbts_in]
"variables not fixed in the context"
exn_prop
end;
fun test_exc_repeated_risset ctxt _ =
let
val sbt = "f"
val UA_c = "UA::'a set"
val UB_c = "UA::'a set"
val rissest = [UA_c, UB_c]
val tts_register_sbts_in : tts_register_sbts_in_type =
((sbt, rissest), ctxt)
val err_msg = mk_msg_tts_register_sbts_error
"the type variables associated with the risset must be distinct"
val exn_prop = Prop.expect_failure (ERROR err_msg) tts_register_sbts
in
check_list_unit
show_tts_register_sbts_in
[tts_register_sbts_in]
"repeated risset"
exn_prop
end;
(**** Test Suite ****)
fun test_suite ctxt s = [test_exc_fvs ctxt s, test_exc_repeated_risset ctxt s]
|> Lecker.test_group ctxt s;
end;
\ No newline at end of file
diff --git a/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_Tests.thy b/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_Tests.thy
--- a/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_Tests.thy
+++ b/thys/Types_To_Sets_Extension/ETTS/Tests/ETTS_Tests.thy
@@ -1,366 +1,365 @@
(* Title: ETTS/Tests/ETTS_Tests.thy
Author: Mihails Milehins
Copyright 2021 (C) Mihails Milehins
A test suite for the ETTS.
*)
section\<open>A test suite for ETTS\<close>
theory ETTS_Tests
imports
"../ETTS_Auxiliary"
Conditional_Transfer_Rule.IML_UT
- SpecCheck.SpecCheck_Dynamic
begin
subsection\<open>\<open>amend_ctxt_data\<close>\<close>
ML_file\<open>ETTS_TEST_AMEND_CTXT_DATA.ML\<close>
locale test_amend_ctxt_data =
fixes UA :: "'ao set" and UB :: "'bo set" and UC :: "'co set"
and le :: "['ao, 'ao] \<Rightarrow> bool" (infix \<open>\<le>\<^sub>o\<^sub>w\<close> 50)
and ls :: "['bo, 'bo] \<Rightarrow> bool" (infix \<open><\<^sub>o\<^sub>w\<close> 50)
and f :: "['ao, 'bo] \<Rightarrow> 'co"
assumes closed_f: "\<lbrakk> a \<in> UA; b \<in> UB \<rbrakk> \<Longrightarrow> f a b \<in> UC"
begin
notation le (\<open>'(\<le>\<^sub>o\<^sub>w')\<close>)
and le (infix \<open>\<le>\<^sub>o\<^sub>w\<close> 50)
and ls (\<open>'(<\<^sub>o\<^sub>w')\<close>)
and ls (infix \<open><\<^sub>o\<^sub>w\<close> 50)
tts_register_sbts \<open>(\<le>\<^sub>o\<^sub>w)\<close> | UA
proof-
assume "Domainp AOA = (\<lambda>x. x \<in> UA)" "bi_unique AOA" "right_total AOA"
from tts_AA_eq_transfer[OF this] show ?thesis by auto
qed
tts_register_sbts \<open>(<\<^sub>o\<^sub>w)\<close> | UB
proof-
assume "Domainp BOA = (\<lambda>x. x \<in> UB)" "bi_unique BOA" "right_total BOA"
from tts_AA_eq_transfer[OF this] show ?thesis by auto
qed
tts_register_sbts f | UA and UB and UC
proof-
assume
"Domainp AOC = (\<lambda>x. x \<in> UA)" "bi_unique AOC" "right_total AOC"
"Domainp BOB = (\<lambda>x. x \<in> UB)" "bi_unique BOB" "right_total BOB"
"Domainp COA = (\<lambda>x. x \<in> UC)" "bi_unique COA" "right_total COA"
from tts_AB_C_transfer[OF closed_f this] show ?thesis by auto
qed
end
context test_amend_ctxt_data
begin
ML\<open>
Lecker.test_group @{context} () [etts_test_amend_ctxt_data.test_suite]
\<close>
end
subsection\<open>\<open>tts_algorithm\<close>\<close>
text\<open>
Some of the elements of the content of this section are based on the
elements of the content of \cite{cain_nine_2019}.
\<close>
(*the following theorem is restated for forward compatibility*)
lemma exI': "P x \<Longrightarrow> \<exists>x. P x" by auto
class tta_mult =
fixes tta_mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*\<^sub>t\<^sub>t\<^sub>a" 65)
class tta_semigroup = tta_mult +
assumes tta_assoc[simp]: "(a *\<^sub>t\<^sub>t\<^sub>a b) *\<^sub>t\<^sub>t\<^sub>a c = a *\<^sub>t\<^sub>t\<^sub>a (b *\<^sub>t\<^sub>t\<^sub>a c)"
definition set_mult :: "'a::tta_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "\<^bold>*\<^sub>t\<^sub>t\<^sub>a" 65)
where "set_mult S T = {s *\<^sub>t\<^sub>t\<^sub>a t | s t. s \<in> S \<and> t \<in> T}"
definition left_ideal :: "'a::tta_mult set \<Rightarrow> bool"
where "left_ideal T \<longleftrightarrow> (\<forall>s. \<forall>t\<in>T. s *\<^sub>t\<^sub>t\<^sub>a t \<in> T)"
lemma left_idealI[intro]:
assumes "\<And>s t. t \<in> T \<Longrightarrow> s *\<^sub>t\<^sub>t\<^sub>a t \<in> T"
shows "left_ideal T"
using assms unfolding left_ideal_def by simp
lemma left_idealE[elim]:
assumes "left_ideal T"
obtains "\<And>s t. t \<in> T \<Longrightarrow> s *\<^sub>t\<^sub>t\<^sub>a t \<in> T"
using assms unfolding left_ideal_def by simp
lemma left_ideal_set_mult_iff: "left_ideal T \<longleftrightarrow> UNIV \<^bold>*\<^sub>t\<^sub>t\<^sub>a T \<subseteq> T"
unfolding left_ideal_def set_mult_def by auto
ud \<open>set_mult\<close>
ud \<open>left_ideal\<close>
ctr relativization
synthesis ctr_simps
assumes [transfer_domain_rule]: "Domainp A = (\<lambda>x. x \<in> U)"
and [transfer_rule]: "bi_unique A" "right_total A"
trp (?'a A)
in set_mult_ow: set_mult.with_def
and left_ideal_ow: left_ideal.with_def
locale tta_semigroup_hom =
fixes f :: "'a::tta_semigroup \<Rightarrow> 'b::tta_semigroup"
assumes hom: "f (a *\<^sub>t\<^sub>t\<^sub>a b) = f a *\<^sub>t\<^sub>t\<^sub>a f b"
context tta_semigroup_hom
begin
lemma tta_left_ideal_closed:
assumes "left_ideal T" and "surj f"
shows "left_ideal (f ` T)"
unfolding left_ideal_def
proof(intro allI ballI)
fix fs ft assume prems: "ft \<in> f ` T"
then obtain t where t: "t \<in> T" and ft_def: "ft = f t" by clarsimp
from assms(2) obtain s where fs_def: "fs = f s" by auto
from assms have "t \<in> T \<Longrightarrow> s *\<^sub>t\<^sub>t\<^sub>a t \<in> T" for s t by auto
with t show "fs *\<^sub>t\<^sub>t\<^sub>a ft \<in> f ` T"
unfolding ft_def fs_def hom[symmetric] by simp
qed
end
locale semigroup_mult_hom_with =
dom: tta_semigroup times_a + cod: tta_semigroup times_b
for times_a (infixl \<open>*\<^sub>o\<^sub>w\<^sub>.\<^sub>a\<close> 70) and times_b (infixl \<open>*\<^sub>o\<^sub>w\<^sub>.\<^sub>b\<close> 70) +
fixes f :: "'a \<Rightarrow> 'b"
assumes f_hom: "f (a *\<^sub>o\<^sub>w\<^sub>.\<^sub>a b) = f a *\<^sub>o\<^sub>w\<^sub>.\<^sub>b f b"
lemma semigroup_mult_hom_with[ud_with]:
"tta_semigroup_hom = semigroup_mult_hom_with (*\<^sub>t\<^sub>t\<^sub>a) (*\<^sub>t\<^sub>t\<^sub>a)"
unfolding
semigroup_mult_hom_with_def tta_semigroup_hom_def
class.tta_semigroup_def semigroup_mult_hom_with_axioms_def
by auto
locale semigroup_ow =
fixes U :: "'ag set" and f :: "['ag, 'ag] \<Rightarrow> 'ag" (infixl \<open>\<^bold>*\<^sub>o\<^sub>w\<close> 70)
assumes f_closed: "\<lbrakk> a \<in> U; b \<in> U \<rbrakk> \<Longrightarrow> a \<^bold>*\<^sub>o\<^sub>w b \<in> U"
and assoc: "\<lbrakk> a \<in> U; b \<in> U; c \<in> U \<rbrakk> \<Longrightarrow> a \<^bold>*\<^sub>o\<^sub>w b \<^bold>*\<^sub>o\<^sub>w c = a \<^bold>*\<^sub>o\<^sub>w (b \<^bold>*\<^sub>o\<^sub>w c)"
begin
notation f (infixl \<open>\<^bold>*\<^sub>o\<^sub>w\<close> 70)
lemma f_closed'[simp]: "\<forall>x\<in>U. \<forall>y\<in>U. x \<^bold>*\<^sub>o\<^sub>w y \<in> U" by (simp add: f_closed)
tts_register_sbts \<open>(\<^bold>*\<^sub>o\<^sub>w)\<close> | U by (rule tts_AA_A_transfer[OF f_closed])
end
locale times_ow =
fixes U :: "'ag set" and times :: "['ag, 'ag] \<Rightarrow> 'ag" (infixl \<open>*\<^sub>o\<^sub>w\<close> 70)
assumes times_closed[simp, intro]: "\<lbrakk> a \<in> U; b \<in> U \<rbrakk> \<Longrightarrow> a *\<^sub>o\<^sub>w b \<in> U"
begin
notation times (infixl \<open>*\<^sub>o\<^sub>w\<close> 70)
lemma times_closed'[simp]: "\<forall>x\<in>U. \<forall>y\<in>U. x *\<^sub>o\<^sub>w y \<in> U" by simp
tts_register_sbts \<open>(*\<^sub>o\<^sub>w)\<close> | U by (rule tts_AA_A_transfer[OF times_closed])
end
locale semigroup_mult_ow = times_ow U times
for U :: "'ag set" and times +
assumes mult_assoc:
"\<lbrakk> a \<in> U; b \<in> U; c \<in> U \<rbrakk> \<Longrightarrow> a *\<^sub>o\<^sub>w b *\<^sub>o\<^sub>w c = a *\<^sub>o\<^sub>w (b *\<^sub>o\<^sub>w c)"
begin
sublocale mult: semigroup_ow U \<open>(*\<^sub>o\<^sub>w)\<close>
by unfold_locales (auto simp: times_closed' mult_assoc)
end
locale semigroup_mult_hom_ow =
dom: semigroup_mult_ow UA times_a +
cod: semigroup_mult_ow UB times_b
for UA :: "'a set"
and UB :: "'b set"
and times_a (infixl \<open>*\<^sub>o\<^sub>w\<^sub>.\<^sub>a\<close> 70)
and times_b (infixl \<open>*\<^sub>o\<^sub>w\<^sub>.\<^sub>b\<close> 70) +
fixes f :: "'a \<Rightarrow> 'b"
assumes f_closed[simp]: "a \<in> UA \<Longrightarrow> f a \<in> UB"
and f_hom: "\<lbrakk> a \<in> UA; b \<in> UA \<rbrakk> \<Longrightarrow> f (a *\<^sub>o\<^sub>w\<^sub>.\<^sub>a b) = f a *\<^sub>o\<^sub>w\<^sub>.\<^sub>b f b"
begin
lemma f_closed'[simp]: "f ` UA \<subseteq> UB" by auto
tts_register_sbts f | UA and UB by (rule tts_AB_transfer[OF f_closed'])
end
context semigroup_mult_hom_ow
begin
lemma tta_left_ideal_ow_closed:
assumes "T \<subseteq> UA"
and "left_ideal_ow UA (*\<^sub>o\<^sub>w\<^sub>.\<^sub>a) T"
and "f ` UA = UB"
shows "left_ideal_ow UB (*\<^sub>o\<^sub>w\<^sub>.\<^sub>b) (f ` T)"
unfolding left_ideal_ow_def
proof(intro ballI)
fix fs ft assume ft: "ft \<in> f ` T" and fs: "fs \<in> UB"
then obtain t where t: "t \<in> T" and ft_def: "ft = f t" by auto
from assms(3) fs obtain s where fs_def: "fs = f s" and s: "s \<in> UA" by auto
from assms have "\<lbrakk> s \<in> UA; t \<in> T \<rbrakk> \<Longrightarrow> s *\<^sub>o\<^sub>w\<^sub>.\<^sub>a t \<in> T" for s t
unfolding left_ideal_ow_def by simp
with assms(1) s t fs show "fs *\<^sub>o\<^sub>w\<^sub>.\<^sub>b ft \<in> f ` T"
using f_hom[symmetric, OF s] unfolding ft_def fs_def by auto
qed
end
lemma semigroup_mult_ow: "class.tta_semigroup = semigroup_mult_ow UNIV"
unfolding
class.tta_semigroup_def semigroup_mult_ow_def
semigroup_mult_ow_axioms_def times_ow_def
by simp
lemma semigroup_mult_hom_ow:
"tta_semigroup_hom = semigroup_mult_hom_ow UNIV UNIV (*\<^sub>t\<^sub>t\<^sub>a) (*\<^sub>t\<^sub>t\<^sub>a)"
unfolding
tta_semigroup_hom_def semigroup_mult_hom_ow_axioms_def
semigroup_mult_hom_ow_def semigroup_mult_ow_def
semigroup_mult_ow_axioms_def times_ow_def
by simp
context
includes lifting_syntax
begin
lemma semigroup_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((A ===> A ===> A) ===> (=))
(semigroup_ow (Collect (Domainp A))) semigroup"
proof-
let ?P = "((A ===> A ===> A) ===> (=))"
let ?semigroup_ow = "semigroup_ow (Collect (Domainp A))"
let ?rf_UNIV =
"(\<lambda>f::['b, 'b] \<Rightarrow> 'b. (\<forall>x y. x \<in> UNIV \<longrightarrow> y \<in> UNIV \<longrightarrow> f x y \<in> UNIV))"
have "?P ?semigroup_ow (\<lambda>f. ?rf_UNIV f \<and> semigroup f)"
unfolding semigroup_ow_def semigroup_def
apply transfer_prover_start
apply transfer_step+
by simp
thus ?thesis by simp
qed
lemma semigroup_mult_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((A ===> A ===> A) ===> (=))
(semigroup_mult_ow (Collect (Domainp A)))
class.tta_semigroup"
proof -
let ?P = \<open>((A ===> A ===> A) ===> (=))\<close>
and ?semigroup_mult_ow =
\<open>(\<lambda>f. semigroup_mult_ow (Collect (Domainp A)) f)\<close>
and ?rf_UNIV =
\<open>(\<lambda>f::['b, 'b] \<Rightarrow> 'b. (\<forall>x y. x \<in> UNIV \<longrightarrow> y \<in> UNIV \<longrightarrow> f x y \<in> UNIV))\<close>
have "?P ?semigroup_mult_ow (\<lambda>f. ?rf_UNIV f \<and> class.tta_semigroup f)"
unfolding
semigroup_mult_ow_def class.tta_semigroup_def
semigroup_mult_ow_axioms_def times_ow_def
apply transfer_prover_start
apply transfer_step+
by simp
thus ?thesis by simp
qed
lemma semigroup_mult_hom_transfer[transfer_rule]:
assumes [transfer_rule]:
"bi_unique A" "right_total A" "bi_unique B" "right_total B"
shows
"((A ===> A ===> A) ===> (B ===> B ===> B) ===> (A ===> B) ===> (=))
(semigroup_mult_hom_ow (Collect (Domainp A)) (Collect (Domainp B)))
semigroup_mult_hom_with"
proof-
let ?PA = "A ===> A ===> A"
and ?PB = "B ===> B ===> B"
and ?semigroup_mult_hom_ow =
\<open>
\<lambda>times_a times_b f. semigroup_mult_hom_ow
(Collect (Domainp A)) (Collect (Domainp B)) times_a times_b f
\<close>
let ?closed = \<open>\<lambda>f::'b\<Rightarrow>'d . \<forall>a. a \<in> UNIV \<longrightarrow> f a \<in> UNIV\<close>
have
"(?PA ===> ?PB ===> (A ===> B) ===> (=))
?semigroup_mult_hom_ow
(
\<lambda>times_a times_b f.
?closed f \<and> semigroup_mult_hom_with times_a times_b f
)"
unfolding
times_ow_def
semigroup_mult_hom_ow_def
semigroup_mult_hom_ow_axioms_def
semigroup_mult_hom_with_def
semigroup_mult_hom_with_axioms_def
apply transfer_prover_start
apply transfer_step+
by blast
thus ?thesis by simp
qed
end
context semigroup_mult_hom_ow
begin
ML_file\<open>ETTS_TEST_TTS_ALGORITHM.ML\<close>
named_theorems semigroup_mult_hom_ow_test_simps
lemmas [semigroup_mult_hom_ow_test_simps] =
ctr_simps_Collect_mem_eq
ctr_simps_in_iff
tts_context
tts: (?'a to UA) and (?'b to UB)
sbterms: (\<open>(*\<^sub>t\<^sub>t\<^sub>a)::[?'a::tta_semigroup, ?'a] \<Rightarrow> ?'a\<close> to \<open>(*\<^sub>o\<^sub>w\<^sub>.\<^sub>a)\<close>)
and (\<open>(*\<^sub>t\<^sub>t\<^sub>a)::[?'b::tta_semigroup, ?'b] \<Rightarrow> ?'b\<close> to \<open>(*\<^sub>o\<^sub>w\<^sub>.\<^sub>b)\<close>)
and (\<open>?f::?'a::tta_semigroup \<Rightarrow> ?'b::tta_semigroup\<close> to f)
rewriting semigroup_mult_hom_ow_test_simps
substituting semigroup_mult_hom_ow_axioms
and dom.semigroup_mult_ow_axioms
and cod.semigroup_mult_ow_axioms
eliminating \<open>UA \<noteq> {}\<close> and \<open>UB \<noteq> {}\<close>
through (auto simp only: left_ideal_ow_def)
begin
ML\<open>
Lecker.test_group @{context} () [etts_test_tts_algorithm.test_suite]
\<close>
end
end
subsection\<open>\<open>tts_register_sbts\<close>\<close>
context
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
and UA :: "'a set"
begin
ML_file\<open>ETTS_TEST_TTS_REGISTER_SBTS.ML\<close>
ML\<open>
Lecker.test_group @{context} () [etts_test_tts_register_sbts.test_suite]
\<close>
end
end
\ No newline at end of file

File Metadata

Mime Type
application/octet-stream
Expires
Fri, May 10, 7:39 PM (2 d)
Storage Engine
blob
Storage Format
Raw Data
Storage Handle
1176676
Default Alt Text
(79 KB)

Event Timeline