1(* Title: HOL/Tools/Function/pat_completeness.ML 2 Author: Alexander Krauss, TU Muenchen 3 4Method "pat_completeness" to prove completeness of datatype patterns. 5*) 6 7signature PAT_COMPLETENESS = 8sig 9 val pat_completeness_tac: Proof.context -> int -> tactic 10 val prove_completeness: Proof.context -> term list -> term -> term list list -> 11 term list list -> thm 12end 13 14structure Pat_Completeness : PAT_COMPLETENESS = 15struct 16 17open Function_Lib 18open Function_Common 19 20 21fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T) 22fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T) 23 24fun inst_free var inst = Thm.forall_elim inst o Thm.forall_intr var 25 26fun inst_case_thm ctxt x P thm = 27 let val [P_name, x_name] = Term.add_var_names (Thm.prop_of thm) [] 28 in 29 thm |> infer_instantiate ctxt [(x_name, Thm.cterm_of ctxt x), (P_name, Thm.cterm_of ctxt P)] 30 end 31 32fun invent_vars constr i = 33 let 34 val Ts = binder_types (fastype_of constr) 35 val j = i + length Ts 36 val is = i upto (j - 1) 37 val avs = map2 mk_argvar is Ts 38 val pvs = map2 mk_patvar is Ts 39 in 40 (avs, pvs, j) 41 end 42 43fun filter_pats _ _ _ [] = [] 44 | filter_pats _ _ _ (([], _) :: _) = raise Match 45 | filter_pats ctxt cons pvars (((pat as Free _) :: pats, thm) :: pts) = 46 let val inst = list_comb (cons, pvars) in 47 (inst :: pats, inst_free (Thm.cterm_of ctxt pat) (Thm.cterm_of ctxt inst) thm) :: 48 filter_pats ctxt cons pvars pts 49 end 50 | filter_pats ctxt cons pvars ((pat :: pats, thm) :: pts) = 51 if fst (strip_comb pat) = cons 52 then (pat :: pats, thm) :: filter_pats ctxt cons pvars pts 53 else filter_pats ctxt cons pvars pts 54 55 56fun transform_pat _ _ _ ([] , _) = raise Match 57 | transform_pat ctxt avars c_assum (pat :: pats, thm) = 58 let 59 val (_, subps) = strip_comb pat 60 val eqs = map (Thm.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps) 61 val c_eq_pat = 62 simplify (put_simpset HOL_basic_ss ctxt addsimps (map Thm.assume eqs)) c_assum 63 in 64 (subps @ pats, 65 fold_rev Thm.implies_intr eqs (Thm.implies_elim thm c_eq_pat)) 66 end 67 68 69exception COMPLETENESS 70 71fun constr_case ctxt P idx (v :: vs) pats cons = 72 let 73 val (avars, pvars, newidx) = invent_vars cons idx 74 val c_hyp = 75 Thm.cterm_of ctxt 76 (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars)))) 77 val c_assum = Thm.assume c_hyp 78 val newpats = map (transform_pat ctxt avars c_assum) (filter_pats ctxt cons pvars pats) 79 in 80 o_alg ctxt P newidx (avars @ vs) newpats 81 |> Thm.implies_intr c_hyp 82 |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) avars 83 end 84 | constr_case _ _ _ _ _ _ = raise Match 85and o_alg _ P idx [] (([], Pthm) :: _) = Pthm 86 | o_alg _ P idx (v :: vs) [] = raise COMPLETENESS 87 | o_alg ctxt P idx (v :: vs) pts = 88 if forall (is_Free o hd o fst) pts (* Var case *) 89 then o_alg ctxt P idx vs 90 (map (fn (pv :: pats, thm) => 91 (pats, refl RS 92 (inst_free (Thm.cterm_of ctxt pv) 93 (Thm.cterm_of ctxt v) thm))) pts) 94 else (* Cons case *) 95 let 96 val T as Type (tname, _) = fastype_of v 97 val SOME {exhaust=case_thm, ...} = Ctr_Sugar.ctr_sugar_of ctxt tname 98 val constrs = inst_constrs_of ctxt T 99 val c_cases = map (constr_case ctxt P idx (v :: vs) pts) constrs 100 in 101 inst_case_thm ctxt v P case_thm 102 |> fold (curry op COMP) c_cases 103 end 104 | o_alg _ _ _ _ _ = raise Match 105 106fun prove_completeness ctxt xs P qss patss = 107 let 108 fun mk_assum qs pats = 109 HOLogic.mk_Trueprop P 110 |> fold_rev (curry Logic.mk_implies o HOLogic.mk_Trueprop o HOLogic.mk_eq) (xs ~~ pats) 111 |> fold_rev Logic.all qs 112 |> Thm.cterm_of ctxt 113 114 val hyps = map2 mk_assum qss patss 115 fun inst_hyps hyp qs = fold (Thm.forall_elim o Thm.cterm_of ctxt) qs (Thm.assume hyp) 116 val assums = map2 inst_hyps hyps qss 117 in 118 o_alg ctxt P 2 xs (patss ~~ assums) 119 |> fold_rev Thm.implies_intr hyps 120 end 121 122fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) => 123 let 124 val (vs, subgf) = dest_all_all subgoal 125 val (cases, _ $ thesis) = Logic.strip_horn subgf 126 handle Bind => raise COMPLETENESS 127 128 fun pat_of assum = 129 let 130 val (qs, imp) = dest_all_all assum 131 val prems = Logic.strip_imp_prems imp 132 in 133 (qs, map (HOLogic.dest_eq o HOLogic.dest_Trueprop) prems) 134 end 135 136 val (qss, x_pats) = split_list (map pat_of cases) 137 val xs = map fst (hd x_pats) 138 handle List.Empty => raise COMPLETENESS 139 140 val patss = map (map snd) x_pats 141 val complete_thm = prove_completeness ctxt xs thesis qss patss 142 |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) vs 143 in 144 PRIMITIVE (fn st => Drule.compose (complete_thm, i, st)) 145 end 146 handle COMPLETENESS => no_tac) 147 148end 149