[isabelle] Countable instantiation addition



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 [ at {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"), [ at {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 *)

Attachment: Countable_Examples.thy
Description: application/isabelle-theory



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.