Added various thms and tactics.
authornipkow
Wed Oct 25 09:48:29 1995 +0100 (1995-10-25)
changeset 130142782316d510
parent 1300 c7a8f374339b
child 1302 ddfdcc9ce667
Added various thms and tactics.
src/HOL/Arith.ML
src/HOL/List.ML
src/HOL/Makefile
src/HOL/Nat.ML
src/HOL/Prod.ML
src/HOL/ROOT.ML
src/HOL/Trancl.ML
src/HOL/Trancl.thy
     1.1 --- a/src/HOL/Arith.ML	Wed Oct 25 09:46:46 1995 +0100
     1.2 +++ b/src/HOL/Arith.ML	Wed Oct 25 09:48:29 1995 +0100
     1.3 @@ -14,6 +14,16 @@
     1.4  val [pred_0, pred_Suc] = nat_recs pred_def;
     1.5  val [add_0,add_Suc] = nat_recs add_def; 
     1.6  val [mult_0,mult_Suc] = nat_recs mult_def; 
     1.7 +Addsimps [pred_0,pred_Suc,add_0,add_Suc,mult_0,mult_Suc];
     1.8 +
     1.9 +(** pred **)
    1.10 +
    1.11 +val prems = goal Arith.thy "n ~= 0 ==> Suc(pred n) = n";
    1.12 +by(res_inst_tac [("n","n")] natE 1);
    1.13 +by(cut_facts_tac prems 1);
    1.14 +by(ALLGOALS Asm_full_simp_tac);
    1.15 +qed "Suc_pred";
    1.16 +Addsimps [Suc_pred];
    1.17  
    1.18  (** Difference **)
    1.19  
    1.20 @@ -30,10 +40,7 @@
    1.21   (fn _ =>
    1.22    [Simp_tac 1, nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
    1.23  
    1.24 -(*** Simplification over add, mult, diff ***)
    1.25 -
    1.26 -Addsimps [pred_0, pred_Suc, add_0, add_Suc, mult_0, mult_Suc, diff_0,
    1.27 -          diff_0_eq_0, diff_Suc_Suc];
    1.28 +Addsimps [diff_0, diff_0_eq_0, diff_Suc_Suc];
    1.29  
    1.30  
    1.31  (**** Inductive properties of the operators ****)
     2.1 --- a/src/HOL/List.ML	Wed Oct 25 09:46:46 1995 +0100
     2.2 +++ b/src/HOL/List.ML	Wed Oct 25 09:48:29 1995 +0100
     2.3 @@ -125,17 +125,62 @@
     2.4  by (list.induct_tac "xs" 1);
     2.5  by (ALLGOALS Asm_simp_tac);
     2.6  qed"length_append";
     2.7 +Addsimps [length_append];
     2.8 +
     2.9 +goal List.thy "length (map f l) = length l";
    2.10 +by (list.induct_tac "l" 1);
    2.11 +by (ALLGOALS Simp_tac);
    2.12 +qed "length_map";
    2.13 +Addsimps [length_map];
    2.14  
    2.15  goal List.thy "length(rev xs) = length(xs)";
    2.16  by (list.induct_tac "xs" 1);
    2.17 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [length_append])));
    2.18 +by (ALLGOALS Asm_simp_tac);
    2.19  qed "length_rev";
    2.20 +Addsimps [length_rev];
    2.21  
    2.22  (** nth **)
    2.23  
    2.24  val [nth_0,nth_Suc] = nat_recs nth_def; 
    2.25  store_thm("nth_0",nth_0);
    2.26  store_thm("nth_Suc",nth_Suc);
    2.27 +Addsimps [nth_0,nth_Suc];
    2.28 +
    2.29 +goal List.thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
    2.30 +by (list.induct_tac "xs" 1);
    2.31 +(* case [] *)
    2.32 +by (Asm_full_simp_tac 1);
    2.33 +(* case x#xl *)
    2.34 +by (rtac allI 1);
    2.35 +by (nat_ind_tac "n" 1);
    2.36 +by (ALLGOALS Asm_full_simp_tac);
    2.37 +bind_thm("nth_map", result() RS spec RS mp);
    2.38 +Addsimps [nth_map];
    2.39 +
    2.40 +goal List.thy "!n. n < length xs --> list_all P xs --> P(nth n xs)";
    2.41 +by (list.induct_tac "xs" 1);
    2.42 +(* case [] *)
    2.43 +by (Simp_tac 1);
    2.44 +(* case x#xl *)
    2.45 +by (rtac allI 1);
    2.46 +by (nat_ind_tac "n" 1);
    2.47 +by (ALLGOALS Asm_full_simp_tac);
    2.48 +bind_thm("list_all_nth", result() RS spec RS mp RS mp);
    2.49 +
    2.50 +goal List.thy "!n. n < length xs --> (nth n xs) mem xs";
    2.51 +by (list.induct_tac "xs" 1);
    2.52 +(* case [] *)
    2.53 +by (Simp_tac 1);
    2.54 +(* case x#xl *)
    2.55 +by (rtac allI 1);
    2.56 +by (nat_ind_tac "n" 1);
    2.57 +(* case 0 *)
    2.58 +by (Asm_full_simp_tac 1);
    2.59 +(* case Suc x *)
    2.60 +by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    2.61 +bind_thm ("nth_mem",result() RS spec RS mp);
    2.62 +Addsimps [nth_mem];
    2.63 +
    2.64  
    2.65  (** Additional mapping lemmas **)
    2.66  
    2.67 @@ -171,5 +216,5 @@
    2.68     mem_append, mem_filter,
    2.69     rev_append, rev_rev_ident,
    2.70     map_ident, map_append, map_compose,
    2.71 -   flat_append, length_append, list_all_True, list_all_conj, nth_0, nth_Suc];
    2.72 +   flat_append, list_all_True, list_all_conj];
    2.73  
     3.1 --- a/src/HOL/Makefile	Wed Oct 25 09:46:46 1995 +0100
     3.2 +++ b/src/HOL/Makefile	Wed Oct 25 09:48:29 1995 +0100
     3.3 @@ -119,6 +119,14 @@
     3.4  Lambda:  $(BIN)/HOL  $(LAMBDA_FILES)
     3.5  	echo 'exit_use"Lambda/ROOT.ML";quit();' | $(LOGIC)
     3.6  
     3.7 +MINIML_NAMES = I Maybe MiniML Type W
     3.8 +
     3.9 +LAMBDA_FILES = MiniML/ROOT.ML \
    3.10 +              $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
    3.11 +
    3.12 +MiniML: $(BIN)/HOL  $(MINIML_FILES)
    3.13 +	echo 'exit_use"MiniML/ROOT.ML";quit();' | $(LOGIC)
    3.14 +
    3.15  ##Miscellaneous examples
    3.16  EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String \
    3.17  	   BT Perm
    3.18 @@ -130,7 +138,7 @@
    3.19  	echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
    3.20  
    3.21  #Full test. (IOA has been removed temporarily)
    3.22 -test:   $(BIN)/HOL IMP Integ Subst Lambda ex
    3.23 +test:   $(BIN)/HOL IMP Integ Subst Lambda MiniML ex
    3.24  	echo 'Test examples ran successfully' > test
    3.25  
    3.26  .PRECIOUS:  $(BIN)/Pure $(BIN)/HOL 
     4.1 --- a/src/HOL/Nat.ML	Wed Oct 25 09:46:46 1995 +0100
     4.2 +++ b/src/HOL/Nat.ML	Wed Oct 25 09:48:29 1995 +0100
     4.3 @@ -97,6 +97,8 @@
     4.4  
     4.5  bind_thm ("Zero_not_Suc", (Suc_not_Zero RS not_sym));
     4.6  
     4.7 +Addsimps [Suc_not_Zero,Zero_not_Suc];
     4.8 +
     4.9  bind_thm ("Suc_neq_Zero", (Suc_not_Zero RS notE));
    4.10  val Zero_neq_Suc = sym RS Suc_neq_Zero;
    4.11  
    4.12 @@ -118,7 +120,7 @@
    4.13  
    4.14  goal Nat.thy "n ~= Suc(n)";
    4.15  by (nat_ind_tac "n" 1);
    4.16 -by (ALLGOALS(asm_simp_tac (!simpset addsimps [Zero_not_Suc,Suc_Suc_eq])));
    4.17 +by (ALLGOALS(asm_simp_tac (!simpset addsimps [Suc_Suc_eq])));
    4.18  qed "n_not_Suc_n";
    4.19  
    4.20  val Suc_n_not_n = n_not_Suc_n RS not_sym;
    4.21 @@ -203,6 +205,7 @@
    4.22  goalw Nat.thy [less_def] "n < Suc(n)";
    4.23  by (rtac (pred_natI RS r_into_trancl) 1);
    4.24  qed "lessI";
    4.25 +Addsimps [lessI];
    4.26  
    4.27  (* i(j ==> i(Suc(j) *)
    4.28  val less_SucI = lessI RSN (2, less_trans);
    4.29 @@ -213,6 +216,7 @@
    4.30  by (etac less_trans 1);
    4.31  by (rtac lessI 1);
    4.32  qed "zero_less_Suc";
    4.33 +Addsimps [zero_less_Suc];
    4.34  
    4.35  (** Elimination properties **)
    4.36  
    4.37 @@ -251,6 +255,7 @@
    4.38  by (etac Zero_neq_Suc 1);
    4.39  by (etac Zero_neq_Suc 1);
    4.40  qed "not_less0";
    4.41 +Addsimps [not_less0];
    4.42  
    4.43  (* n<0 ==> R *)
    4.44  bind_thm ("less_zeroE", (not_less0 RS notE));
    4.45 @@ -269,6 +274,12 @@
    4.46  		     addEs  [less_trans, less_SucE]) 1);
    4.47  qed "less_Suc_eq";
    4.48  
    4.49 +val prems = goal Nat.thy "m<n ==> n ~= 0";
    4.50 +by(res_inst_tac [("n","n")] natE 1);
    4.51 +by(cut_facts_tac prems 1);
    4.52 +by(ALLGOALS Asm_full_simp_tac);
    4.53 +qed "gr_implies_not0";
    4.54 +Addsimps [gr_implies_not0];
    4.55  
    4.56  (** Inductive (?) properties **)
    4.57  
    4.58 @@ -311,10 +322,18 @@
    4.59  goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
    4.60  by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]);
    4.61  qed "Suc_less_eq";
    4.62 +Addsimps [Suc_less_eq];
    4.63  
    4.64  goal Nat.thy "~(Suc(n) < n)";
    4.65  by(fast_tac (HOL_cs addEs [Suc_lessD RS less_anti_refl]) 1);
    4.66  qed "not_Suc_n_less_n";
    4.67 +Addsimps [not_Suc_n_less_n];
    4.68 +
    4.69 +goal Nat.thy "!!i. i<j ==> j<k --> Suc i < k";
    4.70 +by(nat_ind_tac "k" 1);
    4.71 +by(ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
    4.72 +by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
    4.73 +bind_thm("less_trans_Suc",result() RS mp);
    4.74  
    4.75  (*"Less than" is a linear ordering*)
    4.76  goal Nat.thy "m<n | m=n | n<(m::nat)";
    4.77 @@ -328,8 +347,7 @@
    4.78  (*Can be used with less_Suc_eq to get n=m | n<m *)
    4.79  goal Nat.thy "(~ m < n) = (n < Suc(m))";
    4.80  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    4.81 -by(ALLGOALS(asm_simp_tac (!simpset addsimps
    4.82 -                          [not_less0,zero_less_Suc,Suc_less_eq])));
    4.83 +by(ALLGOALS Asm_simp_tac);
    4.84  qed "not_less_eq";
    4.85  
    4.86  (*Complete induction, aka course-of-values induction*)
    4.87 @@ -346,9 +364,18 @@
    4.88  by (rtac not_less0 1);
    4.89  qed "le0";
    4.90  
    4.91 -Addsimps [not_less0, less_not_refl, zero_less_Suc, lessI, 
    4.92 -          Suc_less_eq, less_Suc_eq, le0, not_Suc_n_less_n,
    4.93 -          Suc_not_Zero, Zero_not_Suc, Suc_Suc_eq,
    4.94 +goalw Nat.thy [le_def] "~ Suc n <= n";
    4.95 +by(Simp_tac 1);
    4.96 +qed "Suc_n_not_le_n";
    4.97 +
    4.98 +goalw Nat.thy [le_def] "(i <= 0) = (i = 0)";
    4.99 +by(nat_ind_tac "i" 1);
   4.100 +by(ALLGOALS Asm_simp_tac);
   4.101 +qed "le_0";
   4.102 +
   4.103 +Addsimps [less_not_refl,
   4.104 +          less_Suc_eq, le0, le_0,
   4.105 +          Suc_Suc_eq, Suc_n_not_le_n,
   4.106            n_not_Suc_n, Suc_n_not_n,
   4.107            nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
   4.108  
     5.1 --- a/src/HOL/Prod.ML	Wed Oct 25 09:46:46 1995 +0100
     5.2 +++ b/src/HOL/Prod.ML	Wed Oct 25 09:48:29 1995 +0100
     5.3 @@ -53,12 +53,40 @@
     5.4  by (REPEAT (eresolve_tac [prem,exE] 1));
     5.5  qed "PairE";
     5.6  
     5.7 +(* replace parameters of product type by individual component parameters *)
     5.8 +local
     5.9 +fun is_pair (_,Type("*",_)) = true
    5.10 +  | is_pair _ = false;
    5.11 +
    5.12 +fun find_pair_param t =
    5.13 +  let val params = Logic.strip_params t
    5.14 +  in if exists is_pair params
    5.15 +     then let val params = rev(rename_wrt_term t params)
    5.16 +                           (*as they are printed*)
    5.17 +          in apsome fst (find_first is_pair params) end
    5.18 +     else None
    5.19 +  end;
    5.20 +
    5.21 +in
    5.22 +
    5.23 +val split_all_tac = REPEAT o SUBGOAL (fn (t,_) =>
    5.24 +  case find_pair_param t of
    5.25 +    None => no_tac
    5.26 +  | Some x => EVERY[res_inst_tac[("p",x)] PairE 1,
    5.27 +                    REPEAT(hyp_subst_tac 1), prune_params_tac]);
    5.28 +
    5.29 +end;
    5.30 +
    5.31 +goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
    5.32 +by(fast_tac (HOL_cs addbefore split_all_tac 1) 1);
    5.33 +qed "split_paired_All";
    5.34 +
    5.35  goalw Prod.thy [split_def] "split c (a,b) = c a b";
    5.36  by (sstac [fst_conv, snd_conv] 1);
    5.37  by (rtac refl 1);
    5.38  qed "split";
    5.39  
    5.40 -Addsimps [fst_conv, snd_conv, split, Pair_eq];
    5.41 +Addsimps [fst_conv, snd_conv, split_paired_All, split, Pair_eq];
    5.42  
    5.43  goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
    5.44  by (res_inst_tac[("p","s")] PairE 1);
     6.1 --- a/src/HOL/ROOT.ML	Wed Oct 25 09:46:46 1995 +0100
     6.2 +++ b/src/HOL/ROOT.ML	Wed Oct 25 09:48:29 1995 +0100
     6.3 @@ -11,7 +11,6 @@
     6.4  writeln banner;
     6.5  
     6.6  print_depth 1;
     6.7 -set eta_contract;
     6.8  
     6.9  (* Add user sections *)
    6.10  use "../Pure/section_utils.ML";
     7.1 --- a/src/HOL/Trancl.ML	Wed Oct 25 09:46:46 1995 +0100
     7.2 +++ b/src/HOL/Trancl.ML	Wed Oct 25 09:48:29 1995 +0100
     7.3 @@ -31,9 +31,9 @@
     7.4  qed "rtrancl_into_rtrancl";
     7.5  
     7.6  (*rtrancl of r contains r*)
     7.7 -val [prem] = goal Trancl.thy "[| (a,b) : r |] ==> (a,b) : r^*";
     7.8 -by (rtac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
     7.9 -by (rtac prem 1);
    7.10 +goal Trancl.thy "!!p. p : r ==> p : r^*";
    7.11 +by(split_all_tac 1);
    7.12 +by (etac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
    7.13  qed "r_into_rtrancl";
    7.14  
    7.15  (*monotonicity of rtrancl*)
    7.16 @@ -161,7 +161,24 @@
    7.17  by(fast_tac (HOL_cs addEs [rtrancl_trans]) 1);
    7.18  be r_into_rtrancl 1;
    7.19  qed "rtrancl_idemp";
    7.20 +Addsimps [rtrancl_idemp];
    7.21  
    7.22 +goal Trancl.thy "!!R. [| R <= S; S <= R^* |] ==> S^* = R^*";
    7.23 +bd rtrancl_mono 1;
    7.24 +bd rtrancl_mono 1;
    7.25 +by(Asm_full_simp_tac 1);
    7.26 +by(fast_tac eq_cs 1);
    7.27 +qed "rtrancl_subset";
    7.28 +
    7.29 +goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
    7.30 +by(best_tac (set_cs addIs [rtrancl_subset,r_into_rtrancl,
    7.31 +                           rtrancl_mono RS subsetD]) 1);
    7.32 +qed "trancl_Un_trancl";
    7.33 +
    7.34 +goal Trancl.thy "(R^=)^* = R^*";
    7.35 +by(fast_tac (rel_cs addIs [rtrancl_refl,rtrancl_subset,r_into_rtrancl]) 1);
    7.36 +qed "rtrancl_reflcl";
    7.37 +Addsimps [rtrancl_reflcl];
    7.38  
    7.39  goal Trancl.thy "!!r. (x,y) : (converse r)^* ==> (x,y) : converse(r^*)";
    7.40  br converseI 1;
    7.41 @@ -198,4 +215,5 @@
    7.42  by (fast_tac (rel_cs addSDs [trancl_subset_Sigma_lemma]) 1);
    7.43  qed "trancl_subset_Sigma";
    7.44  
    7.45 +(* Don't add r_into_rtrancl: it messes up the proofs in Lambda *)
    7.46  val trancl_cs = rel_cs addIs [rtrancl_refl];
     8.1 --- a/src/HOL/Trancl.thy	Wed Oct 25 09:46:46 1995 +0100
     8.2 +++ b/src/HOL/Trancl.thy	Wed Oct 25 09:48:29 1995 +0100
     8.3 @@ -5,14 +5,20 @@
     8.4  
     8.5  Relfexive and Transitive closure of a relation
     8.6  
     8.7 -rtrancl is refl&transitive closure;  trancl is transitive closure
     8.8 +rtrancl is refl&transitive closure;
     8.9 +trancl is transitive closure
    8.10 +reflcl is reflexive closure
    8.11  *)
    8.12  
    8.13  Trancl = Lfp + Relation + 
    8.14  consts
    8.15      rtrancl :: "('a * 'a)set => ('a * 'a)set"	("(_^*)" [100] 100)
    8.16      trancl  :: "('a * 'a)set => ('a * 'a)set"	("(_^+)" [100] 100)  
    8.17 +syntax
    8.18 +    reflcl  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [100] 100)
    8.19  defs   
    8.20 -rtrancl_def	"r^* == lfp(%s. id Un (r O s))"
    8.21 -trancl_def	"r^+ == r O rtrancl(r)"
    8.22 +  rtrancl_def	"r^*  ==  lfp(%s. id Un (r O s))"
    8.23 +  trancl_def	"r^+  ==  r O rtrancl(r)"
    8.24 +translations
    8.25 +                "r^=" == "r Un id"
    8.26  end