renamed "rel_simp" to "dtor_rel" and similarly for "srel"
authorblanchet
Fri Sep 21 18:25:17 2012 +0200 (2012-09-21)
changeset 49516d4859efc1096
parent 49515 191d9384966a
child 49517 c473c8749cd1
renamed "rel_simp" to "dtor_rel" and similarly for "srel"
src/HOL/BNF/Tools/bnf_fp.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_gfp_tactics.ML
src/HOL/BNF/Tools/bnf_lfp.ML
src/HOL/BNF/Tools/bnf_lfp_tactics.ML
src/HOL/BNF/Tools/bnf_tactics.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp.ML	Fri Sep 21 18:25:17 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp.ML	Fri Sep 21 18:25:17 2012 +0200
     1.3 @@ -39,15 +39,16 @@
     1.4    val disc_corecsN: string
     1.5    val dtorN: string
     1.6    val dtor_coinductN: string
     1.7 -  val dtor_unfoldN: string
     1.8 -  val dtor_unfold_uniqueN: string
     1.9 -  val dtor_unfoldsN: string
    1.10 +  val dtor_relN: string
    1.11    val dtor_corecN: string
    1.12    val dtor_corecsN: string
    1.13    val dtor_exhaustN: string
    1.14    val dtor_ctorN: string
    1.15    val dtor_injectN: string
    1.16    val dtor_strong_coinductN: string
    1.17 +  val dtor_unfoldN: string
    1.18 +  val dtor_unfold_uniqueN: string
    1.19 +  val dtor_unfoldsN: string
    1.20    val exhaustN: string
    1.21    val foldN: string
    1.22    val foldsN: string
    1.23 @@ -65,7 +66,6 @@
    1.24    val recN: string
    1.25    val recsN: string
    1.26    val rel_coinductN: string
    1.27 -  val rel_simpN: string
    1.28    val rel_strong_coinductN: string
    1.29    val rvN: string
    1.30    val sel_unfoldsN: string
    1.31 @@ -74,7 +74,7 @@
    1.32    val set_set_inclN: string
    1.33    val simpsN: string
    1.34    val srel_coinductN: string
    1.35 -  val srel_simpN: string
    1.36 +  val dtor_srelN: string
    1.37    val srel_strong_coinductN: string
    1.38    val strTN: string
    1.39    val str_initN: string
    1.40 @@ -225,8 +225,8 @@
    1.41  val rel_coinductN = relN ^ "_" ^ coinductN
    1.42  val srel_coinductN = srelN ^ "_" ^ coinductN
    1.43  val simpN = "_simp";
    1.44 -val srel_simpN = srelN ^ simpN;
    1.45 -val rel_simpN = relN ^ simpN;
    1.46 +val dtor_srelN = dtorN ^ "_" ^ srelN
    1.47 +val dtor_relN = dtorN ^ "_" ^ relN
    1.48  val strongN = "strong_"
    1.49  val dtor_strong_coinductN = dtorN ^ "_" ^ strongN ^ coinductN
    1.50  val rel_strong_coinductN = relN ^ "_" ^ strongN ^ coinductN
     2.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Sep 21 18:25:17 2012 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Sep 21 18:25:17 2012 +0200
     2.3 @@ -2899,7 +2899,7 @@
     2.4          val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
     2.5          val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
     2.6  
     2.7 -        val Jsrel_simp_thms =
     2.8 +        val dtor_Jsrel_thms =
     2.9            let
    2.10              fun mk_goal Jz Jz' dtor dtor' JsrelR srelR = fold_rev Logic.all (Jz :: Jz' :: JRs)
    2.11                (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JsrelR),
    2.12 @@ -2910,24 +2910,24 @@
    2.13                fn map_simp => fn set_simps => fn dtor_inject => fn dtor_ctor =>
    2.14                fn set_naturals => fn set_incls => fn set_set_inclss =>
    2.15                Skip_Proof.prove lthy [] [] goal
    2.16 -                (K (mk_srel_simp_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps
    2.17 +                (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps
    2.18                    dtor_inject dtor_ctor set_naturals set_incls set_set_inclss))
    2.19                |> Thm.close_derivation)
    2.20              ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
    2.21                dtor_inject_thms dtor_ctor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
    2.22            end;
    2.23  
    2.24 -        val Jrel_simp_thms =
    2.25 +        val dtor_Jrel_thms =
    2.26            let
    2.27              fun mk_goal Jz Jz' dtor dtor' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis)
    2.28                (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (dtor $ Jz) $ (dtor' $ Jz')));
    2.29              val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
    2.30            in
    2.31 -            map3 (fn goal => fn srel_def => fn Jsrel_simp =>
    2.32 +            map3 (fn goal => fn srel_def => fn dtor_Jsrel =>
    2.33                Skip_Proof.prove lthy [] [] goal
    2.34 -                (mk_rel_simp_tac srel_def Jrel_defs Jsrel_defs Jsrel_simp)
    2.35 +                (mk_dtor_rel_tac srel_def Jrel_defs Jsrel_defs dtor_Jsrel)
    2.36                |> Thm.close_derivation)
    2.37 -            goals srel_defs Jsrel_simp_thms
    2.38 +            goals srel_defs dtor_Jsrel_thms
    2.39            end;
    2.40  
    2.41          val timer = time (timer "additional properties");
    2.42 @@ -2941,11 +2941,11 @@
    2.43              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
    2.44  
    2.45          val Jbnf_notes =
    2.46 -          [(map_simpsN, map single folded_map_simp_thms),
    2.47 -          (rel_simpN, map single Jrel_simp_thms),
    2.48 +          [(dtor_relN, map single dtor_Jrel_thms),
    2.49 +          (dtor_srelN, map single dtor_Jsrel_thms),
    2.50 +          (map_simpsN, map single folded_map_simp_thms),
    2.51            (set_inclN, set_incl_thmss),
    2.52 -          (set_set_inclN, map flat set_set_incl_thmsss),
    2.53 -          (srel_simpN, map single Jsrel_simp_thms)] @
    2.54 +          (set_set_inclN, map flat set_set_incl_thmsss)] @
    2.55            map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
    2.56            |> maps (fn (thmN, thmss) =>
    2.57              map2 (fn b => fn thms =>
     3.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Fri Sep 21 18:25:17 2012 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Fri Sep 21 18:25:17 2012 +0200
     3.3 @@ -38,6 +38,8 @@
     3.4    val mk_corec_tac: int -> thm list -> thm -> thm -> thm list ->
     3.5      {prems: 'a, context: Proof.context} -> tactic
     3.6    val mk_dtor_coinduct_tac: int -> int list -> thm -> thm -> tactic
     3.7 +  val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
     3.8 +    thm list -> thm list -> thm list list -> tactic
     3.9    val mk_dtor_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
    3.10      thm -> thm -> tactic
    3.11    val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
    3.12 @@ -109,8 +111,6 @@
    3.13    val mk_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
    3.14    val mk_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->
    3.15      thm list -> thm list -> tactic
    3.16 -  val mk_srel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
    3.17 -    thm list -> thm list -> thm list list -> tactic
    3.18    val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
    3.19      cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
    3.20      thm list list -> thm list list -> thm -> thm list list -> tactic
    3.21 @@ -1494,7 +1494,7 @@
    3.22    ALLGOALS (TRY o
    3.23      FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
    3.24  
    3.25 -fun mk_srel_simp_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps dtor_inject dtor_ctor
    3.26 +fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps dtor_inject dtor_ctor
    3.27    set_naturals set_incls set_set_inclss =
    3.28    let
    3.29      val m = length set_incls;
     4.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Sep 21 18:25:17 2012 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Sep 21 18:25:17 2012 +0200
     4.3 @@ -1742,7 +1742,7 @@
     4.4          val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
     4.5          val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
     4.6  
     4.7 -        val Isrel_simp_thms =
     4.8 +        val dtor_Isrel_thms =
     4.9            let
    4.10              fun mk_goal xF yF ctor ctor' IsrelR srelR = fold_rev Logic.all (xF :: yF :: IRs)
    4.11                (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (ctor $ xF, ctor' $ yF), IsrelR),
    4.12 @@ -1753,24 +1753,24 @@
    4.13                fn map_simp => fn set_simps => fn ctor_inject => fn ctor_dtor =>
    4.14                fn set_naturals => fn set_incls => fn set_set_inclss =>
    4.15                Skip_Proof.prove lthy [] [] goal
    4.16 -               (K (mk_srel_simp_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps
    4.17 +               (K (mk_dtor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps
    4.18                   ctor_inject ctor_dtor set_naturals set_incls set_set_inclss))
    4.19                |> Thm.close_derivation)
    4.20              ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
    4.21                ctor_inject_thms ctor_dtor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
    4.22            end;
    4.23  
    4.24 -        val Irel_simp_thms =
    4.25 +        val dtor_Irel_thms =
    4.26            let
    4.27              fun mk_goal xF yF ctor ctor' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis)
    4.28                (mk_Trueprop_eq (Ipredphi $ (ctor $ xF) $ (ctor' $ yF), predphi $ xF $ yF));
    4.29              val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
    4.30            in
    4.31 -            map3 (fn goal => fn srel_def => fn Isrel_simp =>
    4.32 +            map3 (fn goal => fn srel_def => fn dtor_Isrel =>
    4.33                Skip_Proof.prove lthy [] [] goal
    4.34 -                (mk_rel_simp_tac srel_def Irel_defs Isrel_defs Isrel_simp)
    4.35 +                (mk_dtor_rel_tac srel_def Irel_defs Isrel_defs dtor_Isrel)
    4.36                |> Thm.close_derivation)
    4.37 -            goals srel_defs Isrel_simp_thms
    4.38 +            goals srel_defs dtor_Isrel_thms
    4.39            end;
    4.40  
    4.41          val timer = time (timer "additional properties");
    4.42 @@ -1783,11 +1783,11 @@
    4.43              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
    4.44  
    4.45          val Ibnf_notes =
    4.46 -          [(map_simpsN, map single folded_map_simp_thms),
    4.47 -          (rel_simpN, map single Irel_simp_thms),
    4.48 +          [(dtor_relN, map single dtor_Irel_thms),
    4.49 +          (dtor_srelN, map single dtor_Isrel_thms),
    4.50 +          (map_simpsN, map single folded_map_simp_thms),
    4.51            (set_inclN, set_incl_thmss),
    4.52 -          (set_set_inclN, map flat set_set_incl_thmsss),
    4.53 -          (srel_simpN, map single Isrel_simp_thms)] @
    4.54 +          (set_set_inclN, map flat set_set_incl_thmsss)] @
    4.55            map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
    4.56            |> maps (fn (thmN, thmss) =>
    4.57              map2 (fn b => fn thms =>
     5.1 --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Fri Sep 21 18:25:17 2012 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Fri Sep 21 18:25:17 2012 +0200
     5.3 @@ -23,6 +23,8 @@
     5.4    val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list ->
     5.5      {prems: 'a, context: Proof.context} -> tactic
     5.6    val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
     5.7 +  val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
     5.8 +    thm list -> thm list -> thm list list -> tactic
     5.9    val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic
    5.10    val mk_in_bd_tac: thm -> thm -> thm -> thm -> tactic
    5.11    val mk_incl_min_alg_tac: (int -> tactic) -> thm list list list -> thm list -> thm ->
    5.12 @@ -69,8 +71,6 @@
    5.13    val mk_set_natural_tac: thm -> tactic
    5.14    val mk_set_simp_tac: thm -> thm -> thm list -> tactic
    5.15    val mk_set_tac: thm -> tactic
    5.16 -  val mk_srel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm ->
    5.17 -    thm -> thm list -> thm list -> thm list list -> tactic
    5.18    val mk_wit_tac: int -> thm list -> thm list -> tactic
    5.19    val mk_wpull_tac: thm -> tactic
    5.20  end;
    5.21 @@ -770,7 +770,7 @@
    5.22            EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
    5.23              REPEAT_DETERM_N n o etac UnE]))))] 1);
    5.24  
    5.25 -fun mk_srel_simp_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject
    5.26 +fun mk_dtor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject
    5.27    ctor_dtor set_naturals set_incls set_set_inclss =
    5.28    let
    5.29      val m = length set_incls;
     6.1 --- a/src/HOL/BNF/Tools/bnf_tactics.ML	Fri Sep 21 18:25:17 2012 +0200
     6.2 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Fri Sep 21 18:25:17 2012 +0200
     6.3 @@ -27,7 +27,7 @@
     6.4    val mk_Abs_inj_thm: thm -> thm
     6.5  
     6.6    val simple_srel_O_Gr_tac: Proof.context -> tactic
     6.7 -  val mk_rel_simp_tac: thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
     6.8 +  val mk_dtor_rel_tac: thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
     6.9      tactic
    6.10  
    6.11    val mk_map_comp_id_tac: thm -> tactic
    6.12 @@ -101,10 +101,10 @@
    6.13  fun simple_srel_O_Gr_tac ctxt =
    6.14    unfold_thms_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1;
    6.15  
    6.16 -fun mk_rel_simp_tac srel_def IJrel_defs IJsrel_defs srel_simp {context = ctxt, prems = _} =
    6.17 +fun mk_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} =
    6.18    unfold_thms_tac ctxt IJrel_defs THEN
    6.19    subst_tac ctxt [unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
    6.20 -    @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) srel_simp] 1 THEN
    6.21 +    @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel] 1 THEN
    6.22    unfold_thms_tac ctxt (srel_def ::
    6.23      @{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv
    6.24        split_conv}) THEN