File ‹derive_aux.ML›
signature DERIVE_AUX =
sig
val split_last : 'a list -> 'a list * 'a
val HOLogic_list_implies : term list * term -> term
val HOLogic_list_conj : term list -> term
val HOLogic_list_all : term list * term -> term
val rulify_only_asm : Proof.context -> thm -> thm
val inductive_thm : theory -> (term list * term list) list -> thm -> sort ->
(Proof.context -> int -> thm list -> thm list -> term list -> term list -> tactic) -> thm
val typ_subst_for_sort : theory -> Old_Datatype_Aux.info -> sort -> typ -> typ
val typ_and_vs_of_typname : theory -> string -> sort -> typ * (string * sort) list
val dt_number_recs : Old_Datatype_Aux.dtyp list -> int * (int * int) list
val my_print_tac : Proof.context -> string -> tactic
val mk_binary_thm :
(theory -> Old_Datatype_Aux.info -> sort -> 'a -> (term list * term list) list) ->
(theory -> Old_Datatype_Aux.info -> sort -> (int -> term) * ('b * int * int) list) ->
string ->
theory ->
Old_Datatype_Aux.info ->
'a ->
sort ->
(Proof.context -> thm list -> thm list -> thm -> (Proof.context -> thm list -> tactic) -> int -> term list ->
term list -> string * Old_Datatype_Aux.dtyp list -> (Old_Datatype_Aux.dtyp -> term -> term -> term) -> tactic)
-> thm
val mk_case_tac : Proof.context ->
term option list list ->
thm ->
(Proof.context * int * thm list * (string * cterm) list -> tactic)
-> tactic
val prop_trm_to_major_imp : (term list * 'a) list -> term * 'a
val mk_xs : theory -> Old_Datatype_Aux.info -> sort -> int -> int -> term
val mk_Some : term -> term
val my_simp_set : simpset
val mk_solve_with_tac : Proof.context -> thm list -> tactic -> tactic
val define_overloaded : (string * term) -> local_theory -> thm * local_theory
val define_overloaded_generic : (Attrib.binding * term) -> local_theory -> thm * local_theory
val mk_def : typ -> string -> term -> term
end
structure Derive_Aux : DERIVE_AUX =
struct
val printing = false
fun my_print_tac ctxt = if printing then print_tac ctxt else (fn _ => Seq.single)
fun split_last xs = (take (length xs - 1) xs, List.last xs)
fun HOLogic_list_implies (prems,r) = fold_rev (fn r => fn p => HOLogic.mk_imp (r,p)) prems r
fun HOLogic_list_conj [] = @{term true}
| HOLogic_list_conj [x] = x
| HOLogic_list_conj (x :: xs) = HOLogic.mk_conj (x, HOLogic_list_conj xs)
fun HOLogic_list_all (xs,p) = fold_rev (fn (x,ty) => fn p => HOLogic.mk_all (x,ty,p)) (map dest_Free xs) p
fun mk_Some t = let
val ty = fastype_of t
in
Const (@{const_name Some}, ty --> Type (@{type_name option}, [ty])) $ t
end
fun rulify_only_asm ctxt thm =
(@{thm conjI[OF TrueI]} OF [thm])
|> Object_Logic.rulify ctxt
|> (fn conj => (@{thm conjunct2} OF [conj]))
fun permute_for_ind_thm ps xs ind_thm =
let
val n = length ps
val vs_p = Thm.prop_of ind_thm |> Term.add_vars |> (fn f => f [] |> rev)
fun number_ih_vars _ [] = []
| number_ih_vars i (P :: x :: pxs) = ((P,i) :: (x,i+n) :: number_ih_vars (i+1) pxs)
| number_ih_vars _ _ = error "odd number of vars in ind-thm"
val vs_c = Thm.concl_of ind_thm |> Term.add_vars |> (fn f => f [] |> rev) |> number_ih_vars 0
val permutation = map (AList.lookup (op =) vs_c #> the) vs_p
in
map (nth (ps @ xs)) permutation
end
fun inductive_thm thy (imp_list : (term list * term list) list) ind_thm sort ind_tac =
let
val imps = map
(fn (imps,xs) => HOLogic_list_all (tl xs, HOLogic_list_implies (split_last imps)))
imp_list
val ind_term =
HOLogic_list_conj imps
|> HOLogic.mk_Trueprop
val nr_prems = length (hd imp_list |> fst) - 1
val nr_arbi = length (hd imp_list |> snd) - 1
val xs = map (snd #> hd) imp_list
val ps = xs ~~ imps
|> map (fn (x,imp) => lambda x imp)
val insts = permute_for_ind_thm ps xs ind_thm
val xs_strings = map (dest_Free #> fst) xs
val conjunctive_thm = Goal.prove_global_future thy xs_strings [] ind_term
(fn {context = ctxt, ...} =>
let
val ind_thm_inst = infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) insts) ind_thm
val ind_thm' = rulify_only_asm (Proof_Context.init_global thy) ind_thm_inst
in
(DETERM o Induct.induct_tac ctxt false [] [] [] (SOME [ind_thm']) [])
THEN_ALL_NEW
(fn i => Subgoal.SUBPROOF
(fn {context = ctxt, prems = prems, params = iparams, ...} =>
let
val m = length prems - nr_prems
val ih_prems = drop m prems
val ih_hyps = take m prems
val tparams = map (snd #> Thm.term_of) iparams
val m' = length tparams - nr_arbi
val arbi_vars = drop m' tparams
val case_vars = take m' tparams
in
ind_tac ctxt (i-1) ih_hyps ih_prems case_vars arbi_vars
end
) ctxt i
)
end 1
)
val first_conj = if length imp_list > 1 then @{thm conjunct1} OF [conjunctive_thm] else conjunctive_thm
val elim_spec = funpow nr_arbi (fn thm => @{thm spec} OF [thm]) first_conj
val elim_imp = funpow nr_prems (fn thm => @{thm mp} OF [thm]) elim_spec
in elim_imp end
fun typ_subst_for_sort thy info sort =
let
val spec = BNF_LFP_Compat.the_spec thy (#descr info |> hd |> (fn (_,(dty_name,_,_)) => dty_name))
val typ_subst = Term.typ_subst_atomic (spec |> fst |> map (fn (n,s) => (TFree (n,s), TFree (n,sort))))
in typ_subst end
fun typ_and_vs_of_typname thy typ_name sort =
let
val ar = Sign.arity_number thy typ_name
val sorts = map (K sort) (1 upto ar)
val ty_vars = Name.invent_names (Name.make_context [typ_name]) "a" sorts
val ty = Type (typ_name,map TFree ty_vars)
in (ty,ty_vars)
end
fun dt_number_recs dtys =
let
fun dtrecs [] j = (j,[])
| dtrecs (Old_Datatype_Aux.DtTFree _ :: dtys) j = dtrecs dtys j
| dtrecs (Old_Datatype_Aux.DtRec i :: dtys) j =
let
val (j',ijs) = dtrecs dtys (j+1)
in (j',(i,j) :: ijs) end
| dtrecs (Old_Datatype_Aux.DtType (_,dtys1) :: dtys2) j =
let
val (j',ijs) = dtrecs dtys1 j
val (j'',ijs') = dtrecs dtys2 j'
in (j'',ijs @ ijs') end
in dtrecs dtys 0
end
fun define_overloaded_generic (binding,eq) lthy =
let
val ((c, _), rhs) = eq |> Syntax.check_term lthy |>
Logic.dest_equals |>> dest_Free;
val ((_, (_, thm)), lthy') = Local_Theory.define
((Binding.name c, NoSyn), (binding, rhs)) lthy
val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm
in (thm', lthy')
end
fun define_overloaded (name,eq) = define_overloaded_generic ((Binding.name name, @{attributes [code]}),eq)
fun mk_def T c rhs = Logic.mk_equals (Const (c, T), rhs)
fun mk_free_tysubst_i typ_subst x i ty = Free (x ^ string_of_int i, ty |> typ_subst)
fun mk_xs thy info sort idx i =
let
val descr = #descr info
val typ_subst = typ_subst_for_sort thy info sort
fun typ_of dty = Old_Datatype_Aux.typ_of_dtyp descr dty |> typ_subst
val mk_free_i = mk_free_tysubst_i typ_subst
in
mk_free_i ("x_" ^ string_of_int idx ^ "_") i (typ_of (Old_Datatype_Aux.DtRec idx))
end
fun prop_trm_to_major_imp prop =
hd prop
|> (fn (p,v) => (
map (HOLogic.mk_Trueprop) p
|> split_last
|> Logic.list_implies,
v))
fun mk_case_tac (ctxt : Proof.context)
(insts : term option list list)
(thm : thm)
(sub_case_tac : Proof.context * int * thm list * (string * cterm) list -> tactic) =
(
DETERM o Induct.cases_tac ctxt false insts (SOME thm) []
THEN_ALL_NEW (fn i => Subgoal.SUBPROOF (fn {context = ctxt, prems = hyps, params = params, ...}
=> sub_case_tac (ctxt, i-1, hyps, params)) ctxt i)
)
1
fun mk_solve_with_tac ctxt thms solver_tac =
SOLVE (Method.insert_tac ctxt thms 1 THEN solver_tac)
fun simps_of_info info = #case_rewrites info @ #rec_rewrites info @ #inject info @ #distinct info
val my_simp_set =
simpset_of (@{context}
delsimps (simpset_of @{context} |> dest_ss |> #simps |> map snd)
addsimps @{thms HOL.simp_thms})
fun mk_binary_thm mk_prop_trm mk_bin_idx bin_const_name thy (info : Old_Datatype_Aux.info) prop_gen sort same_constructor_tac =
let
fun bin_const ty = Const (bin_const_name, ty --> ty --> @{typ bool})
val prop_props = mk_prop_trm thy info sort prop_gen
val (mk_rec,nrec_args) = mk_bin_idx thy info sort
val typ_subst = typ_subst_for_sort thy info sort
val descr = #descr info
fun typ_of dty = Old_Datatype_Aux.typ_of_dtyp descr dty |> typ_subst
fun mk_binary_term (Old_Datatype_Aux.DtRec i) = mk_rec i
| mk_binary_term dty =
let
val ty = typ_of dty
in bin_const ty end;
fun mk_binary dty x y = mk_binary_term dty $ x $ y;
val ind_thm = #induct info
val prop_thm_of_tac = inductive_thm thy prop_props ind_thm sort
fun ind_case_tac ctxt i hyps ihprems params_x ys =
let
val y = hd ys
val (j,idx) = nth nrec_args i |> (fn (_,j,idx) => (j,idx))
val linfo = nth descr idx |> (fn (_,(ty_name,_,_)) => ty_name)
|> BNF_LFP_Compat.the_info thy []
fun solve_with_tac ctxt thms =
let val simp_ctxt =
(ctxt
|> Context_Position.set_visible false
|> put_simpset my_simp_set)
addsimps (simps_of_info info @ simps_of_info linfo)
in mk_solve_with_tac ctxt thms (force_tac simp_ctxt 1) end
fun case_tac ctxt = mk_case_tac ctxt [[SOME y]] (#exhaust linfo)
fun sub_case_tac (ctxt,k,prems,iparams_y) =
let
val case_hyp_y = hd prems
in
if not (j = k)
then my_print_tac ctxt ("different constructors ") THEN solve_with_tac ctxt (case_hyp_y :: ihprems)
else
let
val params_y = map (snd #> Thm.term_of) iparams_y
val c_info = nth descr idx |> snd |> (fn (_,_,info) => nth info j)
in
my_print_tac ctxt ("consider constructor " ^ string_of_int k)
THEN same_constructor_tac ctxt hyps ihprems case_hyp_y solve_with_tac j params_x params_y c_info mk_binary
end
end
in my_print_tac ctxt ("start induct " ^ string_of_int i) THEN case_tac ctxt sub_case_tac end
val prop_thm = prop_thm_of_tac ind_case_tac
in prop_thm end
fun mk_case_tac ctxt
(insts : term option list list)
(thm : thm)
(sub_case_tac : Proof.context * int * thm list * (string * cterm) list -> tactic) =
(
DETERM o Induct.cases_tac ctxt false insts (SOME thm) []
THEN_ALL_NEW (fn i => Subgoal.SUBPROOF (fn {context = ctxt, prems = hyps, params = params, ...}
=> sub_case_tac (ctxt, i-1, hyps, params)) ctxt i)
)
1
end
Theory Order_Generator
section ‹Generating linear orders for datatypes›
theory Order_Generator
imports
Derive_Aux
begin
subsection Introduction
text ‹
The order generator registers itself at the derive-manager for the classes @{class ord},
@{class order}, and @{class linorder}.
To be more precise,
it automatically generates the two functions @{term "(≤)"} and @{term "(<)"} for some datatype
\texttt{dtype} and
proves the following instantiations.
\begin{itemize}
\item \texttt{instantiation dtype :: (ord,\ldots,ord) ord}
\item \texttt{instantiation dtype :: (order,\ldots,order) order}
\item \texttt{instantiation dtype :: (linorder,\ldots,linorder) linorder}
\end{itemize}
All the non-recursive types that are used in the datatype must have similar instantiations.
For recursive type-dependencies this is automatically generated.
For example, for the \texttt{datatype tree = Leaf nat | Node "tree list"} we require that
@{type nat} is already in @{class linorder}, whereas for @{type list} nothing is required, since for the
\texttt{tree}
datatype the @{type list} is only used recursively.
However, if we define \texttt{datatype tree = Leaf "nat list" | Node tree tree} then
@{type list} must
provide the above instantiations.
Note that when calling the generator for @{class linorder}, it will automatically also derive the instantiations
for @{class order}, which in turn invokes the generator for @{class ord}.
A later invokation of @{class linorder}
after @{class order} or @{class ord} is not possible.
›
subsection "Implementation Notes"
text ‹
The generator uses the recursors from the datatype package to define a lexicographic order.
E.g., for a declaration
\texttt{datatype 'a tree = Empty | Node "'a tree" 'a "'a tree"}
this will semantically result in
\begin{verbatim}
(Empty < Node _ _ _) = True
(Node l1 l2 l3 < Node r1 r2 r3) =
(l1 < r1 || l1 = r1 && (l2 < r2 || l2 = r2 && l3 < r3))
(_ < _) = False
(l <= r) = (l < r || l = r)
\end{verbatim}
The desired properties (like @{term "x < y ⟹ y < z ⟹ x < z"})
of the orders are all proven using induction (with the induction theorem from the datatype on @{term x}),
and afterwards there is a case distinction on the remaining variables, i.e., here @{term y} and @{term z}.
If the constructors of @{term x}, @{term y}, and @{term z} are different always some basic tactic is invoked.
In the other case (identical constructors) for each property a dedicated tactic was designed.
›
subsection "Features and Limitations"
text ‹
The order generator has been developed mainly for datatypes without explicit mutual recursion.
For mutual recursive datatypes---like
\texttt{datatype a = C b and b = D a a}---only
for the first mentioned datatype---here \texttt{a}---the instantiations of the order-classes are
derived.
Indirect recursion like in \texttt{datatype tree = Leaf nat | Node "tree list"} should work
without problems.
›
subsection "Installing the generator"
lemma linear_cases: "(x :: 'a :: linorder) = y ∨ x < y ∨ y < x" by auto
ML_file ‹order_generator.ML›
end
File ‹order_generator.ML›
signature ORDER_GENERATOR =
sig
val mk_less_idx : theory -> Old_Datatype_Aux.info -> sort -> (int -> term) * (term * int * int) list;
val mk_less_eq_idx : theory -> Old_Datatype_Aux.info -> sort -> (int -> term -> term -> term);
val mk_transitivity_thms : theory -> Old_Datatype_Aux.info -> thm * thm;
val mk_less_le_not_le_thm : theory -> Old_Datatype_Aux.info -> thm
val mk_le_refl_thm : theory -> Old_Datatype_Aux.info -> thm
val mk_antisym_thm : theory -> Old_Datatype_Aux.info -> thm -> thm -> thm
val mk_linear_thm : theory -> Old_Datatype_Aux.info -> thm
val mk_order_thms : theory -> Old_Datatype_Aux.info -> thm list
val derive : int -> string -> string -> theory -> theory
end
structure Order_Generator : ORDER_GENERATOR =
struct
open Derive_Aux
val less_name = @{const_name "Orderings.less"}
fun mk_free_tysubst_i typ_subst x i ty = Free (x ^ string_of_int i, ty |> typ_subst)
fun mk_less_idx thy info sort =
let
val typ_subst = typ_subst_for_sort thy info sort
val descr = #descr info
fun typ_of dty = Old_Datatype_Aux.typ_of_dtyp descr dty |> typ_subst
val rec_names = #rec_names info
val mk_free_i = mk_free_tysubst_i typ_subst
fun rec_idx i dtys = dt_number_recs (take i dtys) |> fst
fun mk_rhss (idx,(ty_name,_,cons)) =
let
val ty = typ_of (Old_Datatype_Aux.DtRec idx)
val linfo = BNF_LFP_Compat.the_info thy [] ty_name
val case_name = #case_name linfo
fun mk_rhs (i,(_,dtysi)) =
let
val lvars = map_index (fn (i,dty) => mk_free_i "x_" i (typ_of dty)) dtysi
fun res_var (i,oc) = mk_free_i "res_" oc (typ_of (Old_Datatype_Aux.DtRec i) --> @{typ bool});
val res_vars = dt_number_recs dtysi
|> snd
|> map res_var
fun mk_case (j,(_,dtysj)) =
let
val rvars = map_index (fn (i,dty) => mk_free_i "y_" i (typ_of dty)) dtysj
val x = nth lvars
val y = nth rvars
fun combine_dts [] = @{term False}
| combine_dts ((_,c) :: []) = c
| combine_dts ((i,c) :: ics) = HOLogic.mk_disj (c, HOLogic.mk_conj (HOLogic.mk_eq (x i, y i), combine_dts ics))
fun less_of_dty (i,Old_Datatype_Aux.DtRec j) = res_var (j,rec_idx i dtysj) $ y i
| less_of_dty (i,_) =
let
val xi = x i
val ty = Term.type_of xi
val less = Const (less_name, ty --> ty --> @{typ bool})
in less $ xi $ y i end
val rhs =
if i < j then @{term True}
else if i > j then @{term False}
else map_index less_of_dty dtysi
|> map_index I
|> combine_dts
val lam_rhs = fold lambda (rev rvars) rhs
in lam_rhs end
val cases = map_index mk_case cons
val case_ty = (map type_of cases @ [ty]) ---> @{typ bool}
val rhs_case = list_comb (Const (case_name, case_ty), cases)
val rhs = fold lambda (rev (lvars @ res_vars)) rhs_case
in rhs end
val rec_args = map_index (fn (i,c) => (mk_rhs (i,c),i,idx)) cons
in rec_args end
val nrec_args = maps mk_rhss descr
val rec_args = map #1 nrec_args
fun mk_rec i =
let
val ty = typ_of (Old_Datatype_Aux.DtRec i)
val rec_ty = map type_of rec_args @ [ty,ty] ---> @{typ bool}
val rec_name = nth rec_names i
val rhs = list_comb (Const (rec_name, rec_ty), rec_args)
in rhs end
in (mk_rec,nrec_args) end
fun mk_less_eq_idx thy info sort idx x y =
mk_less_idx thy info sort
|> fst
|> (fn less => HOLogic.mk_disj (less idx $ x $ y, HOLogic.mk_eq (x,y)))
fun mk_prop_trm thy info sort
(gen : (int -> term) -> (term -> term -> term)list -> term list * term list) =
let
fun main idx =
let
val xs = mk_xs thy info sort idx
fun less a b = (mk_less_idx thy info sort |> fst) idx $ a $ b
val less_eq = mk_less_eq_idx thy info sort idx
in gen xs [less, less_eq] end
in #descr info
|> map (fst #> main)
end
fun mk_prop_major_trm thy info sort gen =
mk_prop_trm thy info sort gen |> prop_trm_to_major_imp
fun mk_trans_thm_trm thy info =
mk_prop_trm thy info @{sort "order"}
(fn xs => fn [less,_] =>
let val (x,y,z) = (xs 1, xs 2, xs 3)
in ([less x y, less y z, less x z], [x,y,z]) end)
fun mk_trans_eq_thm_trm thy info =
mk_prop_major_trm thy info @{sort "order"}
(fn xs => fn [_, lesseq] =>
let val (x,y,z) = (xs 1, xs 2, xs 3)
in ([lesseq x y, lesseq y z, lesseq x z], [x,y,z]) end)
fun mk_less_disj mk_less px py dtys =
let
fun build_disj [] _ _ = @{term False}
| build_disj (px :: xs) (py :: ys) (dty :: dtys) =
HOLogic.mk_disj (mk_less dty px py, HOLogic.mk_conj (HOLogic.mk_eq (px,py),build_disj xs ys dtys))
in
HOLogic.mk_Trueprop (build_disj px py dtys)
end;
fun simps_of_info info = #case_rewrites info @ #rec_rewrites info @ #inject info @ #distinct info
fun mk_transitivity_thms thy (info : Old_Datatype_Aux.info) =
let
val ctxt = Proof_Context.init_global thy
val trans_props = mk_trans_thm_trm thy info
val sort = @{sort "order"}
val (mk_rec,nrec_args) = mk_less_idx thy info sort
val typ_subst = typ_subst_for_sort thy info sort
val descr = #descr info
fun typ_of dty = Old_Datatype_Aux.typ_of_dtyp descr dty |> typ_subst
fun mk_less_term (Old_Datatype_Aux.DtRec i) = mk_rec i
| mk_less_term dty =
let
val ty = typ_of dty
in Const (less_name, ty --> ty --> @{typ bool}) end;
fun mk_less dty x y = mk_less_term dty $ x $ y;
val ind_thm = #induct info
val trans_thm_of_tac = inductive_thm thy trans_props ind_thm sort
fun ind_case_tac ctxt i hyps [xy,yz] params_x [y,z] =
let
val (j,idx) = nth nrec_args i |> (fn (_,j,idx) => (j,idx))
val linfo = nth descr idx |> (fn (_,(ty_name,_,_)) => ty_name)
|> BNF_LFP_Compat.the_info thy []
fun solve_with_tac ctxt thms =
let
val simp_ctxt =
(ctxt
|> Context_Position.set_visible false
|> put_simpset my_simp_set)
addsimps (simps_of_info info @ simps_of_info linfo @ thms)
in mk_solve_with_tac simp_ctxt thms (asm_full_simp_tac simp_ctxt 1) end
fun case_tac ctxt y_z = mk_case_tac ctxt [[SOME y_z]] (#exhaust linfo)
fun sub_case_tac (ctxt,k,prems,iparams_y) =
let
val case_hyp_y = hd prems
fun sub_sub_case_tac (ctxt,l,prems,iparams_z) =
let
val case_hyp_z = hd prems
val comp_eq = [case_hyp_z, case_hyp_y, xy, yz]
in
(if not (j = l andalso l = k)
then
K (solve_with_tac ctxt comp_eq)
else
let
val params_y = map (snd #> Thm.term_of) iparams_y
val params_z = map (snd #> Thm.term_of) iparams_z
val c_info = nth descr idx |> snd |> (fn (_,_,info) => nth info j)
val pdtys = snd c_info
val build_disj = mk_less_disj mk_less
val xy' = build_disj params_x params_y pdtys
val yz' = build_disj params_y params_z pdtys
fun disj_thm t = Goal.prove_future ctxt [] [] t (K (solve_with_tac ctxt comp_eq))
val xy_disj = disj_thm xy'
val yz_disj = disj_thm yz'
fun solve_tac xy _ [] _ _ _ _ _ = K (solve_with_tac ctxt [xy])
| solve_tac xy yz (px :: pxs) (py :: pys) (pz :: pzs) (dty :: dtys) eqs ihyps =
let
fun case_tac_disj ctxt disj tac =
mk_case_tac ctxt [] (@{thm disjE} OF [disj]) (fn (ctxt,ii,hyps,_) => tac ii ctxt (List.last hyps))
fun yz_case_tac ctxt = case_tac_disj ctxt yz
val rec_type = (fn Old_Datatype_Aux.DtRec _ => true | _ => false) dty
fun xy_tac ii ctxt hyp_xy =
if ii = 1
then
let
val eq_term = HOLogic.mk_eq (px,py) |> HOLogic.mk_Trueprop
val eq_xy_thm = Goal.prove_future ctxt [] [] eq_term (K (solve_with_tac ctxt [hyp_xy]))
val xy'_thm = Goal.prove_future ctxt [] [] (build_disj pxs pys dtys) (K (solve_with_tac ctxt [hyp_xy]))
fun yz_tac jj ctxt hyp_yz =
if jj = 1
then
let
val eq_term = HOLogic.mk_eq (px,pz) |> HOLogic.mk_Trueprop
val eq_thm = Goal.prove_future ctxt [] [] eq_term (K (solve_with_tac ctxt [eq_xy_thm,hyp_yz]))
val yz'_thm = Goal.prove_future ctxt [] [] (build_disj pys pzs dtys) (K (solve_with_tac ctxt [hyp_yz]))
val drop_hyps = if rec_type then tl else I
in
solve_tac xy'_thm yz'_thm pxs pys pzs dtys (eq_thm :: eqs) (drop_hyps ihyps) 1
end
else
let
val xz_term = mk_less dty px pz |> HOLogic.mk_Trueprop
val xz_thm = Goal.prove_future ctxt [] [] xz_term (K (solve_with_tac ctxt [hyp_xy,hyp_yz]))
in
solve_with_tac ctxt (xz_thm :: case_hyp_z :: eqs)
end
in
yz_case_tac ctxt yz_tac
end
else
let
val xz_term = mk_less dty px pz |> HOLogic.mk_Trueprop
fun yz_tac jj ctxt hyp_yz =
if jj = 1
then
let
val xz_thm = Goal.prove_future ctxt [] [] xz_term (K (solve_with_tac ctxt [hyp_xy,hyp_yz]))
in
solve_with_tac ctxt (xz_thm :: case_hyp_z :: eqs)
end
else
let
val trans_thm = if rec_type then hd ihyps else @{thm less_trans}
val tac = resolve_tac ctxt [trans_thm OF [hyp_xy,hyp_yz]] 1
val xz_thm = Goal.prove_future ctxt [] [] xz_term (K tac)
in
solve_with_tac ctxt (xz_thm :: case_hyp_z :: eqs)
end
in
yz_case_tac ctxt yz_tac
end;
val xy_case_tac = case_tac_disj ctxt xy xy_tac
in
K (my_print_tac ctxt ("another case: ") THEN xy_case_tac)
end
in
K (my_print_tac ctxt "recursive case: ")
THEN' solve_tac xy_disj yz_disj params_x params_y params_z pdtys [] hyps
end
) 1
end
in
my_print_tac ctxt ("consider constructor " ^ string_of_int k) THEN
(if k >= j then case_tac ctxt z sub_sub_case_tac else
solve_with_tac ctxt [case_hyp_y,xy])
end
in
my_print_tac ctxt ("start induct " ^ string_of_int i) THEN case_tac ctxt y sub_case_tac
end
val trans_thm = trans_thm_of_tac ind_case_tac
val (trans_eq_trm,vars) = mk_trans_eq_thm_trm thy info
val inst_trans = infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) vars) trans_thm
val trans_eq_vars_string = map (dest_Free #> fst) vars
fun tac_to_eq_thm tac = Goal.prove_global_future thy trans_eq_vars_string [] trans_eq_trm (K tac)
val eq_tac = mk_solve_with_tac ctxt [inst_trans] (blast_tac ctxt 1)
val trans_eq_thm = tac_to_eq_thm eq_tac
in
(trans_thm,trans_eq_thm)
end
val mk_binary_less_thm = mk_binary_thm mk_prop_trm mk_less_idx less_name
fun mk_less_le_not_le_thm thy info =
let
val sort = @{sort "order"}
fun prop_gen xs [less,lesseq] =
let
val (x,y) = (xs 1, xs 2)
in ([less x y, lesseq y x |> HOLogic.mk_not], [x,y]) end
fun main_tac ctxt ih_hyps ih_prems y_prem solve_with_tac _ params_x params_y c_info mk_less =
let
val pdtys = snd c_info
val comp_eq = y_prem :: ih_prems
val build_disj = mk_less_disj mk_less
val xy' = build_disj params_x params_y pdtys
val xy_disj = Goal.prove_future ctxt [] [] xy' (K (solve_with_tac ctxt comp_eq))
fun solve_tac ctxt xy [] _ _ _ _ = solve_with_tac ctxt [xy]
| solve_tac ctxt xy (px :: pxs) (py :: pys) (dty :: dtys) eqs ihyps =
let
val xs_ys = build_disj pxs pys dtys
val x_eq_y = HOLogic.mk_eq (px,py)
val x_less_y = mk_less dty px py
val disj2 =
HOLogic.mk_disj (x_less_y, HOLogic.mk_conj (HOLogic.mk_not x_less_y, HOLogic.mk_conj( x_eq_y, HOLogic.dest_Trueprop xs_ys)))
|> HOLogic.mk_Trueprop
val disj2_thm = Goal.prove_future ctxt [] [] disj2 (K (Method.insert_tac ctxt [xy] 1 THEN blast_tac ctxt 1))
fun case_tac_disj disj tac =
mk_case_tac ctxt [] (@{thm disjE} OF [disj]) (fn (ctxt,ii,hyps,_) => tac ii ctxt (List.last hyps))
val rec_type = (fn Old_Datatype_Aux.DtRec _ => true | _ => false) dty
fun xy_tac ii ctxt hyp_xy =
if ii = 1
then
let
val eq_term = x_eq_y |> HOLogic.mk_Trueprop
val eq_xy_thm = Goal.prove_future ctxt [] [] eq_term (K (solve_with_tac ctxt [hyp_xy]))
val xy'_thm = Goal.prove_future ctxt [] [] xs_ys (K (solve_with_tac ctxt [hyp_xy]))
val yx_thm =
Goal.prove_future ctxt [] [] (mk_less dty py px |> HOLogic.mk_not |> HOLogic.mk_Trueprop)
(K (solve_with_tac ctxt [hyp_xy]))
val ihyps' = if rec_type then tl ihyps else ihyps
val solve_rec = solve_tac ctxt xy'_thm pxs pys dtys (eq_xy_thm :: yx_thm :: eqs) ihyps'
in
solve_rec
end
else
let
val yx = HOLogic.mk_disj (mk_less dty py px, HOLogic.mk_eq (py,px)) |> HOLogic.mk_not |> HOLogic.mk_Trueprop
val tac = if rec_type then solve_with_tac ctxt [hd ihyps OF [hyp_xy]] else solve_with_tac ctxt [hyp_xy]
val yx_thm = Goal.prove_future ctxt [] [] yx (K tac)
in
solve_with_tac ctxt (yx_thm :: y_prem :: eqs)
end;
in
case_tac_disj disj2_thm xy_tac
end
in
(solve_tac ctxt xy_disj params_x params_y pdtys [] ih_hyps : tactic)
end
val main_thm = mk_binary_less_thm thy info prop_gen sort main_tac
val ctxt = Proof_Context.init_global thy
val (thm_trm,vars) = mk_prop_major_trm thy info sort (fn xs => fn [less,lesseq] =>
let val (x,y) = (xs 1, xs 2)
in
([HOLogic.mk_eq (less x y,HOLogic.mk_conj (lesseq x y, lesseq y x |> HOLogic.mk_not))], [x,y])
end)
val inst_thm = infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) vars) main_thm
val vars_strings = map (dest_Free #> fst) vars
val thm =
Goal.prove_future ctxt vars_strings [] thm_trm
(K (Method.insert_tac ctxt [inst_thm] 1 THEN blast_tac ctxt 1))
in
thm
end
fun mk_le_refl_thm thy info =
let
val sort = @{sort "order"}
val ctxt = Proof_Context.init_global thy
val (thm_trm,vars) = mk_prop_major_trm thy info sort (fn xs => fn [_,lesseq] =>
let val x = xs 1
in
([lesseq x x],[x])
end)
val vars_strings = map (dest_Free #> fst) vars
in
Goal.prove_future ctxt vars_strings [] thm_trm (K (blast_tac ctxt 1))
end
fun mk_antisym_thm thy info trans_thm less_thm =
let
val sort = @{sort "order"}
val ctxt = Proof_Context.init_global thy
val (thm_trm,vars) = mk_prop_major_trm thy info sort (fn xs => fn [_,lesseq] =>
let val (x,y) = (xs 1, xs 2)
in
([lesseq x y, lesseq y x, HOLogic.mk_eq (x,y)],[x,y])
end)
val vars_strings = map (dest_Free #> fst) vars
val tvars = vars @ [hd vars]
val lvars = [hd vars,hd vars]
fun inst_thm vars thm = infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) vars) thm
val inst_trans = inst_thm tvars trans_thm
val inst_less = inst_thm lvars less_thm
val res =
Goal.prove_future ctxt vars_strings [] thm_trm
(K (Method.insert_tac ctxt [inst_trans,inst_less] 1 THEN blast_tac ctxt 1))
in
res
end
fun mk_order_thms thy info =
let
val (trans,trans_eq) = mk_transitivity_thms thy info
val less = mk_less_le_not_le_thm thy info
val refl = mk_le_refl_thm thy info
val antisym = mk_antisym_thm thy info trans less
in
[trans_eq,less,refl,antisym]
end
fun mk_linear_thm thy info =
let
val sort = @{sort "linorder"}
fun prop_gen xs [less,_] =
let val (x,y) = (xs 1, xs 2)
in
([HOLogic.mk_disj (HOLogic.mk_eq (x,y),HOLogic.mk_disj(less x y, less y x))],[x,y])
end
fun main_tac ctxt ih_hyps _ y_prem solve_with_tac _ params_x params_y c_info mk_less =
let
val pdtys = snd c_info
fun solve_tac [] _ _ eqs _ = solve_with_tac ctxt eqs
| solve_tac (px :: pxs) (py :: pys) (dty :: dtys) eqs ihyps =
let
val less = mk_less dty
val x_eq_y = HOLogic.mk_eq (px,py)
val disj_trm = HOLogic.mk_disj (x_eq_y,HOLogic.mk_disj(less px py, less py px)) |> HOLogic.mk_Trueprop
val rec_type = (fn Old_Datatype_Aux.DtRec _ => true | _ => false) dty
val disj_thm' = if rec_type then hd ihyps else @{thm linear_cases}
val disj_tac = resolve_tac ctxt [disj_thm'] 1
val disj_thm = Goal.prove_future ctxt [] [] disj_trm (K (disj_tac))
fun case_tac_disj disj tac =
mk_case_tac ctxt [] (@{thm disjE} OF [disj]) (fn (ctxt,ii,hyps,_) => tac ii ctxt (List.last hyps))
fun eq_less_less_tac ii _ eq_less =
if ii = 0
then
let
val ihyps' = if rec_type then tl ihyps else ihyps
val solve_rec = solve_tac pxs pys dtys (eq_less :: eqs) ihyps'
in
solve_rec
end
else
let
fun less_tac _ _ less = solve_with_tac ctxt (less :: eqs)
in
case_tac_disj eq_less less_tac
end;
in
case_tac_disj disj_thm eq_less_less_tac
end
in
(solve_tac params_x params_y pdtys [y_prem] ih_hyps : tactic)
end
val main_thm = mk_binary_less_thm thy info prop_gen sort main_tac
val ctxt = Proof_Context.init_global thy
val (thm_trm,vars) = mk_prop_major_trm thy info sort (fn xs => fn [_,lesseq] =>
let val (x,y) = (xs 1, xs 2)
in
([HOLogic.mk_disj (lesseq x y,lesseq y x)],[x,y])
end)
val inst_thm = infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) vars) main_thm
val vars_strings = map (dest_Free #> fst) vars
val thm =
Goal.prove_future ctxt vars_strings [] thm_trm
(K (Method.insert_tac ctxt [inst_thm] 1 THEN blast_tac ctxt 1))
in
thm
end
fun derive kind dtyp_name _ thy =
let
val tyco = dtyp_name
val base_name = Long_Name.base_name tyco
val _ = writeln ("creating orders for datatype " ^ base_name)
val sort = @{sort ord}
val info = BNF_LFP_Compat.the_info thy [] tyco
val vs_of_sort =
let val i = BNF_LFP_Compat.the_spec thy tyco |> #1
in fn sort => map (fn (n,_) => (n, sort)) i end
val vs = vs_of_sort sort
val less_rhs = mk_less_idx thy info sort |> fst |> (fn x => x 0)
val ty = Term.fastype_of less_rhs |> Term.dest_Type |> snd |> hd
fun mk_binrel_def T = mk_def (T --> T --> HOLogic.boolT)
val less_def = mk_binrel_def ty @{const_name less} less_rhs
val x = Free ("x",ty)
val y = Free ("y",ty)
val less_eq_rhs = lambda x (lambda y (HOLogic.mk_disj (less_rhs $ x $ y, HOLogic.mk_eq (x,y))))
val less_eq_def = mk_binrel_def ty @{const_name less_eq} less_eq_rhs
val ((less_thm,less_eq_thm),lthy) = Class.instantiation ([tyco],vs,sort) thy
|> define_overloaded ("less_" ^ base_name ^ "_def", less_def)
||>> define_overloaded ("less_eq_" ^ base_name ^ "_def", less_eq_def)
val less_thms = [less_thm, less_eq_thm]
val thy' = Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) lthy
val _ = writeln ("registered " ^ base_name ^ " in class ord")
val thy'' =
if kind < 1 then thy'
else
let
val sort = @{sort order}
val vs = vs_of_sort sort
val [trans_eq,less,refl,antisym] = mk_order_thms thy info
val lthy = Class.instantiation ([tyco],vs,sort) thy'
fun order_tac ctxt =
my_print_tac ctxt "enter order" THEN
unfold_tac ctxt less_thms THEN
my_print_tac ctxt "after unfolding" THEN
resolve_tac ctxt [less] 1 THEN
my_print_tac ctxt "after less" THEN
resolve_tac ctxt [refl] 1 THEN
my_print_tac ctxt "after refl" THEN
resolve_tac ctxt [trans_eq] 1 THEN assume_tac ctxt 1 THEN assume_tac ctxt 1 THEN
my_print_tac ctxt "after trans" THEN
resolve_tac ctxt [antisym] 1 THEN assume_tac ctxt 1 THEN assume_tac ctxt 1
val thy'' =
Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [] THEN order_tac ctxt) lthy
val _ = writeln ("registered " ^ base_name ^ " in class order")
in thy'' end
val thy''' =
if kind < 2 then thy''
else
let
val sort = @{sort linorder}
val vs = vs_of_sort sort
val lthy = Class.instantiation ([tyco],vs,sort) thy''
val linear = mk_linear_thm thy info
fun order_tac ctxt =
unfold_tac ctxt less_thms THEN
resolve_tac ctxt [linear] 1
val thy''' = Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [] THEN order_tac ctxt) lthy
val _ = writeln ("registered " ^ base_name ^ " in class linorder")
in thy''' end
in thy''' end
val _ =
Theory.setup
(Derive_Manager.register_derive "ord" "derives ord for a datatype" (derive 0) #>
Derive_Manager.register_derive "order" "derives an order for a datatype" (derive 1) #>
Derive_Manager.register_derive "linorder" "derives a linear order for a datatype" (derive 2))
end
Theory Hash_Generator
section ‹Hash functions›
theory Hash_Generator
imports
Collections.HashCode
Derive_Aux
begin
subsection "Introduction"
text ‹
The interface for hash-functions is defined in the class @{class hashable} which has been developed
as part of the Isabelle Collection Framework \cite{rbt}. It requires a hash-function
(@{const hashcode}), a bounded hash-function (@{const bounded_hashcode}),
and a default hash-table size (@{const def_hashmap_size}).
The @{const hashcode} function for each datatype are created by instantiating the recursors of that
datatype appropriately. E.g., for \texttt{datatype 'a test = C1 'a 'a | C2 "'a test list"}
we get a hash-function which is equivalent to
\begin{verbatim}
hashcode (C1 a b) = c1 * hashcode a + c2 * hashcode b
hashcode (C2 Nil) = c3
hashcode (C2 (a # as)) = c4 * hashcode a + c5 * hashcode as
\end{verbatim}
where each \texttt{c$_{i}$} is a non-negative 32-bit number which is dependent on the
datatype name, the constructor name, and the occurrence of the argument (i.e.,
in the example \texttt{c1} and \texttt{c2} will usually be different numbers.)
These parameters are used in linear combination with prime numbers to hopefully
get some useful hash-function.
The @{const bounded_hashcode} functions are constructed in the same way, except that after each
arithmetic operation a modulo operation is performed.
Finally, the default hash-table size is just set to 10, following Java's default
hash-table constructor.
›
subsection "Features and Limitations"
text ‹
We get same limitation as for the order generator.
For mutual recursive datatypes, only
for the first mentioned datatype the instantiations of the @{class hashable}-class are
derived.
›
subsection "Installing the generator"
lemma hash_mod_lemma: "1 < (n :: nat) ⟹ x mod n < n" by auto
ML_file ‹hash_generator.ML›
end
File ‹hash_generator.ML›
signature HASH_GENERATOR =
sig
val mk_hash : theory -> Old_Datatype_Aux.info -> term;
val derive : string -> string -> theory -> theory
end
structure Hash_Generator : HASH_GENERATOR =
struct
open Derive_Aux
val max_int = 2147483648
fun int_of_string s = fold
(fn c => fn i => (1792318057 * i + Char.ord c) mod max_int)
(String.explode s)
0
fun create_factor ty_name con_name idx i j =
(1444315237 * int_of_string ty_name +
1336760419 * int_of_string con_name +
2044890737 * (idx + 1) +
1622892797 * (i+1) +
2140823281 * (j+1)) mod max_int
fun create_def_size _ = 10
val hash_name = @{const_name "hashcode"}
fun mk_free_tysubst_i typ_subst x i ty = Free (x ^ string_of_int i, ty |> typ_subst)
fun mk_hash thy info =
let
val sort = @{sort hashable}
val typ_subst = typ_subst_for_sort thy info sort
val descr = #descr info
val ty_name = info |> #descr |> hd |> snd |> #1
val cons_hash = create_factor ty_name
val mk_num = HOLogic.mk_number @{typ hashcode}
fun typ_of dty = Old_Datatype_Aux.typ_of_dtyp descr dty |> typ_subst
val rec_names = #rec_names info
val mk_free_i = mk_free_tysubst_i typ_subst
fun rec_idx i dtys = dt_number_recs (take i dtys) |> fst
fun mk_rhss (idx,(_,_,cons)) =
let
fun mk_rhs (i,(cname,dtysi)) =
let
val lvars = map_index (fn (i,dty) => mk_free_i "x_" i (typ_of dty)) dtysi
fun res_var (_,oc) = mk_free_i "res_" oc (@{typ hashcode});
val res_vars = dt_number_recs dtysi
|> snd
|> map res_var
val x = nth lvars
fun combine_dts [] = mk_num (cons_hash cname idx i 0)
| combine_dts ((_,c) :: ics) = @{term "(+) :: hashcode => hashcode => hashcode"} $ c $ combine_dts ics
fun multiply j t =
let
val mult = mk_num (cons_hash cname idx i (j+1))
in @{term "(*) :: hashcode => hashcode => hashcode"} $ mult $ t end
fun hash_of_dty (i,Old_Datatype_Aux.DtRec j) = res_var (j,rec_idx i dtysi) |> multiply i
| hash_of_dty (i,_) =
let
val xi = x i
val ty = Term.type_of xi
val hash = Const (hash_name, ty --> @{typ hashcode}) $ xi
in hash |> multiply i end
val pre_rhs = map_index hash_of_dty dtysi
|> map_index I
|> combine_dts
val rhs = fold lambda (rev (lvars @ res_vars)) pre_rhs
in rhs end
val rec_args = map_index (fn (i,c) => (mk_rhs (i,c),i,idx)) cons
in rec_args end
val nrec_args = maps mk_rhss descr
val rec_args = map #1 nrec_args
fun mk_rec i =
let
val ty = typ_of (Old_Datatype_Aux.DtRec i)
val rec_ty = map type_of rec_args @ [ty] ---> @{typ hashcode}
val rec_name = nth rec_names i
val rhs = list_comb (Const (rec_name, rec_ty), rec_args)
in rhs end
in mk_rec 0 end
fun derive dtyp_name _ thy =
let
val tyco = dtyp_name
val base_name = Long_Name.base_name tyco
val _ = writeln ("creating hashcode for datatype " ^ base_name)
val sort = @{sort hashable}
val info = BNF_LFP_Compat.the_info thy [] tyco
val vs_of_sort =
let val i = BNF_LFP_Compat.the_spec thy tyco |> #1
in fn sort => map (fn (n,_) => (n, sort)) i end
val vs = vs_of_sort sort
val hash_rhs = mk_hash thy info
val ty = Term.fastype_of hash_rhs |> Term.dest_Type |> snd |> hd
val ty_it = Type (@{type_name itself}, [ty])
val hashs_rhs = lambda (Free ("x",ty_it)) (HOLogic.mk_number @{typ nat} (create_def_size ty))
val hash_def = mk_def (ty --> @{typ hashcode}) @{const_name hashcode} hash_rhs
val hashs_def = mk_def (ty_it --> @{typ nat}) @{const_name def_hashmap_size} hashs_rhs
val ((hash_thm , hashs_thm),lthy) = Class.instantiation ([tyco],vs,sort) thy
|> define_overloaded ("hashcode_" ^ base_name ^ "_def", hash_def)
||>> define_overloaded ("def_hashmap_size_" ^ base_name ^ "_def", hashs_def)
val hash_thms = [hash_thm, hashs_thm]
fun hash_tac ctxt =
my_print_tac ctxt "enter hash " THEN
unfold_tac ctxt hash_thms THEN
my_print_tac ctxt "after unfolding" THEN
simp_tac ctxt 1
val thy' = Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [] THEN hash_tac ctxt) lthy
val _ = writeln ("registered " ^ base_name ^ " in class hashable")
in thy' end
val _ =
Theory.setup
(Derive_Manager.register_derive "hashable" "derives a hash function for a datatype" derive)
end
Theory Derive
section ‹Loading derive-commands›
theory Derive
imports
Order_Generator
Hash_Generator
Deriving.Countable_Generator
begin
text‹
We just load the commands to derive (linear) orders, hash-functions, and the
command to show that a datatype is countable, so that now all of them are available.
There are further generators available in the AFP entries of lightweight containers and Show.
›
print_derives
end
Theory Derive_Examples
section Examples
theory Derive_Examples
imports
Derive
HOL.Rat
begin
subsection "Register standard existing types"
derive linorder list sum prod
subsection "Without nested recursion"
datatype 'a bintree = BEmpty | BNode "'a bintree" 'a "'a bintree"
derive linorder bintree
derive hashable bintree
derive countable bintree
subsection "Using other datatypes"
datatype nat_list_list = NNil | CCons "nat list" nat_list_list
derive linorder nat_list_list
derive hashable nat_list_list
derive countable nat_list_list
subsection "Explicit mutual recursion"
datatype
'a mtree = MEmpty | MNode 'a "'a mtree_list" and
'a mtree_list = MNil | MCons "'a mtree" "'a mtree_list"
derive linorder mtree
derive hashable mtree
derive countable mtree
subsection "Implicit mutual recursion"
datatype 'a tree = Empty | Node 'a "'a tree list"
datatype_compat tree
derive linorder tree
derive hashable tree
derive countable tree
datatype 'a ttree = TEmpty | TNode 'a "'a ttree list tree"
datatype_compat ttree
derive linorder ttree
derive hashable ttree
derive countable ttree
subsection "Examples from IsaFoR"
datatype ('f,'v) "term" = Var 'v | Fun 'f "('f,'v) term list"
datatype_compat "term"
datatype ('f, 'l) lab =
Lab "('f, 'l) lab" 'l
| FunLab "('f, 'l) lab" "('f, 'l) lab list"
| UnLab 'f
| Sharp "('f, 'l) lab"
datatype_compat lab
derive linorder "term" lab
derive countable "term" lab
derive hashable "term" lab
subsection "A complex datatype"
text ‹
The following datatype has nested indirect recursion, mutual recursion and
uses other datatypes.
›
datatype ('a, 'b) complex =
C1 nat "'a ttree" |
C2 "('a, 'b) complex list tree tree" 'b "('a, 'b) complex" "('a, 'b) complex2 ttree list"
and ('a, 'b) complex2 = D1 "('a, 'b) complex ttree"
datatype_compat complex complex2
derive linorder complex
derive hashable complex
derive countable complex
end