tuning
authorblanchet
Wed Oct 26 22:40:28 2016 +0200 (2016-10-26)
changeset 64413c0d5e78eb647
parent 64412 2ed3da32bf41
child 64414 f8be2208e99c
child 64419 0f3b0a929c02
tuning
src/HOL/BNF_Greatest_Fixpoint.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/BNF/bnf_tactics.ML
src/HOL/Tools/BNF/bnf_util.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Wed Oct 26 20:59:36 2016 +0200
     1.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Wed Oct 26 22:40:28 2016 +0200
     1.3 @@ -136,8 +136,8 @@
     1.4  lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
     1.5    by simp
     1.6  
     1.7 -lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z" by simp
     1.8 -lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z" by simp
     1.9 +lemma fst_diag_id: "(fst \<circ> (\<lambda>x. (x, x))) z = id z" by simp
    1.10 +lemma snd_diag_id: "(snd \<circ> (\<lambda>x. (x, x))) z = id z" by simp
    1.11  
    1.12  lemma fst_diag_fst: "fst o ((\<lambda>x. (x, x)) o fst) = fst" by auto
    1.13  lemma snd_diag_fst: "snd o ((\<lambda>x. (x, x)) o fst) = fst" by auto
    1.14 @@ -201,16 +201,16 @@
    1.15  lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
    1.16    unfolding Field_card_of csum_def by auto
    1.17  
    1.18 -lemma rec_nat_0_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
    1.19 +lemma rec_nat_0_imp: "f = rec_nat f1 (\<lambda>n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
    1.20    by auto
    1.21  
    1.22 -lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
    1.23 +lemma rec_nat_Suc_imp: "f = rec_nat f1 (\<lambda>n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
    1.24    by auto
    1.25  
    1.26 -lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
    1.27 +lemma rec_list_Nil_imp: "f = rec_list f1 (\<lambda>x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
    1.28    by auto
    1.29  
    1.30 -lemma rec_list_Cons_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
    1.31 +lemma rec_list_Cons_imp: "f = rec_list f1 (\<lambda>x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
    1.32    by auto
    1.33  
    1.34  lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
    1.35 @@ -235,40 +235,40 @@
    1.36  subsection \<open>Equivalence relations, quotients, and Hilbert's choice\<close>
    1.37  
    1.38  lemma equiv_Eps_in:
    1.39 -"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
    1.40 +"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (\<lambda>x. x \<in> X) \<in> X"
    1.41    apply (rule someI2_ex)
    1.42    using in_quotient_imp_non_empty by blast
    1.43  
    1.44  lemma equiv_Eps_preserves:
    1.45    assumes ECH: "equiv A r" and X: "X \<in> A//r"
    1.46 -  shows "Eps (%x. x \<in> X) \<in> A"
    1.47 +  shows "Eps (\<lambda>x. x \<in> X) \<in> A"
    1.48    apply (rule in_mono[rule_format])
    1.49     using assms apply (rule in_quotient_imp_subset)
    1.50    by (rule equiv_Eps_in) (rule assms)+
    1.51  
    1.52  lemma proj_Eps:
    1.53    assumes "equiv A r" and "X \<in> A//r"
    1.54 -  shows "proj r (Eps (%x. x \<in> X)) = X"
    1.55 +  shows "proj r (Eps (\<lambda>x. x \<in> X)) = X"
    1.56  unfolding proj_def
    1.57  proof auto
    1.58    fix x assume x: "x \<in> X"
    1.59 -  thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
    1.60 +  thus "(Eps (\<lambda>x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
    1.61  next
    1.62 -  fix x assume "(Eps (%x. x \<in> X),x) \<in> r"
    1.63 +  fix x assume "(Eps (\<lambda>x. x \<in> X),x) \<in> r"
    1.64    thus "x \<in> X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast
    1.65  qed
    1.66  
    1.67 -definition univ where "univ f X == f (Eps (%x. x \<in> X))"
    1.68 +definition univ where "univ f X == f (Eps (\<lambda>x. x \<in> X))"
    1.69  
    1.70  lemma univ_commute:
    1.71  assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
    1.72  shows "(univ f) (proj r x) = f x"
    1.73  proof (unfold univ_def)
    1.74    have prj: "proj r x \<in> A//r" using x proj_preserves by fast
    1.75 -  hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
    1.76 -  moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
    1.77 -  ultimately have "(x, Eps (%y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
    1.78 -  thus "f (Eps (%y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
    1.79 +  hence "Eps (\<lambda>y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
    1.80 +  moreover have "proj r (Eps (\<lambda>y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
    1.81 +  ultimately have "(x, Eps (\<lambda>y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
    1.82 +  thus "f (Eps (\<lambda>y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
    1.83  qed
    1.84  
    1.85  lemma univ_preserves:
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Oct 26 20:59:36 2016 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Oct 26 22:40:28 2016 +0200
     2.3 @@ -66,8 +66,6 @@
     2.4       fp_bnf_sugar: fp_bnf_sugar,
     2.5       fp_co_induct_sugar: fp_co_induct_sugar option}
     2.6  
     2.7 -  val transfer_plugin: string
     2.8 -
     2.9    val co_induct_of: 'a list -> 'a
    2.10    val strong_co_induct_of: 'a list -> 'a
    2.11  
    2.12 @@ -313,8 +311,6 @@
    2.13     fp_bnf_sugar: fp_bnf_sugar,
    2.14     fp_co_induct_sugar: fp_co_induct_sugar option};
    2.15  
    2.16 -val transfer_plugin = Plugin_Name.declare_setup @{binding transfer};
    2.17 -
    2.18  fun co_induct_of (i :: _) = i;
    2.19  fun strong_co_induct_of [_, s] = s;
    2.20  
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Oct 26 20:59:36 2016 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Oct 26 22:40:28 2016 +0200
     3.3 @@ -464,7 +464,7 @@
     3.4          val goals =
     3.5            @{map 8} mk_goals un_folds xtors ss pre_fold_maps fp_abss fp_reps abss reps;
     3.6  
     3.7 -        val fp_un_folds = map (mk_pointfree lthy) (of_fp_res #xtor_un_fold_thms);
     3.8 +        val fp_un_folds = map (mk_pointfree2 lthy) (of_fp_res #xtor_un_fold_thms);
     3.9  
    3.10          val simps = flat [simp_thms, un_fold_defs, map_defs, fp_un_folds,
    3.11            fp_un_fold_o_maps, map_thms, Rep_o_Abss];
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Oct 26 20:59:36 2016 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Oct 26 22:40:28 2016 +0200
     4.3 @@ -862,7 +862,7 @@
     4.4      val xtor_co_rec_o_map_thms = if forall is_none absT_info_opts
     4.5        then
     4.6          mk_xtor_co_iter_o_map_thms fp true m xtor_co_rec_unique_thm
     4.7 -          (map (mk_pointfree lthy) xtor_maps) (map (mk_pointfree lthy) xtor_co_rec_thms)
     4.8 +          (map (mk_pointfree2 lthy) xtor_maps) (map (mk_pointfree2 lthy) xtor_co_rec_thms)
     4.9            sym_map_comp0s map_cong0s
    4.10        else
    4.11          replicate n refl (* FIXME *);
     5.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Oct 26 20:59:36 2016 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Oct 26 22:40:28 2016 +0200
     5.3 @@ -1676,7 +1676,7 @@
     5.4        dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_notes, dtor_Jset_induct_thms, lthy) =
     5.5        if m = 0 then
     5.6          (timer, replicate n DEADID_bnf,
     5.7 -        map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids),
     5.8 +        map_split (`(mk_pointfree2 lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids),
     5.9          mk_dtor_map_unique_DEADID_thm (),
    5.10          replicate n [],
    5.11          map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs,
    5.12 @@ -2532,7 +2532,7 @@
    5.13        ||>> mk_Frees "S" activephiTs;
    5.14  
    5.15      val dtor_unfold_o_Jmap_thms = mk_xtor_co_iter_o_map_thms Greatest_FP false m
    5.16 -      dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms)
    5.17 +      dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree2 lthy) dtor_unfold_thms)
    5.18        sym_map_comps map_cong0s;
    5.19  
    5.20      val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
     6.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Oct 26 20:59:36 2016 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Oct 26 22:40:28 2016 +0200
     6.3 @@ -1303,7 +1303,7 @@
     6.4          ctor_Irel_thms, Ibnf_notes, lthy) =
     6.5        if m = 0 then
     6.6          (timer, replicate n DEADID_bnf,
     6.7 -        map_split (`(mk_pointfree lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_ids),
     6.8 +        map_split (`(mk_pointfree2 lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_ids),
     6.9          mk_ctor_map_unique_DEADID_thm (),
    6.10          replicate n [], map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, [], lthy)
    6.11        else let
    6.12 @@ -1791,7 +1791,7 @@
    6.13        ||>> mk_Frees "IR" activeIphiTs;
    6.14  
    6.15      val ctor_fold_o_Imap_thms = mk_xtor_co_iter_o_map_thms Least_FP false m ctor_fold_unique_thm
    6.16 -      ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s;
    6.17 +      ctor_Imap_o_thms (map (mk_pointfree2 lthy) ctor_fold_thms) sym_map_comps map_cong0s;
    6.18  
    6.19      val Irels = if m = 0 then map HOLogic.eq_const Ts
    6.20        else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
     7.1 --- a/src/HOL/Tools/BNF/bnf_tactics.ML	Wed Oct 26 20:59:36 2016 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_tactics.ML	Wed Oct 26 22:40:28 2016 +0200
     7.3 @@ -17,7 +17,7 @@
     7.4    val mk_rotate_eq_tac: Proof.context -> (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list ->
     7.5      ''a list -> int -> tactic
     7.6  
     7.7 -  val mk_pointfree: Proof.context -> thm -> thm
     7.8 +  val mk_pointfree2: Proof.context -> thm -> thm
     7.9  
    7.10    val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
    7.11    val mk_Abs_inj_thm: thm -> thm
    7.12 @@ -47,14 +47,13 @@
    7.13  fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0];
    7.14  fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt o the_default [0];
    7.15  
    7.16 -
    7.17  (*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*)
    7.18 -fun mk_pointfree ctxt thm = thm
    7.19 +fun mk_pointfree2 ctxt thm = thm
    7.20    |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
    7.21    |> apply2 (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp)
    7.22    |> mk_Trueprop_eq
    7.23    |> (fn goal => Goal.prove_sorry ctxt [] [] goal
    7.24 -    (K (rtac ctxt @{thm ext} 1 THEN
    7.25 +    (K (rtac ctxt ext 1 THEN
    7.26          unfold_thms_tac ctxt ([o_apply, unfold_thms ctxt [o_apply] (mk_sym thm)]) THEN
    7.27          rtac ctxt refl 1)))
    7.28    |> Thm.close_derivation;
    7.29 @@ -67,7 +66,6 @@
    7.30    (Abs_inj_thm RS @{thm bijI'});
    7.31  
    7.32  
    7.33 -
    7.34  (* General tactic generators *)
    7.35  
    7.36  (*applies assoc rule to the lhs of an equation as long as possible*)
     8.1 --- a/src/HOL/Tools/BNF/bnf_util.ML	Wed Oct 26 20:59:36 2016 +0200
     8.2 +++ b/src/HOL/Tools/BNF/bnf_util.ML	Wed Oct 26 22:40:28 2016 +0200
     8.3 @@ -10,6 +10,8 @@
     8.4    include CTR_SUGAR_UTIL
     8.5    include BNF_FP_REC_SUGAR_UTIL
     8.6  
     8.7 +  val transfer_plugin: string
     8.8 +
     8.9    val unflatt: 'a list list list -> 'b list -> 'b list list list
    8.10    val unflattt: 'a list list list list -> 'b list -> 'b list list list list
    8.11  
    8.12 @@ -121,6 +123,9 @@
    8.13  open Ctr_Sugar_Util
    8.14  open BNF_FP_Rec_Sugar_Util
    8.15  
    8.16 +val transfer_plugin = Plugin_Name.declare_setup @{binding transfer};
    8.17 +
    8.18 +
    8.19  (* Library proper *)
    8.20  
    8.21  fun unfla0 xs = fold_map (fn _ => fn (c :: cs) => (c, cs)) xs;
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Oct 26 20:59:36 2016 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Oct 26 22:40:28 2016 +0200
     9.3 @@ -458,7 +458,7 @@
     9.4  fun all_facts ctxt generous ho_atp keywords add_ths chained css =
     9.5    let
     9.6      val thy = Proof_Context.theory_of ctxt
     9.7 -    val transfer = Global_Theory.transfer_theories thy;
     9.8 +    val transfer = Global_Theory.transfer_theories thy
     9.9      val global_facts = Global_Theory.facts_of thy
    9.10      val is_too_complex =
    9.11        if generous orelse fact_count global_facts >= max_facts_for_complex_check then K false
    9.12 @@ -528,7 +528,7 @@
    9.13    in
    9.14      (* The single-theorem names go before the multiple-theorem ones (e.g., "xxx" vs. "xxx(3)"), so
    9.15         that single names are preferred when both are available. *)
    9.16 -    `I []
    9.17 +    ([], [])
    9.18      |> add_facts false fold local_facts (unnamed_locals @ named_locals)
    9.19      |> add_facts true Facts.fold_static global_facts global_facts
    9.20      |> op @