tuned internal construction
authortraytel
Mon Mar 17 17:35:39 2014 +0100 (2014-03-17)
changeset 561796b5c46582260
parent 56178 2a6f58938573
child 56180 fae7a45d0fef
tuned internal construction
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Mar 17 15:48:30 2014 +0000
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Mar 17 17:35:39 2014 +0100
     1.3 @@ -1707,9 +1707,9 @@
     1.4      
     1.5          fun col_spec j Zero hrec hrec' =
     1.6            let
     1.7 -            fun mk_Suc dtor setss z z' =
     1.8 +            fun mk_Suc dtor sets z z' =
     1.9                let
    1.10 -                val (set, sets) = apfst (fn xs => nth xs (j - 1)) (chop m setss);
    1.11 +                val (set, sets) = apfst (fn xs => nth xs (j - 1)) (chop m sets);
    1.12                  fun mk_UN set k = mk_UNION (set $ (dtor $ z)) (mk_nthN n hrec k);
    1.13                in
    1.14                  Term.absfree z'
    1.15 @@ -1748,295 +1748,32 @@
    1.16          val col_0ss' = transpose col_0ss;
    1.17          val col_Sucss' = transpose col_Sucss;
    1.18      
    1.19 -        fun mk_hset Ts i j T =
    1.20 +        fun mk_set Ts i j T =
    1.21            Abs (Name.uu, nth Ts (i - 1), mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
    1.22              (Term.absfree nat' (mk_col Ts nat i j T $ Bound 1)));
    1.23  
    1.24 -        val setss_by_bnf = map (fn i => map2 (mk_hset Ts i) ls passiveAs) ks;
    1.25 -        val setss_by_range = transpose setss_by_bnf;
    1.26 -
    1.27 -        val hset_minimal_thms =
    1.28 -          let
    1.29 -            fun mk_passive_prem set dtor x K =
    1.30 -              Logic.all x (HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (K $ x)));
    1.31 -    
    1.32 -            fun mk_active_prem dtor x1 K1 set x2 K2 =
    1.33 -              fold_rev Logic.all [x1, x2]
    1.34 -                (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x2, set $ (dtor $ x1))),
    1.35 -                  HOLogic.mk_Trueprop (mk_leq (K2 $ x2) (K1 $ x1))));
    1.36 -    
    1.37 -            val premss = map2 (fn j => fn Ks =>
    1.38 -              map4 mk_passive_prem (map (fn xs => nth xs (j - 1)) FTs_setss) dtors Jzs Ks @
    1.39 -                flat (map4 (fn sets => fn s => fn x1 => fn K1 =>
    1.40 -                  map3 (mk_active_prem s x1 K1) (drop m sets) Jzs_copy Ks) FTs_setss dtors Jzs Ks))
    1.41 -              ls Kss;
    1.42 -    
    1.43 -            val col_minimal_thms =
    1.44 -              let
    1.45 -                fun mk_conjunct j T i K x = mk_leq (mk_col Ts nat i j T $ x) (K $ x);
    1.46 -                fun mk_concl j T Ks = list_all_free Jzs
    1.47 -                  (Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks Jzs));
    1.48 -                val concls = map3 mk_concl ls passiveAs Kss;
    1.49 -    
    1.50 -                val goals = map2 (fn prems => fn concl =>
    1.51 -                  Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls
    1.52 -    
    1.53 -                val ctss =
    1.54 -                  map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls;
    1.55 -              in
    1.56 -                map4 (fn goal => fn cts => fn col_0s => fn col_Sucs =>
    1.57 -                  singleton (Proof_Context.export names_lthy lthy)
    1.58 -                    (Goal.prove_sorry lthy [] [] goal
    1.59 -                      (fn {context = ctxt, prems = _} => mk_col_minimal_tac ctxt m cts col_0s
    1.60 -                        col_Sucs))
    1.61 -                  |> Thm.close_derivation)
    1.62 -                goals ctss col_0ss' col_Sucss'
    1.63 -              end;
    1.64 -    
    1.65 -            fun mk_conjunct j T i K x = mk_leq (mk_hset Ts i j T $ x) (K $ x);
    1.66 -            fun mk_concl j T Ks = Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks Jzs);
    1.67 -            val concls = map3 mk_concl ls passiveAs Kss;
    1.68 -    
    1.69 -            val goals = map3 (fn Ks => fn prems => fn concl =>
    1.70 -              fold_rev Logic.all (Ks @ Jzs)
    1.71 -                (Logic.list_implies (prems, HOLogic.mk_Trueprop concl))) Kss premss concls;
    1.72 -          in
    1.73 -            map2 (fn goal => fn col_minimal =>
    1.74 -              Goal.prove_sorry lthy [] [] goal
    1.75 -                (fn {context = ctxt, prems = _} => mk_hset_minimal_tac ctxt n col_minimal)
    1.76 -              |> Thm.close_derivation)
    1.77 -            goals col_minimal_thms
    1.78 -          end;
    1.79 -
    1.80 -        val (set_incl_hset_thmss, set_hset_incl_hset_thmsss) =
    1.81 -          let
    1.82 -            fun mk_set_incl_hset dtor x set hset = fold_rev Logic.all (x :: ss)
    1.83 -              (HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (hset $ x)));
    1.84 -    
    1.85 -            fun mk_set_hset_incl_hset dtor x y set hset1 hset2 =
    1.86 -              fold_rev Logic.all [x, y]
    1.87 -                (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ (dtor $ y))),
    1.88 -                HOLogic.mk_Trueprop (mk_leq (hset1 $ x) (hset2 $ y))));
    1.89 -    
    1.90 -            val set_incl_hset_goalss =
    1.91 -              map4 (fn dtor => fn x => fn sets => fn hsets =>
    1.92 -                map2 (mk_set_incl_hset dtor x) (take m sets) hsets)
    1.93 -              dtors Jzs FTs_setss setss_by_bnf;
    1.94 -    
    1.95 -            (*xk : F(i)set(m+k) (si yi) ==> F(k)_hset(j) s1 ... sn xk <= F(i)_hset(j) s1 ... sn yi*)
    1.96 -            val set_hset_incl_hset_goalsss =
    1.97 -              map4 (fn dtori => fn yi => fn sets => fn hsetsi =>
    1.98 -                map3 (fn xk => fn set => fn hsetsk =>
    1.99 -                  map2 (mk_set_hset_incl_hset dtori xk yi set) hsetsk hsetsi)
   1.100 -                Jzs_copy (drop m sets) setss_by_bnf)
   1.101 -              dtors Jzs FTs_setss setss_by_bnf;
   1.102 -          in
   1.103 -            (map2 (fn goals => fn rec_Sucs =>
   1.104 -              map2 (fn goal => fn rec_Suc =>
   1.105 -                Goal.prove_sorry lthy [] [] goal (K (mk_set_incl_hset_tac rec_Suc))
   1.106 -                |> Thm.close_derivation)
   1.107 -              goals rec_Sucs)
   1.108 -            set_incl_hset_goalss col_Sucss,
   1.109 -            map2 (fn goalss => fn rec_Sucs =>
   1.110 -              map2 (fn k => fn goals =>
   1.111 -                map2 (fn goal => fn rec_Suc =>
   1.112 -                  Goal.prove_sorry lthy [] [] goal
   1.113 -                    (K (mk_set_hset_incl_hset_tac n rec_Suc k))
   1.114 -                  |> Thm.close_derivation)
   1.115 -                goals rec_Sucs)
   1.116 -              ks goalss)
   1.117 -            set_hset_incl_hset_goalsss col_Sucss)
   1.118 -          end;
   1.119 -    
   1.120 -        val set_incl_hset_thmss' = transpose set_incl_hset_thmss;
   1.121 -        val set_hset_incl_hset_thmsss' = transpose (map transpose set_hset_incl_hset_thmsss);
   1.122 -        val set_hset_thmss = map (map (fn thm => thm RS @{thm set_mp})) set_incl_hset_thmss;
   1.123 -        val set_hset_hset_thmsss = map (map (map (fn thm => thm RS @{thm set_mp})))
   1.124 -          set_hset_incl_hset_thmsss;
   1.125 -        val set_hset_thmss' = transpose set_hset_thmss;
   1.126 -        val set_hset_hset_thmsss' = transpose (map transpose set_hset_hset_thmsss);
   1.127 -
   1.128 -
   1.129 -        val timer = time (timer "Hereditary sets");
   1.130 -    
   1.131 -        val dtor_hset_induct_thms =
   1.132 -          let
   1.133 -            val incls =
   1.134 -              maps (map (fn thm => thm RS @{thm subset_Collect_iff})) set_incl_hset_thmss @
   1.135 -                @{thms subset_Collect_iff[OF subset_refl]};
   1.136 -
   1.137 -            val cTs = map (SOME o certifyT lthy) params';    
   1.138 -            fun mk_induct_tinst phis jsets y y' =
   1.139 -              map4 (fn phi => fn jset => fn Jz => fn Jz' =>
   1.140 -                SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
   1.141 -                  HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz))))))
   1.142 -              phis jsets Jzs Jzs';
   1.143 -          in
   1.144 -            map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
   1.145 -              ((set_minimal
   1.146 -                |> Drule.instantiate' cTs (mk_induct_tinst phis jsets y y')
   1.147 -                |> unfold_thms lthy incls) OF
   1.148 -                (replicate n ballI @
   1.149 -                  maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
   1.150 -              |> singleton (Proof_Context.export names_lthy lthy)
   1.151 -              |> rule_by_tactic lthy (ALLGOALS (TRY o etac asm_rl)))
   1.152 -            hset_minimal_thms set_hset_incl_hset_thmsss' setss_by_range ys ys' dtor_set_induct_phiss
   1.153 -          end;
   1.154 -
   1.155 -        fun close_wit I wit = (I, fold_rev Term.absfree (map (nth ys') I) wit);
   1.156 -
   1.157 -        val all_unitTs = replicate live HOLogic.unitT;
   1.158 -        val unitTs = replicate n HOLogic.unitT;
   1.159 -        val unit_funs = replicate n (Term.absdummy HOLogic.unitT HOLogic.unit);
   1.160 -        fun mk_map_args I =
   1.161 -          map (fn i =>
   1.162 -            if member (op =) I i then Term.absdummy HOLogic.unitT (nth ys i)
   1.163 -            else mk_undefined (HOLogic.unitT --> nth passiveAs i))
   1.164 -          (0 upto (m - 1));
   1.165 -
   1.166 -        fun mk_nat_wit Ds bnf (I, wit) () =
   1.167 -          let
   1.168 -            val passiveI = filter (fn i => i < m) I;
   1.169 -            val map_args = mk_map_args passiveI;
   1.170 -          in
   1.171 -            Term.absdummy HOLogic.unitT (Term.list_comb
   1.172 -              (mk_map_of_bnf Ds all_unitTs (passiveAs @ unitTs) bnf, map_args @ unit_funs) $ wit)
   1.173 -          end;
   1.174 -
   1.175 -        fun mk_dummy_wit Ds bnf I =
   1.176 -          let
   1.177 -            val map_args = mk_map_args I;
   1.178 -          in
   1.179 -            Term.absdummy HOLogic.unitT (Term.list_comb
   1.180 -              (mk_map_of_bnf Ds all_unitTs (passiveAs @ unitTs) bnf, map_args @ unit_funs) $
   1.181 -              mk_undefined (mk_T_of_bnf Ds all_unitTs bnf))
   1.182 -          end;
   1.183 -
   1.184 -        val nat_witss =
   1.185 -          map2 (fn Ds => fn bnf => mk_wits_of_bnf (replicate (nwits_of_bnf bnf) Ds)
   1.186 -            (replicate (nwits_of_bnf bnf) (replicate live HOLogic.unitT)) bnf
   1.187 -            |> map (fn (I, wit) =>
   1.188 -              (I, Lazy.lazy (mk_nat_wit Ds bnf (I, Term.list_comb (wit, map (K HOLogic.unit) I))))))
   1.189 -          Dss bnfs;
   1.190 -
   1.191 -        val nat_wit_thmss = map2 (curry op ~~) nat_witss (map wit_thmss_of_bnf bnfs)
   1.192 -
   1.193 -        val Iss = map (map fst) nat_witss;
   1.194 -
   1.195 -        fun filter_wits (I, wit) =
   1.196 -          let val J = filter (fn i => i < m) I;
   1.197 -          in (J, (length J < length I, wit)) end;
   1.198 -
   1.199 -        val wit_treess = map_index (fn (i, Is) =>
   1.200 -          map_index (finish Iss m [i+m] (i+m)) Is) Iss
   1.201 -          |> map (minimize_wits o map filter_wits o minimize_wits o flat);
   1.202 -
   1.203 -        val coind_wit_argsss =
   1.204 -          map (map (tree_to_coind_wits nat_wit_thmss o snd o snd) o filter (fst o snd)) wit_treess;
   1.205 -
   1.206 -        val nonredundant_coind_wit_argsss =
   1.207 -          fold (fn i => fn argsss =>
   1.208 -            nth_map (i - 1) (filter_out (fn xs =>
   1.209 -              exists (fn ys =>
   1.210 -                let
   1.211 -                  val xs' = (map (fst o fst) xs, snd (fst (hd xs)));
   1.212 -                  val ys' = (map (fst o fst) ys, snd (fst (hd ys)));
   1.213 -                in
   1.214 -                  eq_pair (subset (op =)) (eq_set (op =)) (xs', ys') andalso not (fst xs' = fst ys')
   1.215 -                end)
   1.216 -              (flat argsss)))
   1.217 -            argsss)
   1.218 -          ks coind_wit_argsss;
   1.219 -
   1.220 -        fun prepare_args args =
   1.221 -          let
   1.222 -            val I = snd (fst (hd args));
   1.223 -            val (dummys, args') =
   1.224 -              map_split (fn i =>
   1.225 -                (case find_first (fn arg => fst (fst arg) = i - 1) args of
   1.226 -                  SOME (_, ((_, wit), thms)) => (NONE, (Lazy.force wit, thms))
   1.227 -                | NONE =>
   1.228 -                  (SOME (i - 1), (mk_dummy_wit (nth Dss (i - 1)) (nth bnfs (i - 1)) I, []))))
   1.229 -              ks;
   1.230 -          in
   1.231 -            ((I, dummys), apsnd flat (split_list args'))
   1.232 -          end;
   1.233 -
   1.234 -        fun mk_coind_wits ((I, dummys), (args, thms)) =
   1.235 -          ((I, dummys), (map (fn i => mk_unfold Ts args i $ HOLogic.unit) ks, thms));
   1.236 -
   1.237 -        val coind_witss =
   1.238 -          maps (map (mk_coind_wits o prepare_args)) nonredundant_coind_wit_argsss;
   1.239 -
   1.240 -        val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf
   1.241 -          (replicate (nwits_of_bnf bnf) Ds)
   1.242 -          (replicate (nwits_of_bnf bnf) (passiveAs @ Ts)) bnf) Dss bnfs;
   1.243 -
   1.244 -        val ctor_witss =
   1.245 -          map (map (uncurry close_wit o tree_to_ctor_wit ys ctors witss o snd o snd) o
   1.246 -            filter_out (fst o snd)) wit_treess;
   1.247 -
   1.248 -        fun mk_coind_wit_thms ((I, dummys), (wits, wit_thms)) =
   1.249 -          let
   1.250 -            fun mk_goal sets y y_copy y'_copy j =
   1.251 -              let
   1.252 -                fun mk_conjunct set z dummy wit =
   1.253 -                  mk_Ball (set $ z) (Term.absfree y'_copy
   1.254 -                    (if dummy = NONE orelse member (op =) I (j - 1) then
   1.255 -                      HOLogic.mk_imp (HOLogic.mk_eq (z, wit),
   1.256 -                        if member (op =) I (j - 1) then HOLogic.mk_eq (y_copy, y)
   1.257 -                        else @{term False})
   1.258 -                    else @{term True}));
   1.259 -              in
   1.260 -                fold_rev Logic.all (map (nth ys) I @ Jzs) (HOLogic.mk_Trueprop
   1.261 -                  (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct sets Jzs dummys wits)))
   1.262 -              end;
   1.263 -            val goals = map5 mk_goal setss_by_range ys ys_copy ys'_copy ls;
   1.264 -          in
   1.265 -            map2 (fn goal => fn induct =>
   1.266 -              Goal.prove_sorry lthy [] [] goal
   1.267 -                (fn {context = ctxt, prems = _} => mk_coind_wit_tac ctxt induct dtor_unfold_thms
   1.268 -                  (flat set_mapss) wit_thms)
   1.269 -              |> Thm.close_derivation)
   1.270 -            goals dtor_hset_induct_thms
   1.271 -            |> map split_conj_thm
   1.272 -            |> transpose
   1.273 -            |> map (map_filter (try (fn thm => thm RS bspec RS mp)))
   1.274 -            |> curry op ~~ (map_index Library.I (map (close_wit I) wits))
   1.275 -            |> filter (fn (_, thms) => length thms = m)
   1.276 -          end;
   1.277 -
   1.278 -        val coind_wit_thms = maps mk_coind_wit_thms coind_witss;
   1.279 -
   1.280 -        val (wit_thmss, all_witss) =
   1.281 -          fold (fn ((i, wit), thms) => fn witss =>
   1.282 -            nth_map i (fn (thms', wits) => (thms @ thms', wit :: wits)) witss)
   1.283 -          coind_wit_thms (map (pair []) ctor_witss)
   1.284 -          |> map (apsnd (map snd o minimize_wits))
   1.285 -          |> split_list;
   1.286 +        val setss = map (fn i => map2 (mk_set Ts i) ls passiveAs) ks;
   1.287  
   1.288          val (Jbnf_consts, lthy) =
   1.289 -          fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits =>
   1.290 -              fn T => fn lthy =>
   1.291 -            define_bnf_consts Dont_Inline (user_policy Note_Some lthy) false (SOME deads)
   1.292 +          fold_map7 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn T =>
   1.293 +              fn lthy =>
   1.294 +            define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads)
   1.295                map_b rel_b set_bs
   1.296 -              ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy)
   1.297 -          bs map_bs rel_bs set_bss fs_maps setss_by_bnf all_witss Ts lthy;
   1.298 +              ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd),
   1.299 +                [Const (@{const_name undefined}, T)]), NONE) lthy)
   1.300 +          bs map_bs rel_bs set_bss fs_maps setss Ts lthy;
   1.301  
   1.302          val (_, Jconsts, Jconst_defs, mk_Jconsts) = split_list4 Jbnf_consts;
   1.303 -        val (_, Jsetss, Jbds_Ds, Jwitss_Ds, _) = split_list5 Jconsts;
   1.304 -        val (Jmap_defs, Jset_defss, Jbd_defs, Jwit_defss, Jrel_defs) = split_list5 Jconst_defs;
   1.305 +        val (_, Jsetss, Jbds_Ds, _, _) = split_list5 Jconsts;
   1.306 +        val (Jmap_defs, Jset_defss, Jbd_defs, _, Jrel_defs) = split_list5 Jconst_defs;
   1.307          val (mk_Jmaps_Ds, mk_Jt_Ds, _, mk_Jrels_Ds, _) = split_list5 mk_Jconsts;
   1.308  
   1.309          val Jrel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Jrel_defs;
   1.310          val Jset_defs = flat Jset_defss;
   1.311 -        val Jset_unabs_defs = map (fn def => def RS meta_eq_to_obj_eq RS fun_cong) Jset_defs;
   1.312  
   1.313          fun mk_Jmaps As Bs = map (fn mk => mk deads As Bs) mk_Jmaps_Ds;
   1.314          fun mk_Jsetss As = map2 (fn mk => fn Jsets => map (mk deads As) Jsets) mk_Jt_Ds Jsetss;
   1.315          val Jbds = map2 (fn mk => mk deads passiveAs) mk_Jt_Ds Jbds_Ds;
   1.316 -        val Jwitss =
   1.317 -          map2 (fn mk => fn Jwits => map (mk deads passiveAs o snd) Jwits) mk_Jt_Ds Jwitss_Ds;
   1.318          fun mk_Jrels As Bs = map (fn mk => mk deads As Bs) mk_Jrels_Ds;
   1.319  
   1.320          val Jmaps = mk_Jmaps passiveAs passiveBs;
   1.321 @@ -2098,6 +1835,135 @@
   1.322  
   1.323          val timer = time (timer "map functions for the new codatatypes");
   1.324  
   1.325 +        val Jset_minimal_thms =
   1.326 +          let
   1.327 +            fun mk_passive_prem set dtor x K =
   1.328 +              Logic.all x (HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (K $ x)));
   1.329 +    
   1.330 +            fun mk_active_prem dtor x1 K1 set x2 K2 =
   1.331 +              fold_rev Logic.all [x1, x2]
   1.332 +                (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x2, set $ (dtor $ x1))),
   1.333 +                  HOLogic.mk_Trueprop (mk_leq (K2 $ x2) (K1 $ x1))));
   1.334 +    
   1.335 +            val premss = map2 (fn j => fn Ks =>
   1.336 +              map4 mk_passive_prem (map (fn xs => nth xs (j - 1)) FTs_setss) dtors Jzs Ks @
   1.337 +                flat (map4 (fn sets => fn s => fn x1 => fn K1 =>
   1.338 +                  map3 (mk_active_prem s x1 K1) (drop m sets) Jzs_copy Ks) FTs_setss dtors Jzs Ks))
   1.339 +              ls Kss;
   1.340 +    
   1.341 +            val col_minimal_thms =
   1.342 +              let
   1.343 +                fun mk_conjunct j T i K x = mk_leq (mk_col Ts nat i j T $ x) (K $ x);
   1.344 +                fun mk_concl j T Ks = list_all_free Jzs
   1.345 +                  (Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks Jzs));
   1.346 +                val concls = map3 mk_concl ls passiveAs Kss;
   1.347 +    
   1.348 +                val goals = map2 (fn prems => fn concl =>
   1.349 +                  Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls
   1.350 +    
   1.351 +                val ctss =
   1.352 +                  map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls;
   1.353 +              in
   1.354 +                map4 (fn goal => fn cts => fn col_0s => fn col_Sucs =>
   1.355 +                  singleton (Proof_Context.export names_lthy lthy)
   1.356 +                    (Goal.prove_sorry lthy [] [] goal
   1.357 +                      (fn {context = ctxt, prems = _} => mk_col_minimal_tac ctxt m cts col_0s
   1.358 +                        col_Sucs))
   1.359 +                  |> Thm.close_derivation)
   1.360 +                goals ctss col_0ss' col_Sucss'
   1.361 +              end;
   1.362 +    
   1.363 +            fun mk_conjunct set K x = mk_leq (set $ x) (K $ x);
   1.364 +            fun mk_concl sets Ks = Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct sets Ks Jzs);
   1.365 +            val concls = map2 mk_concl Jsetss_by_range Kss;
   1.366 +    
   1.367 +            val goals = map3 (fn Ks => fn prems => fn concl =>
   1.368 +              fold_rev Logic.all (Ks @ Jzs)
   1.369 +                (Logic.list_implies (prems, HOLogic.mk_Trueprop concl))) Kss premss concls;
   1.370 +          in
   1.371 +            map2 (fn goal => fn col_minimal =>
   1.372 +              Goal.prove_sorry lthy [] [] goal
   1.373 +                (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
   1.374 +                  mk_Jset_minimal_tac ctxt n col_minimal)
   1.375 +              |> Thm.close_derivation)
   1.376 +            goals col_minimal_thms
   1.377 +          end;
   1.378 +
   1.379 +        val (dtor_Jset_incl_thmss, dtor_set_Jset_incl_thmsss) =
   1.380 +          let
   1.381 +            fun mk_set_incl_Jset dtor x set Jset = fold_rev Logic.all (x :: ss)
   1.382 +              (HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (Jset $ x)));
   1.383 +    
   1.384 +            fun mk_set_Jset_incl_Jset dtor x y set Jset1 Jset2 =
   1.385 +              fold_rev Logic.all [x, y]
   1.386 +                (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ (dtor $ y))),
   1.387 +                HOLogic.mk_Trueprop (mk_leq (Jset1 $ x) (Jset2 $ y))));
   1.388 +    
   1.389 +            val set_incl_Jset_goalss =
   1.390 +              map4 (fn dtor => fn x => fn sets => fn Jsets =>
   1.391 +                map2 (mk_set_incl_Jset dtor x) (take m sets) Jsets)
   1.392 +              dtors Jzs FTs_setss Jsetss_by_bnf;
   1.393 +    
   1.394 +            (*x(k) : F(i)set(m+k) (dtor(i) y(i)) ==> J(k)set(j) x(k) <= J(i)set(j) y(i)*)
   1.395 +            val set_Jset_incl_Jset_goalsss =
   1.396 +              map4 (fn dtori => fn yi => fn sets => fn Jsetsi =>
   1.397 +                map3 (fn xk => fn set => fn Jsetsk =>
   1.398 +                  map2 (mk_set_Jset_incl_Jset dtori xk yi set) Jsetsk Jsetsi)
   1.399 +                Jzs_copy (drop m sets) Jsetss_by_bnf)
   1.400 +              dtors Jzs FTs_setss Jsetss_by_bnf;
   1.401 +          in
   1.402 +            (map2 (fn goals => fn rec_Sucs =>
   1.403 +              map2 (fn goal => fn rec_Suc =>
   1.404 +                Goal.prove_sorry lthy [] [] goal
   1.405 +                  (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
   1.406 +                    mk_set_incl_Jset_tac rec_Suc)
   1.407 +                |> Thm.close_derivation)
   1.408 +              goals rec_Sucs)
   1.409 +            set_incl_Jset_goalss col_Sucss,
   1.410 +            map2 (fn goalss => fn rec_Sucs =>
   1.411 +              map2 (fn k => fn goals =>
   1.412 +                map2 (fn goal => fn rec_Suc =>
   1.413 +                  Goal.prove_sorry lthy [] [] goal
   1.414 +                    (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
   1.415 +                      mk_set_Jset_incl_Jset_tac n rec_Suc k)
   1.416 +                  |> Thm.close_derivation)
   1.417 +                goals rec_Sucs)
   1.418 +              ks goalss)
   1.419 +            set_Jset_incl_Jset_goalsss col_Sucss)
   1.420 +          end;
   1.421 +    
   1.422 +        val set_incl_Jset_thmss' = transpose dtor_Jset_incl_thmss;
   1.423 +        val set_Jset_incl_Jset_thmsss' = transpose (map transpose dtor_set_Jset_incl_thmsss);
   1.424 +        val set_Jset_thmss = map (map (fn thm => thm RS @{thm set_mp})) dtor_Jset_incl_thmss;
   1.425 +        val set_Jset_Jset_thmsss = map (map (map (fn thm => thm RS @{thm set_mp})))
   1.426 +          dtor_set_Jset_incl_thmsss;
   1.427 +        val set_Jset_thmss' = transpose set_Jset_thmss;
   1.428 +        val set_Jset_Jset_thmsss' = transpose (map transpose set_Jset_Jset_thmsss);
   1.429 +    
   1.430 +        val dtor_Jset_induct_thms =
   1.431 +          let
   1.432 +            val incls =
   1.433 +              maps (map (fn thm => thm RS @{thm subset_Collect_iff})) dtor_Jset_incl_thmss @
   1.434 +                @{thms subset_Collect_iff[OF subset_refl]};
   1.435 +
   1.436 +            val cTs = map (SOME o certifyT lthy) params';    
   1.437 +            fun mk_induct_tinst phis jsets y y' =
   1.438 +              map4 (fn phi => fn jset => fn Jz => fn Jz' =>
   1.439 +                SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
   1.440 +                  HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz))))))
   1.441 +              phis jsets Jzs Jzs';
   1.442 +          in
   1.443 +            map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
   1.444 +              ((set_minimal
   1.445 +                |> Drule.instantiate' cTs (mk_induct_tinst phis jsets y y')
   1.446 +                |> unfold_thms lthy incls) OF
   1.447 +                (replicate n ballI @
   1.448 +                  maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
   1.449 +              |> singleton (Proof_Context.export names_lthy lthy)
   1.450 +              |> rule_by_tactic lthy (ALLGOALS (TRY o etac asm_rl)))
   1.451 +            Jset_minimal_thms set_Jset_incl_Jset_thmsss' Jsetss_by_range ys ys' dtor_set_induct_phiss
   1.452 +          end;
   1.453 +
   1.454          val (dtor_Jset_thmss', dtor_Jset_thmss) =
   1.455            let
   1.456              fun mk_simp_goal relate pas_set act_sets sets dtor z set =
   1.457 @@ -2115,23 +1981,21 @@
   1.458                (fold_rev Logic.all Jzs o HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj)
   1.459                (mk_goals (uncurry mk_leq));
   1.460              val set_le_thmss = map split_conj_thm
   1.461 -              (map4 (fn goal => fn hset_minimal => fn set_hsets => fn set_hset_hsetss =>
   1.462 +              (map4 (fn goal => fn Jset_minimal => fn set_Jsets => fn set_Jset_Jsetss =>
   1.463                  Goal.prove_sorry lthy [] [] goal
   1.464 -                  (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
   1.465 -                    mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss)
   1.466 +                  (K (mk_set_le_tac n Jset_minimal set_Jsets set_Jset_Jsetss))
   1.467                  |> Thm.close_derivation)
   1.468 -              le_goals hset_minimal_thms set_hset_thmss' set_hset_hset_thmsss');
   1.469 +              le_goals Jset_minimal_thms set_Jset_thmss' set_Jset_Jset_thmsss');
   1.470  
   1.471              val ge_goalss = map (map2 (fn z => fn goal =>
   1.472                  Logic.all z (HOLogic.mk_Trueprop goal)) Jzs)
   1.473                (mk_goals (uncurry mk_leq o swap));
   1.474              val set_ge_thmss = 
   1.475 -              map3 (map3 (fn goal => fn set_incl_hset => fn set_hset_incl_hsets =>
   1.476 +              map3 (map3 (fn goal => fn set_incl_Jset => fn set_Jset_incl_Jsets =>
   1.477                  Goal.prove_sorry lthy [] [] goal
   1.478 -                  (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
   1.479 -                    mk_set_ge_tac n set_incl_hset set_hset_incl_hsets)
   1.480 +                  (K (mk_set_ge_tac n set_incl_Jset set_Jset_incl_Jsets))
   1.481                  |> Thm.close_derivation))
   1.482 -              ge_goalss set_incl_hset_thmss' set_hset_incl_hset_thmsss'
   1.483 +              ge_goalss set_incl_Jset_thmss' set_Jset_incl_Jset_thmsss'
   1.484            in
   1.485              map2 (map2 (fn le => fn ge => equalityI OF [le, ge])) set_le_thmss set_ge_thmss
   1.486              |> `transpose
   1.487 @@ -2222,8 +2086,7 @@
   1.488              val cphis = map9 mk_cphi
   1.489                Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy;
   1.490  
   1.491 -            val coinduct = unfold_thms lthy Jset_defs
   1.492 -              (Drule.instantiate' cTs (map SOME cphis) dtor_coinduct_thm);
   1.493 +            val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_coinduct_thm;
   1.494  
   1.495              val goal =
   1.496                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   1.497 @@ -2231,9 +2094,8 @@
   1.498  
   1.499              val thm = singleton (Proof_Context.export names_lthy lthy)
   1.500                (Goal.prove_sorry lthy [] [] goal
   1.501 -                (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
   1.502 -                  mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_Jmap_thms map_cong0s
   1.503 -                    set_mapss set_hset_thmss set_hset_hset_thmsss in_rels))
   1.504 +                (K (mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_Jmap_thms map_cong0s
   1.505 +                  set_mapss set_Jset_thmss set_Jset_Jset_thmsss in_rels)))
   1.506                |> Thm.close_derivation
   1.507            in
   1.508              split_conj_thm thm
   1.509 @@ -2242,12 +2104,6 @@
   1.510          val in_Jrels = map (fn def => trans OF [def, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD})
   1.511              Jrel_unabs_defs;
   1.512  
   1.513 -        val fold_Jsets = fold_thms lthy Jset_unabs_defs;
   1.514 -        val dtor_Jset_incl_thmss = map (map fold_Jsets) set_incl_hset_thmss;
   1.515 -        val dtor_set_Jset_incl_thmsss = map (map (map fold_Jsets)) set_hset_incl_hset_thmsss;
   1.516 -        val dtor_Jset_induct_thms = map fold_Jsets dtor_hset_induct_thms;
   1.517 -        val Jwit_thmss = map (map fold_Jsets) wit_thmss;
   1.518 -
   1.519          val Jrels = mk_Jrels passiveAs passiveBs;
   1.520          val Jrelphis = map (fn rel => Term.list_comb (rel, Jphis)) Jrels;
   1.521          val relphis = map (fn rel => Term.list_comb (rel, Jphis @ Jrelphis)) rels;
   1.522 @@ -2413,6 +2269,140 @@
   1.523  
   1.524          val timer = time (timer "helpers for BNF properties");
   1.525  
   1.526 +        fun close_wit I wit = (I, fold_rev Term.absfree (map (nth ys') I) wit);
   1.527 +
   1.528 +        val all_unitTs = replicate live HOLogic.unitT;
   1.529 +        val unitTs = replicate n HOLogic.unitT;
   1.530 +        val unit_funs = replicate n (Term.absdummy HOLogic.unitT HOLogic.unit);
   1.531 +        fun mk_map_args I =
   1.532 +          map (fn i =>
   1.533 +            if member (op =) I i then Term.absdummy HOLogic.unitT (nth ys i)
   1.534 +            else mk_undefined (HOLogic.unitT --> nth passiveAs i))
   1.535 +          (0 upto (m - 1));
   1.536 +
   1.537 +        fun mk_nat_wit Ds bnf (I, wit) () =
   1.538 +          let
   1.539 +            val passiveI = filter (fn i => i < m) I;
   1.540 +            val map_args = mk_map_args passiveI;
   1.541 +          in
   1.542 +            Term.absdummy HOLogic.unitT (Term.list_comb
   1.543 +              (mk_map_of_bnf Ds all_unitTs (passiveAs @ unitTs) bnf, map_args @ unit_funs) $ wit)
   1.544 +          end;
   1.545 +
   1.546 +        fun mk_dummy_wit Ds bnf I =
   1.547 +          let
   1.548 +            val map_args = mk_map_args I;
   1.549 +          in
   1.550 +            Term.absdummy HOLogic.unitT (Term.list_comb
   1.551 +              (mk_map_of_bnf Ds all_unitTs (passiveAs @ unitTs) bnf, map_args @ unit_funs) $
   1.552 +              mk_undefined (mk_T_of_bnf Ds all_unitTs bnf))
   1.553 +          end;
   1.554 +
   1.555 +        val nat_witss =
   1.556 +          map2 (fn Ds => fn bnf => mk_wits_of_bnf (replicate (nwits_of_bnf bnf) Ds)
   1.557 +            (replicate (nwits_of_bnf bnf) (replicate live HOLogic.unitT)) bnf
   1.558 +            |> map (fn (I, wit) =>
   1.559 +              (I, Lazy.lazy (mk_nat_wit Ds bnf (I, Term.list_comb (wit, map (K HOLogic.unit) I))))))
   1.560 +          Dss bnfs;
   1.561 +
   1.562 +        val nat_wit_thmss = map2 (curry op ~~) nat_witss (map wit_thmss_of_bnf bnfs)
   1.563 +
   1.564 +        val Iss = map (map fst) nat_witss;
   1.565 +
   1.566 +        fun filter_wits (I, wit) =
   1.567 +          let val J = filter (fn i => i < m) I;
   1.568 +          in (J, (length J < length I, wit)) end;
   1.569 +
   1.570 +        val wit_treess = map_index (fn (i, Is) =>
   1.571 +          map_index (finish Iss m [i+m] (i+m)) Is) Iss
   1.572 +          |> map (minimize_wits o map filter_wits o minimize_wits o flat);
   1.573 +
   1.574 +        val coind_wit_argsss =
   1.575 +          map (map (tree_to_coind_wits nat_wit_thmss o snd o snd) o filter (fst o snd)) wit_treess;
   1.576 +
   1.577 +        val nonredundant_coind_wit_argsss =
   1.578 +          fold (fn i => fn argsss =>
   1.579 +            nth_map (i - 1) (filter_out (fn xs =>
   1.580 +              exists (fn ys =>
   1.581 +                let
   1.582 +                  val xs' = (map (fst o fst) xs, snd (fst (hd xs)));
   1.583 +                  val ys' = (map (fst o fst) ys, snd (fst (hd ys)));
   1.584 +                in
   1.585 +                  eq_pair (subset (op =)) (eq_set (op =)) (xs', ys') andalso not (fst xs' = fst ys')
   1.586 +                end)
   1.587 +              (flat argsss)))
   1.588 +            argsss)
   1.589 +          ks coind_wit_argsss;
   1.590 +
   1.591 +        fun prepare_args args =
   1.592 +          let
   1.593 +            val I = snd (fst (hd args));
   1.594 +            val (dummys, args') =
   1.595 +              map_split (fn i =>
   1.596 +                (case find_first (fn arg => fst (fst arg) = i - 1) args of
   1.597 +                  SOME (_, ((_, wit), thms)) => (NONE, (Lazy.force wit, thms))
   1.598 +                | NONE =>
   1.599 +                  (SOME (i - 1), (mk_dummy_wit (nth Dss (i - 1)) (nth bnfs (i - 1)) I, []))))
   1.600 +              ks;
   1.601 +          in
   1.602 +            ((I, dummys), apsnd flat (split_list args'))
   1.603 +          end;
   1.604 +
   1.605 +        fun mk_coind_wits ((I, dummys), (args, thms)) =
   1.606 +          ((I, dummys), (map (fn i => mk_unfold Ts args i $ HOLogic.unit) ks, thms));
   1.607 +
   1.608 +        val coind_witss =
   1.609 +          maps (map (mk_coind_wits o prepare_args)) nonredundant_coind_wit_argsss;
   1.610 +
   1.611 +        val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf
   1.612 +          (replicate (nwits_of_bnf bnf) Ds)
   1.613 +          (replicate (nwits_of_bnf bnf) (passiveAs @ Ts)) bnf) Dss bnfs;
   1.614 +
   1.615 +        val ctor_witss =
   1.616 +          map (map (uncurry close_wit o tree_to_ctor_wit ys ctors witss o snd o snd) o
   1.617 +            filter_out (fst o snd)) wit_treess;
   1.618 +
   1.619 +        fun mk_coind_wit_thms ((I, dummys), (wits, wit_thms)) =
   1.620 +          let
   1.621 +            fun mk_goal sets y y_copy y'_copy j =
   1.622 +              let
   1.623 +                fun mk_conjunct set z dummy wit =
   1.624 +                  mk_Ball (set $ z) (Term.absfree y'_copy
   1.625 +                    (if dummy = NONE orelse member (op =) I (j - 1) then
   1.626 +                      HOLogic.mk_imp (HOLogic.mk_eq (z, wit),
   1.627 +                        if member (op =) I (j - 1) then HOLogic.mk_eq (y_copy, y)
   1.628 +                        else @{term False})
   1.629 +                    else @{term True}));
   1.630 +              in
   1.631 +                fold_rev Logic.all (map (nth ys) I @ Jzs) (HOLogic.mk_Trueprop
   1.632 +                  (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct sets Jzs dummys wits)))
   1.633 +              end;
   1.634 +            val goals = map5 mk_goal Jsetss_by_range ys ys_copy ys'_copy ls;
   1.635 +          in
   1.636 +            map2 (fn goal => fn induct =>
   1.637 +              Goal.prove_sorry lthy [] [] goal
   1.638 +                (fn {context = ctxt, prems = _} => mk_coind_wit_tac ctxt induct dtor_unfold_thms
   1.639 +                  (flat set_mapss) wit_thms)
   1.640 +              |> Thm.close_derivation)
   1.641 +            goals dtor_Jset_induct_thms
   1.642 +            |> map split_conj_thm
   1.643 +            |> transpose
   1.644 +            |> map (map_filter (try (fn thm => thm RS bspec RS mp)))
   1.645 +            |> curry op ~~ (map_index Library.I (map (close_wit I) wits))
   1.646 +            |> filter (fn (_, thms) => length thms = m)
   1.647 +          end;
   1.648 +
   1.649 +        val coind_wit_thms = maps mk_coind_wit_thms coind_witss;
   1.650 +
   1.651 +        val (wit_thmss, all_witss) =
   1.652 +          fold (fn ((i, wit), thms) => fn witss =>
   1.653 +            nth_map i (fn (thms', wits) => (thms @ thms', wit :: wits)) witss)
   1.654 +          coind_wit_thms (map (pair []) ctor_witss)
   1.655 +          |> map (apsnd (map snd o minimize_wits))
   1.656 +          |> split_list;
   1.657 +
   1.658 +        val timer = time (timer "witnesses");
   1.659 +
   1.660          val map_id0_tacs =
   1.661            map2 (K oo mk_map_id0_tac Jmap_thms) dtor_unfold_unique_thms unfold_dtor_thms;
   1.662          val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) Jmap_comp0_thms;
   1.663 @@ -2439,17 +2429,17 @@
   1.664          val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
   1.665            bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
   1.666  
   1.667 -        fun wit_tac thms ctxt = unfold_thms_tac ctxt (flat Jwit_defss) THEN
   1.668 +        fun wit_tac thms ctxt =
   1.669            mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms;
   1.670  
   1.671          val (Jbnfs, lthy) =
   1.672 -          fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn Jwit_thms =>
   1.673 +          fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms =>
   1.674                fn consts => fn lthy =>
   1.675 -            bnf_def Do_Inline (user_policy Note_Some) false I tacs (wit_tac Jwit_thms) (SOME deads)
   1.676 -              map_b rel_b set_bs consts lthy
   1.677 +            bnf_def Hardly_Inline (user_policy Note_Some) false I tacs (wit_tac wit_thms)
   1.678 +              (SOME deads) map_b rel_b set_bs consts lthy
   1.679              |> register_bnf (Local_Theory.full_name lthy b))
   1.680 -          bs tacss map_bs rel_bs set_bss Jwit_thmss
   1.681 -          ((((((bs ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ Jwitss) ~~ map SOME Jrels)
   1.682 +          bs tacss map_bs rel_bs set_bss wit_thmss
   1.683 +          ((((((bs ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ all_witss) ~~ map SOME Jrels)
   1.684            lthy;
   1.685  
   1.686          val timer = time (timer "registered new codatatypes as BNFs");
     2.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Mar 17 15:48:30 2014 +0000
     2.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Mar 17 17:35:39 2014 +0100
     2.3 @@ -32,7 +32,7 @@
     2.4      thm -> thm -> thm list -> thm list -> thm list list -> tactic
     2.5    val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic
     2.6    val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
     2.7 -  val mk_hset_minimal_tac: Proof.context -> int -> thm -> tactic
     2.8 +  val mk_Jset_minimal_tac: Proof.context -> int -> thm -> tactic
     2.9    val mk_col_minimal_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
    2.10      tactic
    2.11    val mk_incl_lsbis_tac: int -> int -> thm -> tactic
    2.12 @@ -75,10 +75,10 @@
    2.13    val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
    2.14      thm list -> thm list list -> tactic
    2.15    val mk_set_bd_tac: thm -> thm -> tactic
    2.16 -  val mk_set_hset_incl_hset_tac: int -> thm -> int -> tactic
    2.17 +  val mk_set_Jset_incl_Jset_tac: int -> thm -> int -> tactic
    2.18    val mk_set_image_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list ->
    2.19      thm list -> thm list -> thm list list -> thm list list -> tactic
    2.20 -  val mk_set_incl_hset_tac: thm -> tactic
    2.21 +  val mk_set_incl_Jset_tac: thm -> tactic
    2.22    val mk_set_ge_tac: int  -> thm -> thm list -> tactic
    2.23    val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
    2.24    val mk_set_map0_tac: thm -> tactic
    2.25 @@ -162,11 +162,11 @@
    2.26  fun mk_mor_case_sum_tac ks mor_UNIV =
    2.27    (rtac (mor_UNIV RS iffD2) THEN' CONJ_WRAP' (K (rtac @{thm case_sum_o_inj(1)[symmetric]})) ks) 1;
    2.28  
    2.29 -fun mk_set_incl_hset_tac rec_Suc =
    2.30 +fun mk_set_incl_Jset_tac rec_Suc =
    2.31    EVERY' (map rtac [@{thm SUP_upper2}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1}, sym,
    2.32      rec_Suc]) 1;
    2.33  
    2.34 -fun mk_set_hset_incl_hset_tac n rec_Suc i =
    2.35 +fun mk_set_Jset_incl_Jset_tac n rec_Suc i =
    2.36    EVERY' (map rtac [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2, rec_Suc,
    2.37        UnI2, mk_UnIN n i] @ [etac @{thm UN_I}, atac]) 1;
    2.38  
    2.39 @@ -185,7 +185,7 @@
    2.40              rtac subset_trans, atac, Goal.assume_rule_tac ctxt])) rec_0s])
    2.41        rec_Sucs] 1;
    2.42  
    2.43 -fun mk_hset_minimal_tac ctxt n col_minimal =
    2.44 +fun mk_Jset_minimal_tac ctxt n col_minimal =
    2.45    (CONJ_WRAP' (K (EVERY' [rtac @{thm UN_least}, rtac rev_mp, rtac col_minimal,
    2.46      EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI,
    2.47      REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) (1 upto n)) 1
    2.48 @@ -777,20 +777,20 @@
    2.49      REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
    2.50      rtac map_arg_cong, rtac (o_apply RS sym)] 1;
    2.51  
    2.52 -fun mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss =
    2.53 -  EVERY' [rtac hset_minimal,
    2.54 +fun mk_set_le_tac n Jset_minimal set_Jsets set_Jset_Jsetss =
    2.55 +  EVERY' [rtac Jset_minimal,
    2.56      REPEAT_DETERM_N n o rtac @{thm Un_upper1},
    2.57      REPEAT_DETERM_N n o
    2.58 -      EVERY' (map3 (fn i => fn set_hset => fn set_hset_hsets =>
    2.59 +      EVERY' (map3 (fn i => fn set_Jset => fn set_Jset_Jsets =>
    2.60          EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnIN n i), etac @{thm UN_I},
    2.61 -          etac UnE, etac set_hset, REPEAT_DETERM_N (n - 1) o etac UnE,
    2.62 -          EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_hset_hsets)])
    2.63 -      (1 upto n) set_hsets set_hset_hsetss)] 1;
    2.64 +          etac UnE, etac set_Jset, REPEAT_DETERM_N (n - 1) o etac UnE,
    2.65 +          EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_Jset_Jsets)])
    2.66 +      (1 upto n) set_Jsets set_Jset_Jsetss)] 1;
    2.67  
    2.68 -fun mk_set_ge_tac n set_incl_hset set_hset_incl_hsets =
    2.69 -  EVERY' [rtac @{thm Un_least}, rtac set_incl_hset,
    2.70 +fun mk_set_ge_tac n set_incl_Jset set_Jset_incl_Jsets =
    2.71 +  EVERY' [rtac @{thm Un_least}, rtac set_incl_Jset,
    2.72      REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
    2.73 -    EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
    2.74 +    EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_Jset_incl_Jsets)] 1;
    2.75  
    2.76  fun mk_map_id0_tac maps unfold_unique unfold_dtor =
    2.77    EVERY' [rtac (unfold_unique RS trans), EVERY' (map (rtac o mk_sym) maps),
    2.78 @@ -807,15 +807,15 @@
    2.79          @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl]]))
    2.80      maps map_comp0s)] 1;
    2.81  
    2.82 -fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_hsetss
    2.83 -  set_hset_hsetsss in_rels =
    2.84 +fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_Jsetss
    2.85 +  set_Jset_Jsetsss in_rels =
    2.86    let
    2.87      val n = length map_comps;
    2.88      val ks = 1 upto n;
    2.89    in
    2.90      EVERY' ([rtac rev_mp, coinduct_tac] @
    2.91 -      maps (fn ((((((map_comp_trans, dtor_maps_trans), map_cong0), set_map0s), set_hsets),
    2.92 -        set_hset_hsetss), in_rel) =>
    2.93 +      maps (fn ((((((map_comp_trans, dtor_maps_trans), map_cong0), set_map0s), set_Jsets),
    2.94 +        set_Jset_Jsetss), in_rel) =>
    2.95          [REPEAT_DETERM o resolve_tac [allI, impI, in_rel RS iffD2],
    2.96           REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI,
    2.97           rtac (Drule.rotate_prems 1 conjI),
    2.98 @@ -823,25 +823,25 @@
    2.99           REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac @{thm fst_conv}),
   2.100           REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
   2.101           rtac map_comp_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
   2.102 -         EVERY' (maps (fn set_hset =>
   2.103 +         EVERY' (maps (fn set_Jset =>
   2.104             [rtac o_apply_trans_sym, rtac (@{thm snd_conv} RS trans), etac CollectE,
   2.105 -           REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
   2.106 +           REPEAT_DETERM o etac conjE, etac bspec, etac set_Jset]) set_Jsets),
   2.107           REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym,
   2.108           rtac CollectI,
   2.109           EVERY' (map (fn set_map0 => EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map0,
   2.110             rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm case_prodI}, rtac refl])
   2.111          (take m set_map0s)),
   2.112 -         CONJ_WRAP' (fn (set_map0, set_hset_hsets) =>
   2.113 +         CONJ_WRAP' (fn (set_map0, set_Jset_Jsets) =>
   2.114             EVERY' [rtac ord_eq_le_trans, rtac set_map0,
   2.115               rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm case_prodI}, rtac exI, rtac conjI,
   2.116               rtac CollectI, etac CollectE,
   2.117               REPEAT_DETERM o etac conjE,
   2.118 -             CONJ_WRAP' (fn set_hset_hset =>
   2.119 -               EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets,
   2.120 +             CONJ_WRAP' (fn set_Jset_Jset =>
   2.121 +               EVERY' [rtac ballI, etac bspec, etac set_Jset_Jset, atac]) set_Jset_Jsets,
   2.122               rtac (conjI OF [refl, refl])])
   2.123 -           (drop m set_map0s ~~ set_hset_hsetss)])
   2.124 +           (drop m set_map0s ~~ set_Jset_Jsetss)])
   2.125          (map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~
   2.126 -          map_cong0s ~~ set_map0ss ~~ set_hsetss ~~ set_hset_hsetsss ~~ in_rels) @
   2.127 +          map_cong0s ~~ set_map0ss ~~ set_Jsetss ~~ set_Jset_Jsetsss ~~ in_rels) @
   2.128        [rtac impI,
   2.129         CONJ_WRAP' (fn k =>
   2.130           EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI,