pat_completeness gets its own file
authorkrauss
Fri Oct 23 14:33:07 2009 +0200 (2009-10-23)
changeset 330831fad3160d873
parent 33082 ccefc096abc9
child 33085 c1b6cc29496b
child 33175 2083bde13ce1
child 33269 3b7e2dbbd684
pat_completeness gets its own file
src/HOL/FunDef.thy
src/HOL/IsaMakefile
src/HOL/Tools/Function/fundef_datatype.ML
src/HOL/Tools/Function/induction_scheme.ML
src/HOL/Tools/Function/pat_completeness.ML
     1.1 --- a/src/HOL/FunDef.thy	Fri Oct 23 14:22:36 2009 +0200
     1.2 +++ b/src/HOL/FunDef.thy	Fri Oct 23 14:33:07 2009 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    ("Tools/Function/auto_term.ML")
     1.5    ("Tools/Function/measure_functions.ML")
     1.6    ("Tools/Function/lexicographic_order.ML")
     1.7 +  ("Tools/Function/pat_completeness.ML")
     1.8    ("Tools/Function/fundef_datatype.ML")
     1.9    ("Tools/Function/induction_scheme.ML")
    1.10    ("Tools/Function/termination.ML")
    1.11 @@ -113,11 +114,13 @@
    1.12  use "Tools/Function/pattern_split.ML"
    1.13  use "Tools/Function/auto_term.ML"
    1.14  use "Tools/Function/fundef.ML"
    1.15 +use "Tools/Function/pat_completeness.ML"
    1.16  use "Tools/Function/fundef_datatype.ML"
    1.17  use "Tools/Function/induction_scheme.ML"
    1.18  
    1.19  setup {* 
    1.20 -  Fundef.setup 
    1.21 +  Fundef.setup
    1.22 +  #> Pat_Completeness.setup
    1.23    #> FundefDatatype.setup
    1.24    #> InductionScheme.setup
    1.25  *}
     2.1 --- a/src/HOL/IsaMakefile	Fri Oct 23 14:22:36 2009 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Fri Oct 23 14:33:07 2009 +0200
     2.3 @@ -170,6 +170,7 @@
     2.4    Tools/Function/lexicographic_order.ML \
     2.5    Tools/Function/measure_functions.ML \
     2.6    Tools/Function/mutual.ML \
     2.7 +  Tools/Function/pat_completeness.ML \
     2.8    Tools/Function/pattern_split.ML \
     2.9    Tools/Function/scnp_reconstruct.ML \
    2.10    Tools/Function/scnp_solve.ML \
     3.1 --- a/src/HOL/Tools/Function/fundef_datatype.ML	Fri Oct 23 14:22:36 2009 +0200
     3.2 +++ b/src/HOL/Tools/Function/fundef_datatype.ML	Fri Oct 23 14:33:07 2009 +0200
     3.3 @@ -7,18 +7,14 @@
     3.4  
     3.5  signature FUNDEF_DATATYPE =
     3.6  sig
     3.7 -    val pat_completeness_tac: Proof.context -> int -> tactic
     3.8 -    val pat_completeness: Proof.context -> Proof.method
     3.9 -    val prove_completeness : theory -> term list -> term -> term list list -> term list list -> thm
    3.10 -
    3.11 -    val setup : theory -> theory
    3.12 -
    3.13      val add_fun : FundefCommon.fundef_config ->
    3.14        (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
    3.15        bool -> local_theory -> Proof.context
    3.16      val add_fun_cmd : FundefCommon.fundef_config ->
    3.17        (binding * string option * mixfix) list -> (Attrib.binding * string) list ->
    3.18        bool -> local_theory -> Proof.context
    3.19 +
    3.20 +    val setup : theory -> theory
    3.21  end
    3.22  
    3.23  structure FundefDatatype : FUNDEF_DATATYPE =
    3.24 @@ -60,155 +56,9 @@
    3.25        ()
    3.26      end
    3.27      
    3.28 -
    3.29 -fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
    3.30 -fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T)
    3.31 -
    3.32 -fun inst_free var inst thm =
    3.33 -    forall_elim inst (forall_intr var thm)
    3.34 -
    3.35 -
    3.36 -fun inst_case_thm thy x P thm =
    3.37 -    let
    3.38 -        val [Pv, xv] = Term.add_vars (prop_of thm) []
    3.39 -    in
    3.40 -        cterm_instantiate [(cterm_of thy (Var xv), cterm_of thy x), 
    3.41 -                           (cterm_of thy (Var Pv), cterm_of thy P)] thm
    3.42 -    end
    3.43 -
    3.44 -
    3.45 -fun invent_vars constr i =
    3.46 -    let
    3.47 -        val Ts = binder_types (fastype_of constr)
    3.48 -        val j = i + length Ts
    3.49 -        val is = i upto (j - 1)
    3.50 -        val avs = map2 mk_argvar is Ts
    3.51 -        val pvs = map2 mk_patvar is Ts
    3.52 -    in
    3.53 -        (avs, pvs, j)
    3.54 -    end
    3.55 -
    3.56 -
    3.57 -fun filter_pats thy cons pvars [] = []
    3.58 -  | filter_pats thy cons pvars (([], thm) :: pts) = raise Match
    3.59 -  | filter_pats thy cons pvars ((pat :: pats, thm) :: pts) =
    3.60 -    case pat of
    3.61 -        Free _ => let val inst = list_comb (cons, pvars)
    3.62 -                 in (inst :: pats, inst_free (cterm_of thy pat) (cterm_of thy inst) thm)
    3.63 -                    :: (filter_pats thy cons pvars pts) end
    3.64 -      | _ => if fst (strip_comb pat) = cons
    3.65 -             then (pat :: pats, thm) :: (filter_pats thy cons pvars pts)
    3.66 -             else filter_pats thy cons pvars pts
    3.67 -
    3.68 -
    3.69 -fun inst_constrs_of thy (T as Type (name, _)) =
    3.70 -        map (fn (Cn,CT) =>
    3.71 -              Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
    3.72 -            (the (Datatype.get_constrs thy name))
    3.73 -  | inst_constrs_of thy _ = raise Match
    3.74 -
    3.75 -
    3.76 -fun transform_pat thy avars c_assum ([] , thm) = raise Match
    3.77 -  | transform_pat thy avars c_assum (pat :: pats, thm) =
    3.78 -    let
    3.79 -        val (_, subps) = strip_comb pat
    3.80 -        val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
    3.81 -        val a_eqs = map assume eqs
    3.82 -        val c_eq_pat = simplify (HOL_basic_ss addsimps a_eqs) c_assum
    3.83 -    in
    3.84 -        (subps @ pats, fold_rev implies_intr eqs
    3.85 -                                (implies_elim thm c_eq_pat))
    3.86 -    end
    3.87 -
    3.88 -
    3.89 -exception COMPLETENESS
    3.90 -
    3.91 -fun constr_case thy P idx (v :: vs) pats cons =
    3.92 -    let
    3.93 -        val (avars, pvars, newidx) = invent_vars cons idx
    3.94 -        val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
    3.95 -        val c_assum = assume c_hyp
    3.96 -        val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats)
    3.97 -    in
    3.98 -        o_alg thy P newidx (avars @ vs) newpats
    3.99 -              |> implies_intr c_hyp
   3.100 -              |> fold_rev (forall_intr o cterm_of thy) avars
   3.101 -    end
   3.102 -  | constr_case _ _ _ _ _ _ = raise Match
   3.103 -and o_alg thy P idx [] (([], Pthm) :: _)  = Pthm
   3.104 -  | o_alg thy P idx (v :: vs) [] = raise COMPLETENESS
   3.105 -  | o_alg thy P idx (v :: vs) pts =
   3.106 -    if forall (is_Free o hd o fst) pts (* Var case *)
   3.107 -    then o_alg thy P idx vs (map (fn (pv :: pats, thm) =>
   3.108 -                               (pats, refl RS (inst_free (cterm_of thy pv) (cterm_of thy v) thm))) pts)
   3.109 -    else (* Cons case *)
   3.110 -         let
   3.111 -             val T = fastype_of v
   3.112 -             val (tname, _) = dest_Type T
   3.113 -             val {exhaust=case_thm, ...} = Datatype.the_info thy tname
   3.114 -             val constrs = inst_constrs_of thy T
   3.115 -             val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
   3.116 -         in
   3.117 -             inst_case_thm thy v P case_thm
   3.118 -                           |> fold (curry op COMP) c_cases
   3.119 -         end
   3.120 -  | o_alg _ _ _ _ _ = raise Match
   3.121 -
   3.122 -
   3.123 -fun prove_completeness thy xs P qss patss =
   3.124 -    let
   3.125 -        fun mk_assum qs pats = 
   3.126 -            HOLogic.mk_Trueprop P
   3.127 -            |> fold_rev (curry Logic.mk_implies o HOLogic.mk_Trueprop o HOLogic.mk_eq) (xs ~~ pats)
   3.128 -            |> fold_rev Logic.all qs
   3.129 -            |> cterm_of thy
   3.130 -
   3.131 -        val hyps = map2 mk_assum qss patss
   3.132 -
   3.133 -        fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp)
   3.134 -
   3.135 -        val assums = map2 inst_hyps hyps qss
   3.136 -    in
   3.137 -        o_alg thy P 2 xs (patss ~~ assums)
   3.138 -              |> fold_rev implies_intr hyps
   3.139 -    end
   3.140 -
   3.141 -
   3.142 -
   3.143 -fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) =>
   3.144 -    let
   3.145 -      val thy = ProofContext.theory_of ctxt
   3.146 -      val (vs, subgf) = dest_all_all subgoal
   3.147 -      val (cases, _ $ thesis) = Logic.strip_horn subgf
   3.148 -          handle Bind => raise COMPLETENESS
   3.149 -
   3.150 -      fun pat_of assum =
   3.151 -            let
   3.152 -                val (qs, imp) = dest_all_all assum
   3.153 -                val prems = Logic.strip_imp_prems imp
   3.154 -            in
   3.155 -              (qs, map (HOLogic.dest_eq o HOLogic.dest_Trueprop) prems)
   3.156 -            end
   3.157 -
   3.158 -        val (qss, x_pats) = split_list (map pat_of cases)
   3.159 -        val xs = map fst (hd x_pats)
   3.160 -                 handle Empty => raise COMPLETENESS
   3.161 -                 
   3.162 -        val patss = map (map snd) x_pats 
   3.163 -
   3.164 -        val complete_thm = prove_completeness thy xs thesis qss patss
   3.165 -             |> fold_rev (forall_intr o cterm_of thy) vs
   3.166 -    in
   3.167 -      PRIMITIVE (fn st => Drule.compose_single(complete_thm, i, st))
   3.168 -    end
   3.169 -    handle COMPLETENESS => no_tac)
   3.170 -
   3.171 -
   3.172 -fun pat_completeness ctxt = SIMPLE_METHOD' (pat_completeness_tac ctxt)
   3.173 -
   3.174  val by_pat_completeness_auto =
   3.175      Proof.global_future_terminal_proof
   3.176 -      (Method.Basic pat_completeness,
   3.177 +      (Method.Basic Pat_Completeness.pat_completeness,
   3.178         SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
   3.179  
   3.180  fun termination_by method int =
   3.181 @@ -294,9 +144,7 @@
   3.182          FundefCommon.empty_preproc check_defs config ctxt fixes spec
   3.183  
   3.184  val setup =
   3.185 -    Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness)
   3.186 -        "Completeness prover for datatype patterns"
   3.187 -    #> Context.theory_map (FundefCommon.set_preproc sequential_preproc)
   3.188 +  Context.theory_map (FundefCommon.set_preproc sequential_preproc)
   3.189  
   3.190  
   3.191  val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), 
     4.1 --- a/src/HOL/Tools/Function/induction_scheme.ML	Fri Oct 23 14:22:36 2009 +0200
     4.2 +++ b/src/HOL/Tools/Function/induction_scheme.ML	Fri Oct 23 14:33:07 2009 +0200
     4.3 @@ -244,7 +244,7 @@
     4.4       (* Rule for case splitting along the sum types *)
     4.5        val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
     4.6        val pats = map_index (uncurry inject) xss
     4.7 -      val sum_split_rule = FundefDatatype.prove_completeness thy [x] (P_comp $ x) xss (map single pats)
     4.8 +      val sum_split_rule = Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats)
     4.9  
    4.10        fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
    4.11            let
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/Function/pat_completeness.ML	Fri Oct 23 14:33:07 2009 +0200
     5.3 @@ -0,0 +1,163 @@
     5.4 +(*  Title:      HOL/Tools/Function/fundef_datatype.ML
     5.5 +    Author:     Alexander Krauss, TU Muenchen
     5.6 +
     5.7 +Method "pat_completeness" to prove completeness of datatype patterns.
     5.8 +*)
     5.9 +
    5.10 +signature PAT_COMPLETENESS =
    5.11 +sig
    5.12 +    val pat_completeness_tac: Proof.context -> int -> tactic
    5.13 +    val pat_completeness: Proof.context -> Proof.method
    5.14 +    val prove_completeness : theory -> term list -> term -> term list list ->
    5.15 +      term list list -> thm
    5.16 +
    5.17 +    val setup : theory -> theory
    5.18 +end
    5.19 +
    5.20 +structure Pat_Completeness : PAT_COMPLETENESS =
    5.21 +struct
    5.22 +
    5.23 +open FundefLib
    5.24 +open FundefCommon
    5.25 +
    5.26 +
    5.27 +fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
    5.28 +fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T)
    5.29 +
    5.30 +fun inst_free var inst = forall_elim inst o forall_intr var
    5.31 +
    5.32 +fun inst_case_thm thy x P thm =
    5.33 +  let val [Pv, xv] = Term.add_vars (prop_of thm) []
    5.34 +  in
    5.35 +    thm |> cterm_instantiate (map (pairself (cterm_of thy))
    5.36 +      [(Var xv, x), (Var Pv, P)])
    5.37 +  end
    5.38 +
    5.39 +fun invent_vars constr i =
    5.40 +  let
    5.41 +    val Ts = binder_types (fastype_of constr)
    5.42 +    val j = i + length Ts
    5.43 +    val is = i upto (j - 1)
    5.44 +    val avs = map2 mk_argvar is Ts
    5.45 +    val pvs = map2 mk_patvar is Ts
    5.46 + in
    5.47 +   (avs, pvs, j)
    5.48 + end
    5.49 +
    5.50 +fun filter_pats thy cons pvars [] = []
    5.51 +  | filter_pats thy cons pvars (([], thm) :: pts) = raise Match
    5.52 +  | filter_pats thy cons pvars (((pat as Free _) :: pats, thm) :: pts) =
    5.53 +    let val inst = list_comb (cons, pvars)
    5.54 +    in (inst :: pats, inst_free (cterm_of thy pat) (cterm_of thy inst) thm)
    5.55 +       :: (filter_pats thy cons pvars pts)
    5.56 +    end
    5.57 +  | filter_pats thy cons pvars ((pat :: pats, thm) :: pts) =
    5.58 +    if fst (strip_comb pat) = cons
    5.59 +    then (pat :: pats, thm) :: (filter_pats thy cons pvars pts)
    5.60 +    else filter_pats thy cons pvars pts
    5.61 +
    5.62 +
    5.63 +fun inst_constrs_of thy (T as Type (name, _)) =
    5.64 +  map (fn (Cn,CT) =>
    5.65 +          Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
    5.66 +      (the (Datatype.get_constrs thy name))
    5.67 +  | inst_constrs_of thy _ = raise Match
    5.68 +
    5.69 +
    5.70 +fun transform_pat thy avars c_assum ([] , thm) = raise Match
    5.71 +  | transform_pat thy avars c_assum (pat :: pats, thm) =
    5.72 +  let
    5.73 +    val (_, subps) = strip_comb pat
    5.74 +    val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
    5.75 +    val c_eq_pat = simplify (HOL_basic_ss addsimps (map assume eqs)) c_assum
    5.76 +  in
    5.77 +    (subps @ pats,
    5.78 +     fold_rev implies_intr eqs (implies_elim thm c_eq_pat))
    5.79 +  end
    5.80 +
    5.81 +
    5.82 +exception COMPLETENESS
    5.83 +
    5.84 +fun constr_case thy P idx (v :: vs) pats cons =
    5.85 +  let
    5.86 +    val (avars, pvars, newidx) = invent_vars cons idx
    5.87 +    val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
    5.88 +    val c_assum = assume c_hyp
    5.89 +    val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats)
    5.90 +  in
    5.91 +    o_alg thy P newidx (avars @ vs) newpats
    5.92 +    |> implies_intr c_hyp
    5.93 +    |> fold_rev (forall_intr o cterm_of thy) avars
    5.94 +  end
    5.95 +  | constr_case _ _ _ _ _ _ = raise Match
    5.96 +and o_alg thy P idx [] (([], Pthm) :: _)  = Pthm
    5.97 +  | o_alg thy P idx (v :: vs) [] = raise COMPLETENESS
    5.98 +  | o_alg thy P idx (v :: vs) pts =
    5.99 +  if forall (is_Free o hd o fst) pts (* Var case *)
   5.100 +  then o_alg thy P idx vs
   5.101 +         (map (fn (pv :: pats, thm) =>
   5.102 +           (pats, refl RS (inst_free (cterm_of thy pv) (cterm_of thy v) thm))) pts)
   5.103 +  else (* Cons case *)
   5.104 +    let
   5.105 +      val T = fastype_of v
   5.106 +      val (tname, _) = dest_Type T
   5.107 +      val {exhaust=case_thm, ...} = Datatype.the_info thy tname
   5.108 +      val constrs = inst_constrs_of thy T
   5.109 +      val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
   5.110 +    in
   5.111 +      inst_case_thm thy v P case_thm
   5.112 +      |> fold (curry op COMP) c_cases
   5.113 +    end
   5.114 +  | o_alg _ _ _ _ _ = raise Match
   5.115 +
   5.116 +fun prove_completeness thy xs P qss patss =
   5.117 +  let
   5.118 +    fun mk_assum qs pats =
   5.119 +      HOLogic.mk_Trueprop P
   5.120 +      |> fold_rev (curry Logic.mk_implies o HOLogic.mk_Trueprop o HOLogic.mk_eq) (xs ~~ pats)
   5.121 +      |> fold_rev Logic.all qs
   5.122 +      |> cterm_of thy
   5.123 +
   5.124 +    val hyps = map2 mk_assum qss patss
   5.125 +    fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp)
   5.126 +    val assums = map2 inst_hyps hyps qss
   5.127 +    in
   5.128 +      o_alg thy P 2 xs (patss ~~ assums)
   5.129 +      |> fold_rev implies_intr hyps
   5.130 +    end
   5.131 +
   5.132 +fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) =>
   5.133 +  let
   5.134 +    val thy = ProofContext.theory_of ctxt
   5.135 +    val (vs, subgf) = dest_all_all subgoal
   5.136 +    val (cases, _ $ thesis) = Logic.strip_horn subgf
   5.137 +      handle Bind => raise COMPLETENESS
   5.138 +
   5.139 +    fun pat_of assum =
   5.140 +      let
   5.141 +        val (qs, imp) = dest_all_all assum
   5.142 +        val prems = Logic.strip_imp_prems imp
   5.143 +      in
   5.144 +        (qs, map (HOLogic.dest_eq o HOLogic.dest_Trueprop) prems)
   5.145 +      end
   5.146 +
   5.147 +    val (qss, x_pats) = split_list (map pat_of cases)
   5.148 +    val xs = map fst (hd x_pats)
   5.149 +      handle Empty => raise COMPLETENESS
   5.150 +
   5.151 +    val patss = map (map snd) x_pats
   5.152 +    val complete_thm = prove_completeness thy xs thesis qss patss
   5.153 +      |> fold_rev (forall_intr o cterm_of thy) vs
   5.154 +    in
   5.155 +      PRIMITIVE (fn st => Drule.compose_single(complete_thm, i, st))
   5.156 +  end
   5.157 +  handle COMPLETENESS => no_tac)
   5.158 +
   5.159 +
   5.160 +val pat_completeness = SIMPLE_METHOD' o pat_completeness_tac
   5.161 +
   5.162 +val setup =
   5.163 +  Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness)
   5.164 +    "Completeness prover for datatype patterns"
   5.165 +
   5.166 +end