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