--- 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 \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
by simp
-lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z" by simp
-lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z" by simp
+lemma fst_diag_id: "(fst \<circ> (\<lambda>x. (x, x))) z = id z" by simp
+lemma snd_diag_id: "(snd \<circ> (\<lambda>x. (x, x))) z = id z" by simp
lemma fst_diag_fst: "fst o ((\<lambda>x. (x, x)) o fst) = fst" by auto
lemma snd_diag_fst: "snd o ((\<lambda>x. (x, x)) o fst) = fst" by auto
@@ -201,16 +201,16 @@
lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> 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) \<Longrightarrow> f 0 = f1"
+lemma rec_nat_0_imp: "f = rec_nat f1 (\<lambda>n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
by auto
-lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
+lemma rec_nat_Suc_imp: "f = rec_nat f1 (\<lambda>n rec. f2 n rec) \<Longrightarrow> 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) \<Longrightarrow> f [] = f1"
+lemma rec_list_Nil_imp: "f = rec_list f1 (\<lambda>x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
by auto
-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)"
+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)"
by auto
lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
@@ -235,40 +235,40 @@
subsection \<open>Equivalence relations, quotients, and Hilbert's choice\<close>
lemma equiv_Eps_in:
-"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
+"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (\<lambda>x. x \<in> X) \<in> 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 \<in> A//r"
- shows "Eps (%x. x \<in> X) \<in> A"
+ shows "Eps (\<lambda>x. x \<in> X) \<in> 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 \<in> A//r"
- shows "proj r (Eps (%x. x \<in> X)) = X"
+ shows "proj r (Eps (\<lambda>x. x \<in> X)) = X"
unfolding proj_def
proof auto
fix x assume x: "x \<in> X"
- thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
+ thus "(Eps (\<lambda>x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
next
- fix x assume "(Eps (%x. x \<in> X),x) \<in> r"
+ fix x assume "(Eps (\<lambda>x. x \<in> X),x) \<in> r"
thus "x \<in> 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 \<in> X))"
+definition univ where "univ f X == f (Eps (\<lambda>x. x \<in> X))"
lemma univ_commute:
assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
shows "(univ f) (proj r x) = f x"
proof (unfold univ_def)
have prj: "proj r x \<in> A//r" using x proj_preserves by fast
- hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
- moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
- ultimately have "(x, Eps (%y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
- thus "f (Eps (%y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
+ hence "Eps (\<lambda>y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
+ moreover have "proj r (Eps (\<lambda>y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
+ ultimately have "(x, Eps (\<lambda>y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
+ thus "f (Eps (\<lambda>y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
qed
lemma univ_preserves:
--- 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;
--- 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];
--- 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 *);
--- 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;
--- 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;
--- 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*)
--- 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;
--- 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 @