# HG changeset patch # User krauss # Date 1256301187 -7200 # Node ID 1fad3160d873412c09582184472b3229dbfd7182 # Parent ccefc096abc9d79f28d6d740fe1c313603227f1f pat_completeness gets its own file diff -r ccefc096abc9 -r 1fad3160d873 src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Fri Oct 23 14:22:36 2009 +0200 +++ b/src/HOL/FunDef.thy Fri Oct 23 14:33:07 2009 +0200 @@ -21,6 +21,7 @@ ("Tools/Function/auto_term.ML") ("Tools/Function/measure_functions.ML") ("Tools/Function/lexicographic_order.ML") + ("Tools/Function/pat_completeness.ML") ("Tools/Function/fundef_datatype.ML") ("Tools/Function/induction_scheme.ML") ("Tools/Function/termination.ML") @@ -113,11 +114,13 @@ use "Tools/Function/pattern_split.ML" use "Tools/Function/auto_term.ML" use "Tools/Function/fundef.ML" +use "Tools/Function/pat_completeness.ML" use "Tools/Function/fundef_datatype.ML" use "Tools/Function/induction_scheme.ML" setup {* - Fundef.setup + Fundef.setup + #> Pat_Completeness.setup #> FundefDatatype.setup #> InductionScheme.setup *} diff -r ccefc096abc9 -r 1fad3160d873 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Oct 23 14:22:36 2009 +0200 +++ b/src/HOL/IsaMakefile Fri Oct 23 14:33:07 2009 +0200 @@ -170,6 +170,7 @@ Tools/Function/lexicographic_order.ML \ Tools/Function/measure_functions.ML \ Tools/Function/mutual.ML \ + Tools/Function/pat_completeness.ML \ Tools/Function/pattern_split.ML \ Tools/Function/scnp_reconstruct.ML \ Tools/Function/scnp_solve.ML \ diff -r ccefc096abc9 -r 1fad3160d873 src/HOL/Tools/Function/fundef_datatype.ML --- a/src/HOL/Tools/Function/fundef_datatype.ML Fri Oct 23 14:22:36 2009 +0200 +++ b/src/HOL/Tools/Function/fundef_datatype.ML Fri Oct 23 14:33:07 2009 +0200 @@ -7,18 +7,14 @@ signature FUNDEF_DATATYPE = sig - val pat_completeness_tac: Proof.context -> int -> tactic - val pat_completeness: Proof.context -> Proof.method - val prove_completeness : theory -> term list -> term -> term list list -> term list list -> thm - - val setup : theory -> theory - val add_fun : FundefCommon.fundef_config -> (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> bool -> local_theory -> Proof.context val add_fun_cmd : FundefCommon.fundef_config -> (binding * string option * mixfix) list -> (Attrib.binding * string) list -> bool -> local_theory -> Proof.context + + val setup : theory -> theory end structure FundefDatatype : FUNDEF_DATATYPE = @@ -60,155 +56,9 @@ () end - -fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T) -fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T) - -fun inst_free var inst thm = - forall_elim inst (forall_intr var thm) - - -fun inst_case_thm thy x P thm = - let - val [Pv, xv] = Term.add_vars (prop_of thm) [] - in - cterm_instantiate [(cterm_of thy (Var xv), cterm_of thy x), - (cterm_of thy (Var 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 - in - (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) = - 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 - | _ => if fst (strip_comb pat) = cons - 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_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT))) - (the (Datatype.get_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 - in - (subps @ pats, fold_rev implies_intr eqs - (implies_elim thm c_eq_pat)) - end - - -exception COMPLETENESS - -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) - in - 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 - | o_alg thy P idx (v :: vs) [] = raise COMPLETENESS - | 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) - else (* Cons case *) - let - val T = fastype_of v - val (tname, _) = dest_Type T - val {exhaust=case_thm, ...} = Datatype.the_info 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 xs P qss patss = - let - fun mk_assum qs pats = - HOLogic.mk_Trueprop P - |> fold_rev (curry Logic.mk_implies o HOLogic.mk_Trueprop o HOLogic.mk_eq) (xs ~~ pats) - |> fold_rev Logic.all qs - |> cterm_of thy - - val hyps = map2 mk_assum qss patss - - fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp) - - val assums = map2 inst_hyps hyps qss - in - o_alg thy P 2 xs (patss ~~ assums) - |> fold_rev implies_intr hyps - end - - - -fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) => - let - val thy = ProofContext.theory_of ctxt - val (vs, subgf) = dest_all_all subgoal - val (cases, _ $ thesis) = Logic.strip_horn subgf - handle Bind => raise COMPLETENESS - - fun pat_of assum = - let - val (qs, imp) = dest_all_all assum - val prems = Logic.strip_imp_prems imp - in - (qs, map (HOLogic.dest_eq o HOLogic.dest_Trueprop) prems) - end - - val (qss, x_pats) = split_list (map pat_of cases) - val xs = map fst (hd x_pats) - handle Empty => raise COMPLETENESS - - val patss = map (map snd) x_pats - - val complete_thm = prove_completeness thy xs thesis qss patss - |> fold_rev (forall_intr o cterm_of thy) vs - in - PRIMITIVE (fn st => Drule.compose_single(complete_thm, i, st)) - end - handle COMPLETENESS => no_tac) - - -fun pat_completeness ctxt = SIMPLE_METHOD' (pat_completeness_tac ctxt) - val by_pat_completeness_auto = Proof.global_future_terminal_proof - (Method.Basic pat_completeness, + (Method.Basic Pat_Completeness.pat_completeness, SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) fun termination_by method int = @@ -294,9 +144,7 @@ FundefCommon.empty_preproc check_defs config ctxt fixes spec val setup = - Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness) - "Completeness prover for datatype patterns" - #> Context.theory_map (FundefCommon.set_preproc sequential_preproc) + Context.theory_map (FundefCommon.set_preproc sequential_preproc) val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), diff -r ccefc096abc9 -r 1fad3160d873 src/HOL/Tools/Function/induction_scheme.ML --- a/src/HOL/Tools/Function/induction_scheme.ML Fri Oct 23 14:22:36 2009 +0200 +++ b/src/HOL/Tools/Function/induction_scheme.ML Fri Oct 23 14:33:07 2009 +0200 @@ -244,7 +244,7 @@ (* Rule for case splitting along the sum types *) val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches val pats = map_index (uncurry inject) xss - val sum_split_rule = FundefDatatype.prove_completeness thy [x] (P_comp $ x) xss (map single pats) + val sum_split_rule = Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats) fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) = let diff -r ccefc096abc9 -r 1fad3160d873 src/HOL/Tools/Function/pat_completeness.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Function/pat_completeness.ML Fri Oct 23 14:33:07 2009 +0200 @@ -0,0 +1,163 @@ +(* Title: HOL/Tools/Function/fundef_datatype.ML + Author: Alexander Krauss, TU Muenchen + +Method "pat_completeness" to prove completeness of datatype patterns. +*) + +signature PAT_COMPLETENESS = +sig + val pat_completeness_tac: Proof.context -> int -> tactic + val pat_completeness: Proof.context -> Proof.method + val prove_completeness : theory -> term list -> term -> term list list -> + term list list -> thm + + val setup : theory -> theory +end + +structure Pat_Completeness : PAT_COMPLETENESS = +struct + +open FundefLib +open FundefCommon + + +fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T) +fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T) + +fun inst_free var inst = forall_elim inst o forall_intr var + +fun inst_case_thm thy x P thm = + let val [Pv, xv] = Term.add_vars (prop_of thm) [] + in + thm |> cterm_instantiate (map (pairself (cterm_of thy)) + [(Var xv, x), (Var Pv, P)]) + 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 + in + (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 as Free _) :: pats, thm) :: pts) = + 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 + | filter_pats thy cons pvars ((pat :: pats, thm) :: pts) = + if fst (strip_comb pat) = cons + 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_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT))) + (the (Datatype.get_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 c_eq_pat = simplify (HOL_basic_ss addsimps (map assume eqs)) c_assum + in + (subps @ pats, + fold_rev implies_intr eqs (implies_elim thm c_eq_pat)) + end + + +exception COMPLETENESS + +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) + in + 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 + | o_alg thy P idx (v :: vs) [] = raise COMPLETENESS + | 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) + else (* Cons case *) + let + val T = fastype_of v + val (tname, _) = dest_Type T + val {exhaust=case_thm, ...} = Datatype.the_info 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 xs P qss patss = + let + fun mk_assum qs pats = + HOLogic.mk_Trueprop P + |> fold_rev (curry Logic.mk_implies o HOLogic.mk_Trueprop o HOLogic.mk_eq) (xs ~~ pats) + |> fold_rev Logic.all qs + |> cterm_of thy + + val hyps = map2 mk_assum qss patss + fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp) + val assums = map2 inst_hyps hyps qss + in + o_alg thy P 2 xs (patss ~~ assums) + |> fold_rev implies_intr hyps + end + +fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) => + let + val thy = ProofContext.theory_of ctxt + val (vs, subgf) = dest_all_all subgoal + val (cases, _ $ thesis) = Logic.strip_horn subgf + handle Bind => raise COMPLETENESS + + fun pat_of assum = + let + val (qs, imp) = dest_all_all assum + val prems = Logic.strip_imp_prems imp + in + (qs, map (HOLogic.dest_eq o HOLogic.dest_Trueprop) prems) + end + + val (qss, x_pats) = split_list (map pat_of cases) + val xs = map fst (hd x_pats) + handle Empty => raise COMPLETENESS + + val patss = map (map snd) x_pats + val complete_thm = prove_completeness thy xs thesis qss patss + |> fold_rev (forall_intr o cterm_of thy) vs + in + PRIMITIVE (fn st => Drule.compose_single(complete_thm, i, st)) + end + handle COMPLETENESS => no_tac) + + +val pat_completeness = SIMPLE_METHOD' o pat_completeness_tac + +val setup = + Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness) + "Completeness prover for datatype patterns" + +end