added countable tactic for new-style datatypes
authorblanchet
Wed Sep 03 00:31:38 2014 +0200 (2014-09-03)
changeset 58160e4965b677ba9
parent 58159 e3d1912a0c8f
child 58161 deeff89d5b9e
added countable tactic for new-style datatypes
src/HOL/Library/Countable.thy
src/HOL/Library/bnf_lfp_countable.ML
     1.1 --- a/src/HOL/Library/Countable.thy	Wed Sep 03 00:31:37 2014 +0200
     1.2 +++ b/src/HOL/Library/Countable.thy	Wed Sep 03 00:31:38 2014 +0200
     1.3 @@ -1,6 +1,7 @@
     1.4  (*  Title:      HOL/Library/Countable.thy
     1.5      Author:     Alexander Krauss, TU Muenchen
     1.6      Author:     Brian Huffman, Portland State University
     1.7 +    Author:     Jasmin Blanchette, TU Muenchen
     1.8  *)
     1.9  
    1.10  header {* Encoding (almost) everything into natural numbers *}
    1.11 @@ -49,10 +50,7 @@
    1.12    by (simp add: from_nat_def)
    1.13  
    1.14  
    1.15 -subsection {* Countable types *}
    1.16 -
    1.17 -instance nat :: countable
    1.18 -  by (rule countable_classI [of "id"]) simp
    1.19 +subsection {* Finite types are countable *}
    1.20  
    1.21  subclass (in finite) countable
    1.22  proof
    1.23 @@ -65,113 +63,8 @@
    1.24    then show "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat" by (rule exI[of inj])
    1.25  qed
    1.26  
    1.27 -text {* Pairs *}
    1.28  
    1.29 -instance prod :: (countable, countable) countable
    1.30 -  by (rule countable_classI [of "\<lambda>(x, y). prod_encode (to_nat x, to_nat y)"])
    1.31 -    (auto simp add: prod_encode_eq)
    1.32 -
    1.33 -
    1.34 -text {* Sums *}
    1.35 -
    1.36 -instance sum :: (countable, countable) countable
    1.37 -  by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a)
    1.38 -                                     | Inr b \<Rightarrow> to_nat (True, to_nat b))"])
    1.39 -    (simp split: sum.split_asm)
    1.40 -
    1.41 -
    1.42 -text {* Integers *}
    1.43 -
    1.44 -instance int :: countable
    1.45 -  by (rule countable_classI [of "int_encode"])
    1.46 -    (simp add: int_encode_eq)
    1.47 -
    1.48 -
    1.49 -text {* Options *}
    1.50 -
    1.51 -instance option :: (countable) countable
    1.52 -  by (rule countable_classI [of "case_option 0 (Suc \<circ> to_nat)"])
    1.53 -    (simp split: option.split_asm)
    1.54 -
    1.55 -
    1.56 -text {* Lists *}
    1.57 -
    1.58 -instance list :: (countable) countable
    1.59 -  by (rule countable_classI [of "list_encode \<circ> map to_nat"])
    1.60 -    (simp add: list_encode_eq)
    1.61 -
    1.62 -
    1.63 -text {* Further *}
    1.64 -
    1.65 -instance String.literal :: countable
    1.66 -  by (rule countable_classI [of "to_nat o String.explode"])
    1.67 -    (auto simp add: explode_inject)
    1.68 -
    1.69 -text {* Functions *}
    1.70 -
    1.71 -instance "fun" :: (finite, countable) countable
    1.72 -proof
    1.73 -  obtain xs :: "'a list" where xs: "set xs = UNIV"
    1.74 -    using finite_list [OF finite_UNIV] ..
    1.75 -  show "\<exists>to_nat::('a \<Rightarrow> 'b) \<Rightarrow> nat. inj to_nat"
    1.76 -  proof
    1.77 -    show "inj (\<lambda>f. to_nat (map f xs))"
    1.78 -      by (rule injI, simp add: xs fun_eq_iff)
    1.79 -  qed
    1.80 -qed
    1.81 -
    1.82 -
    1.83 -subsection {* The Rationals are Countably Infinite *}
    1.84 -
    1.85 -definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where
    1.86 -"nat_to_rat_surj n = (let (a,b) = prod_decode n
    1.87 -                      in Fract (int_decode a) (int_decode b))"
    1.88 -
    1.89 -lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj"
    1.90 -unfolding surj_def
    1.91 -proof
    1.92 -  fix r::rat
    1.93 -  show "\<exists>n. r = nat_to_rat_surj n"
    1.94 -  proof (cases r)
    1.95 -    fix i j assume [simp]: "r = Fract i j" and "j > 0"
    1.96 -    have "r = (let m = int_encode i; n = int_encode j
    1.97 -               in nat_to_rat_surj(prod_encode (m,n)))"
    1.98 -      by (simp add: Let_def nat_to_rat_surj_def)
    1.99 -    thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def)
   1.100 -  qed
   1.101 -qed
   1.102 -
   1.103 -lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj"
   1.104 -by (simp add: Rats_def surj_nat_to_rat_surj)
   1.105 -
   1.106 -context field_char_0
   1.107 -begin
   1.108 -
   1.109 -lemma Rats_eq_range_of_rat_o_nat_to_rat_surj:
   1.110 -  "\<rat> = range (of_rat o nat_to_rat_surj)"
   1.111 -using surj_nat_to_rat_surj
   1.112 -by (auto simp: Rats_def image_def surj_def)
   1.113 -   (blast intro: arg_cong[where f = of_rat])
   1.114 -
   1.115 -lemma surj_of_rat_nat_to_rat_surj:
   1.116 -  "r\<in>\<rat> \<Longrightarrow> \<exists>n. r = of_rat(nat_to_rat_surj n)"
   1.117 -by(simp add: Rats_eq_range_of_rat_o_nat_to_rat_surj image_def)
   1.118 -
   1.119 -end
   1.120 -
   1.121 -instance rat :: countable
   1.122 -proof
   1.123 -  show "\<exists>to_nat::rat \<Rightarrow> nat. inj to_nat"
   1.124 -  proof
   1.125 -    have "surj nat_to_rat_surj"
   1.126 -      by (rule surj_nat_to_rat_surj)
   1.127 -    then show "inj (inv nat_to_rat_surj)"
   1.128 -      by (rule surj_imp_inj_inv)
   1.129 -  qed
   1.130 -qed
   1.131 -
   1.132 -
   1.133 -subsection {* Automatically proving countability of datatypes *}
   1.134 +subsection {* Automatically proving countability of old-style datatypes *}
   1.135  
   1.136  inductive finite_item :: "'a Old_Datatype.item \<Rightarrow> bool" where
   1.137    undefined: "finite_item undefined"
   1.138 @@ -268,8 +161,8 @@
   1.139  qed
   1.140  
   1.141  ML {*
   1.142 -  fun countable_tac ctxt =
   1.143 -    SUBGOAL (fn (goal, i) =>
   1.144 +  fun old_countable_tac ctxt =
   1.145 +    SUBGOAL (fn (goal, _) =>
   1.146        let
   1.147          val ty_name =
   1.148            (case goal of
   1.149 @@ -279,7 +172,7 @@
   1.150          val typedef_thm = #type_definition (snd typedef_info)
   1.151          val pred_name =
   1.152            (case HOLogic.dest_Trueprop (concl_of typedef_thm) of
   1.153 -            (typedef $ rep $ abs $ (collect $ Const (n, _))) => n
   1.154 +            (_ $ _ $ _ $ (_ $ Const (n, _))) => n
   1.155            | _ => raise Match)
   1.156          val induct_info = Inductive.the_inductive ctxt pred_name
   1.157          val pred_names = #names (fst induct_info)
   1.158 @@ -301,33 +194,124 @@
   1.159        end)
   1.160  *}
   1.161  
   1.162 -method_setup countable_datatype = {*
   1.163 -  Scan.succeed (fn ctxt => SIMPLE_METHOD' (countable_tac ctxt))
   1.164 -*} "prove countable class instances for datatypes"
   1.165 -
   1.166  hide_const (open) finite_item nth_item
   1.167  
   1.168  
   1.169 -subsection {* Countable datatypes *}
   1.170 +subsection {* Automatically proving countability of new-style datatypes *}
   1.171 +
   1.172 +ML_file "bnf_lfp_countable.ML"
   1.173 +
   1.174 +method_setup countable_datatype = {*
   1.175 +  Scan.succeed (fn ctxt =>
   1.176 +    SIMPLE_METHOD (fn st => HEADGOAL (old_countable_tac ctxt) st
   1.177 +      handle ERROR _ => BNF_LFP_Countable.countable_tac ctxt st))
   1.178 +*} "prove countable class instances for datatypes"
   1.179 +
   1.180 +
   1.181 +subsection {* More Countable types *}
   1.182 +
   1.183 +text {* Naturals *}
   1.184  
   1.185 -(* TODO: automate *)
   1.186 +instance nat :: countable
   1.187 +  by (rule countable_classI [of "id"]) simp
   1.188 +
   1.189 +text {* Pairs *}
   1.190 +
   1.191 +instance prod :: (countable, countable) countable
   1.192 +  by (rule countable_classI [of "\<lambda>(x, y). prod_encode (to_nat x, to_nat y)"])
   1.193 +    (auto simp add: prod_encode_eq)
   1.194  
   1.195 -primrec encode_typerep :: "typerep \<Rightarrow> nat" where
   1.196 -  "encode_typerep (Typerep.Typerep s ts) = prod_encode (to_nat s, to_nat (map encode_typerep ts))"
   1.197 +text {* Sums *}
   1.198 +
   1.199 +instance sum :: (countable, countable) countable
   1.200 +  by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a)
   1.201 +                                     | Inr b \<Rightarrow> to_nat (True, to_nat b))"])
   1.202 +    (simp split: sum.split_asm)
   1.203 +
   1.204 +text {* Integers *}
   1.205  
   1.206 -lemma encode_typerep_injective: "\<forall>u. encode_typerep t = encode_typerep u \<longrightarrow> t = u"
   1.207 -  apply (induct t)
   1.208 -  apply (rule allI)
   1.209 -  apply (case_tac u)
   1.210 -  apply (auto simp: sum_encode_eq prod_encode_eq elim: list.inj_map_strong[rotated 1])
   1.211 -  done
   1.212 +instance int :: countable
   1.213 +  by (rule countable_classI [of int_encode]) (simp add: int_encode_eq)
   1.214 +
   1.215 +text {* Options *}
   1.216 +
   1.217 +instance option :: (countable) countable
   1.218 +  by countable_datatype
   1.219 +
   1.220 +text {* Lists *}
   1.221 +
   1.222 +instance list :: (countable) countable
   1.223 +  by countable_datatype
   1.224 +
   1.225 +text {* String literals *}
   1.226 +
   1.227 +instance String.literal :: countable
   1.228 +  by (rule countable_classI [of "to_nat o String.explode"]) (auto simp add: explode_inject)
   1.229 +
   1.230 +text {* Functions *}
   1.231 +
   1.232 +instance "fun" :: (finite, countable) countable
   1.233 +proof
   1.234 +  obtain xs :: "'a list" where xs: "set xs = UNIV"
   1.235 +    using finite_list [OF finite_UNIV] ..
   1.236 +  show "\<exists>to_nat::('a \<Rightarrow> 'b) \<Rightarrow> nat. inj to_nat"
   1.237 +  proof
   1.238 +    show "inj (\<lambda>f. to_nat (map f xs))"
   1.239 +      by (rule injI, simp add: xs fun_eq_iff)
   1.240 +  qed
   1.241 +qed
   1.242 +
   1.243 +text {* Typereps *}
   1.244  
   1.245  instance typerep :: countable
   1.246 -  apply default
   1.247 -  apply (unfold inj_on_def ball_UNIV)
   1.248 -  apply (rule exI)
   1.249 -  apply (rule allI)
   1.250 -  apply (rule encode_typerep_injective)
   1.251 -  done
   1.252 +  by countable_datatype
   1.253 +
   1.254 +
   1.255 +subsection {* The rationals are countably infinite *}
   1.256 +
   1.257 +definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where
   1.258 +  "nat_to_rat_surj n = (let (a, b) = prod_decode n in Fract (int_decode a) (int_decode b))"
   1.259 +
   1.260 +lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj"
   1.261 +unfolding surj_def
   1.262 +proof
   1.263 +  fix r::rat
   1.264 +  show "\<exists>n. r = nat_to_rat_surj n"
   1.265 +  proof (cases r)
   1.266 +    fix i j assume [simp]: "r = Fract i j" and "j > 0"
   1.267 +    have "r = (let m = int_encode i; n = int_encode j
   1.268 +               in nat_to_rat_surj(prod_encode (m,n)))"
   1.269 +      by (simp add: Let_def nat_to_rat_surj_def)
   1.270 +    thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def)
   1.271 +  qed
   1.272 +qed
   1.273 +
   1.274 +lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj"
   1.275 +  by (simp add: Rats_def surj_nat_to_rat_surj)
   1.276 +
   1.277 +context field_char_0
   1.278 +begin
   1.279 +
   1.280 +lemma Rats_eq_range_of_rat_o_nat_to_rat_surj:
   1.281 +  "\<rat> = range (of_rat o nat_to_rat_surj)"
   1.282 +  using surj_nat_to_rat_surj
   1.283 +  by (auto simp: Rats_def image_def surj_def) (blast intro: arg_cong[where f = of_rat])
   1.284 +
   1.285 +lemma surj_of_rat_nat_to_rat_surj:
   1.286 +  "r\<in>\<rat> \<Longrightarrow> \<exists>n. r = of_rat(nat_to_rat_surj n)"
   1.287 +  by (simp add: Rats_eq_range_of_rat_o_nat_to_rat_surj image_def)
   1.288  
   1.289  end
   1.290 +
   1.291 +instance rat :: countable
   1.292 +proof
   1.293 +  show "\<exists>to_nat::rat \<Rightarrow> nat. inj to_nat"
   1.294 +  proof
   1.295 +    have "surj nat_to_rat_surj"
   1.296 +      by (rule surj_nat_to_rat_surj)
   1.297 +    then show "inj (inv nat_to_rat_surj)"
   1.298 +      by (rule surj_imp_inj_inv)
   1.299 +  qed
   1.300 +qed
   1.301 +
   1.302 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/bnf_lfp_countable.ML	Wed Sep 03 00:31:38 2014 +0200
     2.3 @@ -0,0 +1,183 @@
     2.4 +(*  Title:      HOL/Library/bnf_lfp_countable.ML
     2.5 +    Author:     Jasmin Blanchette, TU Muenchen
     2.6 +    Copyright   2014
     2.7 +
     2.8 +Countability tactic for BNF datatypes.
     2.9 +*)
    2.10 +
    2.11 +signature BNF_LFP_COUNTABLE =
    2.12 +sig
    2.13 +  val countable_tac: Proof.context -> tactic
    2.14 +end;
    2.15 +
    2.16 +structure BNF_LFP_Countable : BNF_LFP_COUNTABLE =
    2.17 +struct
    2.18 +
    2.19 +open BNF_FP_Rec_Sugar_Util
    2.20 +open BNF_Def
    2.21 +open BNF_Util
    2.22 +open BNF_Tactics
    2.23 +open BNF_FP_Util
    2.24 +open BNF_FP_Def_Sugar
    2.25 +
    2.26 +fun nchotomy_tac nchotomy =
    2.27 +  HEADGOAL (rtac (nchotomy RS @{thm all_reg[rotated]}) THEN'
    2.28 +    CHANGED_PROP o REPEAT_ALL_NEW (match_tac [allI, impI]) THEN'
    2.29 +    CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac [exE, disjE]));
    2.30 +
    2.31 +fun meta_spec_mp_tac 0 = K all_tac
    2.32 +  | meta_spec_mp_tac n =
    2.33 +    dtac meta_spec THEN' meta_spec_mp_tac (n - 1) THEN' dtac meta_mp THEN' atac;
    2.34 +
    2.35 +val use_induction_hypothesis_tac =
    2.36 +  DEEPEN (1, 1000000 (* large number *))
    2.37 +    (fn depth => meta_spec_mp_tac depth THEN' etac allE THEN' etac impE THEN' atac THEN' atac) 0;
    2.38 +
    2.39 +val same_ctr_simps =
    2.40 +  @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split simp_thms snd_conv};
    2.41 +
    2.42 +fun same_ctr_tac ctxt injects recs map_comps' inj_map_strongs' =
    2.43 +  HEADGOAL (asm_full_simp_tac (ss_only (injects @ recs @ map_comps' @ same_ctr_simps) ctxt) THEN'
    2.44 +    REPEAT_DETERM o CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac (conjE :: inj_map_strongs'))
    2.45 +    THEN_ALL_NEW use_induction_hypothesis_tac);
    2.46 +
    2.47 +fun distinct_ctrs_tac ctxt recs =
    2.48 +  HEADGOAL (asm_full_simp_tac (ss_only (recs @
    2.49 +    @{thms sum_encode_eq sum.inject sum.distinct simp_thms}) ctxt));
    2.50 +
    2.51 +fun mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs' =
    2.52 +  let val ks = 1 upto n in
    2.53 +    EVERY (maps (fn k => nchotomy_tac nchotomy :: map (fn k' =>
    2.54 +      if k = k' then same_ctr_tac ctxt injects recs map_comps' inj_map_strongs'
    2.55 +      else distinct_ctrs_tac ctxt recs) ks) ks)
    2.56 +  end;
    2.57 +
    2.58 +fun mk_encode_injectives_tac ctxt ns induct nchotomys injectss recss map_comps' inj_map_strongs' =
    2.59 +  HEADGOAL (rtac induct) THEN
    2.60 +  EVERY (map4 (fn n => fn nchotomy => fn injects => fn recs =>
    2.61 +      mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs')
    2.62 +    ns nchotomys injectss recss);
    2.63 +
    2.64 +fun endgame_tac ctxt encode_injectives =
    2.65 +  unfold_thms_tac ctxt @{thms inj_on_def ball_UNIV} THEN
    2.66 +  ALLGOALS (rtac exI THEN' rtac allI THEN' resolve_tac encode_injectives);
    2.67 +
    2.68 +fun encode_sumN n k t =
    2.69 +  Balanced_Tree.access {init = t,
    2.70 +      left = fn t => @{const sum_encode} $ (@{const Inl (nat, nat)} $ t),
    2.71 +      right = fn t => @{const sum_encode} $ (@{const Inr (nat, nat)} $ t)}
    2.72 +    n k;
    2.73 +
    2.74 +fun encode_tuple [] = @{term "0 :: nat"}
    2.75 +  | encode_tuple ts =
    2.76 +    Balanced_Tree.make (fn (t, u) => @{const prod_encode} $ (@{const Pair (nat, nat)} $ u $ t)) ts;
    2.77 +
    2.78 +fun mk_to_nat T = Const (@{const_name to_nat}, T --> HOLogic.natT);
    2.79 +
    2.80 +fun mk_encode_funs ctxt fpTs ns ctrss0 recs0 =
    2.81 +  let
    2.82 +    val thy = Proof_Context.theory_of ctxt;
    2.83 +
    2.84 +    val nn = length ns;
    2.85 +    val recs as rec1 :: _ =
    2.86 +      map2 (fn fpT => mk_co_rec thy Least_FP fpT (replicate nn HOLogic.natT)) fpTs recs0;
    2.87 +    val arg_Ts = binder_fun_types (fastype_of rec1);
    2.88 +    val arg_Tss = Library.unflat ctrss0 arg_Ts;
    2.89 +
    2.90 +    fun mk_U (Type (@{type_name prod}, [T1, T2])) =
    2.91 +        if member (op =) fpTs T1 then T2 else HOLogic.mk_prodT (mk_U T1, mk_U T2)
    2.92 +      | mk_U (Type (s, Ts)) = Type (s, map mk_U Ts)
    2.93 +      | mk_U T = T;
    2.94 +
    2.95 +    fun mk_nat (j, T) =
    2.96 +      if T = HOLogic.natT then
    2.97 +        SOME (Bound j)
    2.98 +      else if member (op =) fpTs T then
    2.99 +        NONE
   2.100 +      else if exists_subtype_in fpTs T then
   2.101 +        let val U = mk_U T in
   2.102 +          SOME (mk_to_nat U $ (build_map ctxt [] (snd_const o fst) (T, U) $ Bound j))
   2.103 +        end
   2.104 +      else
   2.105 +        SOME (mk_to_nat T $ Bound j);
   2.106 +
   2.107 +    fun mk_arg n (k, arg_T) =
   2.108 +      let
   2.109 +        val bound_Ts = rev (binder_types arg_T);
   2.110 +        val nats = map_filter mk_nat (tag_list 0 bound_Ts);
   2.111 +      in
   2.112 +        fold (fn T => fn t => Abs (Name.uu, T, t)) bound_Ts (encode_sumN n k (encode_tuple nats))
   2.113 +      end;
   2.114 +
   2.115 +    val argss = map2 (map o mk_arg) ns (map (tag_list 1) arg_Tss);
   2.116 +  in
   2.117 +    map (fn recx => Term.list_comb (recx, flat argss)) recs
   2.118 +  end;
   2.119 +
   2.120 +fun mk_encode_injective_thms _ [] = []
   2.121 +  | mk_encode_injective_thms ctxt fpT_names0 =
   2.122 +    let
   2.123 +      fun not_datatype s = error (quote s ^ " is not a new-style datatype");
   2.124 +      fun not_mutually_recursive ss =
   2.125 +        error ("{" ^ commas ss ^ "} is not a set of mutually recursive new-style datatypes");
   2.126 +
   2.127 +      fun lfp_sugar_of s =
   2.128 +        (case fp_sugar_of ctxt s of
   2.129 +          SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
   2.130 +        | _ => not_datatype s);
   2.131 +
   2.132 +      val fpTs0 as Type (_, var_As) :: _ = #Ts (#fp_res (lfp_sugar_of (hd fpT_names0)));
   2.133 +      val fpT_names = map (fst o dest_Type) fpTs0;
   2.134 +
   2.135 +      val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) ctxt;
   2.136 +      val As =
   2.137 +        map2 (fn s => fn TVar (_, S) => TFree (s, union (op =) @{sort countable} S))
   2.138 +          As_names var_As;
   2.139 +      val fpTs = map (fn s => Type (s, As)) fpT_names;
   2.140 +
   2.141 +      val _ = subset (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
   2.142 +
   2.143 +      fun mk_conjunct fpT x encode_fun =
   2.144 +        HOLogic.all_const fpT $ Abs (Name.uu, fpT,
   2.145 +          HOLogic.mk_imp (HOLogic.mk_eq (encode_fun $ x, encode_fun $ Bound 0),
   2.146 +            HOLogic.eq_const fpT $ x $ Bound 0));
   2.147 +
   2.148 +      val fp_sugars as {fp_nesting_bnfs, common_co_inducts = induct :: _, ...} :: _ =
   2.149 +        map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0;
   2.150 +      val ctr_sugars = map #ctr_sugar fp_sugars;
   2.151 +
   2.152 +      val ctrss0 = map #ctrs ctr_sugars;
   2.153 +      val ns = map length ctrss0;
   2.154 +      val recs0 = map #co_rec fp_sugars;
   2.155 +      val nchotomys = map #nchotomy ctr_sugars;
   2.156 +      val injectss = map #injects ctr_sugars;
   2.157 +      val rec_thmss = map #co_rec_thms fp_sugars;
   2.158 +      val map_comps' = map (unfold_thms ctxt @{thms comp_def} o map_comp_of_bnf) fp_nesting_bnfs;
   2.159 +      val inj_map_strongs' = map (Thm.permute_prems 0 ~1 o inj_map_strong_of_bnf) fp_nesting_bnfs;
   2.160 +
   2.161 +      val (xs, names_ctxt) = ctxt |> mk_Frees "x" fpTs;
   2.162 +
   2.163 +      val conjuncts = map3 mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0);
   2.164 +      val goal = HOLogic.mk_Trueprop (Balanced_Tree.make HOLogic.mk_conj conjuncts);
   2.165 +    in
   2.166 +      Goal.prove_sorry ctxt [] [] goal (fn {context = ctxt, prems = _} =>
   2.167 +        mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'
   2.168 +        inj_map_strongs')
   2.169 +      |> HOLogic.conj_elims
   2.170 +      |> Proof_Context.export names_ctxt ctxt
   2.171 +      |> map Thm.close_derivation
   2.172 +    end;
   2.173 +
   2.174 +fun get_countable_goal_typ (@{const Trueprop} $ (Const (@{const_name Ex}, _)
   2.175 +    $ Abs (_, Type (_, [Type (s, _), _]), Const (@{const_name inj_on}, _) $ Bound 0
   2.176 +        $ Const (@{const_name top}, _)))) = s
   2.177 +  | get_countable_goal_typ _ = error "Wrong goal format for countable tactic";
   2.178 +
   2.179 +fun core_countable_tac ctxt st =
   2.180 +  endgame_tac ctxt (mk_encode_injective_thms ctxt (map get_countable_goal_typ (Thm.prems_of st)))
   2.181 +    st;
   2.182 +
   2.183 +fun countable_tac ctxt =
   2.184 +  TRY (Class.intro_classes_tac []) THEN core_countable_tac ctxt;
   2.185 +
   2.186 +end;