# HG changeset patch # User paulson # Date 933088771 -7200 # Node ID 9bfb8e218b9954c602e104780c9500724acb0a34 # Parent a94c9e226c20364e5f5f8644b6bbe0efd7d61dbb expandshort and tidying diff -r a94c9e226c20 -r 9bfb8e218b99 src/HOL/Fun.ML --- a/src/HOL/Fun.ML Tue Jul 27 10:30:26 1999 +0200 +++ b/src/HOL/Fun.ML Tue Jul 27 17:19:31 1999 +0200 @@ -7,7 +7,7 @@ *) -Goal "(f = g) = (!x. f(x)=g(x))"; +Goal "(f = g) = (! x. f(x)=g(x))"; by (rtac iffI 1); by (Asm_simp_tac 1); by (rtac ext 1 THEN Asm_simp_tac 1); @@ -33,25 +33,34 @@ section "id"; -qed_goalw "id_apply" thy [id_def] "id x = x" (K [rtac refl 1]); +Goalw [id_def] "id x = x"; +by (rtac refl 1); +qed "id_apply"; Addsimps [id_apply]; section "o"; -qed_goalw "o_apply" thy [o_def] "(f o g) x = f (g x)" - (K [rtac refl 1]); +Goalw [o_def] "(f o g) x = f (g x)"; +by (rtac refl 1); +qed "o_apply"; Addsimps [o_apply]; -qed_goalw "o_assoc" thy [o_def] "f o (g o h) = f o g o h" - (K [rtac ext 1, rtac refl 1]); +Goalw [o_def] "f o (g o h) = f o g o h"; +by (rtac ext 1); +by (rtac refl 1); +qed "o_assoc"; -qed_goalw "id_o" thy [id_def] "id o g = g" - (K [rtac ext 1, Simp_tac 1]); +Goalw [id_def] "id o g = g"; +by (rtac ext 1); +by (Simp_tac 1); +qed "id_o"; Addsimps [id_o]; -qed_goalw "o_id" thy [id_def] "f o id = f" - (K [rtac ext 1, Simp_tac 1]); +Goalw [id_def] "f o id = f"; +by (rtac ext 1); +by (Simp_tac 1); +qed "o_id"; Addsimps [o_id]; Goalw [o_def] "(f o g)``r = f``(g``r)"; @@ -66,12 +75,12 @@ (** datatypes involving function types **) Goalw [o_def] - "[| !x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa"; -br ext 1; -be allE 1; -be allE 1; -be mp 1; -be fun_cong 1; + "[| ! x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa"; +by (rtac ext 1); +by (etac allE 1); +by (etac allE 1); +by (etac mp 1); +by (etac fun_cong 1); qed "inj_fun_lemma"; @@ -272,15 +281,20 @@ qed "fun_upd_apply"; Addsimps [fun_upd_apply]; -qed_goal "fun_upd_same" thy "(f(x:=y)) x = y" - (K [Simp_tac 1]); -qed_goal "fun_upd_other" thy "!!X. z~=x ==> (f(x:=y)) z = f z" - (K [Asm_simp_tac 1]); -(*Addsimps [fun_upd_same, fun_upd_other];*) +Goal "(f(x:=y)) x = y"; +by (Simp_tac 1); +qed "fun_upd_same"; + +Goal "z~=x ==> (f(x:=y)) z = f z"; +by (Asm_simp_tac 1); +qed "fun_upd_other"; + +(*Currently unused? + We could try Addsimps [fun_upd_same, fun_upd_other];*) Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)"; by (rtac ext 1); -by (Auto_tac); +by Auto_tac; qed "fun_upd_twist"; diff -r a94c9e226c20 -r 9bfb8e218b99 src/HOL/Nat.ML --- a/src/HOL/Nat.ML Tue Jul 27 10:30:26 1999 +0200 +++ b/src/HOL/Nat.ML Tue Jul 27 17:19:31 1999 +0200 @@ -33,14 +33,13 @@ Goal "(n ~= 0) = (0 < n)"; by (exhaust_tac "n" 1); -by (Blast_tac 1); -by (Blast_tac 1); +by Auto_tac; qed "neq0_conv"; AddIffs [neq0_conv]; Goal "(0 ~= n) = (0 < n)"; by (exhaust_tac "n" 1); -by (Auto_tac); +by Auto_tac; qed "zero_neq_conv"; AddIffs [zero_neq_conv]; @@ -75,33 +74,16 @@ by (hyp_subst_tac 1); by (rewtac Least_nat_def); by (rtac (select_equality RS arg_cong RS sym) 1); -by (Safe_tac); -by (dtac Suc_mono 1); -by (Blast_tac 1); -by (cut_facts_tac [less_linear] 1); -by (Safe_tac); -by (atac 2); -by (Blast_tac 2); -by (dtac Suc_mono 1); -by (Blast_tac 1); +by (blast_tac (claset() addDs [Suc_mono]) 1); +by (cut_inst_tac [("m","m")] less_linear 1); +by (blast_tac (claset() addIs [Suc_mono]) 1); qed "Least_Suc"; val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n"; -by (cut_facts_tac prems 1); by (rtac less_induct 1); by (exhaust_tac "n" 1); -by (hyp_subst_tac 1); -by (atac 1); -by (hyp_subst_tac 1); -by (exhaust_tac "nat" 1); -by (hyp_subst_tac 1); -by (atac 1); -by (hyp_subst_tac 1); -by (resolve_tac prems 1); -by (dtac spec 1); -by (etac mp 1); -by (rtac (lessI RS less_trans) 1); -by (rtac (lessI RS Suc_mono) 1); +by (exhaust_tac "nat" 2); +by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans]))); qed "nat_induct2"; Goal "min 0 n = 0";