# HG changeset patch # User wenzelm # Date 1154782509 -7200 # Node ID d02b43ea722e39eaf57dac216313f14382b6a60b # Parent e093a54bf25ea660b4fb68cccf59e6c2c21b9847 avoid low-level tsig; diff -r e093a54bf25e -r d02b43ea722e src/HOL/Tools/function_package/fundef_datatype.ML --- 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 diff -r e093a54bf25e -r d02b43ea722e src/HOL/Tools/function_package/pattern_split.ML --- 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 diff -r e093a54bf25e -r d02b43ea722e src/HOL/Tools/specification_package.ML --- 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 diff -r e093a54bf25e -r d02b43ea722e src/Provers/ind.ML --- 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;