applying case beta reduction to case term before matching in predicate compile function flattening; moving case beta reduction function to Predicate_Compile_Aux
authorbulwahn
Thu Sep 30 15:37:11 2010 +0200 (2010-09-30)
changeset 398027cadad6a18cc
parent 39801 3a7e2964c9c0
child 39803 a8178a7b7b51
applying case beta reduction to case term before matching in predicate compile function flattening; moving case beta reduction function to Predicate_Compile_Aux
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Sep 30 11:52:22 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Sep 30 15:37:11 2010 +0200
     1.3 @@ -147,6 +147,7 @@
     1.4    (* simple transformations *)
     1.5    val split_conjuncts_in_assms : Proof.context -> thm -> thm
     1.6    val expand_tuples : theory -> thm -> thm
     1.7 +  val case_betapply : theory -> term -> term
     1.8    val eta_contract_ho_arguments : theory -> thm -> thm
     1.9    val remove_equalities : theory -> thm -> thm
    1.10    val remove_pointless_clauses : thm -> thm list
    1.11 @@ -859,6 +860,85 @@
    1.12      intro'''''
    1.13    end
    1.14  
    1.15 +(** making case distributivity rules **)
    1.16 +(*** this should be part of the datatype package ***)
    1.17 +
    1.18 +fun datatype_names_of_case_name thy case_name =
    1.19 +  map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
    1.20 +
    1.21 +fun make_case_distribs new_type_names descr sorts thy =
    1.22 +  let
    1.23 +    val case_combs = Datatype_Prop.make_case_combs new_type_names descr sorts thy "f";
    1.24 +    fun make comb =
    1.25 +      let
    1.26 +        val Type ("fun", [T, T']) = fastype_of comb;
    1.27 +        val (Const (case_name, _), fs) = strip_comb comb
    1.28 +        val used = Term.add_tfree_names comb []
    1.29 +        val U = TFree (Name.variant used "'t", HOLogic.typeS)
    1.30 +        val x = Free ("x", T)
    1.31 +        val f = Free ("f", T' --> U)
    1.32 +        fun apply_f f' =
    1.33 +          let
    1.34 +            val Ts = binder_types (fastype_of f')
    1.35 +            val bs = map Bound ((length Ts - 1) downto 0)
    1.36 +          in
    1.37 +            fold (curry absdummy) (rev Ts) (f $ (list_comb (f', bs)))
    1.38 +          end
    1.39 +        val fs' = map apply_f fs
    1.40 +        val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U)
    1.41 +      in
    1.42 +        HOLogic.mk_eq (f $ (comb $ x), list_comb (case_c', fs') $ x)
    1.43 +      end
    1.44 +  in
    1.45 +    map make case_combs
    1.46 +  end
    1.47 +
    1.48 +fun case_rewrites thy Tcon =
    1.49 +  let
    1.50 +    val info = Datatype.the_info thy Tcon
    1.51 +    val descr = #descr info
    1.52 +    val sorts = #sorts info
    1.53 +    val typ_names = the_default [Tcon] (#alt_names info)
    1.54 +  in
    1.55 +    map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
    1.56 +      (make_case_distribs typ_names [descr] sorts thy)
    1.57 +  end
    1.58 +
    1.59 +fun instantiated_case_rewrites thy Tcon =
    1.60 +  let
    1.61 +    val rew_ths = case_rewrites thy Tcon
    1.62 +    val ctxt = ProofContext.init_global thy
    1.63 +    fun instantiate th =
    1.64 +    let
    1.65 +      val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
    1.66 +      val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
    1.67 +      val ([tname, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
    1.68 +      val T = TFree (tname, HOLogic.typeS)
    1.69 +      val T' = TFree (tname', HOLogic.typeS)
    1.70 +      val U = TFree (uname, HOLogic.typeS)
    1.71 +      val y = Free (yname, U)
    1.72 +      val f' = absdummy (U --> T', Bound 0 $ y)
    1.73 +      val th' = Thm.certify_instantiate
    1.74 +        ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
    1.75 +         [((fst (dest_Var f), (U --> T') --> T'), f')]) th
    1.76 +      val [th'] = Variable.export ctxt' ctxt [th']
    1.77 +   in
    1.78 +     th'
    1.79 +   end
    1.80 + in
    1.81 +   map instantiate rew_ths
    1.82 + end
    1.83 +
    1.84 +fun case_betapply thy t =
    1.85 +  let
    1.86 +    val case_name = fst (dest_Const (fst (strip_comb t)))
    1.87 +    val Tcons = datatype_names_of_case_name thy case_name
    1.88 +    val ths = maps (instantiated_case_rewrites thy) Tcons
    1.89 +  in
    1.90 +    MetaSimplifier.rewrite_term thy
    1.91 +      (map (fn th => th RS @{thm eq_reflection}) ths) [] t
    1.92 +  end
    1.93 +
    1.94  (*** conversions ***)
    1.95  
    1.96  fun imp_prems_conv cv ct =
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Sep 30 11:52:22 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Sep 30 15:37:11 2010 +0200
     2.3 @@ -185,8 +185,9 @@
     2.4              val (f, args) = strip_comb t
     2.5              val split_thm = prepare_split_thm (ProofContext.init_global thy) raw_split_thm
     2.6              val (assms, concl) = Logic.strip_horn (prop_of split_thm)
     2.7 -            val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
     2.8 -            val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
     2.9 +            val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
    2.10 +            val t' = case_betapply thy t
    2.11 +            val subst = Pattern.match thy (split_t, t') (Vartab.empty, Vartab.empty)
    2.12              fun flatten_of_assm assm =
    2.13                let
    2.14                  val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Sep 30 11:52:22 2010 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Sep 30 15:37:11 2010 +0200
     3.3 @@ -19,73 +19,6 @@
     3.4  
     3.5  open Predicate_Compile_Aux
     3.6  
     3.7 -
     3.8 -fun datatype_names_of_case_name thy case_name =
     3.9 -  map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
    3.10 -
    3.11 -fun make_case_distribs new_type_names descr sorts thy =
    3.12 -  let
    3.13 -    val case_combs = Datatype_Prop.make_case_combs new_type_names descr sorts thy "f";
    3.14 -    fun make comb =
    3.15 -      let
    3.16 -        val Type ("fun", [T, T']) = fastype_of comb;
    3.17 -        val (Const (case_name, _), fs) = strip_comb comb
    3.18 -        val used = Term.add_tfree_names comb []
    3.19 -        val U = TFree (Name.variant used "'t", HOLogic.typeS)
    3.20 -        val x = Free ("x", T)
    3.21 -        val f = Free ("f", T' --> U)
    3.22 -        fun apply_f f' =
    3.23 -          let
    3.24 -            val Ts = binder_types (fastype_of f')
    3.25 -            val bs = map Bound ((length Ts - 1) downto 0)
    3.26 -          in
    3.27 -            fold (curry absdummy) (rev Ts) (f $ (list_comb (f', bs)))
    3.28 -          end
    3.29 -        val fs' = map apply_f fs
    3.30 -        val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U)
    3.31 -      in
    3.32 -        HOLogic.mk_eq (f $ (comb $ x), list_comb (case_c', fs') $ x)
    3.33 -      end
    3.34 -  in
    3.35 -    map make case_combs
    3.36 -  end
    3.37 -
    3.38 -fun case_rewrites thy Tcon =
    3.39 -  let
    3.40 -    val info = Datatype.the_info thy Tcon
    3.41 -    val descr = #descr info
    3.42 -    val sorts = #sorts info
    3.43 -    val typ_names = the_default [Tcon] (#alt_names info)
    3.44 -  in
    3.45 -    map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
    3.46 -      (make_case_distribs typ_names [descr] sorts thy)
    3.47 -  end
    3.48 -
    3.49 -fun instantiated_case_rewrites thy Tcon =
    3.50 -  let
    3.51 -    val rew_ths = case_rewrites thy Tcon
    3.52 -    val ctxt = ProofContext.init_global thy
    3.53 -    fun instantiate th =
    3.54 -    let
    3.55 -      val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
    3.56 -      val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
    3.57 -      val ([tname, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
    3.58 -      val T = TFree (tname, HOLogic.typeS)
    3.59 -      val T' = TFree (tname', HOLogic.typeS)
    3.60 -      val U = TFree (uname, HOLogic.typeS)
    3.61 -      val y = Free (yname, U)
    3.62 -      val f' = absdummy (U --> T', Bound 0 $ y)
    3.63 -      val th' = Thm.certify_instantiate
    3.64 -        ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
    3.65 -         [((fst (dest_Var f), (U --> T') --> T'), f')]) th
    3.66 -      val [th'] = Variable.export ctxt' ctxt [th']
    3.67 -   in
    3.68 -     th'
    3.69 -   end
    3.70 - in
    3.71 -   map instantiate rew_ths
    3.72 - end
    3.73 -
    3.74  fun is_compound ((Const (@{const_name Not}, _)) $ t) =
    3.75      error "is_compound: Negation should not occur; preprocessing is defect"
    3.76    | is_compound ((Const (@{const_name Ex}, _)) $ _) = true
    3.77 @@ -99,17 +32,13 @@
    3.78      NONE => NONE
    3.79    | SOME raw_split_thm =>
    3.80      let
    3.81 -      val case_name = fst (dest_Const (fst (strip_comb atom)))
    3.82        val split_thm = prepare_split_thm (ProofContext.init_global thy) raw_split_thm
    3.83        (* TODO: contextify things - this line is to unvarify the split_thm *)
    3.84        (*val ((_, [isplit_thm]), _) =
    3.85          Variable.import true [split_thm] (ProofContext.init_global thy)*)
    3.86        val (assms, concl) = Logic.strip_horn (prop_of split_thm)
    3.87        val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
    3.88 -      val Tcons = datatype_names_of_case_name thy case_name
    3.89 -      val ths = maps (instantiated_case_rewrites thy) Tcons
    3.90 -      val atom' = MetaSimplifier.rewrite_term thy
    3.91 -        (map (fn th => th RS @{thm eq_reflection}) ths) [] atom
    3.92 +      val atom' = case_betapply thy atom
    3.93        val subst = Pattern.match thy (split_t, atom') (Vartab.empty, Vartab.empty)
    3.94        val names' = Term.add_free_names atom' names
    3.95        fun mk_subst_rhs assm =