# HG changeset patch # User blanchet # Date 1477514428 -7200 # Node ID c0d5e78eb6471847921a4466cbbb538c6e6d3e11 # Parent 2ed3da32bf414709577895de479254e518a13e60 tuning diff -r 2ed3da32bf41 -r c0d5e78eb647 src/HOL/BNF_Greatest_Fixpoint.thy --- a/src/HOL/BNF_Greatest_Fixpoint.thy Wed Oct 26 20:59:36 2016 +0200 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy Wed Oct 26 22:40:28 2016 +0200 @@ -136,8 +136,8 @@ lemma subst_Pair: "P x y \ a = (x, y) \ P (fst a) (snd a)" by simp -lemma fst_diag_id: "(fst \ (%x. (x, x))) z = id z" by simp -lemma snd_diag_id: "(snd \ (%x. (x, x))) z = id z" by simp +lemma fst_diag_id: "(fst \ (\x. (x, x))) z = id z" by simp +lemma snd_diag_id: "(snd \ (\x. (x, x))) z = id z" by simp lemma fst_diag_fst: "fst o ((\x. (x, x)) o fst) = fst" by auto lemma snd_diag_fst: "snd o ((\x. (x, x)) o fst) = fst" by auto @@ -201,16 +201,16 @@ lemma Inr_Field_csum: "a \ Field s \ Inr a \ Field (r +c s)" unfolding Field_card_of csum_def by auto -lemma rec_nat_0_imp: "f = rec_nat f1 (%n rec. f2 n rec) \ f 0 = f1" +lemma rec_nat_0_imp: "f = rec_nat f1 (\n rec. f2 n rec) \ f 0 = f1" by auto -lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \ f (Suc n) = f2 n (f n)" +lemma rec_nat_Suc_imp: "f = rec_nat f1 (\n rec. f2 n rec) \ f (Suc n) = f2 n (f n)" by auto -lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \ f [] = f1" +lemma rec_list_Nil_imp: "f = rec_list f1 (\x xs rec. f2 x xs rec) \ f [] = f1" by auto -lemma rec_list_Cons_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \ f (x # xs) = f2 x xs (f xs)" +lemma rec_list_Cons_imp: "f = rec_list f1 (\x xs rec. f2 x xs rec) \ f (x # xs) = f2 x xs (f xs)" by auto lemma not_arg_cong_Inr: "x \ y \ Inr x \ Inr y" @@ -235,40 +235,40 @@ subsection \Equivalence relations, quotients, and Hilbert's choice\ lemma equiv_Eps_in: -"\equiv A r; X \ A//r\ \ Eps (%x. x \ X) \ X" +"\equiv A r; X \ A//r\ \ Eps (\x. x \ X) \ X" apply (rule someI2_ex) using in_quotient_imp_non_empty by blast lemma equiv_Eps_preserves: assumes ECH: "equiv A r" and X: "X \ A//r" - shows "Eps (%x. x \ X) \ A" + shows "Eps (\x. x \ X) \ A" apply (rule in_mono[rule_format]) using assms apply (rule in_quotient_imp_subset) by (rule equiv_Eps_in) (rule assms)+ lemma proj_Eps: assumes "equiv A r" and "X \ A//r" - shows "proj r (Eps (%x. x \ X)) = X" + shows "proj r (Eps (\x. x \ X)) = X" unfolding proj_def proof auto fix x assume x: "x \ X" - thus "(Eps (%x. x \ X), x) \ r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast + thus "(Eps (\x. x \ X), x) \ r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast next - fix x assume "(Eps (%x. x \ X),x) \ r" + fix x assume "(Eps (\x. x \ X),x) \ r" thus "x \ X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast qed -definition univ where "univ f X == f (Eps (%x. x \ X))" +definition univ where "univ f X == f (Eps (\x. x \ X))" lemma univ_commute: assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \ A" shows "(univ f) (proj r x) = f x" proof (unfold univ_def) have prj: "proj r x \ A//r" using x proj_preserves by fast - hence "Eps (%y. y \ proj r x) \ A" using ECH equiv_Eps_preserves by fast - moreover have "proj r (Eps (%y. y \ proj r x)) = proj r x" using ECH prj proj_Eps by fast - ultimately have "(x, Eps (%y. y \ proj r x)) \ r" using x ECH proj_iff by fast - thus "f (Eps (%y. y \ proj r x)) = f x" using RES unfolding congruent_def by fastforce + hence "Eps (\y. y \ proj r x) \ A" using ECH equiv_Eps_preserves by fast + moreover have "proj r (Eps (\y. y \ proj r x)) = proj r x" using ECH prj proj_Eps by fast + ultimately have "(x, Eps (\y. y \ proj r x)) \ r" using x ECH proj_iff by fast + thus "f (Eps (\y. y \ proj r x)) = f x" using RES unfolding congruent_def by fastforce qed lemma univ_preserves: diff -r 2ed3da32bf41 -r c0d5e78eb647 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Oct 26 20:59:36 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Oct 26 22:40:28 2016 +0200 @@ -66,8 +66,6 @@ fp_bnf_sugar: fp_bnf_sugar, fp_co_induct_sugar: fp_co_induct_sugar option} - val transfer_plugin: string - val co_induct_of: 'a list -> 'a val strong_co_induct_of: 'a list -> 'a @@ -313,8 +311,6 @@ fp_bnf_sugar: fp_bnf_sugar, fp_co_induct_sugar: fp_co_induct_sugar option}; -val transfer_plugin = Plugin_Name.declare_setup @{binding transfer}; - fun co_induct_of (i :: _) = i; fun strong_co_induct_of [_, s] = s; diff -r 2ed3da32bf41 -r c0d5e78eb647 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Oct 26 20:59:36 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Oct 26 22:40:28 2016 +0200 @@ -464,7 +464,7 @@ val goals = @{map 8} mk_goals un_folds xtors ss pre_fold_maps fp_abss fp_reps abss reps; - val fp_un_folds = map (mk_pointfree lthy) (of_fp_res #xtor_un_fold_thms); + val fp_un_folds = map (mk_pointfree2 lthy) (of_fp_res #xtor_un_fold_thms); val simps = flat [simp_thms, un_fold_defs, map_defs, fp_un_folds, fp_un_fold_o_maps, map_thms, Rep_o_Abss]; diff -r 2ed3da32bf41 -r c0d5e78eb647 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Oct 26 20:59:36 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Oct 26 22:40:28 2016 +0200 @@ -862,7 +862,7 @@ val xtor_co_rec_o_map_thms = if forall is_none absT_info_opts then mk_xtor_co_iter_o_map_thms fp true m xtor_co_rec_unique_thm - (map (mk_pointfree lthy) xtor_maps) (map (mk_pointfree lthy) xtor_co_rec_thms) + (map (mk_pointfree2 lthy) xtor_maps) (map (mk_pointfree2 lthy) xtor_co_rec_thms) sym_map_comp0s map_cong0s else replicate n refl (* FIXME *); diff -r 2ed3da32bf41 -r c0d5e78eb647 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Wed Oct 26 20:59:36 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Wed Oct 26 22:40:28 2016 +0200 @@ -1676,7 +1676,7 @@ dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_notes, dtor_Jset_induct_thms, lthy) = if m = 0 then (timer, replicate n DEADID_bnf, - map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids), + map_split (`(mk_pointfree2 lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids), mk_dtor_map_unique_DEADID_thm (), replicate n [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs, @@ -2532,7 +2532,7 @@ ||>> mk_Frees "S" activephiTs; val dtor_unfold_o_Jmap_thms = mk_xtor_co_iter_o_map_thms Greatest_FP false m - dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms) + dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree2 lthy) dtor_unfold_thms) sym_map_comps map_cong0s; val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs; diff -r 2ed3da32bf41 -r c0d5e78eb647 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Wed Oct 26 20:59:36 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Wed Oct 26 22:40:28 2016 +0200 @@ -1303,7 +1303,7 @@ ctor_Irel_thms, Ibnf_notes, lthy) = if m = 0 then (timer, replicate n DEADID_bnf, - map_split (`(mk_pointfree lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_ids), + map_split (`(mk_pointfree2 lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_ids), mk_ctor_map_unique_DEADID_thm (), replicate n [], map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, [], lthy) else let @@ -1791,7 +1791,7 @@ ||>> mk_Frees "IR" activeIphiTs; val ctor_fold_o_Imap_thms = mk_xtor_co_iter_o_map_thms Least_FP false m ctor_fold_unique_thm - ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s; + ctor_Imap_o_thms (map (mk_pointfree2 lthy) ctor_fold_thms) sym_map_comps map_cong0s; val Irels = if m = 0 then map HOLogic.eq_const Ts else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs; diff -r 2ed3da32bf41 -r c0d5e78eb647 src/HOL/Tools/BNF/bnf_tactics.ML --- a/src/HOL/Tools/BNF/bnf_tactics.ML Wed Oct 26 20:59:36 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_tactics.ML Wed Oct 26 22:40:28 2016 +0200 @@ -17,7 +17,7 @@ val mk_rotate_eq_tac: Proof.context -> (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list -> int -> tactic - val mk_pointfree: Proof.context -> thm -> thm + val mk_pointfree2: Proof.context -> thm -> thm val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm val mk_Abs_inj_thm: thm -> thm @@ -47,14 +47,13 @@ fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0]; fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt o the_default [0]; - (*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*) -fun mk_pointfree ctxt thm = thm +fun mk_pointfree2 ctxt thm = thm |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> apply2 (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp) |> mk_Trueprop_eq |> (fn goal => Goal.prove_sorry ctxt [] [] goal - (K (rtac ctxt @{thm ext} 1 THEN + (K (rtac ctxt ext 1 THEN unfold_thms_tac ctxt ([o_apply, unfold_thms ctxt [o_apply] (mk_sym thm)]) THEN rtac ctxt refl 1))) |> Thm.close_derivation; @@ -67,7 +66,6 @@ (Abs_inj_thm RS @{thm bijI'}); - (* General tactic generators *) (*applies assoc rule to the lhs of an equation as long as possible*) diff -r 2ed3da32bf41 -r c0d5e78eb647 src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Wed Oct 26 20:59:36 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_util.ML Wed Oct 26 22:40:28 2016 +0200 @@ -10,6 +10,8 @@ include CTR_SUGAR_UTIL include BNF_FP_REC_SUGAR_UTIL + val transfer_plugin: string + val unflatt: 'a list list list -> 'b list -> 'b list list list val unflattt: 'a list list list list -> 'b list -> 'b list list list list @@ -121,6 +123,9 @@ open Ctr_Sugar_Util open BNF_FP_Rec_Sugar_Util +val transfer_plugin = Plugin_Name.declare_setup @{binding transfer}; + + (* Library proper *) fun unfla0 xs = fold_map (fn _ => fn (c :: cs) => (c, cs)) xs; diff -r 2ed3da32bf41 -r c0d5e78eb647 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Oct 26 20:59:36 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Oct 26 22:40:28 2016 +0200 @@ -458,7 +458,7 @@ fun all_facts ctxt generous ho_atp keywords add_ths chained css = let val thy = Proof_Context.theory_of ctxt - val transfer = Global_Theory.transfer_theories thy; + val transfer = Global_Theory.transfer_theories thy val global_facts = Global_Theory.facts_of thy val is_too_complex = if generous orelse fact_count global_facts >= max_facts_for_complex_check then K false @@ -528,7 +528,7 @@ in (* The single-theorem names go before the multiple-theorem ones (e.g., "xxx" vs. "xxx(3)"), so that single names are preferred when both are available. *) - `I [] + ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals) |> add_facts true Facts.fold_static global_facts global_facts |> op @