src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 39658 b3644e40f661
parent 39657 5e57675b7e40
child 39787 a44f6b11cdc4
     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 =