tuned ML and thy file names
authorblanchet
Sat Apr 27 11:37:50 2013 +0200 (2013-04-27)
changeset 51797182454c06a80
parent 51796 f0ee854aa2bd
child 51798 ad3a241def73
tuned ML and thy file names
src/HOL/BNF/BNF_Ctr_Sugar.thy
src/HOL/BNF/BNF_FP.thy
src/HOL/BNF/BNF_Wrap.thy
src/HOL/BNF/Tools/bnf_ctr_sugar.ML
src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_wrap.ML
src/HOL/BNF/Tools/bnf_wrap_tactics.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/BNF/BNF_Ctr_Sugar.thy	Sat Apr 27 11:37:50 2013 +0200
     1.3 @@ -0,0 +1,29 @@
     1.4 +(*  Title:      HOL/BNF/BNF_Ctr_Sugar.thy
     1.5 +    Author:     Jasmin Blanchette, TU Muenchen
     1.6 +    Copyright   2012
     1.7 +
     1.8 +Wrapping existing freely generated type's constructors.
     1.9 +*)
    1.10 +
    1.11 +header {* Wrapping Existing Freely Generated Type's Constructors *}
    1.12 +
    1.13 +theory BNF_Ctr_Sugar
    1.14 +imports BNF_Util
    1.15 +keywords
    1.16 +  "wrap_free_constructors" :: thy_goal and
    1.17 +  "no_dests" and
    1.18 +  "rep_compat"
    1.19 +begin
    1.20 +
    1.21 +lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
    1.22 +by (erule iffI) (erule contrapos_pn)
    1.23 +
    1.24 +lemma iff_contradict:
    1.25 +"\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
    1.26 +"\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
    1.27 +by blast+
    1.28 +
    1.29 +ML_file "Tools/bnf_ctr_sugar_tactics.ML"
    1.30 +ML_file "Tools/bnf_ctr_sugar.ML"
    1.31 +
    1.32 +end
     2.1 --- a/src/HOL/BNF/BNF_FP.thy	Fri Apr 26 14:16:05 2013 +0200
     2.2 +++ b/src/HOL/BNF/BNF_FP.thy	Sat Apr 27 11:37:50 2013 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  header {* Basic Fixed Point Operations on Bounded Natural Functors *}
     2.5  
     2.6  theory BNF_FP
     2.7 -imports BNF_Comp BNF_Wrap
     2.8 +imports BNF_Comp BNF_Ctr_Sugar
     2.9  keywords
    2.10    "defaults"
    2.11  begin
     3.1 --- a/src/HOL/BNF/BNF_Wrap.thy	Fri Apr 26 14:16:05 2013 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,29 +0,0 @@
     3.4 -(*  Title:      HOL/BNF/BNF_Wrap.thy
     3.5 -    Author:     Jasmin Blanchette, TU Muenchen
     3.6 -    Copyright   2012
     3.7 -
     3.8 -Wrapping datatypes.
     3.9 -*)
    3.10 -
    3.11 -header {* Wrapping Datatypes *}
    3.12 -
    3.13 -theory BNF_Wrap
    3.14 -imports BNF_Util
    3.15 -keywords
    3.16 -  "wrap_free_constructors" :: thy_goal and
    3.17 -  "no_dests" and
    3.18 -  "rep_compat"
    3.19 -begin
    3.20 -
    3.21 -lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
    3.22 -by (erule iffI) (erule contrapos_pn)
    3.23 -
    3.24 -lemma iff_contradict:
    3.25 -"\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
    3.26 -"\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
    3.27 -by blast+
    3.28 -
    3.29 -ML_file "Tools/bnf_wrap_tactics.ML"
    3.30 -ML_file "Tools/bnf_wrap.ML"
    3.31 -
    3.32 -end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Sat Apr 27 11:37:50 2013 +0200
     4.3 @@ -0,0 +1,710 @@
     4.4 +(*  Title:      HOL/BNF/Tools/bnf_ctr_sugar.ML
     4.5 +    Author:     Jasmin Blanchette, TU Muenchen
     4.6 +    Copyright   2012
     4.7 +
     4.8 +Wrapping existing freely generated type's constructors.
     4.9 +*)
    4.10 +
    4.11 +signature BNF_CTR_SUGAR =
    4.12 +sig
    4.13 +  val rep_compat_prefix: string
    4.14 +
    4.15 +  val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
    4.16 +  val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
    4.17 +
    4.18 +  val mk_ctr: typ list -> term -> term
    4.19 +  val mk_disc_or_sel: typ list -> term -> term
    4.20 +
    4.21 +  val name_of_ctr: term -> string
    4.22 +  val name_of_disc: term -> string
    4.23 +
    4.24 +  val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
    4.25 +    (((bool * bool) * term list) * term) *
    4.26 +      (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
    4.27 +    (term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list *
    4.28 +     thm list list) * local_theory
    4.29 +  val parse_wrap_options: (bool * bool) parser
    4.30 +  val parse_bound_term: (binding * string) parser
    4.31 +end;
    4.32 +
    4.33 +structure BNF_Ctr_Sugar : BNF_CTR_SUGAR =
    4.34 +struct
    4.35 +
    4.36 +open BNF_Util
    4.37 +open BNF_Ctr_Sugar_Tactics
    4.38 +
    4.39 +val rep_compat_prefix = "new";
    4.40 +
    4.41 +val isN = "is_";
    4.42 +val unN = "un_";
    4.43 +fun mk_unN 1 1 suf = unN ^ suf
    4.44 +  | mk_unN _ l suf = unN ^ suf ^ string_of_int l;
    4.45 +
    4.46 +val caseN = "case";
    4.47 +val case_congN = "case_cong";
    4.48 +val case_convN = "case_conv";
    4.49 +val collapseN = "collapse";
    4.50 +val disc_excludeN = "disc_exclude";
    4.51 +val disc_exhaustN = "disc_exhaust";
    4.52 +val discsN = "discs";
    4.53 +val distinctN = "distinct";
    4.54 +val exhaustN = "exhaust";
    4.55 +val expandN = "expand";
    4.56 +val injectN = "inject";
    4.57 +val nchotomyN = "nchotomy";
    4.58 +val selsN = "sels";
    4.59 +val splitN = "split";
    4.60 +val splitsN = "splits";
    4.61 +val split_asmN = "split_asm";
    4.62 +val weak_case_cong_thmsN = "weak_case_cong";
    4.63 +
    4.64 +val induct_simp_attrs = @{attributes [induct_simp]};
    4.65 +val cong_attrs = @{attributes [cong]};
    4.66 +val iff_attrs = @{attributes [iff]};
    4.67 +val safe_elim_attrs = @{attributes [elim!]};
    4.68 +val simp_attrs = @{attributes [simp]};
    4.69 +
    4.70 +fun unflat_lookup eq ys zs = map (map (fn x => nth zs (find_index (curry eq x) ys)));
    4.71 +
    4.72 +fun mk_half_pairss' _ ([], []) = []
    4.73 +  | mk_half_pairss' indent (x :: xs, _ :: ys) =
    4.74 +    indent @ fold_rev (cons o single o pair x) ys (mk_half_pairss' ([] :: indent) (xs, ys));
    4.75 +
    4.76 +fun mk_half_pairss p = mk_half_pairss' [[]] p;
    4.77 +
    4.78 +fun join_halves n half_xss other_half_xss =
    4.79 +  let
    4.80 +    val xsss =
    4.81 +      map2 (map2 append) (Library.chop_groups n half_xss)
    4.82 +        (transpose (Library.chop_groups n other_half_xss))
    4.83 +    val xs = splice (flat half_xss) (flat other_half_xss);
    4.84 +  in (xs, xsss) end;
    4.85 +
    4.86 +fun mk_undefined T = Const (@{const_name undefined}, T);
    4.87 +
    4.88 +fun mk_ctr Ts t =
    4.89 +  let val Type (_, Ts0) = body_type (fastype_of t) in
    4.90 +    Term.subst_atomic_types (Ts0 ~~ Ts) t
    4.91 +  end;
    4.92 +
    4.93 +fun mk_disc_or_sel Ts t =
    4.94 +  Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
    4.95 +
    4.96 +fun mk_case Ts T t =
    4.97 +  let val (Type (_, Ts0), body) = strip_type (fastype_of t) |>> List.last in
    4.98 +    Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) t
    4.99 +  end;
   4.100 +
   4.101 +fun name_of_const what t =
   4.102 +  (case head_of t of
   4.103 +    Const (s, _) => s
   4.104 +  | Free (s, _) => s
   4.105 +  | _ => error ("Cannot extract name of " ^ what));
   4.106 +
   4.107 +val name_of_ctr = name_of_const "constructor";
   4.108 +
   4.109 +val notN = "not_";
   4.110 +val eqN = "eq_";
   4.111 +val neqN = "neq_";
   4.112 +
   4.113 +fun name_of_disc t =
   4.114 +  (case head_of t of
   4.115 +    Abs (_, _, @{const Not} $ (t' $ Bound 0)) =>
   4.116 +    Long_Name.map_base_name (prefix notN) (name_of_disc t')
   4.117 +  | Abs (_, _, Const (@{const_name HOL.eq}, _) $ Bound 0 $ t') =>
   4.118 +    Long_Name.map_base_name (prefix eqN) (name_of_disc t')
   4.119 +  | Abs (_, _, @{const Not} $ (Const (@{const_name HOL.eq}, _) $ Bound 0 $ t')) =>
   4.120 +    Long_Name.map_base_name (prefix neqN) (name_of_disc t')
   4.121 +  | t' => name_of_const "destructor" t');
   4.122 +
   4.123 +val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
   4.124 +
   4.125 +fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
   4.126 +
   4.127 +fun prepare_wrap_free_constructors prep_term ((((no_dests, rep_compat), raw_ctrs), raw_case),
   4.128 +    (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
   4.129 +  let
   4.130 +    (* TODO: sanity checks on arguments *)
   4.131 +
   4.132 +    val n = length raw_ctrs;
   4.133 +    val ks = 1 upto n;
   4.134 +
   4.135 +    val _ = if n > 0 then () else error "No constructors specified";
   4.136 +
   4.137 +    val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
   4.138 +    val case0 = prep_term no_defs_lthy raw_case;
   4.139 +    val sel_defaultss =
   4.140 +      pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss);
   4.141 +
   4.142 +    val case0T = fastype_of case0;
   4.143 +    val Type (dataT_name, As0) =
   4.144 +      domain_type (snd (strip_typeN (length (binder_types case0T) - 1) case0T));
   4.145 +    val data_b = Binding.qualified_name dataT_name;
   4.146 +    val data_b_name = Binding.name_of data_b;
   4.147 +
   4.148 +    fun qualify mandatory =
   4.149 +      Binding.qualify mandatory data_b_name o
   4.150 +      (rep_compat ? Binding.qualify false rep_compat_prefix);
   4.151 +
   4.152 +    val (As, B) =
   4.153 +      no_defs_lthy
   4.154 +      |> mk_TFrees' (map Type.sort_of_atyp As0)
   4.155 +      ||> the_single o fst o mk_TFrees 1;
   4.156 +
   4.157 +    val dataT = Type (dataT_name, As);
   4.158 +    val ctrs = map (mk_ctr As) ctrs0;
   4.159 +    val ctr_Tss = map (binder_types o fastype_of) ctrs;
   4.160 +
   4.161 +    val ms = map length ctr_Tss;
   4.162 +
   4.163 +    val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings;
   4.164 +
   4.165 +    fun can_definitely_rely_on_disc k =
   4.166 +      not (Binding.is_empty (nth raw_disc_bindings' (k - 1)));
   4.167 +    fun can_rely_on_disc k =
   4.168 +      can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2));
   4.169 +    fun should_omit_disc_binding k =
   4.170 +      n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
   4.171 +
   4.172 +    fun is_disc_binding_valid b =
   4.173 +      not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding));
   4.174 +
   4.175 +    val standard_disc_binding = qualify false o Binding.name o prefix isN o base_name_of_ctr;
   4.176 +
   4.177 +    val disc_bindings =
   4.178 +      raw_disc_bindings'
   4.179 +      |> map4 (fn k => fn m => fn ctr => fn disc =>
   4.180 +        qualify false
   4.181 +          (if Binding.is_empty disc then
   4.182 +             if should_omit_disc_binding k then disc else standard_disc_binding ctr
   4.183 +           else if Binding.eq_name (disc, equal_binding) then
   4.184 +             if m = 0 then disc
   4.185 +             else error "Cannot use \"=\" syntax for discriminating nonnullary constructor"
   4.186 +           else if Binding.eq_name (disc, standard_binding) then
   4.187 +             standard_disc_binding ctr
   4.188 +           else
   4.189 +             disc)) ks ms ctrs0;
   4.190 +
   4.191 +    fun standard_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr;
   4.192 +
   4.193 +    val sel_bindingss =
   4.194 +      pad_list [] n raw_sel_bindingss
   4.195 +      |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
   4.196 +        qualify false
   4.197 +          (if Binding.is_empty sel orelse Binding.eq_name (sel, standard_binding) then
   4.198 +            standard_sel_binding m l ctr
   4.199 +          else
   4.200 +            sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms;
   4.201 +
   4.202 +    val casex = mk_case As B case0;
   4.203 +    val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
   4.204 +
   4.205 +    val (((((((xss, xss'), yss), fs), gs), [u', v']), (p, p')), names_lthy) = no_defs_lthy |>
   4.206 +      mk_Freess' "x" ctr_Tss
   4.207 +      ||>> mk_Freess "y" ctr_Tss
   4.208 +      ||>> mk_Frees "f" case_Ts
   4.209 +      ||>> mk_Frees "g" case_Ts
   4.210 +      ||>> (apfst (map (rpair dataT)) oo Variable.variant_fixes) [data_b_name, data_b_name ^ "'"]
   4.211 +      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
   4.212 +
   4.213 +    val u = Free u';
   4.214 +    val v = Free v';
   4.215 +    val q = Free (fst p', mk_pred1T B);
   4.216 +
   4.217 +    val xctrs = map2 (curry Term.list_comb) ctrs xss;
   4.218 +    val yctrs = map2 (curry Term.list_comb) ctrs yss;
   4.219 +
   4.220 +    val xfs = map2 (curry Term.list_comb) fs xss;
   4.221 +    val xgs = map2 (curry Term.list_comb) gs xss;
   4.222 +
   4.223 +    val fcase = Term.list_comb (casex, fs);
   4.224 +
   4.225 +    val ufcase = fcase $ u;
   4.226 +    val vfcase = fcase $ v;
   4.227 +
   4.228 +    (* TODO: Eta-expension is for compatibility with the old datatype package (but it also provides
   4.229 +       nicer names). Consider removing. *)
   4.230 +    val eta_fs = map2 eta_expand_arg xss xfs;
   4.231 +    val eta_gs = map2 eta_expand_arg xss xgs;
   4.232 +
   4.233 +    val eta_fcase = Term.list_comb (casex, eta_fs);
   4.234 +    val eta_gcase = Term.list_comb (casex, eta_gs);
   4.235 +
   4.236 +    val eta_ufcase = eta_fcase $ u;
   4.237 +    val eta_vgcase = eta_gcase $ v;
   4.238 +
   4.239 +    fun mk_uu_eq () = HOLogic.mk_eq (u, u);
   4.240 +
   4.241 +    val uv_eq = mk_Trueprop_eq (u, v);
   4.242 +
   4.243 +    val exist_xs_u_eq_ctrs =
   4.244 +      map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (u, xctr))) xctrs xss;
   4.245 +
   4.246 +    val unique_disc_no_def = TrueI; (*arbitrary marker*)
   4.247 +    val alternate_disc_no_def = FalseE; (*arbitrary marker*)
   4.248 +
   4.249 +    fun alternate_disc_lhs get_udisc k =
   4.250 +      HOLogic.mk_not
   4.251 +        (let val b = nth disc_bindings (k - 1) in
   4.252 +           if is_disc_binding_valid b then get_udisc b (k - 1) else nth exist_xs_u_eq_ctrs (k - 1)
   4.253 +         end);
   4.254 +
   4.255 +    val (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs,
   4.256 +         sel_defss, lthy') =
   4.257 +      if no_dests then
   4.258 +        (true, [], [], [], [], [], [], [], [], [], no_defs_lthy)
   4.259 +      else
   4.260 +        let
   4.261 +          fun disc_free b = Free (Binding.name_of b, mk_pred1T dataT);
   4.262 +
   4.263 +          fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr);
   4.264 +
   4.265 +          fun alternate_disc k =
   4.266 +            Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k));
   4.267 +
   4.268 +          fun mk_sel_case_args b proto_sels T =
   4.269 +            map2 (fn Ts => fn k =>
   4.270 +              (case AList.lookup (op =) proto_sels k of
   4.271 +                NONE =>
   4.272 +                (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
   4.273 +                  NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T)
   4.274 +                | SOME t => t |> Type.constraint (Ts ---> T) |> Syntax.check_term no_defs_lthy)
   4.275 +              | SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
   4.276 +
   4.277 +          fun sel_spec b proto_sels =
   4.278 +            let
   4.279 +              val _ =
   4.280 +                (case duplicates (op =) (map fst proto_sels) of
   4.281 +                   k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^
   4.282 +                     " for constructor " ^
   4.283 +                     quote (Syntax.string_of_term no_defs_lthy (nth ctrs (k - 1))))
   4.284 +                 | [] => ())
   4.285 +              val T =
   4.286 +                (case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of
   4.287 +                  [T] => T
   4.288 +                | T :: T' :: _ => error ("Inconsistent range type for selector " ^
   4.289 +                    quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
   4.290 +                    " vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T')));
   4.291 +            in
   4.292 +              mk_Trueprop_eq (Free (Binding.name_of b, dataT --> T) $ u,
   4.293 +                Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T) $ u)
   4.294 +            end;
   4.295 +
   4.296 +          val sel_bindings = flat sel_bindingss;
   4.297 +          val uniq_sel_bindings = distinct Binding.eq_name sel_bindings;
   4.298 +          val all_sels_distinct = (length uniq_sel_bindings = length sel_bindings);
   4.299 +
   4.300 +          val sel_binding_index =
   4.301 +            if all_sels_distinct then 1 upto length sel_bindings
   4.302 +            else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) sel_bindings;
   4.303 +
   4.304 +          val proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss);
   4.305 +          val sel_infos =
   4.306 +            AList.group (op =) (sel_binding_index ~~ proto_sels)
   4.307 +            |> sort (int_ord o pairself fst)
   4.308 +            |> map snd |> curry (op ~~) uniq_sel_bindings;
   4.309 +          val sel_bindings = map fst sel_infos;
   4.310 +
   4.311 +          fun unflat_selss xs = unflat_lookup Binding.eq_name sel_bindings xs sel_bindingss;
   4.312 +
   4.313 +          val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
   4.314 +            no_defs_lthy
   4.315 +            |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_u_eq_ctr => fn b =>
   4.316 +                if Binding.is_empty b then
   4.317 +                  if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
   4.318 +                  else pair (alternate_disc k, alternate_disc_no_def)
   4.319 +                else if Binding.eq_name (b, equal_binding) then
   4.320 +                  pair (Term.lambda u exist_xs_u_eq_ctr, refl)
   4.321 +                else
   4.322 +                  Specification.definition (SOME (b, NONE, NoSyn),
   4.323 +                    ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd)
   4.324 +              ks ms exist_xs_u_eq_ctrs disc_bindings
   4.325 +            ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
   4.326 +              Specification.definition (SOME (b, NONE, NoSyn),
   4.327 +                ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos
   4.328 +            ||> `Local_Theory.restore;
   4.329 +
   4.330 +          val phi = Proof_Context.export_morphism lthy lthy';
   4.331 +
   4.332 +          val disc_defs = map (Morphism.thm phi) raw_disc_defs;
   4.333 +          val sel_defs = map (Morphism.thm phi) raw_sel_defs;
   4.334 +          val sel_defss = unflat_selss sel_defs;
   4.335 +
   4.336 +          val discs0 = map (Morphism.term phi) raw_discs;
   4.337 +          val selss0 = unflat_selss (map (Morphism.term phi) raw_sels);
   4.338 +
   4.339 +          val discs = map (mk_disc_or_sel As) discs0;
   4.340 +          val selss = map (map (mk_disc_or_sel As)) selss0;
   4.341 +
   4.342 +          val udiscs = map (rapp u) discs;
   4.343 +          val uselss = map (map (rapp u)) selss;
   4.344 +
   4.345 +          val vdiscs = map (rapp v) discs;
   4.346 +          val vselss = map (map (rapp v)) selss;
   4.347 +        in
   4.348 +          (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs,
   4.349 +           sel_defss, lthy')
   4.350 +        end;
   4.351 +
   4.352 +    fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
   4.353 +
   4.354 +    val exhaust_goal =
   4.355 +      let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (u, xctr)]) in
   4.356 +        fold_rev Logic.all [p, u] (mk_imp_p (map2 mk_prem xctrs xss))
   4.357 +      end;
   4.358 +
   4.359 +    val inject_goalss =
   4.360 +      let
   4.361 +        fun mk_goal _ _ [] [] = []
   4.362 +          | mk_goal xctr yctr xs ys =
   4.363 +            [fold_rev Logic.all (xs @ ys) (mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr),
   4.364 +              Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))];
   4.365 +      in
   4.366 +        map4 mk_goal xctrs yctrs xss yss
   4.367 +      end;
   4.368 +
   4.369 +    val half_distinct_goalss =
   4.370 +      let
   4.371 +        fun mk_goal ((xs, xc), (xs', xc')) =
   4.372 +          fold_rev Logic.all (xs @ xs')
   4.373 +            (HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (xc, xc'))));
   4.374 +      in
   4.375 +        map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs)))
   4.376 +      end;
   4.377 +
   4.378 +    val cases_goal =
   4.379 +      map3 (fn xs => fn xctr => fn xf =>
   4.380 +        fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xss xctrs xfs;
   4.381 +
   4.382 +    val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss @ [cases_goal];
   4.383 +
   4.384 +    fun after_qed thmss lthy =
   4.385 +      let
   4.386 +        val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) =
   4.387 +          (hd thmss, apsnd (chop (n * n)) (chop n (tl thmss)));
   4.388 +
   4.389 +        val inject_thms = flat inject_thmss;
   4.390 +
   4.391 +        val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
   4.392 +
   4.393 +        fun inst_thm t thm =
   4.394 +          Drule.instantiate' [] [SOME (certify lthy t)]
   4.395 +            (Thm.instantiate (Tinst, []) (Drule.zero_var_indexes thm));
   4.396 +
   4.397 +        val uexhaust_thm = inst_thm u exhaust_thm;
   4.398 +
   4.399 +        val exhaust_cases = map base_name_of_ctr ctrs;
   4.400 +
   4.401 +        val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss;
   4.402 +
   4.403 +        val (distinct_thms, (distinct_thmsss', distinct_thmsss)) =
   4.404 +          join_halves n half_distinct_thmss other_half_distinct_thmss ||> `transpose;
   4.405 +
   4.406 +        val nchotomy_thm =
   4.407 +          let
   4.408 +            val goal =
   4.409 +              HOLogic.mk_Trueprop (HOLogic.mk_all (fst u', snd u',
   4.410 +                Library.foldr1 HOLogic.mk_disj exist_xs_u_eq_ctrs));
   4.411 +          in
   4.412 +            Goal.prove_sorry lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
   4.413 +            |> Thm.close_derivation
   4.414 +          end;
   4.415 +
   4.416 +        val (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
   4.417 +             disc_exhaust_thms, collapse_thms, expand_thms, case_conv_thms) =
   4.418 +          if no_dests then
   4.419 +            ([], [], [], [], [], [], [], [], [], [])
   4.420 +          else
   4.421 +            let
   4.422 +              fun make_sel_thm xs' case_thm sel_def =
   4.423 +                zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs')
   4.424 +                    (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
   4.425 +
   4.426 +              fun has_undefined_rhs thm =
   4.427 +                (case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of
   4.428 +                  Const (@{const_name undefined}, _) => true
   4.429 +                | _ => false);
   4.430 +
   4.431 +              val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss;
   4.432 +
   4.433 +              val all_sel_thms =
   4.434 +                (if all_sels_distinct andalso forall null sel_defaultss then
   4.435 +                   flat sel_thmss
   4.436 +                 else
   4.437 +                   map_product (fn s => fn (xs', c) => make_sel_thm xs' c s) sel_defs
   4.438 +                     (xss' ~~ case_thms))
   4.439 +                |> filter_out has_undefined_rhs;
   4.440 +
   4.441 +              fun mk_unique_disc_def () =
   4.442 +                let
   4.443 +                  val m = the_single ms;
   4.444 +                  val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs);
   4.445 +                in
   4.446 +                  Goal.prove_sorry lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm)
   4.447 +                  |> Thm.close_derivation
   4.448 +                  |> singleton (Proof_Context.export names_lthy lthy)
   4.449 +                end;
   4.450 +
   4.451 +              fun mk_alternate_disc_def k =
   4.452 +                let
   4.453 +                  val goal =
   4.454 +                    mk_Trueprop_eq (alternate_disc_lhs (K (nth udiscs)) (3 - k),
   4.455 +                      nth exist_xs_u_eq_ctrs (k - 1));
   4.456 +                in
   4.457 +                  Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   4.458 +                    mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k))
   4.459 +                      (nth distinct_thms (2 - k)) uexhaust_thm)
   4.460 +                  |> Thm.close_derivation
   4.461 +                  |> singleton (Proof_Context.export names_lthy lthy)
   4.462 +                end;
   4.463 +
   4.464 +              val has_alternate_disc_def =
   4.465 +                exists (fn def => Thm.eq_thm_prop (def, alternate_disc_no_def)) disc_defs;
   4.466 +
   4.467 +              val disc_defs' =
   4.468 +                map2 (fn k => fn def =>
   4.469 +                  if Thm.eq_thm_prop (def, unique_disc_no_def) then mk_unique_disc_def ()
   4.470 +                  else if Thm.eq_thm_prop (def, alternate_disc_no_def) then mk_alternate_disc_def k
   4.471 +                  else def) ks disc_defs;
   4.472 +
   4.473 +              val discD_thms = map (fn def => def RS iffD1) disc_defs';
   4.474 +              val discI_thms =
   4.475 +                map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms
   4.476 +                  disc_defs';
   4.477 +              val not_discI_thms =
   4.478 +                map2 (fn m => fn def => funpow m (fn thm => allI RS thm)
   4.479 +                    (unfold_thms lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
   4.480 +                  ms disc_defs';
   4.481 +
   4.482 +              val (disc_thmss', disc_thmss) =
   4.483 +                let
   4.484 +                  fun mk_thm discI _ [] = refl RS discI
   4.485 +                    | mk_thm _ not_discI [distinct] = distinct RS not_discI;
   4.486 +                  fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss;
   4.487 +                in
   4.488 +                  map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
   4.489 +                end;
   4.490 +
   4.491 +              val disc_thms = flat (map2 (fn b => if is_disc_binding_valid b then I else K [])
   4.492 +                disc_bindings disc_thmss);
   4.493 +
   4.494 +              val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) =
   4.495 +                let
   4.496 +                  fun mk_goal [] = []
   4.497 +                    | mk_goal [((_, udisc), (_, udisc'))] =
   4.498 +                      [Logic.all u (Logic.mk_implies (HOLogic.mk_Trueprop udisc,
   4.499 +                         HOLogic.mk_Trueprop (HOLogic.mk_not udisc')))];
   4.500 +
   4.501 +                  fun prove tac goal =
   4.502 +                    Goal.prove_sorry lthy [] [] goal (K tac)
   4.503 +                    |> Thm.close_derivation;
   4.504 +
   4.505 +                  val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs));
   4.506 +
   4.507 +                  val half_goalss = map mk_goal half_pairss;
   4.508 +                  val half_thmss =
   4.509 +                    map3 (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] =>
   4.510 +                        fn disc_thm => [prove (mk_half_disc_exclude_tac m discD disc_thm) goal])
   4.511 +                      half_goalss half_pairss (flat disc_thmss');
   4.512 +
   4.513 +                  val other_half_goalss = map (mk_goal o map swap) half_pairss;
   4.514 +                  val other_half_thmss =
   4.515 +                    map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss
   4.516 +                      other_half_goalss;
   4.517 +                in
   4.518 +                  join_halves n half_thmss other_half_thmss ||> `transpose
   4.519 +                  |>> has_alternate_disc_def ? K []
   4.520 +                end;
   4.521 +
   4.522 +              val disc_exhaust_thm =
   4.523 +                let
   4.524 +                  fun mk_prem udisc = mk_imp_p [HOLogic.mk_Trueprop udisc];
   4.525 +                  val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem udiscs));
   4.526 +                in
   4.527 +                  Goal.prove_sorry lthy [] [] goal (fn _ =>
   4.528 +                    mk_disc_exhaust_tac n exhaust_thm discI_thms)
   4.529 +                  |> Thm.close_derivation
   4.530 +                end;
   4.531 +
   4.532 +              val (collapse_thms, collapse_thm_opts) =
   4.533 +                let
   4.534 +                  fun mk_goal ctr udisc usels =
   4.535 +                    let
   4.536 +                      val prem = HOLogic.mk_Trueprop udisc;
   4.537 +                      val concl =
   4.538 +                        mk_Trueprop_eq ((null usels ? swap) (Term.list_comb (ctr, usels), u));
   4.539 +                    in
   4.540 +                      if prem aconv concl then NONE
   4.541 +                      else SOME (Logic.all u (Logic.mk_implies (prem, concl)))
   4.542 +                    end;
   4.543 +                  val goals = map3 mk_goal ctrs udiscs uselss;
   4.544 +                in
   4.545 +                  map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal =>
   4.546 +                    Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   4.547 +                      mk_collapse_tac ctxt m discD sel_thms)
   4.548 +                    |> Thm.close_derivation
   4.549 +                    |> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals
   4.550 +                  |> `(map_filter I)
   4.551 +                end;
   4.552 +
   4.553 +              val expand_thms =
   4.554 +                let
   4.555 +                  fun mk_prems k udisc usels vdisc vsels =
   4.556 +                    (if k = n then [] else [mk_Trueprop_eq (udisc, vdisc)]) @
   4.557 +                    (if null usels then
   4.558 +                       []
   4.559 +                     else
   4.560 +                       [Logic.list_implies
   4.561 +                          (if n = 1 then [] else map HOLogic.mk_Trueprop [udisc, vdisc],
   4.562 +                             HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   4.563 +                               (map2 (curry HOLogic.mk_eq) usels vsels)))]);
   4.564 +
   4.565 +                  val goal =
   4.566 +                    Library.foldr Logic.list_implies
   4.567 +                      (map5 mk_prems ks udiscs uselss vdiscs vselss, uv_eq);
   4.568 +                  val uncollapse_thms =
   4.569 +                    map2 (fn NONE => K asm_rl | SOME thm => fn [] => thm | _ => thm RS sym)
   4.570 +                      collapse_thm_opts uselss;
   4.571 +                in
   4.572 +                  [Goal.prove_sorry lthy [] [] goal (fn _ =>
   4.573 +                     mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
   4.574 +                       (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
   4.575 +                       disc_exclude_thmsss')]
   4.576 +                  |> map Thm.close_derivation
   4.577 +                  |> Proof_Context.export names_lthy lthy
   4.578 +                end;
   4.579 +
   4.580 +              val case_conv_thms =
   4.581 +                let
   4.582 +                  fun mk_body f usels = Term.list_comb (f, usels);
   4.583 +                  val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs (map2 mk_body fs uselss));
   4.584 +                in
   4.585 +                  [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   4.586 +                     mk_case_conv_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)]
   4.587 +                  |> map Thm.close_derivation
   4.588 +                  |> Proof_Context.export names_lthy lthy
   4.589 +                end;
   4.590 +            in
   4.591 +              (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
   4.592 +               [disc_exhaust_thm], collapse_thms, expand_thms, case_conv_thms)
   4.593 +            end;
   4.594 +
   4.595 +        val (case_cong_thm, weak_case_cong_thm) =
   4.596 +          let
   4.597 +            fun mk_prem xctr xs xf xg =
   4.598 +              fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr),
   4.599 +                mk_Trueprop_eq (xf, xg)));
   4.600 +
   4.601 +            val goal =
   4.602 +              Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss xfs xgs,
   4.603 +                 mk_Trueprop_eq (eta_ufcase, eta_vgcase));
   4.604 +            val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase));
   4.605 +          in
   4.606 +            (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms),
   4.607 +             Goal.prove_sorry lthy [] [] weak_goal (K (etac arg_cong 1)))
   4.608 +            |> pairself (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy))
   4.609 +          end;
   4.610 +
   4.611 +        val (split_thm, split_asm_thm) =
   4.612 +          let
   4.613 +            fun mk_conjunct xctr xs f_xs =
   4.614 +              list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (u, xctr), q $ f_xs));
   4.615 +            fun mk_disjunct xctr xs f_xs =
   4.616 +              list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr),
   4.617 +                HOLogic.mk_not (q $ f_xs)));
   4.618 +
   4.619 +            val lhs = q $ ufcase;
   4.620 +
   4.621 +            val goal =
   4.622 +              mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs));
   4.623 +            val asm_goal =
   4.624 +              mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj
   4.625 +                (map3 mk_disjunct xctrs xss xfs)));
   4.626 +
   4.627 +            val split_thm =
   4.628 +              Goal.prove_sorry lthy [] [] goal
   4.629 +                (fn _ => mk_split_tac lthy uexhaust_thm case_thms inject_thmss distinct_thmsss)
   4.630 +              |> Thm.close_derivation
   4.631 +              |> singleton (Proof_Context.export names_lthy lthy);
   4.632 +            val split_asm_thm =
   4.633 +              Goal.prove_sorry lthy [] [] asm_goal (fn {context = ctxt, ...} =>
   4.634 +                mk_split_asm_tac ctxt split_thm)
   4.635 +              |> Thm.close_derivation
   4.636 +              |> singleton (Proof_Context.export names_lthy lthy);
   4.637 +          in
   4.638 +            (split_thm, split_asm_thm)
   4.639 +          end;
   4.640 +
   4.641 +        val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
   4.642 +        val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name));
   4.643 +
   4.644 +        val notes =
   4.645 +          [(caseN, case_thms, simp_attrs),
   4.646 +           (case_congN, [case_cong_thm], []),
   4.647 +           (case_convN, case_conv_thms, []),
   4.648 +           (collapseN, collapse_thms, simp_attrs),
   4.649 +           (discsN, disc_thms, simp_attrs),
   4.650 +           (disc_excludeN, disc_exclude_thms, []),
   4.651 +           (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
   4.652 +           (distinctN, distinct_thms, simp_attrs @ induct_simp_attrs),
   4.653 +           (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
   4.654 +           (expandN, expand_thms, []),
   4.655 +           (injectN, inject_thms, iff_attrs @ induct_simp_attrs),
   4.656 +           (nchotomyN, [nchotomy_thm], []),
   4.657 +           (selsN, all_sel_thms, simp_attrs),
   4.658 +           (splitN, [split_thm], []),
   4.659 +           (split_asmN, [split_asm_thm], []),
   4.660 +           (splitsN, [split_thm, split_asm_thm], []),
   4.661 +           (weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)]
   4.662 +          |> filter_out (null o #2)
   4.663 +          |> map (fn (thmN, thms, attrs) =>
   4.664 +            ((qualify true (Binding.name thmN), attrs), [(thms, [])]));
   4.665 +
   4.666 +        val notes' =
   4.667 +          [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
   4.668 +          |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
   4.669 +      in
   4.670 +        ((discs, selss, exhaust_thm, inject_thms, distinct_thms, case_thms, disc_thmss, discI_thms,
   4.671 +          sel_thmss),
   4.672 +          lthy
   4.673 +          |> not rep_compat ?
   4.674 +             (Local_Theory.declaration {syntax = false, pervasive = true}
   4.675 +               (fn phi => Case_Translation.register
   4.676 +                 (Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
   4.677 +          |> Local_Theory.notes (notes' @ notes) |> snd)
   4.678 +      end;
   4.679 +  in
   4.680 +    (goalss, after_qed, lthy')
   4.681 +  end;
   4.682 +
   4.683 +fun wrap_free_constructors tacss = (fn (goalss, after_qed, lthy) =>
   4.684 +  map2 (map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])) goalss tacss
   4.685 +  |> (fn thms => after_qed thms lthy)) oo prepare_wrap_free_constructors (K I);
   4.686 +
   4.687 +val wrap_free_constructors_cmd = (fn (goalss, after_qed, lthy) =>
   4.688 +  Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
   4.689 +  prepare_wrap_free_constructors Syntax.read_term;
   4.690 +
   4.691 +fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
   4.692 +
   4.693 +val parse_bindings = parse_bracket_list parse_binding;
   4.694 +val parse_bindingss = parse_bracket_list parse_bindings;
   4.695 +
   4.696 +val parse_bound_term = (parse_binding --| @{keyword ":"}) -- Parse.term;
   4.697 +val parse_bound_terms = parse_bracket_list parse_bound_term;
   4.698 +val parse_bound_termss = parse_bracket_list parse_bound_terms;
   4.699 +
   4.700 +val parse_wrap_options =
   4.701 +  Scan.optional (@{keyword "("} |-- Parse.list1 ((@{keyword "no_dests"} >> K (true, false)) ||
   4.702 +      (@{keyword "rep_compat"} >> K (false, true))) --| @{keyword ")"}
   4.703 +    >> (pairself (exists I) o split_list)) (false, false);
   4.704 +
   4.705 +val _ =
   4.706 +  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"}
   4.707 +    "wrap an existing freely generated type's constructors"
   4.708 +    ((parse_wrap_options -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) --
   4.709 +      Parse.term -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
   4.710 +        Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
   4.711 +     >> wrap_free_constructors_cmd);
   4.712 +
   4.713 +end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Sat Apr 27 11:37:50 2013 +0200
     5.3 @@ -0,0 +1,125 @@
     5.4 +(*  Title:      HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
     5.5 +    Author:     Jasmin Blanchette, TU Muenchen
     5.6 +    Copyright   2012
     5.7 +
     5.8 +Tactics for wrapping existing freely generated type's constructors.
     5.9 +*)
    5.10 +
    5.11 +signature BNF_CTR_SUGAR_TACTICS =
    5.12 +sig
    5.13 +  val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
    5.14 +  val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic
    5.15 +  val mk_case_conv_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list ->
    5.16 +    tactic
    5.17 +  val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
    5.18 +  val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
    5.19 +  val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
    5.20 +    thm list list list -> thm list list list -> tactic
    5.21 +  val mk_half_disc_exclude_tac: int -> thm -> thm -> tactic
    5.22 +  val mk_nchotomy_tac: int -> thm -> tactic
    5.23 +  val mk_other_half_disc_exclude_tac: thm -> tactic
    5.24 +  val mk_split_tac: Proof.context ->
    5.25 +    thm -> thm list -> thm list list -> thm list list list -> tactic
    5.26 +  val mk_split_asm_tac: Proof.context -> thm -> tactic
    5.27 +  val mk_unique_disc_def_tac: int -> thm -> tactic
    5.28 +end;
    5.29 +
    5.30 +structure BNF_Ctr_Sugar_Tactics : BNF_CTR_SUGAR_TACTICS =
    5.31 +struct
    5.32 +
    5.33 +open BNF_Util
    5.34 +open BNF_Tactics
    5.35 +
    5.36 +val meta_mp = @{thm meta_mp};
    5.37 +
    5.38 +fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P});
    5.39 +
    5.40 +fun mk_nchotomy_tac n exhaust =
    5.41 +  (rtac allI THEN' rtac exhaust THEN'
    5.42 +   EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1;
    5.43 +
    5.44 +fun mk_unique_disc_def_tac m uexhaust =
    5.45 +  EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1;
    5.46 +
    5.47 +fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
    5.48 +  EVERY' ([rtac (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans),
    5.49 +    rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
    5.50 +    hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
    5.51 +    rtac distinct, rtac uexhaust] @
    5.52 +    (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
    5.53 +     |> k = 1 ? swap |> op @)) 1;
    5.54 +
    5.55 +fun mk_half_disc_exclude_tac m discD disc' =
    5.56 +  (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' rtac disc') 1;
    5.57 +
    5.58 +fun mk_other_half_disc_exclude_tac half = (etac @{thm contrapos_pn} THEN' etac half) 1;
    5.59 +
    5.60 +fun mk_disc_exhaust_tac n exhaust discIs =
    5.61 +  (rtac exhaust THEN'
    5.62 +   EVERY' (map2 (fn k => fn discI =>
    5.63 +     dtac discI THEN' select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) discIs)) 1;
    5.64 +
    5.65 +fun mk_collapse_tac ctxt m discD sels =
    5.66 +  (dtac discD THEN'
    5.67 +   (if m = 0 then
    5.68 +      atac
    5.69 +    else
    5.70 +      REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN'
    5.71 +      SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)) 1;
    5.72 +
    5.73 +fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
    5.74 +    disc_excludesss' =
    5.75 +  if ms = [0] then
    5.76 +    (rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN'
    5.77 +     TRY o EVERY' [rtac udisc_exhaust, atac, rtac vdisc_exhaust, atac]) 1
    5.78 +  else
    5.79 +    let val ks = 1 upto n in
    5.80 +      (rtac udisc_exhaust THEN'
    5.81 +       EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' =>
    5.82 +           fn uuncollapse =>
    5.83 +         EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac,
    5.84 +           rtac sym, rtac vdisc_exhaust,
    5.85 +           EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse =>
    5.86 +             EVERY'
    5.87 +               (if k' = k then
    5.88 +                  [rtac (vuncollapse RS trans), TRY o atac] @
    5.89 +                  (if m = 0 then
    5.90 +                     [rtac refl]
    5.91 +                   else
    5.92 +                     [if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac],
    5.93 +                      REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE,
    5.94 +                      asm_simp_tac (ss_only [] ctxt)])
    5.95 +                else
    5.96 +                  [dtac (the_single (if k = n then disc_excludes else disc_excludes')),
    5.97 +                   etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),
    5.98 +                   atac, atac]))
    5.99 +             ks disc_excludess disc_excludess' uncollapses)])
   5.100 +         ks ms disc_excludesss disc_excludesss' uncollapses)) 1
   5.101 +    end;
   5.102 +
   5.103 +fun mk_case_conv_tac ctxt n uexhaust cases discss' selss =
   5.104 +  (rtac uexhaust THEN'
   5.105 +   EVERY' (map3 (fn casex => fn if_discs => fn sels =>
   5.106 +       EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), rtac casex])
   5.107 +     cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)) 1;
   5.108 +
   5.109 +fun mk_case_cong_tac ctxt uexhaust cases =
   5.110 +  (rtac uexhaust THEN'
   5.111 +   EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases)) 1;
   5.112 +
   5.113 +val naked_ctxt = @{theory_context HOL};
   5.114 +
   5.115 +(* TODO: More precise "simp_thms"; get rid of "blast_tac" *)
   5.116 +fun mk_split_tac ctxt uexhaust cases injectss distinctsss =
   5.117 +  rtac uexhaust 1 THEN
   5.118 +  ALLGOALS (fn k => (hyp_subst_tac THEN'
   5.119 +     simp_tac (ss_only (@{thms simp_thms} @ cases @ nth injectss (k - 1) @
   5.120 +       flat (nth distinctsss (k - 1))) ctxt)) k) THEN
   5.121 +  ALLGOALS (blast_tac naked_ctxt);
   5.122 +
   5.123 +val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
   5.124 +
   5.125 +fun mk_split_asm_tac ctxt split =
   5.126 +  rtac (split RS trans) 1 THEN unfold_thms_tac ctxt split_asm_thms THEN rtac refl 1;
   5.127 +
   5.128 +end;
     6.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Apr 26 14:16:05 2013 +0200
     6.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sat Apr 27 11:37:50 2013 +0200
     6.3 @@ -26,7 +26,7 @@
     6.4  struct
     6.5  
     6.6  open BNF_Util
     6.7 -open BNF_Wrap
     6.8 +open BNF_Ctr_Sugar
     6.9  open BNF_Def
    6.10  open BNF_FP
    6.11  open BNF_FP_Def_Sugar_Tactics
     7.1 --- a/src/HOL/BNF/Tools/bnf_wrap.ML	Fri Apr 26 14:16:05 2013 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,710 +0,0 @@
     7.4 -(*  Title:      HOL/BNF/Tools/bnf_wrap.ML
     7.5 -    Author:     Jasmin Blanchette, TU Muenchen
     7.6 -    Copyright   2012
     7.7 -
     7.8 -Wrapping existing datatypes.
     7.9 -*)
    7.10 -
    7.11 -signature BNF_WRAP =
    7.12 -sig
    7.13 -  val rep_compat_prefix: string
    7.14 -
    7.15 -  val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
    7.16 -  val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
    7.17 -
    7.18 -  val mk_ctr: typ list -> term -> term
    7.19 -  val mk_disc_or_sel: typ list -> term -> term
    7.20 -
    7.21 -  val name_of_ctr: term -> string
    7.22 -  val name_of_disc: term -> string
    7.23 -
    7.24 -  val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
    7.25 -    (((bool * bool) * term list) * term) *
    7.26 -      (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
    7.27 -    (term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list *
    7.28 -     thm list list) * local_theory
    7.29 -  val parse_wrap_options: (bool * bool) parser
    7.30 -  val parse_bound_term: (binding * string) parser
    7.31 -end;
    7.32 -
    7.33 -structure BNF_Wrap : BNF_WRAP =
    7.34 -struct
    7.35 -
    7.36 -open BNF_Util
    7.37 -open BNF_Wrap_Tactics
    7.38 -
    7.39 -val rep_compat_prefix = "new";
    7.40 -
    7.41 -val isN = "is_";
    7.42 -val unN = "un_";
    7.43 -fun mk_unN 1 1 suf = unN ^ suf
    7.44 -  | mk_unN _ l suf = unN ^ suf ^ string_of_int l;
    7.45 -
    7.46 -val caseN = "case";
    7.47 -val case_congN = "case_cong";
    7.48 -val case_convN = "case_conv";
    7.49 -val collapseN = "collapse";
    7.50 -val disc_excludeN = "disc_exclude";
    7.51 -val disc_exhaustN = "disc_exhaust";
    7.52 -val discsN = "discs";
    7.53 -val distinctN = "distinct";
    7.54 -val exhaustN = "exhaust";
    7.55 -val expandN = "expand";
    7.56 -val injectN = "inject";
    7.57 -val nchotomyN = "nchotomy";
    7.58 -val selsN = "sels";
    7.59 -val splitN = "split";
    7.60 -val splitsN = "splits";
    7.61 -val split_asmN = "split_asm";
    7.62 -val weak_case_cong_thmsN = "weak_case_cong";
    7.63 -
    7.64 -val induct_simp_attrs = @{attributes [induct_simp]};
    7.65 -val cong_attrs = @{attributes [cong]};
    7.66 -val iff_attrs = @{attributes [iff]};
    7.67 -val safe_elim_attrs = @{attributes [elim!]};
    7.68 -val simp_attrs = @{attributes [simp]};
    7.69 -
    7.70 -fun unflat_lookup eq ys zs = map (map (fn x => nth zs (find_index (curry eq x) ys)));
    7.71 -
    7.72 -fun mk_half_pairss' _ ([], []) = []
    7.73 -  | mk_half_pairss' indent (x :: xs, _ :: ys) =
    7.74 -    indent @ fold_rev (cons o single o pair x) ys (mk_half_pairss' ([] :: indent) (xs, ys));
    7.75 -
    7.76 -fun mk_half_pairss p = mk_half_pairss' [[]] p;
    7.77 -
    7.78 -fun join_halves n half_xss other_half_xss =
    7.79 -  let
    7.80 -    val xsss =
    7.81 -      map2 (map2 append) (Library.chop_groups n half_xss)
    7.82 -        (transpose (Library.chop_groups n other_half_xss))
    7.83 -    val xs = splice (flat half_xss) (flat other_half_xss);
    7.84 -  in (xs, xsss) end;
    7.85 -
    7.86 -fun mk_undefined T = Const (@{const_name undefined}, T);
    7.87 -
    7.88 -fun mk_ctr Ts t =
    7.89 -  let val Type (_, Ts0) = body_type (fastype_of t) in
    7.90 -    Term.subst_atomic_types (Ts0 ~~ Ts) t
    7.91 -  end;
    7.92 -
    7.93 -fun mk_disc_or_sel Ts t =
    7.94 -  Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
    7.95 -
    7.96 -fun mk_case Ts T t =
    7.97 -  let val (Type (_, Ts0), body) = strip_type (fastype_of t) |>> List.last in
    7.98 -    Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) t
    7.99 -  end;
   7.100 -
   7.101 -fun name_of_const what t =
   7.102 -  (case head_of t of
   7.103 -    Const (s, _) => s
   7.104 -  | Free (s, _) => s
   7.105 -  | _ => error ("Cannot extract name of " ^ what));
   7.106 -
   7.107 -val name_of_ctr = name_of_const "constructor";
   7.108 -
   7.109 -val notN = "not_";
   7.110 -val eqN = "eq_";
   7.111 -val neqN = "neq_";
   7.112 -
   7.113 -fun name_of_disc t =
   7.114 -  (case head_of t of
   7.115 -    Abs (_, _, @{const Not} $ (t' $ Bound 0)) =>
   7.116 -    Long_Name.map_base_name (prefix notN) (name_of_disc t')
   7.117 -  | Abs (_, _, Const (@{const_name HOL.eq}, _) $ Bound 0 $ t') =>
   7.118 -    Long_Name.map_base_name (prefix eqN) (name_of_disc t')
   7.119 -  | Abs (_, _, @{const Not} $ (Const (@{const_name HOL.eq}, _) $ Bound 0 $ t')) =>
   7.120 -    Long_Name.map_base_name (prefix neqN) (name_of_disc t')
   7.121 -  | t' => name_of_const "destructor" t');
   7.122 -
   7.123 -val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
   7.124 -
   7.125 -fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
   7.126 -
   7.127 -fun prepare_wrap_free_constructors prep_term ((((no_dests, rep_compat), raw_ctrs), raw_case),
   7.128 -    (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
   7.129 -  let
   7.130 -    (* TODO: sanity checks on arguments *)
   7.131 -
   7.132 -    val n = length raw_ctrs;
   7.133 -    val ks = 1 upto n;
   7.134 -
   7.135 -    val _ = if n > 0 then () else error "No constructors specified";
   7.136 -
   7.137 -    val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
   7.138 -    val case0 = prep_term no_defs_lthy raw_case;
   7.139 -    val sel_defaultss =
   7.140 -      pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss);
   7.141 -
   7.142 -    val case0T = fastype_of case0;
   7.143 -    val Type (dataT_name, As0) =
   7.144 -      domain_type (snd (strip_typeN (length (binder_types case0T) - 1) case0T));
   7.145 -    val data_b = Binding.qualified_name dataT_name;
   7.146 -    val data_b_name = Binding.name_of data_b;
   7.147 -
   7.148 -    fun qualify mandatory =
   7.149 -      Binding.qualify mandatory data_b_name o
   7.150 -      (rep_compat ? Binding.qualify false rep_compat_prefix);
   7.151 -
   7.152 -    val (As, B) =
   7.153 -      no_defs_lthy
   7.154 -      |> mk_TFrees' (map Type.sort_of_atyp As0)
   7.155 -      ||> the_single o fst o mk_TFrees 1;
   7.156 -
   7.157 -    val dataT = Type (dataT_name, As);
   7.158 -    val ctrs = map (mk_ctr As) ctrs0;
   7.159 -    val ctr_Tss = map (binder_types o fastype_of) ctrs;
   7.160 -
   7.161 -    val ms = map length ctr_Tss;
   7.162 -
   7.163 -    val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings;
   7.164 -
   7.165 -    fun can_definitely_rely_on_disc k =
   7.166 -      not (Binding.is_empty (nth raw_disc_bindings' (k - 1)));
   7.167 -    fun can_rely_on_disc k =
   7.168 -      can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2));
   7.169 -    fun should_omit_disc_binding k =
   7.170 -      n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
   7.171 -
   7.172 -    fun is_disc_binding_valid b =
   7.173 -      not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding));
   7.174 -
   7.175 -    val standard_disc_binding = qualify false o Binding.name o prefix isN o base_name_of_ctr;
   7.176 -
   7.177 -    val disc_bindings =
   7.178 -      raw_disc_bindings'
   7.179 -      |> map4 (fn k => fn m => fn ctr => fn disc =>
   7.180 -        qualify false
   7.181 -          (if Binding.is_empty disc then
   7.182 -             if should_omit_disc_binding k then disc else standard_disc_binding ctr
   7.183 -           else if Binding.eq_name (disc, equal_binding) then
   7.184 -             if m = 0 then disc
   7.185 -             else error "Cannot use \"=\" syntax for discriminating nonnullary constructor"
   7.186 -           else if Binding.eq_name (disc, standard_binding) then
   7.187 -             standard_disc_binding ctr
   7.188 -           else
   7.189 -             disc)) ks ms ctrs0;
   7.190 -
   7.191 -    fun standard_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr;
   7.192 -
   7.193 -    val sel_bindingss =
   7.194 -      pad_list [] n raw_sel_bindingss
   7.195 -      |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
   7.196 -        qualify false
   7.197 -          (if Binding.is_empty sel orelse Binding.eq_name (sel, standard_binding) then
   7.198 -            standard_sel_binding m l ctr
   7.199 -          else
   7.200 -            sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms;
   7.201 -
   7.202 -    val casex = mk_case As B case0;
   7.203 -    val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
   7.204 -
   7.205 -    val (((((((xss, xss'), yss), fs), gs), [u', v']), (p, p')), names_lthy) = no_defs_lthy |>
   7.206 -      mk_Freess' "x" ctr_Tss
   7.207 -      ||>> mk_Freess "y" ctr_Tss
   7.208 -      ||>> mk_Frees "f" case_Ts
   7.209 -      ||>> mk_Frees "g" case_Ts
   7.210 -      ||>> (apfst (map (rpair dataT)) oo Variable.variant_fixes) [data_b_name, data_b_name ^ "'"]
   7.211 -      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
   7.212 -
   7.213 -    val u = Free u';
   7.214 -    val v = Free v';
   7.215 -    val q = Free (fst p', mk_pred1T B);
   7.216 -
   7.217 -    val xctrs = map2 (curry Term.list_comb) ctrs xss;
   7.218 -    val yctrs = map2 (curry Term.list_comb) ctrs yss;
   7.219 -
   7.220 -    val xfs = map2 (curry Term.list_comb) fs xss;
   7.221 -    val xgs = map2 (curry Term.list_comb) gs xss;
   7.222 -
   7.223 -    val fcase = Term.list_comb (casex, fs);
   7.224 -
   7.225 -    val ufcase = fcase $ u;
   7.226 -    val vfcase = fcase $ v;
   7.227 -
   7.228 -    (* TODO: Eta-expension is for compatibility with the old datatype package (but it also provides
   7.229 -       nicer names). Consider removing. *)
   7.230 -    val eta_fs = map2 eta_expand_arg xss xfs;
   7.231 -    val eta_gs = map2 eta_expand_arg xss xgs;
   7.232 -
   7.233 -    val eta_fcase = Term.list_comb (casex, eta_fs);
   7.234 -    val eta_gcase = Term.list_comb (casex, eta_gs);
   7.235 -
   7.236 -    val eta_ufcase = eta_fcase $ u;
   7.237 -    val eta_vgcase = eta_gcase $ v;
   7.238 -
   7.239 -    fun mk_uu_eq () = HOLogic.mk_eq (u, u);
   7.240 -
   7.241 -    val uv_eq = mk_Trueprop_eq (u, v);
   7.242 -
   7.243 -    val exist_xs_u_eq_ctrs =
   7.244 -      map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (u, xctr))) xctrs xss;
   7.245 -
   7.246 -    val unique_disc_no_def = TrueI; (*arbitrary marker*)
   7.247 -    val alternate_disc_no_def = FalseE; (*arbitrary marker*)
   7.248 -
   7.249 -    fun alternate_disc_lhs get_udisc k =
   7.250 -      HOLogic.mk_not
   7.251 -        (let val b = nth disc_bindings (k - 1) in
   7.252 -           if is_disc_binding_valid b then get_udisc b (k - 1) else nth exist_xs_u_eq_ctrs (k - 1)
   7.253 -         end);
   7.254 -
   7.255 -    val (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs,
   7.256 -         sel_defss, lthy') =
   7.257 -      if no_dests then
   7.258 -        (true, [], [], [], [], [], [], [], [], [], no_defs_lthy)
   7.259 -      else
   7.260 -        let
   7.261 -          fun disc_free b = Free (Binding.name_of b, mk_pred1T dataT);
   7.262 -
   7.263 -          fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr);
   7.264 -
   7.265 -          fun alternate_disc k =
   7.266 -            Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k));
   7.267 -
   7.268 -          fun mk_sel_case_args b proto_sels T =
   7.269 -            map2 (fn Ts => fn k =>
   7.270 -              (case AList.lookup (op =) proto_sels k of
   7.271 -                NONE =>
   7.272 -                (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
   7.273 -                  NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T)
   7.274 -                | SOME t => t |> Type.constraint (Ts ---> T) |> Syntax.check_term no_defs_lthy)
   7.275 -              | SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
   7.276 -
   7.277 -          fun sel_spec b proto_sels =
   7.278 -            let
   7.279 -              val _ =
   7.280 -                (case duplicates (op =) (map fst proto_sels) of
   7.281 -                   k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^
   7.282 -                     " for constructor " ^
   7.283 -                     quote (Syntax.string_of_term no_defs_lthy (nth ctrs (k - 1))))
   7.284 -                 | [] => ())
   7.285 -              val T =
   7.286 -                (case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of
   7.287 -                  [T] => T
   7.288 -                | T :: T' :: _ => error ("Inconsistent range type for selector " ^
   7.289 -                    quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
   7.290 -                    " vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T')));
   7.291 -            in
   7.292 -              mk_Trueprop_eq (Free (Binding.name_of b, dataT --> T) $ u,
   7.293 -                Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T) $ u)
   7.294 -            end;
   7.295 -
   7.296 -          val sel_bindings = flat sel_bindingss;
   7.297 -          val uniq_sel_bindings = distinct Binding.eq_name sel_bindings;
   7.298 -          val all_sels_distinct = (length uniq_sel_bindings = length sel_bindings);
   7.299 -
   7.300 -          val sel_binding_index =
   7.301 -            if all_sels_distinct then 1 upto length sel_bindings
   7.302 -            else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) sel_bindings;
   7.303 -
   7.304 -          val proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss);
   7.305 -          val sel_infos =
   7.306 -            AList.group (op =) (sel_binding_index ~~ proto_sels)
   7.307 -            |> sort (int_ord o pairself fst)
   7.308 -            |> map snd |> curry (op ~~) uniq_sel_bindings;
   7.309 -          val sel_bindings = map fst sel_infos;
   7.310 -
   7.311 -          fun unflat_selss xs = unflat_lookup Binding.eq_name sel_bindings xs sel_bindingss;
   7.312 -
   7.313 -          val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
   7.314 -            no_defs_lthy
   7.315 -            |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_u_eq_ctr => fn b =>
   7.316 -                if Binding.is_empty b then
   7.317 -                  if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
   7.318 -                  else pair (alternate_disc k, alternate_disc_no_def)
   7.319 -                else if Binding.eq_name (b, equal_binding) then
   7.320 -                  pair (Term.lambda u exist_xs_u_eq_ctr, refl)
   7.321 -                else
   7.322 -                  Specification.definition (SOME (b, NONE, NoSyn),
   7.323 -                    ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd)
   7.324 -              ks ms exist_xs_u_eq_ctrs disc_bindings
   7.325 -            ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
   7.326 -              Specification.definition (SOME (b, NONE, NoSyn),
   7.327 -                ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos
   7.328 -            ||> `Local_Theory.restore;
   7.329 -
   7.330 -          val phi = Proof_Context.export_morphism lthy lthy';
   7.331 -
   7.332 -          val disc_defs = map (Morphism.thm phi) raw_disc_defs;
   7.333 -          val sel_defs = map (Morphism.thm phi) raw_sel_defs;
   7.334 -          val sel_defss = unflat_selss sel_defs;
   7.335 -
   7.336 -          val discs0 = map (Morphism.term phi) raw_discs;
   7.337 -          val selss0 = unflat_selss (map (Morphism.term phi) raw_sels);
   7.338 -
   7.339 -          val discs = map (mk_disc_or_sel As) discs0;
   7.340 -          val selss = map (map (mk_disc_or_sel As)) selss0;
   7.341 -
   7.342 -          val udiscs = map (rapp u) discs;
   7.343 -          val uselss = map (map (rapp u)) selss;
   7.344 -
   7.345 -          val vdiscs = map (rapp v) discs;
   7.346 -          val vselss = map (map (rapp v)) selss;
   7.347 -        in
   7.348 -          (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs,
   7.349 -           sel_defss, lthy')
   7.350 -        end;
   7.351 -
   7.352 -    fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
   7.353 -
   7.354 -    val exhaust_goal =
   7.355 -      let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (u, xctr)]) in
   7.356 -        fold_rev Logic.all [p, u] (mk_imp_p (map2 mk_prem xctrs xss))
   7.357 -      end;
   7.358 -
   7.359 -    val inject_goalss =
   7.360 -      let
   7.361 -        fun mk_goal _ _ [] [] = []
   7.362 -          | mk_goal xctr yctr xs ys =
   7.363 -            [fold_rev Logic.all (xs @ ys) (mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr),
   7.364 -              Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))];
   7.365 -      in
   7.366 -        map4 mk_goal xctrs yctrs xss yss
   7.367 -      end;
   7.368 -
   7.369 -    val half_distinct_goalss =
   7.370 -      let
   7.371 -        fun mk_goal ((xs, xc), (xs', xc')) =
   7.372 -          fold_rev Logic.all (xs @ xs')
   7.373 -            (HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (xc, xc'))));
   7.374 -      in
   7.375 -        map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs)))
   7.376 -      end;
   7.377 -
   7.378 -    val cases_goal =
   7.379 -      map3 (fn xs => fn xctr => fn xf =>
   7.380 -        fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xss xctrs xfs;
   7.381 -
   7.382 -    val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss @ [cases_goal];
   7.383 -
   7.384 -    fun after_qed thmss lthy =
   7.385 -      let
   7.386 -        val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) =
   7.387 -          (hd thmss, apsnd (chop (n * n)) (chop n (tl thmss)));
   7.388 -
   7.389 -        val inject_thms = flat inject_thmss;
   7.390 -
   7.391 -        val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
   7.392 -
   7.393 -        fun inst_thm t thm =
   7.394 -          Drule.instantiate' [] [SOME (certify lthy t)]
   7.395 -            (Thm.instantiate (Tinst, []) (Drule.zero_var_indexes thm));
   7.396 -
   7.397 -        val uexhaust_thm = inst_thm u exhaust_thm;
   7.398 -
   7.399 -        val exhaust_cases = map base_name_of_ctr ctrs;
   7.400 -
   7.401 -        val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss;
   7.402 -
   7.403 -        val (distinct_thms, (distinct_thmsss', distinct_thmsss)) =
   7.404 -          join_halves n half_distinct_thmss other_half_distinct_thmss ||> `transpose;
   7.405 -
   7.406 -        val nchotomy_thm =
   7.407 -          let
   7.408 -            val goal =
   7.409 -              HOLogic.mk_Trueprop (HOLogic.mk_all (fst u', snd u',
   7.410 -                Library.foldr1 HOLogic.mk_disj exist_xs_u_eq_ctrs));
   7.411 -          in
   7.412 -            Goal.prove_sorry lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
   7.413 -            |> Thm.close_derivation
   7.414 -          end;
   7.415 -
   7.416 -        val (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
   7.417 -             disc_exhaust_thms, collapse_thms, expand_thms, case_conv_thms) =
   7.418 -          if no_dests then
   7.419 -            ([], [], [], [], [], [], [], [], [], [])
   7.420 -          else
   7.421 -            let
   7.422 -              fun make_sel_thm xs' case_thm sel_def =
   7.423 -                zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs')
   7.424 -                    (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
   7.425 -
   7.426 -              fun has_undefined_rhs thm =
   7.427 -                (case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of
   7.428 -                  Const (@{const_name undefined}, _) => true
   7.429 -                | _ => false);
   7.430 -
   7.431 -              val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss;
   7.432 -
   7.433 -              val all_sel_thms =
   7.434 -                (if all_sels_distinct andalso forall null sel_defaultss then
   7.435 -                   flat sel_thmss
   7.436 -                 else
   7.437 -                   map_product (fn s => fn (xs', c) => make_sel_thm xs' c s) sel_defs
   7.438 -                     (xss' ~~ case_thms))
   7.439 -                |> filter_out has_undefined_rhs;
   7.440 -
   7.441 -              fun mk_unique_disc_def () =
   7.442 -                let
   7.443 -                  val m = the_single ms;
   7.444 -                  val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs);
   7.445 -                in
   7.446 -                  Goal.prove_sorry lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm)
   7.447 -                  |> Thm.close_derivation
   7.448 -                  |> singleton (Proof_Context.export names_lthy lthy)
   7.449 -                end;
   7.450 -
   7.451 -              fun mk_alternate_disc_def k =
   7.452 -                let
   7.453 -                  val goal =
   7.454 -                    mk_Trueprop_eq (alternate_disc_lhs (K (nth udiscs)) (3 - k),
   7.455 -                      nth exist_xs_u_eq_ctrs (k - 1));
   7.456 -                in
   7.457 -                  Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   7.458 -                    mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k))
   7.459 -                      (nth distinct_thms (2 - k)) uexhaust_thm)
   7.460 -                  |> Thm.close_derivation
   7.461 -                  |> singleton (Proof_Context.export names_lthy lthy)
   7.462 -                end;
   7.463 -
   7.464 -              val has_alternate_disc_def =
   7.465 -                exists (fn def => Thm.eq_thm_prop (def, alternate_disc_no_def)) disc_defs;
   7.466 -
   7.467 -              val disc_defs' =
   7.468 -                map2 (fn k => fn def =>
   7.469 -                  if Thm.eq_thm_prop (def, unique_disc_no_def) then mk_unique_disc_def ()
   7.470 -                  else if Thm.eq_thm_prop (def, alternate_disc_no_def) then mk_alternate_disc_def k
   7.471 -                  else def) ks disc_defs;
   7.472 -
   7.473 -              val discD_thms = map (fn def => def RS iffD1) disc_defs';
   7.474 -              val discI_thms =
   7.475 -                map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms
   7.476 -                  disc_defs';
   7.477 -              val not_discI_thms =
   7.478 -                map2 (fn m => fn def => funpow m (fn thm => allI RS thm)
   7.479 -                    (unfold_thms lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
   7.480 -                  ms disc_defs';
   7.481 -
   7.482 -              val (disc_thmss', disc_thmss) =
   7.483 -                let
   7.484 -                  fun mk_thm discI _ [] = refl RS discI
   7.485 -                    | mk_thm _ not_discI [distinct] = distinct RS not_discI;
   7.486 -                  fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss;
   7.487 -                in
   7.488 -                  map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
   7.489 -                end;
   7.490 -
   7.491 -              val disc_thms = flat (map2 (fn b => if is_disc_binding_valid b then I else K [])
   7.492 -                disc_bindings disc_thmss);
   7.493 -
   7.494 -              val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) =
   7.495 -                let
   7.496 -                  fun mk_goal [] = []
   7.497 -                    | mk_goal [((_, udisc), (_, udisc'))] =
   7.498 -                      [Logic.all u (Logic.mk_implies (HOLogic.mk_Trueprop udisc,
   7.499 -                         HOLogic.mk_Trueprop (HOLogic.mk_not udisc')))];
   7.500 -
   7.501 -                  fun prove tac goal =
   7.502 -                    Goal.prove_sorry lthy [] [] goal (K tac)
   7.503 -                    |> Thm.close_derivation;
   7.504 -
   7.505 -                  val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs));
   7.506 -
   7.507 -                  val half_goalss = map mk_goal half_pairss;
   7.508 -                  val half_thmss =
   7.509 -                    map3 (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] =>
   7.510 -                        fn disc_thm => [prove (mk_half_disc_exclude_tac m discD disc_thm) goal])
   7.511 -                      half_goalss half_pairss (flat disc_thmss');
   7.512 -
   7.513 -                  val other_half_goalss = map (mk_goal o map swap) half_pairss;
   7.514 -                  val other_half_thmss =
   7.515 -                    map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss
   7.516 -                      other_half_goalss;
   7.517 -                in
   7.518 -                  join_halves n half_thmss other_half_thmss ||> `transpose
   7.519 -                  |>> has_alternate_disc_def ? K []
   7.520 -                end;
   7.521 -
   7.522 -              val disc_exhaust_thm =
   7.523 -                let
   7.524 -                  fun mk_prem udisc = mk_imp_p [HOLogic.mk_Trueprop udisc];
   7.525 -                  val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem udiscs));
   7.526 -                in
   7.527 -                  Goal.prove_sorry lthy [] [] goal (fn _ =>
   7.528 -                    mk_disc_exhaust_tac n exhaust_thm discI_thms)
   7.529 -                  |> Thm.close_derivation
   7.530 -                end;
   7.531 -
   7.532 -              val (collapse_thms, collapse_thm_opts) =
   7.533 -                let
   7.534 -                  fun mk_goal ctr udisc usels =
   7.535 -                    let
   7.536 -                      val prem = HOLogic.mk_Trueprop udisc;
   7.537 -                      val concl =
   7.538 -                        mk_Trueprop_eq ((null usels ? swap) (Term.list_comb (ctr, usels), u));
   7.539 -                    in
   7.540 -                      if prem aconv concl then NONE
   7.541 -                      else SOME (Logic.all u (Logic.mk_implies (prem, concl)))
   7.542 -                    end;
   7.543 -                  val goals = map3 mk_goal ctrs udiscs uselss;
   7.544 -                in
   7.545 -                  map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal =>
   7.546 -                    Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   7.547 -                      mk_collapse_tac ctxt m discD sel_thms)
   7.548 -                    |> Thm.close_derivation
   7.549 -                    |> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals
   7.550 -                  |> `(map_filter I)
   7.551 -                end;
   7.552 -
   7.553 -              val expand_thms =
   7.554 -                let
   7.555 -                  fun mk_prems k udisc usels vdisc vsels =
   7.556 -                    (if k = n then [] else [mk_Trueprop_eq (udisc, vdisc)]) @
   7.557 -                    (if null usels then
   7.558 -                       []
   7.559 -                     else
   7.560 -                       [Logic.list_implies
   7.561 -                          (if n = 1 then [] else map HOLogic.mk_Trueprop [udisc, vdisc],
   7.562 -                             HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   7.563 -                               (map2 (curry HOLogic.mk_eq) usels vsels)))]);
   7.564 -
   7.565 -                  val goal =
   7.566 -                    Library.foldr Logic.list_implies
   7.567 -                      (map5 mk_prems ks udiscs uselss vdiscs vselss, uv_eq);
   7.568 -                  val uncollapse_thms =
   7.569 -                    map2 (fn NONE => K asm_rl | SOME thm => fn [] => thm | _ => thm RS sym)
   7.570 -                      collapse_thm_opts uselss;
   7.571 -                in
   7.572 -                  [Goal.prove_sorry lthy [] [] goal (fn _ =>
   7.573 -                     mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
   7.574 -                       (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
   7.575 -                       disc_exclude_thmsss')]
   7.576 -                  |> map Thm.close_derivation
   7.577 -                  |> Proof_Context.export names_lthy lthy
   7.578 -                end;
   7.579 -
   7.580 -              val case_conv_thms =
   7.581 -                let
   7.582 -                  fun mk_body f usels = Term.list_comb (f, usels);
   7.583 -                  val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs (map2 mk_body fs uselss));
   7.584 -                in
   7.585 -                  [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   7.586 -                     mk_case_conv_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)]
   7.587 -                  |> map Thm.close_derivation
   7.588 -                  |> Proof_Context.export names_lthy lthy
   7.589 -                end;
   7.590 -            in
   7.591 -              (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
   7.592 -               [disc_exhaust_thm], collapse_thms, expand_thms, case_conv_thms)
   7.593 -            end;
   7.594 -
   7.595 -        val (case_cong_thm, weak_case_cong_thm) =
   7.596 -          let
   7.597 -            fun mk_prem xctr xs xf xg =
   7.598 -              fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr),
   7.599 -                mk_Trueprop_eq (xf, xg)));
   7.600 -
   7.601 -            val goal =
   7.602 -              Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss xfs xgs,
   7.603 -                 mk_Trueprop_eq (eta_ufcase, eta_vgcase));
   7.604 -            val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase));
   7.605 -          in
   7.606 -            (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms),
   7.607 -             Goal.prove_sorry lthy [] [] weak_goal (K (etac arg_cong 1)))
   7.608 -            |> pairself (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy))
   7.609 -          end;
   7.610 -
   7.611 -        val (split_thm, split_asm_thm) =
   7.612 -          let
   7.613 -            fun mk_conjunct xctr xs f_xs =
   7.614 -              list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (u, xctr), q $ f_xs));
   7.615 -            fun mk_disjunct xctr xs f_xs =
   7.616 -              list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr),
   7.617 -                HOLogic.mk_not (q $ f_xs)));
   7.618 -
   7.619 -            val lhs = q $ ufcase;
   7.620 -
   7.621 -            val goal =
   7.622 -              mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs));
   7.623 -            val asm_goal =
   7.624 -              mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj
   7.625 -                (map3 mk_disjunct xctrs xss xfs)));
   7.626 -
   7.627 -            val split_thm =
   7.628 -              Goal.prove_sorry lthy [] [] goal
   7.629 -                (fn _ => mk_split_tac lthy uexhaust_thm case_thms inject_thmss distinct_thmsss)
   7.630 -              |> Thm.close_derivation
   7.631 -              |> singleton (Proof_Context.export names_lthy lthy);
   7.632 -            val split_asm_thm =
   7.633 -              Goal.prove_sorry lthy [] [] asm_goal (fn {context = ctxt, ...} =>
   7.634 -                mk_split_asm_tac ctxt split_thm)
   7.635 -              |> Thm.close_derivation
   7.636 -              |> singleton (Proof_Context.export names_lthy lthy);
   7.637 -          in
   7.638 -            (split_thm, split_asm_thm)
   7.639 -          end;
   7.640 -
   7.641 -        val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
   7.642 -        val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name));
   7.643 -
   7.644 -        val notes =
   7.645 -          [(caseN, case_thms, simp_attrs),
   7.646 -           (case_congN, [case_cong_thm], []),
   7.647 -           (case_convN, case_conv_thms, []),
   7.648 -           (collapseN, collapse_thms, simp_attrs),
   7.649 -           (discsN, disc_thms, simp_attrs),
   7.650 -           (disc_excludeN, disc_exclude_thms, []),
   7.651 -           (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
   7.652 -           (distinctN, distinct_thms, simp_attrs @ induct_simp_attrs),
   7.653 -           (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
   7.654 -           (expandN, expand_thms, []),
   7.655 -           (injectN, inject_thms, iff_attrs @ induct_simp_attrs),
   7.656 -           (nchotomyN, [nchotomy_thm], []),
   7.657 -           (selsN, all_sel_thms, simp_attrs),
   7.658 -           (splitN, [split_thm], []),
   7.659 -           (split_asmN, [split_asm_thm], []),
   7.660 -           (splitsN, [split_thm, split_asm_thm], []),
   7.661 -           (weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)]
   7.662 -          |> filter_out (null o #2)
   7.663 -          |> map (fn (thmN, thms, attrs) =>
   7.664 -            ((qualify true (Binding.name thmN), attrs), [(thms, [])]));
   7.665 -
   7.666 -        val notes' =
   7.667 -          [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
   7.668 -          |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
   7.669 -      in
   7.670 -        ((discs, selss, exhaust_thm, inject_thms, distinct_thms, case_thms, disc_thmss, discI_thms,
   7.671 -          sel_thmss),
   7.672 -          lthy
   7.673 -          |> not rep_compat ?
   7.674 -             (Local_Theory.declaration {syntax = false, pervasive = true}
   7.675 -               (fn phi => Case_Translation.register
   7.676 -                 (Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
   7.677 -          |> Local_Theory.notes (notes' @ notes) |> snd)
   7.678 -      end;
   7.679 -  in
   7.680 -    (goalss, after_qed, lthy')
   7.681 -  end;
   7.682 -
   7.683 -fun wrap_free_constructors tacss = (fn (goalss, after_qed, lthy) =>
   7.684 -  map2 (map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])) goalss tacss
   7.685 -  |> (fn thms => after_qed thms lthy)) oo prepare_wrap_free_constructors (K I);
   7.686 -
   7.687 -val wrap_free_constructors_cmd = (fn (goalss, after_qed, lthy) =>
   7.688 -  Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
   7.689 -  prepare_wrap_free_constructors Syntax.read_term;
   7.690 -
   7.691 -fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
   7.692 -
   7.693 -val parse_bindings = parse_bracket_list parse_binding;
   7.694 -val parse_bindingss = parse_bracket_list parse_bindings;
   7.695 -
   7.696 -val parse_bound_term = (parse_binding --| @{keyword ":"}) -- Parse.term;
   7.697 -val parse_bound_terms = parse_bracket_list parse_bound_term;
   7.698 -val parse_bound_termss = parse_bracket_list parse_bound_terms;
   7.699 -
   7.700 -val parse_wrap_options =
   7.701 -  Scan.optional (@{keyword "("} |-- Parse.list1 ((@{keyword "no_dests"} >> K (true, false)) ||
   7.702 -      (@{keyword "rep_compat"} >> K (false, true))) --| @{keyword ")"}
   7.703 -    >> (pairself (exists I) o split_list)) (false, false);
   7.704 -
   7.705 -val _ =
   7.706 -  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"}
   7.707 -    "wrap an existing (co)datatype's constructors"
   7.708 -    ((parse_wrap_options -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) --
   7.709 -      Parse.term -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
   7.710 -        Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
   7.711 -     >> wrap_free_constructors_cmd);
   7.712 -
   7.713 -end;
     8.1 --- a/src/HOL/BNF/Tools/bnf_wrap_tactics.ML	Fri Apr 26 14:16:05 2013 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,125 +0,0 @@
     8.4 -(*  Title:      HOL/BNF/Tools/bnf_wrap_tactics.ML
     8.5 -    Author:     Jasmin Blanchette, TU Muenchen
     8.6 -    Copyright   2012
     8.7 -
     8.8 -Tactics for wrapping datatypes.
     8.9 -*)
    8.10 -
    8.11 -signature BNF_WRAP_TACTICS =
    8.12 -sig
    8.13 -  val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
    8.14 -  val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic
    8.15 -  val mk_case_conv_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list ->
    8.16 -    tactic
    8.17 -  val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
    8.18 -  val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
    8.19 -  val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
    8.20 -    thm list list list -> thm list list list -> tactic
    8.21 -  val mk_half_disc_exclude_tac: int -> thm -> thm -> tactic
    8.22 -  val mk_nchotomy_tac: int -> thm -> tactic
    8.23 -  val mk_other_half_disc_exclude_tac: thm -> tactic
    8.24 -  val mk_split_tac: Proof.context ->
    8.25 -    thm -> thm list -> thm list list -> thm list list list -> tactic
    8.26 -  val mk_split_asm_tac: Proof.context -> thm -> tactic
    8.27 -  val mk_unique_disc_def_tac: int -> thm -> tactic
    8.28 -end;
    8.29 -
    8.30 -structure BNF_Wrap_Tactics : BNF_WRAP_TACTICS =
    8.31 -struct
    8.32 -
    8.33 -open BNF_Util
    8.34 -open BNF_Tactics
    8.35 -
    8.36 -val meta_mp = @{thm meta_mp};
    8.37 -
    8.38 -fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P});
    8.39 -
    8.40 -fun mk_nchotomy_tac n exhaust =
    8.41 -  (rtac allI THEN' rtac exhaust THEN'
    8.42 -   EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1;
    8.43 -
    8.44 -fun mk_unique_disc_def_tac m uexhaust =
    8.45 -  EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1;
    8.46 -
    8.47 -fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
    8.48 -  EVERY' ([rtac (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans),
    8.49 -    rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
    8.50 -    hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
    8.51 -    rtac distinct, rtac uexhaust] @
    8.52 -    (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
    8.53 -     |> k = 1 ? swap |> op @)) 1;
    8.54 -
    8.55 -fun mk_half_disc_exclude_tac m discD disc' =
    8.56 -  (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' rtac disc') 1;
    8.57 -
    8.58 -fun mk_other_half_disc_exclude_tac half = (etac @{thm contrapos_pn} THEN' etac half) 1;
    8.59 -
    8.60 -fun mk_disc_exhaust_tac n exhaust discIs =
    8.61 -  (rtac exhaust THEN'
    8.62 -   EVERY' (map2 (fn k => fn discI =>
    8.63 -     dtac discI THEN' select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) discIs)) 1;
    8.64 -
    8.65 -fun mk_collapse_tac ctxt m discD sels =
    8.66 -  (dtac discD THEN'
    8.67 -   (if m = 0 then
    8.68 -      atac
    8.69 -    else
    8.70 -      REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN'
    8.71 -      SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)) 1;
    8.72 -
    8.73 -fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
    8.74 -    disc_excludesss' =
    8.75 -  if ms = [0] then
    8.76 -    (rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN'
    8.77 -     TRY o EVERY' [rtac udisc_exhaust, atac, rtac vdisc_exhaust, atac]) 1
    8.78 -  else
    8.79 -    let val ks = 1 upto n in
    8.80 -      (rtac udisc_exhaust THEN'
    8.81 -       EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' =>
    8.82 -           fn uuncollapse =>
    8.83 -         EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac,
    8.84 -           rtac sym, rtac vdisc_exhaust,
    8.85 -           EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse =>
    8.86 -             EVERY'
    8.87 -               (if k' = k then
    8.88 -                  [rtac (vuncollapse RS trans), TRY o atac] @
    8.89 -                  (if m = 0 then
    8.90 -                     [rtac refl]
    8.91 -                   else
    8.92 -                     [if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac],
    8.93 -                      REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE,
    8.94 -                      asm_simp_tac (ss_only [] ctxt)])
    8.95 -                else
    8.96 -                  [dtac (the_single (if k = n then disc_excludes else disc_excludes')),
    8.97 -                   etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),
    8.98 -                   atac, atac]))
    8.99 -             ks disc_excludess disc_excludess' uncollapses)])
   8.100 -         ks ms disc_excludesss disc_excludesss' uncollapses)) 1
   8.101 -    end;
   8.102 -
   8.103 -fun mk_case_conv_tac ctxt n uexhaust cases discss' selss =
   8.104 -  (rtac uexhaust THEN'
   8.105 -   EVERY' (map3 (fn casex => fn if_discs => fn sels =>
   8.106 -       EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), rtac casex])
   8.107 -     cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)) 1;
   8.108 -
   8.109 -fun mk_case_cong_tac ctxt uexhaust cases =
   8.110 -  (rtac uexhaust THEN'
   8.111 -   EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases)) 1;
   8.112 -
   8.113 -val naked_ctxt = @{theory_context HOL};
   8.114 -
   8.115 -(* TODO: More precise "simp_thms"; get rid of "blast_tac" *)
   8.116 -fun mk_split_tac ctxt uexhaust cases injectss distinctsss =
   8.117 -  rtac uexhaust 1 THEN
   8.118 -  ALLGOALS (fn k => (hyp_subst_tac THEN'
   8.119 -     simp_tac (ss_only (@{thms simp_thms} @ cases @ nth injectss (k - 1) @
   8.120 -       flat (nth distinctsss (k - 1))) ctxt)) k) THEN
   8.121 -  ALLGOALS (blast_tac naked_ctxt);
   8.122 -
   8.123 -val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
   8.124 -
   8.125 -fun mk_split_asm_tac ctxt split =
   8.126 -  rtac (split RS trans) 1 THEN unfold_thms_tac ctxt split_asm_thms THEN rtac refl 1;
   8.127 -
   8.128 -end;