# HG changeset patch # User traytel # Date 1406805597 -7200 # Node ID 18b8a8f1031343a5438a1d92332ea8937715d79e # Parent a297879fe5b8d74cafd26fc0eed8d0ec97014eb8 simplified tactics slightly diff -r a297879fe5b8 -r 18b8a8f10313 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Jul 31 00:45:55 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Jul 31 13:19:57 2014 +0200 @@ -223,7 +223,7 @@ val rel_congs = map rel_cong_of_bnf bnfs; val rel_converseps = map rel_conversep_of_bnf bnfs; val rel_Grps = map rel_Grp_of_bnf bnfs; - val rel_OOs = map rel_OO_of_bnf bnfs; + val le_rel_OOs = map le_rel_OO_of_bnf bnfs; val in_rels = map in_rel_of_bnf bnfs; val timer = time (timer "Extracted terms & thms"); @@ -589,7 +589,7 @@ HOLogic.mk_Trueprop (mk_bis Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's)); in Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl)) - (K (mk_bis_O_tac lthy m bis_rel_thm rel_congs rel_OOs)) + (K (mk_bis_O_tac lthy m bis_rel_thm rel_congs le_rel_OOs)) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy) end; @@ -2260,7 +2260,7 @@ val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals); in Goal.prove_sorry lthy [] [] goal - (K (mk_le_rel_OO_tac Jrel_coinduct_thm dtor_Jrel_thms rel_OOs)) + (K (mk_le_rel_OO_tac Jrel_coinduct_thm dtor_Jrel_thms le_rel_OOs)) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy) end; diff -r a297879fe5b8 -r 18b8a8f10313 src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Jul 31 00:45:55 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Jul 31 13:19:57 2014 +0200 @@ -277,21 +277,21 @@ REPEAT_DETERM o etac allE, rtac @{thm conversepI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converseps)] 1; -fun mk_bis_O_tac ctxt m bis_rel rel_congs rel_OOs = +fun mk_bis_O_tac ctxt m bis_rel rel_congs le_rel_OOs = EVERY' [rtac (bis_rel RS iffD2), REPEAT_DETERM o dtac (bis_rel RS iffD1), REPEAT_DETERM o etac conjE, rtac conjI, CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs, - CONJ_WRAP' (fn (rel_cong, rel_OO) => + CONJ_WRAP' (fn (rel_cong, le_rel_OO) => EVERY' [rtac allI, rtac allI, rtac impI, rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}), REPEAT_DETERM_N m o rtac @{thm eq_OO}, REPEAT_DETERM_N (length rel_congs) o rtac @{thm relcompp_in_rel}, - rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}), + rtac (le_rel_OO RS @{thm predicate2D}), etac @{thm relcompE}, REPEAT_DETERM o dtac prod_injectD, etac conjE, hyp_subst_tac ctxt, REPEAT_DETERM o etac allE, rtac @{thm relcomppI}, - etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_OOs)] 1; + etac mp, atac, etac mp, atac]) (rel_congs ~~ le_rel_OOs)] 1; fun mk_bis_Gr_tac ctxt bis_rel rel_Grps mor_images morEs coalg_ins = unfold_thms_tac ctxt (bis_rel :: @{thm eq_alt} :: @{thm in_rel_Gr} :: rel_Grps) THEN @@ -898,14 +898,14 @@ EVERY' (map rtac [@{thm UNION_Cinfinite_bound}, ordIso_ordLeq_trans, @{thm card_of_nat}, @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite]) 1; -fun mk_le_rel_OO_tac coinduct rel_Jrels rel_OOs = - EVERY' (rtac coinduct :: map2 (fn rel_Jrel => fn rel_OO => +fun mk_le_rel_OO_tac coinduct rel_Jrels le_rel_OOs = + EVERY' (rtac coinduct :: map2 (fn rel_Jrel => fn le_rel_OO => let val Jrel_imp_rel = rel_Jrel RS iffD1; in - EVERY' [rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}), etac @{thm relcomppE}, + EVERY' [rtac (le_rel_OO RS @{thm predicate2D}), etac @{thm relcomppE}, rtac @{thm relcomppI}, etac Jrel_imp_rel, etac Jrel_imp_rel] end) - rel_Jrels rel_OOs) 1; + rel_Jrels le_rel_OOs) 1; fun mk_wit_tac ctxt n dtor_ctors dtor_set wit coind_wits = ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN diff -r a297879fe5b8 -r 18b8a8f10313 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Jul 31 00:45:55 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Jul 31 13:19:57 2014 +0200 @@ -168,7 +168,7 @@ val map_ids = map map_id_of_bnf bnfs; val set_mapss = map set_map_of_bnf bnfs; val rel_mono_strongs = map rel_mono_strong_of_bnf bnfs; - val rel_OOs = map rel_OO_of_bnf bnfs; + val le_rel_OOs = map le_rel_OO_of_bnf bnfs; val timer = time (timer "Extracted terms & thms"); @@ -1691,7 +1691,7 @@ in Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms - ctor_Irel_thms rel_mono_strongs rel_OOs) + ctor_Irel_thms rel_mono_strongs le_rel_OOs) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy) end; diff -r a297879fe5b8 -r 18b8a8f10313 src/HOL/Tools/BNF/bnf_lfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Jul 31 00:45:55 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Jul 31 13:19:57 2014 +0200 @@ -582,17 +582,17 @@ (induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1 end; -fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strongs rel_OOs = +fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strongs le_rel_OOs = EVERY' (rtac induct :: - map4 (fn nchotomy => fn Irel => fn rel_mono => fn rel_OO => + map4 (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO => EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}), REPEAT_DETERM_N 2 o dtac (Irel RS iffD1), rtac (Irel RS iffD2), - rtac rel_mono, rtac (rel_OO RS @{thm predicate2_eqD} RS iffD2), + rtac rel_mono, rtac (le_rel_OO RS @{thm predicate2D}), rtac @{thm relcomppI}, atac, atac, REPEAT_DETERM_N m o EVERY' [rtac ballI, rtac ballI, rtac impI, atac], - REPEAT_DETERM_N (length rel_OOs) o + REPEAT_DETERM_N (length le_rel_OOs) o EVERY' [rtac ballI, rtac ballI, Goal.assume_rule_tac ctxt]]) - ctor_nchotomys ctor_Irels rel_mono_strongs rel_OOs) 1; + ctor_nchotomys ctor_Irels rel_mono_strongs le_rel_OOs) 1; (* BNF tactics *)