144 val print_step : options -> string -> unit |
144 val print_step : options -> string -> unit |
145 (* conversions *) |
145 (* conversions *) |
146 val imp_prems_conv : conv -> conv |
146 val imp_prems_conv : conv -> conv |
147 (* simple transformations *) |
147 (* simple transformations *) |
148 val expand_tuples : theory -> thm -> thm |
148 val expand_tuples : theory -> thm -> thm |
149 val expand_tuples_elim : Proof.context -> thm -> thm |
|
150 val eta_contract_ho_arguments : theory -> thm -> thm |
149 val eta_contract_ho_arguments : theory -> thm -> thm |
151 val remove_equalities : theory -> thm -> thm |
150 val remove_equalities : theory -> thm -> thm |
152 val remove_pointless_clauses : thm -> thm list |
151 val remove_pointless_clauses : thm -> thm list |
153 val peephole_optimisation : theory -> thm -> thm option |
152 val peephole_optimisation : theory -> thm -> thm option |
154 val define_quickcheck_predicate : |
153 val define_quickcheck_predicate : |
858 fun all_params_conv cv ctxt ct = |
857 fun all_params_conv cv ctxt ct = |
859 if Logic.is_all (Thm.term_of ct) |
858 if Logic.is_all (Thm.term_of ct) |
860 then Conv.arg_conv (Conv.abs_conv (all_params_conv cv o #2) ctxt) ct |
859 then Conv.arg_conv (Conv.abs_conv (all_params_conv cv o #2) ctxt) ct |
861 else cv ctxt ct; |
860 else cv ctxt ct; |
862 |
861 |
863 fun expand_tuples_elim ctxt elimrule = |
|
864 let |
|
865 val thy = ProofContext.theory_of ctxt |
|
866 val ((_, [elimrule]), ctxt1) = Variable.import false [elimrule] ctxt |
|
867 val prems = Thm.prems_of elimrule |
|
868 val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems)))) |
|
869 fun preprocess_case t = |
|
870 let |
|
871 val (param_names, param_Ts) = split_list (Logic.strip_params t) |
|
872 val prop = Logic.list_implies (Logic.strip_assums_hyp t, Logic.strip_assums_concl t) |
|
873 val (free_names, ctxt2) = Variable.variant_fixes param_names ctxt1 |
|
874 val frees = map Free (free_names ~~ param_Ts) |
|
875 val prop' = subst_bounds (rev frees, prop) |
|
876 val (eqs, prems) = chop nargs (Logic.strip_imp_prems prop') |
|
877 val rhss = map (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop) eqs |
|
878 val (pats, prop'', ctxt2) = fold |
|
879 rewrite_prem (map HOLogic.dest_Trueprop prems) |
|
880 (rewrite_args rhss ([], prop', ctxt2)) |
|
881 val new_frees = fold Term.add_frees (frees @ map snd pats) [] (* FIXME: frees are not minimal and not ordered *) |
|
882 in |
|
883 fold Logic.all (map Free new_frees) prop'' |
|
884 end |
|
885 val cases' = map preprocess_case (tl prems) |
|
886 val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule) |
|
887 val tac = (fn _ => Skip_Proof.cheat_tac thy) |
|
888 val eq = Goal.prove ctxt1 [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac |
|
889 val exported_elimrule' = Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt1 ctxt) |
|
890 val elimrule'' = Conv.fconv_rule (imp_prems_conv (all_params_conv (fn ctxt => Conv.concl_conv nargs |
|
891 (Simplifier.full_rewrite |
|
892 (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]))) ctxt1)) |
|
893 exported_elimrule' |
|
894 (* splitting conjunctions introduced by Pair_eq*) |
|
895 fun split_conj prem = |
|
896 map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem)) |
|
897 fun map_cases f t = |
|
898 let |
|
899 val (prems, concl) = Logic.strip_horn t |
|
900 val ([pred], prems') = chop 1 prems |
|
901 fun map_params f t = |
|
902 let |
|
903 val prop = Logic.list_implies (Logic.strip_assums_hyp t, Logic.strip_assums_concl t) |
|
904 in Term.list_all (Logic.strip_params t, f prop) end |
|
905 val prems'' = map (map_params f) prems' |
|
906 in |
|
907 Logic.list_implies (pred :: prems'', concl) |
|
908 end |
|
909 val elimrule''' = map_term thy (map_cases (maps_premises split_conj)) elimrule'' |
|
910 in |
|
911 elimrule''' |
|
912 end |
|
913 (** eta contract higher-order arguments **) |
862 (** eta contract higher-order arguments **) |
914 |
863 |
915 fun eta_contract_ho_arguments thy intro = |
864 fun eta_contract_ho_arguments thy intro = |
916 let |
865 let |
917 fun f atom = list_comb (apsnd ((map o map_products) Envir.eta_contract) (strip_comb atom)) |
866 fun f atom = list_comb (apsnd ((map o map_products) Envir.eta_contract) (strip_comb atom)) |