--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Aug 12 15:25:16 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Aug 12 15:25:17 2013 +0200
@@ -39,7 +39,7 @@
val name_of_disc: term -> string
val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
- (((bool * bool) * term list) * term) *
+ (((bool * bool) * term list) * binding) *
(binding list * (binding list list * (binding * term) list list)) -> local_theory ->
ctr_sugar * local_theory
val parse_wrap_free_constructors_options: (bool * bool) parser
@@ -177,8 +177,8 @@
fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
-fun prepare_wrap_free_constructors prep_term ((((no_dests, rep_compat), raw_ctrs), raw_case),
- (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
+fun prepare_wrap_free_constructors prep_term ((((no_dests, rep_compat), raw_ctrs),
+ raw_case_binding), (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
let
(* TODO: sanity checks on arguments *)
@@ -188,13 +188,10 @@
val _ = if n > 0 then () else error "No constructors specified";
val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
- val case0 = prep_term no_defs_lthy raw_case;
val sel_defaultss =
pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss);
- val case0T = fastype_of case0;
- val Type (dataT_name, As0) =
- domain_type (snd (strip_typeN (num_binder_types case0T - 1) case0T));
+ val Type (dataT_name, As0) = body_type (fastype_of (hd ctrs0));
val data_b = Binding.qualified_name dataT_name;
val data_b_name = Binding.name_of data_b;
@@ -256,15 +253,15 @@
else
sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms;
- val casex = mk_case As B case0;
val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
- val (((((((xss, xss'), yss), fs), gs), [u', v']), (p, p')), names_lthy) = no_defs_lthy |>
+ val ((((((((xss, xss'), yss), fs), gs), [u', v']), [w]), (p, p')), names_lthy) = no_defs_lthy |>
mk_Freess' "x" ctr_Tss
||>> mk_Freess "y" ctr_Tss
||>> mk_Frees "f" case_Ts
||>> mk_Frees "g" case_Ts
||>> (apfst (map (rpair dataT)) oo Variable.variant_fixes) [data_b_name, data_b_name ^ "'"]
+ ||>> mk_Frees "z" [B]
||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
val u = Free u';
@@ -277,16 +274,43 @@
val xfs = map2 (curry Term.list_comb) fs xss;
val xgs = map2 (curry Term.list_comb) gs xss;
+ (* TODO: Eta-expension is for compatibility with the old datatype package (but it also provides
+ nicer names). Consider removing. *)
+ val eta_fs = map2 eta_expand_arg xss xfs;
+ val eta_gs = map2 eta_expand_arg xss xgs;
+
+ val case_binding =
+ qualify false
+ (if Binding.is_empty raw_case_binding orelse
+ Binding.eq_name (raw_case_binding, standard_binding) then
+ Binding.suffix_name ("_" ^ caseN) data_b
+ else
+ raw_case_binding);
+
+ fun mk_case_disj xctr xf xs =
+ list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr), HOLogic.mk_eq (w, xf)));
+
+ val case_rhs =
+ fold_rev (fold_rev Term.lambda) [fs, [u]]
+ (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $
+ Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss)));
+
+ val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy
+ |> Local_Theory.define ((case_binding, NoSyn), ((Thm.def_binding case_binding, []), case_rhs))
+ ||> `Local_Theory.restore;
+
+ val phi = Proof_Context.export_morphism lthy lthy';
+
+ val case_def = Morphism.thm phi raw_case_def;
+
+ val case0 = Morphism.term phi raw_case;
+ val casex = mk_case As B case0;
+
val fcase = Term.list_comb (casex, fs);
val ufcase = fcase $ u;
val vfcase = fcase $ v;
- (* TODO: Eta-expension is for compatibility with the old datatype package (but it also provides
- nicer names). Consider removing. *)
- val eta_fs = map2 eta_expand_arg xss xfs;
- val eta_gs = map2 eta_expand_arg xss xgs;
-
val eta_fcase = Term.list_comb (casex, eta_fs);
val eta_gcase = Term.list_comb (casex, eta_gs);
@@ -312,7 +336,7 @@
val (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs,
sel_defss, lthy') =
if no_dests then
- (true, [], [], [], [], [], [], [], [], [], no_defs_lthy)
+ (true, [], [], [], [], [], [], [], [], [], lthy)
else
let
fun disc_free b = Free (Binding.name_of b, mk_pred1T dataT);
@@ -328,7 +352,7 @@
NONE =>
(case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T)
- | SOME t => t |> Type.constraint (Ts ---> T) |> Syntax.check_term no_defs_lthy)
+ | SOME t => t |> Type.constraint (Ts ---> T) |> Syntax.check_term lthy)
| SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
fun sel_spec b proto_sels =
@@ -337,14 +361,14 @@
(case duplicates (op =) (map fst proto_sels) of
k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^
" for constructor " ^
- quote (Syntax.string_of_term no_defs_lthy (nth ctrs (k - 1))))
+ quote (Syntax.string_of_term lthy (nth ctrs (k - 1))))
| [] => ())
val T =
(case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of
[T] => T
| T :: T' :: _ => error ("Inconsistent range type for selector " ^
- quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
- " vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T')));
+ quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ lthy T) ^ " vs. "
+ ^ quote (Syntax.string_of_typ lthy T')));
in
mk_Trueprop_eq (Free (Binding.name_of b, dataT --> T) $ u,
Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T) $ u)
@@ -368,7 +392,7 @@
fun unflat_selss xs = unflat_lookup Binding.eq_name sel_bindings xs sel_bindingss;
val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
- no_defs_lthy
+ lthy
|> apfst split_list o fold_map3 (fn k => fn exist_xs_u_eq_ctr => fn b =>
if Binding.is_empty b then
if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
@@ -432,16 +456,11 @@
map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs)))
end;
- val cases_goal =
- map3 (fn xs => fn xctr => fn xf =>
- fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xss xctrs xfs;
-
- val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss @ [cases_goal];
+ val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss;
fun after_qed thmss lthy =
let
- val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) =
- (hd thmss, apsnd (chop (n * n)) (chop n (tl thmss)));
+ val ([exhaust_thm], (inject_thmss, half_distinct_thmss)) = (hd thmss, chop n (tl thmss));
val inject_thms = flat inject_thmss;
@@ -470,6 +489,19 @@
|> Thm.close_derivation
end;
+ val case_thms =
+ let
+ val goals =
+ map3 (fn xctr => fn xf => fn xs =>
+ fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xctrs xfs xss;
+ in
+ map4 (fn k => fn goal => fn injects => fn distinctss =>
+ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_case_tac ctxt n k case_def injects distinctss)
+ |> Thm.close_derivation)
+ ks goals inject_thmss distinct_thmsss
+ end;
+
val (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
disc_exhaust_thms, collapse_thms, expand_thms, case_conv_thms) =
if no_dests then
@@ -767,7 +799,7 @@
"wrap an existing freely generated type's constructors"
((parse_wrap_free_constructors_options -- (@{keyword "["} |-- Parse.list Parse.term --|
@{keyword "]"}) --
- Parse.term -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
+ parse_binding -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
>> wrap_free_constructors_cmd);
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Mon Aug 12 15:25:16 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Mon Aug 12 15:25:17 2013 +0200
@@ -8,6 +8,7 @@
signature BNF_CTR_SUGAR_TACTICS =
sig
val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
+ val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic
val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic
val mk_case_conv_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list ->
tactic
@@ -108,10 +109,14 @@
fun mk_case_distinct_ctrs_tac ctxt distincts =
REPEAT_DETERM o etac exE THEN' etac conjE THEN' full_simp_tac (ss_only distincts ctxt);
-fun mk_case_tac ctxt n k def injects distinctss =
- let val ks = 1 upto n in
- HEADGOAL (rtac (def RS trans) THEN' rtac @{thm the_equality} THEN' rtac (mk_disjIN n k) THEN'
- REPEAT_DETERM o rtac exI THEN' rtac conjI THEN' rtac refl THEN' rtac refl THEN'
+fun mk_case_tac ctxt n k case_def injects distinctss =
+ let
+ val case_def' = mk_unabs_def (n + 1) (case_def RS meta_eq_to_obj_eq);
+ val ks = 1 upto n;
+ in
+ HEADGOAL (rtac (case_def' RS trans) THEN' rtac @{thm the_equality} THEN'
+ rtac (mk_disjIN n k) THEN' REPEAT_DETERM o rtac exI THEN' rtac conjI THEN' rtac refl THEN'
+ rtac refl THEN'
EVERY' (map2 (fn k' => fn distincts =>
(if k' < n then etac disjE else K all_tac) THEN'
(if k' = k then mk_case_same_ctr_tac ctxt injects
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Aug 12 15:25:16 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Aug 12 15:25:17 2013 +0200
@@ -65,10 +65,9 @@
val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list ->
string * term list * term list list * ((term list list * term list list list)
* (typ list * typ list list)) list ->
- thm list -> thm list -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list ->
- typ list -> typ list -> int list list -> int list list -> int list -> thm list list ->
- BNF_Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> (thm list -> thm list) ->
- local_theory ->
+ thm list -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list -> typ list ->
+ int list list -> int list list -> int list -> thm list list -> BNF_Ctr_Sugar.ctr_sugar list ->
+ term list list -> thm list list -> (thm list -> thm list) -> local_theory ->
((thm list * thm) list * Args.src list)
* (thm list list * thm list list * Args.src list)
* (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
@@ -201,7 +200,6 @@
p :: flat_corec_predss_getterss qss fss @ flat_corec_preds_predsss_gettersss ps qsss fsss;
fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));
-fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs;
fun mk_uncurried2_fun f xss =
mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat_rec_arg_args xss);
@@ -689,8 +687,8 @@
fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss,
coiters_args_types as [((pgss, crgsss), _), ((phss, cshsss), _)])
- dtor_coinducts dtor_ctors dtor_coiter_thmss nesting_bnfs nested_bnfs fpTs Cs As kss mss ns
- ctr_defss ctr_sugars coiterss coiter_defss export_args lthy =
+ dtor_coinducts dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs As kss mss ns ctr_defss
+ ctr_sugars coiterss coiter_defss export_args lthy =
let
val coiterss' = transpose coiterss;
val coiter_defss' = transpose coiter_defss;
@@ -703,8 +701,6 @@
val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nesting_bnfs;
val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
- val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
- val nested_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nested_bnfs;
val fp_b_names = map base_name_of_typ fpTs;
@@ -839,7 +835,7 @@
let val T = fastype_of cqf in
if exists_subtype_in Cs T then
let val U = mk_U maybe_mk_sumT T in
- build_map lthy (indexify snd fpTs (fn kk => fn TU =>
+ build_map lthy (indexify snd fpTs (fn kk => fn _ =>
maybe_tack (nth cs kk, nth us kk) (nth fcoiters kk))) (T, U) $ cqf
end
else
@@ -853,20 +849,6 @@
val unfold_goalss = map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss';
val corec_goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
- fun mk_map_if_distrib bnf =
- let
- val mapx = map_of_bnf bnf;
- val live = live_of_bnf bnf;
- val ((Ts, T), U) = strip_typeN (live + 1) (fastype_of mapx) |>> split_last;
- val fs = Variable.variant_frees lthy [mapx] (map (pair "f") Ts);
- val t = Term.list_comb (mapx, map (Var o apfst (rpair 0)) fs);
- in
- Drule.instantiate' (map (SOME o certifyT lthy) [U, T]) [SOME (certify lthy t)]
- @{thm if_distrib}
- end;
-
- val nested_map_if_distribs = map mk_map_if_distrib nested_bnfs;
-
val unfold_tacss =
map3 (map oo mk_coiter_tac unfold_defs nesting_map_ids'')
(map un_fold_of dtor_coiter_thmss) pre_map_defs ctr_defss;
@@ -1139,7 +1121,7 @@
val ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy') =
mk_co_iters_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy;
- fun define_ctrs_case_for_type ((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
+ fun define_ctrs_dtrs_for_type (((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor),
xtor_co_iters), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), ctr_bindings),
ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
@@ -1149,12 +1131,10 @@
val dtorT = domain_type (fastype_of ctor);
val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss;
val ctr_sum_prod_T = mk_sumTN_balanced ctr_prod_Ts;
- val case_Ts = map (fn Ts => Ts ---> C) ctr_Tss;
- val (((((w, fs), xss), yss), u'), names_lthy) =
+ val ((((w, xss), yss), u'), names_lthy) =
no_defs_lthy
|> yield_singleton (mk_Frees "w") dtorT
- ||>> mk_Frees "f" case_Ts
||>> mk_Freess "x" ctr_Tss
||>> mk_Freess "y" (map (map B_ify) ctr_Tss)
||>> yield_singleton Variable.variant_fixes fp_b_name;
@@ -1168,16 +1148,10 @@
map3 (fn k => fn xs => fn tuple_x => fold_rev Term.lambda xs (ctor $
mk_InN_balanced ctr_sum_prod_T n tuple_x k)) ks xss tuple_xs;
- val case_binding = qualify false fp_b_name (Binding.suffix_name ("_" ^ caseN) fp_b);
-
- val case_rhs =
- fold_rev Term.lambda (fs @ [u])
- (mk_sum_caseN_balanced (map2 mk_uncurried_fun fs xss) $ (dtor $ u));
-
- val ((raw_case :: raw_ctrs, raw_case_def :: raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
+ val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
|> apfst split_list o fold_map3 (fn b => fn mx => fn rhs =>
Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd)
- (case_binding :: ctr_bindings) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss)
+ ctr_bindings ctr_mixfixes ctr_rhss
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy lthy';
@@ -1185,11 +1159,8 @@
val ctr_defs = map (Morphism.thm phi) raw_ctr_defs;
val ctr_defs' =
map2 (fn m => fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) ms ctr_defs;
- val case_def = Morphism.thm phi raw_case_def;
val ctrs0 = map (Morphism.term phi) raw_ctrs;
- val casex0 = Morphism.term phi raw_case;
-
val ctrs = map (mk_ctr As) ctrs0;
fun wrap_ctrs lthy =
@@ -1226,15 +1197,11 @@
map (map (fn (def, def') => fn {context = ctxt, ...} =>
mk_half_distinct_tac ctxt ctor_inject [def, def'])) (mk_half_pairss (`I ctr_defs));
- val case_tacs =
- map3 (fn k => fn m => fn ctr_def => fn {context = ctxt, ...} =>
- mk_case_tac ctxt n k m case_def ctr_def dtor_ctor) ks ms ctr_defs;
-
- val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
+ val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss;
val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss
in
- wrap_free_constructors tacss (((wrap_opts, ctrs0), casex0), (disc_bindings,
+ wrap_free_constructors tacss (((wrap_opts, ctrs0), standard_binding), (disc_bindings,
(sel_bindingss, sel_defaultss))) lthy
end;
@@ -1391,9 +1358,8 @@
(disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs),
(sel_unfold_thmss, sel_corec_thmss, sel_coiter_attrs)) =
derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_inducts
- dtor_ctors xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs As kss mss ns ctr_defss
- ctr_sugars coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy)
- lthy;
+ dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs As kss mss ns ctr_defss ctr_sugars
+ coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy) lthy;
val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
@@ -1440,7 +1406,7 @@
end;
val lthy'' = lthy'
- |> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~
+ |> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~
xtor_co_iterss ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~
pre_set_defss ~~ pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~
kss ~~ mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Mon Aug 12 15:25:16 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Mon Aug 12 15:25:17 2013 +0200
@@ -11,7 +11,6 @@
val sum_prod_thms_set: thm list
val sum_prod_thms_rel: thm list
- val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
thm list -> thm list -> thm list list -> thm list list list -> thm list list list -> tactic
val mk_coiter_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic
@@ -70,12 +69,6 @@
val inst_as_projs_tac = PRIMITIVE oo inst_as_projs;
-fun mk_case_tac ctxt n k m case_def ctr_def dtor_ctor =
- unfold_thms_tac ctxt [case_def, ctr_def, dtor_ctor] THEN
- HEADGOAL (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN'
- REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN'
- rtac refl);
-
fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' =
unfold_thms_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN HEADGOAL (rtac sumEN') THEN
unfold_thms_tac ctxt @{thms split_paired_all} THEN