# HG changeset patch # User wenzelm # Date 1349776266 -7200 # Node ID fb88f0e4c710c867ac5b7aba51053ce24ae61744 # Parent 6f02b893dd87338bb9661ceb7459f7260de9e968# Parent dd6fc7c9504a7269186e521c374008ffc5282ea8 merged diff -r dd6fc7c9504a -r fb88f0e4c710 NEWS --- 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: diff -r dd6fc7c9504a -r fb88f0e4c710 src/Doc/Codegen/Further.thy --- 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 \ power x = power x \ 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: diff -r dd6fc7c9504a -r fb88f0e4c710 src/HOL/Finite_Set.thy --- 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 \ f x = f x \ 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 \ "\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 \ f x ^^ h x = f x ^^ h x \ 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 \ F A = F A \ 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 \ F A = F A \ 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 \ (F A \ g) = F A \ (F B \ 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: diff -r dd6fc7c9504a -r fb88f0e4c710 src/HOL/Fun.thy --- 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 "\" 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 \ 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 \ ((\v. a (b v) = c (d v)) \ R) \ 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 \ 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 \ f) -` x = f -` (g -` x)" + by auto + +lemma INF_comp: + "INFI A (g \ f) = INFI (f ` A) g" + by (simp add: INF_def image_comp) + +lemma SUP_comp: + "SUPR A (g \ 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 diff -r dd6fc7c9504a -r fb88f0e4c710 src/HOL/Hilbert_Choice.thy --- 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" diff -r dd6fc7c9504a -r fb88f0e4c710 src/HOL/Library/Permutations.thy --- 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 \ a \ 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 ==> \q. swapidseq n q \ p o q = id \ 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 \ 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} \ i \ {1..n} ==> 1 <= p i \ p i <= n" @@ -770,7 +770,7 @@ proof- fix p r assume "p permutes S" and r:"r permutes S" and rp: "q \ p = q \ 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 diff -r dd6fc7c9504a -r fb88f0e4c710 src/HOL/List.thy --- 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: "\x y. x \ set xs \ y \ set xs \ f x \ f y = f y \ f x" and x: "x \ set xs" shows "fold f xs = fold f (remove1 x xs) \ 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 \ xs = ys \ (\x. x \ set xs \ f x = g x) diff -r dd6fc7c9504a -r fb88f0e4c710 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- 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 diff -r dd6fc7c9504a -r fb88f0e4c710 src/HOL/Word/Misc_Typedef.thy --- 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