--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 04 13:06:28 2012 +0900
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 05 13:44:03 2012 +0200
@@ -99,9 +99,14 @@
|> mk_TFrees N
||> the_single o fst o mk_TFrees 1;
- fun freeze_rec (T as Type (s, Ts')) =
- (case find_index (curry (op =) T) Ts of
- ~1 => Type (s, map freeze_rec Ts')
+ fun is_same_rec (T as Type (s, Us)) (Type (s', Us')) =
+ s = s' andalso (Us = Us' orelse error ("Illegal occurrence of recursive type " ^
+ quote (Syntax.string_of_typ fake_lthy T)))
+ | is_same_rec _ _ = false
+
+ fun freeze_rec (T as Type (s, Us)) =
+ (case find_index (is_same_rec T) Ts of
+ ~1 => Type (s, map freeze_rec Us)
| i => nth Bs i)
| freeze_rec T = T;
@@ -210,11 +215,17 @@
fun sugar_lfp lthy =
let
(*###
- val iter_Tss = map ( ) ctr_Tss
+ val fld_iter = @{term True}; (*###*)
+
+ val iter_Tss = map (fn Ts => Ts) (*###*) ctr_Tss;
val iter_Ts = map (fn Ts => Ts ---> C) iter_Tss;
val iter_fs = map2 (fn Free (s, _) => fn T => Free (s, T)) fs iter_Ts
+ val iter_rhs =
+ fold_rev Term.lambda fs (fld_iter $ mk_sum_caseN (uncurry_fs fs xss) $ (unf $ v));
+
+
val uncurried_fs =
map2 (fn f => fn xs =>
HOLogic.tupled_lambda (HOLogic.mk_tuple xs) (Term.list_comb (f, xs))) fs xss;
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Tue Sep 04 13:06:28 2012 +0900
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Wed Sep 05 13:44:03 2012 +0200
@@ -30,8 +30,9 @@
fun mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf sumEN' =
Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN
Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN
- EVERY' (map2 (fn k => fn m => select_prem_tac n (REPEAT_DETERM_N m o dtac @{thm meta_spec} THEN'
- etac @{thm meta_mp}) k THEN' atac) (1 upto n) ms) 1;
+ EVERY' (map2 (fn k => fn m =>
+ select_prem_tac k (REPEAT_DETERM_N m o dtac @{thm meta_spec} THEN' rotate_tac ~1 THEN'
+ etac @{thm meta_mp}) k THEN' atac) (1 upto n) ms) 1;
fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
(rtac iffI THEN'
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 04 13:06:28 2012 +0900
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 05 13:44:03 2012 +0200
@@ -51,6 +51,7 @@
fun mk_half_pairss ys = mk_half_pairss' [[]] ys;
+(* TODO: provide a way to have a different default value, e.g. "tl Nil = Nil" *)
fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T);
fun eta_expand_case_arg xs f_xs = fold_rev Term.lambda xs f_xs;
@@ -98,10 +99,10 @@
val raw_disc_binders' = pad_list no_binder n raw_disc_binders;
- fun can_rely_on_disc i =
- not (Binding.eq_name (nth raw_disc_binders' i, no_binder)) orelse nth ms i = 0;
+ fun can_rely_on_disc k =
+ not (Binding.eq_name (nth raw_disc_binders' (k - 1), no_binder)) orelse nth ms (k - 1) = 0;
fun can_omit_disc_binder k m =
- n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (2 - k))
+ n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k))
val fallback_disc_binder = Binding.name o prefix is_N o Long_Name.base_name o name_of_ctr;
@@ -173,12 +174,14 @@
fun disc_spec b exist_xs_v_eq_ctr = mk_Trueprop_eq (disc_free b $ v, exist_xs_v_eq_ctr);
- fun alternate_disc_lhs i =
+ fun alternate_disc_lhs k =
HOLogic.mk_not
- (case nth disc_binders i of NONE => nth exist_xs_v_eq_ctrs i | SOME b => disc_free b $ v);
+ (case nth disc_binders (k - 1) of
+ NONE => nth exist_xs_v_eq_ctrs (k - 1)
+ | SOME b => disc_free b $ v);
fun alternate_disc k =
- if n = 2 then Term.lambda v (alternate_disc_lhs (2 - k)) else error "Cannot use \"*\" here"
+ if n = 2 then Term.lambda v (alternate_disc_lhs (3 - k)) else error "Cannot use \"*\" here"
fun sel_spec b x xs k =
let val T' = fastype_of x in
@@ -311,11 +314,11 @@
fun mk_alternate_disc_def k =
let
val goal =
- mk_Trueprop_eq (Morphism.term phi (alternate_disc_lhs (2 - k)),
+ mk_Trueprop_eq (Morphism.term phi (alternate_disc_lhs (3 - k)),
nth exist_xs_v_eq_ctrs (k - 1));
in
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_alternate_disc_def_tac ctxt (nth disc_defs (2 - k)) (nth distinct_thms (2 - k))
+ mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k)) (nth distinct_thms (2 - k))
exhaust_thm')
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
@@ -421,7 +424,7 @@
val goal = mk_Trueprop_eq (caseB_fs $ v, mk_rhs discs fs selss);
in
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_case_eq_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss)
+ mk_case_eq_tac ctxt n exhaust_thm' case_thms disc_thmss' sel_thmss)
|> singleton (Proof_Context.export names_lthy lthy)
end;
--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Tue Sep 04 13:06:28 2012 +0900
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Wed Sep 05 13:44:03 2012 +0200
@@ -7,9 +7,10 @@
signature BNF_WRAP_TACTICS =
sig
- val mk_alternate_disc_def_tac: Proof.context -> thm -> thm -> thm -> tactic
+ val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
val mk_case_cong_tac: thm -> thm list -> tactic
- val mk_case_eq_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic
+ val mk_case_eq_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list ->
+ tactic
val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
val mk_half_disc_exclude_tac: int -> thm -> thm -> tactic
@@ -29,8 +30,10 @@
fun triangle _ [] = []
| triangle k (xs :: xss) = take k xs :: triangle (k + 1) xss
-fun mk_if_P_or_not_P thm =
- thm RS @{thm if_not_P} handle THM _ => thm RS @{thm if_P}
+fun mk_case_if_P_or_not_Ps n k thms =
+ let val (negs, pos) = split_last thms in
+ map (fn thm => thm RS @{thm if_not_P}) negs @ (if k = n then [] else [pos RS @{thm if_P}])
+ end;
fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms
@@ -41,10 +44,11 @@
fun mk_unique_disc_def_tac m exhaust' =
EVERY' [rtac iffI, rtac exhaust', REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1;
-fun mk_alternate_disc_def_tac ctxt other_disc_def distinct exhaust' =
- EVERY' [subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, hyp_subst_tac,
+fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct exhaust' =
+ EVERY' ([subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, hyp_subst_tac,
SELECT_GOAL (Local_Defs.unfold_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI, rtac distinct,
- rtac exhaust', etac notE, atac, REPEAT_DETERM o rtac exI, atac] 1;
+ rtac exhaust'] @
+ (([etac notE, atac], [REPEAT_DETERM o rtac exI, atac]) |> k = 1 ? swap |> op @)) 1;
fun mk_half_disc_exclude_tac m discD disc'_thm =
(dtac discD THEN'
@@ -70,13 +74,12 @@
SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN'
rtac refl)) 1;
-fun mk_case_eq_tac ctxt exhaust' case_thms disc_thmss' sel_thmss =
+fun mk_case_eq_tac ctxt n exhaust' case_thms disc_thmss' sel_thmss =
(rtac exhaust' THEN'
- EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => EVERY' [
- hyp_subst_tac THEN'
- SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)) THEN'
- rtac case_thm]) case_thms
- (map (map mk_if_P_or_not_P) (triangle 1 (map (fst o split_last) disc_thmss'))) sel_thmss)) 1;
+ EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms =>
+ EVERY' [hyp_subst_tac, SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)),
+ rtac case_thm])
+ case_thms (map2 (mk_case_if_P_or_not_Ps n) (1 upto n) (triangle 1 disc_thmss')) sel_thmss)) 1;
fun mk_case_cong_tac exhaust' case_thms =
(rtac exhaust' THEN'