--- a/src/HOL/Library/Countable.thy Wed Sep 03 00:31:38 2014 +0200
+++ b/src/HOL/Library/Countable.thy Wed Sep 03 09:43:00 2014 +0200
@@ -161,7 +161,7 @@
qed
ML {*
- fun old_countable_tac ctxt =
+ fun old_countable_datatype_tac ctxt =
SUBGOAL (fn (goal, _) =>
let
val ty_name =
@@ -201,10 +201,18 @@
ML_file "bnf_lfp_countable.ML"
+ML {*
+fun countable_datatype_tac ctxt st =
+ HEADGOAL (old_countable_datatype_tac ctxt) st
+ handle ERROR _ => BNF_LFP_Countable.countable_datatype_tac ctxt st;
+
+(* compatibility *)
+fun countable_tac ctxt =
+ SELECT_GOAL (countable_datatype_tac ctxt);
+*}
+
method_setup countable_datatype = {*
- Scan.succeed (fn ctxt =>
- SIMPLE_METHOD (fn st => HEADGOAL (old_countable_tac ctxt) st
- handle ERROR _ => BNF_LFP_Countable.countable_tac ctxt st))
+ Scan.succeed (SIMPLE_METHOD o countable_datatype_tac)
*} "prove countable class instances for datatypes"
@@ -279,10 +287,9 @@
show "\<exists>n. r = nat_to_rat_surj n"
proof (cases r)
fix i j assume [simp]: "r = Fract i j" and "j > 0"
- have "r = (let m = int_encode i; n = int_encode j
- in nat_to_rat_surj(prod_encode (m,n)))"
+ have "r = (let m = int_encode i; n = int_encode j in nat_to_rat_surj (prod_encode (m, n)))"
by (simp add: Let_def nat_to_rat_surj_def)
- thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def)
+ thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp: Let_def)
qed
qed
--- a/src/HOL/Library/bnf_lfp_countable.ML Wed Sep 03 00:31:38 2014 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML Wed Sep 03 09:43:00 2014 +0200
@@ -7,7 +7,7 @@
signature BNF_LFP_COUNTABLE =
sig
- val countable_tac: Proof.context -> tactic
+ val countable_datatype_tac: Proof.context -> tactic
end;
structure BNF_LFP_Countable : BNF_LFP_COUNTABLE =
@@ -30,7 +30,7 @@
dtac meta_spec THEN' meta_spec_mp_tac (n - 1) THEN' dtac meta_mp THEN' atac;
val use_induction_hypothesis_tac =
- DEEPEN (1, 1000000 (* large number *))
+ DEEPEN (1, 64 (* large number *))
(fn depth => meta_spec_mp_tac depth THEN' etac allE THEN' etac impE THEN' atac THEN' atac) 0;
val same_ctr_simps =
@@ -119,7 +119,7 @@
let
fun not_datatype s = error (quote s ^ " is not a new-style datatype");
fun not_mutually_recursive ss =
- error ("{" ^ commas ss ^ "} is not a set of mutually recursive new-style datatypes");
+ error ("{" ^ commas ss ^ "} are not mutually recursive new-style datatypes");
fun lfp_sugar_of s =
(case fp_sugar_of ctxt s of
@@ -162,7 +162,7 @@
in
Goal.prove_sorry ctxt [] [] goal (fn {context = ctxt, prems = _} =>
mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'
- inj_map_strongs')
+ inj_map_strongs')
|> HOLogic.conj_elims
|> Proof_Context.export names_ctxt ctxt
|> map Thm.close_derivation
@@ -171,13 +171,13 @@
fun get_countable_goal_typ (@{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_typ _ = error "Wrong goal format for countable tactic";
+ | get_countable_goal_typ _ = error "Wrong goal format for datatype countability tactic";
-fun core_countable_tac ctxt st =
+fun core_countable_datatype_tac ctxt st =
endgame_tac ctxt (mk_encode_injective_thms ctxt (map get_countable_goal_typ (Thm.prems_of st)))
st;
-fun countable_tac ctxt =
- TRY (Class.intro_classes_tac []) THEN core_countable_tac ctxt;
+fun countable_datatype_tac ctxt =
+ TRY (Class.intro_classes_tac []) THEN core_countable_datatype_tac ctxt;
end;