src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 39787 a44f6b11cdc4
parent 39658 b3644e40f661
child 39802 7cadad6a18cc
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 29 10:33:15 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 29 10:33:15 2010 +0200
     1.3 @@ -145,6 +145,7 @@
     1.4    (* conversions *)
     1.5    val imp_prems_conv : conv -> conv
     1.6    (* simple transformations *)
     1.7 +  val split_conjuncts_in_assms : Proof.context -> thm -> thm
     1.8    val expand_tuples : theory -> thm -> thm
     1.9    val eta_contract_ho_arguments : theory -> thm -> thm
    1.10    val remove_equalities : theory -> thm -> thm
    1.11 @@ -821,6 +822,19 @@
    1.12      val (_, args) = strip_comb atom
    1.13    in rewrite_args args end
    1.14  
    1.15 +fun split_conjuncts_in_assms ctxt th =
    1.16 +  let
    1.17 +    val ((_, [fixed_th]), ctxt') = Variable.import false [th] ctxt 
    1.18 +    fun split_conjs i nprems th =
    1.19 +      if i > nprems then th
    1.20 +      else
    1.21 +        case try Drule.RSN (@{thm conjI}, (i, th)) of
    1.22 +          SOME th' => split_conjs i (nprems+1) th'
    1.23 +        | NONE => split_conjs (i+1) nprems th
    1.24 +  in
    1.25 +    singleton (Variable.export ctxt' ctxt) (split_conjs 1 (Thm.nprems_of fixed_th) fixed_th)
    1.26 +  end
    1.27 +  
    1.28  fun expand_tuples thy intro =
    1.29    let
    1.30      val ctxt = ProofContext.init_global thy
    1.31 @@ -840,9 +854,7 @@
    1.32        (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
    1.33        intro'''
    1.34      (* splitting conjunctions introduced by Pair_eq*)
    1.35 -    fun split_conj prem =
    1.36 -      map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem))
    1.37 -    val intro''''' = map_term thy (maps_premises split_conj) intro''''
    1.38 +    val intro''''' = split_conjuncts_in_assms ctxt intro''''
    1.39    in
    1.40      intro'''''
    1.41    end