# HG changeset patch # User wenzelm # Date 1213191668 -7200 # Node ID 5b78e50adc4902d64d1520af3f57c705fff47d60 # Parent 62ab1968c1f42aa4383f7d70874faf96845be15c removed dead code; diff -r 62ab1968c1f4 -r 5b78e50adc49 src/FOL/ex/Classical.thy --- a/src/FOL/ex/Classical.thy Wed Jun 11 15:40:44 2008 +0200 +++ b/src/FOL/ex/Classical.thy Wed Jun 11 15:41:08 2008 +0200 @@ -362,28 +362,6 @@ text{*55*} -(*Original, equational version by Len Schubert, via Pelletier *** NOT PROVED -Goal "(\x. lives(x) & killed(x,agatha)) & - lives(agatha) & lives(butler) & lives(charles) & - (\x. lives(x) --> x=agatha | x=butler | x=charles) & - (\x y. killed(x,y) --> hates(x,y)) & - (\x y. killed(x,y) --> ~richer(x,y)) & - (\x. hates(agatha,x) --> ~hates(charles,x)) & - (\x. ~ x=butler --> hates(agatha,x)) & - (\x. ~richer(x,agatha) --> hates(butler,x)) & - (\x. hates(agatha,x) --> hates(butler,x)) & - (\x. \y. ~hates(x,y)) & - ~ agatha=butler --> - killed(?who,agatha)" -by Safe_tac; -by (dres_inst_tac [("x1","x")] (spec RS mp) 1); -by (assume_tac 1); -by (etac (spec RS exE) 1); -by (REPEAT (etac allE 1)); -by (Blast_tac 1); -result(); -****) - text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988). fast DISCOVERS who killed Agatha. *} lemma "lives(agatha) & lives(butler) & lives(charles) & diff -r 62ab1968c1f4 -r 5b78e50adc49 src/HOL/Complex/NSCA.thy --- a/src/HOL/Complex/NSCA.thy Wed Jun 11 15:40:44 2008 +0200 +++ b/src/HOL/Complex/NSCA.thy Wed Jun 11 15:41:08 2008 +0200 @@ -74,13 +74,6 @@ "z \ SComplex ==> hcmod z \ Reals" by (simp add: Reals_eq_Standard) -(* -Goalw [SComplex_def,SReal_def] "hcmod z \ Reals ==> z \ SComplex" -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [hcmod,hypreal_of_real_def, - hcomplex_of_complex_def,cmod_def])); -*) - subsection{*The Finite Elements form a Subring*} diff -r 62ab1968c1f4 -r 5b78e50adc49 src/HOL/Complex/NSComplex.thy --- a/src/HOL/Complex/NSComplex.thy Wed Jun 11 15:40:44 2008 +0200 +++ b/src/HOL/Complex/NSComplex.thy Wed Jun 11 15:41:08 2008 +0200 @@ -655,108 +655,6 @@ "hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)" by transfer (rule of_real_number_of_eq [symmetric]) -(* -Goal "z + hcnj z = - hcomplex_of_hypreal (2 * hRe(z))" -by (res_inst_tac [("z","z")] eq_Abs_star 1); -by (auto_tac (claset(),HOL_ss addsimps [hRe,hcnj,star_n_add, - hypreal_mult,hcomplex_of_hypreal,complex_add_cnj])); -qed "star_n_add_hcnj"; - -Goal "z - hcnj z = \ -\ hcomplex_of_hypreal (hypreal_of_real #2 * hIm(z)) * iii"; -by (res_inst_tac [("z","z")] eq_Abs_star 1); -by (auto_tac (claset(),simpset() addsimps [hIm,hcnj,hcomplex_diff, - hypreal_of_real_def,hypreal_mult,hcomplex_of_hypreal, - complex_diff_cnj,iii_def,star_n_mult])); -qed "hcomplex_diff_hcnj"; -*) - - -(*** Real and imaginary stuff ***) - -(*Convert??? -Goalw [hcomplex_number_of_def] - "((number_of xa :: hcomplex) + iii * number_of ya = - number_of xb + iii * number_of yb) = - (((number_of xa :: hcomplex) = number_of xb) & - ((number_of ya :: hcomplex) = number_of yb))" -by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff, - hcomplex_hypreal_number_of])); -qed "hcomplex_number_of_eq_cancel_iff"; -Addsimps [hcomplex_number_of_eq_cancel_iff]; - -Goalw [hcomplex_number_of_def] - "((number_of xa :: hcomplex) + number_of ya * iii = \ -\ number_of xb + number_of yb * iii) = \ -\ (((number_of xa :: hcomplex) = number_of xb) & \ -\ ((number_of ya :: hcomplex) = number_of yb))"; -by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffA, - hcomplex_hypreal_number_of])); -qed "hcomplex_number_of_eq_cancel_iffA"; -Addsimps [hcomplex_number_of_eq_cancel_iffA]; - -Goalw [hcomplex_number_of_def] - "((number_of xa :: hcomplex) + number_of ya * iii = \ -\ number_of xb + iii * number_of yb) = \ -\ (((number_of xa :: hcomplex) = number_of xb) & \ -\ ((number_of ya :: hcomplex) = number_of yb))"; -by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffB, - hcomplex_hypreal_number_of])); -qed "hcomplex_number_of_eq_cancel_iffB"; -Addsimps [hcomplex_number_of_eq_cancel_iffB]; - -Goalw [hcomplex_number_of_def] - "((number_of xa :: hcomplex) + iii * number_of ya = \ -\ number_of xb + number_of yb * iii) = \ -\ (((number_of xa :: hcomplex) = number_of xb) & \ -\ ((number_of ya :: hcomplex) = number_of yb))"; -by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iffC, - hcomplex_hypreal_number_of])); -qed "hcomplex_number_of_eq_cancel_iffC"; -Addsimps [hcomplex_number_of_eq_cancel_iffC]; - -Goalw [hcomplex_number_of_def] - "((number_of xa :: hcomplex) + iii * number_of ya = \ -\ number_of xb) = \ -\ (((number_of xa :: hcomplex) = number_of xb) & \ -\ ((number_of ya :: hcomplex) = 0))"; -by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2, - hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff])); -qed "hcomplex_number_of_eq_cancel_iff2"; -Addsimps [hcomplex_number_of_eq_cancel_iff2]; - -Goalw [hcomplex_number_of_def] - "((number_of xa :: hcomplex) + number_of ya * iii = \ -\ number_of xb) = \ -\ (((number_of xa :: hcomplex) = number_of xb) & \ -\ ((number_of ya :: hcomplex) = 0))"; -by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff2a, - hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff])); -qed "hcomplex_number_of_eq_cancel_iff2a"; -Addsimps [hcomplex_number_of_eq_cancel_iff2a]; - -Goalw [hcomplex_number_of_def] - "((number_of xa :: hcomplex) + iii * number_of ya = \ -\ iii * number_of yb) = \ -\ (((number_of xa :: hcomplex) = 0) & \ -\ ((number_of ya :: hcomplex) = number_of yb))"; -by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3, - hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff])); -qed "hcomplex_number_of_eq_cancel_iff3"; -Addsimps [hcomplex_number_of_eq_cancel_iff3]; - -Goalw [hcomplex_number_of_def] - "((number_of xa :: hcomplex) + number_of ya * iii= \ -\ iii * number_of yb) = \ -\ (((number_of xa :: hcomplex) = 0) & \ -\ ((number_of ya :: hcomplex) = number_of yb))"; -by (auto_tac (claset(), HOL_ss addsimps [hcomplex_eq_cancel_iff3a, - hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff])); -qed "hcomplex_number_of_eq_cancel_iff3a"; -Addsimps [hcomplex_number_of_eq_cancel_iff3a]; -*) - lemma hcomplex_number_of_hcnj [simp]: "hcnj (number_of v :: hcomplex) = number_of v" by transfer (rule complex_cnj_number_of) diff -r 62ab1968c1f4 -r 5b78e50adc49 src/HOL/Hyperreal/HLim.thy --- a/src/HOL/Hyperreal/HLim.thy Wed Jun 11 15:40:44 2008 +0200 +++ b/src/HOL/Hyperreal/HLim.thy Wed Jun 11 15:41:08 2008 +0200 @@ -270,53 +270,6 @@ apply (auto intro: approx_hrabs simp add: starfun_rabs_hrabs) done -(**************************************************************** -(%* Leave as commented until I add topology theory or remove? *%) -(%*------------------------------------------------------------ - Elementary topology proof for a characterisation of - continuity now: a function f is continuous if and only - if the inverse image, {x. f(x) \ A}, of any open set A - is always an open set - ------------------------------------------------------------*%) -Goal "[| isNSopen A; \x. isNSCont f x |] - ==> isNSopen {x. f x \ A}" -by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1])); -by (dtac (mem_monad_approx RS approx_sym); -by (dres_inst_tac [("x","a")] spec 1); -by (dtac isNSContD 1 THEN assume_tac 1) -by (dtac bspec 1 THEN assume_tac 1) -by (dres_inst_tac [("x","( *f* f) x")] approx_mem_monad2 1); -by (blast_tac (claset() addIs [starfun_mem_starset]); -qed "isNSCont_isNSopen"; - -Goalw [isNSCont_def] - "\A. isNSopen A --> isNSopen {x. f x \ A} \ -\ ==> isNSCont f x"; -by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS - (approx_minus_iff RS iffD2)],simpset() addsimps - [Infinitesimal_def,SReal_iff])); -by (dres_inst_tac [("x","{z. abs(z + -f(x)) < ya}")] spec 1); -by (etac (isNSopen_open_interval RSN (2,impE)); -by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def])); -by (dres_inst_tac [("x","x")] spec 1); -by (auto_tac (claset() addDs [approx_sym RS approx_mem_monad], - simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus])); -qed "isNSopen_isNSCont"; - -Goal "(\x. isNSCont f x) = \ -\ (\A. isNSopen A --> isNSopen {x. f(x) \ A})"; -by (blast_tac (claset() addIs [isNSCont_isNSopen, - isNSopen_isNSCont]); -qed "isNSCont_isNSopen_iff"; - -(%*------- Standard version of same theorem --------*%) -Goal "(\x. isCont f x) = \ -\ (\A. isopen A --> isopen {x. f(x) \ A})"; -by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff], - simpset() addsimps [isNSopen_isopen_iff RS sym, - isNSCont_isCont_iff RS sym])); -qed "isCont_isopen_iff"; -*******************************************************************) subsection {* Uniform Continuity *} diff -r 62ab1968c1f4 -r 5b78e50adc49 src/HOL/Hyperreal/HTranscendental.thy --- a/src/HOL/Hyperreal/HTranscendental.thy Wed Jun 11 15:40:44 2008 +0200 +++ b/src/HOL/Hyperreal/HTranscendental.thy Wed Jun 11 15:41:08 2008 +0200 @@ -306,19 +306,6 @@ lemma starfun_exp_gt_one [simp]: "!!x::hypreal. 0 < x ==> 1 < ( *f* exp) x" by transfer (rule exp_gt_one) -(* needs derivative of inverse function - TRY a NS one today!!! - -Goal "x @= 1 ==> ( *f* ln) x @= 1" -by (res_inst_tac [("z","x")] eq_Abs_star 1); -by (auto_tac (claset(),simpset() addsimps [hypreal_one_def])); - - -Goalw [nsderiv_def] "0r < x ==> NSDERIV ln x :> inverse x"; - -*) - - lemma starfun_ln_exp [simp]: "!!x. ( *f* ln) (( *f* exp) x) = x" by transfer (rule ln_exp) diff -r 62ab1968c1f4 -r 5b78e50adc49 src/HOL/IMPP/Misc.thy --- a/src/HOL/IMPP/Misc.thy Wed Jun 11 15:40:44 2008 +0200 +++ b/src/HOL/IMPP/Misc.thy Wed Jun 11 15:41:08 2008 +0200 @@ -85,16 +85,9 @@ lemma classic_Local: "!v. G|-{%Z s. P Z (s[Loc Y::=v]) & s = a (s[Loc Y::=v])}. c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|-{P}. LOCAL Y:=a IN c .{Q}" apply (rule export_s) -(*variant 1*) apply (rule hoare_derivs.Local [THEN conseq1]) apply (erule spec) apply force -(*variant 2 -by (res_inst_tac [("P'","%Z s. s' = s & P Z (s[Loc Y::=a s][Loc Y::=s']) & (s[Loc Y::=a s]) = a (s[Loc Y::=a s][Loc Y::=s'])")] conseq1 1) -by (Clarsimp_tac 2); -by (rtac hoare_derivs.Local 1); -by (etac spec 1); -*) done lemma classic_Local_indep: "[| Y~=Y'; G|-{P}. c .{%Z s. s = d} |] ==> diff -r 62ab1968c1f4 -r 5b78e50adc49 src/HOLCF/FOCUS/Fstream.thy --- a/src/HOLCF/FOCUS/Fstream.thy Wed Jun 11 15:40:44 2008 +0200 +++ b/src/HOLCF/FOCUS/Fstream.thy Wed Jun 11 15:41:08 2008 +0200 @@ -68,10 +68,7 @@ apply fast apply fast done -(* -fun fstream_case_tac s i = res_inst_tac [("x",s)] fstream_cases i - THEN hyp_subst_tac i THEN hyp_subst_tac (i+1); -*) + lemma fstream_exhaust_eq: "(x ~= UU) = (? a y. x = a~> y)" apply (simp add: fscons_def2 stream_exhaust_eq) apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) diff -r 62ab1968c1f4 -r 5b78e50adc49 src/HOLCF/Tr.thy --- a/src/HOLCF/Tr.thy Wed Jun 11 15:40:44 2008 +0200 +++ b/src/HOLCF/Tr.thy Wed Jun 11 15:41:08 2008 +0200 @@ -81,15 +81,8 @@ text {* tactic for tr-thms with case split *} lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def -(* -fun prover t = prove_goal thy t - (fn prems => - [ - (res_inst_tac [("p","y")] trE 1), - (REPEAT(asm_simp_tac (simpset() addsimps - [o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1)) - ]) -*) + + text {* distinctness for type @{typ tr} *} lemma dist_less_tr [simp]: