src/HOL/Library/bnf_lfp_countable.ML
author blanchet
Wed, 03 Sep 2014 22:47:05 +0200
changeset 58168 6b6c41aa780b
parent 58166 86a374caeb82
child 58170 d84bab7ed89e
permissions -rw-r--r--
improved tactic further
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58160
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Library/bnf_lfp_countable.ML
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
     3
    Copyright   2014
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
     4
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
     5
Countability tactic for BNF datatypes.
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
     6
*)
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
     7
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
     8
signature BNF_LFP_COUNTABLE =
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
     9
sig
58165
2ec97d9c1e83 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
blanchet
parents: 58161
diff changeset
    10
  val derive_encode_injectives_thms: Proof.context -> string list -> thm list
58161
deeff89d5b9e added compatibility function
blanchet
parents: 58160
diff changeset
    11
  val countable_datatype_tac: Proof.context -> tactic
58160
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    12
end;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    13
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    14
structure BNF_LFP_Countable : BNF_LFP_COUNTABLE =
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    15
struct
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    16
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    17
open BNF_FP_Rec_Sugar_Util
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    18
open BNF_Def
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    19
open BNF_Util
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    20
open BNF_Tactics
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    21
open BNF_FP_Util
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    22
open BNF_FP_Def_Sugar
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    23
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    24
fun nchotomy_tac nchotomy =
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    25
  HEADGOAL (rtac (nchotomy RS @{thm all_reg[rotated]}) THEN'
58168
6b6c41aa780b improved tactic further
blanchet
parents: 58166
diff changeset
    26
    REPEAT_ALL_NEW (resolve_tac [allI, impI] ORELSE' eresolve_tac [exE, disjE]));
58160
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    27
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    28
fun meta_spec_mp_tac 0 = K all_tac
58165
2ec97d9c1e83 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
blanchet
parents: 58161
diff changeset
    29
  | meta_spec_mp_tac depth =
2ec97d9c1e83 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
blanchet
parents: 58161
diff changeset
    30
    dtac meta_spec THEN' meta_spec_mp_tac (depth - 1) THEN' dtac meta_mp THEN' atac;
58160
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    31
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    32
val use_induction_hypothesis_tac =
58161
deeff89d5b9e added compatibility function
blanchet
parents: 58160
diff changeset
    33
  DEEPEN (1, 64 (* large number *))
58160
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    34
    (fn depth => meta_spec_mp_tac depth THEN' etac allE THEN' etac impE THEN' atac THEN' atac) 0;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    35
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    36
val same_ctr_simps =
58165
2ec97d9c1e83 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
blanchet
parents: 58161
diff changeset
    37
  @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split snd_conv simp_thms};
58166
86a374caeb82 improved new countability tactic
blanchet
parents: 58165
diff changeset
    38
val distinct_ctrs_simps = @{thms sum_encode_eq sum.inject sum.distinct simp_thms};
58160
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    39
58166
86a374caeb82 improved new countability tactic
blanchet
parents: 58165
diff changeset
    40
fun same_ctr_tac ctxt injects recs map_congs' inj_map_strongs' =
86a374caeb82 improved new countability tactic
blanchet
parents: 58165
diff changeset
    41
  HEADGOAL (asm_full_simp_tac
86a374caeb82 improved new countability tactic
blanchet
parents: 58165
diff changeset
    42
      (ss_only (injects @ recs @ map_congs' @ same_ctr_simps) ctxt) THEN_MAYBE'
86a374caeb82 improved new countability tactic
blanchet
parents: 58165
diff changeset
    43
    TRY o REPEAT_ALL_NEW (rtac conjI) THEN_ALL_NEW
86a374caeb82 improved new countability tactic
blanchet
parents: 58165
diff changeset
    44
    REPEAT_ALL_NEW (eresolve_tac (conjE :: inj_map_strongs')) THEN_ALL_NEW
86a374caeb82 improved new countability tactic
blanchet
parents: 58165
diff changeset
    45
    use_induction_hypothesis_tac);
58160
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    46
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    47
fun distinct_ctrs_tac ctxt recs =
58166
86a374caeb82 improved new countability tactic
blanchet
parents: 58165
diff changeset
    48
  HEADGOAL (asm_full_simp_tac (ss_only (recs @ distinct_ctrs_simps) ctxt));
58160
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    49
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    50
fun mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs' =
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    51
  let val ks = 1 upto n in
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    52
    EVERY (maps (fn k => nchotomy_tac nchotomy :: map (fn k' =>
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    53
      if k = k' then same_ctr_tac ctxt injects recs map_comps' inj_map_strongs'
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    54
      else distinct_ctrs_tac ctxt recs) ks) ks)
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    55
  end;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    56
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    57
fun mk_encode_injectives_tac ctxt ns induct nchotomys injectss recss map_comps' inj_map_strongs' =
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    58
  HEADGOAL (rtac induct) THEN
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    59
  EVERY (map4 (fn n => fn nchotomy => fn injects => fn recs =>
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    60
      mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs')
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    61
    ns nchotomys injectss recss);
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    62
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    63
fun endgame_tac ctxt encode_injectives =
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    64
  unfold_thms_tac ctxt @{thms inj_on_def ball_UNIV} THEN
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    65
  ALLGOALS (rtac exI THEN' rtac allI THEN' resolve_tac encode_injectives);
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    66
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    67
fun encode_sumN n k t =
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    68
  Balanced_Tree.access {init = t,
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    69
      left = fn t => @{const sum_encode} $ (@{const Inl (nat, nat)} $ t),
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    70
      right = fn t => @{const sum_encode} $ (@{const Inr (nat, nat)} $ t)}
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    71
    n k;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    72
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    73
fun encode_tuple [] = @{term "0 :: nat"}
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    74
  | encode_tuple ts =
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    75
    Balanced_Tree.make (fn (t, u) => @{const prod_encode} $ (@{const Pair (nat, nat)} $ u $ t)) ts;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    76
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    77
fun mk_to_nat T = Const (@{const_name to_nat}, T --> HOLogic.natT);
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    78
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    79
fun mk_encode_funs ctxt fpTs ns ctrss0 recs0 =
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    80
  let
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    81
    val thy = Proof_Context.theory_of ctxt;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    82
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    83
    val nn = length ns;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    84
    val recs as rec1 :: _ =
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    85
      map2 (fn fpT => mk_co_rec thy Least_FP fpT (replicate nn HOLogic.natT)) fpTs recs0;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    86
    val arg_Ts = binder_fun_types (fastype_of rec1);
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    87
    val arg_Tss = Library.unflat ctrss0 arg_Ts;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    88
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    89
    fun mk_U (Type (@{type_name prod}, [T1, T2])) =
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    90
        if member (op =) fpTs T1 then T2 else HOLogic.mk_prodT (mk_U T1, mk_U T2)
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    91
      | mk_U (Type (s, Ts)) = Type (s, map mk_U Ts)
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    92
      | mk_U T = T;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    93
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    94
    fun mk_nat (j, T) =
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    95
      if T = HOLogic.natT then
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    96
        SOME (Bound j)
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    97
      else if member (op =) fpTs T then
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    98
        NONE
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
    99
      else if exists_subtype_in fpTs T then
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   100
        let val U = mk_U T in
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   101
          SOME (mk_to_nat U $ (build_map ctxt [] (snd_const o fst) (T, U) $ Bound j))
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   102
        end
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   103
      else
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   104
        SOME (mk_to_nat T $ Bound j);
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   105
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   106
    fun mk_arg n (k, arg_T) =
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   107
      let
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   108
        val bound_Ts = rev (binder_types arg_T);
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   109
        val nats = map_filter mk_nat (tag_list 0 bound_Ts);
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   110
      in
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   111
        fold (fn T => fn t => Abs (Name.uu, T, t)) bound_Ts (encode_sumN n k (encode_tuple nats))
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   112
      end;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   113
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   114
    val argss = map2 (map o mk_arg) ns (map (tag_list 1) arg_Tss);
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   115
  in
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   116
    map (fn recx => Term.list_comb (recx, flat argss)) recs
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   117
  end;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   118
58165
2ec97d9c1e83 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
blanchet
parents: 58161
diff changeset
   119
fun derive_encode_injectives_thms _ [] = []
2ec97d9c1e83 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
blanchet
parents: 58161
diff changeset
   120
  | derive_encode_injectives_thms ctxt fpT_names0 =
58160
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   121
    let
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   122
      fun not_datatype s = error (quote s ^ " is not a new-style datatype");
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   123
      fun not_mutually_recursive ss =
58166
86a374caeb82 improved new countability tactic
blanchet
parents: 58165
diff changeset
   124
        error (commas ss ^ " are not mutually recursive new-style datatypes");
58160
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   125
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   126
      fun lfp_sugar_of s =
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   127
        (case fp_sugar_of ctxt s of
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   128
          SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   129
        | _ => not_datatype s);
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   130
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   131
      val fpTs0 as Type (_, var_As) :: _ = #Ts (#fp_res (lfp_sugar_of (hd fpT_names0)));
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   132
      val fpT_names = map (fst o dest_Type) fpTs0;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   133
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   134
      val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) ctxt;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   135
      val As =
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   136
        map2 (fn s => fn TVar (_, S) => TFree (s, union (op =) @{sort countable} S))
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   137
          As_names var_As;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   138
      val fpTs = map (fn s => Type (s, As)) fpT_names;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   139
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   140
      val _ = subset (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   141
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   142
      fun mk_conjunct fpT x encode_fun =
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   143
        HOLogic.all_const fpT $ Abs (Name.uu, fpT,
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   144
          HOLogic.mk_imp (HOLogic.mk_eq (encode_fun $ x, encode_fun $ Bound 0),
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   145
            HOLogic.eq_const fpT $ x $ Bound 0));
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   146
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   147
      val fp_sugars as {fp_nesting_bnfs, common_co_inducts = induct :: _, ...} :: _ =
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   148
        map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   149
      val ctr_sugars = map #ctr_sugar fp_sugars;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   150
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   151
      val ctrss0 = map #ctrs ctr_sugars;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   152
      val ns = map length ctrss0;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   153
      val recs0 = map #co_rec fp_sugars;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   154
      val nchotomys = map #nchotomy ctr_sugars;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   155
      val injectss = map #injects ctr_sugars;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   156
      val rec_thmss = map #co_rec_thms fp_sugars;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   157
      val map_comps' = map (unfold_thms ctxt @{thms comp_def} o map_comp_of_bnf) fp_nesting_bnfs;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   158
      val inj_map_strongs' = map (Thm.permute_prems 0 ~1 o inj_map_strong_of_bnf) fp_nesting_bnfs;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   159
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   160
      val (xs, names_ctxt) = ctxt |> mk_Frees "x" fpTs;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   161
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   162
      val conjuncts = map3 mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0);
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   163
      val goal = HOLogic.mk_Trueprop (Balanced_Tree.make HOLogic.mk_conj conjuncts);
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   164
    in
58165
2ec97d9c1e83 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
blanchet
parents: 58161
diff changeset
   165
      Goal.prove ctxt [] [] goal (fn {context = ctxt, prems = _} =>
58160
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   166
        mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'
58161
deeff89d5b9e added compatibility function
blanchet
parents: 58160
diff changeset
   167
          inj_map_strongs')
58160
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   168
      |> HOLogic.conj_elims
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   169
      |> Proof_Context.export names_ctxt ctxt
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   170
      |> map Thm.close_derivation
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   171
    end;
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   172
58165
2ec97d9c1e83 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
blanchet
parents: 58161
diff changeset
   173
fun get_countable_goal_type_name (@{const Trueprop} $ (Const (@{const_name Ex}, _)
58160
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   174
    $ Abs (_, Type (_, [Type (s, _), _]), Const (@{const_name inj_on}, _) $ Bound 0
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   175
        $ Const (@{const_name top}, _)))) = s
58165
2ec97d9c1e83 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
blanchet
parents: 58161
diff changeset
   176
  | get_countable_goal_type_name _ = error "Wrong goal format for datatype countability tactic";
58160
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   177
58161
deeff89d5b9e added compatibility function
blanchet
parents: 58160
diff changeset
   178
fun core_countable_datatype_tac ctxt st =
58165
2ec97d9c1e83 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
blanchet
parents: 58161
diff changeset
   179
  let val T_names = map get_countable_goal_type_name (Thm.prems_of st) in
2ec97d9c1e83 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
blanchet
parents: 58161
diff changeset
   180
    endgame_tac ctxt (derive_encode_injectives_thms ctxt T_names) st
2ec97d9c1e83 'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems
blanchet
parents: 58161
diff changeset
   181
  end;
58160
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   182
58161
deeff89d5b9e added compatibility function
blanchet
parents: 58160
diff changeset
   183
fun countable_datatype_tac ctxt =
deeff89d5b9e added compatibility function
blanchet
parents: 58160
diff changeset
   184
  TRY (Class.intro_classes_tac []) THEN core_countable_datatype_tac ctxt;
58160
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   185
e4965b677ba9 added countable tactic for new-style datatypes
blanchet
parents:
diff changeset
   186
end;