# HG changeset patch # User nipkow # Date 878201103 -3600 # Node ID 4b1c69d8b767f49051483cd0c4c766c0c1e7d878 # Parent 42cbf6256d6092d1e4205ee392903a66316bb922 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). diff -r 42cbf6256d60 -r 4b1c69d8b767 src/HOL/List.ML --- 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); diff -r 42cbf6256d60 -r 4b1c69d8b767 src/HOL/NatDef.ML --- 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*) diff -r 42cbf6256d60 -r 4b1c69d8b767 src/HOL/Option.ML --- 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; diff -r 42cbf6256d60 -r 4b1c69d8b767 src/HOL/datatype.ML --- 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 diff -r 42cbf6256d60 -r 4b1c69d8b767 src/HOL/simpdata.ML --- 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 diff -r 42cbf6256d60 -r 4b1c69d8b767 src/HOL/thy_syntax.ML --- 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");