diff -r 3a8d722fd3ff -r 16c4ea954511 IOA/example/Lemmas.ML --- a/IOA/example/Lemmas.ML Fri Nov 11 10:35:03 1994 +0100 +++ b/IOA/example/Lemmas.ML Mon Nov 21 17:50:34 1994 +0100 @@ -11,37 +11,37 @@ (* Logic *) val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R"; by(fast_tac (HOL_cs addDs prems) 1); -val imp_conj_lemma = result(); +qed "imp_conj_lemma"; goal HOL.thy "(P --> (? x. Q(x))) = (? x. P --> Q(x))"; by(fast_tac HOL_cs 1); -val imp_ex_equiv = result(); +qed "imp_ex_equiv"; goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))"; by (fast_tac HOL_cs 1); -val fork_lemma = result(); +qed "fork_lemma"; goal HOL.thy "((A --> B) & (C --> B)) = ((A | C) --> B)"; by (fast_tac HOL_cs 1); -val imp_or_lem = result(); +qed "imp_or_lem"; goal HOL.thy "(X = (~ Y)) = ((~X) = Y)"; by (fast_tac HOL_cs 1); -val neg_flip = result(); +qed "neg_flip"; goal HOL.thy "P --> Q(M) --> Q(if(P,M,N))"; by (rtac impI 1); by (rtac impI 1); by (rtac (expand_if RS iffD2) 1); by (fast_tac HOL_cs 1); -val imp_true_decompose = result(); +qed "imp_true_decompose"; goal HOL.thy "(~P) --> Q(N) --> Q(if(P,M,N))"; by (rtac impI 1); by (rtac impI 1); by (rtac (expand_if RS iffD2) 1); by (fast_tac HOL_cs 1); -val imp_false_decompose = result(); +qed "imp_false_decompose"; (* Sets *) @@ -57,7 +57,7 @@ goal Arith.thy "n ~= 0 --> Suc(m+pred(n)) = m+n"; by (nat_ind_tac "n" 1); by (REPEAT(simp_tac arith_ss 1)); -val Suc_pred_lemma = result() RS mp; +val Suc_pred_lemma = store_thm("Suc_pred_lemma", result() RS mp); goal Arith.thy "x <= y --> x <= Suc(y)"; by (rtac impI 1); @@ -67,43 +67,43 @@ by (etac disjE 1); by (etac less_SucI 1); by (asm_simp_tac nat_ss 1); -val leq_imp_leq_suc = result() RS mp; +val leq_imp_leq_suc = store_thm("leq_imp_leq_suc", result() RS mp); (* Same as previous! *) goal Arith.thy "(x::nat)<=y --> x<=Suc(y)"; by (simp_tac (arith_ss addsimps [le_eq_less_or_eq]) 1); -val leq_suc = result(); +qed "leq_suc"; goal Arith.thy "((m::nat) + n = m + p) = (n = p)"; by (nat_ind_tac "m" 1); by (simp_tac arith_ss 1); by (asm_simp_tac arith_ss 1); -val left_plus_cancel = result(); +qed "left_plus_cancel"; goal Arith.thy "((x::nat) + y = Suc(x + z)) = (y = Suc(z))"; by (nat_ind_tac "x" 1); by (simp_tac arith_ss 1); by (asm_simp_tac arith_ss 1); -val left_plus_cancel_inside_succ = result(); +qed "left_plus_cancel_inside_succ"; goal Arith.thy "(x ~= 0) = (? y. x = Suc(y))"; by (nat_ind_tac "x" 1); by (simp_tac arith_ss 1); by (asm_simp_tac arith_ss 1); by (fast_tac HOL_cs 1); -val nonzero_is_succ = result(); +qed "nonzero_is_succ"; goal Arith.thy "(m::nat) < n --> m + p < n + p"; by (nat_ind_tac "p" 1); by (simp_tac arith_ss 1); by (asm_simp_tac arith_ss 1); -val less_add_same_less = result(); +qed "less_add_same_less"; goal Arith.thy "(x::nat)<= y --> x<=y+k"; by (nat_ind_tac "k" 1); by (simp_tac arith_ss 1); by (asm_full_simp_tac (arith_ss addsimps [leq_suc]) 1); -val leq_add_leq = result(); +qed "leq_add_leq"; goal Arith.thy "(x::nat) + y <= z --> x <= z"; by (nat_ind_tac "y" 1); @@ -112,7 +112,7 @@ by (rtac impI 1); by (dtac Suc_leD 1); by (fast_tac HOL_cs 1); -val left_add_leq = result(); +qed "left_add_leq"; goal Arith.thy "(A::nat) < B --> C < D --> A + C < B + D"; by (rtac impI 1); @@ -124,12 +124,12 @@ by (res_inst_tac [("m1","B")] (add_commute RS ssubst) 1); by (rtac (less_add_same_less RS mp) 1); by (assume_tac 1); -val less_add_cong = result(); +qed "less_add_cong"; goal Nat.thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)"; by (dtac le_imp_less_or_eq 1); by (fast_tac (HOL_cs addIs [less_trans]) 1); -val less_leq_less = result(); +qed "less_leq_less"; goal Arith.thy "(A::nat) <= B --> C <= D --> A + C <= B + D"; by (rtac impI 1); @@ -145,7 +145,7 @@ by (res_inst_tac [("m1","B")] (add_commute RS ssubst) 1); by (rtac (less_add_same_less RS mp) 1); by (assume_tac 1); -val less_eq_add_cong = result(); +qed "less_eq_add_cong"; goal Arith.thy "(w <= y) --> ((x::nat) + y <= z) --> (x + w <= z)"; by (rtac impI 1); @@ -156,7 +156,7 @@ by (rtac impI 1); by (etac le_trans 1); by (assume_tac 1); -val leq_add_left_cong = result(); +qed "leq_add_left_cong"; goal Arith.thy "(? x. y = Suc(x)) = (~(y = 0))"; by (nat_ind_tac "y" 1); @@ -164,7 +164,7 @@ by (rtac iffI 1); by (asm_full_simp_tac arith_ss 1); by (fast_tac HOL_cs 1); -val suc_not_zero = result(); +qed "suc_not_zero"; goal Arith.thy "Suc(x) <= y --> (? z. y = Suc(z))"; by (rtac impI 1); @@ -176,7 +176,7 @@ by (asm_full_simp_tac (arith_ss addsimps [suc_not_zero]) 1); by (hyp_subst_tac 1); by (asm_full_simp_tac arith_ss 1); -val suc_leq_suc = result(); +qed "suc_leq_suc"; goal Arith.thy "~0 n = 0"; by (nat_ind_tac "n" 1); @@ -184,43 +184,43 @@ by (safe_tac HOL_cs); by (asm_full_simp_tac arith_ss 1); by (asm_full_simp_tac arith_ss 1); -val zero_eq = result(); +qed "zero_eq"; goal Arith.thy "x < Suc(y) --> x<=y"; by (nat_ind_tac "n" 1); by (asm_simp_tac arith_ss 1); by (safe_tac HOL_cs); by (etac less_imp_le 1); -val less_suc_imp_leq = result(); +qed "less_suc_imp_leq"; goal Arith.thy "0 Suc(pred(x)) = x"; by (nat_ind_tac "x" 1); by (simp_tac arith_ss 1); by (asm_simp_tac arith_ss 1); -val suc_pred_id = result(); +qed "suc_pred_id"; goal Arith.thy "0 (pred(x) = y) = (x = Suc(y))"; by (nat_ind_tac "x" 1); by (simp_tac arith_ss 1); by (asm_simp_tac arith_ss 1); -val pred_suc = result(); +qed "pred_suc"; goal Arith.thy "(x ~= 0) = (0 y<=z --> x<(z::nat)"; by (rtac impI 1); by (rtac impI 1); by (dtac le_imp_less_or_eq 1); by (fast_tac (HOL_cs addIs [less_trans]) 1); -val less_leq_less = result(); +qed "less_leq_less"; goal Arith.thy "(Suc(n) <= Suc(m)) = (n <= m)"; by (simp_tac (arith_ss addsimps [le_eq_less_or_eq]) 1); -val succ_leq_mono = result(); +qed "succ_leq_mono"; (* Odd proof. Why do induction? *) goal Arith.thy "((x::nat) = y + z) --> (y <= x)"; @@ -228,7 +228,7 @@ by (simp_tac arith_ss 1); by (simp_tac (arith_ss addsimps [succ_leq_mono, le_refl RS (leq_add_leq RS mp)]) 1); -val plus_leq_lem = result(); +qed "plus_leq_lem"; (* Lists *) @@ -236,20 +236,20 @@ by (list_ind_tac "L" 1); by (simp_tac list_ss 1); by (asm_simp_tac list_ss 1); -val append_cons = result(); +qed "append_cons"; goal List.thy "(X ~= hd(L@M)) = (X ~= if(L = [], hd(M), hd(L)))"; by (list_ind_tac "L" 1); by (simp_tac list_ss 1); by (asm_full_simp_tac list_ss 1); -val not_hd_append = result(); +qed "not_hd_append"; goal List.thy "(L = (x#rst)) --> (L = []) --> P"; by (simp_tac list_ss 1); -val list_cases = result(); +qed "list_cases"; goal List.thy "(? L2. L1 = x#L2) --> (L1 ~= [])"; by (strip_tac 1); by (etac exE 1); by (asm_simp_tac list_ss 1); -val cons_imp_not_null = result(); +qed "cons_imp_not_null";