removing unneccessary expansion procedure for elimination rules; removing obsolete elim preprocessing; tuned
authorbulwahn
Thu Sep 23 17:22:45 2010 +0200 (2010-09-23)
changeset 39658b3644e40f661
parent 39657 5e57675b7e40
child 39668 9d554d257a10
removing unneccessary expansion procedure for elimination rules; removing obsolete elim preprocessing; tuned
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Sep 23 17:22:44 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Sep 23 17:22:45 2010 +0200
     1.3 @@ -146,7 +146,6 @@
     1.4    val imp_prems_conv : conv -> conv
     1.5    (* simple transformations *)
     1.6    val expand_tuples : theory -> thm -> thm
     1.7 -  val expand_tuples_elim : Proof.context -> thm -> thm
     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 @@ -860,56 +859,6 @@
    1.12    then Conv.arg_conv (Conv.abs_conv (all_params_conv cv o #2) ctxt) ct
    1.13    else cv ctxt ct;
    1.14    
    1.15 -fun expand_tuples_elim ctxt elimrule =
    1.16 -  let
    1.17 -    val thy = ProofContext.theory_of ctxt
    1.18 -    val ((_, [elimrule]), ctxt1) = Variable.import false [elimrule] ctxt
    1.19 -    val prems = Thm.prems_of elimrule
    1.20 -    val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems))))
    1.21 -    fun preprocess_case t =
    1.22 -      let
    1.23 -        val (param_names, param_Ts)  = split_list (Logic.strip_params t)
    1.24 -        val prop = Logic.list_implies (Logic.strip_assums_hyp t, Logic.strip_assums_concl t)
    1.25 -        val (free_names, ctxt2) = Variable.variant_fixes param_names ctxt1
    1.26 -        val frees = map Free (free_names ~~ param_Ts)
    1.27 -        val prop' = subst_bounds (rev frees, prop)
    1.28 -        val (eqs, prems) = chop nargs (Logic.strip_imp_prems prop')
    1.29 -        val rhss = map (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop) eqs
    1.30 -        val (pats, prop'', ctxt2) = fold 
    1.31 -          rewrite_prem (map HOLogic.dest_Trueprop prems)
    1.32 -            (rewrite_args rhss ([], prop', ctxt2)) 
    1.33 -        val new_frees = fold Term.add_frees (frees @ map snd pats) [] (* FIXME: frees are not minimal and not ordered *)
    1.34 -      in
    1.35 -        fold Logic.all (map Free new_frees) prop''
    1.36 -      end
    1.37 -    val cases' = map preprocess_case (tl prems)
    1.38 -    val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
    1.39 -    val tac = (fn _ => Skip_Proof.cheat_tac thy)
    1.40 -    val eq = Goal.prove ctxt1 [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac
    1.41 -    val exported_elimrule' = Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt1 ctxt)
    1.42 -    val elimrule'' = Conv.fconv_rule (imp_prems_conv (all_params_conv (fn ctxt => Conv.concl_conv nargs 
    1.43 -      (Simplifier.full_rewrite
    1.44 -        (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]))) ctxt1)) 
    1.45 -      exported_elimrule'
    1.46 -    (* splitting conjunctions introduced by Pair_eq*)
    1.47 -    fun split_conj prem =
    1.48 -      map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem))
    1.49 -    fun map_cases f t =
    1.50 -      let
    1.51 -        val (prems, concl) = Logic.strip_horn t
    1.52 -        val ([pred], prems') = chop 1 prems
    1.53 -        fun map_params f t =
    1.54 -          let
    1.55 -            val prop = Logic.list_implies (Logic.strip_assums_hyp t, Logic.strip_assums_concl t)
    1.56 -          in Term.list_all (Logic.strip_params t, f prop) end 
    1.57 -        val prems'' = map (map_params f) prems'
    1.58 -      in
    1.59 -        Logic.list_implies (pred :: prems'', concl)
    1.60 -      end
    1.61 -    val elimrule''' = map_term thy (map_cases (maps_premises split_conj)) elimrule''
    1.62 -   in
    1.63 -     elimrule'''
    1.64 -  end
    1.65  (** eta contract higher-order arguments **)
    1.66  
    1.67  fun eta_contract_ho_arguments thy intro =
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Sep 23 17:22:44 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Sep 23 17:22:45 2010 +0200
     2.3 @@ -627,36 +627,8 @@
     2.4  
     2.5  fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy
     2.6  
     2.7 -fun preprocess_equality_elim ctxt elimrule =
     2.8 -  let
     2.9 -    fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, T) $ lhs $ rhs)) =
    2.10 -       HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
    2.11 -     | replace_eqs t = t
    2.12 -    val thy = ProofContext.theory_of ctxt
    2.13 -    val ((_, [elimrule]), ctxt') = Variable.import false [elimrule] ctxt
    2.14 -    val prems = Thm.prems_of elimrule
    2.15 -    val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems))))
    2.16 -    fun preprocess_case t =
    2.17 -      let
    2.18 -        val params = Logic.strip_params t
    2.19 -        val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t)
    2.20 -        val assums_hyp' = assums1 @ (map replace_eqs assums2)
    2.21 -      in
    2.22 -        list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t))
    2.23 -      end
    2.24 -    val cases' = map preprocess_case (tl prems)
    2.25 -    val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
    2.26 -    val bigeq = (Thm.symmetric (Conv.implies_concl_conv
    2.27 -      (MetaSimplifier.rewrite true [@{thm Predicate.eq_is_eq}])
    2.28 -        (cterm_of thy elimrule')))
    2.29 -    val tac = (fn _ => Skip_Proof.cheat_tac thy)
    2.30 -    val eq = Goal.prove ctxt' [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac
    2.31 -  in
    2.32 -    Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt' ctxt)
    2.33 -  end;
    2.34 +(* fetching introduction rules or registering introduction rules *)
    2.35  
    2.36 -fun preprocess_elim ctxt = expand_tuples_elim ctxt #> preprocess_equality_elim ctxt
    2.37 -  
    2.38  val no_compilation = ([], ([], []))
    2.39  
    2.40  fun fetch_pred_data ctxt name =