src/HOL/Library/bnf_lfp_countable.ML
changeset 62691 9bfcbab7cd99
parent 62690 c4fad0569a24
child 62692 0701f25fac39
     1.1 --- a/src/HOL/Library/bnf_lfp_countable.ML	Tue Mar 22 08:00:33 2016 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,195 +0,0 @@
     1.4 -(*  Title:      HOL/Library/bnf_lfp_countable.ML
     1.5 -    Author:     Jasmin Blanchette, TU Muenchen
     1.6 -    Copyright   2014
     1.7 -
     1.8 -Countability tactic for BNF datatypes.
     1.9 -*)
    1.10 -
    1.11 -signature BNF_LFP_COUNTABLE =
    1.12 -sig
    1.13 -  val derive_encode_injectives_thms: Proof.context -> string list -> thm list
    1.14 -  val countable_datatype_tac: Proof.context -> tactic
    1.15 -end;
    1.16 -
    1.17 -structure BNF_LFP_Countable : BNF_LFP_COUNTABLE =
    1.18 -struct
    1.19 -
    1.20 -open BNF_FP_Rec_Sugar_Util
    1.21 -open BNF_Def
    1.22 -open BNF_Util
    1.23 -open BNF_Tactics
    1.24 -open BNF_FP_Util
    1.25 -open BNF_FP_Def_Sugar
    1.26 -
    1.27 -val countableS = @{sort countable};
    1.28 -
    1.29 -fun nchotomy_tac ctxt nchotomy =
    1.30 -  HEADGOAL (resolve_tac ctxt [nchotomy RS @{thm all_reg[rotated]}] THEN'
    1.31 -    REPEAT_ALL_NEW (resolve_tac ctxt [allI, impI] ORELSE' eresolve_tac ctxt [exE, disjE]));
    1.32 -
    1.33 -fun meta_spec_mp_tac ctxt 0 = K all_tac
    1.34 -  | meta_spec_mp_tac ctxt depth =
    1.35 -    dtac ctxt meta_spec THEN' meta_spec_mp_tac ctxt (depth - 1) THEN'
    1.36 -    dtac ctxt meta_mp THEN' assume_tac ctxt;
    1.37 -
    1.38 -fun use_induction_hypothesis_tac ctxt =
    1.39 -  DEEPEN (1, 64 (* large number *))
    1.40 -    (fn depth => meta_spec_mp_tac ctxt depth THEN' etac ctxt allE THEN' etac ctxt impE THEN'
    1.41 -      assume_tac ctxt THEN' assume_tac ctxt) 0;
    1.42 -
    1.43 -val same_ctr_simps = @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split
    1.44 -  id_apply snd_conv simp_thms};
    1.45 -val distinct_ctrs_simps = @{thms sum_encode_eq sum.inject sum.distinct simp_thms};
    1.46 -
    1.47 -fun same_ctr_tac ctxt injects recs map_congs' inj_map_strongs' =
    1.48 -  HEADGOAL (asm_full_simp_tac
    1.49 -      (ss_only (injects @ recs @ map_congs' @ same_ctr_simps) ctxt) THEN_MAYBE'
    1.50 -    TRY o REPEAT_ALL_NEW (rtac ctxt conjI) THEN_ALL_NEW
    1.51 -    REPEAT_ALL_NEW (eresolve_tac ctxt (conjE :: inj_map_strongs')) THEN_ALL_NEW
    1.52 -    (assume_tac ctxt ORELSE' use_induction_hypothesis_tac ctxt));
    1.53 -
    1.54 -fun distinct_ctrs_tac ctxt recs =
    1.55 -  HEADGOAL (asm_full_simp_tac (ss_only (recs @ distinct_ctrs_simps) ctxt));
    1.56 -
    1.57 -fun mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs' =
    1.58 -  let val ks = 1 upto n in
    1.59 -    EVERY (maps (fn k => nchotomy_tac ctxt nchotomy :: map (fn k' =>
    1.60 -      if k = k' then same_ctr_tac ctxt injects recs map_comps' inj_map_strongs'
    1.61 -      else distinct_ctrs_tac ctxt recs) ks) ks)
    1.62 -  end;
    1.63 -
    1.64 -fun mk_encode_injectives_tac ctxt ns induct nchotomys injectss recss map_comps' inj_map_strongs' =
    1.65 -  HEADGOAL (rtac ctxt induct) THEN
    1.66 -  EVERY (@{map 4} (fn n => fn nchotomy => fn injects => fn recs =>
    1.67 -      mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs')
    1.68 -    ns nchotomys injectss recss);
    1.69 -
    1.70 -fun endgame_tac ctxt encode_injectives =
    1.71 -  unfold_thms_tac ctxt @{thms inj_on_def ball_UNIV} THEN
    1.72 -  ALLGOALS (rtac ctxt exI THEN' rtac ctxt allI THEN' resolve_tac ctxt encode_injectives);
    1.73 -
    1.74 -fun encode_sumN n k t =
    1.75 -  Balanced_Tree.access {init = t,
    1.76 -      left = fn t => @{const sum_encode} $ (@{const Inl (nat, nat)} $ t),
    1.77 -      right = fn t => @{const sum_encode} $ (@{const Inr (nat, nat)} $ t)}
    1.78 -    n k;
    1.79 -
    1.80 -fun encode_tuple [] = @{term "0 :: nat"}
    1.81 -  | encode_tuple ts =
    1.82 -    Balanced_Tree.make (fn (t, u) => @{const prod_encode} $ (@{const Pair (nat, nat)} $ u $ t)) ts;
    1.83 -
    1.84 -fun mk_encode_funs ctxt fpTs ns ctrss0 recs0 =
    1.85 -  let
    1.86 -    val thy = Proof_Context.theory_of ctxt;
    1.87 -
    1.88 -    fun check_countable T =
    1.89 -      Sign.of_sort thy (T, countableS) orelse
    1.90 -      raise TYPE ("Type is not of sort " ^ Syntax.string_of_sort ctxt countableS, [T], []);
    1.91 -
    1.92 -    fun mk_to_nat_checked T =
    1.93 -      Const (@{const_name to_nat}, tap check_countable T --> HOLogic.natT);
    1.94 -
    1.95 -    val nn = length ns;
    1.96 -    val recs as rec1 :: _ = map2 (mk_co_rec thy Least_FP (replicate nn HOLogic.natT)) fpTs recs0;
    1.97 -    val arg_Ts = binder_fun_types (fastype_of rec1);
    1.98 -    val arg_Tss = Library.unflat ctrss0 arg_Ts;
    1.99 -
   1.100 -    fun mk_U (Type (@{type_name prod}, [T1, T2])) =
   1.101 -        if member (op =) fpTs T1 then T2 else HOLogic.mk_prodT (mk_U T1, mk_U T2)
   1.102 -      | mk_U (Type (s, Ts)) = Type (s, map mk_U Ts)
   1.103 -      | mk_U T = T;
   1.104 -
   1.105 -    fun mk_nat (j, T) =
   1.106 -      if T = HOLogic.natT then
   1.107 -        SOME (Bound j)
   1.108 -      else if member (op =) fpTs T then
   1.109 -        NONE
   1.110 -      else if exists_subtype_in fpTs T then
   1.111 -        let val U = mk_U T in
   1.112 -          SOME (mk_to_nat_checked U $ (build_map ctxt [] (snd_const o fst) (T, U) $ Bound j))
   1.113 -        end
   1.114 -      else
   1.115 -        SOME (mk_to_nat_checked T $ Bound j);
   1.116 -
   1.117 -    fun mk_arg n (k, arg_T) =
   1.118 -      let
   1.119 -        val bound_Ts = rev (binder_types arg_T);
   1.120 -        val nats = map_filter mk_nat (tag_list 0 bound_Ts);
   1.121 -      in
   1.122 -        fold (fn T => fn t => Abs (Name.uu, T, t)) bound_Ts (encode_sumN n k (encode_tuple nats))
   1.123 -      end;
   1.124 -
   1.125 -    val argss = map2 (map o mk_arg) ns (map (tag_list 1) arg_Tss);
   1.126 -  in
   1.127 -    map (fn recx => Term.list_comb (recx, flat argss)) recs
   1.128 -  end;
   1.129 -
   1.130 -fun derive_encode_injectives_thms _ [] = []
   1.131 -  | derive_encode_injectives_thms ctxt fpT_names0 =
   1.132 -    let
   1.133 -      fun not_datatype s = error (quote s ^ " is not a datatype");
   1.134 -      fun not_mutually_recursive ss = error (commas ss ^ " are not mutually recursive datatypes");
   1.135 -
   1.136 -      fun lfp_sugar_of s =
   1.137 -        (case fp_sugar_of ctxt s of
   1.138 -          SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
   1.139 -        | _ => not_datatype s);
   1.140 -
   1.141 -      val fpTs0 as Type (_, var_As) :: _ =
   1.142 -        map (#T o lfp_sugar_of o fst o dest_Type) (#Ts (#fp_res (lfp_sugar_of (hd fpT_names0))));
   1.143 -      val fpT_names = map (fst o dest_Type) fpTs0;
   1.144 -
   1.145 -      val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) ctxt;
   1.146 -      val As =
   1.147 -        map2 (fn s => fn TVar (_, S) => TFree (s, union (op =) countableS S))
   1.148 -          As_names var_As;
   1.149 -      val fpTs = map (fn s => Type (s, As)) fpT_names;
   1.150 -
   1.151 -      val _ = subset (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
   1.152 -
   1.153 -      fun mk_conjunct fpT x encode_fun =
   1.154 -        HOLogic.all_const fpT $ Abs (Name.uu, fpT,
   1.155 -          HOLogic.mk_imp (HOLogic.mk_eq (encode_fun $ x, encode_fun $ Bound 0),
   1.156 -            HOLogic.eq_const fpT $ x $ Bound 0));
   1.157 -
   1.158 -      val fp_sugars as
   1.159 -          {fp_nesting_bnfs, fp_co_induct_sugar = {common_co_inducts = induct :: _, ...}, ...} :: _ =
   1.160 -        map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0;
   1.161 -      val ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars;
   1.162 -
   1.163 -      val ctrss0 = map #ctrs ctr_sugars;
   1.164 -      val ns = map length ctrss0;
   1.165 -      val recs0 = map (#co_rec o #fp_co_induct_sugar) fp_sugars;
   1.166 -      val nchotomys = map #nchotomy ctr_sugars;
   1.167 -      val injectss = map #injects ctr_sugars;
   1.168 -      val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars;
   1.169 -      val map_comps' = map (unfold_thms ctxt @{thms comp_def} o map_comp_of_bnf) fp_nesting_bnfs;
   1.170 -      val inj_map_strongs' = map (Thm.permute_prems 0 ~1 o inj_map_strong_of_bnf) fp_nesting_bnfs;
   1.171 -
   1.172 -      val (xs, names_ctxt) = ctxt |> mk_Frees "x" fpTs;
   1.173 -
   1.174 -      val conjuncts = @{map 3} mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0);
   1.175 -      val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj conjuncts);
   1.176 -    in
   1.177 -      Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
   1.178 -        mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'
   1.179 -          inj_map_strongs')
   1.180 -      |> HOLogic.conj_elims ctxt
   1.181 -      |> Proof_Context.export names_ctxt ctxt
   1.182 -      |> map Thm.close_derivation
   1.183 -    end;
   1.184 -
   1.185 -fun get_countable_goal_type_name (@{const Trueprop} $ (Const (@{const_name Ex}, _)
   1.186 -    $ Abs (_, Type (_, [Type (s, _), _]), Const (@{const_name inj_on}, _) $ Bound 0
   1.187 -        $ Const (@{const_name top}, _)))) = s
   1.188 -  | get_countable_goal_type_name _ = error "Wrong goal format for datatype countability tactic";
   1.189 -
   1.190 -fun core_countable_datatype_tac ctxt st =
   1.191 -  let val T_names = map get_countable_goal_type_name (Thm.prems_of st) in
   1.192 -    endgame_tac ctxt (derive_encode_injectives_thms ctxt T_names) st
   1.193 -  end;
   1.194 -
   1.195 -fun countable_datatype_tac ctxt =
   1.196 -  TRY (Class.intro_classes_tac ctxt []) THEN core_countable_datatype_tac ctxt;
   1.197 -
   1.198 -end;