# HG changeset patch # User blanchet # Date 1409730180 -7200 # Node ID deeff89d5b9ec5b6c92a3da0f02d1165c015e512 # Parent e4965b677ba980249d7d4411514d4f85402054a6 added compatibility function diff -r e4965b677ba9 -r deeff89d5b9e src/HOL/Library/Countable.thy --- 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 "\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 "\n. r = nat_to_rat_surj n" by(auto simp:Let_def) + thus "\n. r = nat_to_rat_surj n" by(auto simp: Let_def) qed qed diff -r e4965b677ba9 -r deeff89d5b9e src/HOL/Library/bnf_lfp_countable.ML --- 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;