--- a/src/HOL/Tools/Function/pat_completeness.ML Fri Mar 06 00:00:57 2015 +0100
+++ b/src/HOL/Tools/Function/pat_completeness.ML Fri Mar 06 13:39:34 2015 +0100
@@ -40,12 +40,13 @@
(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 (Thm.cterm_of thy pat) (Thm.cterm_of thy inst) thm)
- :: (filter_pats thy cons pvars pts)
+fun filter_pats ctxt cons pvars [] = []
+ | filter_pats ctxt cons pvars (([], thm) :: pts) = raise Match
+ | filter_pats ctxt cons pvars (((pat as Free _) :: pats, thm) :: pts) =
+ let val inst = list_comb (cons, pvars) in
+ (inst :: pats,
+ inst_free (Proof_Context.cterm_of ctxt pat) (Proof_Context.cterm_of ctxt inst) thm)
+ :: (filter_pats ctxt cons pvars pts)
end
| filter_pats thy cons pvars ((pat :: pats, thm) :: pts) =
if fst (strip_comb pat) = cons
@@ -55,65 +56,66 @@
fun transform_pat _ avars c_assum ([] , thm) = raise Match
| transform_pat ctxt avars c_assum (pat :: pats, thm) =
- let
- val thy = Proof_Context.theory_of ctxt
- val (_, subps) = strip_comb pat
- val eqs = map (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
- val c_eq_pat = simplify (put_simpset HOL_basic_ss ctxt addsimps (map Thm.assume eqs)) c_assum
- in
- (subps @ pats,
- fold_rev Thm.implies_intr eqs (Thm.implies_elim thm c_eq_pat))
- end
+ let
+ val (_, subps) = strip_comb pat
+ val eqs =
+ map (Proof_Context.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
+ val c_eq_pat =
+ simplify (put_simpset HOL_basic_ss ctxt addsimps (map Thm.assume eqs)) c_assum
+ in
+ (subps @ pats,
+ fold_rev Thm.implies_intr eqs (Thm.implies_elim thm c_eq_pat))
+ end
exception COMPLETENESS
fun constr_case ctxt P idx (v :: vs) pats cons =
- let
- val thy = Proof_Context.theory_of ctxt
- val (avars, pvars, newidx) = invent_vars cons idx
- val c_hyp = Thm.cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
- val c_assum = Thm.assume c_hyp
- val newpats = map (transform_pat ctxt avars c_assum) (filter_pats thy cons pvars pats)
- in
- o_alg ctxt P newidx (avars @ vs) newpats
- |> Thm.implies_intr c_hyp
- |> fold_rev (Thm.forall_intr o Thm.cterm_of thy) avars
- end
+ let
+ val (avars, pvars, newidx) = invent_vars cons idx
+ val c_hyp =
+ Proof_Context.cterm_of ctxt
+ (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
+ val c_assum = Thm.assume c_hyp
+ val newpats = map (transform_pat ctxt avars c_assum) (filter_pats ctxt cons pvars pats)
+ in
+ o_alg ctxt P newidx (avars @ vs) newpats
+ |> Thm.implies_intr c_hyp
+ |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt) avars
+ end
| constr_case _ _ _ _ _ _ = raise Match
and o_alg _ P idx [] (([], Pthm) :: _) = Pthm
| o_alg _ P idx (v :: vs) [] = raise COMPLETENESS
| o_alg ctxt P idx (v :: vs) pts =
- if forall (is_Free o hd o fst) pts (* Var case *)
- then o_alg ctxt P idx vs
- (map (fn (pv :: pats, thm) =>
- (pats, refl RS
- (inst_free (Proof_Context.cterm_of ctxt pv)
- (Proof_Context.cterm_of ctxt v) thm))) pts)
- else (* Cons case *)
- let
- val thy = Proof_Context.theory_of ctxt
- val T as Type (tname, _) = fastype_of v
- val SOME {exhaust=case_thm, ...} = Ctr_Sugar.ctr_sugar_of ctxt tname
- val constrs = inst_constrs_of ctxt T
- val c_cases = map (constr_case ctxt P idx (v :: vs) pts) constrs
- in
- inst_case_thm thy v P case_thm
- |> fold (curry op COMP) c_cases
- end
+ if forall (is_Free o hd o fst) pts (* Var case *)
+ then o_alg ctxt P idx vs
+ (map (fn (pv :: pats, thm) =>
+ (pats, refl RS
+ (inst_free (Proof_Context.cterm_of ctxt pv)
+ (Proof_Context.cterm_of ctxt v) thm))) pts)
+ else (* Cons case *)
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val T as Type (tname, _) = fastype_of v
+ val SOME {exhaust=case_thm, ...} = Ctr_Sugar.ctr_sugar_of ctxt tname
+ val constrs = inst_constrs_of ctxt T
+ val c_cases = map (constr_case ctxt 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 ctxt xs P qss patss =
let
- val thy = Proof_Context.theory_of ctxt
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
- |> Thm.cterm_of thy
+ |> Proof_Context.cterm_of ctxt
val hyps = map2 mk_assum qss patss
- fun inst_hyps hyp qs = fold (Thm.forall_elim o Thm.cterm_of thy) qs (Thm.assume hyp)
+ fun inst_hyps hyp qs = fold (Thm.forall_elim o Proof_Context.cterm_of ctxt) qs (Thm.assume hyp)
val assums = map2 inst_hyps hyps qss
in
o_alg ctxt P 2 xs (patss ~~ assums)
@@ -122,7 +124,6 @@
fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) =>
let
- val thy = Proof_Context.theory_of ctxt
val (vs, subgf) = dest_all_all subgoal
val (cases, _ $ thesis) = Logic.strip_horn subgf
handle Bind => raise COMPLETENESS
@@ -141,7 +142,7 @@
val patss = map (map snd) x_pats
val complete_thm = prove_completeness ctxt xs thesis qss patss
- |> fold_rev (Thm.forall_intr o Thm.cterm_of thy) vs
+ |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt) vs
in
PRIMITIVE (fn st => Drule.compose (complete_thm, i, st))
end