(* Title: HOL/Tools/old_recdef.ML
Author: Konrad Slind, Cambridge University Computer Laboratory
Author: Lucas Dixon, University of Edinburgh
Old TFL/recdef package.
*)
signature CASE_SPLIT =
sig
(* try to recursively split conjectured thm to given list of thms *)
val splitto : Proof.context -> thm list -> thm -> thm
end;
signature UTILS =
sig
exception ERR of {module: string, func: string, mesg: string}
val end_itlist: ('a -> 'a -> 'a) -> 'a list -> 'a
val itlist2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
val pluck: ('a -> bool) -> 'a list -> 'a * 'a list
val zip3: 'a list -> 'b list -> 'c list -> ('a*'b*'c) list
val take: ('a -> 'b) -> int * 'a list -> 'b list
end;
signature USYNTAX =
sig
datatype lambda = VAR of {Name : string, Ty : typ}
| CONST of {Name : string, Ty : typ}
| COMB of {Rator: term, Rand : term}
| LAMB of {Bvar : term, Body : term}
val alpha : typ
(* Types *)
val type_vars : typ -> typ list
val type_varsl : typ list -> typ list
val mk_vartype : string -> typ
val is_vartype : typ -> bool
val strip_prod_type : typ -> typ list
(* Terms *)
val free_vars_lr : term -> term list
val type_vars_in_term : term -> typ list
val dest_term : term -> lambda
(* Prelogic *)
val inst : (typ*typ) list -> term -> term
(* Construction routines *)
val mk_abs :{Bvar : term, Body : term} -> term
val mk_imp :{ant : term, conseq : term} -> term
val mk_select :{Bvar : term, Body : term} -> term
val mk_forall :{Bvar : term, Body : term} -> term
val mk_exists :{Bvar : term, Body : term} -> term
val mk_conj :{conj1 : term, conj2 : term} -> term
val mk_disj :{disj1 : term, disj2 : term} -> term
val mk_pabs :{varstruct : term, body : term} -> term
(* Destruction routines *)
val dest_const: term -> {Name : string, Ty : typ}
val dest_comb : term -> {Rator : term, Rand : term}
val dest_abs : string list -> term -> {Bvar : term, Body : term} * string list
val dest_eq : term -> {lhs : term, rhs : term}
val dest_imp : term -> {ant : term, conseq : term}
val dest_forall : term -> {Bvar : term, Body : term}
val dest_exists : term -> {Bvar : term, Body : term}
val dest_neg : term -> term
val dest_conj : term -> {conj1 : term, conj2 : term}
val dest_disj : term -> {disj1 : term, disj2 : term}
val dest_pair : term -> {fst : term, snd : term}
val dest_pabs : string list -> term -> {varstruct : term, body : term, used : string list}
val lhs : term -> term
val rhs : term -> term
val rand : term -> term
(* Query routines *)
val is_imp : term -> bool
val is_forall : term -> bool
val is_exists : term -> bool
val is_neg : term -> bool
val is_conj : term -> bool
val is_disj : term -> bool
val is_pair : term -> bool
val is_pabs : term -> bool
(* Construction of a term from a list of Preterms *)
val list_mk_abs : (term list * term) -> term
val list_mk_imp : (term list * term) -> term
val list_mk_forall : (term list * term) -> term
val list_mk_conj : term list -> term
(* Destructing a term to a list of Preterms *)
val strip_comb : term -> (term * term list)
val strip_abs : term -> (term list * term)
val strip_imp : term -> (term list * term)
val strip_forall : term -> (term list * term)
val strip_exists : term -> (term list * term)
val strip_disj : term -> term list
(* Miscellaneous *)
val mk_vstruct : typ -> term list -> term
val gen_all : term -> term
val find_term : (term -> bool) -> term -> term option
val dest_relation : term -> term * term * term
val is_WFR : term -> bool
val ARB : typ -> term
end;
signature DCTERM =
sig
val dest_comb: cterm -> cterm * cterm
val dest_abs: string option -> cterm -> cterm * cterm
val capply: cterm -> cterm -> cterm
val cabs: cterm -> cterm -> cterm
val mk_conj: cterm * cterm -> cterm
val mk_disj: cterm * cterm -> cterm
val mk_exists: cterm * cterm -> cterm
val dest_conj: cterm -> cterm * cterm
val dest_const: cterm -> {Name: string, Ty: typ}
val dest_disj: cterm -> cterm * cterm
val dest_eq: cterm -> cterm * cterm
val dest_exists: cterm -> cterm * cterm
val dest_forall: cterm -> cterm * cterm
val dest_imp: cterm -> cterm * cterm
val dest_neg: cterm -> cterm
val dest_pair: cterm -> cterm * cterm
val dest_var: cterm -> {Name:string, Ty:typ}
val is_conj: cterm -> bool
val is_disj: cterm -> bool
val is_eq: cterm -> bool
val is_exists: cterm -> bool
val is_forall: cterm -> bool
val is_imp: cterm -> bool
val is_neg: cterm -> bool
val is_pair: cterm -> bool
val list_mk_disj: cterm list -> cterm
val strip_abs: cterm -> cterm list * cterm
val strip_comb: cterm -> cterm * cterm list
val strip_disj: cterm -> cterm list
val strip_exists: cterm -> cterm list * cterm
val strip_forall: cterm -> cterm list * cterm
val strip_imp: cterm -> cterm list * cterm
val drop_prop: cterm -> cterm
val mk_prop: cterm -> cterm
end;
signature RULES =
sig
val dest_thm: thm -> term list * term
(* Inference rules *)
val REFL: cterm -> thm
val ASSUME: cterm -> thm
val MP: thm -> thm -> thm
val MATCH_MP: thm -> thm -> thm
val CONJUNCT1: thm -> thm
val CONJUNCT2: thm -> thm
val CONJUNCTS: thm -> thm list
val DISCH: cterm -> thm -> thm
val UNDISCH: thm -> thm
val SPEC: cterm -> thm -> thm
val ISPEC: cterm -> thm -> thm
val ISPECL: cterm list -> thm -> thm
val GEN: Proof.context -> cterm -> thm -> thm
val GENL: Proof.context -> cterm list -> thm -> thm
val LIST_CONJ: thm list -> thm
val SYM: thm -> thm
val DISCH_ALL: thm -> thm
val FILTER_DISCH_ALL: (term -> bool) -> thm -> thm
val SPEC_ALL: thm -> thm
val GEN_ALL: Proof.context -> thm -> thm
val IMP_TRANS: thm -> thm -> thm
val PROVE_HYP: thm -> thm -> thm
val CHOOSE: Proof.context -> cterm * thm -> thm -> thm
val EXISTS: cterm * cterm -> thm -> thm
val EXISTL: cterm list -> thm -> thm
val IT_EXISTS: Proof.context -> (cterm * cterm) list -> thm -> thm
val EVEN_ORS: thm list -> thm list
val DISJ_CASESL: thm -> thm list -> thm
val list_beta_conv: cterm -> cterm list -> thm
val SUBS: Proof.context -> thm list -> thm -> thm
val simpl_conv: Proof.context -> thm list -> cterm -> thm
val rbeta: thm -> thm
val tracing: bool Unsynchronized.ref
val CONTEXT_REWRITE_RULE: Proof.context ->
term * term list * thm * thm list -> thm -> thm * term list
val RIGHT_ASSOC: Proof.context -> thm -> thm
val prove: Proof.context -> bool -> term * tactic -> thm
end;
signature THRY =
sig
val match_term: theory -> term -> term -> (term * term) list * (typ * typ) list
val match_type: theory -> typ -> typ -> (typ * typ) list
val typecheck: theory -> term -> cterm
(*datatype facts of various flavours*)
val match_info: theory -> string -> {constructors: term list, case_const: term} option
val induct_info: theory -> string -> {constructors: term list, nchotomy: thm} option
val extract_info: theory -> {case_congs: thm list, case_rewrites: thm list}
end;
signature PRIM =
sig
val trace: bool Unsynchronized.ref
val trace_thms: Proof.context -> string -> thm list -> unit
val trace_cterm: Proof.context -> string -> cterm -> unit
type pattern
val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
val wfrec_definition0: string -> term -> term -> theory -> thm * theory
val post_definition: Proof.context -> thm list -> thm * pattern list ->
{rules: thm,
rows: int list,
TCs: term list list,
full_pats_TCs: (term * term list) list}
val mk_induction: Proof.context ->
{fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm
val postprocess: Proof.context -> bool ->
{wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} ->
{rules: thm, induction: thm, TCs: term list list} ->
{rules: thm, induction: thm, nested_tcs: thm list}
end;
signature TFL =
sig
val define_i: bool -> thm list -> thm list -> xstring -> term -> term list -> Proof.context ->
{lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context
val define: bool -> thm list -> thm list -> xstring -> string -> string list -> Proof.context ->
{lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context
end;
signature OLD_RECDEF =
sig
val get_recdef: theory -> string
-> {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
val get_hints: Proof.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
val simp_add: attribute
val simp_del: attribute
val cong_add: attribute
val cong_del: attribute
val wf_add: attribute
val wf_del: attribute
val add_recdef: bool -> xstring -> string -> ((binding * string) * Token.src list) list ->
Token.src option -> theory -> theory
* {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list ->
theory -> theory * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
end;
structure Old_Recdef: OLD_RECDEF =
struct
(*** extra case splitting for TFL ***)
structure CaseSplit: CASE_SPLIT =
struct
(* make a casethm from an induction thm *)
fun cases_thm_of_induct_thm ctxt =
Seq.hd o (ALLGOALS (fn i => REPEAT (eresolve_tac ctxt [Drule.thin_rl] i)));
(* get the case_thm (my version) from a type *)
fun case_thm_of_ty ctxt ty =
let
val thy = Proof_Context.theory_of ctxt
val ty_str = case ty of
Type(ty_str, _) => ty_str
| TFree(s,_) => error ("Free type: " ^ s)
| TVar((s,_),_) => error ("Free variable: " ^ s)
val {induct, ...} = BNF_LFP_Compat.the_info thy [BNF_LFP_Compat.Keep_Nesting] ty_str
in
cases_thm_of_induct_thm ctxt induct
end;
(* for use when there are no prems to the subgoal *)
(* does a case split on the given variable *)
fun mk_casesplit_goal_thm ctxt (vstr,ty) gt =
let
val thy = Proof_Context.theory_of ctxt;
val x = Free(vstr,ty);
val abst = Abs(vstr, ty, Term.abstract_over (x, gt));
val case_thm = case_thm_of_ty ctxt ty;
val abs_ct = Thm.cterm_of ctxt abst;
val free_ct = Thm.cterm_of ctxt x;
val (Pv, Dv, type_insts) =
case (Thm.concl_of case_thm) of
(_ $ (Pv $ (Dv as Var(_, Dty)))) =>
(Pv, Dv,
Sign.typ_match thy (Dty, ty) Vartab.empty)
| _ => error "not a valid case thm";
val type_cinsts = map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T))
(Vartab.dest type_insts);
val Pv = dest_Var (Envir.subst_term_types type_insts Pv);
val Dv = dest_Var (Envir.subst_term_types type_insts Dv);
in
Conv.fconv_rule Drule.beta_eta_conversion
(case_thm
|> Thm.instantiate (type_cinsts, [])
|> Thm.instantiate ([], [(Pv, abs_ct), (Dv, free_ct)]))
end;
(* the find_XXX_split functions are simply doing a lightwieght (I
think) term matching equivalent to find where to do the next split *)
(* assuming two twems are identical except for a free in one at a
subterm, or constant in another, ie assume that one term is a plit of
another, then gives back the free variable that has been split. *)
exception find_split_exp of string
fun find_term_split (Free v, _ $ _) = SOME v
| find_term_split (Free v, Const _) = SOME v
| find_term_split (Free v, Abs _) = SOME v (* do we really want this case? *)
| find_term_split (Free _, Var _) = NONE (* keep searching *)
| find_term_split (a $ b, a2 $ b2) =
(case find_term_split (a, a2) of
NONE => find_term_split (b,b2)
| vopt => vopt)
| find_term_split (Abs(_,_,t1), Abs(_,_,t2)) =
find_term_split (t1, t2)
| find_term_split (Const (x,_), Const(x2,_)) =
if x = x2 then NONE else (* keep searching *)
raise find_split_exp (* stop now *)
"Terms are not identical upto a free varaible! (Consts)"
| find_term_split (Bound i, Bound j) =
if i = j then NONE else (* keep searching *)
raise find_split_exp (* stop now *)
"Terms are not identical upto a free varaible! (Bound)"
| find_term_split _ =
raise find_split_exp (* stop now *)
"Terms are not identical upto a free varaible! (Other)";
(* assume that "splitth" is a case split form of subgoal i of "genth",
then look for a free variable to split, breaking the subgoal closer to
splitth. *)
fun find_thm_split splitth i genth =
find_term_split (Logic.get_goal (Thm.prop_of genth) i,
Thm.concl_of splitth) handle find_split_exp _ => NONE;
(* as above but searches "splitths" for a theorem that suggest a case split *)
fun find_thms_split splitths i genth =
Library.get_first (fn sth => find_thm_split sth i genth) splitths;
(* split the subgoal i of "genth" until we get to a member of
splitths. Assumes that genth will be a general form of splitths, that
can be case-split, as needed. Otherwise fails. Note: We assume that
all of "splitths" are split to the same level, and thus it doesn't
matter which one we choose to look for the next split. Simply add
search on splitthms and split variable, to change this. *)
(* Note: possible efficiency measure: when a case theorem is no longer
useful, drop it? *)
(* Note: This should not be a separate tactic but integrated into the
case split done during recdef's case analysis, this would avoid us
having to (re)search for variables to split. *)
fun splitto ctxt splitths genth =
let
val _ = not (null splitths) orelse error "splitto: no given splitths";
(* check if we are a member of splitths - FIXME: quicker and
more flexible with discrim net. *)
fun solve_by_splitth th split =
Thm.biresolution (SOME ctxt) false [(false,split)] 1 th;
fun split th =
(case find_thms_split splitths 1 th of
NONE =>
(writeln (cat_lines
(["th:", Display.string_of_thm ctxt th, "split ths:"] @
map (Display.string_of_thm ctxt) splitths @ ["\n--"]));
error "splitto: cannot find variable to split on")
| SOME v =>
let
val gt = HOLogic.dest_Trueprop (#1 (Logic.dest_implies (Thm.prop_of th)));
val split_thm = mk_casesplit_goal_thm ctxt v gt;
val (subthms, expf) = IsaND.fixed_subgoal_thms ctxt split_thm;
in
expf (map recsplitf subthms)
end)
and recsplitf th =
(* note: multiple unifiers! we only take the first element,
probably fine -- there is probably only one anyway. *)
(case get_first (Seq.pull o solve_by_splitth th) splitths of
NONE => split th
| SOME (solved_th, _) => solved_th);
in
recsplitf genth
end;
end;
(*** basic utilities ***)
structure Utils: UTILS =
struct
(*standard exception for TFL*)
exception ERR of {module: string, func: string, mesg: string};
fun UTILS_ERR func mesg = ERR {module = "Utils", func = func, mesg = mesg};
fun end_itlist _ [] = raise (UTILS_ERR "end_itlist" "list too short")
| end_itlist _ [x] = x
| end_itlist f (x :: xs) = f x (end_itlist f xs);
fun itlist2 f L1 L2 base_value =
let fun it ([],[]) = base_value
| it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2))
| it _ = raise UTILS_ERR "itlist2" "different length lists"
in it (L1,L2)
end;
fun pluck p =
let fun remv ([],_) = raise UTILS_ERR "pluck" "item not found"
| remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A)
in fn L => remv(L,[])
end;
fun take f =
let fun grab(0, _) = []
| grab(n, x::rst) = f x::grab(n-1,rst)
in grab
end;
fun zip3 [][][] = []
| zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3
| zip3 _ _ _ = raise UTILS_ERR "zip3" "different lengths";
end;
(*** emulation of HOL's abstract syntax functions ***)
structure USyntax: USYNTAX =
struct
infix 4 ##;
fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg};
(*---------------------------------------------------------------------------
*
* Types
*
*---------------------------------------------------------------------------*)
val mk_prim_vartype = TVar;
fun mk_vartype s = mk_prim_vartype ((s, 0), @{sort type});
(* But internally, it's useful *)
fun dest_vtype (TVar x) = x
| dest_vtype _ = raise USYN_ERR "dest_vtype" "not a flexible type variable";
val is_vartype = can dest_vtype;
val type_vars = map mk_prim_vartype o Misc_Legacy.typ_tvars
fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []);
val alpha = mk_vartype "'a"
val strip_prod_type = HOLogic.flatten_tupleT;
(*---------------------------------------------------------------------------
*
* Terms
*
*---------------------------------------------------------------------------*)
(* Free variables, in order of occurrence, from left to right in the
* syntax tree. *)
fun free_vars_lr tm =
let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end
fun add (t, frees) = case t of
Free _ => if (memb t frees) then frees else t::frees
| Abs (_,_,body) => add(body,frees)
| f$t => add(t, add(f, frees))
| _ => frees
in rev(add(tm,[]))
end;
val type_vars_in_term = map mk_prim_vartype o Misc_Legacy.term_tvars;
(* Prelogic *)
fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty)
fun inst theta = subst_vars (map dest_tybinding theta,[])
(* Construction routines *)
fun mk_abs{Bvar as Var((s,_),ty),Body} = Abs(s,ty,abstract_over(Bvar,Body))
| mk_abs{Bvar as Free(s,ty),Body} = Abs(s,ty,abstract_over(Bvar,Body))
| mk_abs _ = raise USYN_ERR "mk_abs" "Bvar is not a variable";
fun mk_imp{ant,conseq} =
let val c = Const(@{const_name HOL.implies},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in list_comb(c,[ant,conseq])
end;
fun mk_select (r as {Bvar,Body}) =
let val ty = type_of Bvar
val c = Const(@{const_name Eps},(ty --> HOLogic.boolT) --> ty)
in list_comb(c,[mk_abs r])
end;
fun mk_forall (r as {Bvar,Body}) =
let val ty = type_of Bvar
val c = Const(@{const_name All},(ty --> HOLogic.boolT) --> HOLogic.boolT)
in list_comb(c,[mk_abs r])
end;
fun mk_exists (r as {Bvar,Body}) =
let val ty = type_of Bvar
val c = Const(@{const_name Ex},(ty --> HOLogic.boolT) --> HOLogic.boolT)
in list_comb(c,[mk_abs r])
end;
fun mk_conj{conj1,conj2} =
let val c = Const(@{const_name HOL.conj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in list_comb(c,[conj1,conj2])
end;
fun mk_disj{disj1,disj2} =
let val c = Const(@{const_name HOL.disj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in list_comb(c,[disj1,disj2])
end;
fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2);
local
fun mk_uncurry (xt, yt, zt) =
Const(@{const_name case_prod}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
| dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
in
fun mk_pabs{varstruct,body} =
let fun mpa (varstruct, body) =
if is_var varstruct
then mk_abs {Bvar = varstruct, Body = body}
else let val {fst, snd} = dest_pair varstruct
in mk_uncurry (type_of fst, type_of snd, type_of body) $
mpa (fst, mpa (snd, body))
end
in mpa (varstruct, body) end
handle TYPE _ => raise USYN_ERR "mk_pabs" "";
end;
(* Destruction routines *)
datatype lambda = VAR of {Name : string, Ty : typ}
| CONST of {Name : string, Ty : typ}
| COMB of {Rator: term, Rand : term}
| LAMB of {Bvar : term, Body : term};
fun dest_term(Var((s,_),ty)) = VAR{Name = s, Ty = ty}
| dest_term(Free(s,ty)) = VAR{Name = s, Ty = ty}
| dest_term(Const(s,ty)) = CONST{Name = s, Ty = ty}
| dest_term(M$N) = COMB{Rator=M,Rand=N}
| dest_term(Abs(s,ty,M)) = let val v = Free(s,ty)
in LAMB{Bvar = v, Body = Term.betapply (M,v)}
end
| dest_term(Bound _) = raise USYN_ERR "dest_term" "Bound";
fun dest_const(Const(s,ty)) = {Name = s, Ty = ty}
| dest_const _ = raise USYN_ERR "dest_const" "not a constant";
fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2}
| dest_comb _ = raise USYN_ERR "dest_comb" "not a comb";
fun dest_abs used (a as Abs(s, ty, _)) =
let
val s' = singleton (Name.variant_list used) s;
val v = Free(s', ty);
in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
end
| dest_abs _ _ = raise USYN_ERR "dest_abs" "not an abstraction";
fun dest_eq(Const(@{const_name HOL.eq},_) $ M $ N) = {lhs=M, rhs=N}
| dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
fun dest_imp(Const(@{const_name HOL.implies},_) $ M $ N) = {ant=M, conseq=N}
| dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
fun dest_forall(Const(@{const_name All},_) $ (a as Abs _)) = fst (dest_abs [] a)
| dest_forall _ = raise USYN_ERR "dest_forall" "not a forall";
fun dest_exists(Const(@{const_name Ex},_) $ (a as Abs _)) = fst (dest_abs [] a)
| dest_exists _ = raise USYN_ERR "dest_exists" "not an existential";
fun dest_neg(Const(@{const_name Not},_) $ M) = M
| dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
fun dest_conj(Const(@{const_name HOL.conj},_) $ M $ N) = {conj1=M, conj2=N}
| dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction";
fun dest_disj(Const(@{const_name HOL.disj},_) $ M $ N) = {disj1=M, disj2=N}
| dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction";
fun mk_pair{fst,snd} =
let val ty1 = type_of fst
val ty2 = type_of snd
val c = Const(@{const_name Pair},ty1 --> ty2 --> prod_ty ty1 ty2)
in list_comb(c,[fst,snd])
end;
fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
| dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
local fun ucheck t = (if #Name (dest_const t) = @{const_name case_prod} then t
else raise Match)
in
fun dest_pabs used tm =
let val ({Bvar,Body}, used') = dest_abs used tm
in {varstruct = Bvar, body = Body, used = used'}
end handle Utils.ERR _ =>
let val {Rator,Rand} = dest_comb tm
val _ = ucheck Rator
val {varstruct = lv, body, used = used'} = dest_pabs used Rand
val {varstruct = rv, body, used = used''} = dest_pabs used' body
in {varstruct = mk_pair {fst = lv, snd = rv}, body = body, used = used''}
end
end;
val lhs = #lhs o dest_eq
val rhs = #rhs o dest_eq
val rand = #Rand o dest_comb
(* Query routines *)
val is_imp = can dest_imp
val is_forall = can dest_forall
val is_exists = can dest_exists
val is_neg = can dest_neg
val is_conj = can dest_conj
val is_disj = can dest_disj
val is_pair = can dest_pair
val is_pabs = can (dest_pabs [])
(* Construction of a cterm from a list of Terms *)
fun list_mk_abs(L,tm) = fold_rev (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
(* These others are almost never used *)
fun list_mk_imp(A,c) = fold_rev (fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
fun list_mk_forall(V,t) = fold_rev (fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
val list_mk_conj = Utils.end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
(* Need to reverse? *)
fun gen_all tm = list_mk_forall(Misc_Legacy.term_frees tm, tm);
(* Destructing a cterm to a list of Terms *)
fun strip_comb tm =
let fun dest(M$N, A) = dest(M, N::A)
| dest x = x
in dest(tm,[])
end;
fun strip_abs(tm as Abs _) =
let val ({Bvar,Body}, _) = dest_abs [] tm
val (bvs, core) = strip_abs Body
in (Bvar::bvs, core)
end
| strip_abs M = ([],M);
fun strip_imp fm =
if (is_imp fm)
then let val {ant,conseq} = dest_imp fm
val (was,wb) = strip_imp conseq
in ((ant::was), wb)
end
else ([],fm);
fun strip_forall fm =
if (is_forall fm)
then let val {Bvar,Body} = dest_forall fm
val (bvs,core) = strip_forall Body
in ((Bvar::bvs), core)
end
else ([],fm);
fun strip_exists fm =
if (is_exists fm)
then let val {Bvar, Body} = dest_exists fm
val (bvs,core) = strip_exists Body
in (Bvar::bvs, core)
end
else ([],fm);
fun strip_disj w =
if (is_disj w)
then let val {disj1,disj2} = dest_disj w
in (strip_disj disj1@strip_disj disj2)
end
else [w];
(* Miscellaneous *)
fun mk_vstruct ty V =
let fun follow_prod_type (Type(@{type_name Product_Type.prod},[ty1,ty2])) vs =
let val (ltm,vs1) = follow_prod_type ty1 vs
val (rtm,vs2) = follow_prod_type ty2 vs1
in (mk_pair{fst=ltm, snd=rtm}, vs2) end
| follow_prod_type _ (v::vs) = (v,vs)
in #1 (follow_prod_type ty V) end;
(* Search a term for a sub-term satisfying the predicate p. *)
fun find_term p =
let fun find tm =
if (p tm) then SOME tm
else case tm of
Abs(_,_,body) => find body
| (t$u) => (case find t of NONE => find u | some => some)
| _ => NONE
in find
end;
fun dest_relation tm =
if (type_of tm = HOLogic.boolT)
then let val (Const(@{const_name Set.member},_) $ (Const(@{const_name Pair},_)$y$x) $ R) = tm
in (R,y,x)
end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
else raise USYN_ERR "dest_relation" "not a boolean term";
fun is_WFR (Const(@{const_name Wellfounded.wf},_)$_) = true
| is_WFR _ = false;
fun ARB ty = mk_select{Bvar=Free("v",ty),
Body=Const(@{const_name True},HOLogic.boolT)};
end;
(*** derived cterm destructors ***)
structure Dcterm: DCTERM =
struct
fun ERR func mesg = Utils.ERR {module = "Dcterm", func = func, mesg = mesg};
fun dest_comb t = Thm.dest_comb t
handle CTERM (msg, _) => raise ERR "dest_comb" msg;
fun dest_abs a t = Thm.dest_abs a t
handle CTERM (msg, _) => raise ERR "dest_abs" msg;
fun capply t u = Thm.apply t u
handle CTERM (msg, _) => raise ERR "capply" msg;
fun cabs a t = Thm.lambda a t
handle CTERM (msg, _) => raise ERR "cabs" msg;
(*---------------------------------------------------------------------------
* Some simple constructor functions.
*---------------------------------------------------------------------------*)
val mk_hol_const = Thm.cterm_of @{theory_context HOL} o Const;
fun mk_exists (r as (Bvar, Body)) =
let val ty = Thm.typ_of_cterm Bvar
val c = mk_hol_const(@{const_name Ex}, (ty --> HOLogic.boolT) --> HOLogic.boolT)
in capply c (uncurry cabs r) end;
local val c = mk_hol_const(@{const_name HOL.conj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
end;
local val c = mk_hol_const(@{const_name HOL.disj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
end;
(*---------------------------------------------------------------------------
* The primitives.
*---------------------------------------------------------------------------*)
fun dest_const ctm =
(case Thm.term_of ctm
of Const(s,ty) => {Name = s, Ty = ty}
| _ => raise ERR "dest_const" "not a constant");
fun dest_var ctm =
(case Thm.term_of ctm
of Var((s,_),ty) => {Name=s, Ty=ty}
| Free(s,ty) => {Name=s, Ty=ty}
| _ => raise ERR "dest_var" "not a variable");
(*---------------------------------------------------------------------------
* Derived destructor operations.
*---------------------------------------------------------------------------*)
fun dest_monop expected tm =
let
fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected);
val (c, N) = dest_comb tm handle Utils.ERR _ => err ();
val name = #Name (dest_const c handle Utils.ERR _ => err ());
in if name = expected then N else err () end;
fun dest_binop expected tm =
let
fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected);
val (M, N) = dest_comb tm handle Utils.ERR _ => err ()
in (dest_monop expected M, N) handle Utils.ERR _ => err () end;
fun dest_binder expected tm =
dest_abs NONE (dest_monop expected tm)
handle Utils.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
val dest_neg = dest_monop @{const_name Not}
val dest_pair = dest_binop @{const_name Pair}
val dest_eq = dest_binop @{const_name HOL.eq}
val dest_imp = dest_binop @{const_name HOL.implies}
val dest_conj = dest_binop @{const_name HOL.conj}
val dest_disj = dest_binop @{const_name HOL.disj}
val dest_exists = dest_binder @{const_name Ex}
val dest_forall = dest_binder @{const_name All}
(* Query routines *)
val is_eq = can dest_eq
val is_imp = can dest_imp
val is_forall = can dest_forall
val is_exists = can dest_exists
val is_neg = can dest_neg
val is_conj = can dest_conj
val is_disj = can dest_disj
val is_pair = can dest_pair
(*---------------------------------------------------------------------------
* Iterated creation.
*---------------------------------------------------------------------------*)
val list_mk_disj = Utils.end_itlist (fn d1 => fn tm => mk_disj (d1, tm));
(*---------------------------------------------------------------------------
* Iterated destruction. (To the "right" in a term.)
*---------------------------------------------------------------------------*)
fun strip break tm =
let fun dest (p as (ctm,accum)) =
let val (M,N) = break ctm
in dest (N, M::accum)
end handle Utils.ERR _ => p
in dest (tm,[])
end;
fun rev2swap (x,l) = (rev l, x);
val strip_comb = strip (Library.swap o dest_comb) (* Goes to the "left" *)
val strip_imp = rev2swap o strip dest_imp
val strip_abs = rev2swap o strip (dest_abs NONE)
val strip_forall = rev2swap o strip dest_forall
val strip_exists = rev2swap o strip dest_exists
val strip_disj = rev o (op::) o strip dest_disj
(*---------------------------------------------------------------------------
* Going into and out of prop
*---------------------------------------------------------------------------*)
fun is_Trueprop ct =
(case Thm.term_of ct of
Const (@{const_name Trueprop}, _) $ _ => true
| _ => false);
fun mk_prop ct = if is_Trueprop ct then ct else Thm.apply @{cterm Trueprop} ct;
fun drop_prop ct = if is_Trueprop ct then Thm.dest_arg ct else ct;
end;
(*** emulation of HOL inference rules for TFL ***)
structure Rules: RULES =
struct
fun RULES_ERR func mesg = Utils.ERR {module = "Rules", func = func, mesg = mesg};
fun cconcl thm = Dcterm.drop_prop (#prop (Thm.crep_thm thm));
fun chyps thm = map Dcterm.drop_prop (#hyps (Thm.crep_thm thm));
fun dest_thm thm =
let val {prop,hyps,...} = Thm.rep_thm thm
in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop) end
handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop";
(* Inference rules *)
(*---------------------------------------------------------------------------
* Equality (one step)
*---------------------------------------------------------------------------*)
fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq
handle THM (msg, _, _) => raise RULES_ERR "REFL" msg;
fun SYM thm = thm RS sym
handle THM (msg, _, _) => raise RULES_ERR "SYM" msg;
fun ALPHA thm ctm1 =
let
val ctm2 = Thm.cprop_of thm;
val ctm2_eq = Thm.reflexive ctm2;
val ctm1_eq = Thm.reflexive ctm1;
in Thm.equal_elim (Thm.transitive ctm2_eq ctm1_eq) thm end
handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg;
fun rbeta th =
(case Dcterm.strip_comb (cconcl th) of
(_, [_, r]) => Thm.transitive th (Thm.beta_conversion false r)
| _ => raise RULES_ERR "rbeta" "");
(*----------------------------------------------------------------------------
* Implication and the assumption list
*
* Assumptions get stuck on the meta-language assumption list. Implications
* are in the object language, so discharging an assumption "A" from theorem
* "B" results in something that looks like "A --> B".
*---------------------------------------------------------------------------*)
fun ASSUME ctm = Thm.assume (Dcterm.mk_prop ctm);
(*---------------------------------------------------------------------------
* Implication in TFL is -->. Meta-language implication (==>) is only used
* in the implementation of some of the inference rules below.
*---------------------------------------------------------------------------*)
fun MP th1 th2 = th2 RS (th1 RS mp)
handle THM (msg, _, _) => raise RULES_ERR "MP" msg;
(*forces the first argument to be a proposition if necessary*)
fun DISCH tm thm = Thm.implies_intr (Dcterm.mk_prop tm) thm COMP impI
handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;
fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm;
fun FILTER_DISCH_ALL P thm =
let fun check tm = P (Thm.term_of tm)
in fold_rev (fn tm => fn th => if check tm then DISCH tm th else th) (chyps thm) thm
end;
fun UNDISCH thm =
let val tm = Dcterm.mk_prop (#1 (Dcterm.dest_imp (cconcl thm)))
in Thm.implies_elim (thm RS mp) (ASSUME tm) end
handle Utils.ERR _ => raise RULES_ERR "UNDISCH" ""
| THM _ => raise RULES_ERR "UNDISCH" "";
fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath;
fun IMP_TRANS th1 th2 = th2 RS (th1 RS @{thm tfl_imp_trans})
handle THM (msg, _, _) => raise RULES_ERR "IMP_TRANS" msg;
(*----------------------------------------------------------------------------
* Conjunction
*---------------------------------------------------------------------------*)
fun CONJUNCT1 thm = thm RS conjunct1
handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT1" msg;
fun CONJUNCT2 thm = thm RS conjunct2
handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg;
fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle Utils.ERR _ => [th];
fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list"
| LIST_CONJ [th] = th
| LIST_CONJ (th :: rst) = MP (MP (conjI COMP (impI RS impI)) th) (LIST_CONJ rst)
handle THM (msg, _, _) => raise RULES_ERR "LIST_CONJ" msg;
(*----------------------------------------------------------------------------
* Disjunction
*---------------------------------------------------------------------------*)
local
val prop = Thm.prop_of disjI1
val [_,Q] = Misc_Legacy.term_vars prop
val disj1 = Thm.forall_intr (Thm.cterm_of @{context} Q) disjI1
in
fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1)
handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
end;
local
val prop = Thm.prop_of disjI2
val [P,_] = Misc_Legacy.term_vars prop
val disj2 = Thm.forall_intr (Thm.cterm_of @{context} P) disjI2
in
fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2)
handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
end;
(*----------------------------------------------------------------------------
*
* A1 |- M1, ..., An |- Mn
* ---------------------------------------------------
* [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn]
*
*---------------------------------------------------------------------------*)
fun EVEN_ORS thms =
let fun blue ldisjs [] _ = []
| blue ldisjs (th::rst) rdisjs =
let val tail = tl rdisjs
val rdisj_tl = Dcterm.list_mk_disj tail
in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl)
:: blue (ldisjs @ [cconcl th]) rst tail
end handle Utils.ERR _ => [fold_rev DISJ2 ldisjs th]
in blue [] thms (map cconcl thms) end;
(*----------------------------------------------------------------------------
*
* A |- P \/ Q B,P |- R C,Q |- R
* ---------------------------------------------------
* A U B U C |- R
*
*---------------------------------------------------------------------------*)
fun DISJ_CASES th1 th2 th3 =
let
val c = Dcterm.drop_prop (cconcl th1);
val (disj1, disj2) = Dcterm.dest_disj c;
val th2' = DISCH disj1 th2;
val th3' = DISCH disj2 th3;
in
th3' RS (th2' RS (th1 RS @{thm tfl_disjE}))
handle THM (msg, _, _) => raise RULES_ERR "DISJ_CASES" msg
end;
(*-----------------------------------------------------------------------------
*
* |- A1 \/ ... \/ An [A1 |- M, ..., An |- M]
* ---------------------------------------------------
* |- M
*
* Note. The list of theorems may be all jumbled up, so we have to
* first organize it to align with the first argument (the disjunctive
* theorem).
*---------------------------------------------------------------------------*)
fun organize eq = (* a bit slow - analogous to insertion sort *)
let fun extract a alist =
let fun ex (_,[]) = raise RULES_ERR "organize" "not a permutation.1"
| ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t)
in ex ([],alist)
end
fun place [] [] = []
| place (a::rst) alist =
let val (item,next) = extract a alist
in item::place rst next
end
| place _ _ = raise RULES_ERR "organize" "not a permutation.2"
in place
end;
fun DISJ_CASESL disjth thl =
let val c = cconcl disjth
fun eq th atm =
exists (fn t => HOLogic.dest_Trueprop t aconv Thm.term_of atm) (Thm.hyps_of th)
val tml = Dcterm.strip_disj c
fun DL _ [] = raise RULES_ERR "DISJ_CASESL" "no cases"
| DL th [th1] = PROVE_HYP th th1
| DL th [th1,th2] = DISJ_CASES th th1 th2
| DL th (th1::rst) =
let val tm = #2 (Dcterm.dest_disj (Dcterm.drop_prop(cconcl th)))
in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
in DL disjth (organize eq tml thl)
end;
(*----------------------------------------------------------------------------
* Universals
*---------------------------------------------------------------------------*)
local (* this is fragile *)
val prop = Thm.prop_of spec
val x = hd (tl (Misc_Legacy.term_vars prop))
val TV = dest_TVar (type_of x)
val gspec = Thm.forall_intr (Thm.cterm_of @{context} x) spec
in
fun SPEC tm thm =
let val gspec' = Drule.instantiate_normalize ([(TV, Thm.ctyp_of_cterm tm)], []) gspec
in thm RS (Thm.forall_elim tm gspec') end
end;
fun SPEC_ALL thm = fold SPEC (#1 (Dcterm.strip_forall(cconcl thm))) thm;
val ISPEC = SPEC
val ISPECL = fold ISPEC;
(* Not optimized! Too complicated. *)
local
val prop = Thm.prop_of allI
val [P] = Misc_Legacy.add_term_vars (prop, [])
fun cty_theta ctxt = map (fn (i, (S, ty)) => ((i, S), Thm.ctyp_of ctxt ty))
fun ctm_theta ctxt =
map (fn (i, (_, tm2)) =>
let val ctm2 = Thm.cterm_of ctxt tm2
in ((i, Thm.typ_of_cterm ctm2), ctm2) end)
fun certify ctxt (ty_theta,tm_theta) =
(cty_theta ctxt (Vartab.dest ty_theta),
ctm_theta ctxt (Vartab.dest tm_theta))
in
fun GEN ctxt v th =
let val gth = Thm.forall_intr v th
val thy = Proof_Context.theory_of ctxt
val Const(@{const_name Pure.all},_)$Abs(x,ty,rst) = Thm.prop_of gth
val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *)
val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
val allI2 = Drule.instantiate_normalize (certify ctxt theta) allI
val thm = Thm.implies_elim allI2 gth
val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm
val prop' = tp $ (A $ Abs(x,ty,M))
in ALPHA thm (Thm.cterm_of ctxt prop') end
end;
fun GENL ctxt = fold_rev (GEN ctxt);
fun GEN_ALL ctxt thm =
let
val prop = Thm.prop_of thm
val vlist = map (Thm.cterm_of ctxt) (Misc_Legacy.add_term_vars (prop, []))
in GENL ctxt vlist thm end;
fun MATCH_MP th1 th2 =
if (Dcterm.is_forall (Dcterm.drop_prop(cconcl th1)))
then MATCH_MP (th1 RS spec) th2
else MP th1 th2;
(*----------------------------------------------------------------------------
* Existentials
*---------------------------------------------------------------------------*)
(*---------------------------------------------------------------------------
* Existential elimination
*
* A1 |- ?x.t[x] , A2, "t[v]" |- t'
* ------------------------------------ (variable v occurs nowhere)
* A1 u A2 |- t'
*
*---------------------------------------------------------------------------*)
fun CHOOSE ctxt (fvar, exth) fact =
let
val lam = #2 (Dcterm.dest_comb (Dcterm.drop_prop (cconcl exth)))
val redex = Dcterm.capply lam fvar
val t$u = Thm.term_of redex
val residue = Thm.cterm_of ctxt (Term.betapply (t, u))
in
GEN ctxt fvar (DISCH residue fact) RS (exth RS @{thm tfl_exE})
handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
end;
local
val prop = Thm.prop_of exI
val [P, x] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars prop)
in
fun EXISTS (template,witness) thm =
let val abstr = #2 (Dcterm.dest_comb template) in
thm RS (cterm_instantiate [(P, abstr), (x, witness)] exI)
handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
end
end;
(*----------------------------------------------------------------------------
*
* A |- M
* ------------------- [v_1,...,v_n]
* A |- ?v1...v_n. M
*
*---------------------------------------------------------------------------*)
fun EXISTL vlist th =
fold_rev (fn v => fn thm => EXISTS(Dcterm.mk_exists(v,cconcl thm), v) thm)
vlist th;
(*----------------------------------------------------------------------------
*
* A |- M[x_1,...,x_n]
* ---------------------------- [(x |-> y)_1,...,(x |-> y)_n]
* A |- ?y_1...y_n. M
*
*---------------------------------------------------------------------------*)
(* Could be improved, but needs "subst_free" for certified terms *)
fun IT_EXISTS ctxt blist th =
let
val blist' = map (apply2 Thm.term_of) blist
fun ex v M = Thm.cterm_of ctxt (USyntax.mk_exists{Bvar=v,Body = M})
in
fold_rev (fn (b as (r1,r2)) => fn thm =>
EXISTS(ex r2 (subst_free [b]
(HOLogic.dest_Trueprop(Thm.prop_of thm))), Thm.cterm_of ctxt r1)
thm)
blist' th
end;
(*---------------------------------------------------------------------------
* Faster version, that fails for some as yet unknown reason
* fun IT_EXISTS blist th =
* let val {thy,...} = rep_thm th
* val tych = cterm_of thy
* fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y)
* in
* fold (fn (b as (r1,r2), thm) =>
* EXISTS(D.mk_exists(r2, tych(subst_free[detype b](#t(rep_cterm(cconcl thm))))),
* r1) thm) blist th
* end;
*---------------------------------------------------------------------------*)
(*----------------------------------------------------------------------------
* Rewriting
*---------------------------------------------------------------------------*)
fun SUBS ctxt thl =
rewrite_rule ctxt (map (fn th => th RS eq_reflection handle THM _ => th) thl);
val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE));
fun simpl_conv ctxt thl ctm =
rew_conv (ctxt addsimps thl) ctm RS meta_eq_to_obj_eq;
fun RIGHT_ASSOC ctxt = rewrite_rule ctxt @{thms tfl_disj_assoc};
(*---------------------------------------------------------------------------
* TERMINATION CONDITION EXTRACTION
*---------------------------------------------------------------------------*)
(* Object language quantifier, i.e., "!" *)
fun Forall v M = USyntax.mk_forall{Bvar=v, Body=M};
(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
fun is_cong thm =
case (Thm.prop_of thm) of
(Const(@{const_name Pure.imp},_)$(Const(@{const_name Trueprop},_)$ _) $
(Const(@{const_name Pure.eq},_) $ (Const (@{const_name Wfrec.cut},_) $ _ $ _ $ _ $ _) $ _)) =>
false
| _ => true;
fun dest_equal(Const (@{const_name Pure.eq},_) $
(Const (@{const_name Trueprop},_) $ lhs)
$ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs}
| dest_equal(Const (@{const_name Pure.eq},_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}
| dest_equal tm = USyntax.dest_eq tm;
fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
fun dest_all used (Const(@{const_name Pure.all},_) $ (a as Abs _)) = USyntax.dest_abs used a
| dest_all _ _ = raise RULES_ERR "dest_all" "not a !!";
val is_all = can (dest_all []);
fun strip_all used fm =
if (is_all fm)
then let val ({Bvar, Body}, used') = dest_all used fm
val (bvs, core, used'') = strip_all used' Body
in ((Bvar::bvs), core, used'')
end
else ([], fm, used);
fun list_break_all(Const(@{const_name Pure.all},_) $ Abs (s,ty,body)) =
let val (L,core) = list_break_all body
in ((s,ty)::L, core)
end
| list_break_all tm = ([],tm);
(*---------------------------------------------------------------------------
* Rename a term of the form
*
* !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn
* ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn.
* to one of
*
* !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn
* ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn.
*
* This prevents name problems in extraction, and helps the result to read
* better. There is a problem with varstructs, since they can introduce more
* than n variables, and some extra reasoning needs to be done.
*---------------------------------------------------------------------------*)
fun get ([],_,L) = rev L
| get (ant::rst,n,L) =
case (list_break_all ant)
of ([],_) => get (rst, n+1,L)
| (_,body) =>
let val eq = Logic.strip_imp_concl body
val (f,_) = USyntax.strip_comb (get_lhs eq)
val (vstrl,_) = USyntax.strip_abs f
val names =
Name.variant_list (Misc_Legacy.add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
in get (rst, n+1, (names,n)::L) end
handle TERM _ => get (rst, n+1, L)
| Utils.ERR _ => get (rst, n+1, L);
(* Note: Thm.rename_params_rule counts from 1, not 0 *)
fun rename thm =
let
val ants = Logic.strip_imp_prems (Thm.prop_of thm)
val news = get (ants,1,[])
in fold Thm.rename_params_rule news thm end;
(*---------------------------------------------------------------------------
* Beta-conversion to the rhs of an equation (taken from hol90/drule.sml)
*---------------------------------------------------------------------------*)
fun list_beta_conv tm =
let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(Dcterm.dest_eq(cconcl th))))
fun iter [] = Thm.reflexive tm
| iter (v::rst) = rbeta (Thm.combination(iter rst) (Thm.reflexive v))
in iter end;
(*---------------------------------------------------------------------------
* Trace information for the rewriter
*---------------------------------------------------------------------------*)
val tracing = Unsynchronized.ref false;
fun say s = if !tracing then writeln s else ();
fun print_thms ctxt s L =
say (cat_lines (s :: map (Display.string_of_thm ctxt) L));
fun print_term ctxt s t =
say (cat_lines [s, Syntax.string_of_term ctxt t]);
(*---------------------------------------------------------------------------
* General abstraction handlers, should probably go in USyntax.
*---------------------------------------------------------------------------*)
fun mk_aabs (vstr, body) =
USyntax.mk_abs {Bvar = vstr, Body = body}
handle Utils.ERR _ => USyntax.mk_pabs {varstruct = vstr, body = body};
fun list_mk_aabs (vstrl,tm) =
fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
fun dest_aabs used tm =
let val ({Bvar,Body}, used') = USyntax.dest_abs used tm
in (Bvar, Body, used') end
handle Utils.ERR _ =>
let val {varstruct, body, used} = USyntax.dest_pabs used tm
in (varstruct, body, used) end;
fun strip_aabs used tm =
let val (vstr, body, used') = dest_aabs used tm
val (bvs, core, used'') = strip_aabs used' body
in (vstr::bvs, core, used'') end
handle Utils.ERR _ => ([], tm, used);
fun dest_combn tm 0 = (tm,[])
| dest_combn tm n =
let val {Rator,Rand} = USyntax.dest_comb tm
val (f,rands) = dest_combn Rator (n-1)
in (f,Rand::rands)
end;
local fun dest_pair M = let val {fst,snd} = USyntax.dest_pair M in (fst,snd) end
fun mk_fst tm =
let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
in Const (@{const_name Product_Type.fst}, ty --> fty) $ tm end
fun mk_snd tm =
let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
in Const (@{const_name Product_Type.snd}, ty --> sty) $ tm end
in
fun XFILL tych x vstruct =
let fun traverse p xocc L =
if (is_Free p)
then tych xocc::L
else let val (p1,p2) = dest_pair p
in traverse p1 (mk_fst xocc) (traverse p2 (mk_snd xocc) L)
end
in
traverse vstruct x []
end end;
(*---------------------------------------------------------------------------
* Replace a free tuple (vstr) by a universally quantified variable (a).
* Note that the notion of "freeness" for a tuple is different than for a
* variable: if variables in the tuple also occur in any other place than
* an occurrences of the tuple, they aren't "free" (which is thus probably
* the wrong word to use).
*---------------------------------------------------------------------------*)
fun VSTRUCT_ELIM ctxt tych a vstr th =
let val L = USyntax.free_vars_lr vstr
val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
val thm1 = Thm.implies_intr bind1 (SUBS ctxt [SYM(Thm.assume bind1)] th)
val thm2 = forall_intr_list (map tych L) thm1
val thm3 = forall_elim_list (XFILL tych a vstr) thm2
in refl RS
rewrite_rule ctxt [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3
end;
fun PGEN ctxt tych a vstr th =
let val a1 = tych a
val vstr1 = tych vstr
in
Thm.forall_intr a1
(if (is_Free vstr)
then cterm_instantiate [(vstr1,a1)] th
else VSTRUCT_ELIM ctxt tych a vstr th)
end;
(*---------------------------------------------------------------------------
* Takes apart a paired beta-redex, looking like "(\(x,y).N) vstr", into
*
* (([x,y],N),vstr)
*---------------------------------------------------------------------------*)
fun dest_pbeta_redex used M n =
let val (f,args) = dest_combn M n
val _ = dest_aabs used f
in (strip_aabs used f,args)
end;
fun pbeta_redex M n = can (fn t => dest_pbeta_redex [] t n) M;
fun dest_impl tm =
let val ants = Logic.strip_imp_prems tm
val eq = Logic.strip_imp_concl tm
in (ants,get_lhs eq)
end;
fun restricted t = is_some (USyntax.find_term
(fn (Const(@{const_name Wfrec.cut},_)) =>true | _ => false)
t)
fun CONTEXT_REWRITE_RULE main_ctxt (func, G, cut_lemma, congs) th =
let val globals = func::G
val ctxt0 = empty_simpset main_ctxt
val pbeta_reduce = simpl_conv ctxt0 [@{thm split_conv} RS eq_reflection];
val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
val cut_lemma' = cut_lemma RS eq_reflection
fun prover used ctxt thm =
let fun cong_prover ctxt thm =
let val _ = say "cong_prover:"
val cntxt = Simplifier.prems_of ctxt
val _ = print_thms ctxt "cntxt:" cntxt
val _ = say "cong rule:"
val _ = say (Display.string_of_thm ctxt thm)
(* Unquantified eliminate *)
fun uq_eliminate (thm,imp) =
let val tych = Thm.cterm_of ctxt
val _ = print_term ctxt "To eliminate:" imp
val ants = map tych (Logic.strip_imp_prems imp)
val eq = Logic.strip_imp_concl imp
val lhs = tych(get_lhs eq)
val ctxt' = Simplifier.add_prems (map ASSUME ants) ctxt
val lhs_eq_lhs1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used) ctxt' lhs
handle Utils.ERR _ => Thm.reflexive lhs
val _ = print_thms ctxt' "proven:" [lhs_eq_lhs1]
val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
in
lhs_eeq_lhs2 COMP thm
end
fun pq_eliminate (thm, vlist, imp_body, lhs_eq) =
let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
val _ = forall (op aconv) (ListPair.zip (vlist, args))
orelse error "assertion failed in CONTEXT_REWRITE_RULE"
val imp_body1 = subst_free (ListPair.zip (args, vstrl))
imp_body
val tych = Thm.cterm_of ctxt
val ants1 = map tych (Logic.strip_imp_prems imp_body1)
val eq1 = Logic.strip_imp_concl imp_body1
val Q = get_lhs eq1
val QeqQ1 = pbeta_reduce (tych Q)
val Q1 = #2(Dcterm.dest_eq(cconcl QeqQ1))
val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt
val Q1eeqQ2 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used') ctxt' Q1
handle Utils.ERR _ => Thm.reflexive Q1
val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)
val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
val QeeqQ3 = Thm.transitive thA Q2eeqQ3 handle THM _ =>
((Q2eeqQ3 RS meta_eq_to_obj_eq)
RS ((thA RS meta_eq_to_obj_eq) RS trans))
RS eq_reflection
val impth = implies_intr_list ants1 QeeqQ3
val impth1 = impth RS meta_eq_to_obj_eq
(* Need to abstract *)
val ant_th = Utils.itlist2 (PGEN ctxt' tych) args vstrl impth1
in ant_th COMP thm
end
fun q_eliminate (thm, imp) =
let val (vlist, imp_body, used') = strip_all used imp
val (ants,Q) = dest_impl imp_body
in if (pbeta_redex Q) (length vlist)
then pq_eliminate (thm, vlist, imp_body, Q)
else
let val tych = Thm.cterm_of ctxt
val ants1 = map tych ants
val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt
val Q_eeq_Q1 = Raw_Simplifier.rewrite_cterm
(false,true,false) (prover used') ctxt' (tych Q)
handle Utils.ERR _ => Thm.reflexive (tych Q)
val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
in
ant_th COMP thm
end end
fun eliminate thm =
case Thm.prop_of thm of
Const(@{const_name Pure.imp},_) $ imp $ _ =>
eliminate
(if not(is_all imp)
then uq_eliminate (thm, imp)
else q_eliminate (thm, imp))
(* Assume that the leading constant is ==, *)
| _ => thm (* if it is not a ==> *)
in SOME(eliminate (rename thm)) end
handle Utils.ERR _ => NONE (* FIXME handle THM as well?? *)
fun restrict_prover ctxt thm =
let val _ = say "restrict_prover:"
val cntxt = rev (Simplifier.prems_of ctxt)
val _ = print_thms ctxt "cntxt:" cntxt
val Const(@{const_name Pure.imp},_) $ (Const(@{const_name Trueprop},_) $ A) $ _ =
Thm.prop_of thm
fun genl tm = let val vlist = subtract (op aconv) globals
(Misc_Legacy.add_term_frees(tm,[]))
in fold_rev Forall vlist tm
end
(*--------------------------------------------------------------
* This actually isn't quite right, since it will think that
* not-fully applied occs. of "f" in the context mean that the
* current call is nested. The real solution is to pass in a
* term "f v1..vn" which is a pattern that any full application
* of "f" will match.
*-------------------------------------------------------------*)
val func_name = #1(dest_Const func)
fun is_func (Const (name,_)) = (name = func_name)
| is_func _ = false
val rcontext = rev cntxt
val cncl = HOLogic.dest_Trueprop o Thm.prop_of
val antl = case rcontext of [] => []
| _ => [USyntax.list_mk_conj(map cncl rcontext)]
val TC = genl(USyntax.list_mk_imp(antl, A))
val _ = print_term ctxt "func:" func
val _ = print_term ctxt "TC:" (HOLogic.mk_Trueprop TC)
val _ = tc_list := (TC :: !tc_list)
val nestedp = is_some (USyntax.find_term is_func TC)
val _ = if nestedp then say "nested" else say "not_nested"
val th' = if nestedp then raise RULES_ERR "solver" "nested function"
else let val cTC = Thm.cterm_of ctxt (HOLogic.mk_Trueprop TC)
in case rcontext of
[] => SPEC_ALL(ASSUME cTC)
| _ => MP (SPEC_ALL (ASSUME cTC))
(LIST_CONJ rcontext)
end
val th'' = th' RS thm
in SOME (th'')
end handle Utils.ERR _ => NONE (* FIXME handle THM as well?? *)
in
(if (is_cong thm) then cong_prover else restrict_prover) ctxt thm
end
val ctm = Thm.cprop_of th
val names = Misc_Legacy.add_term_names (Thm.term_of ctm, [])
val th1 =
Raw_Simplifier.rewrite_cterm (false, true, false)
(prover names) (ctxt0 addsimps [cut_lemma'] |> fold Simplifier.add_eqcong congs) ctm
val th2 = Thm.equal_elim th1 th
in
(th2, filter_out restricted (!tc_list))
end;
fun prove ctxt strict (t, tac) =
let
val ctxt' = Variable.auto_fixes t ctxt;
in
if strict
then Goal.prove ctxt' [] [] t (K tac)
else Goal.prove ctxt' [] [] t (K tac)
handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg)
end;
end;
(*** theory operations ***)
structure Thry: THRY =
struct
fun THRY_ERR func mesg = Utils.ERR {module = "Thry", func = func, mesg = mesg};
(*---------------------------------------------------------------------------
* Matching
*---------------------------------------------------------------------------*)
local
fun tybind (ixn, (S, T)) = (TVar (ixn, S), T);
in
fun match_term thry pat ob =
let
val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty);
fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.subst_type ty_theta T), t)
in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
end;
fun match_type thry pat ob =
map tybind (Vartab.dest (Sign.typ_match thry (pat, ob) Vartab.empty));
end;
(*---------------------------------------------------------------------------
* Typing
*---------------------------------------------------------------------------*)
fun typecheck thy t =
Thm.global_cterm_of thy t
handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg
| TERM (msg, _) => raise THRY_ERR "typecheck" msg;
(*---------------------------------------------------------------------------
* Get information about datatypes
*---------------------------------------------------------------------------*)
fun match_info thy dtco =
case (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] dtco,
BNF_LFP_Compat.get_constrs thy dtco) of
(SOME {case_name, ... }, SOME constructors) =>
SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors}
| _ => NONE;
fun induct_info thy dtco = case BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] dtco of
NONE => NONE
| SOME {nchotomy, ...} =>
SOME {nchotomy = nchotomy,
constructors = (map Const o the o BNF_LFP_Compat.get_constrs thy) dtco};
fun extract_info thy =
let val infos = map snd (Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting]))
in {case_congs = map (mk_meta_eq o #case_cong) infos,
case_rewrites = maps (map mk_meta_eq o #case_rewrites) infos}
end;
end;
(*** first part of main module ***)
structure Prim: PRIM =
struct
val trace = Unsynchronized.ref false;
fun TFL_ERR func mesg = Utils.ERR {module = "Tfl", func = func, mesg = mesg};
val concl = #2 o Rules.dest_thm;
val list_mk_type = Utils.end_itlist (curry (op -->));
fun front_last [] = raise TFL_ERR "front_last" "empty list"
| front_last [x] = ([],x)
| front_last (h::t) =
let val (pref,x) = front_last t
in
(h::pref,x)
end;
(*---------------------------------------------------------------------------
* The next function is common to pattern-match translation and
* proof of completeness of cases for the induction theorem.
*
* The curried function "gvvariant" returns a function to generate distinct
* variables that are guaranteed not to be in names. The names of
* the variables go u, v, ..., z, aa, ..., az, ... The returned
* function contains embedded refs!
*---------------------------------------------------------------------------*)
fun gvvariant names =
let val slist = Unsynchronized.ref names
val vname = Unsynchronized.ref "u"
fun new() =
if member (op =) (!slist) (!vname)
then (vname := Symbol.bump_string (!vname); new())
else (slist := !vname :: !slist; !vname)
in
fn ty => Free(new(), ty)
end;
(*---------------------------------------------------------------------------
* Used in induction theorem production. This is the simple case of
* partitioning up pattern rows by the leading constructor.
*---------------------------------------------------------------------------*)
fun ipartition gv (constructors,rows) =
let fun pfail s = raise TFL_ERR "partition.part" s
fun part {constrs = [], rows = [], A} = rev A
| part {constrs = [], rows = _::_, A} = pfail"extra cases in defn"
| part {constrs = _::_, rows = [], A} = pfail"cases missing in defn"
| part {constrs = c::crst, rows, A} =
let val (c, T) = dest_Const c
val L = binder_types T
val (in_group, not_in_group) =
fold_rev (fn (row as (p::rst, rhs)) =>
fn (in_group,not_in_group) =>
let val (pc,args) = USyntax.strip_comb p
in if (#1(dest_Const pc) = c)
then ((args@rst, rhs)::in_group, not_in_group)
else (in_group, row::not_in_group)
end) rows ([],[])
val col_types = Utils.take type_of (length L, #1(hd in_group))
in
part{constrs = crst, rows = not_in_group,
A = {constructor = c,
new_formals = map gv col_types,
group = in_group}::A}
end
in part{constrs = constructors, rows = rows, A = []}
end;
(*---------------------------------------------------------------------------
* Each pattern carries with it a tag (i,b) where
* i is the clause it came from and
* b=true indicates that clause was given by the user
* (or is an instantiation of a user supplied pattern)
* b=false --> i = ~1
*---------------------------------------------------------------------------*)
type pattern = term * (int * bool)
fun pattern_map f (tm,x) = (f tm, x);
fun pattern_subst theta = pattern_map (subst_free theta);
val pat_of = fst;
fun row_of_pat x = fst (snd x);
fun given x = snd (snd x);
(*---------------------------------------------------------------------------
* Produce an instance of a constructor, plus genvars for its arguments.
*---------------------------------------------------------------------------*)
fun fresh_constr ty_match colty gv c =
let val (_,Ty) = dest_Const c
val L = binder_types Ty
and ty = body_type Ty
val ty_theta = ty_match ty colty
val c' = USyntax.inst ty_theta c
val gvars = map (USyntax.inst ty_theta o gv) L
in (c', gvars)
end;
(*---------------------------------------------------------------------------
* Goes through a list of rows and picks out the ones beginning with a
* pattern with constructor = name.
*---------------------------------------------------------------------------*)
fun mk_group name rows =
fold_rev (fn (row as ((prfx, p::rst), rhs)) =>
fn (in_group,not_in_group) =>
let val (pc,args) = USyntax.strip_comb p
in if ((#1 (Term.dest_Const pc) = name) handle TERM _ => false)
then (((prfx,args@rst), rhs)::in_group, not_in_group)
else (in_group, row::not_in_group) end)
rows ([],[]);
(*---------------------------------------------------------------------------
* Partition the rows. Not efficient: we should use hashing.
*---------------------------------------------------------------------------*)
fun partition _ _ (_,_,_,[]) = raise TFL_ERR "partition" "no rows"
| partition gv ty_match
(constructors, colty, res_ty, rows as (((prfx,_),_)::_)) =
let val fresh = fresh_constr ty_match colty gv
fun part {constrs = [], rows, A} = rev A
| part {constrs = c::crst, rows, A} =
let val (c',gvars) = fresh c
val (in_group, not_in_group) = mk_group (#1 (dest_Const c')) rows
val in_group' =
if (null in_group) (* Constructor not given *)
then [((prfx, #2(fresh c)), (USyntax.ARB res_ty, (~1,false)))]
else in_group
in
part{constrs = crst,
rows = not_in_group,
A = {constructor = c',
new_formals = gvars,
group = in_group'}::A}
end
in part{constrs=constructors, rows=rows, A=[]}
end;
(*---------------------------------------------------------------------------
* Misc. routines used in mk_case
*---------------------------------------------------------------------------*)
fun mk_pat (c,l) =
let val L = length (binder_types (type_of c))
fun build (prfx,tag,plist) =
let val (args, plist') = chop L plist
in (prfx,tag,list_comb(c,args)::plist') end
in map build l end;
fun v_to_prfx (prfx, v::pats) = (v::prfx,pats)
| v_to_prfx _ = raise TFL_ERR "mk_case" "v_to_prfx";
fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, v::pats)
| v_to_pats _ = raise TFL_ERR "mk_case" "v_to_pats";
(*----------------------------------------------------------------------------
* Translation of pattern terms into nested case expressions.
*
* This performs the translation and also builds the full set of patterns.
* Thus it supports the construction of induction theorems even when an
* incomplete set of patterns is given.
*---------------------------------------------------------------------------*)
fun mk_case ty_info ty_match usednames range_ty =
let
fun mk_case_fail s = raise TFL_ERR "mk_case" s
val fresh_var = gvvariant usednames
val divide = partition fresh_var ty_match
fun expand _ ty ((_,[]), _) = mk_case_fail"expand_var_row"
| expand constructors ty (row as ((prfx, p::rst), rhs)) =
if (is_Free p)
then let val fresh = fresh_constr ty_match ty fresh_var
fun expnd (c,gvs) =
let val capp = list_comb(c,gvs)
in ((prfx, capp::rst), pattern_subst[(p,capp)] rhs)
end
in map expnd (map fresh constructors) end
else [row]
fun mk{rows=[],...} = mk_case_fail"no rows"
| mk{path=[], rows = ((prfx, []), (tm,tag))::_} = (* Done *)
([(prfx,tag,[])], tm)
| mk{path=[], rows = _::_} = mk_case_fail"blunder"
| mk{path as u::rstp, rows as ((prfx, []), rhs)::rst} =
mk{path = path,
rows = ((prfx, [fresh_var(type_of u)]), rhs)::rst}
| mk{path = u::rstp, rows as ((_, p::_), _)::_} =
let val (pat_rectangle,rights) = ListPair.unzip rows
val col0 = map(hd o #2) pat_rectangle
in
if (forall is_Free col0)
then let val rights' = map (fn(v,e) => pattern_subst[(v,u)] e)
(ListPair.zip (col0, rights))
val pat_rectangle' = map v_to_prfx pat_rectangle
val (pref_patl,tm) = mk{path = rstp,
rows = ListPair.zip (pat_rectangle',
rights')}
in (map v_to_pats pref_patl, tm)
end
else
let val pty as Type (ty_name,_) = type_of p
in
case (ty_info ty_name)
of NONE => mk_case_fail("Not a known datatype: "^ty_name)
| SOME{case_const,constructors} =>
let
val case_const_name = #1(dest_Const case_const)
val nrows = maps (expand constructors pty) rows
val subproblems = divide(constructors, pty, range_ty, nrows)
val groups = map #group subproblems
and new_formals = map #new_formals subproblems
and constructors' = map #constructor subproblems
val news = map (fn (nf,rows) => {path = nf@rstp, rows=rows})
(ListPair.zip (new_formals, groups))
val rec_calls = map mk news
val (pat_rect,dtrees) = ListPair.unzip rec_calls
val case_functions = map USyntax.list_mk_abs
(ListPair.zip (new_formals, dtrees))
val types = map type_of (case_functions@[u]) @ [range_ty]
val case_const' = Const(case_const_name, list_mk_type types)
val tree = list_comb(case_const', case_functions@[u])
val pat_rect1 = flat (ListPair.map mk_pat (constructors', pat_rect))
in (pat_rect1,tree)
end
end end
in mk
end;
(* Repeated variable occurrences in a pattern are not allowed. *)
fun FV_multiset tm =
case (USyntax.dest_term tm)
of USyntax.VAR{Name = c, Ty = T} => [Free(c, T)]
| USyntax.CONST _ => []
| USyntax.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand
| USyntax.LAMB _ => raise TFL_ERR "FV_multiset" "lambda";
fun no_repeat_vars thy pat =
let fun check [] = true
| check (v::rst) =
if member (op aconv) rst v then
raise TFL_ERR "no_repeat_vars"
(quote (#1 (dest_Free v)) ^
" occurs repeatedly in the pattern " ^
quote (Syntax.string_of_term_global thy pat))
else check rst
in check (FV_multiset pat)
end;
fun dest_atom (Free p) = p
| dest_atom (Const p) = p
| dest_atom _ = raise TFL_ERR "dest_atom" "function name not an identifier";
fun same_name (p,q) = #1(dest_atom p) = #1(dest_atom q);
local fun mk_functional_err s = raise TFL_ERR "mk_functional" s
fun single [_$_] =
mk_functional_err "recdef does not allow currying"
| single [f] = f
| single fs =
(*multiple function names?*)
if length (distinct same_name fs) < length fs
then mk_functional_err
"The function being declared appears with multiple types"
else mk_functional_err
(string_of_int (length fs) ^
" distinct function names being declared")
in
fun mk_functional thy clauses =
let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses
handle TERM _ => raise TFL_ERR "mk_functional"
"recursion equations must use the = relation")
val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
val atom = single (distinct (op aconv) funcs)
val (fname,ftype) = dest_atom atom
val _ = map (no_repeat_vars thy) pats
val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
map_index (fn (i, t) => (t,(i,true))) R)
val names = List.foldr Misc_Legacy.add_term_names [] R
val atype = type_of(hd pats)
and aname = singleton (Name.variant_list names) "a"
val a = Free(aname,atype)
val ty_info = Thry.match_info thy
val ty_match = Thry.match_type thy
val range_ty = type_of (hd R)
val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty
{path=[a], rows=rows}
val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts
handle Match => mk_functional_err "error in pattern-match translation"
val patts2 = Library.sort (Library.int_ord o apply2 row_of_pat) patts1
val finals = map row_of_pat patts2
val originals = map (row_of_pat o #2) rows
val _ = case (subtract (op =) finals originals)
of [] => ()
| L => mk_functional_err
("The following clauses are redundant (covered by preceding clauses): " ^
commas (map (fn i => string_of_int (i + 1)) L))
in {functional = Abs(Long_Name.base_name fname, ftype,
abstract_over (atom, absfree (aname,atype) case_tm)),
pats = patts2}
end end;
(*----------------------------------------------------------------------------
*
* PRINCIPLES OF DEFINITION
*
*---------------------------------------------------------------------------*)
(*For Isabelle, the lhs of a definition must be a constant.*)
fun const_def sign (c, Ty, rhs) =
singleton (Syntax.check_terms (Proof_Context.init_global sign))
(Const(@{const_name Pure.eq},dummyT) $ Const(c,Ty) $ rhs);
(*Make all TVars available for instantiation by adding a ? to the front*)
fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)
| poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
| poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
local
val f_eq_wfrec_R_M =
#ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl @{thm tfl_wfrec}))))
val {lhs=f, rhs} = USyntax.dest_eq f_eq_wfrec_R_M
val _ = dest_Free f
val (wfrec,_) = USyntax.strip_comb rhs
in
fun wfrec_definition0 fid R (functional as Abs(x, Ty, _)) thy =
let
val def_name = Thm.def_name (Long_Name.base_name fid)
val wfrec_R_M = map_types poly_tvars (wfrec $ map_types poly_tvars R) $ functional
val def_term = const_def thy (fid, Ty, wfrec_R_M)
val ([def], thy') =
Global_Theory.add_defs false [Thm.no_attributes (Binding.name def_name, def_term)] thy
in (def, thy') end;
end;
(*---------------------------------------------------------------------------
* This structure keeps track of congruence rules that aren't derived
* from a datatype definition.
*---------------------------------------------------------------------------*)
fun extraction_thms thy =
let val {case_rewrites,case_congs} = Thry.extract_info thy
in (case_rewrites, case_congs)
end;
(*---------------------------------------------------------------------------
* Pair patterns with termination conditions. The full list of patterns for
* a definition is merged with the TCs arising from the user-given clauses.
* There can be fewer clauses than the full list, if the user omitted some
* cases. This routine is used to prepare input for mk_induction.
*---------------------------------------------------------------------------*)
fun merge full_pats TCs =
let fun insert (p,TCs) =
let fun insrt ((x as (h,[]))::rst) =
if (p aconv h) then (p,TCs)::rst else x::insrt rst
| insrt (x::rst) = x::insrt rst
| insrt[] = raise TFL_ERR "merge.insert" "pattern not found"
in insrt end
fun pass ([],ptcl_final) = ptcl_final
| pass (ptcs::tcl, ptcl) = pass(tcl, insert ptcs ptcl)
in
pass (TCs, map (fn p => (p,[])) full_pats)
end;
fun givens pats = map pat_of (filter given pats);
fun post_definition ctxt meta_tflCongs (def, pats) =
let val thy = Proof_Context.theory_of ctxt
val tych = Thry.typecheck thy
val f = #lhs(USyntax.dest_eq(concl def))
val corollary = Rules.MATCH_MP @{thm tfl_wfrec} def
val pats' = filter given pats
val given_pats = map pat_of pats'
val rows = map row_of_pat pats'
val WFR = #ant(USyntax.dest_imp(concl corollary))
val R = #Rand(USyntax.dest_comb WFR)
val corollary' = Rules.UNDISCH corollary (* put WF R on assums *)
val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats
val (case_rewrites,context_congs) = extraction_thms thy
(*case_ss causes minimal simplification: bodies of case expressions are
not simplified. Otherwise large examples (Red-Black trees) are too
slow.*)
val case_simpset =
put_simpset HOL_basic_ss ctxt
addsimps case_rewrites
|> fold (Simplifier.add_cong o #case_cong_weak o snd)
(Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting]))
val corollaries' = map (Simplifier.simplify case_simpset) corollaries
val extract =
Rules.CONTEXT_REWRITE_RULE ctxt (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
val (rules, TCs) = ListPair.unzip (map extract corollaries')
val rules0 = map (rewrite_rule ctxt @{thms tfl_cut_def}) rules
val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
val rules1 = Rules.LIST_CONJ(map mk_cond_rule rules0)
in
{rules = rules1,
rows = rows,
full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)),
TCs = TCs}
end;
(*----------------------------------------------------------------------------
*
* INDUCTION THEOREM
*
*---------------------------------------------------------------------------*)
(*------------------------ Miscellaneous function --------------------------
*
* [x_1,...,x_n] ?v_1...v_n. M[v_1,...,v_n]
* -----------------------------------------------------------
* ( M[x_1,...,x_n], [(x_i,?v_1...v_n. M[v_1,...,v_n]),
* ...
* (x_j,?v_n. M[x_1,...,x_(n-1),v_n])] )
*
* This function is totally ad hoc. Used in the production of the induction
* theorem. The nchotomy theorem can have clauses that look like
*
* ?v1..vn. z = C vn..v1
*
* in which the order of quantification is not the order of occurrence of the
* quantified variables as arguments to C. Since we have no control over this
* aspect of the nchotomy theorem, we make the correspondence explicit by
* pairing the incoming new variable with the term it gets beta-reduced into.
*---------------------------------------------------------------------------*)
fun alpha_ex_unroll (xlist, tm) =
let val (qvars,body) = USyntax.strip_exists tm
val vlist = #2 (USyntax.strip_comb (USyntax.rhs body))
val plist = ListPair.zip (vlist, xlist)
val args = map (the o AList.lookup (op aconv) plist) qvars
handle Option.Option => raise Fail "TFL.alpha_ex_unroll: no correspondence"
fun build ex [] = []
| build (_$rex) (v::rst) =
let val ex1 = Term.betapply(rex, v)
in ex1 :: build ex1 rst
end
val (nex::exl) = rev (tm::build tm args)
in
(nex, ListPair.zip (args, rev exl))
end;
(*----------------------------------------------------------------------------
*
* PROVING COMPLETENESS OF PATTERNS
*
*---------------------------------------------------------------------------*)
fun mk_case ctxt ty_info usednames =
let
val thy = Proof_Context.theory_of ctxt
val divide = ipartition (gvvariant usednames)
val tych = Thry.typecheck thy
fun tych_binding(x,y) = (tych x, tych y)
fun fail s = raise TFL_ERR "mk_case" s
fun mk{rows=[],...} = fail"no rows"
| mk{path=[], rows = [([], (thm, bindings))]} =
Rules.IT_EXISTS ctxt (map tych_binding bindings) thm
| mk{path = u::rstp, rows as (p::_, _)::_} =
let val (pat_rectangle,rights) = ListPair.unzip rows
val col0 = map hd pat_rectangle
val pat_rectangle' = map tl pat_rectangle
in
if (forall is_Free col0) (* column 0 is all variables *)
then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[(u,v)]))
(ListPair.zip (rights, col0))
in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')}
end
else (* column 0 is all constructors *)
let val Type (ty_name,_) = type_of p
in
case (ty_info ty_name)
of NONE => fail("Not a known datatype: "^ty_name)
| SOME{constructors,nchotomy} =>
let val thm' = Rules.ISPEC (tych u) nchotomy
val disjuncts = USyntax.strip_disj (concl thm')
val subproblems = divide(constructors, rows)
val groups = map #group subproblems
and new_formals = map #new_formals subproblems
val existentials = ListPair.map alpha_ex_unroll
(new_formals, disjuncts)
val constraints = map #1 existentials
val vexl = map #2 existentials
fun expnd tm (pats,(th,b)) = (pats, (Rules.SUBS ctxt [Rules.ASSUME (tych tm)] th, b))
val news = map (fn (nf,rows,c) => {path = nf@rstp,
rows = map (expnd c) rows})
(Utils.zip3 new_formals groups constraints)
val recursive_thms = map mk news
val build_exists = Library.foldr
(fn((x,t), th) =>
Rules.CHOOSE ctxt (tych x, Rules.ASSUME (tych t)) th)
val thms' = ListPair.map build_exists (vexl, recursive_thms)
val same_concls = Rules.EVEN_ORS thms'
in Rules.DISJ_CASESL thm' same_concls
end
end end
in mk
end;
fun complete_cases ctxt =
let val thy = Proof_Context.theory_of ctxt
val tych = Thry.typecheck thy
val ty_info = Thry.induct_info thy
in fn pats =>
let val names = List.foldr Misc_Legacy.add_term_names [] pats
val T = type_of (hd pats)
val aname = singleton (Name.variant_list names) "a"
val vname = singleton (Name.variant_list (aname::names)) "v"
val a = Free (aname, T)
val v = Free (vname, T)
val a_eq_v = HOLogic.mk_eq(a,v)
val ex_th0 = Rules.EXISTS (tych (USyntax.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
(Rules.REFL (tych a))
val th0 = Rules.ASSUME (tych a_eq_v)
val rows = map (fn x => ([x], (th0,[]))) pats
in
Rules.GEN ctxt (tych a)
(Rules.RIGHT_ASSOC ctxt
(Rules.CHOOSE ctxt (tych v, ex_th0)
(mk_case ctxt ty_info (vname::aname::names)
{path=[v], rows=rows})))
end end;
(*---------------------------------------------------------------------------
* Constructing induction hypotheses: one for each recursive call.
*
* Note. R will never occur as a variable in the ind_clause, because
* to do so, it would have to be from a nested definition, and we don't
* allow nested defns to have R variable.
*
* Note. When the context is empty, there can be no local variables.
*---------------------------------------------------------------------------*)
local infix 5 ==>
fun (tm1 ==> tm2) = USyntax.mk_imp{ant = tm1, conseq = tm2}
in
fun build_ih f (P,SV) (pat,TCs) =
let val pat_vars = USyntax.free_vars_lr pat
val globals = pat_vars@SV
fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
fun dest_TC tm =
let val (cntxt,R_y_pat) = USyntax.strip_imp(#2(USyntax.strip_forall tm))
val (R,y,_) = USyntax.dest_relation R_y_pat
val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
in case cntxt
of [] => (P_y, (tm,[]))
| _ => let
val imp = USyntax.list_mk_conj cntxt ==> P_y
val lvs = subtract (op aconv) globals (USyntax.free_vars_lr imp)
val locals = #2(Utils.pluck (curry (op aconv) P) lvs) handle Utils.ERR _ => lvs
in (USyntax.list_mk_forall(locals,imp), (tm,locals)) end
end
in case TCs
of [] => (USyntax.list_mk_forall(pat_vars, P$pat), [])
| _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
val ind_clause = USyntax.list_mk_conj ihs ==> P$pat
in (USyntax.list_mk_forall(pat_vars,ind_clause), TCs_locals)
end
end
end;
(*---------------------------------------------------------------------------
* This function makes good on the promise made in "build_ih".
*
* Input is tm = "(!y. R y pat ==> P y) ==> P pat",
* TCs = TC_1[pat] ... TC_n[pat]
* thm = ih1 /\ ... /\ ih_n |- ih[pat]
*---------------------------------------------------------------------------*)
fun prove_case ctxt f (tm,TCs_locals,thm) =
let val tych = Thry.typecheck (Proof_Context.theory_of ctxt)
val antc = tych(#ant(USyntax.dest_imp tm))
val thm' = Rules.SPEC_ALL thm
fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
fun get_cntxt TC = tych(#ant(USyntax.dest_imp(#2(USyntax.strip_forall(concl TC)))))
fun mk_ih ((TC,locals),th2,nested) =
Rules.GENL ctxt (map tych locals)
(if nested then Rules.DISCH (get_cntxt TC) th2 handle Utils.ERR _ => th2
else if USyntax.is_imp (concl TC) then Rules.IMP_TRANS TC th2
else Rules.MP th2 TC)
in
Rules.DISCH antc
(if USyntax.is_imp(concl thm') (* recursive calls in this clause *)
then let val th1 = Rules.ASSUME antc
val TCs = map #1 TCs_locals
val ylist = map (#2 o USyntax.dest_relation o #2 o USyntax.strip_imp o
#2 o USyntax.strip_forall) TCs
val TClist = map (fn(TC,lvs) => (Rules.SPEC_ALL(Rules.ASSUME(tych TC)),lvs))
TCs_locals
val th2list = map (fn t => Rules.SPEC (tych t) th1) ylist
val nlist = map nested TCs
val triples = Utils.zip3 TClist th2list nlist
val Pylist = map mk_ih triples
in Rules.MP thm' (Rules.LIST_CONJ Pylist) end
else thm')
end;
(*---------------------------------------------------------------------------
*
* x = (v1,...,vn) |- M[x]
* ---------------------------------------------
* ?v1 ... vn. x = (v1,...,vn) |- M[x]
*
*---------------------------------------------------------------------------*)
fun LEFT_ABS_VSTRUCT ctxt tych thm =
let fun CHOOSER v (tm,thm) =
let val ex_tm = USyntax.mk_exists{Bvar=v,Body=tm}
in (ex_tm, Rules.CHOOSE ctxt (tych v, Rules.ASSUME (tych ex_tm)) thm)
end
val [veq] = filter (can USyntax.dest_eq) (#1 (Rules.dest_thm thm))
val {lhs,rhs} = USyntax.dest_eq veq
val L = USyntax.free_vars_lr rhs
in #2 (fold_rev CHOOSER L (veq,thm)) end;
(*----------------------------------------------------------------------------
* Input : f, R, and [(pat1,TCs1),..., (patn,TCsn)]
*
* Instantiates tfl_wf_induct, getting Sinduct and then tries to prove
* recursion induction (Rinduct) by proving the antecedent of Sinduct from
* the antecedent of Rinduct.
*---------------------------------------------------------------------------*)
fun mk_induction ctxt {fconst, R, SV, pat_TCs_list} =
let
val thy = Proof_Context.theory_of ctxt
val tych = Thry.typecheck thy
val Sinduction = Rules.UNDISCH (Rules.ISPEC (tych R) @{thm tfl_wf_induct})
val (pats,TCsl) = ListPair.unzip pat_TCs_list
val case_thm = complete_cases ctxt pats
val domain = (type_of o hd) pats
val Pname = singleton (Name.variant_list (List.foldr (Library.foldr Misc_Legacy.add_term_names)
[] (pats::TCsl))) "P"
val P = Free(Pname, domain --> HOLogic.boolT)
val Sinduct = Rules.SPEC (tych P) Sinduction
val Sinduct_assumf = USyntax.rand ((#ant o USyntax.dest_imp o concl) Sinduct)
val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list
val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
val Rinduct_assum = Rules.ASSUME (tych (USyntax.list_mk_conj Rassums))
val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum)
val proved_cases = map (prove_case ctxt fconst) tasks
val v =
Free (singleton
(Name.variant_list (List.foldr Misc_Legacy.add_term_names [] (map concl proved_cases))) "v",
domain)
val vtyped = tych v
val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS ctxt [th]th')
(substs, proved_cases)
val abs_cases = map (LEFT_ABS_VSTRUCT ctxt tych) proved_cases1
val dant = Rules.GEN ctxt vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
val dc = Rules.MP Sinduct dant
val Parg_ty = type_of(#Bvar(USyntax.dest_forall(concl dc)))
val vars = map (gvvariant[Pname]) (USyntax.strip_prod_type Parg_ty)
val dc' = fold_rev (Rules.GEN ctxt o tych) vars
(Rules.SPEC (tych(USyntax.mk_vstruct Parg_ty vars)) dc)
in
Rules.GEN ctxt (tych P) (Rules.DISCH (tych(concl Rinduct_assum)) dc')
end
handle Utils.ERR _ => raise TFL_ERR "mk_induction" "failed derivation";
(*---------------------------------------------------------------------------
*
* POST PROCESSING
*
*---------------------------------------------------------------------------*)
fun simplify_induction thy hth ind =
let val tych = Thry.typecheck thy
val (asl,_) = Rules.dest_thm ind
val (_,tc_eq_tc') = Rules.dest_thm hth
val tc = USyntax.lhs tc_eq_tc'
fun loop [] = ind
| loop (asm::rst) =
if (can (Thry.match_term thy asm) tc)
then Rules.UNDISCH
(Rules.MATCH_MP
(Rules.MATCH_MP @{thm tfl_simp_thm} (Rules.DISCH (tych asm) ind))
hth)
else loop rst
in loop asl
end;
(*---------------------------------------------------------------------------
* The termination condition is an antecedent to the rule, and an
* assumption to the theorem.
*---------------------------------------------------------------------------*)
fun elim_tc tcthm (rule,induction) =
(Rules.MP rule tcthm, Rules.PROVE_HYP tcthm induction)
fun trace_thms ctxt s L =
if !trace then writeln (cat_lines (s :: map (Display.string_of_thm ctxt) L))
else ();
fun trace_cterm ctxt s ct =
if !trace then
writeln (cat_lines [s, Syntax.string_of_term ctxt (Thm.term_of ct)])
else ();
fun postprocess ctxt strict {wf_tac, terminator, simplifier} {rules,induction,TCs} =
let
val thy = Proof_Context.theory_of ctxt;
val tych = Thry.typecheck thy;
(*---------------------------------------------------------------------
* Attempt to eliminate WF condition. It's the only assumption of rules
*---------------------------------------------------------------------*)
val (rules1,induction1) =
let val thm =
Rules.prove ctxt strict (HOLogic.mk_Trueprop (hd(#1(Rules.dest_thm rules))), wf_tac)
in (Rules.PROVE_HYP thm rules, Rules.PROVE_HYP thm induction)
end handle Utils.ERR _ => (rules,induction);
(*----------------------------------------------------------------------
* The termination condition (tc) is simplified to |- tc = tc' (there
* might not be a change!) and then 3 attempts are made:
*
* 1. if |- tc = T, then eliminate it with tfl_eq_True; otherwise,
* 2. apply the terminator to tc'. If |- tc' = T then eliminate; else
* 3. replace tc by tc' in both the rules and the induction theorem.
*---------------------------------------------------------------------*)
fun simplify_tc tc (r,ind) =
let val tc1 = tych tc
val _ = trace_cterm ctxt "TC before simplification: " tc1
val tc_eq = simplifier tc1
val _ = trace_thms ctxt "result: " [tc_eq]
in
elim_tc (Rules.MATCH_MP @{thm tfl_eq_True} tc_eq) (r,ind)
handle Utils.ERR _ =>
(elim_tc (Rules.MATCH_MP(Rules.MATCH_MP @{thm tfl_rev_eq_mp} tc_eq)
(Rules.prove ctxt strict (HOLogic.mk_Trueprop(USyntax.rhs(concl tc_eq)),
terminator)))
(r,ind)
handle Utils.ERR _ =>
(Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP @{thm tfl_simp_thm} r) tc_eq),
simplify_induction thy tc_eq ind))
end
(*----------------------------------------------------------------------
* Nested termination conditions are harder to get at, since they are
* left embedded in the body of the function (and in induction
* theorem hypotheses). Our "solution" is to simplify them, and try to
* prove termination, but leave the application of the resulting theorem
* to a higher level. So things go much as in "simplify_tc": the
* termination condition (tc) is simplified to |- tc = tc' (there might
* not be a change) and then 2 attempts are made:
*
* 1. if |- tc = T, then return |- tc; otherwise,
* 2. apply the terminator to tc'. If |- tc' = T then return |- tc; else
* 3. return |- tc = tc'
*---------------------------------------------------------------------*)
fun simplify_nested_tc tc =
let val tc_eq = simplifier (tych (#2 (USyntax.strip_forall tc)))
in
Rules.GEN_ALL ctxt
(Rules.MATCH_MP @{thm tfl_eq_True} tc_eq
handle Utils.ERR _ =>
(Rules.MATCH_MP(Rules.MATCH_MP @{thm tfl_rev_eq_mp} tc_eq)
(Rules.prove ctxt strict (HOLogic.mk_Trueprop (USyntax.rhs(concl tc_eq)),
terminator))
handle Utils.ERR _ => tc_eq))
end
(*-------------------------------------------------------------------
* Attempt to simplify the termination conditions in each rule and
* in the induction theorem.
*-------------------------------------------------------------------*)
fun strip_imp tm = if USyntax.is_neg tm then ([],tm) else USyntax.strip_imp tm
fun loop ([],extras,R,ind) = (rev R, ind, extras)
| loop ((r,ftcs)::rst, nthms, R, ind) =
let val tcs = #1(strip_imp (concl r))
val extra_tcs = subtract (op aconv) tcs ftcs
val extra_tc_thms = map simplify_nested_tc extra_tcs
val (r1,ind1) = fold simplify_tc tcs (r,ind)
val r2 = Rules.FILTER_DISCH_ALL(not o USyntax.is_WFR) r1
in loop(rst, nthms@extra_tc_thms, r2::R, ind1)
end
val rules_tcs = ListPair.zip (Rules.CONJUNCTS rules1, TCs)
val (rules2,ind2,extras) = loop(rules_tcs,[],[],induction1)
in
{induction = ind2, rules = Rules.LIST_CONJ rules2, nested_tcs = extras}
end;
end;
(*** second part of main module (postprocessing of TFL definitions) ***)
structure Tfl: TFL =
struct
(* misc *)
(*---------------------------------------------------------------------------
* Extract termination goals so that they can be put it into a goalstack, or
* have a tactic directly applied to them.
*--------------------------------------------------------------------------*)
fun termination_goals rules =
map (Type.legacy_freeze o HOLogic.dest_Trueprop)
(fold_rev (union (op aconv) o Thm.prems_of) rules []);
(*---------------------------------------------------------------------------
* Three postprocessors are applied to the definition. It
* attempts to prove wellfoundedness of the given relation, simplifies the
* non-proved termination conditions, and finally attempts to prove the
* simplified termination conditions.
*--------------------------------------------------------------------------*)
fun std_postprocessor ctxt strict wfs =
Prim.postprocess ctxt strict
{wf_tac = REPEAT (ares_tac wfs 1),
terminator =
asm_simp_tac ctxt 1
THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE
fast_force_tac (ctxt addSDs @{thms not0_implies_Suc}) 1),
simplifier = Rules.simpl_conv ctxt []};
val concl = #2 o Rules.dest_thm;
(*---------------------------------------------------------------------------
* Postprocess a definition made by "define". This is a separate stage of
* processing from the definition stage.
*---------------------------------------------------------------------------*)
local
(* The rest of these local definitions are for the tricky nested case *)
val solved = not o can USyntax.dest_eq o #2 o USyntax.strip_forall o concl
fun id_thm th =
let val {lhs,rhs} = USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (Rules.dest_thm th))));
in lhs aconv rhs end
handle Utils.ERR _ => false;
val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
fun mk_meta_eq r =
(case Thm.concl_of r of
Const(@{const_name Pure.eq},_)$_$_ => r
| _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection
| _ => r RS P_imp_P_eq_True)
(*Is this the best way to invoke the simplifier??*)
fun rewrite ctxt L = rewrite_rule ctxt (map mk_meta_eq (filter_out id_thm L))
fun join_assums ctxt th =
let val tych = Thm.cterm_of ctxt
val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th)))
val cntxtl = (#1 o USyntax.strip_imp) lhs (* cntxtl should = cntxtr *)
val cntxtr = (#1 o USyntax.strip_imp) rhs (* but union is solider *)
val cntxt = union (op aconv) cntxtl cntxtr
in
Rules.GEN_ALL ctxt
(Rules.DISCH_ALL
(rewrite ctxt (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
end
val gen_all = USyntax.gen_all
in
fun proof_stage ctxt strict wfs {f, R, rules, full_pats_TCs, TCs} =
let
val _ = writeln "Proving induction theorem ..."
val ind =
Prim.mk_induction ctxt
{fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
val _ = writeln "Postprocessing ...";
val {rules, induction, nested_tcs} =
std_postprocessor ctxt strict wfs {rules=rules, induction=ind, TCs=TCs}
in
case nested_tcs
of [] => {induction=induction, rules=rules,tcs=[]}
| L => let val _ = writeln "Simplifying nested TCs ..."
val (solved,simplified,stubborn) =
fold_rev (fn th => fn (So,Si,St) =>
if (id_thm th) then (So, Si, th::St) else
if (solved th) then (th::So, Si, St)
else (So, th::Si, St)) nested_tcs ([],[],[])
val simplified' = map (join_assums ctxt) simplified
val dummy = (Prim.trace_thms ctxt "solved =" solved;
Prim.trace_thms ctxt "simplified' =" simplified')
val rewr = full_simplify (ctxt addsimps (solved @ simplified'));
val dummy = Prim.trace_thms ctxt "Simplifying the induction rule..." [induction]
val induction' = rewr induction
val dummy = Prim.trace_thms ctxt "Simplifying the recursion rules..." [rules]
val rules' = rewr rules
val _ = writeln "... Postprocessing finished";
in
{induction = induction',
rules = rules',
tcs = map (gen_all o USyntax.rhs o #2 o USyntax.strip_forall o concl)
(simplified@stubborn)}
end
end;
(*lcp: curry the predicate of the induction rule*)
fun curry_rule ctxt rl =
Split_Rule.split_rule_var ctxt (Term.head_of (HOLogic.dest_Trueprop (Thm.concl_of rl))) rl;
(*lcp: put a theorem into Isabelle form, using meta-level connectives*)
fun meta_outer ctxt =
curry_rule ctxt o Drule.export_without_context o
rule_by_tactic ctxt
(REPEAT (FIRSTGOAL (resolve_tac ctxt [allI, impI, conjI] ORELSE' eresolve_tac ctxt [conjE])));
(*Strip off the outer !P*)
val spec'=
Rule_Insts.read_instantiate @{context} [((("x", 0), Position.none), "P::'b=>bool")] [] spec;
fun simplify_defn ctxt strict congs wfs pats def0 =
let
val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
val {rules, rows, TCs, full_pats_TCs} = Prim.post_definition ctxt congs (def, pats)
val {lhs=f,rhs} = USyntax.dest_eq (concl def)
val (_,[R,_]) = USyntax.strip_comb rhs
val _ = Prim.trace_thms ctxt "congs =" congs
(*the next step has caused simplifier looping in some cases*)
val {induction, rules, tcs} =
proof_stage ctxt strict wfs
{f = f, R = R, rules = rules,
full_pats_TCs = full_pats_TCs,
TCs = TCs}
val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
(Rules.CONJUNCTS rules)
in
{induct = meta_outer ctxt (Object_Logic.rulify_no_asm ctxt (induction RS spec')),
rules = ListPair.zip(rules', rows),
tcs = (termination_goals rules') @ tcs}
end
handle Utils.ERR {mesg,func,module} =>
error (mesg ^ "\n (In TFL function " ^ module ^ "." ^ func ^ ")");
(* Derive the initial equations from the case-split rules to meet the
users specification of the recursive function. *)
local
fun get_related_thms i =
map_filter ((fn (r,x) => if x = i then SOME r else NONE));
fun solve_eq _ (_, [], _) = error "derive_init_eqs: missing rules"
| solve_eq _ (_, [a], i) = [(a, i)]
| solve_eq ctxt (th, splitths, i) =
(writeln "Proving unsplit equation...";
[((Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
(CaseSplit.splitto ctxt splitths th), i)])
handle ERROR s =>
(warning ("recdef (solve_eq): " ^ s); map (fn x => (x,i)) splitths);
in
fun derive_init_eqs ctxt rules eqs =
map (Thm.trivial o Thm.cterm_of ctxt o HOLogic.mk_Trueprop) eqs
|> map_index (fn (i, e) => solve_eq ctxt (e, (get_related_thms i rules), i))
|> flat;
end;
(*---------------------------------------------------------------------------
* Defining a function with an associated termination relation.
*---------------------------------------------------------------------------*)
fun define_i strict congs wfs fid R eqs ctxt =
let
val thy = Proof_Context.theory_of ctxt
val {functional, pats} = Prim.mk_functional thy eqs
val (def, thy') = Prim.wfrec_definition0 fid R functional thy
val ctxt' = Proof_Context.transfer thy' ctxt
val (lhs, _) = Logic.dest_equals (Thm.prop_of def)
val {induct, rules, tcs} = simplify_defn ctxt' strict congs wfs pats def
val rules' = if strict then derive_init_eqs ctxt' rules eqs else rules
in ({lhs = lhs, rules = rules', induct = induct, tcs = tcs}, ctxt') end;
fun define strict congs wfs fid R seqs ctxt =
define_i strict congs wfs fid
(Syntax.read_term ctxt R) (map (Syntax.read_term ctxt) seqs) ctxt
handle Utils.ERR {mesg,...} => error mesg;
end;
end;
(*** wrappers for Isar ***)
(** recdef hints **)
(* type hints *)
type hints = {simps: thm list, congs: (string * thm) list, wfs: thm list};
fun mk_hints (simps, congs, wfs) = {simps = simps, congs = congs, wfs = wfs}: hints;
fun map_hints f ({simps, congs, wfs}: hints) = mk_hints (f (simps, congs, wfs));
fun map_simps f = map_hints (fn (simps, congs, wfs) => (f simps, congs, wfs));
fun map_congs f = map_hints (fn (simps, congs, wfs) => (simps, f congs, wfs));
fun map_wfs f = map_hints (fn (simps, congs, wfs) => (simps, congs, f wfs));
(* congruence rules *)
local
val cong_head =
fst o Term.dest_Const o Term.head_of o fst o Logic.dest_equals o Thm.concl_of;
fun prep_cong raw_thm =
let val thm = safe_mk_meta_eq raw_thm in (cong_head thm, thm) end;
in
fun add_cong raw_thm congs =
let
val (c, thm) = prep_cong raw_thm;
val _ = if AList.defined (op =) congs c
then warning ("Overwriting recdef congruence rule for " ^ quote c)
else ();
in AList.update (op =) (c, thm) congs end;
fun del_cong raw_thm congs =
let
val (c, _) = prep_cong raw_thm;
val _ = if AList.defined (op =) congs c
then ()
else warning ("No recdef congruence rule for " ^ quote c);
in AList.delete (op =) c congs end;
end;
(** global and local recdef data **)
(* theory data *)
type recdef_info = {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list};
structure Data = Generic_Data
(
type T = recdef_info Symtab.table * hints;
val empty = (Symtab.empty, mk_hints ([], [], [])): T;
val extend = I;
fun merge
((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
(tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
(Symtab.merge (K true) (tab1, tab2),
mk_hints (Thm.merge_thms (simps1, simps2),
AList.merge (op =) (K true) (congs1, congs2),
Thm.merge_thms (wfs1, wfs2)));
);
val get_recdef = Symtab.lookup o #1 o Data.get o Context.Theory;
fun put_recdef name info =
(Context.theory_map o Data.map o apfst) (fn tab =>
Symtab.update_new (name, info) tab
handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name));
val get_hints = #2 o Data.get o Context.Proof;
val map_hints = Data.map o apsnd;
(* attributes *)
fun attrib f = Thm.declaration_attribute (map_hints o f);
val simp_add = attrib (map_simps o Thm.add_thm);
val simp_del = attrib (map_simps o Thm.del_thm);
val cong_add = attrib (map_congs o add_cong);
val cong_del = attrib (map_congs o del_cong);
val wf_add = attrib (map_wfs o Thm.add_thm);
val wf_del = attrib (map_wfs o Thm.del_thm);
(* modifiers *)
val recdef_simpN = "recdef_simp";
val recdef_congN = "recdef_cong";
val recdef_wfN = "recdef_wf";
val recdef_modifiers =
[Args.$$$ recdef_simpN -- Args.colon >> K (Method.modifier simp_add @{here}),
Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
Args.$$$ recdef_congN -- Args.colon >> K (Method.modifier cong_add @{here}),
Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (Method.modifier cong_add @{here}),
Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (Method.modifier cong_del @{here}),
Args.$$$ recdef_wfN -- Args.colon >> K (Method.modifier wf_add @{here}),
Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (Method.modifier wf_add @{here}),
Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (Method.modifier wf_del @{here})] @
Clasimp.clasimp_modifiers;
(** prepare hints **)
fun prepare_hints opt_src ctxt =
let
val ctxt' =
(case opt_src of
NONE => ctxt
| SOME src => #2 (Token.syntax (Method.sections recdef_modifiers) src ctxt));
val {simps, congs, wfs} = get_hints ctxt';
val ctxt'' = ctxt' addsimps simps |> Simplifier.del_cong @{thm imp_cong};
in ((rev (map snd congs), wfs), ctxt'') end;
fun prepare_hints_i () ctxt =
let
val {simps, congs, wfs} = get_hints ctxt;
val ctxt' = ctxt addsimps simps |> Simplifier.del_cong @{thm imp_cong};
in ((rev (map snd congs), wfs), ctxt') end;
(** add_recdef(_i) **)
fun gen_add_recdef tfl_fn prep_att prep_hints not_permissive raw_name R eq_srcs hints thy =
let
val _ = legacy_feature "Old 'recdef' command -- use 'fun' or 'function' instead";
val name = Sign.intern_const thy raw_name;
val bname = Long_Name.base_name name;
val _ = writeln ("Defining recursive function " ^ quote name ^ " ...");
val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
val eq_atts = map (map (prep_att thy)) raw_eq_atts;
val ((congs, wfs), ctxt) = prep_hints hints (Proof_Context.init_global thy);
(*We must remove imp_cong to prevent looping when the induction rule
is simplified. Many induction rules have nested implications that would
give rise to looping conditional rewriting.*)
val ({lhs, rules = rules_idx, induct, tcs}, ctxt1) =
tfl_fn not_permissive congs wfs name R eqs ctxt;
val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
val simp_att =
if null tcs then [Simplifier.simp_add,
Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute]
else [];
val ((simps' :: rules', [induct']), thy2) =
Proof_Context.theory_of ctxt1
|> Sign.add_path bname
|> Global_Theory.add_thmss
(((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])]
||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules);
val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
val thy3 =
thy2
|> put_recdef name result
|> Sign.parent_path;
in (thy3, result) end;
val add_recdef = gen_add_recdef Tfl.define Attrib.attribute_cmd_global prepare_hints;
fun add_recdef_i x y z w = gen_add_recdef Tfl.define_i (K I) prepare_hints_i x y z w ();
(** package setup **)
(* setup theory *)
val _ =
Theory.setup
(Attrib.setup @{binding recdef_simp} (Attrib.add_del simp_add simp_del)
"declaration of recdef simp rule" #>
Attrib.setup @{binding recdef_cong} (Attrib.add_del cong_add cong_del)
"declaration of recdef cong rule" #>
Attrib.setup @{binding recdef_wf} (Attrib.add_del wf_add wf_del)
"declaration of recdef wf rule");
(* outer syntax *)
val hints =
@{keyword "("} |--
Parse.!!! (Parse.position @{keyword "hints"} -- Parse.args --| @{keyword ")"})
>> uncurry Token.src;
val recdef_decl =
Scan.optional
(@{keyword "("} -- Parse.!!! (@{keyword "permissive"} -- @{keyword ")"}) >> K false) true --
Parse.name -- Parse.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
-- Scan.option hints
>> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
val _ =
Outer_Syntax.command @{command_keyword recdef} "define general recursive functions (obsolete TFL)"
(recdef_decl >> Toplevel.theory);
end;