--- 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
*}
--- 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 \
--- 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*),
--- 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
--- /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