put all 'bnf_*.ML' files together, irrespective of bootstrapping/dependency constraints
--- a/src/HOL/Library/BNF_Axiomatization.thy Tue Mar 22 08:00:33 2016 +0100
+++ b/src/HOL/Library/BNF_Axiomatization.thy Tue Mar 22 12:39:37 2016 +0100
@@ -13,6 +13,6 @@
"bnf_axiomatization" :: thy_decl
begin
-ML_file "bnf_axiomatization.ML"
+ML_file "../Tools/BNF/bnf_axiomatization.ML"
end
--- a/src/HOL/Library/Countable.thy Tue Mar 22 08:00:33 2016 +0100
+++ b/src/HOL/Library/Countable.thy Tue Mar 22 12:39:37 2016 +0100
@@ -200,7 +200,7 @@
subsection \<open>Automatically proving countability of datatypes\<close>
-ML_file "bnf_lfp_countable.ML"
+ML_file "../Tools/BNF/bnf_lfp_countable.ML"
ML \<open>
fun countable_datatype_tac ctxt st =
--- a/src/HOL/Library/bnf_axiomatization.ML Tue Mar 22 08:00:33 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,128 +0,0 @@
-(* Title: HOL/Library/bnf_axiomatization.ML
- Author: Dmitriy Traytel, TU Muenchen
- Copyright 2013
-
-Axiomatic declaration of bounded natural functors.
-*)
-
-signature BNF_AXIOMATIZATION =
-sig
- val bnf_axiomatization: (string -> bool) -> (binding option * (typ * sort)) list -> binding ->
- mixfix -> binding -> binding -> binding -> typ list -> local_theory ->
- BNF_Def.bnf * local_theory
-end
-
-structure BNF_Axiomatization : BNF_AXIOMATIZATION =
-struct
-
-open BNF_Util
-open BNF_Def
-
-fun prepare_decl prepare_plugins prepare_constraint prepare_typ
- raw_plugins raw_vars b mx user_mapb user_relb user_predb user_witTs lthy =
- let
- val plugins = prepare_plugins lthy raw_plugins;
-
- fun prepare_type_arg (set_opt, (ty, c)) =
- let val s = fst (dest_TFree (prepare_typ lthy ty)) in
- (set_opt, (s, prepare_constraint lthy c))
- end;
- val ((user_setbs, vars), raw_vars') =
- map prepare_type_arg raw_vars
- |> `split_list
- |>> apfst (map_filter I);
- val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars';
-
- fun mk_b name user_b =
- (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b)
- |> Binding.qualify false (Binding.name_of b);
- val (Tname, lthy) = Typedecl.basic_typedecl {final = true} (b, length vars, mx) lthy;
- val (bd_type_Tname, lthy) = lthy
- |> Typedecl.basic_typedecl {final = true} (mk_b "bd_type" Binding.empty, length deads, NoSyn);
- val T = Type (Tname, map TFree vars);
- val bd_type_T = Type (bd_type_Tname, map TFree deads);
- val lives = map TFree (filter_out (member (op =) deads) vars);
- val live = length lives;
- val _ = "Trying to declare a BNF with no live variables" |> null lives ? error;
- val (lives', _) = BNF_Util.mk_TFrees (length lives)
- (fold Variable.declare_typ (map TFree vars) lthy);
- val T' = Term.typ_subst_atomic (lives ~~ lives') T;
- val mapT = map2 (curry op -->) lives lives' ---> T --> T';
- val setTs = map (fn U => T --> HOLogic.mk_setT U) lives;
- val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T);
- val mapb = mk_b mapN user_mapb;
- val bdb = mk_b "bd" Binding.empty;
- val setbs = map2 (fn b => fn i => mk_b (mk_setN i) b) user_setbs
- (if live = 1 then [0] else 1 upto live);
-
- val witTs = map (prepare_typ lthy) user_witTs;
- val nwits = length witTs;
- val witbs = map (fn i => mk_b (mk_witN i) Binding.empty)
- (if nwits = 1 then [0] else 1 upto nwits);
-
- val lthy = Local_Theory.background_theory
- (Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
- map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @
- map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs))
- lthy;
- val Fmap = Const (Local_Theory.full_name lthy mapb, mapT);
- val Fsets = map2 (fn setb => fn setT =>
- Const (Local_Theory.full_name lthy setb, setT)) setbs setTs;
- val Fbd = Const (Local_Theory.full_name lthy bdb, bdT);
- val Fwits = map2 (fn witb => fn witT =>
- Const (Local_Theory.full_name lthy witb, witT)) witbs witTs;
- val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) =
- prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads))
- user_mapb user_relb user_predb user_setbs
- (((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE), NONE)
- lthy;
-
- fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps;
- val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
- val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
-
- val (((_, [raw_thms])), lthy) = Local_Theory.background_theory_result
- (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy;
-
- fun mk_wit_thms set_maps =
- Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
- (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
- |> Thm.close_derivation
- |> Conjunction.elim_balanced (length wit_goals)
- |> map2 (Conjunction.elim_balanced o length) wit_goalss
- |> (map o map) (Thm.forall_elim_vars 0);
- val phi = Local_Theory.target_morphism lthy;
- val thms = unflat all_goalss (Morphism.fact phi raw_thms);
-
- val (bnf, lthy') = after_qed mk_wit_thms thms lthy
- in
- (bnf, register_bnf plugins key bnf lthy')
- end;
-
-val bnf_axiomatization = prepare_decl (K I) (K I) (K I);
-
-fun read_constraint _ NONE = @{sort type}
- | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
-
-val bnf_axiomatization_cmd = prepare_decl Plugin_Name.make_filter read_constraint Syntax.read_typ;
-
-val parse_witTs =
- @{keyword "["} |-- (Parse.name --| @{keyword ":"} -- Scan.repeat Parse.typ
- >> (fn ("wits", Ts) => Ts
- | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --|
- @{keyword "]"} || Scan.succeed [];
-
-val parse_bnf_axiomatization_options =
- Scan.optional (@{keyword "("} |-- Plugin_Name.parse_filter --| @{keyword ")"}) (K (K true));
-
-val parse_bnf_axiomatization =
- parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding --
- parse_witTs -- Parse.opt_mixfix -- parse_map_rel_pred_bindings;
-
-val _ =
- Outer_Syntax.local_theory @{command_keyword bnf_axiomatization} "bnf declaration"
- (parse_bnf_axiomatization >>
- (fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb, predb)) =>
- bnf_axiomatization_cmd plugins bsTs b mx mapb relb predb witTs #> snd));
-
-end;
--- a/src/HOL/Library/bnf_lfp_countable.ML Tue Mar 22 08:00:33 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,195 +0,0 @@
-(* Title: HOL/Library/bnf_lfp_countable.ML
- Author: Jasmin Blanchette, TU Muenchen
- Copyright 2014
-
-Countability tactic for BNF datatypes.
-*)
-
-signature BNF_LFP_COUNTABLE =
-sig
- val derive_encode_injectives_thms: Proof.context -> string list -> thm list
- val countable_datatype_tac: Proof.context -> tactic
-end;
-
-structure BNF_LFP_Countable : BNF_LFP_COUNTABLE =
-struct
-
-open BNF_FP_Rec_Sugar_Util
-open BNF_Def
-open BNF_Util
-open BNF_Tactics
-open BNF_FP_Util
-open BNF_FP_Def_Sugar
-
-val countableS = @{sort countable};
-
-fun nchotomy_tac ctxt nchotomy =
- HEADGOAL (resolve_tac ctxt [nchotomy RS @{thm all_reg[rotated]}] THEN'
- REPEAT_ALL_NEW (resolve_tac ctxt [allI, impI] ORELSE' eresolve_tac ctxt [exE, disjE]));
-
-fun meta_spec_mp_tac ctxt 0 = K all_tac
- | meta_spec_mp_tac ctxt depth =
- dtac ctxt meta_spec THEN' meta_spec_mp_tac ctxt (depth - 1) THEN'
- dtac ctxt meta_mp THEN' assume_tac ctxt;
-
-fun use_induction_hypothesis_tac ctxt =
- DEEPEN (1, 64 (* large number *))
- (fn depth => meta_spec_mp_tac ctxt depth THEN' etac ctxt allE THEN' etac ctxt impE THEN'
- assume_tac ctxt THEN' assume_tac ctxt) 0;
-
-val same_ctr_simps = @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split
- id_apply snd_conv simp_thms};
-val distinct_ctrs_simps = @{thms sum_encode_eq sum.inject sum.distinct simp_thms};
-
-fun same_ctr_tac ctxt injects recs map_congs' inj_map_strongs' =
- HEADGOAL (asm_full_simp_tac
- (ss_only (injects @ recs @ map_congs' @ same_ctr_simps) ctxt) THEN_MAYBE'
- TRY o REPEAT_ALL_NEW (rtac ctxt conjI) THEN_ALL_NEW
- REPEAT_ALL_NEW (eresolve_tac ctxt (conjE :: inj_map_strongs')) THEN_ALL_NEW
- (assume_tac ctxt ORELSE' use_induction_hypothesis_tac ctxt));
-
-fun distinct_ctrs_tac ctxt recs =
- HEADGOAL (asm_full_simp_tac (ss_only (recs @ distinct_ctrs_simps) ctxt));
-
-fun mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs' =
- let val ks = 1 upto n in
- EVERY (maps (fn k => nchotomy_tac ctxt nchotomy :: map (fn k' =>
- if k = k' then same_ctr_tac ctxt injects recs map_comps' inj_map_strongs'
- else distinct_ctrs_tac ctxt recs) ks) ks)
- end;
-
-fun mk_encode_injectives_tac ctxt ns induct nchotomys injectss recss map_comps' inj_map_strongs' =
- HEADGOAL (rtac ctxt induct) THEN
- EVERY (@{map 4} (fn n => fn nchotomy => fn injects => fn recs =>
- mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs')
- ns nchotomys injectss recss);
-
-fun endgame_tac ctxt encode_injectives =
- unfold_thms_tac ctxt @{thms inj_on_def ball_UNIV} THEN
- ALLGOALS (rtac ctxt exI THEN' rtac ctxt allI THEN' resolve_tac ctxt encode_injectives);
-
-fun encode_sumN n k t =
- Balanced_Tree.access {init = t,
- left = fn t => @{const sum_encode} $ (@{const Inl (nat, nat)} $ t),
- right = fn t => @{const sum_encode} $ (@{const Inr (nat, nat)} $ t)}
- n k;
-
-fun encode_tuple [] = @{term "0 :: nat"}
- | encode_tuple ts =
- Balanced_Tree.make (fn (t, u) => @{const prod_encode} $ (@{const Pair (nat, nat)} $ u $ t)) ts;
-
-fun mk_encode_funs ctxt fpTs ns ctrss0 recs0 =
- let
- val thy = Proof_Context.theory_of ctxt;
-
- fun check_countable T =
- Sign.of_sort thy (T, countableS) orelse
- raise TYPE ("Type is not of sort " ^ Syntax.string_of_sort ctxt countableS, [T], []);
-
- fun mk_to_nat_checked T =
- Const (@{const_name to_nat}, tap check_countable T --> HOLogic.natT);
-
- val nn = length ns;
- val recs as rec1 :: _ = map2 (mk_co_rec thy Least_FP (replicate nn HOLogic.natT)) fpTs recs0;
- val arg_Ts = binder_fun_types (fastype_of rec1);
- val arg_Tss = Library.unflat ctrss0 arg_Ts;
-
- fun mk_U (Type (@{type_name prod}, [T1, T2])) =
- if member (op =) fpTs T1 then T2 else HOLogic.mk_prodT (mk_U T1, mk_U T2)
- | mk_U (Type (s, Ts)) = Type (s, map mk_U Ts)
- | mk_U T = T;
-
- fun mk_nat (j, T) =
- if T = HOLogic.natT then
- SOME (Bound j)
- else if member (op =) fpTs T then
- NONE
- else if exists_subtype_in fpTs T then
- let val U = mk_U T in
- SOME (mk_to_nat_checked U $ (build_map ctxt [] (snd_const o fst) (T, U) $ Bound j))
- end
- else
- SOME (mk_to_nat_checked T $ Bound j);
-
- fun mk_arg n (k, arg_T) =
- let
- val bound_Ts = rev (binder_types arg_T);
- val nats = map_filter mk_nat (tag_list 0 bound_Ts);
- in
- fold (fn T => fn t => Abs (Name.uu, T, t)) bound_Ts (encode_sumN n k (encode_tuple nats))
- end;
-
- val argss = map2 (map o mk_arg) ns (map (tag_list 1) arg_Tss);
- in
- map (fn recx => Term.list_comb (recx, flat argss)) recs
- end;
-
-fun derive_encode_injectives_thms _ [] = []
- | derive_encode_injectives_thms ctxt fpT_names0 =
- let
- fun not_datatype s = error (quote s ^ " is not a datatype");
- fun not_mutually_recursive ss = error (commas ss ^ " are not mutually recursive datatypes");
-
- fun lfp_sugar_of s =
- (case fp_sugar_of ctxt s of
- SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
- | _ => not_datatype s);
-
- val fpTs0 as Type (_, var_As) :: _ =
- map (#T o lfp_sugar_of o fst o dest_Type) (#Ts (#fp_res (lfp_sugar_of (hd fpT_names0))));
- val fpT_names = map (fst o dest_Type) fpTs0;
-
- val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) ctxt;
- val As =
- map2 (fn s => fn TVar (_, S) => TFree (s, union (op =) countableS S))
- As_names var_As;
- val fpTs = map (fn s => Type (s, As)) fpT_names;
-
- val _ = subset (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
-
- fun mk_conjunct fpT x encode_fun =
- HOLogic.all_const fpT $ Abs (Name.uu, fpT,
- HOLogic.mk_imp (HOLogic.mk_eq (encode_fun $ x, encode_fun $ Bound 0),
- HOLogic.eq_const fpT $ x $ Bound 0));
-
- val fp_sugars as
- {fp_nesting_bnfs, fp_co_induct_sugar = {common_co_inducts = induct :: _, ...}, ...} :: _ =
- map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0;
- val ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars;
-
- val ctrss0 = map #ctrs ctr_sugars;
- val ns = map length ctrss0;
- val recs0 = map (#co_rec o #fp_co_induct_sugar) fp_sugars;
- val nchotomys = map #nchotomy ctr_sugars;
- val injectss = map #injects ctr_sugars;
- val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars;
- val map_comps' = map (unfold_thms ctxt @{thms comp_def} o map_comp_of_bnf) fp_nesting_bnfs;
- val inj_map_strongs' = map (Thm.permute_prems 0 ~1 o inj_map_strong_of_bnf) fp_nesting_bnfs;
-
- val (xs, names_ctxt) = ctxt |> mk_Frees "x" fpTs;
-
- val conjuncts = @{map 3} mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0);
- val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj conjuncts);
- in
- Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
- mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'
- inj_map_strongs')
- |> HOLogic.conj_elims ctxt
- |> Proof_Context.export names_ctxt ctxt
- |> map Thm.close_derivation
- end;
-
-fun get_countable_goal_type_name (@{const Trueprop} $ (Const (@{const_name Ex}, _)
- $ Abs (_, Type (_, [Type (s, _), _]), Const (@{const_name inj_on}, _) $ Bound 0
- $ Const (@{const_name top}, _)))) = s
- | get_countable_goal_type_name _ = error "Wrong goal format for datatype countability tactic";
-
-fun core_countable_datatype_tac ctxt st =
- let val T_names = map get_countable_goal_type_name (Thm.prems_of st) in
- endgame_tac ctxt (derive_encode_injectives_thms ctxt T_names) st
- end;
-
-fun countable_datatype_tac ctxt =
- TRY (Class.intro_classes_tac ctxt []) THEN core_countable_datatype_tac ctxt;
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/BNF/bnf_axiomatization.ML Tue Mar 22 12:39:37 2016 +0100
@@ -0,0 +1,128 @@
+(* Title: HOL/Tools/BNF/bnf_axiomatization.ML
+ Author: Dmitriy Traytel, TU Muenchen
+ Copyright 2013
+
+Axiomatic declaration of bounded natural functors.
+*)
+
+signature BNF_AXIOMATIZATION =
+sig
+ val bnf_axiomatization: (string -> bool) -> (binding option * (typ * sort)) list -> binding ->
+ mixfix -> binding -> binding -> binding -> typ list -> local_theory ->
+ BNF_Def.bnf * local_theory
+end
+
+structure BNF_Axiomatization : BNF_AXIOMATIZATION =
+struct
+
+open BNF_Util
+open BNF_Def
+
+fun prepare_decl prepare_plugins prepare_constraint prepare_typ
+ raw_plugins raw_vars b mx user_mapb user_relb user_predb user_witTs lthy =
+ let
+ val plugins = prepare_plugins lthy raw_plugins;
+
+ fun prepare_type_arg (set_opt, (ty, c)) =
+ let val s = fst (dest_TFree (prepare_typ lthy ty)) in
+ (set_opt, (s, prepare_constraint lthy c))
+ end;
+ val ((user_setbs, vars), raw_vars') =
+ map prepare_type_arg raw_vars
+ |> `split_list
+ |>> apfst (map_filter I);
+ val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars';
+
+ fun mk_b name user_b =
+ (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b)
+ |> Binding.qualify false (Binding.name_of b);
+ val (Tname, lthy) = Typedecl.basic_typedecl {final = true} (b, length vars, mx) lthy;
+ val (bd_type_Tname, lthy) = lthy
+ |> Typedecl.basic_typedecl {final = true} (mk_b "bd_type" Binding.empty, length deads, NoSyn);
+ val T = Type (Tname, map TFree vars);
+ val bd_type_T = Type (bd_type_Tname, map TFree deads);
+ val lives = map TFree (filter_out (member (op =) deads) vars);
+ val live = length lives;
+ val _ = "Trying to declare a BNF with no live variables" |> null lives ? error;
+ val (lives', _) = BNF_Util.mk_TFrees (length lives)
+ (fold Variable.declare_typ (map TFree vars) lthy);
+ val T' = Term.typ_subst_atomic (lives ~~ lives') T;
+ val mapT = map2 (curry op -->) lives lives' ---> T --> T';
+ val setTs = map (fn U => T --> HOLogic.mk_setT U) lives;
+ val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T);
+ val mapb = mk_b mapN user_mapb;
+ val bdb = mk_b "bd" Binding.empty;
+ val setbs = map2 (fn b => fn i => mk_b (mk_setN i) b) user_setbs
+ (if live = 1 then [0] else 1 upto live);
+
+ val witTs = map (prepare_typ lthy) user_witTs;
+ val nwits = length witTs;
+ val witbs = map (fn i => mk_b (mk_witN i) Binding.empty)
+ (if nwits = 1 then [0] else 1 upto nwits);
+
+ val lthy = Local_Theory.background_theory
+ (Sign.add_consts ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) ::
+ map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @
+ map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs))
+ lthy;
+ val Fmap = Const (Local_Theory.full_name lthy mapb, mapT);
+ val Fsets = map2 (fn setb => fn setT =>
+ Const (Local_Theory.full_name lthy setb, setT)) setbs setTs;
+ val Fbd = Const (Local_Theory.full_name lthy bdb, bdT);
+ val Fwits = map2 (fn witb => fn witT =>
+ Const (Local_Theory.full_name lthy witb, witT)) witbs witTs;
+ val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) =
+ prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads))
+ user_mapb user_relb user_predb user_setbs
+ (((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE), NONE)
+ lthy;
+
+ fun mk_wits_tac ctxt set_maps = TRYALL Goal.conjunction_tac THEN the triv_tac_opt ctxt set_maps;
+ val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
+ val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
+
+ val (((_, [raw_thms])), lthy) = Local_Theory.background_theory_result
+ (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy;
+
+ fun mk_wit_thms set_maps =
+ Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
+ (fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
+ |> Thm.close_derivation
+ |> Conjunction.elim_balanced (length wit_goals)
+ |> map2 (Conjunction.elim_balanced o length) wit_goalss
+ |> (map o map) (Thm.forall_elim_vars 0);
+ val phi = Local_Theory.target_morphism lthy;
+ val thms = unflat all_goalss (Morphism.fact phi raw_thms);
+
+ val (bnf, lthy') = after_qed mk_wit_thms thms lthy
+ in
+ (bnf, register_bnf plugins key bnf lthy')
+ end;
+
+val bnf_axiomatization = prepare_decl (K I) (K I) (K I);
+
+fun read_constraint _ NONE = @{sort type}
+ | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
+
+val bnf_axiomatization_cmd = prepare_decl Plugin_Name.make_filter read_constraint Syntax.read_typ;
+
+val parse_witTs =
+ @{keyword "["} |-- (Parse.name --| @{keyword ":"} -- Scan.repeat Parse.typ
+ >> (fn ("wits", Ts) => Ts
+ | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --|
+ @{keyword "]"} || Scan.succeed [];
+
+val parse_bnf_axiomatization_options =
+ Scan.optional (@{keyword "("} |-- Plugin_Name.parse_filter --| @{keyword ")"}) (K (K true));
+
+val parse_bnf_axiomatization =
+ parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding --
+ parse_witTs -- Parse.opt_mixfix -- parse_map_rel_pred_bindings;
+
+val _ =
+ Outer_Syntax.local_theory @{command_keyword bnf_axiomatization} "bnf declaration"
+ (parse_bnf_axiomatization >>
+ (fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb, predb)) =>
+ bnf_axiomatization_cmd plugins bsTs b mx mapb relb predb witTs #> snd));
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML Tue Mar 22 12:39:37 2016 +0100
@@ -0,0 +1,195 @@
+(* Title: HOL/Tools/BNF/bnf_lfp_countable.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2014
+
+Countability tactic for BNF datatypes.
+*)
+
+signature BNF_LFP_COUNTABLE =
+sig
+ val derive_encode_injectives_thms: Proof.context -> string list -> thm list
+ val countable_datatype_tac: Proof.context -> tactic
+end;
+
+structure BNF_LFP_Countable : BNF_LFP_COUNTABLE =
+struct
+
+open BNF_FP_Rec_Sugar_Util
+open BNF_Def
+open BNF_Util
+open BNF_Tactics
+open BNF_FP_Util
+open BNF_FP_Def_Sugar
+
+val countableS = @{sort countable};
+
+fun nchotomy_tac ctxt nchotomy =
+ HEADGOAL (resolve_tac ctxt [nchotomy RS @{thm all_reg[rotated]}] THEN'
+ REPEAT_ALL_NEW (resolve_tac ctxt [allI, impI] ORELSE' eresolve_tac ctxt [exE, disjE]));
+
+fun meta_spec_mp_tac ctxt 0 = K all_tac
+ | meta_spec_mp_tac ctxt depth =
+ dtac ctxt meta_spec THEN' meta_spec_mp_tac ctxt (depth - 1) THEN'
+ dtac ctxt meta_mp THEN' assume_tac ctxt;
+
+fun use_induction_hypothesis_tac ctxt =
+ DEEPEN (1, 64 (* large number *))
+ (fn depth => meta_spec_mp_tac ctxt depth THEN' etac ctxt allE THEN' etac ctxt impE THEN'
+ assume_tac ctxt THEN' assume_tac ctxt) 0;
+
+val same_ctr_simps = @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split
+ id_apply snd_conv simp_thms};
+val distinct_ctrs_simps = @{thms sum_encode_eq sum.inject sum.distinct simp_thms};
+
+fun same_ctr_tac ctxt injects recs map_congs' inj_map_strongs' =
+ HEADGOAL (asm_full_simp_tac
+ (ss_only (injects @ recs @ map_congs' @ same_ctr_simps) ctxt) THEN_MAYBE'
+ TRY o REPEAT_ALL_NEW (rtac ctxt conjI) THEN_ALL_NEW
+ REPEAT_ALL_NEW (eresolve_tac ctxt (conjE :: inj_map_strongs')) THEN_ALL_NEW
+ (assume_tac ctxt ORELSE' use_induction_hypothesis_tac ctxt));
+
+fun distinct_ctrs_tac ctxt recs =
+ HEADGOAL (asm_full_simp_tac (ss_only (recs @ distinct_ctrs_simps) ctxt));
+
+fun mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs' =
+ let val ks = 1 upto n in
+ EVERY (maps (fn k => nchotomy_tac ctxt nchotomy :: map (fn k' =>
+ if k = k' then same_ctr_tac ctxt injects recs map_comps' inj_map_strongs'
+ else distinct_ctrs_tac ctxt recs) ks) ks)
+ end;
+
+fun mk_encode_injectives_tac ctxt ns induct nchotomys injectss recss map_comps' inj_map_strongs' =
+ HEADGOAL (rtac ctxt induct) THEN
+ EVERY (@{map 4} (fn n => fn nchotomy => fn injects => fn recs =>
+ mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs')
+ ns nchotomys injectss recss);
+
+fun endgame_tac ctxt encode_injectives =
+ unfold_thms_tac ctxt @{thms inj_on_def ball_UNIV} THEN
+ ALLGOALS (rtac ctxt exI THEN' rtac ctxt allI THEN' resolve_tac ctxt encode_injectives);
+
+fun encode_sumN n k t =
+ Balanced_Tree.access {init = t,
+ left = fn t => @{const sum_encode} $ (@{const Inl (nat, nat)} $ t),
+ right = fn t => @{const sum_encode} $ (@{const Inr (nat, nat)} $ t)}
+ n k;
+
+fun encode_tuple [] = @{term "0 :: nat"}
+ | encode_tuple ts =
+ Balanced_Tree.make (fn (t, u) => @{const prod_encode} $ (@{const Pair (nat, nat)} $ u $ t)) ts;
+
+fun mk_encode_funs ctxt fpTs ns ctrss0 recs0 =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+
+ fun check_countable T =
+ Sign.of_sort thy (T, countableS) orelse
+ raise TYPE ("Type is not of sort " ^ Syntax.string_of_sort ctxt countableS, [T], []);
+
+ fun mk_to_nat_checked T =
+ Const (@{const_name to_nat}, tap check_countable T --> HOLogic.natT);
+
+ val nn = length ns;
+ val recs as rec1 :: _ = map2 (mk_co_rec thy Least_FP (replicate nn HOLogic.natT)) fpTs recs0;
+ val arg_Ts = binder_fun_types (fastype_of rec1);
+ val arg_Tss = Library.unflat ctrss0 arg_Ts;
+
+ fun mk_U (Type (@{type_name prod}, [T1, T2])) =
+ if member (op =) fpTs T1 then T2 else HOLogic.mk_prodT (mk_U T1, mk_U T2)
+ | mk_U (Type (s, Ts)) = Type (s, map mk_U Ts)
+ | mk_U T = T;
+
+ fun mk_nat (j, T) =
+ if T = HOLogic.natT then
+ SOME (Bound j)
+ else if member (op =) fpTs T then
+ NONE
+ else if exists_subtype_in fpTs T then
+ let val U = mk_U T in
+ SOME (mk_to_nat_checked U $ (build_map ctxt [] (snd_const o fst) (T, U) $ Bound j))
+ end
+ else
+ SOME (mk_to_nat_checked T $ Bound j);
+
+ fun mk_arg n (k, arg_T) =
+ let
+ val bound_Ts = rev (binder_types arg_T);
+ val nats = map_filter mk_nat (tag_list 0 bound_Ts);
+ in
+ fold (fn T => fn t => Abs (Name.uu, T, t)) bound_Ts (encode_sumN n k (encode_tuple nats))
+ end;
+
+ val argss = map2 (map o mk_arg) ns (map (tag_list 1) arg_Tss);
+ in
+ map (fn recx => Term.list_comb (recx, flat argss)) recs
+ end;
+
+fun derive_encode_injectives_thms _ [] = []
+ | derive_encode_injectives_thms ctxt fpT_names0 =
+ let
+ fun not_datatype s = error (quote s ^ " is not a datatype");
+ fun not_mutually_recursive ss = error (commas ss ^ " are not mutually recursive datatypes");
+
+ fun lfp_sugar_of s =
+ (case fp_sugar_of ctxt s of
+ SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
+ | _ => not_datatype s);
+
+ val fpTs0 as Type (_, var_As) :: _ =
+ map (#T o lfp_sugar_of o fst o dest_Type) (#Ts (#fp_res (lfp_sugar_of (hd fpT_names0))));
+ val fpT_names = map (fst o dest_Type) fpTs0;
+
+ val (As_names, _) = Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As) ctxt;
+ val As =
+ map2 (fn s => fn TVar (_, S) => TFree (s, union (op =) countableS S))
+ As_names var_As;
+ val fpTs = map (fn s => Type (s, As)) fpT_names;
+
+ val _ = subset (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
+
+ fun mk_conjunct fpT x encode_fun =
+ HOLogic.all_const fpT $ Abs (Name.uu, fpT,
+ HOLogic.mk_imp (HOLogic.mk_eq (encode_fun $ x, encode_fun $ Bound 0),
+ HOLogic.eq_const fpT $ x $ Bound 0));
+
+ val fp_sugars as
+ {fp_nesting_bnfs, fp_co_induct_sugar = {common_co_inducts = induct :: _, ...}, ...} :: _ =
+ map (the o fp_sugar_of ctxt o fst o dest_Type) fpTs0;
+ val ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars;
+
+ val ctrss0 = map #ctrs ctr_sugars;
+ val ns = map length ctrss0;
+ val recs0 = map (#co_rec o #fp_co_induct_sugar) fp_sugars;
+ val nchotomys = map #nchotomy ctr_sugars;
+ val injectss = map #injects ctr_sugars;
+ val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars;
+ val map_comps' = map (unfold_thms ctxt @{thms comp_def} o map_comp_of_bnf) fp_nesting_bnfs;
+ val inj_map_strongs' = map (Thm.permute_prems 0 ~1 o inj_map_strong_of_bnf) fp_nesting_bnfs;
+
+ val (xs, names_ctxt) = ctxt |> mk_Frees "x" fpTs;
+
+ val conjuncts = @{map 3} mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0);
+ val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj conjuncts);
+ in
+ Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
+ mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'
+ inj_map_strongs')
+ |> HOLogic.conj_elims ctxt
+ |> Proof_Context.export names_ctxt ctxt
+ |> map Thm.close_derivation
+ end;
+
+fun get_countable_goal_type_name (@{const Trueprop} $ (Const (@{const_name Ex}, _)
+ $ Abs (_, Type (_, [Type (s, _), _]), Const (@{const_name inj_on}, _) $ Bound 0
+ $ Const (@{const_name top}, _)))) = s
+ | get_countable_goal_type_name _ = error "Wrong goal format for datatype countability tactic";
+
+fun core_countable_datatype_tac ctxt st =
+ let val T_names = map get_countable_goal_type_name (Thm.prems_of st) in
+ endgame_tac ctxt (derive_encode_injectives_thms ctxt T_names) st
+ end;
+
+fun countable_datatype_tac ctxt =
+ TRY (Class.intro_classes_tac ctxt []) THEN core_countable_datatype_tac ctxt;
+
+end;