renamed "set_incl" etc. to have "ctor" or "dtor" in the name
authorblanchet
Sun Sep 23 14:52:53 2012 +0200 (2012-09-23)
changeset 4954424094fa47e0d
parent 49543 53b3c532a082
child 49545 8bb6e2d7346b
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
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
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp.ML	Sun Sep 23 14:52:53 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp.ML	Sun Sep 23 14:52:53 2012 +0200
     1.3 @@ -36,6 +36,8 @@
     1.4    val ctor_recN: string
     1.5    val ctor_recsN: string
     1.6    val ctor_relN: string
     1.7 +  val ctor_set_inclN: string
     1.8 +  val ctor_set_set_inclN: string
     1.9    val ctor_srelN: string
    1.10    val disc_unfold_iffN: string
    1.11    val disc_unfoldsN: string
    1.12 @@ -51,6 +53,8 @@
    1.13    val dtor_exhaustN: string
    1.14    val dtor_injectN: string
    1.15    val dtor_map_uniqueN: string
    1.16 +  val dtor_set_inclN: string
    1.17 +  val dtor_set_set_inclN: string
    1.18    val dtor_srelN: string
    1.19    val dtor_strong_coinductN: string
    1.20    val dtor_unfoldN: string
    1.21 @@ -249,7 +253,11 @@
    1.22  val hsetN = "Hset"
    1.23  val hset_recN = hsetN ^ "_rec"
    1.24  val set_inclN = "set_incl"
    1.25 +val ctor_set_inclN = ctorN ^ "_" ^ set_inclN
    1.26 +val dtor_set_inclN = dtorN ^ "_" ^ set_inclN
    1.27  val set_set_inclN = "set_set_incl"
    1.28 +val ctor_set_set_inclN = ctorN ^ "_" ^ set_set_inclN
    1.29 +val dtor_set_set_inclN = dtorN ^ "_" ^ set_set_inclN
    1.30  
    1.31  val caseN = "case"
    1.32  val discN = "disc"
     2.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Sep 23 14:52:53 2012 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Sep 23 14:52:53 2012 +0200
     2.3 @@ -2874,8 +2874,8 @@
     2.4  
     2.5          val timer = time (timer "registered new codatatypes as BNFs");
     2.6  
     2.7 -        val set_incl_thmss = map (map fold_sets) hset_dtor_incl_thmss;
     2.8 -        val set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss;
     2.9 +        val dtor_set_incl_thmss = map (map fold_sets) hset_dtor_incl_thmss;
    2.10 +        val dtor_set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss;
    2.11          val dtor_set_induct_thms = map fold_sets dtor_hset_induct_thms;
    2.12  
    2.13          val srels = map2 (fn Ds => mk_srel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
    2.14 @@ -2906,13 +2906,14 @@
    2.15            in
    2.16              map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
    2.17                fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
    2.18 -              fn set_naturals => fn set_incls => fn set_set_inclss =>
    2.19 +              fn set_naturals => fn dtor_set_incls => fn dtor_set_set_inclss =>
    2.20                Skip_Proof.prove lthy [] [] goal
    2.21                  (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets
    2.22 -                  dtor_inject dtor_ctor set_naturals set_incls set_set_inclss))
    2.23 +                  dtor_inject dtor_ctor set_naturals dtor_set_incls dtor_set_set_inclss))
    2.24                |> Thm.close_derivation)
    2.25              ks goals in_srels map_comp's map_congs folded_dtor_map_thms folded_set_simp_thmss'
    2.26 -              dtor_inject_thms dtor_ctor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
    2.27 +              dtor_inject_thms dtor_ctor_thms set_natural'ss dtor_set_incl_thmss
    2.28 +              dtor_set_set_incl_thmsss
    2.29            end;
    2.30  
    2.31          val dtor_Jrel_thms =
    2.32 @@ -2941,9 +2942,9 @@
    2.33          val Jbnf_notes =
    2.34            [(dtor_mapN, map single folded_dtor_map_thms),
    2.35            (dtor_relN, map single dtor_Jrel_thms),
    2.36 -          (dtor_srelN, map single dtor_Jsrel_thms),
    2.37 -          (set_inclN, set_incl_thmss),
    2.38 -          (set_set_inclN, map flat set_set_incl_thmsss)] @
    2.39 +          (dtor_set_inclN, dtor_set_incl_thmss),
    2.40 +          (dtor_set_set_inclN, map flat dtor_set_set_incl_thmsss),
    2.41 +          (dtor_srelN, map single dtor_Jsrel_thms)] @
    2.42            map2 (fn i => fn thms => (mk_dtor_setsN i, map single thms)) ls' folded_set_simp_thmss
    2.43            |> maps (fn (thmN, thmss) =>
    2.44              map2 (fn b => fn thms =>
     3.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
     3.3 @@ -1495,10 +1495,10 @@
     3.4      FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
     3.5  
     3.6  fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets dtor_inject dtor_ctor
     3.7 -  set_naturals set_incls set_set_inclss =
     3.8 +  set_naturals dtor_set_incls dtor_set_set_inclss =
     3.9    let
    3.10 -    val m = length set_incls;
    3.11 -    val n = length set_set_inclss;
    3.12 +    val m = length dtor_set_incls;
    3.13 +    val n = length dtor_set_set_inclss;
    3.14      val (passive_set_naturals, active_set_naturals) = chop m set_naturals;
    3.15      val in_Jsrel = nth in_Jsrels (i - 1);
    3.16      val if_tac =
    3.17 @@ -1508,13 +1508,13 @@
    3.18            EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural,
    3.19              rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
    3.20              etac (set_incl RS @{thm subset_trans})])
    3.21 -        passive_set_naturals set_incls),
    3.22 -        CONJ_WRAP' (fn (in_Jsrel, (set_natural, set_set_incls)) =>
    3.23 +        passive_set_naturals dtor_set_incls),
    3.24 +        CONJ_WRAP' (fn (in_Jsrel, (set_natural, dtor_set_set_incls)) =>
    3.25            EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI},
    3.26              rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
    3.27 -            CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) set_set_incls,
    3.28 +            CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls,
    3.29              rtac conjI, rtac refl, rtac refl])
    3.30 -        (in_Jsrels ~~ (active_set_naturals ~~ set_set_inclss)),
    3.31 +        (in_Jsrels ~~ (active_set_naturals ~~ dtor_set_set_inclss)),
    3.32          CONJ_WRAP' (fn conv =>
    3.33            EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
    3.34            REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
     4.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Sun Sep 23 14:52:53 2012 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Sun Sep 23 14:52:53 2012 +0200
     4.3 @@ -1734,8 +1734,8 @@
     4.4          val Isrel_defs = map srel_def_of_bnf Ibnfs;
     4.5          val Irel_defs = map rel_def_of_bnf Ibnfs;
     4.6  
     4.7 -        val set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
     4.8 -        val set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss;
     4.9 +        val ctor_set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
    4.10 +        val ctor_set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss;
    4.11          val folded_ctor_map_thms = map fold_maps ctor_map_thms;
    4.12          val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
    4.13          val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
    4.14 @@ -1749,13 +1749,14 @@
    4.15            in
    4.16              map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
    4.17                fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
    4.18 -              fn set_naturals => fn set_incls => fn set_set_inclss =>
    4.19 +              fn set_naturals => fn ctor_set_incls => fn ctor_set_set_inclss =>
    4.20                Skip_Proof.prove lthy [] [] goal
    4.21                 (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets
    4.22 -                 ctor_inject ctor_dtor set_naturals set_incls set_set_inclss))
    4.23 +                 ctor_inject ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss))
    4.24                |> Thm.close_derivation)
    4.25              ks goals in_srels map_comp's map_congs folded_ctor_map_thms folded_set_simp_thmss'
    4.26 -              ctor_inject_thms ctor_dtor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
    4.27 +              ctor_inject_thms ctor_dtor_thms set_natural'ss ctor_set_incl_thmss
    4.28 +              ctor_set_set_incl_thmsss
    4.29            end;
    4.30  
    4.31          val ctor_Irel_thms =
    4.32 @@ -1784,8 +1785,8 @@
    4.33            [(ctor_mapN, map single folded_ctor_map_thms),
    4.34            (ctor_relN, map single ctor_Irel_thms),
    4.35            (ctor_srelN, map single ctor_Isrel_thms),
    4.36 -          (set_inclN, set_incl_thmss),
    4.37 -          (set_set_inclN, map flat set_set_incl_thmsss)] @
    4.38 +          (ctor_set_inclN, ctor_set_incl_thmss),
    4.39 +          (ctor_set_set_inclN, map flat ctor_set_set_incl_thmsss)] @
    4.40            map2 (fn i => fn thms => (mk_ctor_setsN i, map single thms)) ls' folded_set_simp_thmss
    4.41            |> maps (fn (thmN, thmss) =>
    4.42              map2 (fn b => fn thms =>
     5.1 --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
     5.3 @@ -771,10 +771,10 @@
     5.4              REPEAT_DETERM_N n o etac UnE]))))] 1);
     5.5  
     5.6  fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets ctor_inject
     5.7 -  ctor_dtor set_naturals set_incls set_set_inclss =
     5.8 +  ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss =
     5.9    let
    5.10 -    val m = length set_incls;
    5.11 -    val n = length set_set_inclss;
    5.12 +    val m = length ctor_set_incls;
    5.13 +    val n = length ctor_set_set_inclss;
    5.14  
    5.15      val (passive_set_naturals, active_set_naturals) = chop m set_naturals;
    5.16      val in_Isrel = nth in_Isrels (i - 1);
    5.17 @@ -783,19 +783,19 @@
    5.18      val if_tac =
    5.19        EVERY' [dtac (in_Isrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
    5.20          rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
    5.21 -        EVERY' (map2 (fn set_natural => fn set_incl =>
    5.22 +        EVERY' (map2 (fn set_natural => fn ctor_set_incl =>
    5.23            EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural,
    5.24              rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
    5.25 -            rtac (set_incl RS subset_trans), etac le_arg_cong_ctor_dtor])
    5.26 -        passive_set_naturals set_incls),
    5.27 -        CONJ_WRAP' (fn (in_Isrel, (set_natural, set_set_incls)) =>
    5.28 +            rtac (ctor_set_incl RS subset_trans), etac le_arg_cong_ctor_dtor])
    5.29 +        passive_set_naturals ctor_set_incls),
    5.30 +        CONJ_WRAP' (fn (in_Isrel, (set_natural, ctor_set_set_incls)) =>
    5.31            EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI},
    5.32              rtac (in_Isrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
    5.33              CONJ_WRAP' (fn thm =>
    5.34                EVERY' (map etac [thm RS subset_trans, le_arg_cong_ctor_dtor]))
    5.35 -            set_set_incls,
    5.36 +            ctor_set_set_incls,
    5.37              rtac conjI, rtac refl, rtac refl])
    5.38 -        (in_Isrels ~~ (active_set_naturals ~~ set_set_inclss)),
    5.39 +        (in_Isrels ~~ (active_set_naturals ~~ ctor_set_set_inclss)),
    5.40          CONJ_WRAP' (fn conv =>
    5.41            EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
    5.42            REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},