--- a/src/HOL/Tools/function_package/fundef_datatype.ML Sat Aug 05 14:52:58 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML Sat Aug 05 14:55:09 2006 +0200
@@ -2,11 +2,11 @@
ID: $Id$
Author: Alexander Krauss, TU Muenchen
-A package for general recursive function definitions.
+A package for general recursive function definitions.
A tactic to prove completeness of datatype patterns.
*)
-signature FUNDEF_DATATYPE =
+signature FUNDEF_DATATYPE =
sig
val pat_complete_tac: int -> tactic
@@ -28,52 +28,52 @@
fun inst_case_thm thy x P thm =
let
- val [Pv, xv] = term_vars (prop_of thm)
+ val [Pv, xv] = term_vars (prop_of thm)
in
- cterm_instantiate [(cterm_of thy xv, cterm_of thy x), (cterm_of thy Pv, cterm_of thy P)] thm
+ cterm_instantiate [(cterm_of thy xv, cterm_of thy x), (cterm_of thy Pv, cterm_of thy P)] thm
end
fun invent_vars constr i =
let
- val Ts = binder_types (fastype_of constr)
- val j = i + length Ts
- val is = i upto (j - 1)
- val avs = map2 mk_argvar is Ts
- val pvs = map2 mk_patvar is Ts
+ val Ts = binder_types (fastype_of constr)
+ val j = i + length Ts
+ val is = i upto (j - 1)
+ val avs = map2 mk_argvar is Ts
+ val pvs = map2 mk_patvar is Ts
in
- (avs, pvs, j)
+ (avs, pvs, j)
end
fun filter_pats thy cons pvars [] = []
| filter_pats thy cons pvars (([], thm) :: pts) = raise Match
- | filter_pats thy cons pvars ((pat :: pats, thm) :: pts) =
+ | filter_pats thy cons pvars ((pat :: pats, thm) :: pts) =
case pat of
- Free _ => let val inst = list_comb (cons, pvars)
- in (inst :: pats, inst_free (cterm_of thy pat) (cterm_of thy inst) thm)
- :: (filter_pats thy cons pvars pts) end
+ Free _ => let val inst = list_comb (cons, pvars)
+ in (inst :: pats, inst_free (cterm_of thy pat) (cterm_of thy inst) thm)
+ :: (filter_pats thy cons pvars pts) end
| _ => if fst (strip_comb pat) = cons
- then (pat :: pats, thm) :: (filter_pats thy cons pvars pts)
- else filter_pats thy cons pvars pts
+ then (pat :: pats, thm) :: (filter_pats thy cons pvars pts)
+ else filter_pats thy cons pvars pts
fun inst_constrs_of thy (T as Type (name, _)) =
- map (fn (Cn,CT) => Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy) (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
- (the (DatatypePackage.get_datatype_constrs thy name))
+ map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
+ (the (DatatypePackage.get_datatype_constrs thy name))
| inst_constrs_of thy _ = raise Match
fun transform_pat thy avars c_assum ([] , thm) = raise Match
| transform_pat thy avars c_assum (pat :: pats, thm) =
let
- val (_, subps) = strip_comb pat
- val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
- val a_eqs = map assume eqs
- val c_eq_pat = simplify (HOL_basic_ss addsimps a_eqs) c_assum
+ val (_, subps) = strip_comb pat
+ val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
+ val a_eqs = map assume eqs
+ val c_eq_pat = simplify (HOL_basic_ss addsimps a_eqs) c_assum
in
- (subps @ pats, fold_rev implies_intr eqs
- (implies_elim thm c_eq_pat))
+ (subps @ pats, fold_rev implies_intr eqs
+ (implies_elim thm c_eq_pat))
end
@@ -81,14 +81,14 @@
fun constr_case thy P idx (v :: vs) pats cons =
let
- val (avars, pvars, newidx) = invent_vars cons idx
- val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
- val c_assum = assume c_hyp
- val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats)
+ val (avars, pvars, newidx) = invent_vars cons idx
+ val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
+ val c_assum = assume c_hyp
+ val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats)
in
- o_alg thy P newidx (avars @ vs) newpats
- |> implies_intr c_hyp
- |> fold_rev (forall_intr o cterm_of thy) avars
+ o_alg thy P newidx (avars @ vs) newpats
+ |> implies_intr c_hyp
+ |> fold_rev (forall_intr o cterm_of thy) avars
end
| constr_case _ _ _ _ _ _ = raise Match
and o_alg thy P idx [] (([], Pthm) :: _) = Pthm
@@ -96,72 +96,72 @@
| o_alg thy P idx (v :: vs) pts =
if forall (is_Free o hd o fst) pts (* Var case *)
then o_alg thy P idx vs (map (fn (pv :: pats, thm) =>
- (pats, refl RS (inst_free (cterm_of thy pv) (cterm_of thy v) thm))) pts)
+ (pats, refl RS (inst_free (cterm_of thy pv) (cterm_of thy v) thm))) pts)
else (* Cons case *)
- let
- val T = fastype_of v
- val (tname, _) = dest_Type T
- val {exhaustion=case_thm, ...} = DatatypePackage.the_datatype thy tname
- val constrs = inst_constrs_of thy T
- val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
- in
- inst_case_thm thy v P case_thm
- |> fold (curry op COMP) c_cases
- end
+ let
+ val T = fastype_of v
+ val (tname, _) = dest_Type T
+ val {exhaustion=case_thm, ...} = DatatypePackage.the_datatype thy tname
+ val constrs = inst_constrs_of thy T
+ val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
+ in
+ inst_case_thm thy v P case_thm
+ |> fold (curry op COMP) c_cases
+ end
| o_alg _ _ _ _ _ = raise Match
-
+
fun prove_completeness thy x P qss pats =
let
- fun mk_assum qs pat = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x,pat)),
- HOLogic.mk_Trueprop P)
- |> fold_rev mk_forall qs
- |> cterm_of thy
+ fun mk_assum qs pat = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x,pat)),
+ HOLogic.mk_Trueprop P)
+ |> fold_rev mk_forall qs
+ |> cterm_of thy
- val hyps = map2 mk_assum qss pats
+ val hyps = map2 mk_assum qss pats
- fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp)
+ fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp)
- val assums = map2 inst_hyps hyps qss
+ val assums = map2 inst_hyps hyps qss
in
- o_alg thy P 2 [x] (map2 (pair o single) pats assums)
- |> fold_rev implies_intr hyps
+ o_alg thy P 2 [x] (map2 (pair o single) pats assums)
+ |> fold_rev implies_intr hyps
end
fun pat_complete_tac i thm =
- let
+ let
val thy = theory_of_thm thm
- val subgoal = nth (prems_of thm) (i - 1)
+ val subgoal = nth (prems_of thm) (i - 1) (* FIXME SUBGOAL tactical *)
val ([P, x], subgf) = dest_all_all subgoal
- val assums = Logic.strip_imp_prems subgf
-
- fun pat_of assum =
- let
- val (qs, imp) = dest_all_all assum
- in
- case Logic.dest_implies imp of
- (_ $ (_ $ _ $ pat), _) => (qs, pat)
- | _ => raise COMPLETENESS
- end
+ val assums = Logic.strip_imp_prems subgf
- val (qss, pats) = split_list (map pat_of assums)
+ fun pat_of assum =
+ let
+ val (qs, imp) = dest_all_all assum
+ in
+ case Logic.dest_implies imp of
+ (_ $ (_ $ _ $ pat), _) => (qs, pat)
+ | _ => raise COMPLETENESS
+ end
- val complete_thm = prove_completeness thy x P qss pats
+ val (qss, pats) = split_list (map pat_of assums)
+
+ val complete_thm = prove_completeness thy x P qss pats
|> forall_intr (cterm_of thy x)
|> forall_intr (cterm_of thy P)
in
- Seq.single (Drule.compose_single(complete_thm, i, thm))
+ Seq.single (Drule.compose_single(complete_thm, i, thm))
end
handle COMPLETENESS => Seq.empty
-val setup =
+val setup =
Method.add_methods [("pat_completeness", Method.no_args (Method.SIMPLE_METHOD (pat_complete_tac 1)), "Completeness prover for datatype patterns")]
-end
\ No newline at end of file
+end
--- a/src/HOL/Tools/function_package/pattern_split.ML Sat Aug 05 14:52:58 2006 +0200
+++ b/src/HOL/Tools/function_package/pattern_split.ML Sat Aug 05 14:55:09 2006 +0200
@@ -2,29 +2,29 @@
ID: $Id$
Author: Alexander Krauss, TU Muenchen
-A package for general recursive function definitions.
+A package for general recursive function definitions.
-Automatic splitting of overlapping constructor patterns. This is a preprocessing step which
+Automatic splitting of overlapping constructor patterns. This is a preprocessing step which
turns a specification with overlaps into an overlap-free specification.
*)
-signature FUNDEF_SPLIT =
+signature FUNDEF_SPLIT =
sig
val split_some_equations :
Proof.context -> (('a * ('b * bool)) * term) list -> (('a * 'b) * term list) list
end
-structure FundefSplit : FUNDEF_SPLIT =
+structure FundefSplit : FUNDEF_SPLIT =
struct
(* We use proof context for the variable management *)
(* FIXME: no __ *)
-fun new_var ctx vs T =
- let
+fun new_var ctx vs T =
+ let
val [v] = Variable.variant_frees ctx vs [("v", T)]
in
(Free v :: vs, Free v)
@@ -37,17 +37,17 @@
(* This is copied from "fundef_datatype.ML" *)
fun inst_constrs_of thy (T as Type (name, _)) =
- map (fn (Cn,CT) => Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy) (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
- (the (DatatypePackage.get_datatype_constrs thy name))
+ map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
+ (the (DatatypePackage.get_datatype_constrs thy name))
| inst_constrs_of thy t = (print t; sys_error "inst_constrs_of")
fun pattern_subtract_subst ctx vs _ (Free v2) = []
| pattern_subtract_subst ctx vs (v as (Free (_, T))) t' =
- let
- fun foo constr =
- let
+ let
+ fun foo constr =
+ let
val (vs', t) = saturate ctx vs constr
val substs = pattern_subtract_subst ctx vs' t t'
in
@@ -95,7 +95,7 @@
fun split_all_equations ctx eqns =
- let
+ let
fun split_aux prev [] = []
| split_aux prev (e::es) = pattern_subtract_many ctx prev [e] @ split_aux (e::prev) es
in
@@ -108,8 +108,8 @@
fun split_aux prev [] = []
| split_aux prev (((n, (att, true)), eq) :: es) = ((n, att), pattern_subtract_many ctx prev [eq])
:: split_aux (eq :: prev) es
- | split_aux prev (((n, (att, false)), eq) :: es) = ((n, att), [eq])
- :: split_aux (eq :: prev) es
+ | split_aux prev (((n, (att, false)), eq) :: es) = ((n, att), [eq])
+ :: split_aux (eq :: prev) es
in
split_aux [] eqns
end
--- a/src/HOL/Tools/specification_package.ML Sat Aug 05 14:52:58 2006 +0200
+++ b/src/HOL/Tools/specification_package.ML Sat Aug 05 14:55:09 2006 +0200
@@ -131,8 +131,7 @@
fun proc_single prop =
let
val frees = Term.term_frees prop
- val tsig = Sign.tsig_of (sign_of thy)
- val _ = assert (forall (fn v => Type.of_sort tsig (type_of v,HOLogic.typeS)) frees)
+ val _ = assert (forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees)
"Specificaton: Only free variables of sort 'type' allowed"
val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
in
--- a/src/Provers/ind.ML Sat Aug 05 14:52:58 2006 +0200
+++ b/src/Provers/ind.ML Sat Aug 05 14:55:09 2006 +0200
@@ -26,9 +26,9 @@
val _$(_$Var(a_ixname,aT)) = concl_of spec;
-fun add_term_frees tsig =
+fun add_term_frees thy =
let fun add(tm, vars) = case tm of
- Free(v,T) => if Type.typ_instance tsig (T,aT) then v ins vars
+ Free(v,T) => if Sign.typ_instance thy (T,aT) then v ins vars
else vars
| Abs (_,_,body) => add(body,vars)
| rator$rand => add(rator, add(rand, vars))
@@ -40,8 +40,7 @@
(*Generalizes over all free variables, with the named var outermost.*)
fun all_frees_tac (var:string) i thm =
- let val tsig = Sign.tsig_of (Thm.sign_of_thm thm);
- val frees = add_term_frees tsig (List.nth(prems_of thm,i-1),[var]);
+ let val frees = add_term_frees (Thm.theory_of_thm thm) (List.nth(prems_of thm,i-1),[var]);
val frees' = sort (rev_order o string_ord) (remove (op =) var frees) @ [var]
in Library.foldl (qnt_tac i) (all_tac,frees') thm end;