# HG changeset patch # User paulson # Date 840446316 -7200 # Node ID c27e624b6d872919ee6ddc9ebd88b0a7a83338d9 # Parent 6d572f96fb765ac8f97a2505a9aeb3f04a3adab7 Tidied some proofs diff -r 6d572f96fb76 -r c27e624b6d87 src/HOL/ex/Comb.ML --- a/src/HOL/ex/Comb.ML Mon Aug 19 11:17:20 1996 +0200 +++ b/src/HOL/ex/Comb.ML Mon Aug 19 11:18:36 1996 +0200 @@ -17,7 +17,6 @@ open Comb; - (*** Reflexive/Transitive closure preserves the Church-Rosser property So does the Transitive closure; use r_into_trancl instead of rtrancl_refl ***) @@ -29,17 +28,17 @@ "!!r. [| diamond(r); (x,y):r^* |] ==> \ \ ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)"; by (etac rtrancl_induct 1); -by (fast_tac (!claset addIs [rtrancl_refl]) 1); +by (Fast_tac 1); by (slow_best_tac (!claset addIs [r_into_rtrancl RSN (2, rtrancl_trans)] - addSDs [spec_mp]) 1); + addSDs [spec_mp]) 1); val diamond_strip_lemmaE = result() RS spec RS mp RS exE; val [major] = goal Comb.thy "diamond(r) ==> diamond(r^*)"; by (rewtac diamond_def); (*unfold only in goal, not in premise!*) by (rtac (impI RS allI RS allI) 1); by (etac rtrancl_induct 1); -by (fast_tac (!claset addIs [rtrancl_refl]) 1); -by (ALLGOALS +by (Fast_tac 1); +by (ALLGOALS (*Seems to be a brittle, undirected search*) (slow_best_tac ((claset_of "Fun") addIs [r_into_rtrancl, rtrancl_trans] addEs [major RS diamond_strip_lemmaE]))); qed "diamond_rtrancl"; @@ -56,27 +55,26 @@ AddIs contract.intrs; AddSEs [K_contractE, S_contractE, Ap_contractE]; -Addss (HOL_ss addsimps comb.simps); +Addss (!simpset); goalw Comb.thy [I_def] "!!z. I -1-> z ==> P"; by (Fast_tac 1); qed "I_contract_E"; +AddSEs [I_contract_E]; -(*Unused*) -goal Comb.thy "!!x z. K#x -1-> z ==> (EX y. z = K#y & x -1-> y)"; +goal Comb.thy "!!x z. K#x -1-> z ==> (EX x'. z = K#x' & x -1-> x')"; by (Fast_tac 1); qed "K1_contractD"; +AddSEs [K1_contractD]; goal Comb.thy "!!x z. x ---> y ==> x#z ---> y#z"; by (etac rtrancl_induct 1); -by (rtac rtrancl_refl 1); -by (fast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans]) 1); +by (ALLGOALS (best_tac (!claset addIs [r_into_rtrancl, rtrancl_trans]))); qed "Ap_reduce1"; goal Comb.thy "!!x z. x ---> y ==> z#x ---> z#y"; by (etac rtrancl_induct 1); -by (rtac rtrancl_refl 1); -by (fast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans]) 1); +by (ALLGOALS (best_tac (!claset addIs [r_into_rtrancl, rtrancl_trans]))); qed "Ap_reduce2"; (** Counterexample to the diamond property for -1-> **) @@ -94,8 +92,7 @@ qed "KIII_contract3"; goalw Comb.thy [diamond_def] "~ diamond(contract)"; -by (fast_tac (!claset addIs [KIII_contract1,KIII_contract2,KIII_contract3] - addSEs [I_contract_E]) 1); +by (fast_tac (!claset addIs [KIII_contract1,KIII_contract2,KIII_contract3]) 1); qed "not_diamond_contract"; @@ -109,30 +106,34 @@ AddIs parcontract.intrs; AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE]; -Addss (HOL_ss addsimps comb.simps); +Addss (!simpset); (*** Basic properties of parallel contraction ***) goal Comb.thy "!!x z. K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')"; by (Fast_tac 1); qed "K1_parcontractD"; +AddSDs [K1_parcontractD]; goal Comb.thy "!!x z. S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')"; by (Fast_tac 1); qed "S1_parcontractD"; +AddSDs [S1_parcontractD]; goal Comb.thy "!!x y z. S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')"; -by (fast_tac (!claset addSDs [S1_parcontractD]) 1); - (*the extra rule makes the proof more than twice as fast*) +by (Fast_tac 1); qed "S2_parcontractD"; +AddSDs [S2_parcontractD]; + +(*The rules above are not essential but make proofs much faster*) + (*Church-Rosser property for parallel contraction*) -goalw Comb.thy [diamond_def] "diamond(parcontract)"; +goalw Comb.thy [diamond_def] "diamond parcontract"; by (rtac (impI RS allI RS allI) 1); by (etac parcontract.induct 1 THEN prune_params_tac); -by (ALLGOALS - (fast_tac (!claset addSDs [K1_parcontractD,S2_parcontractD]))); +by (ALLGOALS Fast_tac); qed "diamond_parcontract"; @@ -142,19 +143,18 @@ by (rtac subsetI 1); by (split_all_tac 1); by (etac contract.induct 1); -by (ALLGOALS (Fast_tac)); +by (ALLGOALS Fast_tac); qed "contract_subset_parcontract"; (*Reductions: simply throw together reflexivity, transitivity and the one-step reductions*) -AddIs [rtrancl_refl, r_into_rtrancl, - contract.K, contract.S, Ap_reduce1, Ap_reduce2, - rtrancl_trans]; +AddSIs [contract.K, contract.S]; +AddIs [Ap_reduce1, Ap_reduce2, r_into_rtrancl, rtrancl_trans]; (*Example only: not used*) goalw Comb.thy [I_def] "I#x ---> x"; -by (Best_tac 1); +by (Deepen_tac 0 1); qed "reduce_I"; goal Comb.thy "parcontract <= contract^*"; @@ -172,9 +172,8 @@ qed "reduce_eq_parreduce"; goal Comb.thy "diamond(contract^*)"; -by (simp_tac (HOL_ss addsimps [reduce_eq_parreduce, diamond_rtrancl, - diamond_parcontract]) 1); - +by (simp_tac (!simpset addsimps [reduce_eq_parreduce, diamond_rtrancl, + diamond_parcontract]) 1); qed "diamond_reduce"; diff -r 6d572f96fb76 -r c27e624b6d87 src/HOL/ex/Mutil.ML --- a/src/HOL/ex/Mutil.ML Mon Aug 19 11:17:20 1996 +0200 +++ b/src/HOL/ex/Mutil.ML Mon Aug 19 11:18:36 1996 +0200 @@ -17,34 +17,37 @@ by (etac tiling.induct 1); by (Simp_tac 1); by (fast_tac (!claset addIs tiling.intrs - addss (HOL_ss addsimps [Un_assoc, - subset_empty_iff RS sym])) 1); -bind_thm ("tiling_UnI", result() RS mp RS mp); + addss (HOL_ss addsimps [Un_assoc, + subset_empty_iff RS sym])) 1); +qed_spec_mp "tiling_UnI"; (*** Chess boards ***) val [below_0, below_Suc] = nat_recs below_def; -Addsimps [below_0]; -(*below_Suc should NOT be added, or Sigma_Suc1,2 cannot be used*) +Addsimps [below_0, below_Suc]; -goal thy "(i: below k) = (i finite d"; by (fast_tac (!claset addSIs [finite_insertI, finite_emptyI] - addEs [domino.elim]) 1); + addEs [domino.elim]) 1); qed "domino_finite"; @@ -165,6 +168,6 @@ THEN asm_simp_tac (!simpset addsimps [tiling_domino_finite, finite_evnodd]) 1 THEN - asm_simp_tac (!simpset addsimps [mod_less, evnodd_iff, below_less_iff]) 1)); + asm_simp_tac (!simpset addsimps [mod_less, evnodd_iff]) 1)); qed "mutil_not_tiling";