File ‹More_Library.ML›
signature LIBRARY =
sig
include LIBRARY
val reroute_ps_sp : ('a * 'b) * 'c -> 'a * ('b * 'c)
val reroute_sp_ps : 'a * ('b * 'c) -> ('a * 'b) * 'c
val reroute_ps_triple : ('a * 'b) * 'c -> 'a * 'b * 'c
val reroute_sp_triple : 'a * ('b * 'c) -> 'a * 'b * 'c
val reroute_triple_ps : 'a * 'b * 'c -> ('a * 'b) * 'c
val reroute_triple_sp : 'a * 'b * 'c -> 'a * ('b * 'c)
val dup : 'a -> 'a * 'a
val apdupr : ('a -> 'b) -> 'a -> 'a * 'b
val apdupl : ('a -> 'b) -> 'a -> 'b * 'a
val map_slice_l : ('a list -> 'b list) -> ('a * 'c) list -> ('b * 'c) list
val map_slice_r : ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list
val map_slice_side_l :
('a list -> 'b list * 'c) -> ('a * 'd) list -> ('b * 'd) list * 'c
val map_slice_side_r :
('a list -> 'b list * 'c) -> ('d * 'a) list -> ('d * 'b) list * 'c
val find_indices : ('a -> bool) -> 'a list -> int list
val tabulate : string -> string
val mk_opt_id : ('a -> 'b) -> ('a -> 'b option) -> 'a -> 'b
val kw_bo : string parser
val kw_bc : string parser
val kw_col : string parser
end
structure Library: LIBRARY =
struct
open Library;
fun reroute_ps_sp ((x, y), z) = (x, (y, z));
fun reroute_sp_ps (x, (y, z)) = ((x, y), z);
fun reroute_ps_triple ((x, y), z) = (x, y, z);
fun reroute_sp_triple (x, (y, z)) = (x, y, z);
fun reroute_triple_ps (x, y, z) = ((x, y), z);
fun reroute_triple_sp (x, y, z) = (x, (y, z));
fun dup x = (x, x);
fun apdupr f x = (x, f x);
fun apdupl f x = (f x, x);
fun map_slice_l f xs = xs
|> split_list
|>> f
|> op~~;
fun map_slice_r f xs = xs
|> split_list
||> f
|> op~~;
fun map_slice_side_l f xs = xs
|> split_list
|>> f
|> swap
|> reroute_sp_ps
|>> swap
|>> op~~;
fun map_slice_side_r f xs = xs
|> split_list
||> f
|> reroute_sp_ps
|>> op~~;
fun find_indices p xs =
let
fun find_indices_impl _ _ [] = []
| find_indices_impl p i (x::xs) =
if p x
then i::find_indices_impl p (i + 1) xs
else find_indices_impl p (i + 1) xs
in find_indices_impl p 0 xs end;
fun mk_opt_id g f x = case f x of SOME y => y | NONE => g x;
val tabulate = split_lines #> map (fn c => "\t" ^ c) #> String.concatWith "\n"
val kw_bo = \<^keyword>‹(›;
val kw_bc = \<^keyword>‹)›;
val kw_col = \<^keyword>‹:›;
end
open Library;File ‹More_Binding.ML›
signature BINDING =
sig
include BINDING
val qualified_name_mandatory : string -> binding
end;
structure Binding: BINDING =
struct
open Binding;
fun qualified_name_mandatory c = fold
(fn c => fn b => Binding.qualify_name true b c)
(Long_Name.explode c)
Binding.empty;
end;
File ‹More_Type.ML›
signature TYPE =
sig
include TYPE
val typ_matches : tsig -> typ list * typ list -> tyenv -> tyenv
val default_sorts_of_empty_sorts : theory -> typ -> typ
val default_sorts : theory -> typ -> typ
end
structure Type: TYPE =
struct
open Type;
fun typ_matches tsig (T :: Ts, U :: Us) subs =
typ_matches tsig (Ts, Us) (Type.typ_match tsig (T, U) subs)
| typ_matches _ ([], []) subs = subs
| typ_matches _ _ _ = raise Type.TYPE_MATCH;
fun default_sorts_of_empty_sorts thy =
let val dS = Sign.defaultS thy
in
map_atyps
(
fn TFree (x, []) => TFree (x, dS)
| TVar (xi, []) => TVar (xi, dS)
| TFree (x, S) => TFree (x, S)
| TVar (xi, S) => TVar (xi, S)
)
end;
fun default_sorts thy =
let val dS = Sign.defaultS thy
in
map_atyps
(
fn TFree (x, _) => TFree (x, dS)
| TVar (xi, _) => TVar (xi, dS)
)
end;
end;File ‹More_Sort.ML›
signature SORTS =
sig
include SORTS
val params_of_super_classes : theory -> class -> (string * typ) list
val params_of_sort : theory -> class list -> (string * typ) list
end;
structure Sorts: SORTS =
struct
open Sorts;
fun params_of_class thy class =
try (Axclass.get_info thy #> #params) class |> these;
fun params_of_super_classes thy class =
class :: Sorts.super_classes (Sign.classes_of thy) class
|> maps (params_of_class thy);
fun params_of_sort thy sort = maps (params_of_super_classes thy) sort;
end;
File ‹More_Term.ML›
signature TERM =
sig
include TERM
val map_sv : (indexname * typ -> term) -> term -> term
val map_fv : (string * typ -> term) -> term -> term
val map_const : (string * typ -> term) -> term -> term
val map_tfree: (string * sort -> typ) -> term -> term
val has_tfreesT : typ -> bool
val is_comb : term -> bool
val could_match_const : (''a * typ) * (''a * typ) -> bool
end;
structure Term: TERM =
struct
open Term;
fun map_sv f (Var sv_spec) = f sv_spec
| map_sv f (Abs (c, T, t)) = Abs (c, T, map_sv f t)
| map_sv f (t $ u) = map_sv f t $ map_sv f u
| map_sv _ t = t;
fun map_fv f (Free fv_spec) = f fv_spec
| map_fv f (Abs (c, T, t)) = Abs (c, T, map_fv f t)
| map_fv f (t $ u) = map_fv f t $ map_fv f u
| map_fv _ t = t;
fun map_const f (Const const_spec) = f const_spec
| map_const f (Abs (c, T, t)) = Abs (c, T, map_const f t)
| map_const f (t $ u) = map_const f t $ map_const f u
| map_const _ t = t;
fun map_tfree f (Const (c, T)) = Const (c, map_type_tfree f T)
| map_tfree f (Free (c, T)) = Free (c, map_type_tfree f T)
| map_tfree f (Var (v, T)) = Var (v, map_type_tfree f T)
| map_tfree f (Abs (c, T, t)) = Abs (c, map_type_tfree f T, map_tfree f t)
| map_tfree f (t $ u) = map_tfree f t $ map_tfree f u
| map_tfree _ t = t
fun has_tfreesT (TFree _) = true
| has_tfreesT (TVar _) = false
| has_tfreesT (Type (_, Ts)) = has_tfreesT_list Ts
and has_tfreesT_list [] = false
| has_tfreesT_list (T::Ts) = has_tfreesT T orelse has_tfreesT_list Ts;
fun is_comb (_ $ _) = true
| is_comb _ = false;
fun could_match_const ((c, T), (c', T')) =
c = c' andalso Type.could_match (T, T');
end;File ‹More_Variable.ML›
signature VARIABLE =
sig
include VARIABLE
val fix_new_vars : Proof.context -> string list -> Proof.context
val variant_name_const : Proof.context -> string list -> string list
end
structure Variable: VARIABLE =
struct
open Variable;
fun fix_new_vars ctxt cs =
let
fun fix_new_vars_select c ctxt =
if Variable.is_fixed ctxt c
then ctxt
else ctxt |> Variable.add_fixes (single c) |> #2
in fold_rev fix_new_vars_select cs ctxt end;
fun variant_name_const ctxt names =
let
val {constants=constants, ...} = Consts.dest (Proof_Context.consts_of ctxt)
val const_names = map (#1 #> Long_Name.base_name) constants
val name_ctxt = ctxt
|> Variable.names_of
|> fold Name.declare const_names
val names =
let
fun folder name (names, name_ctxt) =
Name.variant name name_ctxt |>> curry (swap #> op::) names
in ([], name_ctxt) |> fold folder names |> #1 end
in names end;
endFile ‹More_Logic.ML›
signature LOGIC =
sig
include LOGIC
val unvarify_types_local_term :
Proof.context -> term -> term * Proof.context
val unvarify_local_term : Proof.context -> term -> term * Proof.context
val varifyT_mixed_global : typ -> typ
val varify_mixed_global : term -> term
val unoverload_types_term : theory -> term -> term
val is_equals : term -> bool
end
structure Logic : LOGIC =
struct
open Logic;
fun unvarify_types_local_factt ctxt ts =
let
val stv_specs = ts
|> map (fn thmt => Term.add_tvars thmt [] |> rev)
|> flat
|> distinct op=
val ctxt' = fold Proof_Context.augment ts ctxt
val (ftv_specs, _) = Variable.invent_types (map #2 stv_specs) ctxt'
val ctxt'' = fold Variable.declare_typ (map TFree ftv_specs) ctxt
val stv_to_ftv = stv_specs ~~ ftv_specs
|> AList.lookup op=
#> the
#> TFree
val ts = map (map_types (map_type_tvar stv_to_ftv)) ts
in (ts, ctxt'') end;
fun unvarify_types_local_term ctxt t = t
|> single
|> unvarify_types_local_factt ctxt
|>> the_single;
fun unvarify_local_factt ctxt ts =
let
val (ts, ctxt') = unvarify_types_local_factt ctxt ts
val sv_specs = map (fn thmt => Term.add_vars thmt [] |> rev) ts
|> flat
|> distinct op=
val stvcs = sv_specs |> (#1 #> #1 |> map)
|> Variable.variant_name_const ctxt'
|> rev
val ftvcs = Variable.variant_fixes stvcs ctxt' |> #1
val ctxt'' = ctxt' |> Variable.add_fixes ftvcs |> #2
val stvc_to_ftvc = (sv_specs ~~ (ftvcs ~~ map #2 sv_specs))
|> AList.lookup op=
#> the
#> Free
val ts = map (Term.map_sv stvc_to_ftvc) ts
in (ts, ctxt'') end;
fun unvarify_local_term ctxt thm = thm
|> single
|> unvarify_local_factt ctxt
|>> the_single;
local
fun ftvs_stvs_map svtcs stvs = stvs
|> map (apdupr #1)
|> map_slice_r (fn cs => Name.variant_list svtcs cs)
|> map (K 0 |> apdupr |> apsnd)
|> map (fn ((c, S), v) => ((c, S), (v, S)))
|> map (apsnd TVar)
|> AList.lookup op= #> the
in
fun varifyT_mixed_global T =
let
val svtcs = map (#1 #> #1) (Term.add_tvarsT T [])
val ftvs_stvs_map = ftvs_stvs_map svtcs (Term.add_tfreesT T [])
in Term.map_type_tfree ftvs_stvs_map T end;
fun varify_mixed_global t =
let
val svtcs = map (#1 #> #1) (Term.add_tvars t [])
val ftvs_stvs_map = ftvs_stvs_map svtcs (Term.add_tfrees t [])
val t = Term.map_tfree ftvs_stvs_map t
val svcs = map (#1 #> #1) (Term.add_vars t [])
val fvs_svs_map = Term.add_frees t []
|> map (apdupr #1)
|> map_slice_r (fn cs => Name.variant_list svcs cs)
|> map (K 0 |> apdupr |> apsnd)
|> map (fn ((c, T), v) => ((c, T), (v, T)))
|> map (apsnd Var)
|> AList.lookup op= #> the
val t = Term.map_fv fvs_svs_map t
in t end;
end;
fun unoverload_types_term thy t =
let
val sort_consts = Term.add_tvars t []
|> map #2
|> map (Sorts.params_of_sort thy)
|> flat
|> distinct op=
val const_map = Term.add_consts t []
|> distinct op=
|> filter (member Term.could_match_const sort_consts)
|> dup
||> map (#1 #> Long_Name.base_name)
||> Name.variant_list (Term.add_vars t [] |> map #1 |> map #1)
|> op~~
|> map (fn ((c, T), d) => ((c, T), Var ((d, 0), T)))
fun const_map_opt const_spec = case AList.lookup op= const_map const_spec of
SOME t => t |
NONE => Const const_spec
val t' = Term.map_const const_map_opt t
val t'' =
let
val uctxt = Logic.unconstrainT [] t' |> #1
val map_atyps =
Term.map_atyps (Type.default_sorts thy o (#atyp_map uctxt))
val t'' = t'
|> Term.map_types map_atyps
|> curry Logic.list_implies (map #2 (#constraints uctxt));
val prems = Logic.strip_imp_prems t'
val prems = drop (length prems - Logic.count_prems t') prems
in Logic.list_implies (prems, Logic.strip_imp_concl t'') end
in t'' end;
fun is_equals (Const (\<^const_name>‹Pure.eq›, _) $ _ $ _) = true
| is_equals _ = false;
end;File ‹More_Thm.ML›
signature THM =
sig
include THM
val unvarify_local_fact :
Proof.context -> thm list -> thm list * Proof.context
val unvarify_local_thm : Proof.context -> thm -> thm * Proof.context
val unvarify_local_thms :
Proof.context -> thm list -> thm list * Proof.context
val tags_rule : (string * string) list -> thm -> thm
val apply_attributes:
attribute list -> thm list -> Context.generic -> thm list * Context.generic
val forall_intr_var_order : Proof.context -> int list -> thm -> thm
val pure_unfold : Proof.context -> thm list -> thm -> thm
end;
structure Thm: THM =
struct
open Thm;
fun unvarify_local_fact ctxt thms =
let
val thmts = map Thm.full_prop_of thms
val stv_specs = thmts
|> map (fn thmt => Term.add_tvars thmt [] |> rev)
|> flat
|> distinct op=
val ctxt' = fold Proof_Context.augment thmts ctxt
val (ftv_specs, ctxt'') = Variable.invent_types (map #2 stv_specs) ctxt'
val ctxt''' = fold Variable.declare_typ (map TFree ftv_specs) ctxt
val stv_to_ftv = stv_specs ~~ ftv_specs |> AList.lookup op= #> the
val instT = map (fn v => (v, v |> stv_to_ftv |> TFree)) stv_specs
val sv_specs = thmts
|> map (fn thmt => Term.add_vars thmt [] |> rev)
|> flat
|> distinct op=
val ftvcs =
let
val stvcs = sv_specs
|> map (#1 #> #1)
|> Variable.variant_name_const ctxt''
|> rev
in Variable.variant_fixes stvcs ctxt'' |> #1 end
val ctxt'''' = Variable.add_fixes ftvcs ctxt''' |> #2
val insts =
let val stvc_to_ftvc = AList.lookup op= (sv_specs ~~ ftvcs) #> the
in
map
(
fn v as ((a, i), T) =>
let val T' = Term_Subst.instantiateT instT T
in
(
((a, i), T'),
((stvc_to_ftvc v, T') |> Free |> Thm.cterm_of ctxt'''')
)
end
)
sv_specs
end
val ctxt''''' = ctxt''''
|> fold Variable.declare_term (map (#2 #> Thm.term_of) insts)
val thms' =
map
(
Drule.instantiate_normalize
(map (apsnd (Thm.ctyp_of ctxt)) instT, insts)
)
thms
in (thms', ctxt''''') end;
fun unvarify_local_thm ctxt thm = thm
|> single
|> unvarify_local_fact ctxt
|>> the_single;
fun unvarify_local_thms ctxt thms =
let
fun folder thm (thms, ctxt) = thm
|> single
|> unvarify_local_fact ctxt
|>> the_single
|>> curry (swap #> op::) thms;
in fold_rev folder thms ([], ctxt) end;
fun tags_rule tgs thm = fold Thm.tag_rule tgs thm;
fun apply_attributes attrs thms context =
let
fun apply_attributes_single attrs thm context =
fold
(fn attr => fn (thm, context) => Thm.apply_attribute attr thm context)
attrs
(thm, context);
fun folder thm (thms, context) = context
|> apply_attributes_single attrs thm
|>> curry (op:: o swap) thms;
in fold folder thms ([], context) |>> rev end;
fun forall_intr_var_order ctxt order thm' =
let
val stvs = thm'
|> Thm.full_prop_of
|> (fn t => Term.add_vars t [])
|> rev
val stv_cts = map (nth stvs #> Var #> Thm.cterm_of ctxt) order
in fold Thm.forall_intr (rev stv_cts) thm' end;
fun pure_unfold ctxt thms = ctxt
|>
(
thms
|> Conv.rewrs_conv
|> Conv.try_conv
|> K
|> Conv.top_conv
)
|> Conv.fconv_rule;
end;File ‹More_Simplifier.ML›
structure More_Simplifier =
struct
fun asm_full_var_simplify ctxt thm =
let
val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
in
Simplifier.full_simplify ctxt' thm'
|> singleton (Variable.export ctxt' ctxt)
|> Drule.zero_var_indexes
end;
fun var_simplify_only ctxt ths thm =
asm_full_var_simplify (Raw_Simplifier.clear_simpset ctxt addsimps ths) thm;
val var_simplified = Attrib.thms >>
(fn ths => Thm.rule_attribute ths
(fn context => var_simplify_only (Context.proof_of context) ths));
fun rewrite_simp_opt ctxt simp_spec_opt = case simp_spec_opt of
SOME simp_spec => var_simplify_only ctxt simp_spec
| NONE => Simplifier.full_simplify ctxt;
end;File ‹More_HOLogic.ML›
signature HOLOGIC =
sig
include HOLOGIC
val mk_binrelT : typ * typ -> typ
val is_binrelT : typ -> bool
val dest_binrelT : typ -> typ * typ
val mk_rel : string * (typ * typ) -> term
val is_conj : term -> bool
end;
structure HOLogic: HOLOGIC =
struct
open HOLogic;
fun mk_binrelT (T, U) = T --> U --> HOLogic.boolT;
fun is_binrelT (
Type (\<^type_name>‹fun›, [_, Type (\<^type_name>‹fun›, [_, \<^typ>‹bool›])])
) = true
| is_binrelT _ = false
fun dest_binrelT (Type (\<^type_name>‹fun›, [T, Type (\<^type_name>‹fun›, [U, _])])) =
(T, U)
| dest_binrelT T = raise TYPE("dest_binrelT", single T, []);
fun mk_rel (c, (T, U)) = Free (c, mk_binrelT (T, U))
fun is_conj (Const (\<^const_name>‹conj›, _) $ _ $ _) = true
| is_conj _ = false;
end;File ‹More_Transfer.ML›
signature TRANSFER =
sig
include TRANSFER
val is_is_equality : term -> bool
end;
structure Transfer: TRANSFER =
struct
open Transfer;
fun is_is_equality (Const (\<^const_name>‹is_equality›, _) $ _) = true
| is_is_equality _ = false;
end;
File ‹CTR_Utilities.ML›
signature CTR_UTILITIES =
sig
val thm_printer : Proof.context -> bool -> string -> thm list -> unit
val qualified_name_of_const_name : string -> string
end;
structure CTR_Utilities : CTR_UTILITIES =
struct
fun thm_printer ctxt print name thms =
Proof_Display.print_results
print
(Position.thread_data ())
ctxt
((Thm.theoremK, ""), single (name, thms));
fun qualified_name_of_const_name c =
if Long_Name.qualification c = 0
then error "qualified_name_of_const_name: invalid constant name"
else
if Long_Name.qualification c = 1
then c
else c |> Long_Name.explode |> tl |> Long_Name.implode
end;Theory IML_UT
section‹‹IML_UT››
theory IML_UT
imports "../CTR_Tools/CTR_Tools"
begin
ML_file ‹UT_Test_Suite.ML›
end
File ‹UT_Test_Suite.ML›
signature UT_TEST_SUITE =
sig
type ('x, 'y) test_suite
type ('x, 'y) test_results_suite
val init :
string ->
('x -> 'y) ->
('x -> string) ->
('y -> string) ->
('x, 'y) test_suite
val assert_brel :
string ->
('y * 'y -> bool) ->
'y -> 'x ->
('x, 'y) test_suite ->
('x, 'y) test_suite
val assert_exception :
string -> 'x -> exn -> ('x, 'y) test_suite -> ('x, 'y) test_suite
val execute : ('x, 'y) test_suite -> ('x, 'y) test_results_suite
val output_test_results : bool -> ('a, 'b) test_results_suite -> unit
end;
structure UT_Test_Suite: UT_TEST_SUITE =
struct
exception BLANK;
datatype 'y test_output = Exception of exn | Result of 'y;
type 'y assertion_output =
{
expected_output : string,
output : 'y test_output,
status : bool
};
type ('x, 'y) test_result =
{
test_id : int,
name : string,
input : 'x,
assertion_output : 'y assertion_output
};
type ('x, 'y) unit_test =
{
test_id : int,
name : string,
input : 'x,
assertion : 'x -> 'y assertion_output
};
type ('x, 'y) test_results_suite =
{
id : string,
function : 'x -> 'y,
string_of_input : 'x -> string,
string_of_output : 'y -> string,
test_results : ('x, 'y) test_result Queue.T
};
type ('x, 'y) test_suite =
{
id : string,
function : 'x -> 'y,
string_of_input : 'x -> string,
string_of_output : 'y -> string,
tests : ('x, 'y) unit_test Queue.T
};
fun init id f string_of_input string_of_output : ('x, 'y) test_suite =
{
id = id,
function = f,
string_of_input = string_of_input,
string_of_output = string_of_output,
tests = Queue.empty
};
fun get_num_tests tests = length (Queue.content tests);
fun is_empty_test_suite test_suite = Queue.is_empty (#tests test_suite);
fun eval f x =
let
val y_opt = try f x
val out = case y_opt of
SOME y => Result y
| NONE => Exception
(
let val _ = f x in BLANK end
handle exn =>
if Exn.is_interrupt exn then Exn.reraise exn else exn
)
in out end;
local
fun assert_brel_impl
string_of_output brel test_id name y f x : ('x, 'y) unit_test =
let
fun assertion x : 'y assertion_output =
let
val output = eval f x
val status = case output of
Exception _ => false
| Result y' => brel (y', y)
in
{
expected_output = string_of_output y,
output = output,
status = status
}
end
in {test_id = test_id, name = name, input = x, assertion = assertion} end;
in
fun assert_brel name brel y x (test_suite : ('x, 'y) test_suite) =
let
val f = #function test_suite
val string_of_input = #string_of_input test_suite
val string_of_output = #string_of_output test_suite
val tests = #tests test_suite
val test_id = get_num_tests tests
val test = assert_brel_impl string_of_output brel test_id name y f x
in
{
id = #id test_suite,
function = f,
string_of_input = string_of_input,
string_of_output = string_of_output,
tests = Queue.enqueue test tests
} : ('x, 'y) test_suite
end;
end;
local
fun assert_exception_impl test_id name (exn : exn) f x : ('x, 'y) unit_test =
let
fun assertion x : 'y assertion_output =
let
val output = eval f x
val status = case output of
Exception exn' =>
exnName exn' = exnName exn
andalso exnMessage exn' = exnMessage exn
| Result _ => false
in
{
expected_output = "exception '" ^ exnMessage exn ^ "'",
output = output,
status = status
}
end
in {test_id = test_id, name = name, input = x, assertion = assertion} end;
in
fun assert_exception name x (exn : exn) (test_suite : ('x, 'y) test_suite) =
let
val f = #function test_suite
val string_of_input = #string_of_input test_suite
val string_of_output = #string_of_output test_suite
val tests = #tests test_suite
val test_id = get_num_tests tests
val test = assert_exception_impl test_id name exn f x
in
{
id = #id test_suite,
function = f,
string_of_input = string_of_input,
string_of_output = string_of_output,
tests = Queue.enqueue test tests
} : ('x, 'y) test_suite
end;
end;
local
fun execute_test (test_suite : ('x, 'y) test_suite) :
(('x, 'y) test_result * ('x, 'y) test_suite) =
let
val {id, function, string_of_input, string_of_output, tests} = test_suite
val ({test_id, name, input, assertion}, tests') = Queue.dequeue tests
val assertion_output = assertion input
val test_result =
{
test_id = test_id,
name = name,
input = input,
assertion_output = assertion_output
}
val test_suite' =
{
id = id,
function = function,
string_of_input = string_of_input,
string_of_output = string_of_output,
tests = tests'
}
in (test_result, test_suite') end;
in
fun execute (test_suite : ('x, 'y) test_suite) =
let
fun execute_impl test_results test_suite =
let
val (test_result, test_suite') = execute_test test_suite
val test_results' = Queue.enqueue test_result test_results
in
if is_empty_test_suite test_suite'
then test_results'
else execute_impl test_results' test_suite'
end;
val test_results =
{
id = #id test_suite,
function = #function test_suite,
string_of_input = #string_of_input test_suite,
string_of_output = #string_of_output test_suite,
test_results =
if is_empty_test_suite test_suite
then Queue.empty
else execute_impl Queue.empty test_suite
}
in test_results : ('x, 'y) test_results_suite end;
end;
local
fun mk_message
string_of_input string_of_output (test_result : ('x, 'y) test_result) =
let
fun string_of_output' (Exception exn) =
"execution failed with the exception '" ^ exnMessage exn ^ "'"
| string_of_output' (Result y) = string_of_output y
val test = "Test " ^ Int.toString (#test_id test_result) ^ "\n"
val function = "Name: " ^ #name test_result ^ "\n"
val input =
"Input data:\n" ^
tabulate (string_of_input (#input test_result)) ^
"\n"
val output =
"Outcome:\n" ^
tabulate (string_of_output' (#output (#assertion_output test_result))) ^
"\n"
val expected_output =
"Expected outcome:\n" ^
tabulate (#expected_output (#assertion_output test_result)) ^
"\n"
val test_pass_flag = #status (#assertion_output test_result)
val status = "Test result: " ^ (if test_pass_flag then "pass" else "fail")
val c = String.concatWith
" " [test, function, input, output, expected_output, status]
in (test_pass_flag, c) end;
in
fun output_test_results
error_flag (test_results_suite : ('x, 'y) test_results_suite) =
let
val
{
id = id,
string_of_input = string_of_input,
string_of_output = string_of_output,
test_results = test_results,
...
} = test_results_suite
fun mk_messages cs test_results =
if Queue.is_empty test_results
then rev cs
else
let
val (test_result, test_results') = Queue.dequeue test_results
val (test_pass_flag, c) =
mk_message string_of_input string_of_output test_result
in mk_messages ((test_pass_flag, c)::cs) test_results' end
val test_results = mk_messages [] test_results
val heading_c = "Test results for the test suite: " ^ id ^ "\n"
val test_cs = map snd test_results
val num_tests = length test_cs
val test_cs = test_cs
|> String.concatWith "\n\n"
|> single
val tests_failed = test_results
|> map fst
|> map not
|> find_indices I
val num_tests_failed = length tests_failed
val num_tests_passed = num_tests - num_tests_failed
val success_flag = num_tests_failed = 0
val num_tests_c = "Number of tests: " ^ Int.toString num_tests
val num_tests_passed_c =
"Number of tests passed: " ^ Int.toString num_tests_passed
val num_tests_failed_c =
"Number of tests failed: " ^ Int.toString num_tests_failed
val summary_c =
"Test outcome: " ^
(if success_flag then "success" else "failure")
val failed_tests_c =
if success_flag
then "\n"
else
(
"Failed tests: " ^
ML_Syntax.print_list Int.toString tests_failed ^
"\n"
)
val _ =
(
heading_c ::
num_tests_c ::
num_tests_passed_c ::
num_tests_failed_c ::
summary_c ::
failed_tests_c ::
test_cs
)
|> map Pretty.str
|> Pretty.chunks
|> Pretty.writeln
val _ = (not error_flag orelse success_flag)
orelse error ("at least one of the " ^ id ^ " tests failed")
in () end;
end;
end;Theory UD
section‹UD›
theory UD
imports "../CTR_Tools/CTR_Tools" Main
keywords "ud" :: thy_decl
begin
subsection‹Import›
ML_file‹UD_With.ML›
ML_file‹UD_Consts.ML›
ML_file‹UD.ML›
subsection‹‹ud_with››
setup‹UD_With.UDWithData.setup›
end
File ‹UD_With.ML›
signature UD_WITH =
sig
structure UDWithData: NAMED_THMS
end;
structure UD_With : UD_WITH =
struct
structure UDWithData = Named_Thms
(
val name = \<^binding>‹ud_with›
val description = "Unoverloaded definitions"
);
end;File ‹UD_Consts.ML›
signature UD_CONSTS =
sig
structure ConstsData : THEORY_DATA
val const_of_key : theory -> Symtab.key -> term option
val update_const : Symtab.key -> term -> theory -> theory
val remove_const : Symtab.key -> theory -> theory
val get_keys : theory -> Symtab.key list
end;
structure UD_Consts : UD_CONSTS =
struct
structure ConstsData = Theory_Data
(
type T = term Symtab.table
val empty = Symtab.empty
val extend = I
val merge = Symtab.merge (K true)
)
val const_of_key = Symtab.lookup o ConstsData.get
fun update_const k v = ConstsData.map (Symtab.update (k, v))
fun remove_const k = ConstsData.map (Symtab.delete k)
val get_keys = Symtab.keys o ConstsData.get
end;File ‹UD.ML›
signature UD =
sig
datatype ud_thm_out_type = trivial of thm | nontrivial of thm * thm
val axioms_of_ci :
theory -> Defs.T -> string * typ -> (string option * string) list
val das_of_ci : theory -> Defs.T -> string * typ -> thm list
val unoverload_definition :
binding * mixfix -> string * typ -> theory -> ud_thm_out_type * theory
end;
structure UD : UD =
struct
fun mk_msg_unoverload_definition msg = "ud: " ^ msg;
datatype ud_thm_out_type = trivial of thm | nontrivial of thm * thm
local
fun match_args (Ts, Us) =
if Type.could_matches (Ts, Us)
then
Option.map Envir.subst_type
(
SOME (Type.raw_matches (Ts, Us) Vartab.empty)
handle Type.TYPE_MATCH => NONE
)
else NONE;
in
fun axioms_of_ci thy defs (c, T) =
let
val const_entry = Theory.const_dep thy (c, T);
val Uss = Defs.specifications_of defs (fst const_entry);
in
Uss
|> filter (fn spec => is_some (match_args (#lhs spec, snd const_entry)))
|> map (fn Us => (#def Us, #description Us))
end;
fun das_of_ci thy defs = axioms_of_ci thy defs
#> map #1
#> filter is_some
#> map (the #> try (Thm.axiom thy))
#> filter is_some
#> map (the #> Drule.abs_def);
end;
local
val msg_no_cids =
mk_msg_unoverload_definition "no suitable constant-instance definitions";
val msg_ud_ex =
mk_msg_unoverload_definition "unoverloaded constant already exists";
val msg_multiple_cids =
mk_msg_unoverload_definition "multiple constant-instance definitions";
val msg_extra_type_variables =
mk_msg_unoverload_definition "specification depends on extra type variables";
fun map_sorts ctxt map_sortsT thm =
let
val Ts = thm
|> Thm.full_prop_of
|> (fn t => Term.add_tvars t [])
val instTs = Ts
|> map TVar
|> map (Term.map_atyps (map_sortsT (Proof_Context.theory_of ctxt)))
|> map (Thm.ctyp_of ctxt)
|> curry op~~ Ts
in Drule.instantiate_normalize (instTs, []) thm end;
fun trivial_ud thy b cid' =
let
val (with_thm, thy') =
let
val b' = Binding.qualify_name true b "with"
val attr = single UD_With.UDWithData.add
in Global_Theory.add_thm ((b', cid'), attr) thy end
val _ =
let val c = Thm.derivation_name with_thm
in
with_thm
|> single
|> CTR_Utilities.thm_printer (Proof_Context.init_global thy') true c
end
in (trivial with_thm, thy') end;
fun nontrivial_ud thy defs (b, mixfix) cid T =
let
fun mk_with_thm thm_rhs_ct with_def_thm cid =
let
val with_def_thm_rhs_ct = with_def_thm
|> Thm.cprop_of
|> Thm.dest_equals_rhs
val inst = Thm.match (with_def_thm_rhs_ct, thm_rhs_ct)
val const_with_def = with_def_thm
|> Drule.instantiate_normalize inst
|> Thm.symmetric
val with_thm = Thm.transitive cid const_with_def
in with_thm end;
val ctxt = Proof_Context.init_global thy
val cid' = Thm.unvarify_global thy cid
val cid_rhs_ct = cid' |> Thm.cprop_of |> Thm.dest_equals_rhs
val (cid_rhs_t, ctxt') = cid_rhs_ct
|> Thm.term_of
|> Logic.unoverload_types_term thy
|> Logic.unvarify_types_local_term ctxt
val rhs_consts =
let
val sort_const_cs = Term.add_tvarsT T []
|> map #2
|> map (Sorts.params_of_sort thy)
|> flat
|> distinct op=
|> map #1
val consts = Term.add_consts cid_rhs_t []
val consts_no_cids = consts
|> map (fn const => (const, axioms_of_ci thy defs const))
|> filter (fn (_, cid_opt) => null cid_opt)
|> map fst
val consts_in_sort = consts
|> filter (fn (_, T) => Term.has_tfreesT T)
|> filter (fn (c, _) => member op= sort_const_cs c)
val elim_consts = thy
|> UD_Consts.get_keys
|> map (UD_Consts.const_of_key thy #> the #> dest_Const)
val consts_out = consts_no_cids @ consts_in_sort
|> distinct op=
|> filter_out (member (swap #> Term.could_match_const) elim_consts)
in consts_out end
val (cs, ctxt'') = ctxt'
|> Variable.variant_fixes (map (#1 #> Long_Name.base_name) rhs_consts)
val fv_of_const =
(map Const rhs_consts ~~ map Free (cs ~~ map #2 rhs_consts))
|> AList.lookup op=
|> mk_opt_id I
val rhs_const_ts = map Const rhs_consts
val arg_ts = map fv_of_const rhs_const_ts
val cid_rhs_t' = map_aterms fv_of_const cid_rhs_t
fun declare_const_with thy =
let
val T = map type_of arg_ts ---> type_of cid_rhs_t'
val b' = Binding.qualify_name true b "with"
in Sign.declare_const_global ((b', T), mixfix) thy end
val (lhst, thy') = declare_const_with thy
val lhst' = Term.list_comb (lhst, arg_ts)
val (with_def_thm, thy'') =
let
val b' = Binding.qualify_name true b "with_def"
val def_t = Logic.mk_equals (lhst', cid_rhs_t')
in
Global_Theory.add_defs false [((b', def_t), [])] thy' |>> the_single
handle ERROR c =>
let val msg_match = "Specification depends on extra type variables"
in
if String.isSubstring msg_match c
then error msg_extra_type_variables
else error c
end
end
val _ =
let val c = Thm.derivation_name with_def_thm
in
with_def_thm
|> single
|> CTR_Utilities.thm_printer (Proof_Context.init_global thy'') true c
end
val (with_thm, thy''') =
let
val b' = Binding.qualify_name true b "with"
val with_thm = cid'
|> mk_with_thm cid_rhs_ct with_def_thm
|> singleton (Proof_Context.export ctxt'' ctxt)
val attr = single UD_With.UDWithData.add
in Global_Theory.add_thm ((b', with_thm), attr) thy'' end
val _ =
let val c = Thm.derivation_name with_thm
in
with_thm
|> single
|> CTR_Utilities.thm_printer (Proof_Context.init_global thy''') true c
end
in (nontrivial (with_def_thm, with_thm), thy''') end;
in
fun unoverload_definition (b, mixfix) (c, T) thy =
let
fun get_ud_const lr ud_thms =
let
val get_ud_const_impl = Thm.cprop_of
#> lr
#> Thm.term_of
#> strip_abs_body
#> head_of
#> dest_Const
in map get_ud_const_impl ud_thms end
val ctxt = Proof_Context.init_global thy
val defs = Theory.defs_of thy
val ud_thms = ctxt
|> UD_With.UDWithData.get
|> map (Local_Defs.meta_rewrite_rule ctxt)
val T' = T
|> Type.default_sorts_of_empty_sorts thy
|> Logic.varifyT_mixed_global
val _ =
let
val ud_lhs_consts = get_ud_const Thm.dest_equals_lhs ud_thms
val ex = member (swap #> Term.could_match_const) ud_lhs_consts (c, T')
in not ex orelse error msg_ud_ex end
val cids = das_of_ci thy defs (c, T')
val cid =
if null cids
then error msg_no_cids
else
if length cids = 1
then the_single cids
else error msg_multiple_cids
val cid' =
let
val lhs_const = cid
|> Thm.cprop_of
|> Thm.dest_equals_lhs
|> Thm.term_of
|> head_of
val insts = (lhs_const, Const (c, T'))
|> apply2 (Thm.cterm_of ctxt)
|> Thm.first_order_match
in
cid
|> Drule.instantiate_normalize insts
|> map_sorts ctxt Type.default_sorts_of_empty_sorts
|> Local_Defs.unfold ctxt ud_thms
end
val cid_rhs_t = cid'
|> Thm.cprop_of
|> Thm.dest_equals_rhs
|> Thm.term_of
val trivial_flag =
let val ud_rhs_consts = get_ud_const Thm.dest_equals_rhs ud_thms
in
Term.is_comb cid_rhs_t
andalso cid_rhs_t |> head_of |> is_Const
andalso cid_rhs_t
|> head_of
|> dest_Const
|> member (swap #> Term.could_match_const) ud_rhs_consts
end
val (ud_thm_out, thy') =
if trivial_flag
then trivial_ud thy b cid'
else nontrivial_ud thy defs (b, mixfix) cid' T'
in (ud_thm_out, thy') end;
end;
val msg_not_constant =
mk_msg_unoverload_definition "the input term is not a constant";
fun process_ud ((b_opt, t), mixfix) thy =
let
val t' = Proof_Context.read_term_pattern (Proof_Context.init_global thy) t
val (c, T) = dest_Const t'
handle TERM _ => error msg_not_constant
val b = case b_opt of
SOME b => b
| NONE => Binding.name (Long_Name.base_name c)
in unoverload_definition (b, mixfix) (c, T) thy |> #2 end;
val parse_ud = Scan.option Parse.binding -- Parse.const -- Parse.opt_mixfix';
val _ = Outer_Syntax.command
\<^command_keyword>‹ud›
"unoverloading of constant-instance definitions"
(parse_ud >> (process_ud #> Toplevel.theory));
end;Theory CTR
section‹‹CTR››
theory CTR
imports
"../UD/UD"
"HOL-Library.Conditional_Parametricity"
keywords "ctr_relator" :: thy_defn
and "ctr" :: thy_defn
and "trp"
and "synthesis"
and "relativization"
and "hybrid"
and "parametricity"
begin
subsection‹Import›
ML_file "CTR_Relators.ML"
ML_file "CTR_Foundations.ML"
ML_file "CTR_Algorithm.ML"
ML_file "CTR_Conversions.ML"
ML_file "CTR_Relativization.ML"
ML_file "CTR_Parametricity.ML"
ML_file "CTR_Postprocessing.ML"
ML_file "CTR.ML"
subsection‹Rewriting›
named_theorems ctr_blank
named_theorems ctr_simps
lemma ctr_simps_pred_fun_top_eq_range[ctr_simps]:
"pred_fun top (λx. x ∈ R) f = (range f ⊆ R)"
by auto
lemma ctr_simps_pred_prod_eq_cart[ctr_simps]:
"pred_prod (λx. x ∈ A) (λx. x ∈ B) = (λx. x ∈ A × B)"
by auto
lemma ctr_simps_pred_fun_eq_image[ctr_simps]:
"pred_fun (λx. x ∈ D) (λx. x ∈ R) f ⟷ (f ` D ⊆ R)"
by auto
lemma ctr_simps_in_iff[ctr_simps]: "(∀x∈A. x ∈ U) ⟷ A ⊆ U" by auto
lemma ctr_simps_subset_pow_iff[ctr_simps]: "(∀A∈S. A ⊆ U) ⟷ S ⊆ Pow U"
by auto
lemma ctr_simps_subset_pow_iff'[ctr_simps]:
"(∀A. A ∈ S ⟶ A ⊆ U) ⟷ S ⊆ Pow U"
by auto
lemma ctr_simps_subset_pow_iff''[ctr_simps]: "(S ⊆ {S. S ⊆ U}) ⟷ S ⊆ Pow U"
by (simp add: subset_eq)
lemma ctr_simps_range_ss_iff[ctr_simps]: "(∀x. f x ∈ U) ⟷ range f ⊆ U"
by auto
lemma ctr_simps_range_pow_ss_iff[ctr_simps]: "(∀x. f x ⊆ U) ⟷ range f ⊆ Pow U"
by auto
lemma ctr_simps_Ball_def'[ctr_simps]: "(∀x. x ∈ A ⟶ P x) ⟷ (∀x ∈ A. P x)"
by auto
lemma ctr_simps_True_imp[ctr_simps]: "(True ⟶ A) ⟷ A" by simp
lemma ctr_simps_True_conj[ctr_simps]: "(True ∧ A) ⟷ A" by simp
lemma ctr_simps_conj_True[ctr_simps]: "(A ∧ True) ⟷ A" by simp
lemma ctr_simps_top_True[ctr_simps]: "top A ⟷ True" by auto
lemma ctr_simps_Ball_True[ctr_simps]: "(∀x∈U. True) ⟷ True" by auto
lemma ctr_simps_Ball_UNIV[ctr_simps]: "(∀n∈UNIV. A n) ⟷ (∀n. A n)" by simp
lemma ctr_simps_Bex_UNIV[ctr_simps]: "(∃n∈UNIV. A n) ⟷ (∃n. A n)" by simp
lemma ctr_simps_subset_Pow[ctr_simps]: "{A. A ⊆ U} = Pow U" by blast
lemma ctr_simps_mem_Collect_eq[ctr_simps]: "(a ∈ Collect P) = P a"
by (rule mem_Collect_eq)
lemma ctr_simps_relation_top_empty_eq[ctr_simps]: "(λx. x ∈ UNIV) = top"
by auto
lemma ctr_simps_pred_fun_eq[ctr_simps]:
"pred_fun A B = (λf. ∀x. A x ⟶ B (f x))"
by simp
lemma ctr_simps_subset_eq_sym[ctr_simps]: "(∀x∈A. x ∈ B) ⟷ (A ⊆ B)" by auto
lemma ctr_simps_UNIV_I[ctr_simps]: "x ∈ UNIV" by simp
lemma ctr_simps_UNIV_def[ctr_simps]: "{x. True} = UNIV" by simp
lemma ctr_simps_conj_commute[ctr_simps]: "(P ∧ Q) ⟷ (Q ∧ P)" by auto
lemma ctr_simps_conj_absorb[ctr_simps]: "(A ∧ A) ⟷ A" by simp
lemma ctr_simps_conj_left_absorb[ctr_simps]: "(A ∧ A ∧ B) ⟷ (A ∧ B)" by simp
lemma ctr_simps_inf_idem[ctr_simps]: "inf a a = (a::'a::semilattice_inf)"
by simp
lemma ctr_simps_sup_idem[ctr_simps]: "sup a a = (a::'a::semilattice_sup)"
by simp
lemma ctr_simps_inf_assoc[ctr_simps]:
"inf (inf a b) c = inf (a::'a::semilattice_inf) (inf b c)"
by (auto simp: semilattice_inf_class.inf.assoc)
lemma ctr_simps_sup_assoc[ctr_simps]:
"sup (sup a b) c = sup (a::'a::semilattice_sup) (sup b c)"
by (auto simp: semilattice_sup_class.sup.assoc)
lemma ctr_simps_Collect_mem_eq[ctr_simps]: "{x. x ∈ U} = U" by simp
subsection‹tts relators›
ctr_relator rel_set
ctr_relator rel_filter
endFile ‹CTR_Relators.ML›
signature CTR_RELATORS =
sig
structure RelatorData: GENERIC_DATA
val get_relator_data_generic : Context.generic -> RelatorData.T
val get_relator_data_proof : Proof.context -> RelatorData.T
val get_relator_data_global : theory -> RelatorData.T
val relator_of_generic : Context.generic -> Symtab.key -> term option
val relator_of_proof : Proof.context -> Symtab.key -> term option
val relator_of_global : theory -> Symtab.key -> term option
val update_relator : Symtab.key -> term -> local_theory -> local_theory
val process_ctr_relator : string -> Proof.context -> local_theory
val pr_of_typ : Proof.context -> ((string * sort) * term) list -> typ -> term
val bnf_relator_of_type_name : Proof.context -> string -> term option
end;
structure CTR_Relators : CTR_RELATORS =
struct
structure RelatorData = Generic_Data
(
type T = term Symtab.table
val empty = Symtab.empty
val extend = I
val merge = Symtab.merge (K true)
);
val get_relator_data_generic = RelatorData.get;
val get_relator_data_proof = Context.Proof #> get_relator_data_generic;
val get_relator_data_global = Context.Theory #> get_relator_data_generic;
fun relator_of_generic context = context
|> get_relator_data_generic
|> Symtab.lookup
#>
(
context
|> Context.theory_of
|> (Morphism.transfer_morphism #> Morphism.term)
|> Option.map
);
val relator_of_proof = Context.Proof #> relator_of_generic;
val relator_of_global = Context.Theory #> relator_of_generic;
fun update_relator k rel = Local_Theory.declaration
{pervasive=true, syntax=false}
(fn phi => (k, Morphism.term phi rel) |> Symtab.update |> RelatorData.map);
fun mk_msg_ctr_relator msg = "ctr_relator: " ^ msg;
val mk_msg_not_const = "the input must be a constant term";
val mk_msg_not_body_bool = "the body of the type of the input must be bool";
val mk_msg_not_binders_2 =
"the type of the input must have more than two binders";
val mk_msg_not_binders_binrelT =
"all of the binders associated with the type of the input" ^
"except the last two must be the binary relation types";
val mk_msg_no_dup_binrelT =
"the types of the binders of the binary relations associated " ^
"with the type of the input must have no duplicates";
val mk_msg_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";
val mk_msg_not_type_constructor =
"the last two binders of the input type must be " ^
"the results of an application of a type constructor";
val mk_msg_not_identical_type_constructors =
"the type constructors that are associated with the last two binders " ^
"of the input type must be identical";
val mk_msg_not_identical_input_types =
"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";
fun relator_type_name_of_type T =
let
val _ = T |> body_type |> curry op= HOLogic.boolT
orelse error (mk_msg_ctr_relator mk_msg_not_body_bool)
val binders = binder_types T
val n = length binders
val _ = n |> (fn n => n > 2)
orelse error (mk_msg_ctr_relator mk_msg_not_binders_2)
val (relTs, (mainT_lhs, mainT_rhs)) = binders
|> chop (n - 2)
||> chop 1
||> apfst the_single
||> apsnd the_single
val _ = relTs |> map HOLogic.is_binrelT |> List.all I
orelse error (mk_msg_ctr_relator mk_msg_not_binders_binrelT)
val (lhs_tvars, rhs_tvars) = relTs
|> map HOLogic.dest_binrelT
|> split_list
val tvars = lhs_tvars @ rhs_tvars
val _ = tvars |> has_duplicates op= |> not
orelse error (mk_msg_ctr_relator mk_msg_no_dup_binrelT)
val _ = tvars |> map (fn T => is_TVar T orelse is_TFree T) |> List.all I
orelse error (mk_msg_ctr_relator mk_msg_not_binders_binrelT_ftv_stv)
val _ = is_Type mainT_lhs
orelse error (mk_msg_ctr_relator mk_msg_not_type_constructor)
val _ = is_Type mainT_rhs
orelse error (mk_msg_ctr_relator mk_msg_not_type_constructor)
val mainT_lhs = dest_Type mainT_lhs
val mainT_rhs = dest_Type mainT_rhs
val _ = op= (apply2 #1 (mainT_lhs, mainT_rhs))
orelse error (mk_msg_ctr_relator mk_msg_not_identical_type_constructors)
val _ = lhs_tvars = #2 mainT_lhs
orelse error (mk_msg_ctr_relator mk_msg_not_identical_input_types)
val _ = rhs_tvars = #2 mainT_rhs
orelse error (mk_msg_ctr_relator mk_msg_not_identical_input_types)
in #1 mainT_lhs end;
fun process_ctr_relator args ctxt =
let
val t = Syntax.read_term ctxt args
val _ = is_Const t orelse error (mk_msg_ctr_relator mk_msg_not_const)
val c = relator_type_name_of_type (type_of t)
in update_relator c t ctxt end;
val _ = Outer_Syntax.local_theory
\<^command_keyword>‹ctr_relator›
"registration of the ctr relators"
(Parse.const >> process_ctr_relator);
fun bnf_relator_of_type_name ctxt c =
let
fun bnf_relator_of_type_name ctxt c =
let
val relator_of_bnf = BNF_Def.rel_of_bnf
#> strip_comb
#> #1
#> dest_Const
#> #1
#> Syntax.read_term ctxt
#> Logic.varify_global
in c |> BNF_Def.bnf_of ctxt |> Option.map relator_of_bnf end
in
case relator_of_proof ctxt c of
SOME t => SOME t
| NONE => bnf_relator_of_type_name ctxt c
end;
fun pr_of_typ ctxt ftv_spec_relt T =
let
fun pr_of_typ _ trel (TFree ftv_spec) = trel ftv_spec
| pr_of_typ _ _ (Type (c, [])) =
Const
(
\<^const_name>‹HOL.eq›,
HOLogic.mk_binrelT (Type (c, []), Type (c, []))
)
| pr_of_typ relator_of_type_name trel (Type (c, Ts)) =
let
val constt = relator_of_type_name c
handle Option =>
raise TYPE ("pr_of_typ: no relator", [Type (c, Ts)], [])
val constT = type_of constt
val binders = constT |> binder_types |> take (length Ts)
val argts = map (pr_of_typ relator_of_type_name trel) Ts
val argTs = map type_of argts
val tyenv_match = Type.typ_matches
(Proof_Context.tsig_of ctxt) (binders, argTs) Vartab.empty
handle Type.TYPE_MATCH =>
raise TYPE ("pr_of_typ: invalid relator", [Type (c, Ts)], [])
val constt = constt
|> dest_Const
||> K (Envir.subst_type tyenv_match constT)
|> Const
in list_comb (constt, argts) end
| pr_of_typ _ _ T = raise TYPE ("pr_of_typ: type", single T, [])
val trel = AList.lookup op= ftv_spec_relt #> the
in pr_of_typ (bnf_relator_of_type_name ctxt #> the) trel T end;
end;File ‹CTR_Foundations.ML›
signature CTR_FOUNDATIONS =
sig
datatype ctr_algorithm = relativization | parametricity
datatype ctr_alg_out =
ALGRelativization of thm | ALGParametricity of thm | ALGFailure
datatype ctr_pp_out =
PPRelativization of (thm * thm) * local_theory
| PPParametricity of thm * local_theory
| PPFailure of local_theory;
val apply_alg_out : (thm -> thm) -> ctr_alg_out -> ctr_alg_out
val lthy_of_pp_out : ctr_pp_out -> local_theory
val string_of_pp_out : ctr_pp_out -> string
end;
structure CTR_Foundations : CTR_FOUNDATIONS =
struct
datatype ctr_algorithm = relativization | parametricity;
datatype ctr_alg_out =
ALGRelativization of thm | ALGParametricity of thm | ALGFailure;
datatype ctr_pp_out =
PPRelativization of (thm * thm) * local_theory
| PPParametricity of thm * local_theory
| PPFailure of local_theory;
fun apply_alg_out f (ALGRelativization thm) = ALGRelativization (f thm)
| apply_alg_out f (ALGParametricity thm) = ALGParametricity (f thm)
| apply_alg_out _ ALGFailure = ALGFailure;
fun lthy_of_pp_out (PPRelativization (_, lthy)) = lthy
| lthy_of_pp_out (PPParametricity (_, lthy)) = lthy
| lthy_of_pp_out (PPFailure lthy) = lthy;
fun string_of_pp_out (PPRelativization ((ow_def_thm, tr_thm), lthy)) =
let
val preamble_c =
"PPRelativization ((ow_def_thm, tr_thm), lthy), where"
val ow_def_thm_c = "ow_def_thm: " ^ Thm.string_of_thm lthy ow_def_thm
val tr_thm_c = "tr_thm: " ^ Thm.string_of_thm lthy tr_thm
val lthy_c = "lthy: unknown local theory"
val out_c = [preamble_c, ow_def_thm_c, tr_thm_c, lthy_c]
|> String.concatWith "\n"
in out_c end
| string_of_pp_out (PPParametricity (tr_thm, lthy)) =
let
val preamble_c = "PPParametricity (tr_thm, lthy), where"
val tr_thm_c = "tr_thm" ^ Thm.string_of_thm lthy tr_thm
val lthy_c = "lthy: unknown local theory"
val out_c = [preamble_c, tr_thm_c, lthy_c]
|> String.concatWith "\n"
in out_c end
| string_of_pp_out (PPFailure _) = "Failure";
end;
open CTR_Foundations;File ‹CTR_Algorithm.ML›
signature CTR_ALGORITHM =
sig
val apply :
Proof.context ->
bool * thm list option ->
thm list ->
((indexname * sort) * term) list ->
thm ->
ctr_alg_out
end;
File ‹CTR_Conversions.ML›
signature CTR_CONVERSIONS =
sig
val const_of_def : Proof.context -> thm -> string * typ
val trt_of_const :
Proof.context -> ((indexname * sort) * term) list -> string * typ -> term
val dest_trt : term -> term * term * term
val prt_of_trt : term -> term
end;
structure CTR_Conversions : CTR_CONVERSIONS =
struct
fun type_specs_rhs_ftv_of_stv type_specs = type_specs
|> map (apsnd (type_of #> HOLogic.dest_binrelT #> #2))
|> AList.lookup op= #> the;
fun type_specs_lhs_ftv_of_stv type_specs = type_specs
|> map (apsnd (type_of #> HOLogic.dest_binrelT #> #1))
|> AList.lookup op= #> the;
fun const_of_def ctxt thm = thm
|> Local_Defs.meta_rewrite_rule ctxt
|> Thm.full_prop_of
|> Logic.dest_equals
|> #1
|> strip_comb
|> #1
|> dest_Const;
fun trt_of_const ctxt type_specs const_spec =
let
fun mk_lhs_stv T = (("a", 0), T)
val rhs_ftv_of_stv = type_specs_rhs_ftv_of_stv type_specs
val lhs_ftv_of_stv = type_specs_lhs_ftv_of_stv type_specs
val rhs_const_spec = apsnd (map_type_tvar rhs_ftv_of_stv) const_spec
val lhs_var_spec = const_spec
|> #2
|> mk_lhs_stv
||> map_type_tvar lhs_ftv_of_stv
val prt =
let val type_specs = map (apfst (rhs_ftv_of_stv #> dest_TFree)) type_specs
in rhs_const_spec |> #2 |> CTR_Relators.pr_of_typ ctxt type_specs end
in prt $ (Var lhs_var_spec) $ (Const rhs_const_spec) end;
fun dest_trt (pr $ lhst $ rhst) = (pr, lhst, rhst)
| dest_trt t = raise TERM ("dest_trt", single t);
fun prt_of_trt trt =
let val (pr, lhst, rhst) = dest_trt trt
in pr $ Const (rhst |> dest_Const |> #1, type_of lhst) $ rhst end;
end;File ‹CTR_Relativization.ML›
structure CTR_Relativization : CTR_ALGORITHM =
struct
open More_Simplifier;
fun pp_tac ctxt unfld_thms def_thm i =
SELECT_GOAL (Local_Defs.unfold_tac ctxt (def_thm :: unfld_thms)) i
THEN CONVERSION (Thm.beta_conversion true) i
THEN CONVERSION Thm.eta_conversion i
THEN Transfer.transfer_prover_start_tac ctxt i
THEN (TRYALL (Transfer.transfer_step_tac ctxt))
THEN (Transfer.transfer_prover_end_tac ctxt i);
fun try_prove ctxt xs asms prop tac = SOME (Goal.prove ctxt xs asms prop tac)
handle ERROR _ => NONE;
fun try_relativization ctxt simp_spec_opt trt unfld_thms def_thm =
let
val tr_thm_opt = pp_tac ctxt unfld_thms def_thm 1
|> K
|> try_prove ctxt [] [] (HOLogic.mk_Trueprop trt)
val tr_thm_opt = Option.map (rewrite_simp_opt ctxt simp_spec_opt) tr_thm_opt
in tr_thm_opt end;
fun apply ctxt (synthesis, simp_spec_opt) assms type_specs def_thm =
let
val is_equality_assms =
let val is_is_equality_thm =
Thm.full_prop_of
#> HOLogic.dest_Trueprop
#> Transfer.is_is_equality
in
assms
|> filter is_is_equality_thm
|> map (@{thm is_equality_def} |> single |> Local_Defs.unfold ctxt)
end
val trt = def_thm
|> CTR_Conversions.const_of_def ctxt
|> CTR_Conversions.trt_of_const ctxt type_specs
val pp_thm_opt =
let val ppt = CTR_Conversions.prt_of_trt trt
in
pp_tac ctxt is_equality_assms def_thm 1
|> K
|> try_prove ctxt [] [] (HOLogic.mk_Trueprop ppt)
end
val tr_thm_opt =
if pp_thm_opt |> Option.isSome |> not andalso synthesis
then try_relativization ctxt simp_spec_opt trt is_equality_assms def_thm
else NONE
val output =
if Option.isSome tr_thm_opt
then ALGRelativization (the tr_thm_opt)
else
if Option.isSome pp_thm_opt
then ALGParametricity (the pp_thm_opt)
else ALGFailure
in output end;
end;File ‹CTR_Parametricity.ML›
structure CTR_Parametricity : CTR_ALGORITHM =
struct
fun theorem_format_error ctxt thm =
let
val msg_main = "Unexpected format for the definition."
val msg = [(Pretty.para msg_main), Thm.pretty_thm ctxt thm]
|> Pretty.chunks
|> Pretty.string_of;
in error msg end;
fun gen_parametric_constant settings lthy def_thm =
let
val eq = Ctr_Sugar_Util.mk_abs_def def_thm
handle TERM _ => theorem_format_error lthy def_thm
val goalt = Conditional_Parametricity.mk_param_goal_from_eq_def lthy eq
val thm = Conditional_Parametricity.prove_goal settings lthy (SOME eq) goalt
in thm end;
fun apply ctxt (_, _) _ _ def_thm =
let
val thm = def_thm
|> gen_parametric_constant Conditional_Parametricity.quiet_settings ctxt
in ALGParametricity thm end;
end;File ‹CTR_Postprocessing.ML›
signature CTR_POSTPROCESSING =
sig
val postprocess_parametricity :
binding -> thm -> local_theory -> ctr_pp_out
val postprocess_relativization :
binding -> mixfix -> thm -> Proof.context -> ctr_pp_out
val postprocess_failure : Proof.context -> ctr_pp_out
end;
structure CTR_Postprocessing : CTR_POSTPROCESSING =
struct
open CTR_Utilities;
fun postprocess_transfer_rule b thm ctxt =
let
val b = ((b |> Binding.path_of |> map fst) @ [Binding.name_of b, "transfer"])
|> Long_Name.implode
|> Binding.qualified_name_mandatory
val lthy = ctxt
|> Local_Theory.note
(
(b, Transfer.transfer_add |> K |> Attrib.internal |> single),
single thm
)
|>> #2
|>> the_single
|> #2
val _ =
let
val lthy_print =
("Transfer.lifting_syntax" |> single |> Bundle.includes) lthy
in
thm
|> single
|> (Local_Theory.full_name lthy_print b |> thm_printer lthy_print true)
end
in lthy end;
fun postprocess_parametricity b thm ctxt =
PPParametricity (thm, postprocess_transfer_rule b thm ctxt);
fun postprocess_relativization b mf thm ctxt =
let
val (_, rhst, _) = thm
|> Thm.concl_of
|> HOLogic.dest_Trueprop
|> CTR_Conversions.dest_trt
val (rhst, ctxt') = Logic.unvarify_local_term ctxt rhst
val (absts, rhst) = rhst
|> Term.strip_abs_eta (rhst |> strip_abs_vars |> length)
val argts = rhst
|> (fn t => Term.add_frees t [])
|> rev
|> subtract op= absts
|> curry (swap #> op@) absts
|> map Free
val (lhst, lthy) =
let
fun declare_const_with thy =
let val T = map type_of argts ---> type_of rhst
in Sign.declare_const_global ((b, T), mf) thy end
in Local_Theory.raw_theory_result declare_const_with ctxt' end
val lhst = Term.list_comb (lhst, argts)
fun make_with_def thy =
let
val b =
((b |> Binding.path_of |> map fst) @ [Binding.name_of b ^ "_def"])
|> Long_Name.implode
|> Binding.qualified_name_mandatory
in
Global_Theory.add_defs
false (single ((b, Logic.mk_equals (lhst, rhst)), [])) thy
|>> the_single
end
val (ow_def_thm, lthy') = Local_Theory.raw_theory_result make_with_def lthy
val _ = ow_def_thm
|> single
|> (ow_def_thm |> Thm.derivation_name |> thm_printer lthy' true)
val thm = Thm.pure_unfold lthy' (ow_def_thm |> Thm.symmetric |> single) thm
in
PPRelativization ((ow_def_thm, thm), postprocess_transfer_rule b thm lthy')
end;
fun postprocess_failure lthy = PPFailure lthy;
end;File ‹CTR.ML›
signature CTR =
sig
datatype alg_input =
ALG_PP of ((binding option * (Facts.ref * Token.src list)) * mixfix) list
| ALG_RP of
(
(
(
(string * (Facts.ref * Token.src list) option) option *
(string, string, Facts.ref) Element.ctxt list
) *
(string * string) list
) * ((binding option * (Facts.ref * Token.src list)) * mixfix) list
)
val ctr_parser : alg_input parser
val process_parametricity :
(binding option * thm) * mixfix ->
Proof.context ->
ctr_pp_out
val process_relativization :
(string * thm list option) option ->
Element.context list ->
(string * string) list ->
(binding option * thm) * mixfix ->
Proof.context ->
ctr_pp_out
val process_ctrs : alg_input -> Proof.context -> Proof.context
end;
structure CTR : CTR =
struct
datatype alg_input =
ALG_PP of ((binding option * (Facts.ref * Token.src list)) * mixfix) list
| ALG_RP of
(
(
(
(string * (Facts.ref * Token.src list) option) option *
(string, string, Facts.ref) Element.ctxt list
) * (string * string) list
) * ((binding option * (Facts.ref * Token.src list)) * mixfix) list
);
local
val algorithm_parser = \<^keyword>‹relativization› || \<^keyword>‹parametricity›;
val synthesis_parser =
Scan.option (\<^keyword>‹synthesis› -- Scan.option Parse.thm);
val type_specs_parser =
Scan.optional
(
\<^keyword>‹trp› |--
Parse.and_list (kw_bo |-- Parse.type_var -- Parse.term --| kw_bc)
)
[];
val thm_specs_parser =
\<^keyword>‹in› |--
Parse.and_list
(
(Scan.option (Parse.binding --| \<^keyword>‹:›)) --
Parse.thm --
Parse.opt_mixfix'
);
fun rel_opt_thm_name s =
Scan.optional
(
(
Parse.binding -- Parse.opt_attribs || Parse.attribs >>
pair Binding.empty
) --| Parse.$$$ s
)
Binding.empty_atts;
val rel_loc_element =
\<^keyword>‹fixes› |-- Parse.!!! Parse_Spec.locale_fixes >> Element.Fixes ||
\<^keyword>‹assumes› |--
Parse.!!! (Parse.and_list1 (rel_opt_thm_name ":" -- Scan.repeat1 Parse.propp))
>> Element.Assumes;
val rel_context_element =
Parse.group (fn () => "context element") rel_loc_element;
fun parametricity_parser tokens = thm_specs_parser tokens |>> ALG_PP;
fun relativization_parser tokens = tokens
|>
(
synthesis_parser --
Scan.repeat rel_context_element --
type_specs_parser --
thm_specs_parser
)
|>> ALG_RP;
in
val ctr_parser =
algorithm_parser :|--
(
fn c => case c of
"relativization" => relativization_parser
| "parametricity" => parametricity_parser
| _ => error "relativization or parametricity expected"
);
end;
fun mk_msg_ctr msg = "ctr: " ^ msg;
fun mk_msg_binrel c = c ^ ": trp must consist of (stv, binary relation) pairs" ;
fun mk_msg_binrel_ftv c = c ^
": the user-specified binary relations must be defined over type variables";
fun mk_msg_no_dup_stvs c = c ^ ": duplicate stvs";
fun mk_msg_no_dup_binrel_ftvs c = c ^
": duplicate ftvs in the specification of the binary relations";
fun mk_msg_def ctxt t = Syntax.string_of_term ctxt t ^ " is not a definition";
fun check_def ctxt thm =
let
val t = Thm.full_prop_of thm
val _ = (ctxt, t) |> #2 |> Logic.is_equals
orelse error (mk_msg_def ctxt t |> mk_msg_ctr)
in () end;
fun mk_msg_no_relator c = "no relator found for the type constructor " ^ c
fun mk_msg_invalid_relator c =
"the relator found for the type constructor " ^ c ^
" is not suitable (is there is a mismatch of type variables?)"
fun preprocess_type_specs ctxt type_specs =
let
fun preprocess_entry ctxt ctxt' (T, relt) =
let
val v = T |> Syntax.parse_typ ctxt' |> dest_TVar |> #1
val relt = Syntax.read_term ctxt relt
val T = type_of relt
val _ = T |> HOLogic.is_binrelT
orelse error ("trp" |> mk_msg_binrel |> mk_msg_ctr)
val (U, V) = HOLogic.dest_binrelT T
val _ = is_TFree U andalso is_TFree V
orelse error ("trp" |> mk_msg_binrel_ftv |> mk_msg_ctr)
val S = V |> dest_TFree |> #2
in ((v, S), relt) end
val type_specs =
let val ctxt' = Proof_Context.init_global (Proof_Context.theory_of ctxt)
in map (preprocess_entry ctxt ctxt') type_specs end
val _ = type_specs |> map #1 |> has_duplicates op= |> not
orelse error ("trp" |> mk_msg_no_dup_stvs |> mk_msg_ctr)
val _ = type_specs
|> map #2
|> map (fn T => Term.add_tfrees T [])
|> flat
|> has_duplicates op=
|> not
orelse error ("trp" |> mk_msg_no_dup_binrel_ftvs |> mk_msg_ctr)
val ctxt' = type_specs
|> map (#2 #> (fn t => Term.add_frees t []))
|> flat
|> map #1
|> Variable.fix_new_vars ctxt
|> fold (Variable.declare_term) (map #2 type_specs)
in (type_specs, ctxt') end;
fun preprocess_declaration elems lthy =
let
val lthy' = Expression.read_statement elems (Element.Shows []) lthy |> #2
val assms = Assumption.local_prems_of lthy' lthy
val (assms', lthy'') = Thm.unvarify_local_fact lthy' assms
in (assms', lthy'') end;
fun preprocess_definition ctxt thm_spec =
let
val thm_spec' = apfst (apsnd (Local_Defs.meta_rewrite_rule ctxt)) thm_spec
val thm = thm_spec' |> #1 |> #2
val _ = check_def ctxt thm
val b = case thm_spec' |> #1 |> #1 of
SOME b => b
| NONE =>
let
val c = thm
|> Thm.cprop_of
|> Thm.dest_equals_lhs
|> Thm.term_of
|> head_of
|> dest_Const
|> fst
in
Binding.qualified_name_mandatory
(CTR_Utilities.qualified_name_of_const_name c ^ ".transferred")
end
in ((b, thm_spec' |> #1 |> #2), thm_spec' |> #2) end;
fun preprocess_thm_spec ctxt type_specs thm_spec =
let
fun gen_indexed_rel_names n c = ((replicate n c), (1 upto n))
||> map Int.toString
|> op~~
|> map (op^)
val thm_spec = preprocess_definition ctxt thm_spec
val ftvs = thm_spec
|> (#1 #> #2 #> Thm.full_prop_of #> (fn t => Term.add_tvars t []))
|> distinct op=
|> subtract op= (map #1 type_specs)
val (cs, ctxt') =
Variable.variant_fixes (gen_indexed_rel_names (length ftvs) "A") ctxt
val Ss = map #2 ftvs
val (lhsTs, ctxt'') = Variable.invent_types Ss ctxt' |>> map TFree
val (rhsTs, ctxt''') = Variable.invent_types Ss ctxt'' |>> map TFree
val ts = map Free (cs ~~ map HOLogic.mk_binrelT (lhsTs ~~ rhsTs))
val ctxt'''' = fold Variable.declare_term ts ctxt'''
val type_specs = type_specs @ (ftvs ~~ ts)
in ((thm_spec, type_specs), ctxt'''') end;
fun preprocess_synthesis (synthesis : (string * thm list option) option) =
case synthesis of
SOME (_, thm_opt) =>
(
case thm_opt of
SOME simp_spec => (true, SOME simp_spec)
| NONE => (true, NONE)
)
| NONE => (false, NONE);
fun apply_algorithm ctxt' alg synthesis assms type_specs thm_spec =
let
fun mk_msg_relator f T = T
|> dest_Type
|> #1
|> f
|> mk_msg_ctr
fun mk_error_no_relator T = mk_msg_relator mk_msg_no_relator T
fun mk_error_invalid_relator T = mk_msg_relator mk_msg_invalid_relator T
val alg_out = case alg of
relativization =>
(
CTR_Relativization.apply ctxt' synthesis assms type_specs thm_spec
handle
TYPE ("pr_of_typ: no relator", [T], []) =>
error (mk_error_no_relator T)
| TYPE ("pr_of_typ: invalid relator", [T], []) =>
error (mk_error_invalid_relator T)
)
| parametricity => CTR_Parametricity.apply
ctxt' synthesis assms type_specs thm_spec
in alg_out end;
fun postprocess_alg_out b mf alg_out ctxt = case alg_out of
ALGRelativization thm =>
CTR_Postprocessing.postprocess_relativization b mf thm ctxt
| ALGParametricity thm =>
CTR_Postprocessing.postprocess_parametricity b thm ctxt
| ALGFailure => error "ctr: a transfer rule could not be established.";
fun process_definition ctxt' alg synthesis assms type_specs thm_spec ctxt =
let
val alg_out = thm_spec
|> #1
|> #2
|> apply_algorithm ctxt' alg synthesis assms type_specs
|> apply_alg_out (singleton (Proof_Context.export ctxt' ctxt))
in postprocess_alg_out (thm_spec |> #1 |> #1) (#2 thm_spec) alg_out ctxt end;
fun process_parametricity thm_spec lthy =
let val thm_spec' = preprocess_definition lthy thm_spec
in
process_definition lthy parametricity (false, NONE) [] [] thm_spec' lthy
end;
fun preprocess_relativization lthy synthesis elems type_specs thm_spec =
let
val synthesis' = preprocess_synthesis synthesis
val (assms, lthy') = preprocess_declaration elems lthy
val (type_specs', lthy'') = preprocess_type_specs lthy' type_specs
val ((thm_spec', type_specs''), lthy''') =
preprocess_thm_spec lthy'' type_specs' thm_spec
in ((synthesis', assms, type_specs'', thm_spec'), lthy''') end;
fun process_relativization synthesis elems type_specs thm_spec lthy =
let
val ((synthesis, assms, type_specs, thm_spec), lthy') =
preprocess_relativization lthy synthesis elems type_specs thm_spec
val lthy'' = process_definition
lthy' relativization synthesis assms type_specs thm_spec lthy
in lthy'' end;
fun process_parametricities thm_specs lthy = fold
(
fn thm_spec => fn ctxt =>
process_parametricity thm_spec ctxt |> lthy_of_pp_out
)
thm_specs
lthy;
fun process_relativizations synthesis elems type_specs thm_specs lthy =
let
fun process_relativization' thm_spec ctxt =
process_relativization synthesis elems type_specs thm_spec ctxt
|> lthy_of_pp_out
in fold process_relativization' thm_specs lthy end;
fun process_ctrs args lthy =
let
fun preprocess_thm_specs lthy =
map (apfst (apsnd (singleton (Attrib.eval_thms lthy))))
fun process_ctrs_impl (ALG_PP thm_specs) lthy =
process_parametricities (preprocess_thm_specs lthy thm_specs) lthy
| process_ctrs_impl
(ALG_RP (((synthesis, elems), type_specs), thm_specs)) lthy =
let
val thm_specs' = preprocess_thm_specs lthy thm_specs
val synthesis' = Option.map
(apsnd (Option.map ((single #> Attrib.eval_thms lthy))))
synthesis
in
process_relativizations synthesis' elems type_specs thm_specs' lthy
end
in process_ctrs_impl args lthy end;
val _ =
Outer_Syntax.local_theory
\<^command_keyword>‹ctr›
"automated synthesis of transfer rules and relativization of definitions"
(ctr_parser >> process_ctrs);
end;Theory UD_Tests
section‹Test suite for UD›
theory UD_Tests
imports
"../UD"
"../../IML_UT/IML_UT"
Complex_Main
begin
subsection‹Background›
definition (in topological_space) islimpt:: "'a ⇒ 'a set ⇒ bool"
where "islimpt x S ⟷ (∀T. x∈T ⟶ open T ⟶ (∃y∈S. y∈T ∧ y≠x))"
definition closure :: "('a::topological_space) set ⇒ 'a set"
where "closure S = S ∪ {x. islimpt x S}"
ud ‹topological_space.closed›
ud ‹islimpt›
lemma closed_with: "closed ≡ closed.with open"
unfolding closed_def closed.with_def .
definition closure_with :: "('a set ⇒ bool) ⇒ 'a set ⇒ 'a set"
where "closure_with τ ≡ λS. S ∪ {x. islimpt.with τ x S}"
lemma closure_with: "closure ≡ closure_with open"
unfolding closure_def islimpt.with closure_with_def .
subsection‹Tests›
ML_file‹UD_TEST_UNOVERLOAD_DEFINITION.ML›
ML‹
val ud_test_unoverload_definition_test_results =
ud_test_unoverload_definition.execute_test_suite_unoverload_definition
@{theory}
›
ML‹
val _ = ud_test_unoverload_definition_test_results
|> UT_Test_Suite.output_test_results true
›
endFile ‹UD_TEST_UNOVERLOAD_DEFINITION.ML›
signature UD_TEST_UNOVERLOAD_DEFINITION =
sig
type unoverload_definition_in_type
val execute_test_suite_unoverload_definition :
theory ->
(unoverload_definition_in_type, UD.ud_thm_out_type * theory)
UT_Test_Suite.test_results_suite
end;
structure ud_test_unoverload_definition : UD_TEST_UNOVERLOAD_DEFINITION =
struct
fun mk_msg_unoverload_definition_error msg = "ud: " ^ msg
type unoverload_definition_in_type =
(binding * mixfix) * (string * typ) * theory;
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;
fun test_eq_trivial thy =
let
val act_c = "UD_Tests.closed'.with"
val exp_c = ""
val b = Binding.name "closed'"
val aT = TVar (("'a", 0), \<^sort>‹topological_space›)
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)
val ud_out = (UD.trivial (@{thm closed_with}), thy)
in
UT_Test_Suite.assert_brel
"nontrivial output equivalence"
(ud_test_eq_thm thy (act_c, exp_c))
ud_out
ud_in
end;
fun test_eq_nontrivial thy =
let
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>‹topological_space›)
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)
val ud_out =
(UD.nontrivial (@{thm closure_with_def}, @{thm closure_with}), thy)
in
UT_Test_Suite.assert_brel
"nontrivial output equivalence"
(ud_test_eq_thm thy (act_c, exp_c))
ud_out
ud_in
end;
fun test_exc_extra_type_variables thy =
let
val aT = TVar (("'a", 0), \<^sort>‹type›)
val Sup_class_c = "Complete_Lattices.Sup_class"
val args : unoverload_definition_in_type =
(
(Binding.empty, NoSyn),
(Sup_class_c, Term.itselfT aT --> \<^typ>‹prop›),
thy
)
val err_msg = mk_msg_unoverload_definition_error
"specification depends on extra type variables"
in
UT_Test_Suite.assert_exception
"extra type variables" args (ERROR err_msg)
end;
fun test_exc_ud_ex thy =
let
val aT = TVar (("'a", 0), \<^sort>‹type›)
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"
in
UT_Test_Suite.assert_exception
"constant already exists" args (ERROR err_msg)
end;
fun test_exc_no_cids thy =
let
val aT = TVar (("'a", 0), \<^sort>‹type›)
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"
in
UT_Test_Suite.assert_exception
"no suitable CIs" args (ERROR err_msg)
end;
local
fun unoverload_definition_string_of_input
(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 out_c end;
fun unoverload_definition_string_of_output (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 out_c end;
fun unoverload_definition
(((b, mixfix), (c, T), thy) : unoverload_definition_in_type) =
UD.unoverload_definition (b, mixfix) (c, T) thy;
in
fun mk_test_suite_unoverload_definition thy =
let
val test_suite_unoverload_definition = UT_Test_Suite.init
"unoverload_definition"
unoverload_definition
unoverload_definition_string_of_input
unoverload_definition_string_of_output
in
test_suite_unoverload_definition
|> test_eq_trivial thy
|> test_eq_nontrivial thy
|> test_exc_extra_type_variables thy
|> test_exc_ud_ex thy
|> test_exc_no_cids thy
end;
end;
fun execute_test_suite_unoverload_definition thy =
UT_Test_Suite.execute (mk_test_suite_unoverload_definition thy)
end;Theory CTR_Tests
section‹A test suite for CTR›
theory CTR_Tests
imports
"../CTR"
"../../IML_UT/IML_UT"
Complex_Main
keywords "ctr_test" :: thy_defn
begin
subsection‹Background›
ML‹
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 extend = I
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;
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>‹ctr_test›
"test setup for the command ctr"
(ctr_test_parser >> process_ctr_test_data);
›
ud ‹order.mono›
ud mono' ‹mono›
definition mono_ow ::
"'a set ⇒ ('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ bool"
where "mono_ow UB leb lea f ≡ ∀x∈UB. ∀y∈UB. lea x y ⟶ leb (f x) (f y)"
typedef 'a K = ‹{xs::'a list. length xs = 2}›
by (simp add: Ex_list_of_length)
definition KK :: "'a K ⇒ 'a K ⇒ bool"
where "KK k1 k2 ≡ k1 = k2"
typedef 'a L = ‹{xs::'a list. length xs = 2}›
by (simp add: Ex_list_of_length)
definition LL :: "'a L ⇒ 'a L ⇒ bool"
where "LL k1 k2 ≡ k1 = k2"
definition rel_L ::
"('a::group_add ⇒ 'b::group_add ⇒ bool) ⇒ 'a::group_add L ⇒ 'b::group_add L ⇒ bool"
where "rel_L A b c = True"
ctr_relator rel_L
definition not_binders_binrelT ::
"('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ bool) ⇒ 'a ⇒ 'b ⇒ bool"
where "not_binders_binrelT R1 R2 a b = True"
definition no_dup_binrelT ::
"('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'b ⇒ bool"
where "no_dup_binrelT R1 R2 a b = True"
definition not_binders_binrelT_ftv_stv ::
"('a ⇒ 'b ⇒ bool) ⇒ (nat ⇒ 'c ⇒ bool) ⇒ 'a ⇒ 'b ⇒ bool"
where "not_binders_binrelT_ftv_stv R1 R2 a b = True"
definition not_type_constructor_lhs ::
"('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'd ⇒ bool) ⇒ 'a ⇒ 'a K ⇒ bool"
where "not_type_constructor_lhs R1 R2 a b = True"
definition not_type_constructor_rhs ::
"('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'd ⇒ bool) ⇒ 'a K ⇒ 'e ⇒ bool"
where "not_type_constructor_rhs R1 R2 a b = True"
definition not_identical_type_constructors ::
"('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'd ⇒ bool) ⇒ 'a K ⇒ 'e L ⇒ bool"
where "not_identical_type_constructors R1 R2 a b = True"
definition not_identical_type_constructors_lhs ::
"('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'd ⇒ bool) ⇒ 'a K ⇒ 'b K ⇒ bool"
where "not_identical_type_constructors_lhs R1 R2 a b = True"
definition not_identical_type_constructors_rhs ::
"('a ⇒ 'b ⇒ bool) ⇒ 'a K ⇒ 'c K ⇒ bool"
where "not_identical_type_constructors_rhs R1 a b = True"
subsection‹Test data›
lemma mono_ow_transfer':
includes lifting_syntax
assumes [transfer_domain_rule, transfer_rule]: "Domainp B = (λx. x ∈ 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⇒'d⇒bool) = (λx. x ∈ UB)"
and [transfer_rule]: "right_total B"
trp (?'b ‹A::'a⇒'b⇒bool›) 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⇒'d⇒bool) = (λx. x ∈ 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⇒'d⇒bool) = (λx. x ∈ UB)"
and [transfer_rule]: "right_total B"
trp (?'b ‹A::nat⇒'b⇒bool›) 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⇒'d⇒bool) = (λx. x ∈ UB)"
and [transfer_rule]: "right_total B"
trp (?'b ‹A::'a⇒'b⇒bool›) 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⇒'d⇒bool) = (λx. x ∈ UB)"
and [transfer_rule]: "right_total B"
trp (?'b ‹A::'a⇒'d⇒bool›) 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⇒'d⇒bool) = (λx. x ∈ UB)"
and [transfer_rule]: "right_total B"
trp (?'b ‹A::'a⇒'b⇒bool›) 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⇒'d⇒bool) = (λx. x ∈ UB)"
and [transfer_rule]: "right_total B"
trp (?'b ‹A::'a⇒'b⇒bool›) and (?'a B)
in LL_def
subsection‹Tests›
subsubsection‹‹process_relativization››
ML_file‹CTR_TEST_PROCESS_RELATIVIZATION.ML›
context
includes lifting_syntax
begin
ML‹
val ctr_test_process_relativization_test_results =
ctr_test_process_relativization.execute_test_suite_process_relativization
@{context}
›
ML‹
val _ = ctr_test_process_relativization_test_results
|> UT_Test_Suite.output_test_results true
›
end
subsubsection‹‹process_ctr_relator››
ML_file‹CTR_TEST_PROCESS_CTR_RELATOR.ML›
ML‹
val ctr_test_process_ctr_relator_test_results =
ctr_test_process_ctr_relator.execute_test_suite_process_ctr_relator
@{context}
›
ML‹
val _ = ctr_test_process_ctr_relator_test_results
|> UT_Test_Suite.output_test_results true
›
endFile ‹CTR_TEST_PROCESS_RELATIVIZATION.ML›
signature CTR_TEST_PROCESS_RELATIVIZATION =
sig
type process_relativization_in_type
val execute_test_suite_process_relativization :
Proof.context -> (process_relativization_in_type, ctr_pp_out)
UT_Test_Suite.test_results_suite
end;
structure ctr_test_process_relativization : CTR_TEST_PROCESS_RELATIVIZATION =
struct
fun mk_msg_ctr_error msg = "ctr: " ^ msg
type process_relativization_in_type =
(
(string * thm list option) option *
Element.context list *
(string * string) list *
((binding option * thm) * mixfix)
) * Proof.context;
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) =
Thm.eq_thm (fst args1, fst args2)
| process_relativization_test_eq (_, _) = false;
end;
fun test_eq_trivial ctxt =
let
val {synthesis, elems, type_specs, thm_specs, ...} =
ctr_test_data_of_proof ctxt "mono_with" |> the
val process_relativization_in =
((synthesis, elems, type_specs, the_single thm_specs), ctxt)
val process_relativization_out =
PPRelativization ((@{thm mono_ow_def}, @{thm mono_ow_transfer'}), ctxt)
in
UT_Test_Suite.assert_brel
"output equivalence"
process_relativization_test_eq
process_relativization_out
process_relativization_in
end;
fun test_exc_def ctxt =
let
val {synthesis, elems, type_specs, thm_specs, ...} =
ctr_test_data_of_proof ctxt "exI" |> the
val args =
((synthesis, elems, type_specs, the_single thm_specs), ctxt)
val err_msg = mk_msg_ctr_error
(
Syntax.string_of_term ctxt (Thm.full_prop_of @{thm exI}) ^
" is not a definition"
)
in UT_Test_Suite.assert_exception "not a definition" args (ERROR err_msg) end;
fun test_exc_binrel ctxt =
let
val {synthesis, elems, type_specs, thm_specs, ...} =
ctr_test_data_of_proof ctxt "binrel" |> the
val args = ((synthesis, elems, type_specs, the_single thm_specs), ctxt)
val err_msg = mk_msg_ctr_error
"trp: trp must consist of (stv, binary relation) pairs"
in UT_Test_Suite.assert_exception "binary relation" args (ERROR err_msg) end;
fun test_exc_binrel_ftv ctxt =
let
val {synthesis, elems, type_specs, thm_specs, ...} =
ctr_test_data_of_proof ctxt "binrel_ftv" |> the
val args = ((synthesis, elems, type_specs, the_single thm_specs), ctxt)
val err_msg = mk_msg_ctr_error
"trp: the user-specified binary relations must " ^
"be defined over type variables"
in
UT_Test_Suite.assert_exception "binary relation ftv" args (ERROR err_msg)
end;
fun test_exc_dup_stvs ctxt =
let
val {synthesis, elems, type_specs, thm_specs, ...} =
ctr_test_data_of_proof ctxt "dup_stvs" |> the
val args = ((synthesis, elems, type_specs, the_single thm_specs), ctxt)
val err_msg = mk_msg_ctr_error "trp: duplicate stvs"
in UT_Test_Suite.assert_exception "duplicate stv" args (ERROR err_msg) end;
fun test_exc_dup_binrel_ftvs ctxt =
let
val {synthesis, elems, type_specs, thm_specs, ...} =
ctr_test_data_of_proof ctxt "dup_binrel_ftvs" |> the
val args = ((synthesis, elems, type_specs, the_single thm_specs), ctxt)
val err_msg = mk_msg_ctr_error
"trp: duplicate ftvs in the specification of the binary relations"
in
UT_Test_Suite.assert_exception "duplicate binrel ftvs" args (ERROR err_msg)
end;
fun test_exc_no_relator ctxt =
let
val {synthesis, elems, type_specs, thm_specs, ...} =
ctr_test_data_of_proof ctxt "no_relator" |> the
val args = ((synthesis, elems, type_specs, the_single thm_specs), ctxt)
val err_msg = mk_msg_ctr_error
"no relator found for the type constructor CTR_Tests.K"
in
UT_Test_Suite.assert_exception "no relator" args (ERROR err_msg)
end;
fun test_exc_invalid_relator ctxt =
let
val {synthesis, elems, type_specs, thm_specs, ...} =
ctr_test_data_of_proof ctxt "invalid_relator" |> the
val args = ((synthesis, elems, type_specs, the_single thm_specs), ctxt)
val err_msg = mk_msg_ctr_error
(
"the relator found for the type constructor CTR_Tests.L " ^
"is not suitable (is there is a mismatch of type variables?)"
)
in
UT_Test_Suite.assert_exception "no relator" args (ERROR err_msg)
end;
local
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 process_relativization_string_of_input 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 out_c end;
fun process_relativization
(
((synthesis, assms, type_specs, thm_spec), lthy) :
process_relativization_in_type
) = CTR.process_relativization synthesis assms type_specs thm_spec lthy;
in
fun mk_test_suite_process_relativization ctxt =
let
val test_suite_process_relativization = UT_Test_Suite.init
"process_relativization"
process_relativization
(process_relativization_string_of_input ctxt)
string_of_pp_out
in
test_suite_process_relativization
|> test_eq_trivial ctxt
|> test_exc_def ctxt
|> test_exc_binrel ctxt
|> test_exc_binrel_ftv ctxt
|> test_exc_dup_stvs ctxt
|> test_exc_dup_binrel_ftvs ctxt
|> test_exc_no_relator ctxt
|> test_exc_invalid_relator ctxt
end;
end;
fun execute_test_suite_process_relativization ctxt =
UT_Test_Suite.execute (mk_test_suite_process_relativization ctxt)
end;File ‹CTR_TEST_PROCESS_CTR_RELATOR.ML›
signature CTR_TEST_PROCESS_CTR_RELATOR =
sig
type process_ctr_relator_in_type
val execute_test_suite_process_ctr_relator :
Proof.context -> (process_ctr_relator_in_type, local_theory)
UT_Test_Suite.test_results_suite
end;
structure ctr_test_process_ctr_relator : CTR_TEST_PROCESS_CTR_RELATOR =
struct
fun mk_msg_ctr_relator msg = "ctr_relator: " ^ msg;
type process_ctr_relator_in_type = string * Proof.context;
fun test_exc_not_const ctxt =
let
val c = "a + b"
val args = (c, ctxt)
val err_msg = mk_msg_ctr_relator "the input must be a constant term"
in UT_Test_Suite.assert_exception "not a constant" args (ERROR err_msg) end;
fun test_exc_not_body_bool ctxt =
let
val c = "Cons"
val args = (c, ctxt)
val err_msg = mk_msg_ctr_relator
"the body of the type of the input must be bool"
in UT_Test_Suite.assert_exception "not bool body" args (ERROR err_msg) end;
fun test_exc_not_binders_2 ctxt =
let
val c = "Ex"
val args = (c, ctxt)
val err_msg = mk_msg_ctr_relator
"the type of the input must have more than two binders"
in UT_Test_Suite.assert_exception "not two binders" args (ERROR err_msg) end;
fun test_exc_not_binders_binrelT ctxt =
let
val c = "not_binders_binrelT"
val args = (c, ctxt)
val err_msg = mk_msg_ctr_relator
"all of the binders associated with the type of the input" ^
"except the last two must be the binary relation types"
in
UT_Test_Suite.assert_exception
"not binary relation types" args (ERROR err_msg)
end;
fun test_exc_no_dup_binrelT ctxt =
let
val c = "no_dup_binrelT"
val args = (c, ctxt)
val err_msg = mk_msg_ctr_relator
"the types of the binders of the binary relations associated " ^
"with the type of the input must have no duplicates"
in
UT_Test_Suite.assert_exception
"no duplicates in the binary relation types" args (ERROR err_msg)
end;
fun test_exc_not_binders_binrelT_ftv_stv ctxt =
let
val c = "not_binders_binrelT_ftv_stv"
val args = (c, ctxt)
val err_msg = mk_msg_ctr_relator
"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"
in
UT_Test_Suite.assert_exception
"not binrel type ftv or stv" args (ERROR err_msg)
end;
fun test_exc_not_type_constructor_lhs ctxt =
let
val c = "not_type_constructor_lhs"
val args = (c, ctxt)
val err_msg = mk_msg_ctr_relator
"the last two binders of the input type must be " ^
"the results of an application of a type constructor"
in
UT_Test_Suite.assert_exception
"not type constructor lhs" args (ERROR err_msg)
end;
fun test_exc_not_type_constructor_rhs ctxt =
let
val c = "not_type_constructor_rhs"
val args = (c, ctxt)
val err_msg = mk_msg_ctr_relator
"the last two binders of the input type must be " ^
"the results of an application of a type constructor"
in
UT_Test_Suite.assert_exception
"not type constructor rhs" args (ERROR err_msg)
end;
fun test_exc_not_identical_type_constructors_lhs ctxt =
let
val c = "not_identical_type_constructors_lhs"
val args = (c, ctxt)
val err_msg = mk_msg_ctr_relator
"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"
in
UT_Test_Suite.assert_exception
"not identical type constructors lhs" args (ERROR err_msg)
end;
fun test_exc_not_identical_type_constructors_rhs ctxt =
let
val c = "not_identical_type_constructors_rhs"
val args = (c, ctxt)
val err_msg = mk_msg_ctr_relator
"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"
in
UT_Test_Suite.assert_exception
"not identical type constructors rhs" args (ERROR err_msg)
end;
local
fun process_ctr_relator_string_of_input
(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 out_c end;
fun process_ctr_relator ((c, ctxt) : process_ctr_relator_in_type) =
CTR_Relators.process_ctr_relator c ctxt;
in
fun mk_test_suite_process_ctr_relator ctxt =
let
val test_suite_process_ctr_relator = UT_Test_Suite.init
"process_ctr_relator"
process_ctr_relator
process_ctr_relator_string_of_input
(fn _ => "lthy: unknown local theory")
in
test_suite_process_ctr_relator
|> test_exc_not_const ctxt
|> test_exc_not_body_bool ctxt
|> test_exc_not_binders_2 ctxt
|> test_exc_not_binders_binrelT ctxt
|> test_exc_no_dup_binrelT ctxt
|> test_exc_not_binders_binrelT_ftv_stv ctxt
|> test_exc_not_type_constructor_lhs ctxt
|> test_exc_not_type_constructor_rhs ctxt
|> test_exc_not_identical_type_constructors_lhs ctxt
|> test_exc_not_identical_type_constructors_rhs ctxt
end;
end;
fun execute_test_suite_process_ctr_relator ctxt =
UT_Test_Suite.execute (mk_test_suite_process_ctr_relator ctxt)
end;Theory Reference_Prerequisites
section‹Reference prerequisites›
theory Reference_Prerequisites
imports "HOL-Library.LaTeXsugar"
begin
ML_file ‹~~/src/Doc/antiquote_setup.ML›
notation rel_fun (infixr "===>" 55)
notation map_fun (infixr "--->" 55)
end
File ‹~~/src/Doc/antiquote_setup.ML›
structure Antiquote_Setup: sig end =
struct
fun translate f = Symbol.explode #> map f #> implode;
val clean_string = translate
(fn "_" => "\\_"
| "#" => "\\#"
| "$" => "\\$"
| "%" => "\\%"
| "<" => "$<$"
| ">" => "$>$"
| "{" => "\\{"
| "|" => "$\\mid$"
| "}" => "\\}"
| "‐" => "-"
| c => c);
fun clean_name "…" = "dots"
| clean_name ".." = "ddot"
| clean_name "." = "dot"
| clean_name "_" = "underscore"
| clean_name "{" = "braceleft"
| clean_name "}" = "braceright"
| clean_name s = s |> translate (fn "_" => "-" | "‐" => "-" | c => c);
local
fun ml_val (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read ");"
| ml_val (toks1, toks2) =
ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";
fun ml_op (toks1, []) = ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read ");"
| ml_op (toks1, toks2) =
ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";
fun ml_type (toks1, []) = ML_Lex.read "val _ = NONE : (" @ toks1 @ ML_Lex.read ") option;"
| ml_type (toks1, toks2) =
ML_Lex.read "val _ = [NONE : (" @ toks1 @ ML_Lex.read ") option, NONE : (" @
toks2 @ ML_Lex.read ") option];";
fun ml_exception (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : exn);"
| ml_exception (toks1, toks2) =
ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read " -> exn);";
fun ml_structure (toks, _) =
ML_Lex.read "functor XXX() = struct structure XX = " @ toks @ ML_Lex.read " end;";
fun ml_functor (Antiquote.Text tok :: _, _) =
ML_Lex.read "ML_Env.check_functor " @
ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok))
| ml_functor _ = raise Fail "Bad ML functor specification";
val is_name =
ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.Long_Ident);
fun ml_name txt =
(case filter is_name (ML_Lex.tokenize txt) of
toks as [_] => ML_Lex.flatten toks
| _ => error ("Single ML name expected in input: " ^ quote txt));
fun prep_ml source =
(#1 (Input.source_content source), ML_Lex.read_source source);
fun index_ml name kind ml = Thy_Output.antiquotation_raw name
(Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input)))
(fn ctxt => fn (source1, opt_source2) =>
let
val (txt1, toks1) = prep_ml source1;
val (txt2, toks2) =
(case opt_source2 of
SOME source => prep_ml source
| NONE => ("", []));
val txt =
if txt2 = "" then txt1
else if kind = "type" then txt1 ^ " = " ^ txt2
else if kind = "exception" then txt1 ^ " of " ^ txt2
else if Symbol_Pos.is_identifier (Long_Name.base_name (ml_name txt1))
then txt1 ^ ": " ^ txt2
else txt1 ^ " : " ^ txt2;
val txt' = if kind = "" then txt else kind ^ " " ^ txt;
val pos = Input.pos_of source1;
val _ =
ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2))
handle ERROR msg => error (msg ^ Position.here pos);
val kind' = if kind = "" then "ML" else "ML " ^ kind;
in
Latex.block
[Latex.string ("\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}"),
Thy_Output.verbatim ctxt txt']
end);
in
val _ =
Theory.setup
(index_ml \<^binding>‹index_ML› "" ml_val #>
index_ml \<^binding>‹index_ML_op› "infix" ml_op #>
index_ml \<^binding>‹index_ML_type› "type" ml_type #>
index_ml \<^binding>‹index_ML_exception› "exception" ml_exception #>
index_ml \<^binding>‹index_ML_structure› "structure" ml_structure #>
index_ml \<^binding>‹index_ML_functor› "functor" ml_functor);
end;
val _ =
Theory.setup (Thy_Output.antiquotation_raw \<^binding>‹named_thms›
(Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
(fn ctxt =>
map (fn (thm, name) =>
Output.output
(Document_Antiquotation.format ctxt
(Document_Antiquotation.delimit ctxt (Thy_Output.pretty_thm ctxt thm))) ^
enclose "\\rulename{" "}" (Output.output name))
#> space_implode "\\par\\smallskip%\n"
#> Latex.string #> single
#> Thy_Output.isabelle ctxt));
local
fun no_check (_: Proof.context) (name, _: Position.T) = name;
fun check_keyword ctxt (name, pos) =
if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then name
else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos);
fun check_system_option ctxt arg =
(Completion.check_option (Options.default ()) ctxt arg; true)
handle ERROR _ => false;
val arg = enclose "{" "}" o clean_string;
fun entity check markup binding index =
Thy_Output.antiquotation_raw
(binding |> Binding.map_name (fn name => name ^
(case index of NONE => "" | SOME true => "_def" | SOME false => "_ref")))
(Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name_position))
(fn ctxt => fn (logic, (name, pos)) =>
let
val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding);
val hyper_name =
"{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
val hyper =
enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";
val idx =
(case index of
NONE => ""
| SOME is_def =>
"\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
val _ =
if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else ();
val latex =
idx ^
(Output.output name
|> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
|> hyper o enclose "\\mbox{\\isa{" "}}");
in Latex.string latex end);
fun entity_antiqs check markup kind =
entity check markup kind NONE #>
entity check markup kind (SOME true) #>
entity check markup kind (SOME false);
in
val _ =
Theory.setup
(entity_antiqs no_check "" \<^binding>‹syntax› #>
entity_antiqs Outer_Syntax.check_command "isacommand" \<^binding>‹command› #>
entity_antiqs check_keyword "isakeyword" \<^binding>‹keyword› #>
entity_antiqs check_keyword "isakeyword" \<^binding>‹element› #>
entity_antiqs Method.check_name "" \<^binding>‹method› #>
entity_antiqs Attrib.check_name "" \<^binding>‹attribute› #>
entity_antiqs no_check "" \<^binding>‹fact› #>
entity_antiqs no_check "" \<^binding>‹variable› #>
entity_antiqs no_check "" \<^binding>‹case› #>
entity_antiqs Document_Antiquotation.check "" \<^binding>‹antiquotation› #>
entity_antiqs Document_Antiquotation.check_option "" \<^binding>‹antiquotation_option› #>
entity_antiqs Document_Marker.check "" \<^binding>‹document_marker› #>
entity_antiqs no_check "isasystem" \<^binding>‹setting› #>
entity_antiqs check_system_option "isasystem" \<^binding>‹system_option› #>
entity_antiqs no_check "" \<^binding>‹inference› #>
entity_antiqs no_check "isasystem" \<^binding>‹executable› #>
entity_antiqs Isabelle_Tool.check "isatool" \<^binding>‹tool› #>
entity_antiqs ML_Context.check_antiquotation "" \<^binding>‹ML_antiquotation› #>
entity_antiqs (K JEdit.check_action) "isasystem" \<^binding>‹action›);
end;
end;
Theory CTR_Introduction
section‹Introduction›
theory CTR_Introduction
imports Main
begin
subsection‹Background›
text‹
The framework ‹Conditional Transfer Rule› provides several experimental
Isabelle/Isar commands that are aimed at the automation of unoverloading
of definitions and synthesis of conditional transfer rules in Isabelle/HOL.
›
subsection‹Structure and organization›
text‹
The remainder of the reference manual is organized into two explicit sections,
one for each sub-framework of the CTR:
\begin{itemize}
\item ‹Unoverload Definition› (UD): automated elimination of sort
constraints and unoverloading of definitions
\item ‹Conditional Transfer Rule› (CTR): automated synthesis of
relativized definitions and transfer rules
\end{itemize}
It should be noted that the abbreviation CTR will be used to
refer both to the general framework and the sub-framework.
›
text‹\newpage›
endTheory UD_Reference
section‹UD›
theory UD_Reference
imports
UD
"../Reference_Prerequisites"
begin
subsection‹Introduction›
subsubsection‹Background›
text‹
This section presents a reference manual for the (sub-)framework UD.
The framework UD can be used for the elimination of sort constraints and
unoverloading of definitions in the object logic Isabelle/HOL of the
formal proof assistant Isabelle \cite{paulson_natural_1986}.
The framework UD evolved from the author's work on the extension of the
framework Types-To-Sets (see \cite{blanchette_types_2016,kuncar_types_2019},
\cite{immler_smooth_2019} and \cite{immler_automation_2019} for a
description of the framework Types-To-Sets, but not the author's extension)
and builds upon certain ideas expressed in \cite{kaufmann_mechanized_2010}.
›
subsubsection‹Purpose and scope›
text‹
The primary functionality of the framework is available via the Isabelle/Isar
command @{command ud}. This command automates the processes of the
elimination of sort constrains and unoverloading of definitions.
Thus, the command @{command ud} allows for the synthesis
of the convenience constants and theorems that are usually needed for the
application of the derivation step 2 of the original relativization algorithm
of Types-To-Sets (see \cite{blanchette_types_2016}). However,
it is expected that the command can be useful for other purposes.
›
subsubsection‹Related and previous work›
text‹
The functionality provided by the command @{command ud} shares similarities
with the functionality provided by the algorithms for the elimination of
sort constraints and elimination of overloading that were
presented in \cite{kaufmann_mechanized_2010}
and with the algorithms associated with the command
\mbox{\textbf{unoverload\_definition}} that was proposed
in \cite{immler_automation_2019}.
Nonetheless, technically, unlike \mbox{\textbf{unoverload\_definition}},
the command @{command ud} does
not require the additional axiom UO associated with Types-To-Sets for
its operation (see \cite{blanchette_types_2016},
\cite{immler_automation_2019}), it uses the definitional axioms
instead of arbitrary theorems supplied by the user
and can be used for unoverloading almost any overloaded constants,
not merely the constants overloaded using the Isabelle's type-class
infrastructure
\cite{nipkow_type_1991,wenzel_type_1997,altenkirch_constructive_2007}.
It should also be mentioned that the Isabelle/ML code from the main
distribution of Isabelle was frequently reused during the
development of the UD.
›
subsection‹Theory\label{sec:ud_theory}›
text‹
It is assumed that there exists a variable $ud_{\mathsf{with}}$ that stores theorems
of the form $c_{\tau} = c_{\mathsf{with}}\ \bar{*}$, where $c_{\tau}$ and $c_{\mathsf{with}}$ are
distinct constant-instances and $\bar{*}$ is a finite sequence of unresolvable
constant-instances, such that, if $c_{\tau}$ depends on a type
variable $\alpha_{\Upsilon}$, with $\Upsilon$ being a type class that depends
on the overloaded constants $\bar{*'}$, then $\bar{*}$ contains $\bar{*'}$
as a subsequence. The binary operation $\cup$ is defined
in a manner such that for any sequences $\bar{*}$ and $\bar{*'}$,
$\bar{*} \cup \bar{*'}$ is a sequence that consists of all elements of the
union of the elements of $\bar{*}$ and $\bar{*'}$ without duplication.
The inputs to the algorithm associated with the command @{command ud}
are assumed to be a constant-instance $c_{\sigma}$ and a well-formed
definitional theory $D$.
Given the constant-instance $c_{\sigma}$, there exists at most
one definitional axiom $c_{\tau} = \phi_{\tau}\left[\bar{*}\right]$
in $D$ such that $c_{\sigma} \leq c_{\tau}$: otherwise the orthogonality
of $D$ and, therefore, the well-formedness of $D$ are violated
($\phi$ is assumed to be parameterized by the types that it can have with
respect to the type substitution operation, and $\bar{*}$ in
$c_{\tau} = \phi_{\tau}\left[\bar{*}\right]$ is a list of all uninterpreted
constant-instances that occur in $\phi_{\tau}\left[\bar{*}\right]$).
If a definitional axiom $c_{\tau}=\phi_{\tau}\left[\bar{*}\right]$
such that $c_{\sigma} \leq c_{\tau}$ exists for the constant-instance
$c_{\sigma}$, then the following derivation is applied to it by the algorithm
\[
\infer[(6)]
{\vdash c_{\sigma} = c_{\mathsf{with}}\ \left(\bar{*} \cup \bar{*'}\right)}
{
\infer[(5)]
{
\vdash c_{\mathsf{with}}\ \left(\bar{*} \cup \bar{*'}\right) =
\phi_{\mathsf{with}}\left[\bar{*} \cup \bar{*'}\right]
}
{
\infer[(4)]
{\vdash c_{\mathsf{with}}\ ?\bar{f} = \phi_{\mathsf{with}}\left[?\bar{f}\right]}
{
\infer[(3)]
{\vdash c_{\mathsf{with}} = (\lambda \bar{f}.\ \phi_{\mathsf{with}}\left[\bar{f}\right])}
{
\infer[(2)]
{\vdash c_{\sigma}=\phi_{\mathsf{with}}\left[\bar{*} \cup \bar{*'}\right]}
{
\infer[(1)]
{\vdash c_{\sigma}=\phi_{\sigma}\left[\bar{*}\right]}
{\vdash c_{\tau}=\phi_{\tau}\left[\bar{*}\right]}
}
}
}
}
}
\]
In step 1, the previously established property $c_{\sigma} \leq c_{\tau}$ is
used to create the (extended variant of the) type substitution map $\rho$
such that $\sigma = \rho \left( \tau \right)$ (see \cite{kuncar_types_2015})
and perform the type substitution in
$c_{\tau}=\phi_{\tau}\left[\bar{*}\right]$ to obtain
$c_{\sigma}=\phi_{\sigma}\left[\bar{*}\right]$; in step 2, the
collection of theorems $ud_{\mathsf{with}}$ is unfolded, using it as
a term rewriting system, possibly introducing further uninterpreted constants
$\bar{*'}$; in step 3, the term on the right hand side of the
theorem is processed by removing the sort constraints from all type variables
that occur in it, replacing every uninterpreted constant-instance (this
excludes all built-in constants of Isabelle/HOL) that occurs in
it by a fresh term variable,
and applying the abstraction until the resulting term is closed:
this term forms the right hand side of a new definitional axiom
of a fresh constant $c_{\mathsf{with}}$ (if the conditions associated with the
definitional principles of Isabelle/HOL \cite{yang_comprehending_2017} are
satisfied); step 4 is justified by the beta-contraction; step 5 is a
substitution of the uninterpreted constants $\bar{*} \cup \bar{*'}$;
step 6 follows trivially from the results of the application of steps 2 and 5.
Assuming that the definitional axiom for the input to the
algorithm $c_{\sigma}$ does not have any occurrences of uninterpreted
constants and there is exactly one type-variable $\alpha_{\Upsilon}$ that occurs
in $c_{\sigma}$, with $\Upsilon$ being a type class that depends on the
overloaded constants $\bar{*}$, the algorithm can be restated as follows:
\[
\infer[(6)]
{\vdash c_{\sigma}\left[?\alpha_{\Upsilon}\right] = c_{\mathsf{with}}\left[?\alpha_{\Upsilon}\right]\ \bar{*}}
{
\infer[(5)]
{
\vdash c_{\mathsf{with}}\left[?\alpha_{\Upsilon}\right]\ \bar{*} = \phi_{\mathsf{with}}\left[?\alpha_{\Upsilon}, \bar{*}\right]
}
{
\infer[(4)]
{\vdash c_{\mathsf{with}}\left[?\alpha\right]\ ?\bar{f}\left[?\alpha\right] = \phi_{\mathsf{with}}\left[?\alpha, ?\bar{f}\right]}
{
\infer[(3)]
{\vdash c_{\mathsf{with}}\left[?\alpha\right] = (\lambda \bar{f}\left[?\alpha\right].\ \phi_{\mathsf{with}}\left[?\alpha, \bar{f}\right])}
{
\infer[(2)]
{\vdash c_{\sigma}\left[?\alpha_{\Upsilon}\right] = \phi_{\mathsf{with}}\left[?\alpha_{\Upsilon}, \bar{*}\right]}
{
\infer[(1)]
{\vdash c_{\sigma}\left[?\alpha_{\Upsilon}\right] = \phi_{\sigma}\left[?\alpha_{\Upsilon}\right]}
{\vdash c_{\tau}\left[?\alpha\right]=\phi_{\tau}\left[?\alpha\right]}
}
}
}
}
}
\]
The implementation of the command @{command ud} closely follows the steps of
the algorithm outlined above. Thus, at the end of the successful
execution, the command declares the constant $c_{\mathsf{with}}$ and stores the
constant-instance definition that is obtained at the end of step 3 of
the algorithm UD; furthermore, the command stores the theorem that is
obtained after the execution of step 6 of the algorithm.
Unlike the classical overloading elimination algorithm,
the algorithm employed in the implementation
of the command @{command ud} is not recursive. Thus, the users are responsible
for maintaining an adequate collection of theorems $ud_{\mathsf{with}}$.
Nonetheless, in this case, the users can provide their own
unoverloaded constants $c_{\mathsf{with}}$ and the associated theorems
$c_{\sigma} = c_{\mathsf{with}}\ \bar{*}$ for any constant-instance $c_{\sigma}$.
From the perspective of the relativization algorithm associated with
Types-To-Sets this can be useful because there is no
guarantee that the automatically synthesized constants $c_{\mathsf{with}}$
will possess desirable parametricity characteristics
(e.g., see \cite{kuncar_types_2015} and \cite{immler_smooth_2019}).
Unfortunately, the implemented algorithm still suffers from the fundamental
limitation that was already outlined in \cite{kaufmann_mechanized_2010},
\cite{blanchette_types_2016} and \cite{kuncar_types_2019}:
it does not offer a solution for handling the
constants whose types contain occurrences of the type constructors whose
type definitions contain occurrences of unresolvable overloading.
›
subsection‹Syntax›
text‹
This subsection presents the syntactic categories that are associated with the
command @{command ud}. It is important to note that the presentation is
only approximate.
›
text‹
\begin{matharray}{rcl}
@{command_def "ud"} & : & ‹theory → theory›\\
\end{matharray}
┉
\<^rail>‹@@{command ud} binding? const mixfix?›
➧ ⬚‹ud› (‹b›) ‹const› (‹mixfix›) provides access to the algorithm for
the elimination of sort constraints and unoverloading of definitions
that was described in subsection \ref{sec:ud_theory}.
The optional binding ‹b› is used for the specification
of the names of the entities added by the command to the theory and the
optional argument ‹mixfix› is used for the specification
of the concrete inner syntax for the constant in the usual manner
(e.g., see \cite{wenzel_isabelle/isar_2019-1}).
If either ‹b› or ‹mixfix› are not specified by the user, then the command
introduces sensible defaults. Following the specification of the
definition of the constant, an additional theorem that establishes
the relationship between the newly introduced constant and the
constant provided by the user as an input is established and added
to the dynamic fact @{thm [source] ud_with}.
›
subsection‹Examples\label{sec:ud_ex}›
text‹
In this subsection, some of the capabilities of the framework UD are
demonstrated by example. The examples that are presented in this subsection are
expected to be sufficient for beginning an independent exploration of the
framework, but do not cover the entire spectrum of the functionality
and the problems that one may encounter while using it.
›
subsubsection‹Type classes›
text‹
We begin the exploration of the capabilities of the framework by considering
the constant @{const mono}.
The constant @{const mono} is an overloaded constant that is defined
in the standard library of Isabelle/HOL \cite{noauthor_isabellehol_2020} as
\begin{center}
@{thm [names_short = true] mono_def[no_vars]}
\end{center}
for any @{term [show_sorts] "f::'a::order⇒'b::order"}.
Technically, there exist two distinct constants that are associated with
the definition of the constant @{const mono}
(see, e.g., \cite{berardi_local_2009}
for further details): @{const order.mono} that is provided by the
Isabelle system automatically and the constant @{const mono} itself.
The constants are unoverloaded successively using the command @{command ud}:
›
ud ‹order.mono›
ud mono' ‹mono›
text‹
The invocation of the commands above declares the constant @{const mono.with}
that is defined as
\begin{center}
@{thm mono.with_def[no_vars]}
\end{center}
and provides the theorem @{thm [source] mono.with} given by
\begin{center}
@{thm mono.with[no_vars]}
\end{center}
and the theorem @{thm [source] mono'.with} given by
\begin{center}
@{thm mono'.with[no_vars]}.
\end{center}
The theorems establish the relationship between the unoverloaded constant
@{const mono.with} and the overloaded constant @{const mono}:
both theorems are automatically added to the dynamic fact
@{thm [source] ud_with}.
›
subsubsection‹Low-level overloading›
text‹
The following example closely follows Example 5 in section 5.2. in
\cite{kaufmann_mechanized_2010}.
›
consts pls :: "'a ⇒ 'a ⇒ 'a"
overloading
pls_nat ≡ "pls::nat ⇒ nat ⇒ nat"
pls_times ≡ "pls::'a × 'b ⇒ 'a × 'b ⇒ 'a × 'b"
begin
definition pls_nat :: "nat ⇒ nat ⇒ nat" where "pls_nat a b = a + b"
definition pls_times :: "'a × 'b ⇒ 'a × 'b ⇒ 'a × 'b"
where "pls_times ≡ λx y. (pls (fst x) (fst y), pls (snd x) (snd y))"
end
ud pls_nat ‹pls::nat ⇒ nat ⇒ nat›
ud pls_times ‹pls::'a × 'b ⇒ 'a × 'b ⇒ 'a × 'b›
text‹
As expected, two new unoverloaded constants are produced via
the invocations of the command @{command ud} above. The first constant,
\<^const>‹pls_nat.with›, corresponds to ‹pls::nat ⇒ nat ⇒ nat› and is given by
\begin{center}
@{thm pls_nat.with_def[no_vars]},
\end{center}
the second constant, \<^const>‹pls_times.with›, corresponds to
\begin{center}
‹pls::'a × 'b ⇒ 'a × 'b ⇒ 'a × 'b›
\end{center}
and is given by
\begin{center}
@{thm pls_times.with_def[no_vars]}.
\end{center}
The theorems that establish the relationship between the overloaded and
the unoverloaded constants are given by
\begin{center}
@{thm pls_nat.with}
\end{center}
and
\begin{center}
@{thm pls_times.with}.
\end{center}
The definitions of the constants \<^const>‹pls_nat.with› and
\<^const>‹pls_times.with› are consistent with the ones suggested in
\cite{kaufmann_mechanized_2010}. Nonetheless, of course, it is
important to keep in mind that the command @{command ud}
has a more restricted scope of applicability than the
algorithm suggested in \cite{kaufmann_mechanized_2010}.
›
text‹\newpage›
endTheory CTR_Reference
section‹CTR›
theory CTR_Reference
imports
CTR
"../UD/UD_Reference"
begin
subsection‹Introduction›
subsubsection‹Background›
text‹
This section presents a reference manual for the (sub-)framework CTR.
The framework CTR can be used for the automated synthesis of transfer rules and
relativization of definitions.
CTR evolved from the frameworks Conditional Parametricity (CP)
\cite{gilcher_conditional_2017} and Types-To-Sets
(see \cite{blanchette_types_2016} and \cite{immler_smooth_2019})
that are available as part of the main distribution of Isabelle.
However, it does not require either the axiom LT or the axiom UO
associated with the Types-To-Sets for its operation.
The framework CTR introduces the following Isabelle/Isar commands:
\[
\begin{array}{rcl}
@{command ctr} & : & ‹local_theory → local_theory›\\
@{command ctr_relator} & : & ‹local_theory → local_theory›\\
\end{array}
\]
›
subsubsection‹Purpose and scope›
text‹
The primary functionality of the CTR is available via the
command @{command ctr}. The command @{command ctr}, given a definition
of a constant, attempts to provide a conditional transfer rule for this
constant, possibly under arbitrary user-defined side conditions.
The process of the synthesis of a transfer rule for
a constant may or may not involve declaration and synthesis of a
definition of a new (relativized) constant.
The command provides an interface for the application of two
plausible algorithms for the synthesis of the transfer rules
that have a restricted and overlapping scope of applicability.
The first algorithm (\textit{CTR I}) was developed and implemented in
\cite{gilcher_conditional_2017}.
An outline of the second algorithm (\textit{CTR II})
was proposed in \cite{lammich_automatic_2013} and \cite{immler_smooth_2019}:
CTR II relies on the functionality of the
@{method transfer_prover}
(see subsection 4.6 in \cite{kuncar_types_2015}).
More details about CTR II are given in the next subsection.
The command @{command ctr_relator} can be used for the
registration of the so-called \textit{ctr-relators} that need to be provided
for every non-nullary type constructor that occurs in the type of the
constant-instance whose definition is passed as an argument to CTR II.
However, as a fallback solution, the command @{command ctr} may
use the relators that are associated with the standard BNF infrastructure
of Isabelle/HOL (e.g., see \cite{traytel_foundational_2012}).
The only necessary condition for the registration of the ctr-relators
is that they must satisfy the type-constraint
associated with the action of a BNF on relations (e.g., see
\cite{traytel_foundational_2012} or \cite{blanchette_bindings_2019}).
›
subsubsection‹Related and previous work›
text‹
As already mentioned, the framework CTR evolved from the framework
CP that is available as part of the main
distribution of Isabelle. Furthermore, CTR provides an interface to the main
functionality associated with the framework CP
and builds upon many ideas that could be associated with it.
The primary reason for the development of the command @{command ctr} instead
of extending the implementation of the existing command
@{command parametric_constant} was the philosophy of non-intervention with the
development version of Isabelle that was adopted at the onset of the design of
the CTR. Perhaps, in the future, the functionality of the aforementioned
commands can be integrated.
It should also be mentioned that the Isabelle/ML code from the main
distribution of Isabelle was frequently reused during the
development of CTR.
›
subsection‹Theory›
text‹
Assume the existence of an underlying well-formed
definitional theory $D$ and an associated HOL signature $\Sigma$.
Furthermore, assume the existence of a map $\mathsf{ctr}_{\mathsf{Rel}}$ from a
finite set of non-nullary type constructors to ctr-relators, mapping each
non-nullary type constructor in its domain to a valid ctr-relator for this
type constructor.
The inputs to CTR II are a context $\Gamma$,
a constant-instance definition
\mbox{$\vdash c_{?\bar{\gamma}\ K} = \phi\left[?\bar{\gamma}\right]$}
of the constant-instance $c_{?\bar{\gamma}\ K}$
and the map $\mathsf{trp}$ from the set of all schematic type variables
in ?$\bar{\gamma}$ to the set of (fixed) binary relations
$x_{\alpha\rightarrow\beta\rightarrow\mathbb{B}}$ in $\Gamma$
($?\bar{\gamma}$ corresponds to a sequence of all
distinct type variables that occur in the type $?\bar{\gamma}\ K$,
while $K$, applied using a postfix notation, contains all information about
the type constructors of the type $?\bar{\gamma}\ K$,
such that the non-nullary type constructors associated with $K$
form a subset of the domain of $\mathsf{ctr}_{\mathsf{Rel}}$).
CTR II consists of three parts:
\textit{synthesis of a parametricity relation},
\textit{synthesis of a transfer rule} and \textit{post-processing}.
\textbf{Synthesis of a parametricity relation}.
An outline of an algorithm for the conversion of a type to a
parametricity relation is given in subsection 4.1.1 in \cite{kuncar_types_2015}.
Thus, every nullary type constructor in $?\bar{\gamma}\ K$ is replaced
by the identity relation $=$, every non-nullary type constructor $\kappa$
in $?\bar{\gamma}\ K$ is replaced by its corresponding ctr-relator
$\mathsf{ctr}_{\mathsf{Rel}}\left(\kappa\right)$ and every type variable
$?\gamma$ in $?\bar{\gamma}\ K$ is replaced by $\mathsf{trp}\left(?\gamma\right)$,
obtaining the parametricity relation
$R_{\bar{\alpha}\ K \rightarrow \bar{\beta}\ K \rightarrow\mathbb{B}}$.
\textbf{Synthesis of a transfer rule}.
First, the goal
$R\ \left(\phi\left[\bar{\alpha}\right]\right)\ \left(\phi\left[\bar{\beta}\right]\right)$
is created in $\Gamma$ and an attempt to prove it is made
using the algorithm associated with
the method @{method transfer_prover} (see subsection 4.6 in
\cite{kuncar_types_2015}).
If the proof is successful, nothing else needs to be done in this part.
Otherwise, an attempt to find a solution for $?a$ in
$R\ \left(?a_{\bar{\alpha}\ K}\right)\ \left(\phi\left[\bar{\beta}\right]\right)$
is made, once again, using the @{method transfer_prover}
(see subsection 4.6 in \cite{kuncar_types_2015}).
Of course, the success of this part is not guaranteed
(see \cite{kuncar_types_2015} for more information).
In summary, the result of the successful completion of the synthesis
is a transfer rule
$\Gamma \vdash R\ \left(\psi\left[\bar{\alpha},\bar{x}\right]\right)\ \left(\phi\left[\bar{\beta}\right]\right)$,
where $\bar{x}$ is used to denote a sequence of typed variables,
each of which occurs free in the context $\Gamma$.
\textbf{Post-processing}. If
$\psi\left[\bar{\alpha},\bar{x}\right] = \phi\left[\bar{\alpha}\right]$
after the successful completion of part 2 of the algorithm, then
the definitions of the constant-instances $c_{\bar{\alpha}\ K}$
and $c_{\bar{\beta}\ K}$ are folded, resulting in the deduction
\mbox{$\Gamma \vdash R\ \left( c_{\bar{\alpha}\ K}\right)\ \left(c_{\bar{\beta}\ K}\right)$}. Otherwise, if
\mbox{$\psi\left[\bar{\alpha},\bar{x}\right]\ \neq \phi\left[\bar{\alpha}\right]$},
then a new constant $d$ is declared such that
\mbox{$\vdash d_{\sigma\left[?\bar{\alpha}\right]} = \left(\lambda \bar{x}.\ \psi\left[?\bar{\alpha},\bar{x}\right]\right)$},
where $\sigma$ is determined uniquely by $\bar{x}$ and $?\bar{\alpha}\ K$.
In this case,
\mbox{$\Gamma \vdash R\ \left(\psi\left[\bar{\alpha},\bar{x}\right]\right)\ \left(\phi\left[\bar{\beta}\right]\right)$}
can be restated as
\mbox{$\Gamma \vdash R\ (d_{\sigma\left[\bar{\alpha}\right]}\ \bar{x})\ \left(c_{\bar{\beta}\ K}\right)$}.
This result can be exported to the global theory context and forms a
conditional transfer rule for $c_{?\bar{\gamma}\ K}$.
›
subsection‹Syntax›
subsubsection‹Background›
text‹
This subsection presents the syntactic categories that are associated with the
command @{command ctr} and closely related auxiliary commands and attributes.
It is important to note that the presentation is only approximate.
›
subsubsection‹‹ctr_relator››
text‹
\begin{matharray}{rcl}
@{command_def ctr_relator} & : & ‹local_theory → local_theory›
\end{matharray}
┉
\<^rail>‹@@{command ctr_relator} term›
➧ ⬚‹ctr_relator› ‹c› saves the ‹ctr relator› ‹c› to a database of
ctr relators for future reference. A ctr relator is defined as any constant
that has the type of the form
\begin{center}
‹(α⇩1⇒β⇩1⇒𝔹)⇒…⇒(α⇩n⇒β⇩n⇒𝔹)⇒(α⇩1…α⇩n)κ⇒(β⇩1…β⇩n)κ⇒𝔹›,
\end{center}
where ‹α⇩1…α⇩n› and ‹β⇩1…β⇩n› are distinct type variables,
‹n› is a positive integer and ‹κ› is a type constructor.
›
subsubsection‹‹ctr››
text‹
\begin{matharray}{rcl}
@{command_def ctr} & : & ‹local_theory → local_theory› \\
\end{matharray}
┉
\<^rail>‹
@@{command ctr} (@'parametricity' | @'relativization' rlt) in_def
;
rlt:
(synthesis*)
(cce*)
trp
;
synthesis: @'synthesis' (thm*)
;
cce:
@'fixes' vars |
@'assumes' (props + @'and')
;
trp: (@'trp' ('(' type_var term ')' + @'and'))?
;
in_def: ((binding @':')? thm mixfix?) + and
›
➧ ⬚‹ctr› provides access to two algorithms for the automated synthesis of
the transfer rules and the relativization of constants based on their
definitions.
➧ @{element "parametricity"} indicates that CTR I needs
to be invoked by the command.
➧ @{element "relativization"} indicates that CTR II needs to be
invoked by the command.
➧ @{element "synthesis"} ‹thm› indicates that the relativization of the
inputs needs to be performed and post-processed using the simplifier with
the collection of rewrite rules stated as the fact ‹thm›. If the optional
argument ‹thm› is not provided, then the default ‹simpset› is used for
post-processing. If the keyword @{element "synthesis"} is omitted,
then no attempt to perform the relativization is made.
The keyword @{keyword "synthesis"} is relevant only for CTR II.
➧ @{element "trp"} ‹(?a⇩1 A⇩1)› ⬚‹and› ‹…› ⬚‹and› ‹(?a⇩n A⇩n)› indicates
that the type variable that has the indexname ‹?a⇩i› (‹1≤i≤n›,
‹n› is a non-negative integer) is meant to
correspond to the binary relation ‹A⇩i› in the transfer relation constructed by
the command prior to the statement of the transfer rule (for further
information see subsection 4.1 in \cite{kuncar_types_2015}). This is relevant only
for CTR II.
➧ @{element "in"} ‹(b:) def_thm (mixfix)› is used for
the specification of the input to the algorithms that are associated with
the command @{command ctr}. ‹def_thm› is meant to be a fact that
consists of exactly one theorem of the form
\begin{center}
‹A a⇩1…a⇩n ≃ f a⇩1…a⇩n›,
\end{center}
where ‹A› is a constant, ‹≃› is either meta- or object-equality,
‹n› is a non-negative integer,
‹a⇩1…a⇩n› are schematic variables and ‹f› is a suitable formula in ‹n›
arguments (however, there are further implicit restrictions).
If a new constant is introduced by the command, then the optional argument
‹mixfix› is used for the specification
of the concrete inner syntax for the constant
in the usual manner
(e.g. see \cite{wenzel_isabelle/isar_2019-1}). The optional binding ‹b› is
used for the specification of the names of the entities that
are provided after the successful execution of the command. It is hoped
that the algorithm chosen for the specification of the names
is sufficiently intuitive and does not require further explanation.
If either ‹b› or ‹mixfix› are not specified by the user, then the command
introduces sensible defaults.
Multiple theorems may be provided after the
keyword @{element "in"}, employing the keyword ⬚‹and› as a separator.
In this case, the parameterized algorithm associated with the command is
applied repeatedly to each input theorem in the order of their specification
from left to right and the local context is augmented incrementally.
›
subsection‹Examples\label{sec:ctr_ex}›
text‹
In this subsection, some of the capabilities of the framework CTR are
demonstrated by example. The examples that are presented in this subsection are
expected to be sufficient to begin an independent exploration of the framework,
but do not cover the entire spectrum of the functionality and the problems that
one may encounter while using it.
The examples that are presented in this subsection continue the example
of the application of the command @{command ud}
to the definition of the constant @{const mono} that was presented in
subsection \ref{sec:ud_ex}.
›
subsubsection‹CTR I›
text‹
As already explained, the command @{command ctr} can be used to invoke
the algorithm associated with the command @{command parametric_constant}
for the synthesis of the parametricity relation for a given constant. For
example, the invocation of
›
ctr parametricity
in mono: mono.with_def
text‹
generates the transfer rule @{thm [source] mono_transfer}:
\begin{center}
@{thm [display, mode=IfThenNoBox] mono_transfer[no_vars]}
\end{center}
A detailed explanation of the underlying algorithm can be found in
\cite{gilcher_conditional_2017}.
›
subsubsection‹CTR II›
text‹
The first example demonstrates how CTR II can be
used to produce a conditional parametricity property, identical
to the parametricity property produced by CTR I:
›
ctr relativization
fixes A1 :: "'a ⇒ 'b ⇒ bool" and A2 :: "'c ⇒ 'd ⇒ bool"
assumes [transfer_rule]: "bi_total A1"
trp (?'a A1) and (?'b A2)
in mono': mono.with_def
text‹
This produces the theorem @{thm [source] mono'.transfer}:
@{thm [display, mode=IfThenNoBox] mono'.transfer[no_vars]}
which is identical to the theorem @{thm [source] mono_transfer} generated
by CTR I in the previous subsection.
›
text‹
Of course, there is very little value in trying to establish a parametricity
property using CTR II due to the availability of CTR I. However,
it is often the case that the constant is not parametric under a given
set of side conditions. Nonetheless, in this case, it is often possible to
define a new (relativized) constant that is related to the original
constant under the transfer relation associated with the original constant.
It is expected that the most common application of CTR II will be the
synthesis of the relativized constants.
For example, suppose one desires to find a conditional transfer rule for
the constant @{const mono.with} such that (using the conventions from the
previous example) the relation ‹A1› is right total, but not, necessarily,
left total. While, under such restriction on the involved relations, the
constant @{const mono.with} is no longer conditionally parametric, its
relativization exists and can be found using the transfer prover. To automate
the relativization process, the user merely needs to add the keyword
@{keyword "synthesis"} immediately after the keyword
@{keyword "relativization"}:
›
ctr relativization
synthesis ctr_simps
fixes A1 :: "'a ⇒ 'b ⇒ bool" and A2 :: "'c ⇒ 'd ⇒ bool"
assumes [transfer_domain_rule]: "Domainp A1 = (λx. x ∈ U1)"
and [transfer_rule]: "right_total A1"
trp (?'a A1) and (?'b A2)
in mono_ow: mono.with_def
text‹
This produces the definition @{thm [source] mono_ow_def}:
@{thm [display, mode=IfThenNoBox] mono_ow_def[no_vars]}
and the theorem @{thm [source] mono_ow.transfer}:
@{thm [display, mode=IfThenNoBox] mono_ow.transfer[no_vars]}
It should be noted that, given that the keyword @{keyword "synthesis"} was
followed by the name of the named collection of theorems
@{thm [source] ctr_simps}, this collection was used in post-processing of
the result of the relativization. The users can omit simplification
entirely by specifying the collection @{thm [source] ctr_blank} instead
of @{thm [source] ctr_simps}.
›
text‹\newpage›
end