--- a/NEWS Mon Oct 08 23:29:07 2012 +0200
+++ b/NEWS Tue Oct 09 11:51:06 2012 +0200
@@ -62,13 +62,15 @@
*** HOL ***
-* Class "comm_monoid_diff" formalised properties of bounded
+* Theorem UN_o generalized to SUP_comp. INCOMPATIBILITY.
+
+* Class "comm_monoid_diff" formalises properties of bounded
subtraction, with natural numbers and multisets as typical instances.
* Theory "Library/Option_ord" provides instantiation of option type
to lattice type classes.
-* New combinator "Option.these" with type "'a option set => 'a option".
+* New combinator "Option.these" with type "'a option set => 'a set".
* Renamed theory Library/List_Prefix to Library/Sublist.
INCOMPATIBILITY. Related changes are:
--- a/src/Doc/Codegen/Further.thy Mon Oct 08 23:29:07 2012 +0200
+++ b/src/Doc/Codegen/Further.thy Tue Oct 09 11:51:06 2012 +0200
@@ -166,7 +166,7 @@
lemma %quote powers_power:
"powers xs \<circ> power x = power x \<circ> powers xs"
by (induct xs)
- (simp_all del: o_apply id_apply add: o_assoc [symmetric],
+ (simp_all del: o_apply id_apply add: comp_assoc,
simp del: o_apply add: o_assoc power_commute)
lemma %quote powers_rev:
--- a/src/HOL/Finite_Set.thy Mon Oct 08 23:29:07 2012 +0200
+++ b/src/HOL/Finite_Set.thy Tue Oct 09 11:51:06 2012 +0200
@@ -793,7 +793,7 @@
with Suc have hyp: "f y ^^ h y \<circ> f x = f x \<circ> f y ^^ h y"
by auto
from Suc h_def have "g y = Suc (h y)" by simp
- then show ?case by (simp add: o_assoc [symmetric] hyp)
+ then show ?case by (simp add: comp_assoc hyp)
(simp add: o_assoc comp_fun_commute)
qed
def h \<equiv> "\<lambda>z. if z = x then g x - 1 else g z"
@@ -803,7 +803,7 @@
with False h_def have hyp2: "f y ^^ g y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ g y" by simp
from Suc h_def have "g x = Suc (h x)" by simp
then show ?case by (simp del: funpow.simps add: funpow_Suc_right o_assoc hyp2)
- (simp add: o_assoc [symmetric] hyp1)
+ (simp add: comp_assoc hyp1)
qed
qed
qed
@@ -1507,7 +1507,7 @@
assumes "finite A"
shows "f x \<circ> F A = F A \<circ> f x"
using assms by (induct A)
- (simp, simp del: o_apply add: o_assoc, simp del: o_apply add: o_assoc [symmetric] comp_fun_commute)
+ (simp, simp del: o_apply add: o_assoc, simp del: o_apply add: comp_assoc comp_fun_commute)
lemma commute_left_comp':
assumes "finite A"
@@ -1518,14 +1518,14 @@
assumes "finite A" and "finite B"
shows "F B \<circ> F A = F A \<circ> F B"
using assms by (induct A)
- (simp_all add: o_assoc, simp add: o_assoc [symmetric] comp_fun_commute')
+ (simp_all add: o_assoc, simp add: comp_assoc comp_fun_commute')
lemma commute_left_comp'':
assumes "finite A" and "finite B"
shows "F B \<circ> (F A \<circ> g) = F A \<circ> (F B \<circ> g)"
using assms by (simp add: o_assoc comp_fun_commute'')
-lemmas comp_fun_commutes = o_assoc [symmetric] comp_fun_commute commute_left_comp
+lemmas comp_fun_commutes = comp_assoc comp_fun_commute commute_left_comp
comp_fun_commute' commute_left_comp' comp_fun_commute'' commute_left_comp''
lemma union_inter:
--- a/src/HOL/Fun.thy Mon Oct 08 23:29:07 2012 +0200
+++ b/src/HOL/Fun.thy Tue Oct 09 11:51:06 2012 +0200
@@ -41,34 +41,41 @@
notation (HTML output)
comp (infixl "\<circ>" 55)
-lemma o_apply [simp]: "(f o g) x = f (g x)"
-by (simp add: comp_def)
-
-lemma o_assoc: "f o (g o h) = f o g o h"
-by (simp add: comp_def)
+lemma comp_apply [simp]: "(f o g) x = f (g x)"
+ by (simp add: comp_def)
-lemma id_o [simp]: "id o g = g"
-by (simp add: comp_def)
+lemma comp_assoc: "(f o g) o h = f o (g o h)"
+ by (simp add: fun_eq_iff)
-lemma o_id [simp]: "f o id = f"
-by (simp add: comp_def)
+lemma id_comp [simp]: "id o g = g"
+ by (simp add: fun_eq_iff)
-lemma o_eq_dest:
+lemma comp_id [simp]: "f o id = f"
+ by (simp add: fun_eq_iff)
+
+lemma comp_eq_dest:
"a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
- by (simp only: comp_def) (fact fun_cong)
+ by (simp add: fun_eq_iff)
-lemma o_eq_elim:
+lemma comp_eq_elim:
"a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
- by (erule meta_mp) (fact o_eq_dest)
+ by (simp add: fun_eq_iff)
-lemma image_compose: "(f o g) ` r = f`(g`r)"
-by (simp add: comp_def, blast)
-
-lemma vimage_compose: "(g \<circ> f) -` x = f -` (g -` x)"
+lemma image_comp:
+ "(f o g) ` r = f ` (g ` r)"
by auto
-lemma UN_o: "UNION A (g o f) = UNION (f`A) g"
-by (unfold comp_def, blast)
+lemma vimage_comp:
+ "(g \<circ> f) -` x = f -` (g -` x)"
+ by auto
+
+lemma INF_comp:
+ "INFI A (g \<circ> f) = INFI (f ` A) g"
+ by (simp add: INF_def image_comp)
+
+lemma SUP_comp:
+ "SUPR A (g \<circ> f) = SUPR (f ` A) g"
+ by (simp add: SUP_def image_comp)
subsection {* The Forward Composition Operator @{text fcomp} *}
@@ -735,10 +742,6 @@
by (rule the_inv_into_f_f)
-text{*compatibility*}
-lemmas o_def = comp_def
-
-
subsection {* Cantor's Paradox *}
lemma Cantors_paradox [no_atp]:
@@ -806,7 +809,19 @@
by (simp_all add: fun_eq_iff)
enriched_type vimage
- by (simp_all add: fun_eq_iff vimage_compose)
+ by (simp_all add: fun_eq_iff vimage_comp)
+
+text {* Legacy theorem names *}
+
+lemmas o_def = comp_def
+lemmas o_apply = comp_apply
+lemmas o_assoc = comp_assoc [symmetric]
+lemmas id_o = id_comp
+lemmas o_id = comp_id
+lemmas o_eq_dest = comp_eq_dest
+lemmas o_eq_elim = comp_eq_elim
+lemmas image_compose = image_comp
+lemmas vimage_compose = vimage_comp
end
--- a/src/HOL/Hilbert_Choice.thy Mon Oct 08 23:29:07 2012 +0200
+++ b/src/HOL/Hilbert_Choice.thy Tue Oct 09 11:51:06 2012 +0200
@@ -144,7 +144,7 @@
by (simp add: inj_iff)
lemma o_inv_o_cancel[simp]: "inj f ==> g o inv f o f = g"
-by (simp add: o_assoc[symmetric])
+by (simp add: comp_assoc)
lemma inv_into_image_cancel[simp]:
"inj_on f A ==> S <= A ==> inv_into A f ` f ` S = S"
--- a/src/HOL/Library/Permutations.thy Mon Oct 08 23:29:07 2012 +0200
+++ b/src/HOL/Library/Permutations.thy Tue Oct 09 11:51:06 2012 +0200
@@ -292,7 +292,7 @@
next
case (comp_Suc n p a b m q)
have th: "Suc n + m = Suc (n + m)" by arith
- show ?case unfolding th o_assoc[symmetric]
+ show ?case unfolding th comp_assoc
apply (rule swapidseq.comp_Suc) using comp_Suc.hyps(2)[OF comp_Suc.prems] comp_Suc.hyps(3) by blast+
qed
@@ -302,7 +302,7 @@
lemma swapidseq_endswap: "swapidseq n p \<Longrightarrow> a \<noteq> b ==> swapidseq (Suc n) (p o Fun.swap a b id)"
apply (induct n p rule: swapidseq.induct)
using swapidseq_swap[of a b]
- by (auto simp add: o_assoc[symmetric] intro: swapidseq.comp_Suc)
+ by (auto simp add: comp_assoc intro: swapidseq.comp_Suc)
lemma swapidseq_inverse_exists: "swapidseq n p ==> \<exists>q. swapidseq n q \<and> p o q = id \<and> q o p = id"
proof(induct n p rule: swapidseq.induct)
@@ -418,7 +418,7 @@
have th2: "swapidseq (n - 1) (Fun.swap a z id o q)" "n \<noteq> 0" by blast+
have th: "Suc n - 1 = Suc (n - 1)" using th2(2) by auto
have ?case unfolding cdqm(2) H o_assoc th
- apply (simp only: Suc_not_Zero simp_thms o_assoc[symmetric])
+ apply (simp only: Suc_not_Zero simp_thms comp_assoc)
apply (rule comp_Suc)
using th2 H apply blast+
done}
@@ -734,7 +734,7 @@
apply (rule permutes_compose)
using q apply auto
apply (rule_tac x = "x o inv q" in exI)
-by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o o_assoc[symmetric])
+by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o comp_assoc)
lemma permutes_in_seg: "p permutes {1 ..n} \<Longrightarrow> i \<in> {1..n} ==> 1 <= p i \<and> p i <= n"
@@ -770,7 +770,7 @@
proof-
fix p r
assume "p permutes S" and r:"r permutes S" and rp: "q \<circ> p = q \<circ> r"
- hence "inv q o q o p = inv q o q o r" by (simp add: o_assoc[symmetric])
+ hence "inv q o q o p = inv q o q o r" by (simp add: comp_assoc)
with permutes_inj[OF q, unfolded inj_iff]
show "p = r" by simp
--- a/src/HOL/List.thy Mon Oct 08 23:29:07 2012 +0200
+++ b/src/HOL/List.thy Tue Oct 09 11:51:06 2012 +0200
@@ -2398,7 +2398,7 @@
assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
and x: "x \<in> set xs"
shows "fold f xs = fold f (remove1 x xs) \<circ> f x"
- using assms by (induct xs) (auto simp add: o_assoc [symmetric])
+ using assms by (induct xs) (auto simp add: comp_assoc)
lemma fold_cong [fundef_cong]:
"a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Oct 08 23:29:07 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Oct 09 11:51:06 2012 +0200
@@ -833,14 +833,151 @@
step :: aux subst depth nextp proof
in aux [] 0 (1, 1) end
-fun string_for_proof ctxt0 type_enc lam_trans i n =
+
+(** Type annotations **)
+
+fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s
+ | post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s
+ | post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s
+ | post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s
+ | post_traverse_term_type' f env (Abs (x, T1, b)) s =
+ let
+ val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s
+ in f (Abs (x, T1, b')) (T1 --> T2) s' end
+ | post_traverse_term_type' f env (u $ v) s =
+ let
+ val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
+ val ((v', s''), _) = post_traverse_term_type' f env v s'
+ in f (u' $ v') T s'' end
+
+fun post_traverse_term_type f s t =
+ post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst
+fun post_fold_term_type f s t =
+ post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
+
+(* Data structures, orders *)
+val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
+
+structure Var_Set_Tab = Table(
+ type key = indexname list
+ val ord = list_ord Term_Ord.fast_indexname_ord)
+
+(* (1) Generalize Types *)
+fun generalize_types ctxt t =
+ t |> map_types (fn _ => dummyT)
+ |> Syntax.check_term
+ (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
+
+(* (2) Typing-spot Table *)
+local
+fun key_of_atype (TVar (idxn, _)) =
+ Ord_List.insert Term_Ord.fast_indexname_ord idxn
+ | key_of_atype _ = I
+fun key_of_type T = fold_atyps key_of_atype T []
+fun update_tab t T (tab, pos) =
+ (case key_of_type T of
+ [] => tab
+ | key =>
+ let val cost = (size_of_typ T, (size_of_term t, pos)) in
+ case Var_Set_Tab.lookup tab key of
+ NONE => Var_Set_Tab.update_new (key, cost) tab
+ | SOME old_cost =>
+ (case cost_ord (cost, old_cost) of
+ LESS => Var_Set_Tab.update (key, cost) tab
+ | _ => tab)
+ end,
+ pos + 1)
+in
+val typing_spot_table =
+ post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
+end
+
+(* (3) Reverse-Greedy *)
+fun reverse_greedy typing_spot_tab =
let
- val ctxt = ctxt0
-(* FIXME: Implement proper handling of type constraints:
- |> Config.put show_free_types false
- |> Config.put show_types false
- |> Config.put show_sorts false
-*)
+ fun update_count z =
+ fold (fn tvar => fn tab =>
+ let val c = Vartab.lookup tab tvar |> the_default 0 in
+ Vartab.update (tvar, c + z) tab
+ end)
+ fun superfluous tcount =
+ forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
+ fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) =
+ if superfluous tcount tvars then (spots, update_count ~1 tvars tcount)
+ else (spot :: spots, tcount)
+ val (typing_spots, tvar_count_tab) =
+ Var_Set_Tab.fold
+ (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
+ typing_spot_tab ([], Vartab.empty)
+ |>> sort_distinct (rev_order o cost_ord o pairself snd)
+ in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end
+
+(* (4) Introduce Annotations *)
+fun introduce_annotations thy spots t t' =
+ let
+ val get_types = post_fold_term_type (K cons) []
+ fun match_types tp =
+ fold (Sign.typ_match thy) (op ~~ (pairself get_types tp)) Vartab.empty
+ fun unica' b x [] = if b then [x] else []
+ | unica' b x (y :: ys) =
+ if x = y then unica' false x ys
+ else unica' true y ys |> b ? cons x
+ fun unica ord xs =
+ case sort ord xs of x :: ys => unica' true x ys | [] => []
+ val add_all_tfree_namesT = fold_atyps (fn TFree (x, _) => cons x | _ => I)
+ fun erase_unica_tfrees env =
+ let
+ val unica =
+ Vartab.fold (add_all_tfree_namesT o snd o snd) env []
+ |> unica fast_string_ord
+ val erase_unica = map_atyps
+ (fn T as TFree (s, _) =>
+ if Ord_List.member fast_string_ord unica s then dummyT else T
+ | T => T)
+ in Vartab.map (K (apsnd erase_unica)) env end
+ val env = match_types (t', t) |> erase_unica_tfrees
+ fun get_annot env (TFree _) = (false, (env, dummyT))
+ | get_annot env (T as TVar (v, S)) =
+ let val T' = Envir.subst_type env T in
+ if T' = dummyT then (false, (env, dummyT))
+ else (true, (Vartab.update (v, (S, dummyT)) env, T'))
+ end
+ | get_annot env (Type (S, Ts)) =
+ (case fold_rev (fn T => fn (b, (env, Ts)) =>
+ let
+ val (b', (env', T)) = get_annot env T
+ in (b orelse b', (env', T :: Ts)) end)
+ Ts (false, (env, [])) of
+ (true, (env', Ts)) => (true, (env', Type (S, Ts)))
+ | (false, (env', _)) => (false, (env', dummyT)))
+ fun post1 _ T (env, cp, ps as p :: ps', annots) =
+ if p <> cp then
+ (env, cp + 1, ps, annots)
+ else
+ let val (_, (env', T')) = get_annot env T in
+ (env', cp + 1, ps', (p, T') :: annots)
+ end
+ | post1 _ _ accum = accum
+ val (_, _, _, annots) = post_fold_term_type post1 (env, 0, spots, []) t'
+ fun post2 t _ (cp, annots as (p, T) :: annots') =
+ if p <> cp then (t, (cp + 1, annots))
+ else (Type.constraint T t, (cp + 1, annots'))
+ | post2 t _ x = (t, x)
+ in post_traverse_term_type post2 (0, rev annots) t |> fst end
+
+(* (5) Annotate *)
+fun annotate_types ctxt t =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val t' = generalize_types ctxt t
+ val typing_spots =
+ t' |> typing_spot_table
+ |> reverse_greedy
+ |> sort int_ord
+ in introduce_annotations thy typing_spots t t' end
+
+fun string_for_proof ctxt type_enc lam_trans i n =
+ let
fun fix_print_mode f x =
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
(print_mode_value ())) f x
@@ -856,7 +993,9 @@
if member (op =) qs Show then "thus" else "hence"
else
if member (op =) qs Show then "show" else "have")
- val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
+ val do_term =
+ maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
+ o annotate_types ctxt
val reconstr = Metis (type_enc, lam_trans)
fun do_facts (ls, ss) =
reconstructor_command reconstr 1 1 [] 0
--- a/src/HOL/Word/Misc_Typedef.thy Mon Oct 08 23:29:07 2012 +0200
+++ b/src/HOL/Word/Misc_Typedef.thy Tue Oct 09 11:51:06 2012 +0200
@@ -102,7 +102,7 @@
"norm o norm = norm ==> (fr o norm = norm o fr) =
(norm o fr o norm = fr o norm & norm o fr o norm = norm o fr)"
apply safe
- apply (simp_all add: o_assoc [symmetric])
+ apply (simp_all add: comp_assoc)
apply (simp_all add: o_assoc)
done
@@ -192,7 +192,7 @@
apply (fold eq_norm')
apply safe
prefer 2
- apply (simp add: o_assoc [symmetric])
+ apply (simp add: comp_assoc)
apply (rule ext)
apply (drule fun_cong)
apply simp
@@ -208,7 +208,7 @@
apply (rule fns3 [THEN iffD1])
prefer 3
apply (rule fns2 [THEN iffD1])
- apply (simp_all add: o_assoc [symmetric])
+ apply (simp_all add: comp_assoc)
apply (simp_all add: o_assoc)
done