# HG changeset patch # User traytel # Date 1375956045 -7200 # Node ID f8fca14c8cbd6d10f80059c7b1f11771c74b3fbd # Parent 6c89225ddeba84dfe094af039185952b2037e0d3 tuned diff -r 6c89225ddeba -r f8fca14c8cbd src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Wed Aug 07 23:20:11 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 08 12:00:45 2013 +0200 @@ -326,7 +326,7 @@ val coalg_prem = HOLogic.mk_Trueprop (mk_coalg As Bs ss); val coalg_in_thms = map (fn i => - coalg_def RS @{thm subst[of _ _ "%x. x"]} RS mk_conjunctN n i RS bspec) ks + coalg_def RS iffD1 RS mk_conjunctN n i RS bspec) ks val coalg_set_thmss = let @@ -922,9 +922,9 @@ |> Thm.close_derivation; val lsbis_incl_thms = map (fn i => sbis_lsbis_thm RS - (bis_def RS @{thm subst[of _ _ "%x. x"]} RS conjunct1 RS mk_conjunctN n i)) ks; + (bis_def RS iffD1 RS conjunct1 RS mk_conjunctN n i)) ks; val lsbisE_thms = map (fn i => (mk_specN 2 (sbis_lsbis_thm RS - (bis_def RS @{thm subst[of _ _ "%x. x"]} RS conjunct2 RS mk_conjunctN n i))) RS mp) ks; + (bis_def RS iffD1 RS conjunct2 RS mk_conjunctN n i))) RS mp) ks; val incl_lsbis_thms = let @@ -1482,8 +1482,8 @@ 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_weak_cong} RS @{thm subst[of _ _ "%x. x"]}) RS - (mk_sum_casesN n i' RS @{thm subst[of _ _ "%x. x"]}))) ks) ks + (2, @{thm sum_case_weak_cong} RS iffD1) RS + (mk_sum_casesN n i' RS iffD1))) ks) ks end; val set_Lev_thmsss = @@ -1838,7 +1838,7 @@ end; val (dtor_unfold_unique_thms, dtor_unfold_unique_thm) = `split_conj_thm (split_conj_prems n - (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS unfold_unique_mor_thm)); + (mor_UNIV_thm RS iffD2 RS unfold_unique_mor_thm)); val unfold_dtor_thms = map (fn thm => mor_id_thm RS thm RS sym) unfold_unique_mor_thms; @@ -2005,7 +2005,7 @@ val dtor_corec_unique_thms = split_conj_thm (split_conj_prems n - (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS corec_unique_mor_thm) + (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm) |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @ map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]}); diff -r 6c89225ddeba -r f8fca14c8cbd src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Wed Aug 07 23:20:11 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 08 12:00:45 2013 +0200 @@ -1135,7 +1135,7 @@ val ctor_fold_unique_thms = split_conj_thm (mk_conjIN n RS - (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS fold_unique_mor_thm)) + (mor_UNIV_thm RS iffD2 RS fold_unique_mor_thm)) val fold_ctor_thms = map (fn thm => (mor_incl_thm OF replicate n @{thm subset_UNIV}) RS thm RS sym) @@ -1296,7 +1296,7 @@ val ctor_rec_unique_thms = split_conj_thm (split_conj_prems n - (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS rec_unique_mor_thm) + (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm) |> Local_Defs.unfold lthy (@{thms convol_o o_id id_o o_assoc[symmetric] fst_convol} @ map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]}); diff -r 6c89225ddeba -r f8fca14c8cbd src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Wed Aug 07 23:20:11 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 08 12:00:45 2013 +0200 @@ -245,7 +245,7 @@ REPEAT_DETERM o rtac subset_UNIV, REPEAT_DETERM_N n o (set_tac thms)]) (set_map's ~~ alg_sets); in - (rtac (iso_alt RS @{thm ssubst[of _ _ "%x. x"]}) THEN' + (rtac (iso_alt RS iffD2) THEN' etac copy_str THEN' REPEAT_DETERM o atac THEN' rtac conjI THEN' stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN' CONJ_WRAP' (K atac) alg_sets) 1 @@ -372,7 +372,7 @@ etac @{thm underS_I}, atac, atac]])) set_bds]; in - (rtac (alg_def RS @{thm ssubst[of _ _ "%x. x"]}) THEN' + (rtac (alg_def RS iffD2) THEN' CONJ_WRAP' mk_conjunct_tac (set_bdss ~~ (min_algs ~~ min_alg_defs))) 1 end;