Hi all, I have written a little ML library allowing to automatically prove, in most cases, instantiations of types (typedefs, records and datatypes) as countable (see ~~/src/HOL/Library/Countable). The style of the library is still a little rough but I think it could be a nice addition to the Isabelle Library with some more work, mostly for Imperative_HOL (~~/src/HOL/Imperative_HOL) which can only store values of countable types in its heap.
However, as Lukas Bulwhan said to me, improving it and integrating it in Isabelle while nobody use it would certainly be a lost of time. So here is my question: would anybody be interested in this addition ? I attach this library with a theory containing tests/examples. Anyway, if you have some advices for improving it, they would be welcome. Regards, Mathieu Giorgino
signature COUNTABLE =
sig
(* typedef: Works for countable embedding type *)
val typedef_instantiate: string -> theory -> theory
(* records: Works for records with countable fields *)
val record_instantiate: string -> theory -> theory
(* Datatypes: works for any mutual recursive datatype which contains only:
- countable types
- or/and type parameters
- or/and mutual/recursive types
*)
(* Add a function encoding datatypes to natural numbers: "<type>_encode" *)
val dtype_add_encfun: string list -> local_theory -> local_theory
(* Add also the injectiity thm as "inj_<type1..._type<i>>_encode" *)
val dtype_add_encfun_and_injthm: string list -> local_theory -> local_theory
(* Instantiate the type as countable *)
val dtype_instantiate: string list -> theory -> theory
(* Add the encoding function and instantiate the type as countable *)
val dtype_add_encfun_and_instantiate: string list -> theory -> theory
end (* signature COUNTABLE_DATATYPE *)
structure Countable : COUNTABLE =
struct
type fun_spec = ((string * typ) * term) list
type descr_elem =
int * (string * Datatype_Data.dtyp list * (string * Datatype_Data.dtyp list) list);
type the_descr = Datatype_Data.descr * (string * sort) list * string list
* string * (string list * string list) * (typ list * typ list);
(* Replacing "o" with "x" to avoid a conflict with Fun.comp for
induction variables ... *)
fun varname_from_typname s =
String.substring (String.map Char.toLower (Long_Name.base_name s), 0, 1)
|> (fn "o" => "x" | s => s);
fun varname_from_type (t as Type (s, ts)) =
if s = @{type_name list}
then (#1 (varname_from_type (hd ts)) ^ "s", t)
else (varname_from_typname s, t)
| varname_from_type t = ("x", t);
fun lookup_or_id f xs x = (case f xs x of NONE => x | SOME t' => t')
fun fresh_typ ctxt f tys =
tys
|> (fn x => (x, x))
||> map #2
||> (fn Ss => Variable.invent_types Ss ctxt)
||> #1
||> map TFree
|>> map f
|> ListPair.zip
|> lookup_or_id (AList.lookup (op =))
fun apply_fresh_args f ts ctxt =
f
|> fastype_of
|> binder_types
|> map varname_from_type
|> Variable.variant_frees ctxt (f :: ts)
|> map Free
|> (fn x => (x, x))
|>> curry list_comb f;
fun encode_fun_name s = (Long_Name.base_name s) ^ "_encode";
fun tree_app e _ _ [] = e
| tree_app _ f1 _ [t] = f1 t
| tree_app _ _ f2 [t1, t2] = f2 t1 t2
| tree_app e f1 f2 ts =
let val n = (length ts) div 2 in
f2 (tree_app e f1 f2 (take n ts)) (tree_app e f1 f2 (drop n ts))
end;
fun tyenv_unif thy ty1 ty2 =
#1 ((Sign.typ_unify thy (ty1, ty2)) (Vartab.empty, 0))
fun tconstrs typ thy t = the ((Datatype_Data.get_constrs thy) t)
|> map (apsnd (fn t => Envir.norm_type (tyenv_unif thy (Type typ) (body_type t)) t))
|> map Const;
fun constrs typ dconstrs thy =
ListPair.zip (tconstrs typ thy (#1 typ), map #2 dconstrs);
(* TODO: detect functions whose at least one parameter is non-finite *)
(* TODO: case where a function with this name is already defined *)
fun mk_fun_spec ctxt typ constrs (mut_typs:string list) =
let
fun nth_type_name n = nth mut_typs n;
fun nth_encode_fun_name n = encode_fun_name (nth_type_name n);
val current_encode_fun_name = encode_fun_name (#1 (dest_Type typ));
fun ensure_countable (Datatype_Aux.DtRec n) t =
Free (nth_encode_fun_name n, dummyT) $ t
| ensure_countable _ t = t;
fun first_prod n = Const(@{const_name "to_nat"}, dummyT) $ HOLogic.mk_number @{typ nat} n;
fun pair_const (t1, t2) = Const (@{const_name Pair}, dummyT) $ t1 $ t2
val prods_encode_tree =
map (fn (t, v) => (ensure_countable t) v)
#> tree_app @{term "to_nat ()"} I (curry pair_const);
fun mk_fun_spec_aux [] _ ts = ts
| mk_fun_spec_aux ((constr, constr_dtyps)::constrs) n ts =
let val encode_fun = (current_encode_fun_name, typ --> @{typ nat}) in
(apply_fresh_args constr [] ctxt)
|>> curry op $ (Free encode_fun)
||> curry ListPair.zip constr_dtyps
||> prods_encode_tree
||> curry op $ (Const(@{const_name "to_nat"}, dummyT))
||> (fn t => Const(@{const_name "to_nat"}, dummyT) $ pair_const (first_prod n, t))
|> (fn (x, y) => (encode_fun, HOLogic.mk_eq (x, y)))
|> (fn t => mk_fun_spec_aux constrs (n+1) (t::ts))
end;
in
mk_fun_spec_aux constrs 0 []
end;
fun mk_fun_spec_dtype ctxt typ (the_descr:the_descr) (dtype_descr:descr_elem) =
let
val thy = ProofContext.theory_of ctxt;
val (_, (_ , _, dconstrs)) = dtype_descr;
val mut_typs = map (#1 o #2) (#1 the_descr)
in mk_fun_spec ctxt typ (constrs (dest_Type typ) dconstrs thy) mut_typs end;
fun remdups [] = []
| remdups (x::xs) = if List.exists (curry (op =) x) xs
then remdups xs
else x::(remdups xs);
fun typedef_instantiate typ_name thy0 =
let
val lthy = Named_Target.theory_init thy0
val thy = ProofContext.theory_of lthy
val typ = Syntax.parse_typ lthy typ_name
val typ_lname = (#1 o dest_Type) typ
val info = the_single (Typedef.get_info lthy typ_lname)
val rep_fun_lname = (#Rep_name o #1) info
val inj_thm = (#Rep_inject o #2) info
val enc_fun_string = "to_nat o " ^ rep_fun_lname
fun tactic ctxt =
let
val classII = RuleInsts.read_instantiate ctxt [(("f", 0), enc_fun_string)] @{thm countable_classI};
val simpset = HOL_basic_ss addsimps [@{thm "o_def"}, @{thm "to_nat_split"}, inj_thm]
in
(rtac classII THEN' asm_full_simp_tac simpset) 1
end
val sorts = Term.add_tfrees (Syntax.check_term lthy (Syntax.read_term lthy enc_fun_string)) []
|> map #2 |> rev
|> map (fn S => Sign.minimize_sort thy (append S @{sort "countable"}))
val vs = Name.names Name.context "'a" sorts
in
Local_Theory.exit_global lthy
|> Class.instantiation ([typ_lname], vs, @{sort countable})
|> (fn lthy => Class.prove_instantiation_exit (fn _ => tactic lthy) lthy)
end;
fun record_instantiate typ_name = typedef_instantiate (typ_name ^ Record.ext_typeN)
fun constrain_frees thy S (TFree (tyn, S')) =
TFree (tyn, Sign.minimize_sort thy (append S S'))
| constrain_frees thy S (Type (tyn, tys)) =
Type (tyn, map (constrain_frees thy S) tys)
| constrain_frees _ _ t = t;
fun fun_spec ctxt ss =
let
val thy = ProofContext.theory_of ctxt;
val long_tyname = #1 o dest_Type o (Syntax.parse_typ ctxt)
val the_descr = Datatype_Data.the_descr thy (map long_tyname ss)
val dtys = #1 (#6 the_descr)
in
dtys |> map (map_atyps (fresh_typ ctxt TFree (rev (fold Term.add_tfreesT dtys []))))
|> curry ListPair.zip (#1 the_descr)
|> map (fn (x, typ) =>
mk_fun_spec_dtype ctxt (constrain_frees thy @{sort "countable"} typ) the_descr x)
|> List.concat
|> (fn xs => fold (fn (s, sp) => AList.map_default (op =) (s,[]) (cons sp)) xs [])
end;
fun add_encode_fun fun_spec =
let
val (fun_names, eqs) =
ListPair.unzip fun_spec
|>> map (Long_Name.base_name o #1)
||> flat
||> map ((pair (Attrib.empty_binding)) o HOLogic.mk_Trueprop);
val funs = map (fn name => (Binding.qualified_name name, NONE, NoSyn)) fun_names
in
Function_Fun.add_fun funs eqs Function_Common.default_config
end;
fun enc_funs ctxt enc_fun_spec =
enc_fun_spec
|> map (#1 o #1)
|> remdups
|> map (Syntax.read_term ctxt);
fun inj_goal ctxt enc_fun_spec =
let
val sy = (#1 o hd) (Variable.variant_frees ctxt [] [("y", ())]);
fun constr_goal enc_fun (xs, ts, f, p) =
let
val (tency, y) = (Free (sy, (hd o binder_types o fastype_of) enc_fun))
|> (fn x => (x, x))
|>> (curry (op $) enc_fun)
val (tencx, x) = apsnd hd (apply_fresh_args enc_fun (y::ts) ctxt)
val (sy, ty) = dest_Free y
val imp = HOLogic.mk_imp (HOLogic.mk_eq (tencx, tency), HOLogic.mk_eq (x, y))
in
(x::xs, tencx::tency::ts,
(Logic.all x) o f,
HOLogic.mk_conj (HOLogic.mk_all (sy, ty, imp), p))
end;
val (xs, _, f, p) = fold constr_goal (rev (enc_funs ctxt enc_fun_spec)) ([], [], I, @{term True})
in
(sy, xs, f (HOLogic.mk_Trueprop p))
end;
fun Function_get_info ctxt t =
Item_Net.retrieve (Function_Common.get_function ctxt) t
|> hd |> #2
fun inj_thm ctxt fun_spec =
let
val {safeIs, safeEs, ...} = ctxt |> claset_of |> rep_cs
fun safe n = REPEAT (((resolve_tac safeIs) ORELSE' (eresolve_tac safeEs)) n);
fun encode_simps t = (the o #simps) (Function_get_info ctxt t);
fun case_simpset t = HOL_basic_ss addsimps ((encode_simps t) @
@{thms prod_encode_eq prod.inject to_nat_split
nat.simps Nat_Numeral.numerals Nat.One_nat_def})
val (case_var_name, vars, goal) = inj_goal ctxt fun_spec;
val vars = map (#1 o dest_Free) vars;
val induct_vars = map ((fn x => [x]) o SOME) vars;
val goal = (map_types o map_atyps) (fresh_typ ctxt TVar (Term.add_tvars goal [])) goal;
val enc_fun0 = hd (enc_funs ctxt fun_spec)
in
Goal.prove ctxt [] [] goal (fn {context, ...} =>
InductTacs.induct_tac context induct_vars 1
THEN REPEAT(
((safe THEN' (InductTacs.case_tac context case_var_name)) 1)
THEN REPEAT (CHANGED (((asm_full_simp_tac (case_simpset enc_fun0))
THEN' safe) 1))))
end
fun add_inj_thm fun_spec thm_name lthy =
Local_Theory.note
((Binding.qualified_name thm_name, []), [inj_thm lthy fun_spec]) lthy
|> snd
fun dtype_add_encfun ty_names lthy = add_encode_fun (fun_spec lthy ty_names) lthy
fun dtype_add_encfun_and_injthm ty_names lthy =
let
val fspec = fun_spec lthy ty_names
val thm_name = "inj_" ^
(String.concatWith "_" (map Long_Name.base_name ty_names))
^ "_encode"
in
add_encode_fun fspec lthy
|> Local_Theory.restore
|> add_inj_thm fspec thm_name
end
fun is_instance_of tyco class thy =
let
val algebra = Sign.classes_of thy;
in
(case Symtab.lookup (Sorts.arities_of algebra) tyco of
NONE => false
| SOME xs => exists ((curry (op =) class) o #1) xs)
end;
fun prove_instantiation fspec inj_thm thy =
let
val lthy = Named_Target.theory_init thy;
val thy = ProofContext.theory_of lthy
val enc_fun_names = map (#1 o #1) fspec
val enc_funs = enc_fun_names |> map (Syntax.read_term lthy)
val type_names = map fastype_of enc_funs
|> map (fn Type (@{type_name "fun"}, (Type (s, _)) :: _) => s
| _ => raise TERM(("Encoding function should be a function"
^ " from a fixed type to nat"), [@{term "1"}]))
val sorts = Term.add_tfrees (hd enc_funs) [] |> map #2 |> rev
val vs = Name.names Name.context "'a" sorts
fun tactic ctxt =
let
val insts = map (pair ("f", 0)) enc_fun_names
val classI = @{thm countable_classI}
val classIs = insts
|> map (fn inst => (RuleInsts.read_instantiate ctxt [inst] classI))
val simpset = HOL_basic_ss addsimps [inj_thm]
in
REPEAT (CHANGED ((resolve_tac classIs THEN' asm_full_simp_tac simpset) 1))
end
in (case filter (fn tyco => is_instance_of tyco @{class countable} thy) type_names
of [x] => (error (x ^ " is already an instance of class countable"))
| xs as _::_ => (error ("[" ^ (commas xs) ^ "] are already instances of class countable"))
| _ => Class.instantiation (type_names, vs, @{sort countable}) thy
|> (fn lthy => Class.prove_instantiation_exit (fn _ => tactic lthy) lthy))
end;
fun dtype_instantiate ty_names thy =
let
val lthy = Named_Target.theory_init thy
val fspec = fun_spec lthy ty_names
val thm = inj_thm lthy fspec
in prove_instantiation fspec thm (Local_Theory.exit_global lthy) end;
fun dtype_add_encfun_and_instantiate ty_names thy =
let
val lthy = Named_Target.theory_init thy
val fspec = fun_spec lthy ty_names
val lthy' = Local_Theory.restore (add_encode_fun fspec lthy)
val thm = inj_thm lthy' fspec
in prove_instantiation fspec thm (Local_Theory.exit_global lthy') end;
end (* structure Countable_Datatype *)
Countable_Examples.thy
Description: application/isabelle-theory
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
