--- a/src/HOL/Codatatype/BNF_Library.thy Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Library.thy Tue Sep 04 15:51:32 2012 +0200
@@ -17,6 +17,19 @@
lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
by (erule iffI) (erule contrapos_pn)
+lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()" by simp
+
+lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" by auto
+
+lemma False_imp_eq: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
+by presburger
+
+lemma case_unit: "(case u of () => f) = f"
+by (cases u) (hypsubst, rule unit.cases)
+
+lemma All_point_1: "(\<And>z. z = b \<Longrightarrow> phi z) \<equiv> Trueprop (phi b)"
+by presburger
+
lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
by blast
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 04 15:51:32 2012 +0200
@@ -166,13 +166,21 @@
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
mk_fld_iff_unf_tac ctxt (map (SOME o certifyT lthy) [unf_T, T]) (certify lthy fld)
(certify lthy unf) fld_unf unf_fld)
+ |> Thm.close_derivation
end;
+ val sumEN_thm = mk_sumEN n;
+ val sumEN_thm' =
+ let val cTs = map (SOME o certifyT lthy) prod_Ts in
+ Local_Defs.unfold lthy @{thms all_unit_eq} (Drule.instantiate' cTs [] sumEN_thm)
+ end;
+
+ fun exhaust_tac {context = ctxt, ...} =
+ mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf_thm sumEN_thm';
+
(* ### *)
fun cheat_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
- val exhaust_tac = cheat_tac;
-
val inject_tacss = map (fn 0 => [] | _ => [cheat_tac]) ms;
val half_distinct_tacss = map (map (K cheat_tac)) (mk_half_pairss ks);
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Tue Sep 04 15:51:32 2012 +0200
@@ -7,6 +7,7 @@
signature BNF_FP_SUGAR_TACTICS =
sig
+ val mk_exhaust_tac: Proof.context -> int -> int list -> thm list -> thm -> thm -> tactic
val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
-> tactic
end;
@@ -14,8 +15,17 @@
structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
struct
+open BNF_Tactics
open BNF_Util
+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;
+
fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
(rtac iffI THEN'
EVERY' (map3 (fn cTs => fn cx => fn th =>
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Tue Sep 04 15:51:32 2012 +0200
@@ -85,6 +85,8 @@
val mk_Field: term -> term
val mk_union: term * term -> term
+ val mk_sumEN: int -> thm
+
val mk_tactics: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
@@ -210,6 +212,15 @@
if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th;
in split limit 1 th end;
+local
+ fun mk_sumEN' 1 = @{thm obj_sum_step}
+ | mk_sumEN' n = mk_sumEN' (n - 1) RSN (2, @{thm obj_sum_step});
+in
+ fun mk_sumEN 1 = @{thm obj_sum_base}
+ | mk_sumEN 2 = @{thm sumE}
+ | mk_sumEN n = (mk_sumEN' (n - 2) RSN (2, @{thm obj_sumE})) OF replicate n (impI RS allI);
+end;
+
fun mk_tactics mid mcomp mcong snat bdco bdinf sbd inbd wpull =
[mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull];
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 04 15:51:32 2012 +0200
@@ -9,8 +9,8 @@
signature BNF_GFP =
sig
- val bnf_gfp: binding list -> typ list list -> BNF_Def.BNF list -> Proof.context ->
- (term list * term list * thm list * thm list) * Proof.context
+ val bnf_gfp: binding list -> typ list list -> BNF_Def.BNF list -> local_theory ->
+ (term list * term list * thm list * thm list) * local_theory
end;
structure BNF_GFP : BNF_GFP =
--- a/src/HOL/Codatatype/Tools/bnf_gfp_util.ML Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_util.ML Tue Sep 04 15:51:32 2012 +0200
@@ -40,7 +40,6 @@
val mk_specN: int -> thm -> thm
val mk_sum_casesN: int -> int -> thm
- val mk_sumEN: int -> thm
val mk_InN_Field: int -> int -> thm
val mk_InN_inject: int -> int -> thm
@@ -218,15 +217,6 @@
| mk_sum_casesN 2 2 = @{thm sum.cases(2)}
| mk_sum_casesN n m = trans OF [@{thm sum_case_step(2)}, mk_sum_casesN (n - 1) (m - 1)];
-local
- fun mk_sumEN' 1 = @{thm obj_sum_step}
- | mk_sumEN' n = mk_sumEN' (n - 1) RSN (2, @{thm obj_sum_step});
-in
- fun mk_sumEN 1 = @{thm obj_sum_base}
- | mk_sumEN 2 = @{thm sumE}
- | mk_sumEN n = (mk_sumEN' (n - 2) RSN (2, @{thm obj_sumE})) OF replicate n (impI RS allI);
-end;
-
fun mk_rec_simps n rec_thm defs = map (fn i =>
map (fn def => def RS rec_thm RS mk_nthI n i RS fun_cong) defs) (1 upto n);
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Tue Sep 04 15:51:32 2012 +0200
@@ -8,8 +8,8 @@
signature BNF_LFP =
sig
- val bnf_lfp: binding list -> typ list list -> BNF_Def.BNF list -> Proof.context ->
- (term list * term list * thm list * thm list) * Proof.context
+ val bnf_lfp: binding list -> typ list list -> BNF_Def.BNF list -> local_theory ->
+ (term list * term list * thm list * thm list) * local_theory
end;
structure BNF_LFP : BNF_LFP =
--- a/src/HOL/Codatatype/Tools/bnf_tactics.ML Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML Tue Sep 04 15:51:32 2012 +0200
@@ -10,6 +10,7 @@
sig
val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
val fo_rtac: thm -> Proof.context -> int -> tactic
+ val subst_asm_tac: Proof.context -> thm list -> int -> tactic
val subst_tac: Proof.context -> thm list -> int -> tactic
val substs_tac: Proof.context -> thm list -> int -> tactic
@@ -70,6 +71,7 @@
end);
(*unlike "unfold_tac", succeeds when the RHS contains schematic variables not in the LHS*)
+fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt [0];
fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt [0];
fun substs_tac ctxt = REPEAT_DETERM oo subst_tac ctxt;
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 04 14:21:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 04 15:51:32 2012 +0200
@@ -303,6 +303,7 @@
mk_not_other_disc_def_tac ctxt (nth disc_defs (2 - k)) (nth distinct_thms (2 - k))
exhaust_thm')
|> singleton (Proof_Context.export names_lthy lthy)
+ |> Thm.close_derivation
end;
val has_not_other_disc_def =