adding splitting of conjuncts in assumptions as forward rule on theorems; replacing term transformation for splitting conjuncts by theorem transformation; removing obsolete functions; tuned
authorbulwahn
Wed Sep 29 10:33:15 2010 +0200 (2010-09-29)
changeset 39787a44f6b11cdc4
parent 39786 30c077288dfe
child 39788 9ab014d47c4d
adding splitting of conjuncts in assumptions as forward rule on theorems; replacing term transformation for splitting conjuncts by theorem transformation; removing obsolete functions; tuned
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
     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
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Sep 29 10:33:15 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Sep 29 10:33:15 2010 +0200
     2.3 @@ -256,34 +256,18 @@
     2.4    #> Conv.fconv_rule nnf_conv 
     2.5    #> Simplifier.simplify (HOL_basic_ss addsimps [@{thm ex_disj_distrib}])
     2.6  
     2.7 -fun split_conjs thy t =
     2.8 -  let 
     2.9 -    fun split_conjunctions (Const (@{const_name HOL.conj}, _) $ t1 $ t2) =
    2.10 -    (split_conjunctions t1) @ (split_conjunctions t2)
    2.11 -    | split_conjunctions t = [t]
    2.12 -  in
    2.13 -    map HOLogic.mk_Trueprop (split_conjunctions (HOLogic.dest_Trueprop t))
    2.14 -  end
    2.15 -
    2.16  fun rewrite_intros thy =
    2.17    Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm all_not_ex}])
    2.18    #> Simplifier.full_simplify
    2.19      (HOL_basic_ss addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps})
    2.20 -  #> map_term thy (maps_premises (split_conjs thy))
    2.21 +  #> split_conjuncts_in_assms (ProofContext.init_global thy)
    2.22  
    2.23  fun print_specs options thy msg ths =
    2.24    if show_intermediate_results options then
    2.25      (tracing (msg); tracing (commas (map (Display.string_of_thm_global thy) ths)))
    2.26    else
    2.27      ()
    2.28 -(*
    2.29 -fun split_cases thy th =
    2.30 -  let
    2.31 -    
    2.32 -  in
    2.33 -    map_term thy th
    2.34 -  end
    2.35 -*)
    2.36 +
    2.37  fun preprocess options (constname, specs) thy =
    2.38  (*  case Predicate_Compile_Data.processed_specs thy constname of
    2.39      SOME specss => (specss, thy)
    2.40 @@ -292,7 +276,7 @@
    2.41        val ctxt = ProofContext.init_global thy
    2.42        val intros =
    2.43          if forall is_pred_equation specs then 
    2.44 -          map (map_term thy (maps_premises (split_conjs thy))) (introrulify thy (map rewrite specs))
    2.45 +          map (split_conjuncts_in_assms ctxt) (introrulify thy (map rewrite specs))
    2.46          else if forall (is_intro constname) specs then
    2.47            map (rewrite_intros thy) specs
    2.48          else