# HG changeset patch
# User blanchet
# Date 1348404773 -7200
# Node ID 24094fa47e0d853bb70c355746711a38ab598798
# Parent  53b3c532a08238741c65a1f69eea8e34eb890fb4
renamed "set_incl" etc. to have "ctor" or "dtor" in the name

diff -r 53b3c532a082 -r 24094fa47e0d src/HOL/BNF/Tools/bnf_fp.ML
--- a/src/HOL/BNF/Tools/bnf_fp.ML	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Sun Sep 23 14:52:53 2012 +0200
@@ -36,6 +36,8 @@
   val ctor_recN: string
   val ctor_recsN: string
   val ctor_relN: string
+  val ctor_set_inclN: string
+  val ctor_set_set_inclN: string
   val ctor_srelN: string
   val disc_unfold_iffN: string
   val disc_unfoldsN: string
@@ -51,6 +53,8 @@
   val dtor_exhaustN: string
   val dtor_injectN: string
   val dtor_map_uniqueN: string
+  val dtor_set_inclN: string
+  val dtor_set_set_inclN: string
   val dtor_srelN: string
   val dtor_strong_coinductN: string
   val dtor_unfoldN: string
@@ -249,7 +253,11 @@
 val hsetN = "Hset"
 val hset_recN = hsetN ^ "_rec"
 val set_inclN = "set_incl"
+val ctor_set_inclN = ctorN ^ "_" ^ set_inclN
+val dtor_set_inclN = dtorN ^ "_" ^ set_inclN
 val set_set_inclN = "set_set_incl"
+val ctor_set_set_inclN = ctorN ^ "_" ^ set_set_inclN
+val dtor_set_set_inclN = dtorN ^ "_" ^ set_set_inclN
 
 val caseN = "case"
 val discN = "disc"
diff -r 53b3c532a082 -r 24094fa47e0d src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Sep 23 14:52:53 2012 +0200
@@ -2874,8 +2874,8 @@
 
         val timer = time (timer "registered new codatatypes as BNFs");
 
-        val set_incl_thmss = map (map fold_sets) hset_dtor_incl_thmss;
-        val set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss;
+        val dtor_set_incl_thmss = map (map fold_sets) hset_dtor_incl_thmss;
+        val dtor_set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss;
         val dtor_set_induct_thms = map fold_sets dtor_hset_induct_thms;
 
         val srels = map2 (fn Ds => mk_srel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
@@ -2906,13 +2906,14 @@
           in
             map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
               fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
-              fn set_naturals => fn set_incls => fn set_set_inclss =>
+              fn set_naturals => fn dtor_set_incls => fn dtor_set_set_inclss =>
               Skip_Proof.prove lthy [] [] goal
                 (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets
-                  dtor_inject dtor_ctor set_naturals set_incls set_set_inclss))
+                  dtor_inject dtor_ctor set_naturals dtor_set_incls dtor_set_set_inclss))
               |> Thm.close_derivation)
             ks goals in_srels map_comp's map_congs folded_dtor_map_thms folded_set_simp_thmss'
-              dtor_inject_thms dtor_ctor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
+              dtor_inject_thms dtor_ctor_thms set_natural'ss dtor_set_incl_thmss
+              dtor_set_set_incl_thmsss
           end;
 
         val dtor_Jrel_thms =
@@ -2941,9 +2942,9 @@
         val Jbnf_notes =
           [(dtor_mapN, map single folded_dtor_map_thms),
           (dtor_relN, map single dtor_Jrel_thms),
-          (dtor_srelN, map single dtor_Jsrel_thms),
-          (set_inclN, set_incl_thmss),
-          (set_set_inclN, map flat set_set_incl_thmsss)] @
+          (dtor_set_inclN, dtor_set_incl_thmss),
+          (dtor_set_set_inclN, map flat dtor_set_set_incl_thmsss),
+          (dtor_srelN, map single dtor_Jsrel_thms)] @
           map2 (fn i => fn thms => (mk_dtor_setsN i, map single thms)) ls' folded_set_simp_thmss
           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>
diff -r 53b3c532a082 -r 24094fa47e0d src/HOL/BNF/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
@@ -1495,10 +1495,10 @@
     FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
 
 fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets dtor_inject dtor_ctor
-  set_naturals set_incls set_set_inclss =
+  set_naturals dtor_set_incls dtor_set_set_inclss =
   let
-    val m = length set_incls;
-    val n = length set_set_inclss;
+    val m = length dtor_set_incls;
+    val n = length dtor_set_set_inclss;
     val (passive_set_naturals, active_set_naturals) = chop m set_naturals;
     val in_Jsrel = nth in_Jsrels (i - 1);
     val if_tac =
@@ -1508,13 +1508,13 @@
           EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural,
             rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
             etac (set_incl RS @{thm subset_trans})])
-        passive_set_naturals set_incls),
-        CONJ_WRAP' (fn (in_Jsrel, (set_natural, set_set_incls)) =>
+        passive_set_naturals dtor_set_incls),
+        CONJ_WRAP' (fn (in_Jsrel, (set_natural, dtor_set_set_incls)) =>
           EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI},
             rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
-            CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) set_set_incls,
+            CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls,
             rtac conjI, rtac refl, rtac refl])
-        (in_Jsrels ~~ (active_set_naturals ~~ set_set_inclss)),
+        (in_Jsrels ~~ (active_set_naturals ~~ dtor_set_set_inclss)),
         CONJ_WRAP' (fn conv =>
           EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
diff -r 53b3c532a082 -r 24094fa47e0d src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Sun Sep 23 14:52:53 2012 +0200
@@ -1734,8 +1734,8 @@
         val Isrel_defs = map srel_def_of_bnf Ibnfs;
         val Irel_defs = map rel_def_of_bnf Ibnfs;
 
-        val set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
-        val set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss;
+        val ctor_set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
+        val ctor_set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss;
         val folded_ctor_map_thms = map fold_maps ctor_map_thms;
         val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
         val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
@@ -1749,13 +1749,14 @@
           in
             map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
               fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
-              fn set_naturals => fn set_incls => fn set_set_inclss =>
+              fn set_naturals => fn ctor_set_incls => fn ctor_set_set_inclss =>
               Skip_Proof.prove lthy [] [] goal
                (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets
-                 ctor_inject ctor_dtor set_naturals set_incls set_set_inclss))
+                 ctor_inject ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss))
               |> Thm.close_derivation)
             ks goals in_srels map_comp's map_congs folded_ctor_map_thms folded_set_simp_thmss'
-              ctor_inject_thms ctor_dtor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
+              ctor_inject_thms ctor_dtor_thms set_natural'ss ctor_set_incl_thmss
+              ctor_set_set_incl_thmsss
           end;
 
         val ctor_Irel_thms =
@@ -1784,8 +1785,8 @@
           [(ctor_mapN, map single folded_ctor_map_thms),
           (ctor_relN, map single ctor_Irel_thms),
           (ctor_srelN, map single ctor_Isrel_thms),
-          (set_inclN, set_incl_thmss),
-          (set_set_inclN, map flat set_set_incl_thmsss)] @
+          (ctor_set_inclN, ctor_set_incl_thmss),
+          (ctor_set_set_inclN, map flat ctor_set_set_incl_thmsss)] @
           map2 (fn i => fn thms => (mk_ctor_setsN i, map single thms)) ls' folded_set_simp_thmss
           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>
diff -r 53b3c532a082 -r 24094fa47e0d src/HOL/BNF/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
@@ -771,10 +771,10 @@
             REPEAT_DETERM_N n o etac UnE]))))] 1);
 
 fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets ctor_inject
-  ctor_dtor set_naturals set_incls set_set_inclss =
+  ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss =
   let
-    val m = length set_incls;
-    val n = length set_set_inclss;
+    val m = length ctor_set_incls;
+    val n = length ctor_set_set_inclss;
 
     val (passive_set_naturals, active_set_naturals) = chop m set_naturals;
     val in_Isrel = nth in_Isrels (i - 1);
@@ -783,19 +783,19 @@
     val if_tac =
       EVERY' [dtac (in_Isrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
         rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
-        EVERY' (map2 (fn set_natural => fn set_incl =>
+        EVERY' (map2 (fn set_natural => fn ctor_set_incl =>
           EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural,
             rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
-            rtac (set_incl RS subset_trans), etac le_arg_cong_ctor_dtor])
-        passive_set_naturals set_incls),
-        CONJ_WRAP' (fn (in_Isrel, (set_natural, set_set_incls)) =>
+            rtac (ctor_set_incl RS subset_trans), etac le_arg_cong_ctor_dtor])
+        passive_set_naturals ctor_set_incls),
+        CONJ_WRAP' (fn (in_Isrel, (set_natural, ctor_set_set_incls)) =>
           EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI},
             rtac (in_Isrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
             CONJ_WRAP' (fn thm =>
               EVERY' (map etac [thm RS subset_trans, le_arg_cong_ctor_dtor]))
-            set_set_incls,
+            ctor_set_set_incls,
             rtac conjI, rtac refl, rtac refl])
-        (in_Isrels ~~ (active_set_naturals ~~ set_set_inclss)),
+        (in_Isrels ~~ (active_set_naturals ~~ ctor_set_set_inclss)),
         CONJ_WRAP' (fn conv =>
           EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},