# HG changeset patch # User wenzelm # Date 1347454885 -7200 # Node ID 77c7ce7609cd866f48423c730ce6ce50f470320f # Parent f4169aa675130f4b53aa4fbfcf063c3afd78f8c1# Parent 4f28543ae7fab0da82484139e9e024fd5b8b71cb merged diff -r 4f28543ae7fa -r 77c7ce7609cd src/HOL/Codatatype/BNF_Def.thy --- a/src/HOL/Codatatype/BNF_Def.thy Wed Sep 12 14:46:13 2012 +0200 +++ b/src/HOL/Codatatype/BNF_Def.thy Wed Sep 12 15:01:25 2012 +0200 @@ -51,7 +51,7 @@ moreover have "f1 (fst a') = f2 (snd a')" using a' unfolding csquare_def thePull_def by auto ultimately show "\ ja'. ?phi a' ja'" - using assms unfolding wppull_def by auto + using assms unfolding wppull_def by blast qed lemma wpull_wppull: @@ -64,7 +64,7 @@ then obtain a' where a': "a' \ A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'" using wp unfolding wpull_def by blast show "\a\A. e1 (p1 a) = e1 b1 \ e2 (p2 a) = e2 b2" - apply(rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto + apply (rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto qed lemma wppull_id: "\wpull UNIV UNIV UNIV f1 f2 p1 p2; e1 = id; e2 = id\ \ @@ -87,8 +87,7 @@ definition "pick_middle P Q a c = (SOME b. (a,b) \ P \ (b,c) \ Q)" lemma pick_middle: -assumes "(a,c) \ P O Q" -shows "(a, pick_middle P Q a c) \ P \ (pick_middle P Q a c, c) \ Q" +"(a,c) \ P O Q \ (a, pick_middle P Q a c) \ P \ (pick_middle P Q a c, c) \ Q" unfolding pick_middle_def apply(rule someI_ex) using assms unfolding relcomp_def by auto @@ -96,7 +95,8 @@ definition sndO where "sndO P Q ac = (pick_middle P Q (fst ac) (snd ac), snd ac)" lemma fstO_in: "ac \ P O Q \ fstO P Q ac \ P" -by (metis assms fstO_def pick_middle surjective_pairing) +unfolding fstO_def +by (subst (asm) surjective_pairing) (rule pick_middle[THEN conjunct1]) lemma fst_fstO: "fst bc = (fst \ fstO P Q) bc" unfolding comp_def fstO_def by simp @@ -105,11 +105,12 @@ unfolding comp_def sndO_def by simp lemma sndO_in: "ac \ P O Q \ sndO P Q ac \ Q" -by (metis assms sndO_def pick_middle surjective_pairing) +unfolding sndO_def +by (subst (asm) surjective_pairing) (rule pick_middle[THEN conjunct2]) lemma csquare_fstO_sndO: "csquare (P O Q) snd fst (fstO P Q) (sndO P Q)" -unfolding csquare_def fstO_def sndO_def using pick_middle by auto +unfolding csquare_def fstO_def sndO_def using pick_middle by simp lemma wppull_fstO_sndO: shows "wppull (P O Q) P Q snd fst fst snd (fstO P Q) (sndO P Q)" diff -r 4f28543ae7fa -r 77c7ce7609cd src/HOL/Codatatype/BNF_FP.thy --- a/src/HOL/Codatatype/BNF_FP.thy Wed Sep 12 14:46:13 2012 +0200 +++ b/src/HOL/Codatatype/BNF_FP.thy Wed Sep 12 15:01:25 2012 +0200 @@ -80,16 +80,24 @@ lemma obj_one_pointE: "\x. s = x \ P \ P" by blast +lemma obj_sumE_f': +"\\x. s = f (Inl x) \ P; \x. s = f (Inr x) \ P\ \ s = f x \ P" +by (cases x) blast+ + lemma obj_sumE_f: "\\x. s = f (Inl x) \ P; \x. s = f (Inr x) \ P\ \ \x. s = f x \ P" -by (metis sum.exhaust) +by (rule allI) (rule obj_sumE_f') lemma obj_sumE: "\\x. s = Inl x \ P; \x. s = Inr x \ P\ \ P" by (cases s) auto +lemma obj_sum_step': +"\\x. s = f (Inr (Inl x)) \ P; \x. s = f (Inr (Inr x)) \ P\ \ s = f (Inr x) \ P" +by (cases x) blast+ + lemma obj_sum_step: - "\\x. s = f (Inr (Inl x)) \ P; \x. s = f (Inr (Inr x)) \ P\ \ \x. s = f (Inr x) \ P" -by (metis obj_sumE) +"\\x. s = f (Inr (Inl x)) \ P; \x. s = f (Inr (Inr x)) \ P\ \ \x. s = f (Inr x) \ P" +by (rule allI) (rule obj_sum_step') lemma sum_case_if: "sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)" diff -r 4f28543ae7fa -r 77c7ce7609cd src/HOL/Codatatype/BNF_GFP.thy --- a/src/HOL/Codatatype/BNF_GFP.thy Wed Sep 12 14:46:13 2012 +0200 +++ b/src/HOL/Codatatype/BNF_GFP.thy Wed Sep 12 15:01:25 2012 +0200 @@ -278,12 +278,10 @@ (* pick according to the weak pullback *) definition pickWP_pred where -"pickWP_pred A p1 p2 b1 b2 a \ - a \ A \ p1 a = b1 \ p2 a = b2" +"pickWP_pred A p1 p2 b1 b2 a \ a \ A \ p1 a = b1 \ p2 a = b2" definition pickWP where -"pickWP A p1 p2 b1 b2 \ - SOME a. pickWP_pred A p1 p2 b1 b2 a" +"pickWP A p1 p2 b1 b2 \ SOME a. pickWP_pred A p1 p2 b1 b2 a" lemma pickWP_pred: assumes "wpull A B1 B2 f1 f2 p1 p2" and @@ -323,9 +321,6 @@ lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \ f (x # xs) = f2 x xs (f xs)" by auto -lemma sum_case_cong: "p = q \ sum_case f g p = sum_case f g q" -by simp - lemma not_arg_cong_Inr: "x \ y \ Inr x \ Inr y" by simp diff -r 4f28543ae7fa -r 77c7ce7609cd src/HOL/Codatatype/BNF_LFP.thy --- a/src/HOL/Codatatype/BNF_LFP.thy Wed Sep 12 14:46:13 2012 +0200 +++ b/src/HOL/Codatatype/BNF_LFP.thy Wed Sep 12 15:01:25 2012 +0200 @@ -61,7 +61,8 @@ then obtain g where g: "ALL b : B. g b : A \ f (g b) = b" using bchoice[of B ?phi] by blast hence gg: "ALL b : f ` A. g b : A \ f (g b) = b" using f by blast - have gf: "inver g f A" unfolding inver_def by (metis gg imageI inj_f the_inv_into_f_f) + have gf: "inver g f A" unfolding inver_def + by (metis (no_types) gg imageI[of _ A f] the_inv_into_f_f[OF inj_f]) moreover have "g ` B \ A \ inver f g B" using g unfolding inver_def by blast moreover have "A \ g ` B" proof safe @@ -123,13 +124,16 @@ unfolding bij_betw_def inver_def by auto lemma bij_betwI: "\bij_betw g B A; inver g f A; inver f g B\ \ bij_betw f A B" -by (metis bij_betw_iff_ex bij_betw_imageE) +by (drule bij_betw_imageE, unfold bij_betw_iff_ex) blast lemma bij_betwI': "\\x y. \x \ X; y \ X\ \ (f x = f y) = (x = y); \x. x \ X \ f x \ Y; \y. y \ Y \ \x \ X. y = f x\ \ bij_betw f X Y" -unfolding bij_betw_def inj_on_def by auto (metis rev_image_eqI) +unfolding bij_betw_def inj_on_def +apply (rule conjI) + apply blast +by (erule thin_rl) blast lemma surj_fun_eq: assumes surj_on: "f ` X = UNIV" and eq_on: "\x \ X. (g1 o f) x = (g2 o f) x" @@ -192,7 +196,15 @@ then obtain y where y: "y \ Field r" "\x \ X. (x \ y \ (x, y) \ r)" by blast then obtain z where z: "z \ Field r" "x \ z \ (x, z) \ r" "y \ z \ (y, z) \ r" using Cinfinite_limit2[OF _ y(1) insert(5), of x] insert(4) by blast - show ?case by (metis Card_order_trans insert(5) insertE y(2) z) + show ?case + apply (intro bexI ballI) + apply (erule insertE) + apply hypsubst + apply (rule z(2)) + using Card_order_trans[OF insert(5)[THEN conjunct2]] y(2) z(3) + apply blast + apply (rule z(1)) + done qed lemma insert_subsetI: "\x \ A; X \ A\ \ insert x X \ A" diff -r 4f28543ae7fa -r 77c7ce7609cd src/HOL/Codatatype/Tools/bnf_def.ML --- a/src/HOL/Codatatype/Tools/bnf_def.ML Wed Sep 12 14:46:13 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML Wed Sep 12 15:01:25 2012 +0200 @@ -482,7 +482,6 @@ val bd_CnotzeroN = "bd_Cnotzero"; val collect_set_naturalN = "collect_set_natural"; val in_bdN = "in_bd"; -val in_congN = "in_cong"; val in_monoN = "in_mono"; val in_relN = "in_rel"; val map_idN = "map_id"; @@ -490,9 +489,7 @@ val map_compN = "map_comp"; val map_comp'N = "map_comp'"; val map_congN = "map_cong"; -val map_wppullN = "map_wppull"; val map_wpullN = "map_wpull"; -val rel_congN = "rel_cong"; val rel_IdN = "rel_Id"; val rel_GrN = "rel_Gr"; val rel_converseN = "rel_converse"; diff -r 4f28543ae7fa -r 77c7ce7609cd src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 14:46:13 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 15:01:25 2012 +0200 @@ -59,12 +59,8 @@ fun resort_tfree S (TFree (s, _)) = TFree (s, S); -fun retype_free T (Free (s, _)) = Free (s, T); - val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs)); -fun mk_predT T = T --> HOLogic.boolT; - fun mk_id T = Const (@{const_name id}, T --> T); fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs)); @@ -704,10 +700,11 @@ val datatype_cmd = define_datatype Typedecl.read_constraint Syntax.parse_typ Syntax.read_term; -val parse_opt_binding_colon = Scan.optional (Parse.binding --| @{keyword ":"}) no_binder +val parse_binding_colon = Parse.binding --| @{keyword ":"}; +val parse_opt_binding_colon = Scan.optional parse_binding_colon no_binder; val parse_ctr_arg = - @{keyword "("} |-- parse_opt_binding_colon -- Parse.typ --| @{keyword ")"} || + @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} || (Parse.typ >> pair no_binder); val parse_defaults = diff -r 4f28543ae7fa -r 77c7ce7609cd src/HOL/Codatatype/Tools/bnf_fp_util.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Wed Sep 12 14:46:13 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Wed Sep 12 15:01:25 2012 +0200 @@ -78,9 +78,15 @@ val mk_set_minimalN: int -> string val mk_set_inductN: int -> string + val mk_bundle_name: binding list -> string + val split_conj_thm: thm -> thm list val split_conj_prems: int -> thm -> thm + val retype_free: typ -> term -> term + + val mk_predT: typ -> typ; + val mk_sumTN: typ list -> typ val mk_sumTN_balanced: typ list -> typ @@ -207,6 +213,12 @@ val set_inclN = "set_incl" val set_set_inclN = "set_set_incl" +val mk_bundle_name = space_implode "_" o map Binding.name_of; + +fun mk_predT T = T --> HOLogic.boolT; + +fun retype_free T (Free (s, _)) = Free (s, T); + fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T'); fun dest_sumTN 1 T = [T] @@ -319,7 +331,7 @@ fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold lthy = let - val name = fold_rev (fn b => fn s => Binding.name_of b ^ s) bs ""; + val name = mk_bundle_name bs; fun qualify i bind = let val namei = if i > 0 then name ^ string_of_int i else name; in diff -r 4f28543ae7fa -r 77c7ce7609cd src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Wed Sep 12 14:46:13 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Wed Sep 12 15:01:25 2012 +0200 @@ -64,7 +64,7 @@ val ks = 1 upto n; val m = live - n (*passive, if 0 don't generate a new bnf*); val ls = 1 upto m; - val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs ""); + val b = Binding.name (mk_bundle_name bs); (* TODO: check if m, n etc are sane *) @@ -1675,7 +1675,7 @@ map (fn i => map (fn i' => split_conj_thm (if n = 1 then set_rv_Lev' RS mk_conjunctN n i RS mp else set_rv_Lev' RS mk_conjunctN n i RS mp RSN - (2, @{thm sum_case_cong} RS @{thm subst[of _ _ "%x. x"]}) RS + (2, @{thm sum_case_weak_cong} RS @{thm subst[of _ _ "%x. x"]}) RS (mk_sum_casesN n i' RS @{thm subst[of _ _ "%x. x"]}))) ks) ks end; @@ -1873,7 +1873,7 @@ ||>> mk_Frees "f" coiter_fTs ||>> mk_Frees "g" coiter_fTs ||>> mk_Frees "s" corec_sTs - ||>> mk_Frees "phi" (map (fn T => T --> T --> HOLogic.boolT) Ts); + ||>> mk_Frees "phi" (map (fn T => T --> mk_predT T) Ts); fun unf_bind i = Binding.suffix_name ("_" ^ unfN) (nth bs (i - 1)); val unf_name = Binding.name_of o unf_bind; @@ -2291,7 +2291,7 @@ val pTs = map2 (curry op -->) passiveXs passiveCs; val uTs = map2 (curry op -->) Ts Ts'; val JRTs = map2 (curry mk_relT) passiveAs passiveBs; - val JphiTs = map2 (fn T => fn U => T --> U --> HOLogic.boolT) passiveAs passiveBs; + val JphiTs = map2 (fn T => fn U => T --> mk_predT U) passiveAs passiveBs; val prodTs = map2 (curry HOLogic.mk_prodT) Ts Ts'; val B1Ts = map HOLogic.mk_setT passiveAs; val B2Ts = map HOLogic.mk_setT passiveBs; @@ -2309,7 +2309,7 @@ ||>> mk_Frees "u" uTs ||>> mk_Frees' "b" Ts' ||>> mk_Frees' "b" Ts' - ||>> mk_Freess "phi" (map (fn T => map (fn U => T --> U --> HOLogic.boolT) Ts) passiveAs) + ||>> mk_Freess "phi" (map (fn T => map (fn U => T --> mk_predT U) Ts) passiveAs) ||>> mk_Frees "R" JRTs ||>> mk_Frees "phi" JphiTs ||>> mk_Frees "B1" B1Ts diff -r 4f28543ae7fa -r 77c7ce7609cd src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Wed Sep 12 14:46:13 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Wed Sep 12 15:01:25 2012 +0200 @@ -143,6 +143,7 @@ val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym; val ssubst_id = @{thm ssubst[of _ _ "%x. x"]}; val subst_id = @{thm subst[of _ _ "%x. x"]}; +val sum_case_weak_cong = @{thm sum_case_weak_cong}; val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]}; fun mk_coalg_set_tac coalg_def = @@ -701,7 +702,7 @@ CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI, rtac (@{thm append_Cons} RS arg_cong RS trans), - rtac (rv_Cons RS trans), etac (@{thm sum_case_cong} RS arg_cong RS trans), + rtac (rv_Cons RS trans), etac (sum_case_weak_cong RS arg_cong RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans), atac]) ks]) rv_Conss) @@ -873,7 +874,7 @@ rtac exI, rtac conjI, (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev' else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN' - etac (@{thm sum_case_cong} RS trans) THEN' rtac (mk_sum_casesN n i)), + etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)), EVERY' (map2 (fn set_natural => fn set_rv_Lev => EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans), rtac trans_fun_cong_image_id_id_apply, @@ -897,7 +898,7 @@ rtac exI, rtac conjI, (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev' else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN' - etac (@{thm sum_case_cong} RS trans) THEN' rtac (mk_sum_casesN n i)), + etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)), EVERY' (map2 (fn set_natural => fn set_rv_Lev => EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans), rtac trans_fun_cong_image_id_id_apply, @@ -946,13 +947,13 @@ ((map_comp_id, (map_cong, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) = EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def, rtac (@{thm if_P} RS - (if n = 1 then map_arg_cong else @{thm sum_case_cong}) RS trans), + (if n = 1 then map_arg_cong else sum_case_weak_cong) RS trans), rtac (@{thm list.size(3)} RS arg_cong RS trans RS equalityD2 RS set_mp), rtac Lev_0, rtac @{thm singletonI}, CONVERSION (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt), if n = 1 then K all_tac - else (rtac (@{thm sum_case_cong} RS trans) THEN' + else (rtac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)), rtac (map_comp_id RS trans), rtac (map_cong OF replicate m refl), EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd => @@ -990,7 +991,7 @@ CONVERSION (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt), if n = 1 then K all_tac - else rtac @{thm sum_case_cong} THEN' rtac (mk_sum_casesN n i' RS trans), + else rtac sum_case_weak_cong THEN' rtac (mk_sum_casesN n i' RS trans), SELECT_GOAL (Local_Defs.unfold_tac ctxt [from_to_sbd]), rtac refl, rtac refl]) ks to_sbd_injs from_to_sbds)]; diff -r 4f28543ae7fa -r 77c7ce7609cd src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Wed Sep 12 14:46:13 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Wed Sep 12 15:01:25 2012 +0200 @@ -33,7 +33,7 @@ val n = length bnfs; (*active*) val ks = 1 upto n; val m = live - n; (*passive, if 0 don't generate a new bnf*) - val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs ""); + val b = Binding.name (mk_bundle_name bs); (* TODO: check if m, n etc are sane *) @@ -792,7 +792,7 @@ ||>> mk_Frees' "x" init_FTs ||>> mk_Frees "f" init_fTs ||>> mk_Frees "f" init_fTs - ||>> mk_Frees "phi" (replicate n (initT --> HOLogic.boolT)); + ||>> mk_Frees "phi" (replicate n (mk_predT initT)); val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss) (HOLogic.mk_conj (HOLogic.mk_eq (iidx, @@ -977,20 +977,21 @@ val rec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts_rev; val rec_fsts = map (Term.subst_atomic_types (activeBs ~~ Ts)) fsts; - val (((((((((((Izs, (Izs1, Izs1')), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')), - (iter_f, iter_f')), fs), phis), phi2s), rec_ss), names_lthy) = names_lthy - |> mk_Frees "z" Ts - ||>> mk_Frees' "z1" Ts + val (((((((((Izs1, Izs1'), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')), + (iter_f, iter_f')), fs), rec_ss), names_lthy) = names_lthy + |> mk_Frees' "z1" Ts ||>> mk_Frees' "z2" Ts' ||>> mk_Frees' "x" FTs ||>> mk_Frees "y" FTs' ||>> mk_Freess' "z" setFTss ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") iterT ||>> mk_Frees "f" fTs - ||>> mk_Frees "phi" (map (fn T => T --> HOLogic.boolT) Ts) - ||>> mk_Frees "phi" (map2 (fn T => fn U => T --> U --> HOLogic.boolT) Ts Ts') ||>> mk_Frees "s" rec_sTs; + val Izs = map2 retype_free Ts zs; + val phis = map2 retype_free (map mk_predT Ts) init_phis; + val phi2s = map2 retype_free (map2 (fn T => fn T' => T --> mk_predT T') Ts Ts') init_phis; + fun fld_bind i = Binding.suffix_name ("_" ^ fldN) (nth bs (i - 1)); val fld_name = Binding.name_of o fld_bind; val fld_def_bind = rpair [] o Thm.def_binding o fld_bind; @@ -1353,7 +1354,7 @@ val XTs = mk_Ts passiveXs; val YTs = mk_Ts passiveYs; val IRTs = map2 (curry mk_relT) passiveAs passiveBs; - val IphiTs = map2 (fn T => fn U => T --> U --> HOLogic.boolT) passiveAs passiveBs; + val IphiTs = map2 (fn T => fn U => T --> mk_predT U) passiveAs passiveBs; val (((((((((((((((fs, fs'), fs_copy), us), B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')), IRs), Iphis),