# HG changeset patch # User traytel # Date 1367930842 -7200 # Node ID 7c43b8df0f5d1b72234e56596e88ea0493275a62 # Parent 596baae88a88a1aec050b182ec2cf6287f9a3f1d tuned diff -r 596baae88a88 -r 7c43b8df0f5d src/HOL/BNF/BNF.thy --- a/src/HOL/BNF/BNF.thy Tue May 07 14:22:54 2013 +0200 +++ b/src/HOL/BNF/BNF.thy Tue May 07 14:47:22 2013 +0200 @@ -13,8 +13,8 @@ imports More_BNFs begin -hide_const (open) Gr collect fsts snds setl setr - convol thePull pick_middle fstO sndO csquare inver +hide_const (open) Gr Grp collect fsts snds setl setr + convol thePull pick_middle pick_middlep fstO sndO fstOp sndOp csquare inver image2 relImage relInvImage prefCl PrefCl Succ Shift shift end diff -r 596baae88a88 -r 7c43b8df0f5d src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Tue May 07 14:22:54 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def.ML Tue May 07 14:47:22 2013 +0200 @@ -662,7 +662,6 @@ val CB' = mk_bnf_T Bs' CA; val CC' = mk_bnf_T Cs CA; val CRs' = mk_bnf_T RTs CA; - val CA'CB' = HOLogic.mk_prodT (CA', CB'); val bnf_map_AsAs = mk_bnf_map As' As'; val bnf_map_AsBs = mk_bnf_map As' Bs'; @@ -674,15 +673,14 @@ val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits; val pre_names_lthy = lthy; - val (((((((((((((((((((((((fs, gs), hs), p), (x, x')), (y, y')), (z, z')), zs), As), + val ((((((((((((((((((((((fs, gs), hs), x), y), (z, z')), zs), As), As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss), names_lthy) = pre_names_lthy |> mk_Frees "f" (map2 (curry (op -->)) As' Bs') ||>> mk_Frees "g" (map2 (curry (op -->)) Bs' Cs) ||>> mk_Frees "h" (map2 (curry (op -->)) As' Ts) - ||>> yield_singleton (mk_Frees "p") CA'CB' - ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "x") CA' - ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "y") CB' + ||>> yield_singleton (mk_Frees "x") CA' + ||>> yield_singleton (mk_Frees "y") CB' ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "z") CRs' ||>> mk_Frees "z" As' ||>> mk_Frees "A" (map HOLogic.mk_setT As') @@ -1022,7 +1020,7 @@ Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'), HOLogic.eq_const CA')) - (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id axioms)) + (K (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id axioms))) |> Thm.close_derivation end; @@ -1083,16 +1081,13 @@ val in_rel = Lazy.lazy mk_in_rel; - val predicate2_cong = @{thm predicate2_cong}; - val mem_Collect_etc = @{thms fst_conv mem_Collect_eq prod.cases snd_conv}; - fun mk_rel_flip () = let val rel_conversep_thm = Lazy.force rel_conversep; val cts = map (SOME o certify lthy) Rs; val rel_conversep_thm' = cterm_instantiate_pos cts rel_conversep_thm; in - unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS predicate2_cong) + unfold_thms lthy @{thms conversep_iff} (rel_conversep_thm' RS @{thm predicate2_cong}) |> singleton (Proof_Context.export names_lthy pre_names_lthy) end; diff -r 596baae88a88 -r 7c43b8df0f5d src/HOL/BNF/Tools/bnf_def_tactics.ML --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Tue May 07 14:22:54 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Tue May 07 14:47:22 2013 +0200 @@ -18,7 +18,7 @@ val mk_rel_Grp_tac: thm list -> thm -> thm -> thm -> thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic - val mk_rel_eq_tac: int -> thm -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic + val mk_rel_eq_tac: int -> thm -> thm -> thm -> tactic val mk_rel_OO_tac: thm list -> thm -> thm -> thm -> thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic val mk_in_rel_tac: thm list -> {prems: 'b, context: Proof.context} -> tactic @@ -104,7 +104,7 @@ @{thms fst_convol snd_convol} [map_id', refl])] 1 end; -fun mk_rel_eq_tac n rel_Grp rel_cong map_id {context = ctxt, prems = _} = +fun mk_rel_eq_tac n rel_Grp rel_cong map_id = (EVERY' (rtac (rel_cong RS trans) :: replicate n (rtac @{thm eq_alt})) THEN' rtac (rel_Grp RSN (2, @{thm box_equals[OF _ sym sym[OF eq_alt]]})) THEN' (if n = 0 then rtac refl diff -r 596baae88a88 -r 7c43b8df0f5d src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Tue May 07 14:22:54 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Tue May 07 14:47:22 2013 +0200 @@ -59,8 +59,6 @@ let val timer = time (Timer.startRealTimer ()); - val note_all = Config.get lthy bnf_note_all; - val live = live_of_bnf (hd bnfs); val n = length bnfs; (*active*) val ks = 1 upto n; @@ -228,7 +226,6 @@ val set_map'ss = map set_map'_of_bnf bnfs; val rel_congs = map rel_cong_of_bnf bnfs; val rel_converseps = map rel_conversep_of_bnf bnfs; - val rel_defs = map rel_def_of_bnf bnfs; val rel_Grps = map rel_Grp_of_bnf bnfs; val rel_eqs = map rel_eq_of_bnf bnfs; val rel_monos = map rel_mono_of_bnf bnfs; @@ -2315,7 +2312,6 @@ val p2Ts = map2 (curry op -->) passiveXs passiveBs; 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 mk_pred2T passiveAs passiveBs; val prodTs = map2 (curry HOLogic.mk_prodT) Ts Ts'; val B1Ts = map HOLogic.mk_setT passiveAs; @@ -2324,8 +2320,8 @@ val XTs = mk_Ts passiveXs; val YTs = mk_Ts passiveYs; - val ((((((((((((((((((((fs, fs'), fs_copy), gs), us), - (Jys, Jys')), (Jys_copy, Jys'_copy)), dtor_set_induct_phiss), JRs), Jphis), + val (((((((((((((((((((fs, fs'), fs_copy), gs), us), + (Jys, Jys')), (Jys_copy, Jys'_copy)), dtor_set_induct_phiss), Jphis), B1s), B2s), AXs), f1s), f2s), p1s), p2s), ps), (ys, ys')), (ys_copy, ys'_copy)), names_lthy) = names_lthy |> mk_Frees' "f" fTs @@ -2335,7 +2331,6 @@ ||>> mk_Frees' "b" Ts' ||>> mk_Frees' "b" Ts' ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs) - ||>> mk_Frees "r" JRTs ||>> mk_Frees "P" JphiTs ||>> mk_Frees "B1" B1Ts ||>> mk_Frees "B2" B2Ts @@ -2912,7 +2907,6 @@ val in_rels = map in_rel_of_bnf bnfs; val in_Jrels = map in_rel_of_bnf Jbnfs; - val Jrel_defs = map rel_def_of_bnf Jbnfs; val folded_dtor_map_thms = map fold_maps dtor_map_thms; val folded_dtor_set_thmss = map (map fold_sets) dtor_set_thmss; diff -r 596baae88a88 -r 7c43b8df0f5d src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Tue May 07 14:22:54 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Tue May 07 14:47:22 2013 +0200 @@ -30,8 +30,6 @@ let val timer = time (Timer.startRealTimer ()); - val note_all = Config.get lthy bnf_note_all; - val live = live_of_bnf (hd bnfs); val n = length bnfs; (*active*) val ks = 1 upto n; @@ -1380,11 +1378,10 @@ val AXTs = map HOLogic.mk_setT passiveXs; val XTs = mk_Ts passiveXs; val YTs = mk_Ts passiveYs; - val IRTs = map2 (curry mk_relT) passiveAs passiveBs; val IphiTs = map2 mk_pred2T passiveAs passiveBs; - val (((((((((((((((fs, fs'), fs_copy), us), - B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')), IRs), Iphis), + val ((((((((((((((fs, fs'), fs_copy), us), + B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')), Iphis), names_lthy) = names_lthy |> mk_Frees' "f" fTs ||>> mk_Frees "f" fTs @@ -1398,7 +1395,6 @@ ||>> mk_Frees "p1" p1Ts ||>> mk_Frees "p2" p2Ts ||>> mk_Frees' "y" passiveAs - ||>> mk_Frees "S" IRTs ||>> mk_Frees "R" IphiTs; val map_FTFT's = map2 (fn Ds => @@ -1753,8 +1749,6 @@ val in_rels = map in_rel_of_bnf bnfs; val in_Irels = map in_rel_of_bnf Ibnfs; - val rel_defs = map rel_def_of_bnf bnfs; - val Irel_defs = map rel_def_of_bnf Ibnfs; val ctor_set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss; val ctor_set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss; diff -r 596baae88a88 -r 7c43b8df0f5d src/HOL/BNF/Tools/bnf_util.ML --- a/src/HOL/BNF/Tools/bnf_util.ML Tue May 07 14:22:54 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_util.ML Tue May 07 14:47:22 2013 +0200 @@ -375,7 +375,8 @@ fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts)); fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list; -fun retype_free T (Free (s, _)) = Free (s, T); +fun retype_free T (Free (s, _)) = Free (s, T) + | retype_free _ t = raise TERM ("retype_free", [t]); (** Types **)