blanchet@58160: (*  Title:      HOL/Library/bnf_lfp_countable.ML
blanchet@58160:     Author:     Jasmin Blanchette, TU Muenchen
blanchet@58160:     Copyright   2014
blanchet@58160: 
blanchet@58160: Countability tactic for BNF datatypes.
blanchet@58160: *)
blanchet@58160: 
blanchet@58160: signature BNF_LFP_COUNTABLE =
blanchet@58160: sig
blanchet@58165:   val derive_encode_injectives_thms: Proof.context -> string list -> thm list
blanchet@58161:   val countable_datatype_tac: Proof.context -> tactic
blanchet@58160: end;
blanchet@58160: 
blanchet@58160: structure BNF_LFP_Countable : BNF_LFP_COUNTABLE =
blanchet@58160: struct
blanchet@58160: 
blanchet@58160: open BNF_FP_Rec_Sugar_Util
blanchet@58160: open BNF_Def
blanchet@58160: open BNF_Util
blanchet@58160: open BNF_Tactics
blanchet@58160: open BNF_FP_Util
blanchet@58160: open BNF_FP_Def_Sugar
blanchet@58160: 
blanchet@58174: val countableS = @{sort countable};
blanchet@58174: 
blanchet@58160: fun nchotomy_tac nchotomy =
blanchet@58160:   HEADGOAL (rtac (nchotomy RS @{thm all_reg[rotated]}) THEN'
blanchet@58168:     REPEAT_ALL_NEW (resolve_tac [allI, impI] ORELSE' eresolve_tac [exE, disjE]));
blanchet@58160: 
blanchet@58160: fun meta_spec_mp_tac 0 = K all_tac
blanchet@58165:   | meta_spec_mp_tac depth =
blanchet@58165:     dtac meta_spec THEN' meta_spec_mp_tac (depth - 1) THEN' dtac meta_mp THEN' atac;
blanchet@58160: 
blanchet@58160: val use_induction_hypothesis_tac =
blanchet@58161:   DEEPEN (1, 64 (* large number *))
blanchet@58160:     (fn depth => meta_spec_mp_tac depth THEN' etac allE THEN' etac impE THEN' atac THEN' atac) 0;
blanchet@58160: 
blanchet@58172: val same_ctr_simps = @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split
blanchet@58172:   id_apply snd_conv simp_thms};
blanchet@58166: val distinct_ctrs_simps = @{thms sum_encode_eq sum.inject sum.distinct simp_thms};
blanchet@58160: 
blanchet@58166: fun same_ctr_tac ctxt injects recs map_congs' inj_map_strongs' =
blanchet@58166:   HEADGOAL (asm_full_simp_tac
blanchet@58166:       (ss_only (injects @ recs @ map_congs' @ same_ctr_simps) ctxt) THEN_MAYBE'
blanchet@58166:     TRY o REPEAT_ALL_NEW (rtac conjI) THEN_ALL_NEW
blanchet@58166:     REPEAT_ALL_NEW (eresolve_tac (conjE :: inj_map_strongs')) THEN_ALL_NEW
blanchet@58172:     (atac ORELSE' use_induction_hypothesis_tac));
blanchet@58160: 
blanchet@58160: fun distinct_ctrs_tac ctxt recs =
blanchet@58166:   HEADGOAL (asm_full_simp_tac (ss_only (recs @ distinct_ctrs_simps) ctxt));
blanchet@58160: 
blanchet@58160: fun mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs' =
blanchet@58160:   let val ks = 1 upto n in
blanchet@58160:     EVERY (maps (fn k => nchotomy_tac nchotomy :: map (fn k' =>
blanchet@58160:       if k = k' then same_ctr_tac ctxt injects recs map_comps' inj_map_strongs'
blanchet@58160:       else distinct_ctrs_tac ctxt recs) ks) ks)
blanchet@58160:   end;
blanchet@58160: 
blanchet@58160: fun mk_encode_injectives_tac ctxt ns induct nchotomys injectss recss map_comps' inj_map_strongs' =
blanchet@58160:   HEADGOAL (rtac induct) THEN
blanchet@58160:   EVERY (map4 (fn n => fn nchotomy => fn injects => fn recs =>
blanchet@58160:       mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs')
blanchet@58160:     ns nchotomys injectss recss);
blanchet@58160: 
blanchet@58160: fun endgame_tac ctxt encode_injectives =
blanchet@58160:   unfold_thms_tac ctxt @{thms inj_on_def ball_UNIV} THEN
blanchet@58160:   ALLGOALS (rtac exI THEN' rtac allI THEN' resolve_tac encode_injectives);
blanchet@58160: 
blanchet@58160: fun encode_sumN n k t =
blanchet@58160:   Balanced_Tree.access {init = t,
blanchet@58160:       left = fn t => @{const sum_encode} $ (@{const Inl (nat, nat)} $ t),
blanchet@58160:       right = fn t => @{const sum_encode} $ (@{const Inr (nat, nat)} $ t)}
blanchet@58160:     n k;
blanchet@58160: 
blanchet@58160: fun encode_tuple [] = @{term "0 :: nat"}
blanchet@58160:   | encode_tuple ts =
blanchet@58160:     Balanced_Tree.make (fn (t, u) => @{const prod_encode} $ (@{const Pair (nat, nat)} $ u $ t)) ts;
blanchet@58160: 
blanchet@58160: fun mk_encode_funs ctxt fpTs ns ctrss0 recs0 =
blanchet@58160:   let
blanchet@58160:     val thy = Proof_Context.theory_of ctxt;
blanchet@58160: 
blanchet@58174:     fun check_countable T =
blanchet@58174:       Sign.of_sort thy (T, countableS) orelse
blanchet@58174:       raise TYPE ("Type is not of sort " ^ Syntax.string_of_sort ctxt countableS, [T], []);
blanchet@58174: 
blanchet@58174:     fun mk_to_nat_checked T =
blanchet@58174:       Const (@{const_name to_nat}, tap check_countable T --> HOLogic.natT);
blanchet@58174: 
blanchet@58160:     val nn = length ns;
blanchet@58221:     val recs as rec1 :: _ = map2 (mk_co_rec thy Least_FP (replicate nn HOLogic.natT)) fpTs recs0;
blanchet@58160:     val arg_Ts = binder_fun_types (fastype_of rec1);
blanchet@58160:     val arg_Tss = Library.unflat ctrss0 arg_Ts;
blanchet@58160: 
blanchet@58160:     fun mk_U (Type (@{type_name prod}, [T1, T2])) =
blanchet@58160:         if member (op =) fpTs T1 then T2 else HOLogic.mk_prodT (mk_U T1, mk_U T2)
blanchet@58160:       | mk_U (Type (s, Ts)) = Type (s, map mk_U Ts)
blanchet@58160:       | mk_U T = T;
blanchet@58160: 
blanchet@58160:     fun mk_nat (j, T) =
blanchet@58160:       if T = HOLogic.natT then
blanchet@58160:         SOME (Bound j)
blanchet@58160:       else if member (op =) fpTs T then
blanchet@58160:         NONE
blanchet@58160:       else if exists_subtype_in fpTs T then
blanchet@58160:         let val U = mk_U T in
blanchet@58174:           SOME (mk_to_nat_checked U $ (build_map ctxt [] (snd_const o fst) (T, U) $ Bound j))
blanchet@58160:         end
blanchet@58160:       else
blanchet@58174:         SOME (mk_to_nat_checked T $ Bound j);
blanchet@58160: 
blanchet@58160:     fun mk_arg n (k, arg_T) =
blanchet@58160:       let
blanchet@58160:         val bound_Ts = rev (binder_types arg_T);
blanchet@58160:         val nats = map_filter mk_nat (tag_list 0 bound_Ts);
blanchet@58160:       in
blanchet@58160:         fold (fn T => fn t => Abs (Name.uu, T, t)) bound_Ts (encode_sumN n k (encode_tuple nats))
blanchet@58160:       end;
blanchet@58160: 
blanchet@58160:     val argss = map2 (map o mk_arg) ns (map (tag_list 1) arg_Tss);
blanchet@58160:   in
blanchet@58160:     map (fn recx => Term.list_comb (recx, flat argss)) recs
blanchet@58160:   end;
blanchet@58160: 
blanchet@58165: fun derive_encode_injectives_thms _ [] = []
blanchet@58165:   | derive_encode_injectives_thms ctxt fpT_names0 =
blanchet@58160:     let
blanchet@58315:       fun not_datatype s = error (quote s ^ " is not a datatype");
blanchet@58315:       fun not_mutually_recursive ss = error (commas ss ^ " are not mutually recursive datatypes");
blanchet@58160: 
blanchet@58160:       fun lfp_sugar_of s =
blanchet@58160:         (case fp_sugar_of ctxt s of
blanchet@58160:           SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
blanchet@58160:         | _ => not_datatype s);
blanchet@58160: 
blanchet@58232:       val fpTs0 as Type (_, var_As) :: _ =
blanchet@58232:         map (#T o lfp_sugar_of o fst o dest_Type) (#Ts (#fp_res (lfp_sugar_of (hd fpT_names0))));
blanchet@58160:       val fpT_names = map (fst o dest_Type) fpTs0;
blanchet@58160: 
blanchet@58160:       val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) ctxt;
blanchet@58160:       val As =
blanchet@58174:         map2 (fn s => fn TVar (_, S) => TFree (s, union (op =) countableS S))
blanchet@58160:           As_names var_As;
blanchet@58160:       val fpTs = map (fn s => Type (s, As)) fpT_names;
blanchet@58160: 
blanchet@58160:       val _ = subset (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
blanchet@58160: 
blanchet@58160:       fun mk_conjunct fpT x encode_fun =
blanchet@58160:         HOLogic.all_const fpT $ Abs (Name.uu, fpT,
blanchet@58160:           HOLogic.mk_imp (HOLogic.mk_eq (encode_fun $ x, encode_fun $ Bound 0),
blanchet@58160:             HOLogic.eq_const fpT $ x $ Bound 0));
blanchet@58160: 
blanchet@58160:       val fp_sugars as {fp_nesting_bnfs, common_co_inducts = induct :: _, ...} :: _ =
blanchet@58160:         map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0;
blanchet@58160:       val ctr_sugars = map #ctr_sugar fp_sugars;
blanchet@58160: 
blanchet@58160:       val ctrss0 = map #ctrs ctr_sugars;
blanchet@58160:       val ns = map length ctrss0;
blanchet@58160:       val recs0 = map #co_rec fp_sugars;
blanchet@58160:       val nchotomys = map #nchotomy ctr_sugars;
blanchet@58160:       val injectss = map #injects ctr_sugars;
blanchet@58160:       val rec_thmss = map #co_rec_thms fp_sugars;
blanchet@58160:       val map_comps' = map (unfold_thms ctxt @{thms comp_def} o map_comp_of_bnf) fp_nesting_bnfs;
blanchet@58160:       val inj_map_strongs' = map (Thm.permute_prems 0 ~1 o inj_map_strong_of_bnf) fp_nesting_bnfs;
blanchet@58160: 
blanchet@58160:       val (xs, names_ctxt) = ctxt |> mk_Frees "x" fpTs;
blanchet@58160: 
blanchet@58160:       val conjuncts = map3 mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0);
blanchet@58170:       val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj conjuncts);
blanchet@58160:     in
blanchet@58296:       Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
blanchet@58160:         mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'
blanchet@58161:           inj_map_strongs')
blanchet@58160:       |> HOLogic.conj_elims
blanchet@58160:       |> Proof_Context.export names_ctxt ctxt
blanchet@58160:       |> map Thm.close_derivation
blanchet@58160:     end;
blanchet@58160: 
blanchet@58165: fun get_countable_goal_type_name (@{const Trueprop} $ (Const (@{const_name Ex}, _)
blanchet@58160:     $ Abs (_, Type (_, [Type (s, _), _]), Const (@{const_name inj_on}, _) $ Bound 0
blanchet@58160:         $ Const (@{const_name top}, _)))) = s
blanchet@58165:   | get_countable_goal_type_name _ = error "Wrong goal format for datatype countability tactic";
blanchet@58160: 
blanchet@58161: fun core_countable_datatype_tac ctxt st =
blanchet@58165:   let val T_names = map get_countable_goal_type_name (Thm.prems_of st) in
blanchet@58165:     endgame_tac ctxt (derive_encode_injectives_thms ctxt T_names) st
blanchet@58165:   end;
blanchet@58160: 
blanchet@58161: fun countable_datatype_tac ctxt =
blanchet@58161:   TRY (Class.intro_classes_tac []) THEN core_countable_datatype_tac ctxt;
blanchet@58160: 
blanchet@58160: end;