For each datatype `t' there is now a theorem `split_t_case' of the form
P(t_case f1 ... fn x) = ((!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1))&
...
(!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn)))
The simplifier now reduces !x. (..x.. & x = t & ..x..) --> P x
to (..t.. & ..t..) --> P t
(and similarly for t=x).
--- a/src/HOL/List.ML Wed Oct 29 16:03:19 1997 +0100
+++ b/src/HOL/List.ML Thu Oct 30 09:45:03 1997 +0100
@@ -48,13 +48,7 @@
(** list_case **)
-goal thy
- "P(list_case a f xs) = ((xs=[] --> P(a)) & \
-\ (!y ys. xs=y#ys --> P(f y ys)))";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
-qed "expand_list_case";
+val expand_list_case = split_list_case;
val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
by (induct_tac "xs" 1);
--- a/src/HOL/NatDef.ML Wed Oct 29 16:03:19 1997 +0100
+++ b/src/HOL/NatDef.ML Thu Oct 30 09:45:03 1997 +0100
@@ -722,7 +722,7 @@
(* add function nat_add_primrec *)
-val (_, nat_add_primrec, _) = Datatype.add_datatype
+val (_, nat_add_primrec, _, _) = Datatype.add_datatype
([], "nat", [("0", [], Mixfix ("0", [], max_pri)), ("Suc", [dtTyp ([],
"nat")], NoSyn)]) (Theory.add_name "Arith" HOL.thy);
(*pretend Arith is part of the basic theory to fool package*)
--- a/src/HOL/Option.ML Wed Oct 29 16:03:19 1997 +0100
+++ b/src/HOL/Option.ML Thu Oct 30 09:45:03 1997 +0100
@@ -6,11 +6,4 @@
Derived rules
*)
-open Option;
-
-goal Option.thy "P(case opt of None => a | Some(x) => b x) = \
-\ ((opt = None --> P a) & (!x. opt = Some x --> P(b x)))";
-by (option.induct_tac "opt" 1);
-by (Simp_tac 1);
-by (Asm_full_simp_tac 1);
-qed "expand_option_case";
+val expand_option_case = split_option_case;
--- a/src/HOL/datatype.ML Wed Oct 29 16:03:19 1997 +0100
+++ b/src/HOL/datatype.ML Thu Oct 30 09:45:03 1997 +0100
@@ -443,6 +443,25 @@
val size_eqns = map size_eqn cons_list;
(* -------------------------------------------------------------------- *)
+(* The split equation *)
+
+ local
+ val fs = map (fn i => "f"^(string_of_int i)) (1 upto num_of_cons);
+
+ fun split1case ((_,name,_,vns,_),fi) =
+ let val svns = " " ^ (space_implode " " vns);
+ val all = if null vns then "" else "!" ^ svns ^ ". "
+ in "("^all^tname^"0 = "^C_exp name vns^" --> P("^fi^svns^"))" end;
+
+ val rhss = map split1case (cons_list ~~ fs);
+ val rhs = space_implode " & " rhss;
+ val lhs = "P(" ^ t_case ^ " " ^ (space_implode " " fs) ^" "^ tname^"0)"
+ in
+ val split_eqn = lhs ^ " = (" ^ rhs ^ ")"
+ end;
+
+(* -------------------------------------------------------------------- *)
+
val consts =
map const_type cons_list
@ (if num_of_cons < dtK then []
@@ -512,7 +531,7 @@
|> Theory.add_arities arities
|> Theory.add_consts consts
|> Theory.add_trrules xrules
- |> Theory.add_axioms rules, add_primrec, size_eqns)
+ |> Theory.add_axioms rules, add_primrec, size_eqns, split_eqn)
end
(*Warn if the (induction) variable occurs Free among the premises, which
--- a/src/HOL/simpdata.ML Wed Oct 29 16:03:19 1997 +0100
+++ b/src/HOL/simpdata.ML Thu Oct 30 09:45:03 1997 +0100
@@ -145,10 +145,22 @@
"(ALL x. P x --> Q) = ((EX x. P x) --> Q)",
"(ALL x. P --> Q x) = (P --> (ALL x. Q x))"];
-(*** Simplification procedure for turning ? x. ... & x = t & ...
- into ? x. x = t & ... & ...
- where the latter can be rewritten via (? x. x = t & P(x)) = P(t)
- ***)
+(*** Simplification procedures for turning
+
+ ? x. ... & x = t & ...
+ into ? x. x = t & ... & ...
+ where the `? x. x = t &' in the latter formula is eliminated
+ by ordinary simplification.
+
+ and ! x. (... & x = t & ...) --> P x
+ into ! x. x = t --> (... & ...) --> P x
+ where the `!x. x=t -->' in the latter formula is eliminated
+ by ordinary simplification.
+
+NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)"
+ "!x. x=t --> P(x)" and "!x. t=x --> P(x)"
+ must be taken care of by ordinary rewrite rules.
+***)
local
@@ -171,25 +183,49 @@
| None => None))))
| extract _ = None;
-fun prove_eq(ceqt) =
+fun prove_ex_eq(ceqt) =
let val tac = rtac eq_reflection 1 THEN rtac iffI 1 THEN
ALLGOALS(EVERY'[etac exE, REPEAT o (etac conjE),
rtac exI, REPEAT o (ares_tac [conjI] ORELSE' etac sym)])
in rule_by_tactic tac (trivial ceqt) end;
-fun rearrange sg _ (F as ex $ Abs(x,T,P)) =
+fun rearrange_ex sg _ (F as ex $ Abs(x,T,P)) =
(case extract P of
None => None
| Some(eq,Q) =>
let val ceqt = cterm_of sg
(Logic.mk_equals(F,ex $ Abs(x,T,HOLogic.conj$eq$Q)))
- in Some(prove_eq ceqt) end)
- | rearrange _ _ _ = None;
+ in Some(prove_ex_eq ceqt) end)
+ | rearrange_ex _ _ _ = None;
+
+val ex_pattern =
+ read_cterm (sign_of HOL.thy) ("? x. P(x) & Q(x)",HOLogic.boolT)
-val pattern = read_cterm (sign_of HOL.thy) ("? x. P(x) & Q(x)",HOLogic.boolT)
+fun prove_all_eq(ceqt) =
+ let fun tac _ = [EVERY1[rtac eq_reflection, rtac iffI,
+ rtac allI, etac allE, rtac impI, rtac impI, etac mp,
+ REPEAT o (etac conjE),
+ REPEAT o (ares_tac [conjI] ORELSE' etac sym),
+ rtac allI, etac allE, rtac impI, REPEAT o (etac conjE),
+ etac impE, atac ORELSE' etac sym, etac mp,
+ REPEAT o (ares_tac [conjI])]]
+ in prove_goalw_cterm [] ceqt tac end;
+
+fun rearrange_all sg _ (F as all $ Abs(x,T,Const("op -->",_)$P$Q)) =
+ (case extract P of
+ None => None
+ | Some(eq,P') =>
+ let val R = HOLogic.imp $ eq $ (HOLogic.imp $ P' $ Q)
+ val ceqt = cterm_of sg (Logic.mk_equals(F,all$Abs(x,T,R)))
+ in Some(prove_all_eq ceqt) end)
+ | rearrange_all _ _ _ = None;
+
+val all_pattern =
+ read_cterm (sign_of HOL.thy) ("! x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
in
-val defEX_regroup = mk_simproc "defined EX" [pattern] rearrange;
+val defEX_regroup = mk_simproc "defined EX" [ex_pattern] rearrange_ex;
+val defALL_regroup = mk_simproc "defined ALL" [all_pattern] rearrange_all;
end;
@@ -386,7 +422,7 @@
de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
not_all, not_ex, cases_simp]
@ ex_simps @ all_simps @ simp_thms)
- addsimprocs [defEX_regroup]
+ addsimprocs [defALL_regroup,defEX_regroup]
addcongs [imp_cong];
qed_goal "if_distrib" HOL.thy
--- a/src/HOL/thy_syntax.ML Wed Oct 29 16:03:19 1997 +0100
+++ b/src/HOL/thy_syntax.ML Thu Oct 30 09:45:03 1997 +0100
@@ -126,9 +126,10 @@
(*generate string for calling add_datatype and build_record*)
fun mk_params ((ts, tname), cons) =
- ("val (thy," ^ tname ^ "_add_primrec," ^ tname ^ "_size_eqns) = Datatype.add_datatype\n"
+ ("val (thy,"^tname^"_add_primrec,size_"^tname^"_eqns,split_"^tname^"_eqn) =\n\
+ \ Datatype.add_datatype\n"
^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
- \val thy = ("^tname^"_add_primrec "^tname^"_size_eqns thy)"
+ \val thy = ("^tname^"_add_primrec size_"^tname^"_eqns thy)"
,
"val _ = deny (" ^ quote tname ^ " mem (Sign.stamp_names_of (sign_of thy)))\n\
\ (\"Datatype \\\""^tname^"\\\" would clash with the theory of the same name!\");\n\
@@ -161,9 +162,19 @@
tname ^ ".distinct;\n\
\val dummy = Addsimps(map (fn (_,eqn) =>\n\
\ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^
- "] eqn (fn _ => [Simp_tac 1]))\n" ^
- tname^"_size_eqns)\n"
+ "] eqn (fn _ => [Simp_tac 1])) size_"^tname^"_eqns);\n\
+ \val split_"^tname^"_case = prove_goal thy split_"^tname^"_eqn\n\
+ \ (fn _ => [#exhaust_tac(snd(hd(!datatypes))) \""^tname^"0\" 1,\n\
+ \ ALLGOALS Asm_simp_tac])"
);
+(*
+The #exhaust_tac(snd(hd(!datatypes))) in the proof of split_"^tname^"_case
+is a hack. Ideally I would just write exhaust_tac, but the latter extracts the
+specific exhaustion tactic from the theory associated with the proof
+state. However, the exhaustion tactic for the current datatype has only just
+been added to !datatypes (a few lines above) but is not yet associated with
+the theory. Hope this can be simplified in the future.
+*)
(*parsers*)
val tvars = type_args >> map (cat "dtVar");