put all 'bnf_*.ML' files together, irrespective of bootstrapping/dependency constraints
authorblanchet
Tue Mar 22 12:39:37 2016 +0100 (2016-03-22)
changeset 626919bfcbab7cd99
parent 62690 c4fad0569a24
child 62692 0701f25fac39
put all 'bnf_*.ML' files together, irrespective of bootstrapping/dependency constraints
src/HOL/Library/BNF_Axiomatization.thy
src/HOL/Library/Countable.thy
src/HOL/Library/bnf_axiomatization.ML
src/HOL/Library/bnf_lfp_countable.ML
src/HOL/Tools/BNF/bnf_axiomatization.ML
src/HOL/Tools/BNF/bnf_lfp_countable.ML
     1.1 --- a/src/HOL/Library/BNF_Axiomatization.thy	Tue Mar 22 08:00:33 2016 +0100
     1.2 +++ b/src/HOL/Library/BNF_Axiomatization.thy	Tue Mar 22 12:39:37 2016 +0100
     1.3 @@ -13,6 +13,6 @@
     1.4    "bnf_axiomatization" :: thy_decl
     1.5  begin
     1.6  
     1.7 -ML_file "bnf_axiomatization.ML"
     1.8 +ML_file "../Tools/BNF/bnf_axiomatization.ML"
     1.9  
    1.10  end
     2.1 --- a/src/HOL/Library/Countable.thy	Tue Mar 22 08:00:33 2016 +0100
     2.2 +++ b/src/HOL/Library/Countable.thy	Tue Mar 22 12:39:37 2016 +0100
     2.3 @@ -200,7 +200,7 @@
     2.4  
     2.5  subsection \<open>Automatically proving countability of datatypes\<close>
     2.6  
     2.7 -ML_file "bnf_lfp_countable.ML"
     2.8 +ML_file "../Tools/BNF/bnf_lfp_countable.ML"
     2.9  
    2.10  ML \<open>
    2.11  fun countable_datatype_tac ctxt st =
     3.1 --- a/src/HOL/Library/bnf_axiomatization.ML	Tue Mar 22 08:00:33 2016 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,128 +0,0 @@
     3.4 -(*  Title:      HOL/Library/bnf_axiomatization.ML
     3.5 -    Author:     Dmitriy Traytel, TU Muenchen
     3.6 -    Copyright   2013
     3.7 -
     3.8 -Axiomatic declaration of bounded natural functors.
     3.9 -*)
    3.10 -
    3.11 -signature BNF_AXIOMATIZATION =
    3.12 -sig
    3.13 -  val bnf_axiomatization: (string -> bool) -> (binding option * (typ * sort)) list -> binding ->
    3.14 -    mixfix -> binding -> binding -> binding -> typ list -> local_theory ->
    3.15 -    BNF_Def.bnf * local_theory
    3.16 -end
    3.17 -
    3.18 -structure BNF_Axiomatization : BNF_AXIOMATIZATION =
    3.19 -struct
    3.20 -
    3.21 -open BNF_Util
    3.22 -open BNF_Def
    3.23 -
    3.24 -fun prepare_decl prepare_plugins prepare_constraint prepare_typ
    3.25 -    raw_plugins raw_vars b mx user_mapb user_relb user_predb user_witTs lthy =
    3.26 -  let
    3.27 -   val plugins = prepare_plugins lthy raw_plugins;
    3.28 -
    3.29 -   fun prepare_type_arg (set_opt, (ty, c)) =
    3.30 -      let val s = fst (dest_TFree (prepare_typ lthy ty)) in
    3.31 -        (set_opt, (s, prepare_constraint lthy c))
    3.32 -      end;
    3.33 -    val ((user_setbs, vars), raw_vars') =
    3.34 -      map prepare_type_arg raw_vars
    3.35 -      |> `split_list
    3.36 -      |>> apfst (map_filter I);
    3.37 -    val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars';
    3.38 -
    3.39 -    fun mk_b name user_b =
    3.40 -      (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b)
    3.41 -      |> Binding.qualify false (Binding.name_of b);
    3.42 -    val (Tname, lthy) = Typedecl.basic_typedecl {final = true} (b, length vars, mx) lthy;
    3.43 -    val (bd_type_Tname, lthy) = lthy
    3.44 -      |> Typedecl.basic_typedecl {final = true} (mk_b "bd_type" Binding.empty, length deads, NoSyn);
    3.45 -    val T = Type (Tname, map TFree vars);
    3.46 -    val bd_type_T = Type (bd_type_Tname, map TFree deads);
    3.47 -    val lives = map TFree (filter_out (member (op =) deads) vars);
    3.48 -    val live = length lives;
    3.49 -    val _ = "Trying to declare a BNF with no live variables" |> null lives ? error;
    3.50 -    val (lives', _) = BNF_Util.mk_TFrees (length lives)
    3.51 -      (fold Variable.declare_typ (map TFree vars) lthy);
    3.52 -    val T' = Term.typ_subst_atomic (lives ~~ lives') T;
    3.53 -    val mapT = map2 (curry op -->) lives lives' ---> T --> T';
    3.54 -    val setTs = map (fn U => T --> HOLogic.mk_setT U) lives;
    3.55 -    val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T);
    3.56 -    val mapb = mk_b mapN user_mapb;
    3.57 -    val bdb = mk_b "bd" Binding.empty;
    3.58 -    val setbs = map2 (fn b => fn i => mk_b (mk_setN i) b) user_setbs
    3.59 -      (if live = 1 then [0] else 1 upto live);
    3.60 -
    3.61 -    val witTs = map (prepare_typ lthy) user_witTs;
    3.62 -    val nwits = length witTs;
    3.63 -    val witbs = map (fn i => mk_b (mk_witN i) Binding.empty)
    3.64 -      (if nwits = 1 then [0] else 1 upto nwits);
    3.65 -
    3.66 -    val lthy = Local_Theory.background_theory
    3.67 -      (Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
    3.68 -        map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @
    3.69 -        map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs))
    3.70 -      lthy;
    3.71 -    val Fmap = Const (Local_Theory.full_name lthy mapb, mapT);
    3.72 -    val Fsets = map2 (fn setb => fn setT =>
    3.73 -      Const (Local_Theory.full_name lthy setb, setT)) setbs setTs;
    3.74 -    val Fbd = Const (Local_Theory.full_name lthy bdb, bdT);
    3.75 -    val Fwits = map2 (fn witb => fn witT =>
    3.76 -      Const (Local_Theory.full_name lthy witb, witT)) witbs witTs;
    3.77 -    val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) =
    3.78 -      prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads))
    3.79 -      user_mapb user_relb user_predb user_setbs
    3.80 -      (((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE), NONE)
    3.81 -      lthy;
    3.82 -
    3.83 -    fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps;
    3.84 -    val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
    3.85 -    val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
    3.86 -
    3.87 -    val (((_, [raw_thms])), lthy) = Local_Theory.background_theory_result
    3.88 -      (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy;
    3.89 -
    3.90 -    fun mk_wit_thms set_maps =
    3.91 -      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
    3.92 -        (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
    3.93 -      |> Thm.close_derivation
    3.94 -      |> Conjunction.elim_balanced (length wit_goals)
    3.95 -      |> map2 (Conjunction.elim_balanced o length) wit_goalss
    3.96 -      |> (map o map) (Thm.forall_elim_vars 0);
    3.97 -    val phi = Local_Theory.target_morphism lthy;
    3.98 -    val thms = unflat all_goalss (Morphism.fact phi raw_thms);
    3.99 -
   3.100 -    val (bnf, lthy') = after_qed mk_wit_thms thms lthy
   3.101 -  in
   3.102 -    (bnf, register_bnf plugins key bnf lthy')
   3.103 -  end;
   3.104 -
   3.105 -val bnf_axiomatization = prepare_decl (K I) (K I) (K I);
   3.106 -
   3.107 -fun read_constraint _ NONE = @{sort type}
   3.108 -  | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
   3.109 -
   3.110 -val bnf_axiomatization_cmd = prepare_decl Plugin_Name.make_filter read_constraint Syntax.read_typ;
   3.111 -
   3.112 -val parse_witTs =
   3.113 -  @{keyword "["} |-- (Parse.name --| @{keyword ":"} -- Scan.repeat Parse.typ
   3.114 -    >> (fn ("wits", Ts) => Ts
   3.115 -         | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --|
   3.116 -  @{keyword "]"} || Scan.succeed [];
   3.117 -
   3.118 -val parse_bnf_axiomatization_options =
   3.119 -  Scan.optional (@{keyword "("} |-- Plugin_Name.parse_filter --| @{keyword ")"}) (K (K true));
   3.120 -
   3.121 -val parse_bnf_axiomatization =
   3.122 -  parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding --
   3.123 -  parse_witTs -- Parse.opt_mixfix -- parse_map_rel_pred_bindings;
   3.124 -
   3.125 -val _ =
   3.126 -  Outer_Syntax.local_theory @{command_keyword bnf_axiomatization} "bnf declaration"
   3.127 -    (parse_bnf_axiomatization >> 
   3.128 -      (fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb, predb)) =>
   3.129 -         bnf_axiomatization_cmd plugins bsTs b mx mapb relb predb witTs #> snd));
   3.130 -
   3.131 -end;
     4.1 --- a/src/HOL/Library/bnf_lfp_countable.ML	Tue Mar 22 08:00:33 2016 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,195 +0,0 @@
     4.4 -(*  Title:      HOL/Library/bnf_lfp_countable.ML
     4.5 -    Author:     Jasmin Blanchette, TU Muenchen
     4.6 -    Copyright   2014
     4.7 -
     4.8 -Countability tactic for BNF datatypes.
     4.9 -*)
    4.10 -
    4.11 -signature BNF_LFP_COUNTABLE =
    4.12 -sig
    4.13 -  val derive_encode_injectives_thms: Proof.context -> string list -> thm list
    4.14 -  val countable_datatype_tac: Proof.context -> tactic
    4.15 -end;
    4.16 -
    4.17 -structure BNF_LFP_Countable : BNF_LFP_COUNTABLE =
    4.18 -struct
    4.19 -
    4.20 -open BNF_FP_Rec_Sugar_Util
    4.21 -open BNF_Def
    4.22 -open BNF_Util
    4.23 -open BNF_Tactics
    4.24 -open BNF_FP_Util
    4.25 -open BNF_FP_Def_Sugar
    4.26 -
    4.27 -val countableS = @{sort countable};
    4.28 -
    4.29 -fun nchotomy_tac ctxt nchotomy =
    4.30 -  HEADGOAL (resolve_tac ctxt [nchotomy RS @{thm all_reg[rotated]}] THEN'
    4.31 -    REPEAT_ALL_NEW (resolve_tac ctxt [allI, impI] ORELSE' eresolve_tac ctxt [exE, disjE]));
    4.32 -
    4.33 -fun meta_spec_mp_tac ctxt 0 = K all_tac
    4.34 -  | meta_spec_mp_tac ctxt depth =
    4.35 -    dtac ctxt meta_spec THEN' meta_spec_mp_tac ctxt (depth - 1) THEN'
    4.36 -    dtac ctxt meta_mp THEN' assume_tac ctxt;
    4.37 -
    4.38 -fun use_induction_hypothesis_tac ctxt =
    4.39 -  DEEPEN (1, 64 (* large number *))
    4.40 -    (fn depth => meta_spec_mp_tac ctxt depth THEN' etac ctxt allE THEN' etac ctxt impE THEN'
    4.41 -      assume_tac ctxt THEN' assume_tac ctxt) 0;
    4.42 -
    4.43 -val same_ctr_simps = @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split
    4.44 -  id_apply snd_conv simp_thms};
    4.45 -val distinct_ctrs_simps = @{thms sum_encode_eq sum.inject sum.distinct simp_thms};
    4.46 -
    4.47 -fun same_ctr_tac ctxt injects recs map_congs' inj_map_strongs' =
    4.48 -  HEADGOAL (asm_full_simp_tac
    4.49 -      (ss_only (injects @ recs @ map_congs' @ same_ctr_simps) ctxt) THEN_MAYBE'
    4.50 -    TRY o REPEAT_ALL_NEW (rtac ctxt conjI) THEN_ALL_NEW
    4.51 -    REPEAT_ALL_NEW (eresolve_tac ctxt (conjE :: inj_map_strongs')) THEN_ALL_NEW
    4.52 -    (assume_tac ctxt ORELSE' use_induction_hypothesis_tac ctxt));
    4.53 -
    4.54 -fun distinct_ctrs_tac ctxt recs =
    4.55 -  HEADGOAL (asm_full_simp_tac (ss_only (recs @ distinct_ctrs_simps) ctxt));
    4.56 -
    4.57 -fun mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs' =
    4.58 -  let val ks = 1 upto n in
    4.59 -    EVERY (maps (fn k => nchotomy_tac ctxt nchotomy :: map (fn k' =>
    4.60 -      if k = k' then same_ctr_tac ctxt injects recs map_comps' inj_map_strongs'
    4.61 -      else distinct_ctrs_tac ctxt recs) ks) ks)
    4.62 -  end;
    4.63 -
    4.64 -fun mk_encode_injectives_tac ctxt ns induct nchotomys injectss recss map_comps' inj_map_strongs' =
    4.65 -  HEADGOAL (rtac ctxt induct) THEN
    4.66 -  EVERY (@{map 4} (fn n => fn nchotomy => fn injects => fn recs =>
    4.67 -      mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs')
    4.68 -    ns nchotomys injectss recss);
    4.69 -
    4.70 -fun endgame_tac ctxt encode_injectives =
    4.71 -  unfold_thms_tac ctxt @{thms inj_on_def ball_UNIV} THEN
    4.72 -  ALLGOALS (rtac ctxt exI THEN' rtac ctxt allI THEN' resolve_tac ctxt encode_injectives);
    4.73 -
    4.74 -fun encode_sumN n k t =
    4.75 -  Balanced_Tree.access {init = t,
    4.76 -      left = fn t => @{const sum_encode} $ (@{const Inl (nat, nat)} $ t),
    4.77 -      right = fn t => @{const sum_encode} $ (@{const Inr (nat, nat)} $ t)}
    4.78 -    n k;
    4.79 -
    4.80 -fun encode_tuple [] = @{term "0 :: nat"}
    4.81 -  | encode_tuple ts =
    4.82 -    Balanced_Tree.make (fn (t, u) => @{const prod_encode} $ (@{const Pair (nat, nat)} $ u $ t)) ts;
    4.83 -
    4.84 -fun mk_encode_funs ctxt fpTs ns ctrss0 recs0 =
    4.85 -  let
    4.86 -    val thy = Proof_Context.theory_of ctxt;
    4.87 -
    4.88 -    fun check_countable T =
    4.89 -      Sign.of_sort thy (T, countableS) orelse
    4.90 -      raise TYPE ("Type is not of sort " ^ Syntax.string_of_sort ctxt countableS, [T], []);
    4.91 -
    4.92 -    fun mk_to_nat_checked T =
    4.93 -      Const (@{const_name to_nat}, tap check_countable T --> HOLogic.natT);
    4.94 -
    4.95 -    val nn = length ns;
    4.96 -    val recs as rec1 :: _ = map2 (mk_co_rec thy Least_FP (replicate nn HOLogic.natT)) fpTs recs0;
    4.97 -    val arg_Ts = binder_fun_types (fastype_of rec1);
    4.98 -    val arg_Tss = Library.unflat ctrss0 arg_Ts;
    4.99 -
   4.100 -    fun mk_U (Type (@{type_name prod}, [T1, T2])) =
   4.101 -        if member (op =) fpTs T1 then T2 else HOLogic.mk_prodT (mk_U T1, mk_U T2)
   4.102 -      | mk_U (Type (s, Ts)) = Type (s, map mk_U Ts)
   4.103 -      | mk_U T = T;
   4.104 -
   4.105 -    fun mk_nat (j, T) =
   4.106 -      if T = HOLogic.natT then
   4.107 -        SOME (Bound j)
   4.108 -      else if member (op =) fpTs T then
   4.109 -        NONE
   4.110 -      else if exists_subtype_in fpTs T then
   4.111 -        let val U = mk_U T in
   4.112 -          SOME (mk_to_nat_checked U $ (build_map ctxt [] (snd_const o fst) (T, U) $ Bound j))
   4.113 -        end
   4.114 -      else
   4.115 -        SOME (mk_to_nat_checked T $ Bound j);
   4.116 -
   4.117 -    fun mk_arg n (k, arg_T) =
   4.118 -      let
   4.119 -        val bound_Ts = rev (binder_types arg_T);
   4.120 -        val nats = map_filter mk_nat (tag_list 0 bound_Ts);
   4.121 -      in
   4.122 -        fold (fn T => fn t => Abs (Name.uu, T, t)) bound_Ts (encode_sumN n k (encode_tuple nats))
   4.123 -      end;
   4.124 -
   4.125 -    val argss = map2 (map o mk_arg) ns (map (tag_list 1) arg_Tss);
   4.126 -  in
   4.127 -    map (fn recx => Term.list_comb (recx, flat argss)) recs
   4.128 -  end;
   4.129 -
   4.130 -fun derive_encode_injectives_thms _ [] = []
   4.131 -  | derive_encode_injectives_thms ctxt fpT_names0 =
   4.132 -    let
   4.133 -      fun not_datatype s = error (quote s ^ " is not a datatype");
   4.134 -      fun not_mutually_recursive ss = error (commas ss ^ " are not mutually recursive datatypes");
   4.135 -
   4.136 -      fun lfp_sugar_of s =
   4.137 -        (case fp_sugar_of ctxt s of
   4.138 -          SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
   4.139 -        | _ => not_datatype s);
   4.140 -
   4.141 -      val fpTs0 as Type (_, var_As) :: _ =
   4.142 -        map (#T o lfp_sugar_of o fst o dest_Type) (#Ts (#fp_res (lfp_sugar_of (hd fpT_names0))));
   4.143 -      val fpT_names = map (fst o dest_Type) fpTs0;
   4.144 -
   4.145 -      val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) ctxt;
   4.146 -      val As =
   4.147 -        map2 (fn s => fn TVar (_, S) => TFree (s, union (op =) countableS S))
   4.148 -          As_names var_As;
   4.149 -      val fpTs = map (fn s => Type (s, As)) fpT_names;
   4.150 -
   4.151 -      val _ = subset (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
   4.152 -
   4.153 -      fun mk_conjunct fpT x encode_fun =
   4.154 -        HOLogic.all_const fpT $ Abs (Name.uu, fpT,
   4.155 -          HOLogic.mk_imp (HOLogic.mk_eq (encode_fun $ x, encode_fun $ Bound 0),
   4.156 -            HOLogic.eq_const fpT $ x $ Bound 0));
   4.157 -
   4.158 -      val fp_sugars as
   4.159 -          {fp_nesting_bnfs, fp_co_induct_sugar = {common_co_inducts = induct :: _, ...}, ...} :: _ =
   4.160 -        map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0;
   4.161 -      val ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars;
   4.162 -
   4.163 -      val ctrss0 = map #ctrs ctr_sugars;
   4.164 -      val ns = map length ctrss0;
   4.165 -      val recs0 = map (#co_rec o #fp_co_induct_sugar) fp_sugars;
   4.166 -      val nchotomys = map #nchotomy ctr_sugars;
   4.167 -      val injectss = map #injects ctr_sugars;
   4.168 -      val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars;
   4.169 -      val map_comps' = map (unfold_thms ctxt @{thms comp_def} o map_comp_of_bnf) fp_nesting_bnfs;
   4.170 -      val inj_map_strongs' = map (Thm.permute_prems 0 ~1 o inj_map_strong_of_bnf) fp_nesting_bnfs;
   4.171 -
   4.172 -      val (xs, names_ctxt) = ctxt |> mk_Frees "x" fpTs;
   4.173 -
   4.174 -      val conjuncts = @{map 3} mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0);
   4.175 -      val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj conjuncts);
   4.176 -    in
   4.177 -      Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
   4.178 -        mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'
   4.179 -          inj_map_strongs')
   4.180 -      |> HOLogic.conj_elims ctxt
   4.181 -      |> Proof_Context.export names_ctxt ctxt
   4.182 -      |> map Thm.close_derivation
   4.183 -    end;
   4.184 -
   4.185 -fun get_countable_goal_type_name (@{const Trueprop} $ (Const (@{const_name Ex}, _)
   4.186 -    $ Abs (_, Type (_, [Type (s, _), _]), Const (@{const_name inj_on}, _) $ Bound 0
   4.187 -        $ Const (@{const_name top}, _)))) = s
   4.188 -  | get_countable_goal_type_name _ = error "Wrong goal format for datatype countability tactic";
   4.189 -
   4.190 -fun core_countable_datatype_tac ctxt st =
   4.191 -  let val T_names = map get_countable_goal_type_name (Thm.prems_of st) in
   4.192 -    endgame_tac ctxt (derive_encode_injectives_thms ctxt T_names) st
   4.193 -  end;
   4.194 -
   4.195 -fun countable_datatype_tac ctxt =
   4.196 -  TRY (Class.intro_classes_tac ctxt []) THEN core_countable_datatype_tac ctxt;
   4.197 -
   4.198 -end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/BNF/bnf_axiomatization.ML	Tue Mar 22 12:39:37 2016 +0100
     5.3 @@ -0,0 +1,128 @@
     5.4 +(*  Title:      HOL/Tools/BNF/bnf_axiomatization.ML
     5.5 +    Author:     Dmitriy Traytel, TU Muenchen
     5.6 +    Copyright   2013
     5.7 +
     5.8 +Axiomatic declaration of bounded natural functors.
     5.9 +*)
    5.10 +
    5.11 +signature BNF_AXIOMATIZATION =
    5.12 +sig
    5.13 +  val bnf_axiomatization: (string -> bool) -> (binding option * (typ * sort)) list -> binding ->
    5.14 +    mixfix -> binding -> binding -> binding -> typ list -> local_theory ->
    5.15 +    BNF_Def.bnf * local_theory
    5.16 +end
    5.17 +
    5.18 +structure BNF_Axiomatization : BNF_AXIOMATIZATION =
    5.19 +struct
    5.20 +
    5.21 +open BNF_Util
    5.22 +open BNF_Def
    5.23 +
    5.24 +fun prepare_decl prepare_plugins prepare_constraint prepare_typ
    5.25 +    raw_plugins raw_vars b mx user_mapb user_relb user_predb user_witTs lthy =
    5.26 +  let
    5.27 +   val plugins = prepare_plugins lthy raw_plugins;
    5.28 +
    5.29 +   fun prepare_type_arg (set_opt, (ty, c)) =
    5.30 +      let val s = fst (dest_TFree (prepare_typ lthy ty)) in
    5.31 +        (set_opt, (s, prepare_constraint lthy c))
    5.32 +      end;
    5.33 +    val ((user_setbs, vars), raw_vars') =
    5.34 +      map prepare_type_arg raw_vars
    5.35 +      |> `split_list
    5.36 +      |>> apfst (map_filter I);
    5.37 +    val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars';
    5.38 +
    5.39 +    fun mk_b name user_b =
    5.40 +      (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b)
    5.41 +      |> Binding.qualify false (Binding.name_of b);
    5.42 +    val (Tname, lthy) = Typedecl.basic_typedecl {final = true} (b, length vars, mx) lthy;
    5.43 +    val (bd_type_Tname, lthy) = lthy
    5.44 +      |> Typedecl.basic_typedecl {final = true} (mk_b "bd_type" Binding.empty, length deads, NoSyn);
    5.45 +    val T = Type (Tname, map TFree vars);
    5.46 +    val bd_type_T = Type (bd_type_Tname, map TFree deads);
    5.47 +    val lives = map TFree (filter_out (member (op =) deads) vars);
    5.48 +    val live = length lives;
    5.49 +    val _ = "Trying to declare a BNF with no live variables" |> null lives ? error;
    5.50 +    val (lives', _) = BNF_Util.mk_TFrees (length lives)
    5.51 +      (fold Variable.declare_typ (map TFree vars) lthy);
    5.52 +    val T' = Term.typ_subst_atomic (lives ~~ lives') T;
    5.53 +    val mapT = map2 (curry op -->) lives lives' ---> T --> T';
    5.54 +    val setTs = map (fn U => T --> HOLogic.mk_setT U) lives;
    5.55 +    val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T);
    5.56 +    val mapb = mk_b mapN user_mapb;
    5.57 +    val bdb = mk_b "bd" Binding.empty;
    5.58 +    val setbs = map2 (fn b => fn i => mk_b (mk_setN i) b) user_setbs
    5.59 +      (if live = 1 then [0] else 1 upto live);
    5.60 +
    5.61 +    val witTs = map (prepare_typ lthy) user_witTs;
    5.62 +    val nwits = length witTs;
    5.63 +    val witbs = map (fn i => mk_b (mk_witN i) Binding.empty)
    5.64 +      (if nwits = 1 then [0] else 1 upto nwits);
    5.65 +
    5.66 +    val lthy = Local_Theory.background_theory
    5.67 +      (Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
    5.68 +        map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @
    5.69 +        map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs))
    5.70 +      lthy;
    5.71 +    val Fmap = Const (Local_Theory.full_name lthy mapb, mapT);
    5.72 +    val Fsets = map2 (fn setb => fn setT =>
    5.73 +      Const (Local_Theory.full_name lthy setb, setT)) setbs setTs;
    5.74 +    val Fbd = Const (Local_Theory.full_name lthy bdb, bdT);
    5.75 +    val Fwits = map2 (fn witb => fn witT =>
    5.76 +      Const (Local_Theory.full_name lthy witb, witT)) witbs witTs;
    5.77 +    val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) =
    5.78 +      prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads))
    5.79 +      user_mapb user_relb user_predb user_setbs
    5.80 +      (((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE), NONE)
    5.81 +      lthy;
    5.82 +
    5.83 +    fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps;
    5.84 +    val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
    5.85 +    val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
    5.86 +
    5.87 +    val (((_, [raw_thms])), lthy) = Local_Theory.background_theory_result
    5.88 +      (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy;
    5.89 +
    5.90 +    fun mk_wit_thms set_maps =
    5.91 +      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
    5.92 +        (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
    5.93 +      |> Thm.close_derivation
    5.94 +      |> Conjunction.elim_balanced (length wit_goals)
    5.95 +      |> map2 (Conjunction.elim_balanced o length) wit_goalss
    5.96 +      |> (map o map) (Thm.forall_elim_vars 0);
    5.97 +    val phi = Local_Theory.target_morphism lthy;
    5.98 +    val thms = unflat all_goalss (Morphism.fact phi raw_thms);
    5.99 +
   5.100 +    val (bnf, lthy') = after_qed mk_wit_thms thms lthy
   5.101 +  in
   5.102 +    (bnf, register_bnf plugins key bnf lthy')
   5.103 +  end;
   5.104 +
   5.105 +val bnf_axiomatization = prepare_decl (K I) (K I) (K I);
   5.106 +
   5.107 +fun read_constraint _ NONE = @{sort type}
   5.108 +  | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
   5.109 +
   5.110 +val bnf_axiomatization_cmd = prepare_decl Plugin_Name.make_filter read_constraint Syntax.read_typ;
   5.111 +
   5.112 +val parse_witTs =
   5.113 +  @{keyword "["} |-- (Parse.name --| @{keyword ":"} -- Scan.repeat Parse.typ
   5.114 +    >> (fn ("wits", Ts) => Ts
   5.115 +         | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --|
   5.116 +  @{keyword "]"} || Scan.succeed [];
   5.117 +
   5.118 +val parse_bnf_axiomatization_options =
   5.119 +  Scan.optional (@{keyword "("} |-- Plugin_Name.parse_filter --| @{keyword ")"}) (K (K true));
   5.120 +
   5.121 +val parse_bnf_axiomatization =
   5.122 +  parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding --
   5.123 +  parse_witTs -- Parse.opt_mixfix -- parse_map_rel_pred_bindings;
   5.124 +
   5.125 +val _ =
   5.126 +  Outer_Syntax.local_theory @{command_keyword bnf_axiomatization} "bnf declaration"
   5.127 +    (parse_bnf_axiomatization >> 
   5.128 +      (fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb, predb)) =>
   5.129 +         bnf_axiomatization_cmd plugins bsTs b mx mapb relb predb witTs #> snd));
   5.130 +
   5.131 +end;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML	Tue Mar 22 12:39:37 2016 +0100
     6.3 @@ -0,0 +1,195 @@
     6.4 +(*  Title:      HOL/Tools/BNF/bnf_lfp_countable.ML
     6.5 +    Author:     Jasmin Blanchette, TU Muenchen
     6.6 +    Copyright   2014
     6.7 +
     6.8 +Countability tactic for BNF datatypes.
     6.9 +*)
    6.10 +
    6.11 +signature BNF_LFP_COUNTABLE =
    6.12 +sig
    6.13 +  val derive_encode_injectives_thms: Proof.context -> string list -> thm list
    6.14 +  val countable_datatype_tac: Proof.context -> tactic
    6.15 +end;
    6.16 +
    6.17 +structure BNF_LFP_Countable : BNF_LFP_COUNTABLE =
    6.18 +struct
    6.19 +
    6.20 +open BNF_FP_Rec_Sugar_Util
    6.21 +open BNF_Def
    6.22 +open BNF_Util
    6.23 +open BNF_Tactics
    6.24 +open BNF_FP_Util
    6.25 +open BNF_FP_Def_Sugar
    6.26 +
    6.27 +val countableS = @{sort countable};
    6.28 +
    6.29 +fun nchotomy_tac ctxt nchotomy =
    6.30 +  HEADGOAL (resolve_tac ctxt [nchotomy RS @{thm all_reg[rotated]}] THEN'
    6.31 +    REPEAT_ALL_NEW (resolve_tac ctxt [allI, impI] ORELSE' eresolve_tac ctxt [exE, disjE]));
    6.32 +
    6.33 +fun meta_spec_mp_tac ctxt 0 = K all_tac
    6.34 +  | meta_spec_mp_tac ctxt depth =
    6.35 +    dtac ctxt meta_spec THEN' meta_spec_mp_tac ctxt (depth - 1) THEN'
    6.36 +    dtac ctxt meta_mp THEN' assume_tac ctxt;
    6.37 +
    6.38 +fun use_induction_hypothesis_tac ctxt =
    6.39 +  DEEPEN (1, 64 (* large number *))
    6.40 +    (fn depth => meta_spec_mp_tac ctxt depth THEN' etac ctxt allE THEN' etac ctxt impE THEN'
    6.41 +      assume_tac ctxt THEN' assume_tac ctxt) 0;
    6.42 +
    6.43 +val same_ctr_simps = @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split
    6.44 +  id_apply snd_conv simp_thms};
    6.45 +val distinct_ctrs_simps = @{thms sum_encode_eq sum.inject sum.distinct simp_thms};
    6.46 +
    6.47 +fun same_ctr_tac ctxt injects recs map_congs' inj_map_strongs' =
    6.48 +  HEADGOAL (asm_full_simp_tac
    6.49 +      (ss_only (injects @ recs @ map_congs' @ same_ctr_simps) ctxt) THEN_MAYBE'
    6.50 +    TRY o REPEAT_ALL_NEW (rtac ctxt conjI) THEN_ALL_NEW
    6.51 +    REPEAT_ALL_NEW (eresolve_tac ctxt (conjE :: inj_map_strongs')) THEN_ALL_NEW
    6.52 +    (assume_tac ctxt ORELSE' use_induction_hypothesis_tac ctxt));
    6.53 +
    6.54 +fun distinct_ctrs_tac ctxt recs =
    6.55 +  HEADGOAL (asm_full_simp_tac (ss_only (recs @ distinct_ctrs_simps) ctxt));
    6.56 +
    6.57 +fun mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs' =
    6.58 +  let val ks = 1 upto n in
    6.59 +    EVERY (maps (fn k => nchotomy_tac ctxt nchotomy :: map (fn k' =>
    6.60 +      if k = k' then same_ctr_tac ctxt injects recs map_comps' inj_map_strongs'
    6.61 +      else distinct_ctrs_tac ctxt recs) ks) ks)
    6.62 +  end;
    6.63 +
    6.64 +fun mk_encode_injectives_tac ctxt ns induct nchotomys injectss recss map_comps' inj_map_strongs' =
    6.65 +  HEADGOAL (rtac ctxt induct) THEN
    6.66 +  EVERY (@{map 4} (fn n => fn nchotomy => fn injects => fn recs =>
    6.67 +      mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs')
    6.68 +    ns nchotomys injectss recss);
    6.69 +
    6.70 +fun endgame_tac ctxt encode_injectives =
    6.71 +  unfold_thms_tac ctxt @{thms inj_on_def ball_UNIV} THEN
    6.72 +  ALLGOALS (rtac ctxt exI THEN' rtac ctxt allI THEN' resolve_tac ctxt encode_injectives);
    6.73 +
    6.74 +fun encode_sumN n k t =
    6.75 +  Balanced_Tree.access {init = t,
    6.76 +      left = fn t => @{const sum_encode} $ (@{const Inl (nat, nat)} $ t),
    6.77 +      right = fn t => @{const sum_encode} $ (@{const Inr (nat, nat)} $ t)}
    6.78 +    n k;
    6.79 +
    6.80 +fun encode_tuple [] = @{term "0 :: nat"}
    6.81 +  | encode_tuple ts =
    6.82 +    Balanced_Tree.make (fn (t, u) => @{const prod_encode} $ (@{const Pair (nat, nat)} $ u $ t)) ts;
    6.83 +
    6.84 +fun mk_encode_funs ctxt fpTs ns ctrss0 recs0 =
    6.85 +  let
    6.86 +    val thy = Proof_Context.theory_of ctxt;
    6.87 +
    6.88 +    fun check_countable T =
    6.89 +      Sign.of_sort thy (T, countableS) orelse
    6.90 +      raise TYPE ("Type is not of sort " ^ Syntax.string_of_sort ctxt countableS, [T], []);
    6.91 +
    6.92 +    fun mk_to_nat_checked T =
    6.93 +      Const (@{const_name to_nat}, tap check_countable T --> HOLogic.natT);
    6.94 +
    6.95 +    val nn = length ns;
    6.96 +    val recs as rec1 :: _ = map2 (mk_co_rec thy Least_FP (replicate nn HOLogic.natT)) fpTs recs0;
    6.97 +    val arg_Ts = binder_fun_types (fastype_of rec1);
    6.98 +    val arg_Tss = Library.unflat ctrss0 arg_Ts;
    6.99 +
   6.100 +    fun mk_U (Type (@{type_name prod}, [T1, T2])) =
   6.101 +        if member (op =) fpTs T1 then T2 else HOLogic.mk_prodT (mk_U T1, mk_U T2)
   6.102 +      | mk_U (Type (s, Ts)) = Type (s, map mk_U Ts)
   6.103 +      | mk_U T = T;
   6.104 +
   6.105 +    fun mk_nat (j, T) =
   6.106 +      if T = HOLogic.natT then
   6.107 +        SOME (Bound j)
   6.108 +      else if member (op =) fpTs T then
   6.109 +        NONE
   6.110 +      else if exists_subtype_in fpTs T then
   6.111 +        let val U = mk_U T in
   6.112 +          SOME (mk_to_nat_checked U $ (build_map ctxt [] (snd_const o fst) (T, U) $ Bound j))
   6.113 +        end
   6.114 +      else
   6.115 +        SOME (mk_to_nat_checked T $ Bound j);
   6.116 +
   6.117 +    fun mk_arg n (k, arg_T) =
   6.118 +      let
   6.119 +        val bound_Ts = rev (binder_types arg_T);
   6.120 +        val nats = map_filter mk_nat (tag_list 0 bound_Ts);
   6.121 +      in
   6.122 +        fold (fn T => fn t => Abs (Name.uu, T, t)) bound_Ts (encode_sumN n k (encode_tuple nats))
   6.123 +      end;
   6.124 +
   6.125 +    val argss = map2 (map o mk_arg) ns (map (tag_list 1) arg_Tss);
   6.126 +  in
   6.127 +    map (fn recx => Term.list_comb (recx, flat argss)) recs
   6.128 +  end;
   6.129 +
   6.130 +fun derive_encode_injectives_thms _ [] = []
   6.131 +  | derive_encode_injectives_thms ctxt fpT_names0 =
   6.132 +    let
   6.133 +      fun not_datatype s = error (quote s ^ " is not a datatype");
   6.134 +      fun not_mutually_recursive ss = error (commas ss ^ " are not mutually recursive datatypes");
   6.135 +
   6.136 +      fun lfp_sugar_of s =
   6.137 +        (case fp_sugar_of ctxt s of
   6.138 +          SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
   6.139 +        | _ => not_datatype s);
   6.140 +
   6.141 +      val fpTs0 as Type (_, var_As) :: _ =
   6.142 +        map (#T o lfp_sugar_of o fst o dest_Type) (#Ts (#fp_res (lfp_sugar_of (hd fpT_names0))));
   6.143 +      val fpT_names = map (fst o dest_Type) fpTs0;
   6.144 +
   6.145 +      val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) ctxt;
   6.146 +      val As =
   6.147 +        map2 (fn s => fn TVar (_, S) => TFree (s, union (op =) countableS S))
   6.148 +          As_names var_As;
   6.149 +      val fpTs = map (fn s => Type (s, As)) fpT_names;
   6.150 +
   6.151 +      val _ = subset (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
   6.152 +
   6.153 +      fun mk_conjunct fpT x encode_fun =
   6.154 +        HOLogic.all_const fpT $ Abs (Name.uu, fpT,
   6.155 +          HOLogic.mk_imp (HOLogic.mk_eq (encode_fun $ x, encode_fun $ Bound 0),
   6.156 +            HOLogic.eq_const fpT $ x $ Bound 0));
   6.157 +
   6.158 +      val fp_sugars as
   6.159 +          {fp_nesting_bnfs, fp_co_induct_sugar = {common_co_inducts = induct :: _, ...}, ...} :: _ =
   6.160 +        map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0;
   6.161 +      val ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars;
   6.162 +
   6.163 +      val ctrss0 = map #ctrs ctr_sugars;
   6.164 +      val ns = map length ctrss0;
   6.165 +      val recs0 = map (#co_rec o #fp_co_induct_sugar) fp_sugars;
   6.166 +      val nchotomys = map #nchotomy ctr_sugars;
   6.167 +      val injectss = map #injects ctr_sugars;
   6.168 +      val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars;
   6.169 +      val map_comps' = map (unfold_thms ctxt @{thms comp_def} o map_comp_of_bnf) fp_nesting_bnfs;
   6.170 +      val inj_map_strongs' = map (Thm.permute_prems 0 ~1 o inj_map_strong_of_bnf) fp_nesting_bnfs;
   6.171 +
   6.172 +      val (xs, names_ctxt) = ctxt |> mk_Frees "x" fpTs;
   6.173 +
   6.174 +      val conjuncts = @{map 3} mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0);
   6.175 +      val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj conjuncts);
   6.176 +    in
   6.177 +      Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
   6.178 +        mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'
   6.179 +          inj_map_strongs')
   6.180 +      |> HOLogic.conj_elims ctxt
   6.181 +      |> Proof_Context.export names_ctxt ctxt
   6.182 +      |> map Thm.close_derivation
   6.183 +    end;
   6.184 +
   6.185 +fun get_countable_goal_type_name (@{const Trueprop} $ (Const (@{const_name Ex}, _)
   6.186 +    $ Abs (_, Type (_, [Type (s, _), _]), Const (@{const_name inj_on}, _) $ Bound 0
   6.187 +        $ Const (@{const_name top}, _)))) = s
   6.188 +  | get_countable_goal_type_name _ = error "Wrong goal format for datatype countability tactic";
   6.189 +
   6.190 +fun core_countable_datatype_tac ctxt st =
   6.191 +  let val T_names = map get_countable_goal_type_name (Thm.prems_of st) in
   6.192 +    endgame_tac ctxt (derive_encode_injectives_thms ctxt T_names) st
   6.193 +  end;
   6.194 +
   6.195 +fun countable_datatype_tac ctxt =
   6.196 +  TRY (Class.intro_classes_tac ctxt []) THEN core_countable_datatype_tac ctxt;
   6.197 +
   6.198 +end;