# HG changeset patch # User blanchet # Date 1348244717 -7200 # Node ID d4859efc1096414b34e4b5f6565ccf089427106c # Parent 191d9384966ac8aaa8037ca9ed0037dc19de2c42 renamed "rel_simp" to "dtor_rel" and similarly for "srel" diff -r 191d9384966a -r d4859efc1096 src/HOL/BNF/Tools/bnf_fp.ML --- a/src/HOL/BNF/Tools/bnf_fp.ML Fri Sep 21 18:25:17 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp.ML Fri Sep 21 18:25:17 2012 +0200 @@ -39,15 +39,16 @@ val disc_corecsN: string val dtorN: string val dtor_coinductN: string - val dtor_unfoldN: string - val dtor_unfold_uniqueN: string - val dtor_unfoldsN: string + val dtor_relN: string val dtor_corecN: string val dtor_corecsN: string val dtor_exhaustN: string val dtor_ctorN: string val dtor_injectN: string val dtor_strong_coinductN: string + val dtor_unfoldN: string + val dtor_unfold_uniqueN: string + val dtor_unfoldsN: string val exhaustN: string val foldN: string val foldsN: string @@ -65,7 +66,6 @@ val recN: string val recsN: string val rel_coinductN: string - val rel_simpN: string val rel_strong_coinductN: string val rvN: string val sel_unfoldsN: string @@ -74,7 +74,7 @@ val set_set_inclN: string val simpsN: string val srel_coinductN: string - val srel_simpN: string + val dtor_srelN: string val srel_strong_coinductN: string val strTN: string val str_initN: string @@ -225,8 +225,8 @@ val rel_coinductN = relN ^ "_" ^ coinductN val srel_coinductN = srelN ^ "_" ^ coinductN val simpN = "_simp"; -val srel_simpN = srelN ^ simpN; -val rel_simpN = relN ^ simpN; +val dtor_srelN = dtorN ^ "_" ^ srelN +val dtor_relN = dtorN ^ "_" ^ relN val strongN = "strong_" val dtor_strong_coinductN = dtorN ^ "_" ^ strongN ^ coinductN val rel_strong_coinductN = relN ^ "_" ^ strongN ^ coinductN diff -r 191d9384966a -r d4859efc1096 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Fri Sep 21 18:25:17 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Fri Sep 21 18:25:17 2012 +0200 @@ -2899,7 +2899,7 @@ val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss; val folded_set_simp_thmss' = transpose folded_set_simp_thmss; - val Jsrel_simp_thms = + val dtor_Jsrel_thms = let fun mk_goal Jz Jz' dtor dtor' JsrelR srelR = fold_rev Logic.all (Jz :: Jz' :: JRs) (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JsrelR), @@ -2910,24 +2910,24 @@ fn map_simp => fn set_simps => fn dtor_inject => fn dtor_ctor => fn set_naturals => fn set_incls => fn set_set_inclss => Skip_Proof.prove lthy [] [] goal - (K (mk_srel_simp_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps + (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps dtor_inject dtor_ctor set_naturals set_incls set_set_inclss)) |> Thm.close_derivation) ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss' dtor_inject_thms dtor_ctor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss end; - val Jrel_simp_thms = + val dtor_Jrel_thms = let fun mk_goal Jz Jz' dtor dtor' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis) (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (dtor $ Jz) $ (dtor' $ Jz'))); val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis; in - map3 (fn goal => fn srel_def => fn Jsrel_simp => + map3 (fn goal => fn srel_def => fn dtor_Jsrel => Skip_Proof.prove lthy [] [] goal - (mk_rel_simp_tac srel_def Jrel_defs Jsrel_defs Jsrel_simp) + (mk_dtor_rel_tac srel_def Jrel_defs Jsrel_defs dtor_Jsrel) |> Thm.close_derivation) - goals srel_defs Jsrel_simp_thms + goals srel_defs dtor_Jsrel_thms end; val timer = time (timer "additional properties"); @@ -2941,11 +2941,11 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); val Jbnf_notes = - [(map_simpsN, map single folded_map_simp_thms), - (rel_simpN, map single Jrel_simp_thms), + [(dtor_relN, map single dtor_Jrel_thms), + (dtor_srelN, map single dtor_Jsrel_thms), + (map_simpsN, map single folded_map_simp_thms), (set_inclN, set_incl_thmss), - (set_set_inclN, map flat set_set_incl_thmsss), - (srel_simpN, map single Jsrel_simp_thms)] @ + (set_set_inclN, map flat set_set_incl_thmsss)] @ map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => diff -r 191d9384966a -r d4859efc1096 src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Fri Sep 21 18:25:17 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Fri Sep 21 18:25:17 2012 +0200 @@ -38,6 +38,8 @@ val mk_corec_tac: int -> thm list -> thm -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic val mk_dtor_coinduct_tac: int -> int list -> thm -> thm -> tactic + val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> + thm list -> thm list -> thm list list -> tactic val mk_dtor_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm -> thm -> thm -> tactic val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> @@ -109,8 +111,6 @@ val mk_srel_coinduct_tac: 'a list -> thm -> thm -> tactic val mk_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm -> thm list -> thm list -> tactic - val mk_srel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> - thm list -> thm list -> thm list list -> tactic val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list -> cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list -> thm list list -> thm -> thm list list -> tactic @@ -1494,7 +1494,7 @@ ALLGOALS (TRY o FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE]) -fun mk_srel_simp_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps dtor_inject dtor_ctor +fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps dtor_inject dtor_ctor set_naturals set_incls set_set_inclss = let val m = length set_incls; diff -r 191d9384966a -r d4859efc1096 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Fri Sep 21 18:25:17 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Fri Sep 21 18:25:17 2012 +0200 @@ -1742,7 +1742,7 @@ val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss; val folded_set_simp_thmss' = transpose folded_set_simp_thmss; - val Isrel_simp_thms = + val dtor_Isrel_thms = let fun mk_goal xF yF ctor ctor' IsrelR srelR = fold_rev Logic.all (xF :: yF :: IRs) (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (ctor $ xF, ctor' $ yF), IsrelR), @@ -1753,24 +1753,24 @@ fn map_simp => fn set_simps => fn ctor_inject => fn ctor_dtor => fn set_naturals => fn set_incls => fn set_set_inclss => Skip_Proof.prove lthy [] [] goal - (K (mk_srel_simp_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps + (K (mk_dtor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject ctor_dtor set_naturals set_incls set_set_inclss)) |> Thm.close_derivation) ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss' ctor_inject_thms ctor_dtor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss end; - val Irel_simp_thms = + val dtor_Irel_thms = let fun mk_goal xF yF ctor ctor' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis) (mk_Trueprop_eq (Ipredphi $ (ctor $ xF) $ (ctor' $ yF), predphi $ xF $ yF)); val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis; in - map3 (fn goal => fn srel_def => fn Isrel_simp => + map3 (fn goal => fn srel_def => fn dtor_Isrel => Skip_Proof.prove lthy [] [] goal - (mk_rel_simp_tac srel_def Irel_defs Isrel_defs Isrel_simp) + (mk_dtor_rel_tac srel_def Irel_defs Isrel_defs dtor_Isrel) |> Thm.close_derivation) - goals srel_defs Isrel_simp_thms + goals srel_defs dtor_Isrel_thms end; val timer = time (timer "additional properties"); @@ -1783,11 +1783,11 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); val Ibnf_notes = - [(map_simpsN, map single folded_map_simp_thms), - (rel_simpN, map single Irel_simp_thms), + [(dtor_relN, map single dtor_Irel_thms), + (dtor_srelN, map single dtor_Isrel_thms), + (map_simpsN, map single folded_map_simp_thms), (set_inclN, set_incl_thmss), - (set_set_inclN, map flat set_set_incl_thmsss), - (srel_simpN, map single Isrel_simp_thms)] @ + (set_set_inclN, map flat set_set_incl_thmsss)] @ map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => diff -r 191d9384966a -r d4859efc1096 src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Fri Sep 21 18:25:17 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Fri Sep 21 18:25:17 2012 +0200 @@ -23,6 +23,8 @@ val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic + val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> + thm list -> thm list -> thm list list -> tactic val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic val mk_in_bd_tac: thm -> thm -> thm -> thm -> tactic val mk_incl_min_alg_tac: (int -> tactic) -> thm list list list -> thm list -> thm -> @@ -69,8 +71,6 @@ val mk_set_natural_tac: thm -> tactic val mk_set_simp_tac: thm -> thm -> thm list -> tactic val mk_set_tac: thm -> tactic - val mk_srel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> - thm -> thm list -> thm list -> thm list list -> tactic val mk_wit_tac: int -> thm list -> thm list -> tactic val mk_wpull_tac: thm -> tactic end; @@ -770,7 +770,7 @@ EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp, REPEAT_DETERM_N n o etac UnE]))))] 1); -fun mk_srel_simp_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject +fun mk_dtor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject ctor_dtor set_naturals set_incls set_set_inclss = let val m = length set_incls; diff -r 191d9384966a -r d4859efc1096 src/HOL/BNF/Tools/bnf_tactics.ML --- a/src/HOL/BNF/Tools/bnf_tactics.ML Fri Sep 21 18:25:17 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML Fri Sep 21 18:25:17 2012 +0200 @@ -27,7 +27,7 @@ val mk_Abs_inj_thm: thm -> thm val simple_srel_O_Gr_tac: Proof.context -> tactic - val mk_rel_simp_tac: thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> + val mk_dtor_rel_tac: thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic val mk_map_comp_id_tac: thm -> tactic @@ -101,10 +101,10 @@ fun simple_srel_O_Gr_tac ctxt = unfold_thms_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1; -fun mk_rel_simp_tac srel_def IJrel_defs IJsrel_defs srel_simp {context = ctxt, prems = _} = +fun mk_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} = unfold_thms_tac ctxt IJrel_defs THEN subst_tac ctxt [unfold_thms ctxt (IJrel_defs @ IJsrel_defs @ - @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) srel_simp] 1 THEN + @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel] 1 THEN unfold_thms_tac ctxt (srel_def :: @{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv split_conv}) THEN