--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Wed Jan 01 21:23:32 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Thu Jan 02 09:50:22 2014 +0100
@@ -336,7 +336,7 @@
if exists (exists_subtype_in seen) mutual_Ts then
(case gen_rhss_in gen_seen rho mutual_Ts of
[] => fresh_tyargs ()
- | gen_tyargss as gen_tyargs :: gen_tyargss_tl =>
+ | gen_tyargs :: gen_tyargss_tl =>
let
val unify_pairs = split_list (maps (curry (op ~~) gen_tyargs) gen_tyargss_tl);
val mgu = Type.raw_unifys unify_pairs Vartab.empty;
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Wed Jan 01 21:23:32 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Jan 02 09:50:22 2014 +0100
@@ -2806,8 +2806,8 @@
(parse_co_datatype_cmd Greatest_FP construct_gfp);
val option_parser = Parse.group (fn () => "option")
- ((Parse.reserved "sequential" >> K Option_Sequential)
- || (Parse.reserved "exhaustive" >> K Option_Exhaustive))
+ ((Parse.reserved "sequential" >> K Sequential_Option)
+ || (Parse.reserved "exhaustive" >> K Exhaustive_Option))
val where_alt_specs_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
(Parse_Spec.spec -- Scan.option (Parse.reserved "of" |-- Parse.const)));
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Wed Jan 01 21:23:32 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 02 09:50:22 2014 +0100
@@ -8,9 +8,8 @@
signature BNF_GFP_REC_SUGAR =
sig
- datatype primcorec_option =
- Option_Sequential |
- Option_Exhaustive
+ datatype primcorec_option = Sequential_Option | Exhaustive_Option
+
val add_primcorecursive_cmd: primcorec_option list ->
(binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
Proof.context -> Proof.state
@@ -48,9 +47,7 @@
fun primcorec_error_eqn str eqn = raise Primcorec_Error (str, [eqn]);
fun primcorec_error_eqns str eqns = raise Primcorec_Error (str, eqns);
-datatype primcorec_option =
- Option_Sequential |
- Option_Exhaustive
+datatype primcorec_option = Sequential_Option | Exhaustive_Option;
datatype corec_call =
Dummy_No_Corec of int |
@@ -852,8 +849,8 @@
[] => ()
| (b, _) :: _ => primcorec_error ("type of " ^ Binding.print b ^ " contains top sort"));
- val seq = member (op =) opts Option_Sequential;
- val exhaustive = member (op =) opts Option_Exhaustive;
+ val seq = member (op =) opts Sequential_Option;
+ val exhaustive = member (op =) opts Exhaustive_Option;
val fun_names = map Binding.name_of bs;
val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts;
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Wed Jan 01 21:23:32 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Thu Jan 02 09:50:22 2014 +0100
@@ -12,6 +12,7 @@
val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
tactic
+ val mk_primcorec_disc_iff_tac: Proof.context -> int -> thm -> thm list -> thm list list -> tactic
val mk_primcorec_exhaust_tac: int -> thm -> tactic
val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list ->
thm list -> int list -> thm list -> thm option -> tactic
@@ -25,6 +26,7 @@
open BNF_Util
open BNF_Tactics
+val atomize_conjL = @{thm atomize_conjL};
val falseEs = @{thms not_TrueE FalseE};
val Let_def = @{thm Let_def};
val neq_eq_eq_contradict = @{thm neq_eq_eq_contradict};
@@ -74,6 +76,15 @@
fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss =
mk_primcorec_prelude ctxt defs disc_corec THEN mk_primcorec_cases_tac ctxt k m exclsss;
+fun mk_primcorec_disc_iff_tac ctxt k exhaust discs disc_excludess =
+ HEADGOAL (rtac iffI THEN'
+ rtac exhaust THEN'
+ EVERY' (map2 (fn disc => fn [] => REPEAT_DETERM o (atac ORELSE' etac conjI)
+ | [disc_exclude] =>
+ dtac disc THEN' (REPEAT_DETERM o atac) THEN' dtac disc_exclude THEN' etac notE THEN' atac)
+ discs disc_excludess) THEN'
+ etac (unfold_thms ctxt [atomize_conjL] (nth discs (k - 1))));
+
fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms map_idents map_comps f_sel k m
exclsss =
mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN
@@ -139,7 +150,7 @@
(ms |> split_last ||> K [n - 1] |> op @,
f_ctrs
|> split_last
- ||> unfold_thms ctxt @{thms atomize_conjL}
+ ||> unfold_thms ctxt [atomize_conjL]
||> (fn thm => [rulify_nchotomy n nchotomy RS thm])
|> op @));
in