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