--- 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 "(\<exists>x. lives(x) & killed(x,agatha)) &
- lives(agatha) & lives(butler) & lives(charles) &
- (\<forall>x. lives(x) --> x=agatha | x=butler | x=charles) &
- (\<forall>x y. killed(x,y) --> hates(x,y)) &
- (\<forall>x y. killed(x,y) --> ~richer(x,y)) &
- (\<forall>x. hates(agatha,x) --> ~hates(charles,x)) &
- (\<forall>x. ~ x=butler --> hates(agatha,x)) &
- (\<forall>x. ~richer(x,agatha) --> hates(butler,x)) &
- (\<forall>x. hates(agatha,x) --> hates(butler,x)) &
- (\<forall>x. \<exists>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) &
--- 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 \<in> SComplex ==> hcmod z \<in> Reals"
by (simp add: Reals_eq_Standard)
-(*
-Goalw [SComplex_def,SReal_def] "hcmod z \<in> Reals ==> z \<in> 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*}
--- 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)
--- 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) \<in> A}, of any open set A
- is always an open set
- ------------------------------------------------------------*%)
-Goal "[| isNSopen A; \<forall>x. isNSCont f x |]
- ==> isNSopen {x. f x \<in> 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]
- "\<forall>A. isNSopen A --> isNSopen {x. f x \<in> 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 "(\<forall>x. isNSCont f x) = \
-\ (\<forall>A. isNSopen A --> isNSopen {x. f(x) \<in> A})";
-by (blast_tac (claset() addIs [isNSCont_isNSopen,
- isNSopen_isNSCont]);
-qed "isNSCont_isNSopen_iff";
-
-(%*------- Standard version of same theorem --------*%)
-Goal "(\<forall>x. isCont f x) = \
-\ (\<forall>A. isopen A --> isopen {x. f(x) \<in> 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 *}
--- 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)
--- 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<Y> = 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'<Y>]) & (s[Loc Y::=a s])<Y> = a (s[Loc Y::=a s][Loc Y::=s'<Y>])")] 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<Y'> = d} |] ==>
--- 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)
--- 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]: