Added various thms and tactics.
--- a/src/HOL/Arith.ML Wed Oct 25 09:46:46 1995 +0100
+++ b/src/HOL/Arith.ML Wed Oct 25 09:48:29 1995 +0100
@@ -14,6 +14,16 @@
val [pred_0, pred_Suc] = nat_recs pred_def;
val [add_0,add_Suc] = nat_recs add_def;
val [mult_0,mult_Suc] = nat_recs mult_def;
+Addsimps [pred_0,pred_Suc,add_0,add_Suc,mult_0,mult_Suc];
+
+(** pred **)
+
+val prems = goal Arith.thy "n ~= 0 ==> Suc(pred n) = n";
+by(res_inst_tac [("n","n")] natE 1);
+by(cut_facts_tac prems 1);
+by(ALLGOALS Asm_full_simp_tac);
+qed "Suc_pred";
+Addsimps [Suc_pred];
(** Difference **)
@@ -30,10 +40,7 @@
(fn _ =>
[Simp_tac 1, nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
-(*** Simplification over add, mult, diff ***)
-
-Addsimps [pred_0, pred_Suc, add_0, add_Suc, mult_0, mult_Suc, diff_0,
- diff_0_eq_0, diff_Suc_Suc];
+Addsimps [diff_0, diff_0_eq_0, diff_Suc_Suc];
(**** Inductive properties of the operators ****)
--- a/src/HOL/List.ML Wed Oct 25 09:46:46 1995 +0100
+++ b/src/HOL/List.ML Wed Oct 25 09:48:29 1995 +0100
@@ -125,17 +125,62 @@
by (list.induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed"length_append";
+Addsimps [length_append];
+
+goal List.thy "length (map f l) = length l";
+by (list.induct_tac "l" 1);
+by (ALLGOALS Simp_tac);
+qed "length_map";
+Addsimps [length_map];
goal List.thy "length(rev xs) = length(xs)";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [length_append])));
+by (ALLGOALS Asm_simp_tac);
qed "length_rev";
+Addsimps [length_rev];
(** nth **)
val [nth_0,nth_Suc] = nat_recs nth_def;
store_thm("nth_0",nth_0);
store_thm("nth_Suc",nth_Suc);
+Addsimps [nth_0,nth_Suc];
+
+goal List.thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
+by (list.induct_tac "xs" 1);
+(* case [] *)
+by (Asm_full_simp_tac 1);
+(* case x#xl *)
+by (rtac allI 1);
+by (nat_ind_tac "n" 1);
+by (ALLGOALS Asm_full_simp_tac);
+bind_thm("nth_map", result() RS spec RS mp);
+Addsimps [nth_map];
+
+goal List.thy "!n. n < length xs --> list_all P xs --> P(nth n xs)";
+by (list.induct_tac "xs" 1);
+(* case [] *)
+by (Simp_tac 1);
+(* case x#xl *)
+by (rtac allI 1);
+by (nat_ind_tac "n" 1);
+by (ALLGOALS Asm_full_simp_tac);
+bind_thm("list_all_nth", result() RS spec RS mp RS mp);
+
+goal List.thy "!n. n < length xs --> (nth n xs) mem xs";
+by (list.induct_tac "xs" 1);
+(* case [] *)
+by (Simp_tac 1);
+(* case x#xl *)
+by (rtac allI 1);
+by (nat_ind_tac "n" 1);
+(* case 0 *)
+by (Asm_full_simp_tac 1);
+(* case Suc x *)
+by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+bind_thm ("nth_mem",result() RS spec RS mp);
+Addsimps [nth_mem];
+
(** Additional mapping lemmas **)
@@ -171,5 +216,5 @@
mem_append, mem_filter,
rev_append, rev_rev_ident,
map_ident, map_append, map_compose,
- flat_append, length_append, list_all_True, list_all_conj, nth_0, nth_Suc];
+ flat_append, list_all_True, list_all_conj];
--- a/src/HOL/Makefile Wed Oct 25 09:46:46 1995 +0100
+++ b/src/HOL/Makefile Wed Oct 25 09:48:29 1995 +0100
@@ -119,6 +119,14 @@
Lambda: $(BIN)/HOL $(LAMBDA_FILES)
echo 'exit_use"Lambda/ROOT.ML";quit();' | $(LOGIC)
+MINIML_NAMES = I Maybe MiniML Type W
+
+LAMBDA_FILES = MiniML/ROOT.ML \
+ $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
+
+MiniML: $(BIN)/HOL $(MINIML_FILES)
+ echo 'exit_use"MiniML/ROOT.ML";quit();' | $(LOGIC)
+
##Miscellaneous examples
EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String \
BT Perm
@@ -130,7 +138,7 @@
echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
#Full test. (IOA has been removed temporarily)
-test: $(BIN)/HOL IMP Integ Subst Lambda ex
+test: $(BIN)/HOL IMP Integ Subst Lambda MiniML ex
echo 'Test examples ran successfully' > test
.PRECIOUS: $(BIN)/Pure $(BIN)/HOL
--- a/src/HOL/Nat.ML Wed Oct 25 09:46:46 1995 +0100
+++ b/src/HOL/Nat.ML Wed Oct 25 09:48:29 1995 +0100
@@ -97,6 +97,8 @@
bind_thm ("Zero_not_Suc", (Suc_not_Zero RS not_sym));
+Addsimps [Suc_not_Zero,Zero_not_Suc];
+
bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE));
val Zero_neq_Suc = sym RS Suc_neq_Zero;
@@ -118,7 +120,7 @@
goal Nat.thy "n ~= Suc(n)";
by (nat_ind_tac "n" 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsimps [Zero_not_Suc,Suc_Suc_eq])));
+by (ALLGOALS(asm_simp_tac (!simpset addsimps [Suc_Suc_eq])));
qed "n_not_Suc_n";
val Suc_n_not_n = n_not_Suc_n RS not_sym;
@@ -203,6 +205,7 @@
goalw Nat.thy [less_def] "n < Suc(n)";
by (rtac (pred_natI RS r_into_trancl) 1);
qed "lessI";
+Addsimps [lessI];
(* i(j ==> i(Suc(j) *)
val less_SucI = lessI RSN (2, less_trans);
@@ -213,6 +216,7 @@
by (etac less_trans 1);
by (rtac lessI 1);
qed "zero_less_Suc";
+Addsimps [zero_less_Suc];
(** Elimination properties **)
@@ -251,6 +255,7 @@
by (etac Zero_neq_Suc 1);
by (etac Zero_neq_Suc 1);
qed "not_less0";
+Addsimps [not_less0];
(* n<0 ==> R *)
bind_thm ("less_zeroE", (not_less0 RS notE));
@@ -269,6 +274,12 @@
addEs [less_trans, less_SucE]) 1);
qed "less_Suc_eq";
+val prems = goal Nat.thy "m<n ==> n ~= 0";
+by(res_inst_tac [("n","n")] natE 1);
+by(cut_facts_tac prems 1);
+by(ALLGOALS Asm_full_simp_tac);
+qed "gr_implies_not0";
+Addsimps [gr_implies_not0];
(** Inductive (?) properties **)
@@ -311,10 +322,18 @@
goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]);
qed "Suc_less_eq";
+Addsimps [Suc_less_eq];
goal Nat.thy "~(Suc(n) < n)";
by(fast_tac (HOL_cs addEs [Suc_lessD RS less_anti_refl]) 1);
qed "not_Suc_n_less_n";
+Addsimps [not_Suc_n_less_n];
+
+goal Nat.thy "!!i. i<j ==> j<k --> Suc i < k";
+by(nat_ind_tac "k" 1);
+by(ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
+by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
+bind_thm("less_trans_Suc",result() RS mp);
(*"Less than" is a linear ordering*)
goal Nat.thy "m<n | m=n | n<(m::nat)";
@@ -328,8 +347,7 @@
(*Can be used with less_Suc_eq to get n=m | n<m *)
goal Nat.thy "(~ m < n) = (n < Suc(m))";
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by(ALLGOALS(asm_simp_tac (!simpset addsimps
- [not_less0,zero_less_Suc,Suc_less_eq])));
+by(ALLGOALS Asm_simp_tac);
qed "not_less_eq";
(*Complete induction, aka course-of-values induction*)
@@ -346,9 +364,18 @@
by (rtac not_less0 1);
qed "le0";
-Addsimps [not_less0, less_not_refl, zero_less_Suc, lessI,
- Suc_less_eq, less_Suc_eq, le0, not_Suc_n_less_n,
- Suc_not_Zero, Zero_not_Suc, Suc_Suc_eq,
+goalw Nat.thy [le_def] "~ Suc n <= n";
+by(Simp_tac 1);
+qed "Suc_n_not_le_n";
+
+goalw Nat.thy [le_def] "(i <= 0) = (i = 0)";
+by(nat_ind_tac "i" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "le_0";
+
+Addsimps [less_not_refl,
+ less_Suc_eq, le0, le_0,
+ Suc_Suc_eq, Suc_n_not_le_n,
n_not_Suc_n, Suc_n_not_n,
nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
--- a/src/HOL/Prod.ML Wed Oct 25 09:46:46 1995 +0100
+++ b/src/HOL/Prod.ML Wed Oct 25 09:48:29 1995 +0100
@@ -53,12 +53,40 @@
by (REPEAT (eresolve_tac [prem,exE] 1));
qed "PairE";
+(* replace parameters of product type by individual component parameters *)
+local
+fun is_pair (_,Type("*",_)) = true
+ | is_pair _ = false;
+
+fun find_pair_param t =
+ let val params = Logic.strip_params t
+ in if exists is_pair params
+ then let val params = rev(rename_wrt_term t params)
+ (*as they are printed*)
+ in apsome fst (find_first is_pair params) end
+ else None
+ end;
+
+in
+
+val split_all_tac = REPEAT o SUBGOAL (fn (t,_) =>
+ case find_pair_param t of
+ None => no_tac
+ | Some x => EVERY[res_inst_tac[("p",x)] PairE 1,
+ REPEAT(hyp_subst_tac 1), prune_params_tac]);
+
+end;
+
+goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
+by(fast_tac (HOL_cs addbefore split_all_tac 1) 1);
+qed "split_paired_All";
+
goalw Prod.thy [split_def] "split c (a,b) = c a b";
by (sstac [fst_conv, snd_conv] 1);
by (rtac refl 1);
qed "split";
-Addsimps [fst_conv, snd_conv, split, Pair_eq];
+Addsimps [fst_conv, snd_conv, split_paired_All, split, Pair_eq];
goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
by (res_inst_tac[("p","s")] PairE 1);
--- a/src/HOL/ROOT.ML Wed Oct 25 09:46:46 1995 +0100
+++ b/src/HOL/ROOT.ML Wed Oct 25 09:48:29 1995 +0100
@@ -11,7 +11,6 @@
writeln banner;
print_depth 1;
-set eta_contract;
(* Add user sections *)
use "../Pure/section_utils.ML";
--- a/src/HOL/Trancl.ML Wed Oct 25 09:46:46 1995 +0100
+++ b/src/HOL/Trancl.ML Wed Oct 25 09:48:29 1995 +0100
@@ -31,9 +31,9 @@
qed "rtrancl_into_rtrancl";
(*rtrancl of r contains r*)
-val [prem] = goal Trancl.thy "[| (a,b) : r |] ==> (a,b) : r^*";
-by (rtac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
-by (rtac prem 1);
+goal Trancl.thy "!!p. p : r ==> p : r^*";
+by(split_all_tac 1);
+by (etac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
qed "r_into_rtrancl";
(*monotonicity of rtrancl*)
@@ -161,7 +161,24 @@
by(fast_tac (HOL_cs addEs [rtrancl_trans]) 1);
be r_into_rtrancl 1;
qed "rtrancl_idemp";
+Addsimps [rtrancl_idemp];
+goal Trancl.thy "!!R. [| R <= S; S <= R^* |] ==> S^* = R^*";
+bd rtrancl_mono 1;
+bd rtrancl_mono 1;
+by(Asm_full_simp_tac 1);
+by(fast_tac eq_cs 1);
+qed "rtrancl_subset";
+
+goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
+by(best_tac (set_cs addIs [rtrancl_subset,r_into_rtrancl,
+ rtrancl_mono RS subsetD]) 1);
+qed "trancl_Un_trancl";
+
+goal Trancl.thy "(R^=)^* = R^*";
+by(fast_tac (rel_cs addIs [rtrancl_refl,rtrancl_subset,r_into_rtrancl]) 1);
+qed "rtrancl_reflcl";
+Addsimps [rtrancl_reflcl];
goal Trancl.thy "!!r. (x,y) : (converse r)^* ==> (x,y) : converse(r^*)";
br converseI 1;
@@ -198,4 +215,5 @@
by (fast_tac (rel_cs addSDs [trancl_subset_Sigma_lemma]) 1);
qed "trancl_subset_Sigma";
+(* Don't add r_into_rtrancl: it messes up the proofs in Lambda *)
val trancl_cs = rel_cs addIs [rtrancl_refl];
--- a/src/HOL/Trancl.thy Wed Oct 25 09:46:46 1995 +0100
+++ b/src/HOL/Trancl.thy Wed Oct 25 09:48:29 1995 +0100
@@ -5,14 +5,20 @@
Relfexive and Transitive closure of a relation
-rtrancl is refl&transitive closure; trancl is transitive closure
+rtrancl is refl&transitive closure;
+trancl is transitive closure
+reflcl is reflexive closure
*)
Trancl = Lfp + Relation +
consts
rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [100] 100)
trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [100] 100)
+syntax
+ reflcl :: "('a*'a)set => ('a*'a)set" ("(_^=)" [100] 100)
defs
-rtrancl_def "r^* == lfp(%s. id Un (r O s))"
-trancl_def "r^+ == r O rtrancl(r)"
+ rtrancl_def "r^* == lfp(%s. id Un (r O s))"
+ trancl_def "r^+ == r O rtrancl(r)"
+translations
+ "r^=" == "r Un id"
end