# HG changeset patch # User nipkow # Date 978716898 -3600 # Node ID 028d22926a4151ec6a49b76923ca8675ff56c92d # Parent c0bcea781b3ac0488f1886ca0c879e84148fd257 ^^ -> ``` Univalent -> single_valued diff -r c0bcea781b3a -r 028d22926a41 src/HOL/BCV/JType.ML --- a/src/HOL/BCV/JType.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/BCV/JType.ML Fri Jan 05 18:48:18 2001 +0100 @@ -103,7 +103,7 @@ Addsimps [is_type_def]; Goalw [closed_def,plussub_def,lift2_def,err_def,JType.sup_def] - "[| univalent S; acyclic S |] ==> \ + "[| single_valued S; acyclic S |] ==> \ \ closed (err(types S)) (lift2 (JType.sup S))"; by (simp_tac (simpset() addsplits [err.split,ty.split]) 1); by (blast_tac (claset() addSDs [is_lub_some_lub,is_lubD,is_ubD] @@ -113,7 +113,7 @@ AddIffs [OK_le_conv]; Goalw [semilat_def,split RS eq_reflection,JType.esl_def,Err.sl_def] - "[| univalent S; acyclic S |] ==> err_semilat (JType.esl S)"; + "[| single_valued S; acyclic S |] ==> err_semilat (JType.esl S)"; by (asm_full_simp_tac (simpset() addsimps [acyclic_impl_order_subtype,closed_err_types]) 1); by (rtac conjI 1); diff -r c0bcea781b3a -r 028d22926a41 src/HOL/BCV/JVM.ML --- a/src/HOL/BCV/JVM.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/BCV/JVM.ML Fri Jan 05 18:48:18 2001 +0100 @@ -229,7 +229,7 @@ Goalw [JVM.sl_def,stk_esl_def,reg_sl_def] - "[| univalent S; acyclic S |] ==> semilat(JVM.sl S maxs maxr)"; + "[| single_valued S; acyclic S |] ==> semilat(JVM.sl S maxs maxr)"; by (REPEAT(ares_tac [semilat_opt,err_semilat_Product_esl,err_semilat_upto_esl, err_semilat_eslI,semilat_Listn_sl,err_semilat_JType_esl] 1)); qed "semilat_JVM_slI"; @@ -241,7 +241,7 @@ qed "sl_triple_conv"; Goalw [kiljvm_def,sl_triple_conv] - "[| univalent S; wf(S^-1); wfis S md maxr bs; wf_mdict S md; \ + "[| single_valued S; wf(S^-1); wfis S md maxr bs; wf_mdict S md; \ \ bounded (succs bs) (size bs) |] ==> \ \ is_bcv (JVM.le S maxs maxr) (Some Err) (wti S maxs rT bs) \ \ (size bs) (states S maxs maxr) (kiljvm S maxs maxr rT bs)"; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/BCV/Semilat.ML --- a/src/HOL/BCV/Semilat.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/BCV/Semilat.ML Fri Jan 05 18:48:18 2001 +0100 @@ -136,21 +136,21 @@ Goalw [is_lub_def,is_ub_def] - "[| univalent r; is_lub (r^*) x y u; (x',x) : r |] ==> \ + "[| single_valued r; is_lub (r^*) x y u; (x',x) : r |] ==> \ \ EX v. is_lub (r^*) x' y v"; by (case_tac "(y,x) : r^*" 1); by (case_tac "(y,x') : r^*" 1); by (Blast_tac 1); by (blast_tac (claset() addIs [r_into_rtrancl] addEs [converse_rtranclE] - addDs [univalentD]) 1); + addDs [single_valuedD]) 1); by (rtac exI 1); by (rtac conjI 1); - by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]addDs [univalentD]) 1); + by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]addDs [single_valuedD]) 1); by (blast_tac (claset() addIs [rtrancl_into_rtrancl,rtrancl_into_rtrancl2] - addEs [converse_rtranclE] addDs [univalentD]) 1); + addEs [converse_rtranclE] addDs [single_valuedD]) 1); qed "extend_lub"; -Goal "[| univalent r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> \ +Goal "[| single_valued r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> \ \ (EX z. is_lub (r^*) x y z))"; by (etac converse_rtrancl_induct 1); by (Clarify_tac 1); @@ -158,7 +158,7 @@ by (Blast_tac 1); by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); by (blast_tac (claset() addIs [extend_lub]) 1); -qed_spec_mp "univalent_has_lubs"; +qed_spec_mp "single_valued_has_lubs"; Goalw [some_lub_def,is_lub_def] "[| acyclic r; is_lub (r^*) x y u |] ==> some_lub (r^*) x y = u"; @@ -169,9 +169,9 @@ qed "some_lub_conv"; Goal - "[| univalent r; acyclic r; (x,u):r^*; (y,u):r^* |] ==> \ + "[| single_valued r; acyclic r; (x,u):r^*; (y,u):r^* |] ==> \ \ is_lub (r^*) x y (some_lub (r^*) x y)"; by (fast_tac - (claset() addDs [univalent_has_lubs] + (claset() addDs [single_valued_has_lubs] addss (simpset() addsimps [some_lub_conv])) 1); qed "is_lub_some_lub"; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Hyperreal/HRealAbs.ML --- a/src/HOL/Hyperreal/HRealAbs.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Hyperreal/HRealAbs.ML Fri Jan 05 18:48:18 2001 +0100 @@ -19,8 +19,8 @@ Addsimps [hrabs_number_of]; Goalw [hrabs_def] - "abs (Abs_hypreal (hyprel ^^ {X})) = \ -\ Abs_hypreal(hyprel ^^ {%n. abs (X n)})"; + "abs (Abs_hypreal (hyprel ``` {X})) = \ +\ Abs_hypreal(hyprel ``` {%n. abs (X n)})"; by (auto_tac (claset(), simpset_of HyperDef.thy addsimps [hypreal_zero_def, hypreal_le,hypreal_minus])); @@ -232,7 +232,7 @@ (*------------------------------------------------------------*) Goalw [hypreal_of_nat_def, hypreal_of_real_def, real_of_nat_def] - "hypreal_of_nat m = Abs_hypreal(hyprel^^{%n. real_of_nat m})"; + "hypreal_of_nat m = Abs_hypreal(hyprel```{%n. real_of_nat m})"; by Auto_tac; qed "hypreal_of_nat_iff"; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Hyperreal/HSeries.ML --- a/src/HOL/Hyperreal/HSeries.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Hyperreal/HSeries.ML Fri Jan 05 18:48:18 2001 +0100 @@ -8,14 +8,14 @@ Goalw [sumhr_def] "sumhr(M,N,f) = \ \ Abs_hypreal(UN X:Rep_hypnat(M). UN Y: Rep_hypnat(N). \ -\ hyprel ^^{%n::nat. sumr (X n) (Y n) f})"; +\ hyprel ```{%n::nat. sumr (X n) (Y n) f})"; by (Auto_tac); qed "sumhr_iff"; Goalw [sumhr_def] - "sumhr(Abs_hypnat(hypnatrel^^{%n. M n}), \ -\ Abs_hypnat(hypnatrel^^{%n. N n}), f) = \ -\ Abs_hypreal(hyprel ^^ {%n. sumr (M n) (N n) f})"; + "sumhr(Abs_hypnat(hypnatrel```{%n. M n}), \ +\ Abs_hypnat(hypnatrel```{%n. N n}), f) = \ +\ Abs_hypreal(hyprel ``` {%n. sumr (M n) (N n) f})"; by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); by (Auto_tac THEN Ultra_tac 1); qed "sumhr"; @@ -27,7 +27,7 @@ Goalw [sumhr_def] "sumhr p = (%(M,N,f). Abs_hypreal(UN X:Rep_hypnat(M). \ \ UN Y: Rep_hypnat(N). \ -\ hyprel ^^{%n::nat. sumr (X n) (Y n) f})) p"; +\ hyprel ```{%n::nat. sumr (X n) (Y n) f})) p"; by (res_inst_tac [("p","p")] PairE 1); by (res_inst_tac [("p","y")] PairE 1); by (Auto_tac); diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Hyperreal/HSeries.thy --- a/src/HOL/Hyperreal/HSeries.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Hyperreal/HSeries.thy Fri Jan 05 18:48:18 2001 +0100 @@ -15,7 +15,7 @@ "sumhr p == Abs_hypreal(UN X:Rep_hypnat(fst p). UN Y: Rep_hypnat(fst(snd p)). - hyprel ^^{%n::nat. sumr (X n) (Y n) (snd(snd p))})" + hyprel```{%n::nat. sumr (X n) (Y n) (snd(snd p))})" constdefs NSsums :: [nat=>real,real] => bool (infixr 80) diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Hyperreal/HyperDef.ML --- a/src/HOL/Hyperreal/HyperDef.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Hyperreal/HyperDef.ML Fri Jan 05 18:48:18 2001 +0100 @@ -206,11 +206,11 @@ simpset() addsimps [FreeUltrafilterNat_Nat_set])); qed "equiv_hyprel"; -(* (hyprel ^^ {x} = hyprel ^^ {y}) = ((x,y) : hyprel) *) +(* (hyprel ``` {x} = hyprel ``` {y}) = ((x,y) : hyprel) *) bind_thm ("equiv_hyprel_iff", [equiv_hyprel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff); -Goalw [hypreal_def,hyprel_def,quotient_def] "hyprel^^{x}:hypreal"; +Goalw [hypreal_def,hyprel_def,quotient_def] "hyprel```{x}:hypreal"; by (Blast_tac 1); qed "hyprel_in_hypreal"; @@ -230,7 +230,7 @@ by (rtac Rep_hypreal_inverse 1); qed "inj_Rep_hypreal"; -Goalw [hyprel_def] "x: hyprel ^^ {x}"; +Goalw [hyprel_def] "x: hyprel ``` {x}"; by (Step_tac 1); by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset())); qed "lemma_hyprel_refl"; @@ -267,7 +267,7 @@ qed "inj_hypreal_of_real"; val [prem] = goal (the_context ()) - "(!!x y. z = Abs_hypreal(hyprel^^{x}) ==> P) ==> P"; + "(!!x y. z = Abs_hypreal(hyprel```{x}) ==> P) ==> P"; by (res_inst_tac [("x1","z")] (rewrite_rule [hypreal_def] Rep_hypreal RS quotientE) 1); by (dres_inst_tac [("f","Abs_hypreal")] arg_cong 1); @@ -278,13 +278,13 @@ (**** hypreal_minus: additive inverse on hypreal ****) Goalw [congruent_def] - "congruent hyprel (%X. hyprel^^{%n. - (X n)})"; + "congruent hyprel (%X. hyprel```{%n. - (X n)})"; by Safe_tac; by (ALLGOALS Ultra_tac); qed "hypreal_minus_congruent"; Goalw [hypreal_minus_def] - "- (Abs_hypreal(hyprel^^{%n. X n})) = Abs_hypreal(hyprel ^^ {%n. -(X n)})"; + "- (Abs_hypreal(hyprel```{%n. X n})) = Abs_hypreal(hyprel ``` {%n. -(X n)})"; by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); by (simp_tac (simpset() addsimps [hyprel_in_hypreal RS Abs_hypreal_inverse, @@ -322,20 +322,20 @@ (**** hyperreal addition: hypreal_add ****) Goalw [congruent2_def] - "congruent2 hyprel (%X Y. hyprel^^{%n. X n + Y n})"; + "congruent2 hyprel (%X Y. hyprel```{%n. X n + Y n})"; by Safe_tac; by (ALLGOALS(Ultra_tac)); qed "hypreal_add_congruent2"; Goalw [hypreal_add_def] - "Abs_hypreal(hyprel^^{%n. X n}) + Abs_hypreal(hyprel^^{%n. Y n}) = \ -\ Abs_hypreal(hyprel^^{%n. X n + Y n})"; + "Abs_hypreal(hyprel```{%n. X n}) + Abs_hypreal(hyprel```{%n. Y n}) = \ +\ Abs_hypreal(hyprel```{%n. X n + Y n})"; by (simp_tac (simpset() addsimps [[equiv_hyprel, hypreal_add_congruent2] MRS UN_equiv_class2]) 1); qed "hypreal_add"; -Goal "Abs_hypreal(hyprel^^{%n. X n}) - Abs_hypreal(hyprel^^{%n. Y n}) = \ -\ Abs_hypreal(hyprel^^{%n. X n - Y n})"; +Goal "Abs_hypreal(hyprel```{%n. X n}) - Abs_hypreal(hyprel```{%n. Y n}) = \ +\ Abs_hypreal(hyprel```{%n. X n - Y n})"; by (simp_tac (simpset() addsimps [hypreal_diff_def, hypreal_minus,hypreal_add]) 1); qed "hypreal_diff"; @@ -496,14 +496,14 @@ (**** hyperreal multiplication: hypreal_mult ****) Goalw [congruent2_def] - "congruent2 hyprel (%X Y. hyprel^^{%n. X n * Y n})"; + "congruent2 hyprel (%X Y. hyprel```{%n. X n * Y n})"; by Safe_tac; by (ALLGOALS(Ultra_tac)); qed "hypreal_mult_congruent2"; Goalw [hypreal_mult_def] - "Abs_hypreal(hyprel^^{%n. X n}) * Abs_hypreal(hyprel^^{%n. Y n}) = \ -\ Abs_hypreal(hyprel^^{%n. X n * Y n})"; + "Abs_hypreal(hyprel```{%n. X n}) * Abs_hypreal(hyprel```{%n. Y n}) = \ +\ Abs_hypreal(hyprel```{%n. X n * Y n})"; by (simp_tac (simpset() addsimps [[equiv_hyprel, hypreal_mult_congruent2] MRS UN_equiv_class2]) 1); qed "hypreal_mult"; @@ -622,13 +622,13 @@ (**** multiplicative inverse on hypreal ****) Goalw [congruent_def] - "congruent hyprel (%X. hyprel^^{%n. if X n = #0 then #0 else inverse(X n)})"; + "congruent hyprel (%X. hyprel```{%n. if X n = #0 then #0 else inverse(X n)})"; by (Auto_tac THEN Ultra_tac 1); qed "hypreal_inverse_congruent"; Goalw [hypreal_inverse_def] - "inverse (Abs_hypreal(hyprel^^{%n. X n})) = \ -\ Abs_hypreal(hyprel ^^ {%n. if X n = #0 then #0 else inverse(X n)})"; + "inverse (Abs_hypreal(hyprel```{%n. X n})) = \ +\ Abs_hypreal(hyprel ``` {%n. if X n = #0 then #0 else inverse(X n)})"; by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); by (simp_tac (simpset() addsimps [hyprel_in_hypreal RS Abs_hypreal_inverse, @@ -800,8 +800,8 @@ makes many of them more straightforward. -------------------------------------------------------*) Goalw [hypreal_less_def] - "(Abs_hypreal(hyprel^^{%n. X n}) < \ -\ Abs_hypreal(hyprel^^{%n. Y n})) = \ + "(Abs_hypreal(hyprel```{%n. X n}) < \ +\ Abs_hypreal(hyprel```{%n. Y n})) = \ \ ({n. X n < Y n} : FreeUltrafilterNat)"; by (auto_tac (claset() addSIs [lemma_hyprel_refl], simpset())); by (Ultra_tac 1); @@ -840,7 +840,7 @@ Trichotomy of the hyperreals --------------------------------------------------------------------------------*) -Goalw [hyprel_def] "EX x. x: hyprel ^^ {%n. #0}"; +Goalw [hyprel_def] "EX x. x: hyprel ``` {%n. #0}"; by (res_inst_tac [("x","%n. #0")] exI 1); by (Step_tac 1); by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset())); @@ -958,8 +958,8 @@ (*------ hypreal le iff reals le a.e ------*) Goalw [hypreal_le_def,real_le_def] - "(Abs_hypreal(hyprel^^{%n. X n}) <= \ -\ Abs_hypreal(hyprel^^{%n. Y n})) = \ + "(Abs_hypreal(hyprel```{%n. X n}) <= \ +\ Abs_hypreal(hyprel```{%n. Y n})) = \ \ ({n. X n <= Y n} : FreeUltrafilterNat)"; by (auto_tac (claset(),simpset() addsimps [hypreal_less])); by (ALLGOALS(Ultra_tac)); diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Hyperreal/HyperDef.thy --- a/src/HOL/Hyperreal/HyperDef.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Hyperreal/HyperDef.thy Fri Jan 05 18:48:18 2001 +0100 @@ -37,28 +37,28 @@ defs hypreal_zero_def - "0 == Abs_hypreal(hyprel^^{%n::nat. (#0::real)})" + "0 == Abs_hypreal(hyprel```{%n::nat. (#0::real)})" hypreal_one_def - "1hr == Abs_hypreal(hyprel^^{%n::nat. (#1::real)})" + "1hr == Abs_hypreal(hyprel```{%n::nat. (#1::real)})" (* an infinite number = [<1,2,3,...>] *) omega_def - "whr == Abs_hypreal(hyprel^^{%n::nat. real_of_nat (Suc n)})" + "whr == Abs_hypreal(hyprel```{%n::nat. real_of_nat (Suc n)})" (* an infinitesimal number = [<1,1/2,1/3,...>] *) epsilon_def - "ehr == Abs_hypreal(hyprel^^{%n::nat. inverse (real_of_nat (Suc n))})" + "ehr == Abs_hypreal(hyprel```{%n::nat. inverse (real_of_nat (Suc n))})" hypreal_minus_def - "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel^^{%n::nat. - (X n)})" + "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel```{%n::nat. - (X n)})" hypreal_diff_def "x - y == x + -(y::hypreal)" hypreal_inverse_def "inverse P == Abs_hypreal(UN X: Rep_hypreal(P). - hyprel^^{%n. if X n = #0 then #0 else inverse (X n)})" + hyprel```{%n. if X n = #0 then #0 else inverse (X n)})" hypreal_divide_def "P / Q::hypreal == P * inverse Q" @@ -66,17 +66,17 @@ constdefs hypreal_of_real :: real => hypreal - "hypreal_of_real r == Abs_hypreal(hyprel^^{%n::nat. r})" + "hypreal_of_real r == Abs_hypreal(hyprel```{%n::nat. r})" defs hypreal_add_def "P + Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q). - hyprel^^{%n::nat. X n + Y n})" + hyprel```{%n::nat. X n + Y n})" hypreal_mult_def "P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q). - hyprel^^{%n::nat. X n * Y n})" + hyprel```{%n::nat. X n * Y n})" hypreal_less_def "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) & diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Hyperreal/HyperNat.ML --- a/src/HOL/Hyperreal/HyperNat.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Hyperreal/HyperNat.ML Fri Jan 05 18:48:18 2001 +0100 @@ -65,7 +65,7 @@ val equiv_hypnatrel_iff = [UNIV_I, UNIV_I] MRS (equiv_hypnatrel RS eq_equiv_class_iff); -Goalw [hypnat_def,hypnatrel_def,quotient_def] "hypnatrel^^{x}:hypnat"; +Goalw [hypnat_def,hypnatrel_def,quotient_def] "hypnatrel```{x}:hypnat"; by (Blast_tac 1); qed "hypnatrel_in_hypnat"; @@ -85,7 +85,7 @@ by (rtac Rep_hypnat_inverse 1); qed "inj_Rep_hypnat"; -Goalw [hypnatrel_def] "x: hypnatrel ^^ {x}"; +Goalw [hypnatrel_def] "x: hypnatrel ``` {x}"; by (Step_tac 1); by Auto_tac; qed "lemma_hypnatrel_refl"; @@ -121,7 +121,7 @@ qed "inj_hypnat_of_nat"; val [prem] = Goal - "(!!x. z = Abs_hypnat(hypnatrel^^{x}) ==> P) ==> P"; + "(!!x. z = Abs_hypnat(hypnatrel```{x}) ==> P) ==> P"; by (res_inst_tac [("x1","z")] (rewrite_rule [hypnat_def] Rep_hypnat RS quotientE) 1); by (dres_inst_tac [("f","Abs_hypnat")] arg_cong 1); @@ -133,14 +133,14 @@ Addition for hyper naturals: hypnat_add -----------------------------------------------------------*) Goalw [congruent2_def] - "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n + Y n})"; + "congruent2 hypnatrel (%X Y. hypnatrel```{%n. X n + Y n})"; by Safe_tac; by (ALLGOALS(Fuf_tac)); qed "hypnat_add_congruent2"; Goalw [hypnat_add_def] - "Abs_hypnat(hypnatrel^^{%n. X n}) + Abs_hypnat(hypnatrel^^{%n. Y n}) = \ -\ Abs_hypnat(hypnatrel^^{%n. X n + Y n})"; + "Abs_hypnat(hypnatrel```{%n. X n}) + Abs_hypnat(hypnatrel```{%n. Y n}) = \ +\ Abs_hypnat(hypnatrel```{%n. X n + Y n})"; by (asm_simp_tac (simpset() addsimps [[equiv_hypnatrel, hypnat_add_congruent2] MRS UN_equiv_class2]) 1); @@ -186,14 +186,14 @@ Subtraction for hyper naturals: hypnat_minus -----------------------------------------------------------*) Goalw [congruent2_def] - "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n - Y n})"; + "congruent2 hypnatrel (%X Y. hypnatrel```{%n. X n - Y n})"; by Safe_tac; by (ALLGOALS(Fuf_tac)); qed "hypnat_minus_congruent2"; Goalw [hypnat_minus_def] - "Abs_hypnat(hypnatrel^^{%n. X n}) - Abs_hypnat(hypnatrel^^{%n. Y n}) = \ -\ Abs_hypnat(hypnatrel^^{%n. X n - Y n})"; + "Abs_hypnat(hypnatrel```{%n. X n}) - Abs_hypnat(hypnatrel```{%n. Y n}) = \ +\ Abs_hypnat(hypnatrel```{%n. X n - Y n})"; by (asm_simp_tac (simpset() addsimps [[equiv_hypnatrel, hypnat_minus_congruent2] MRS UN_equiv_class2]) 1); @@ -273,14 +273,14 @@ Multiplication for hyper naturals: hypnat_mult -----------------------------------------------------------*) Goalw [congruent2_def] - "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n * Y n})"; + "congruent2 hypnatrel (%X Y. hypnatrel```{%n. X n * Y n})"; by Safe_tac; by (ALLGOALS(Fuf_tac)); qed "hypnat_mult_congruent2"; Goalw [hypnat_mult_def] - "Abs_hypnat(hypnatrel^^{%n. X n}) * Abs_hypnat(hypnatrel^^{%n. Y n}) = \ -\ Abs_hypnat(hypnatrel^^{%n. X n * Y n})"; + "Abs_hypnat(hypnatrel```{%n. X n}) * Abs_hypnat(hypnatrel```{%n. Y n}) = \ +\ Abs_hypnat(hypnatrel```{%n. X n * Y n})"; by (asm_simp_tac (simpset() addsimps [[equiv_hypnatrel,hypnat_mult_congruent2] MRS UN_equiv_class2]) 1); @@ -475,8 +475,8 @@ (* See comments in HYPER for corresponding thm *) Goalw [hypnat_less_def] - "(Abs_hypnat(hypnatrel^^{%n. X n}) < \ -\ Abs_hypnat(hypnatrel^^{%n. Y n})) = \ + "(Abs_hypnat(hypnatrel```{%n. X n}) < \ +\ Abs_hypnat(hypnatrel```{%n. Y n})) = \ \ ({n. X n < Y n} : FreeUltrafilterNat)"; by (auto_tac (claset() addSIs [lemma_hypnatrel_refl],simpset())); by (Fuf_tac 1); @@ -527,7 +527,7 @@ (*--------------------------------------------------------------------------------- Trichotomy of the hyper naturals --------------------------------------------------------------------------------*) -Goalw [hypnatrel_def] "EX x. x: hypnatrel ^^ {%n. 0}"; +Goalw [hypnatrel_def] "EX x. x: hypnatrel ``` {%n. 0}"; by (res_inst_tac [("x","%n. 0")] exI 1); by (Step_tac 1); by Auto_tac; @@ -620,8 +620,8 @@ (*------ hypnat le iff nat le a.e ------*) Goalw [hypnat_le_def,le_def] - "(Abs_hypnat(hypnatrel^^{%n. X n}) <= \ -\ Abs_hypnat(hypnatrel^^{%n. Y n})) = \ + "(Abs_hypnat(hypnatrel```{%n. X n}) <= \ +\ Abs_hypnat(hypnatrel```{%n. Y n})) = \ \ ({n. X n <= Y n} : FreeUltrafilterNat)"; by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem], simpset() addsimps [hypnat_less])); @@ -833,7 +833,7 @@ Existence of infinite hypernatural number ---------------------------------------------------------------------------------*) -Goal "hypnatrel^^{%n::nat. n} : hypnat"; +Goal "hypnatrel```{%n::nat. n} : hypnat"; by Auto_tac; qed "hypnat_omega"; @@ -1066,7 +1066,7 @@ "HNatInfinite = {N. ALL n:SNat. n < N}"; by (Step_tac 1); by (dres_inst_tac [("x","Abs_hypnat \ -\ (hypnatrel ^^ {%n. N})")] bspec 2); +\ (hypnatrel ``` {%n. N})")] bspec 2); by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); by (auto_tac (claset(),simpset() addsimps [hypnat_less_iff])); @@ -1215,14 +1215,14 @@ Embedding of the hypernaturals into the hyperreal --------------------------------------------------------------*) -Goal "(Ya : hyprel ^^{%n. f(n)}) = \ +Goal "(Ya : hyprel ```{%n. f(n)}) = \ \ ({n. f n = Ya n} : FreeUltrafilterNat)"; by Auto_tac; qed "lemma_hyprel_FUFN"; Goalw [hypreal_of_hypnat_def] - "hypreal_of_hypnat (Abs_hypnat(hypnatrel^^{%n. X n})) = \ -\ Abs_hypreal(hyprel ^^ {%n. real_of_nat (X n)})"; + "hypreal_of_hypnat (Abs_hypnat(hypnatrel```{%n. X n})) = \ +\ Abs_hypreal(hyprel ``` {%n. real_of_nat (X n)})"; by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); by (auto_tac (claset() addEs [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset], diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Hyperreal/HyperNat.thy --- a/src/HOL/Hyperreal/HyperNat.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Hyperreal/HyperNat.thy Fri Jan 05 18:48:18 2001 +0100 @@ -25,7 +25,7 @@ (* embedding the naturals in the hypernaturals *) hypnat_of_nat :: nat => hypnat - "hypnat_of_nat m == Abs_hypnat(hypnatrel^^{%n::nat. m})" + "hypnat_of_nat m == Abs_hypnat(hypnatrel```{%n::nat. m})" (* hypernaturals as members of the hyperreals; the set is defined as *) (* the nonstandard extension of set of naturals embedded in the reals *) @@ -39,7 +39,7 @@ (* explicit embedding of the hypernaturals in the hyperreals *) hypreal_of_hypnat :: hypnat => hypreal "hypreal_of_hypnat N == Abs_hypreal(UN X: Rep_hypnat(N). - hyprel^^{%n::nat. real_of_nat (X n)})" + hyprel```{%n::nat. real_of_nat (X n)})" defs @@ -53,23 +53,23 @@ (** hypernatural arithmetic **) - hypnat_zero_def "0 == Abs_hypnat(hypnatrel^^{%n::nat. 0})" - hypnat_one_def "1hn == Abs_hypnat(hypnatrel^^{%n::nat. 1})" + hypnat_zero_def "0 == Abs_hypnat(hypnatrel```{%n::nat. 0})" + hypnat_one_def "1hn == Abs_hypnat(hypnatrel```{%n::nat. 1})" (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *) - hypnat_omega_def "whn == Abs_hypnat(hypnatrel^^{%n::nat. n})" + hypnat_omega_def "whn == Abs_hypnat(hypnatrel```{%n::nat. n})" hypnat_add_def "P + Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q). - hypnatrel^^{%n::nat. X n + Y n})" + hypnatrel```{%n::nat. X n + Y n})" hypnat_mult_def "P * Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q). - hypnatrel^^{%n::nat. X n * Y n})" + hypnatrel```{%n::nat. X n * Y n})" hypnat_minus_def "P - Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q). - hypnatrel^^{%n::nat. X n - Y n})" + hypnatrel```{%n::nat. X n - Y n})" hypnat_less_def "P < (Q::hypnat) == EX X Y. X: Rep_hypnat(P) & diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Hyperreal/HyperPow.ML --- a/src/HOL/Hyperreal/HyperPow.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Hyperreal/HyperPow.ML Fri Jan 05 18:48:18 2001 +0100 @@ -178,7 +178,7 @@ simpset() addsimps [hypreal_mult_less_mono2])); qed_spec_mp "hrealpow_Suc_le"; -Goal "Abs_hypreal(hyprel^^{%n. X n}) ^ m = Abs_hypreal(hyprel^^{%n. (X n) ^ m})"; +Goal "Abs_hypreal(hyprel```{%n. X n}) ^ m = Abs_hypreal(hyprel```{%n. (X n) ^ m})"; by (induct_tac "m" 1); by (auto_tac (claset(), simpset() delsimps [one_eq_numeral_1] @@ -221,14 +221,14 @@ --------------------------------------------------------------*) Goalw [congruent_def] "congruent hyprel \ -\ (%X Y. hyprel^^{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})"; +\ (%X Y. hyprel```{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})"; by (safe_tac (claset() addSIs [ext])); by (ALLGOALS(Fuf_tac)); qed "hyperpow_congruent"; Goalw [hyperpow_def] - "Abs_hypreal(hyprel^^{%n. X n}) pow Abs_hypnat(hypnatrel^^{%n. Y n}) = \ -\ Abs_hypreal(hyprel^^{%n. X n ^ Y n})"; + "Abs_hypreal(hyprel```{%n. X n}) pow Abs_hypnat(hypnatrel```{%n. Y n}) = \ +\ Abs_hypreal(hyprel```{%n. X n ^ Y n})"; by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); by (auto_tac (claset() addSIs [lemma_hyprel_refl,bexI], simpset() addsimps [hyprel_in_hypreal RS diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Hyperreal/HyperPow.thy --- a/src/HOL/Hyperreal/HyperPow.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Hyperreal/HyperPow.thy Fri Jan 05 18:48:18 2001 +0100 @@ -32,5 +32,5 @@ hyperpow_def "(R::hypreal) pow (N::hypnat) == Abs_hypreal(UN X:Rep_hypreal(R). UN Y: Rep_hypnat(N). - hyprel^^{%n::nat. (X n) ^ (Y n)})" + hyprel```{%n::nat. (X n) ^ (Y n)})" end diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Hyperreal/Lim.ML --- a/src/HOL/Hyperreal/Lim.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Hyperreal/Lim.ML Fri Jan 05 18:48:18 2001 +0100 @@ -220,7 +220,7 @@ by (fold_tac [real_le_def]); by (dtac lemma_skolemize_LIM2 1); by (Step_tac 1); -by (dres_inst_tac [("x","Abs_hypreal(hyprel^^{X})")] spec 1); +by (dres_inst_tac [("x","Abs_hypreal(hyprel```{X})")] spec 1); by (asm_full_simp_tac (simpset() addsimps [starfun, hypreal_minus, hypreal_of_real_def,hypreal_add]) 1); @@ -726,8 +726,8 @@ by (fold_tac [real_le_def]); by (dtac lemma_skolemize_LIM2u 1); by (Step_tac 1); -by (dres_inst_tac [("x","Abs_hypreal(hyprel^^{X})")] spec 1); -by (dres_inst_tac [("x","Abs_hypreal(hyprel^^{Y})")] spec 1); +by (dres_inst_tac [("x","Abs_hypreal(hyprel```{X})")] spec 1); +by (dres_inst_tac [("x","Abs_hypreal(hyprel```{Y})")] spec 1); by (asm_full_simp_tac (simpset() addsimps [starfun, hypreal_minus,hypreal_add]) 1); by Auto_tac; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Hyperreal/NSA.ML --- a/src/HOL/Hyperreal/NSA.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Hyperreal/NSA.ML Fri Jan 05 18:48:18 2001 +0100 @@ -2059,7 +2059,7 @@ Omega is a member of HInfinite -----------------------------------------------*) -Goal "hyprel^^{%n::nat. real_of_nat (Suc n)} : hypreal"; +Goal "hyprel```{%n::nat. real_of_nat (Suc n)} : hypreal"; by Auto_tac; qed "hypreal_omega"; @@ -2192,7 +2192,7 @@ |X(n) - x| < 1/n ==> [] - hypreal_of_real x|: Infinitesimal -----------------------------------------------------*) Goal "ALL n. abs(X n + -x) < inverse(real_of_nat(Suc n)) \ -\ ==> Abs_hypreal(hyprel^^{X}) + -hypreal_of_real x : Infinitesimal"; +\ ==> Abs_hypreal(hyprel```{X}) + -hypreal_of_real x : Infinitesimal"; by (auto_tac (claset() addSIs [bexI] addDs [rename_numerals FreeUltrafilterNat_inverse_real_of_posnat, FreeUltrafilterNat_all,FreeUltrafilterNat_Int] @@ -2203,21 +2203,21 @@ qed "real_seq_to_hypreal_Infinitesimal"; Goal "ALL n. abs(X n + -x) < inverse(real_of_nat(Suc n)) \ -\ ==> Abs_hypreal(hyprel^^{X}) @= hypreal_of_real x"; +\ ==> Abs_hypreal(hyprel```{X}) @= hypreal_of_real x"; by (rtac (inf_close_minus_iff RS ssubst) 1); by (rtac (mem_infmal_iff RS subst) 1); by (etac real_seq_to_hypreal_Infinitesimal 1); qed "real_seq_to_hypreal_inf_close"; Goal "ALL n. abs(x + -X n) < inverse(real_of_nat(Suc n)) \ -\ ==> Abs_hypreal(hyprel^^{X}) @= hypreal_of_real x"; +\ ==> Abs_hypreal(hyprel```{X}) @= hypreal_of_real x"; by (asm_full_simp_tac (simpset() addsimps [abs_minus_add_cancel, real_seq_to_hypreal_inf_close]) 1); qed "real_seq_to_hypreal_inf_close2"; Goal "ALL n. abs(X n + -Y n) < inverse(real_of_nat(Suc n)) \ -\ ==> Abs_hypreal(hyprel^^{X}) + \ -\ -Abs_hypreal(hyprel^^{Y}) : Infinitesimal"; +\ ==> Abs_hypreal(hyprel```{X}) + \ +\ -Abs_hypreal(hyprel```{Y}) : Infinitesimal"; by (auto_tac (claset() addSIs [bexI] addDs [rename_numerals FreeUltrafilterNat_inverse_real_of_posnat, diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Hyperreal/NatStar.ML --- a/src/HOL/Hyperreal/NatStar.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Hyperreal/NatStar.ML Fri Jan 05 18:48:18 2001 +0100 @@ -188,15 +188,15 @@ qed "starfunNat2_n_starfunNat2"; Goalw [congruent_def] - "congruent hypnatrel (%X. hypnatrel^^{%n. f (X n)})"; + "congruent hypnatrel (%X. hypnatrel```{%n. f (X n)})"; by (safe_tac (claset())); by (ALLGOALS(Fuf_tac)); qed "starfunNat_congruent"; (* f::nat=>real *) Goalw [starfunNat_def] - "(*fNat* f) (Abs_hypnat(hypnatrel^^{%n. X n})) = \ -\ Abs_hypreal(hyprel ^^ {%n. f (X n)})"; + "(*fNat* f) (Abs_hypnat(hypnatrel```{%n. X n})) = \ +\ Abs_hypreal(hyprel ``` {%n. f (X n)})"; by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); by (simp_tac (simpset() addsimps [hyprel_in_hypreal RS Abs_hypreal_inverse]) 1); @@ -205,8 +205,8 @@ (* f::nat=>nat *) Goalw [starfunNat2_def] - "(*fNat2* f) (Abs_hypnat(hypnatrel^^{%n. X n})) = \ -\ Abs_hypnat(hypnatrel ^^ {%n. f (X n)})"; + "(*fNat2* f) (Abs_hypnat(hypnatrel```{%n. X n})) = \ +\ Abs_hypnat(hypnatrel ``` {%n. f (X n)})"; by (res_inst_tac [("f","Abs_hypnat")] arg_cong 1); by (simp_tac (simpset() addsimps [hypnatrel_in_hypnat RS Abs_hypnat_inverse, @@ -413,14 +413,14 @@ Internal functions - some redundancy with *fNat* now ---------------------------------------------------------*) Goalw [congruent_def] - "congruent hypnatrel (%X. hypnatrel^^{%n. f n (X n)})"; + "congruent hypnatrel (%X. hypnatrel```{%n. f n (X n)})"; by (safe_tac (claset())); by (ALLGOALS(Fuf_tac)); qed "starfunNat_n_congruent"; Goalw [starfunNat_n_def] - "(*fNatn* f) (Abs_hypnat(hypnatrel^^{%n. X n})) = \ -\ Abs_hypreal(hyprel ^^ {%n. f n (X n)})"; + "(*fNatn* f) (Abs_hypnat(hypnatrel```{%n. X n})) = \ +\ Abs_hypreal(hyprel ``` {%n. f n (X n)})"; by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); by Auto_tac; by (Ultra_tac 1); @@ -468,7 +468,7 @@ by (auto_tac (claset(), simpset() addsimps [starfunNat_n, hypreal_minus])); qed "starfunNat_n_minus"; -Goal "(*fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel ^^ {%i. f i n})"; +Goal "(*fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel ``` {%i. f i n})"; by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_def])); qed "starfunNat_n_eq"; Addsimps [starfunNat_n_eq]; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Hyperreal/NatStar.thy --- a/src/HOL/Hyperreal/NatStar.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Hyperreal/NatStar.thy Fri Jan 05 18:48:18 2001 +0100 @@ -23,10 +23,10 @@ (* star transform of functions f:Nat --> Real *) starfunNat :: (nat => real) => hypnat => hypreal ("*fNat* _" [80] 80) - "*fNat* f == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel^^{%n. f (X n)}))" + "*fNat* f == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel```{%n. f (X n)}))" starfunNat_n :: (nat => (nat => real)) => hypnat => hypreal ("*fNatn* _" [80] 80) - "*fNatn* F == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel^^{%n. (F n)(X n)}))" + "*fNatn* F == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel```{%n. (F n)(X n)}))" InternalNatFuns :: (hypnat => hypreal) set "InternalNatFuns == {X. EX F. X = *fNatn* F}" @@ -34,10 +34,10 @@ (* star transform of functions f:Nat --> Nat *) starfunNat2 :: (nat => nat) => hypnat => hypnat ("*fNat2* _" [80] 80) - "*fNat2* f == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel^^{%n. f (X n)}))" + "*fNat2* f == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel```{%n. f (X n)}))" starfunNat2_n :: (nat => (nat => nat)) => hypnat => hypnat ("*fNat2n* _" [80] 80) - "*fNat2n* F == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel^^{%n. (F n)(X n)}))" + "*fNat2n* F == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel```{%n. (F n)(X n)}))" InternalNatFuns2 :: (hypnat => hypnat) set "InternalNatFuns2 == {X. EX F. X = *fNat2n* F}" diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Hyperreal/SEQ.ML --- a/src/HOL/Hyperreal/SEQ.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Hyperreal/SEQ.ML Fri Jan 05 18:48:18 2001 +0100 @@ -141,7 +141,7 @@ (* thus, the sequence defines an infinite hypernatural! *) Goal "ALL n. n <= f n \ -\ ==> Abs_hypnat (hypnatrel ^^ {f}) : HNatInfinite"; +\ ==> Abs_hypnat (hypnatrel ``` {f}) : HNatInfinite"; by (auto_tac (claset(),simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff])); by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]); by (etac FreeUltrafilterNat_NSLIMSEQ 1); @@ -156,7 +156,7 @@ val lemmaLIM2 = result(); Goal "[| #0 < r; ALL n. r <= abs (X (f n) + - L); \ -\ (*fNat* X) (Abs_hypnat (hypnatrel ^^ {f})) + \ +\ (*fNat* X) (Abs_hypnat (hypnatrel ``` {f})) + \ \ - hypreal_of_real L @= 0 |] ==> False"; by (auto_tac (claset(),simpset() addsimps [starfunNat, mem_infmal_iff RS sym,hypreal_of_real_def, @@ -178,7 +178,7 @@ by (Step_tac 1); (* skolemization step *) by (dtac choice 1 THEN Step_tac 1); -by (dres_inst_tac [("x","Abs_hypnat(hypnatrel^^{f})")] bspec 1); +by (dres_inst_tac [("x","Abs_hypnat(hypnatrel```{f})")] bspec 1); by (dtac (inf_close_minus_iff RS iffD1) 2); by (fold_tac [real_le_def]); by (blast_tac (claset() addIs [HNatInfinite_NSLIMSEQ]) 1); @@ -511,7 +511,7 @@ val lemmaNSBseq2 = result(); Goal "ALL N. real_of_nat(Suc N) < abs (X (f N)) \ -\ ==> Abs_hypreal(hyprel^^{X o f}) : HInfinite"; +\ ==> Abs_hypreal(hyprel```{X o f}) : HInfinite"; by (auto_tac (claset(), simpset() addsimps [HInfinite_FreeUltrafilterNat_iff,o_def])); by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]); @@ -542,7 +542,7 @@ val lemma_finite_NSBseq2 = result(); Goal "ALL N. real_of_nat(Suc N) < abs (X (f N)) \ -\ ==> Abs_hypnat(hypnatrel^^{f}) : HNatInfinite"; +\ ==> Abs_hypnat(hypnatrel```{f}) : HNatInfinite"; by (auto_tac (claset(), simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff])); by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]); @@ -795,7 +795,7 @@ (*------------------------------- Standard def => NS def -------------------------------*) -Goal "Abs_hypnat (hypnatrel ^^ {x}) : HNatInfinite \ +Goal "Abs_hypnat (hypnatrel ``` {x}) : HNatInfinite \ \ ==> {n. M <= x n} : FreeUltrafilterNat"; by (auto_tac (claset(), simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff])); @@ -843,7 +843,7 @@ step_tac (claset() addSDs [all_conj_distrib RS iffD1]) 1); by (REPEAT(dtac HNatInfinite_NSLIMSEQ 1)); by (dtac bspec 1 THEN assume_tac 1); -by (dres_inst_tac [("x","Abs_hypnat (hypnatrel ^^ {fa})")] bspec 1 +by (dres_inst_tac [("x","Abs_hypnat (hypnatrel ``` {fa})")] bspec 1 THEN auto_tac (claset(), simpset() addsimps [starfunNat])); by (dtac (inf_close_minus_iff RS iffD1) 1); by (dtac (mem_infmal_iff RS iffD2) 1); @@ -1334,7 +1334,7 @@ Hyperreals and Sequences ---------------------------------------------------------------***) (*** A bounded sequence is a finite hyperreal ***) -Goal "NSBseq X ==> Abs_hypreal(hyprel^^{X}) : HFinite"; +Goal "NSBseq X ==> Abs_hypreal(hyprel```{X}) : HFinite"; by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl] addIs [FreeUltrafilterNat_all RS FreeUltrafilterNat_subset], simpset() addsimps [HFinite_FreeUltrafilterNat_iff, @@ -1343,7 +1343,7 @@ (*** A sequence converging to zero defines an infinitesimal ***) Goalw [NSLIMSEQ_def] - "X ----NS> #0 ==> Abs_hypreal(hyprel^^{X}) : Infinitesimal"; + "X ----NS> #0 ==> Abs_hypreal(hyprel```{X}) : Infinitesimal"; by (dres_inst_tac [("x","whn")] bspec 1); by (simp_tac (simpset() addsimps [HNatInfinite_whn]) 1); by (auto_tac (claset(), diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Hyperreal/Star.ML --- a/src/HOL/Hyperreal/Star.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Hyperreal/Star.ML Fri Jan 05 18:48:18 2001 +0100 @@ -108,7 +108,7 @@ Goalw [starset_def] "ALL n. (X n) ~: M \ -\ ==> Abs_hypreal(hyprel^^{X}) ~: *s* M"; +\ ==> Abs_hypreal(hyprel```{X}) ~: *s* M"; by (Auto_tac THEN rtac bexI 1 THEN rtac lemma_hyprel_refl 2); by (Auto_tac); qed "STAR_real_seq_to_hypreal"; @@ -193,14 +193,14 @@ Nonstandard extension of functions- congruence -----------------------------------------------------------------------*) -Goalw [congruent_def] "congruent hyprel (%X. hyprel^^{%n. f (X n)})"; +Goalw [congruent_def] "congruent hyprel (%X. hyprel```{%n. f (X n)})"; by (safe_tac (claset())); by (ALLGOALS(Fuf_tac)); qed "starfun_congruent"; Goalw [starfun_def] - "(*f* f) (Abs_hypreal(hyprel^^{%n. X n})) = \ -\ Abs_hypreal(hyprel ^^ {%n. f (X n)})"; + "(*f* f) (Abs_hypreal(hyprel```{%n. X n})) = \ +\ Abs_hypreal(hyprel ``` {%n. f (X n)})"; by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); by (simp_tac (simpset() addsimps [hyprel_in_hypreal RS Abs_hypreal_inverse,[equiv_hyprel, @@ -417,8 +417,8 @@ applied entrywise to equivalence class representative. This is easily proved using starfun and ns extension thm ------------------------------------------------------------*) -Goal "abs (Abs_hypreal (hyprel ^^ {X})) = \ -\ Abs_hypreal(hyprel ^^ {%n. abs (X n)})"; +Goal "abs (Abs_hypreal (hyprel ``` {X})) = \ +\ Abs_hypreal(hyprel ``` {%n. abs (X n)})"; by (simp_tac (simpset() addsimps [starfun_rabs_hrabs RS sym,starfun]) 1); qed "hypreal_hrabs"; @@ -470,7 +470,7 @@ by (Fuf_tac 1); qed "Infinitesimal_FreeUltrafilterNat_iff2"; -Goal "(Abs_hypreal(hyprel^^{X}) @= Abs_hypreal(hyprel^^{Y})) = \ +Goal "(Abs_hypreal(hyprel```{X}) @= Abs_hypreal(hyprel```{Y})) = \ \ (ALL m. {n. abs (X n + - Y n) < \ \ inverse(real_of_nat(Suc m))} : FreeUltrafilterNat)"; by (rtac (inf_close_minus_iff RS ssubst) 1); @@ -485,6 +485,6 @@ Goal "inj starfun"; by (rtac injI 1); by (rtac ext 1 THEN rtac ccontr 1); -by (dres_inst_tac [("x","Abs_hypreal(hyprel ^^{%n. xa})")] fun_cong 1); +by (dres_inst_tac [("x","Abs_hypreal(hyprel ```{%n. xa})")] fun_cong 1); by (auto_tac (claset(),simpset() addsimps [starfun])); qed "inj_starfun"; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Hyperreal/Star.thy --- a/src/HOL/Hyperreal/Star.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Hyperreal/Star.thy Fri Jan 05 18:48:18 2001 +0100 @@ -25,11 +25,11 @@ ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))" starfun :: (real => real) => hypreal => hypreal ("*f* _" [80] 80) - "*f* f == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel^^{%n. f (X n)}))" + "*f* f == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel```{%n. f(X n)}))" (* internal functions *) starfun_n :: (nat => (real => real)) => hypreal => hypreal ("*fn* _" [80] 80) - "*fn* F == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel^^{%n. (F n)(X n)}))" + "*fn* F == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel```{%n. (F n)(X n)}))" InternalFuns :: (hypreal => hypreal) set "InternalFuns == {X. EX F. X = *fn* F}" diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Induct/Com.ML --- a/src/HOL/Induct/Com.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Induct/Com.ML Fri Jan 05 18:48:18 2001 +0100 @@ -30,15 +30,15 @@ Unify.search_bound := 60; (*Command execution is functional (deterministic) provided evaluation is*) -Goal "univalent ev ==> univalent(exec ev)"; -by (simp_tac (simpset() addsimps [univalent_def]) 1); +Goal "single_valued ev ==> single_valued(exec ev)"; +by (simp_tac (simpset() addsimps [single_valued_def]) 1); by (REPEAT (rtac allI 1)); by (rtac impI 1); by (etac exec.induct 1); by (Blast_tac 3); by (Blast_tac 1); -by (rewrite_goals_tac [univalent_def]); +by (rewrite_goals_tac [single_valued_def]); by (REPEAT (blast_tac (claset() addEs [exec_WHILE_case]) 1)); -qed "univalent_exec"; +qed "single_valued_exec"; Addsimps [fun_upd_same, fun_upd_other]; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Induct/Exp.ML --- a/src/HOL/Induct/Exp.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Induct/Exp.ML Fri Jan 05 18:48:18 2001 +0100 @@ -84,14 +84,14 @@ (*Expression evaluation is functional, or deterministic*) -Goalw [univalent_def] "univalent eval"; +Goalw [single_valued_def] "single_valued eval"; by (EVERY1[rtac allI, rtac allI, rtac impI]); by (split_all_tac 1); by (etac eval_induct 1); by (dtac com_Unique 4); by (ALLGOALS Full_simp_tac); by (ALLGOALS Blast_tac); -qed "univalent_eval"; +qed "single_valued_eval"; Goal "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)"; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Integ/Equiv.ML --- a/src/HOL/Integ/Equiv.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Integ/Equiv.ML Fri Jan 05 18:48:18 2001 +0100 @@ -37,33 +37,33 @@ (*Lemma for the next result*) Goalw [equiv_def,trans_def,sym_def] - "[| equiv A r; (a,b): r |] ==> r^^{a} <= r^^{b}"; + "[| equiv A r; (a,b): r |] ==> r```{a} <= r```{b}"; by (Blast_tac 1); qed "equiv_class_subset"; -Goal "[| equiv A r; (a,b): r |] ==> r^^{a} = r^^{b}"; +Goal "[| equiv A r; (a,b): r |] ==> r```{a} = r```{b}"; by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1)); by (rewrite_goals_tac [equiv_def,sym_def]); by (Blast_tac 1); qed "equiv_class_eq"; -Goalw [equiv_def,refl_def] "[| equiv A r; a: A |] ==> a: r^^{a}"; +Goalw [equiv_def,refl_def] "[| equiv A r; a: A |] ==> a: r```{a}"; by (Blast_tac 1); qed "equiv_class_self"; (*Lemma for the next result*) Goalw [equiv_def,refl_def] - "[| equiv A r; r^^{b} <= r^^{a}; b: A |] ==> (a,b): r"; + "[| equiv A r; r```{b} <= r```{a}; b: A |] ==> (a,b): r"; by (Blast_tac 1); qed "subset_equiv_class"; -Goal "[| r^^{a} = r^^{b}; equiv A r; b: A |] ==> (a,b): r"; +Goal "[| r```{a} = r```{b}; equiv A r; b: A |] ==> (a,b): r"; by (REPEAT (ares_tac [equalityD2, subset_equiv_class] 1)); qed "eq_equiv_class"; -(*thus r^^{a} = r^^{b} as well*) +(*thus r```{a} = r```{b} as well*) Goalw [equiv_def,trans_def,sym_def] - "[| equiv A r; x: (r^^{a} Int r^^{b}) |] ==> (a,b): r"; + "[| equiv A r; x: (r```{a} Int r```{b}) |] ==> (a,b): r"; by (Blast_tac 1); qed "equiv_class_nondisjoint"; @@ -71,12 +71,12 @@ by (Blast_tac 1); qed "equiv_type"; -Goal "equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)"; +Goal "equiv A r ==> ((x,y): r) = (r```{x} = r```{y} & x:A & y:A)"; by (blast_tac (claset() addSIs [equiv_class_eq] addDs [eq_equiv_class, equiv_type]) 1); qed "equiv_class_eq_iff"; -Goal "[| equiv A r; x: A; y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)"; +Goal "[| equiv A r; x: A; y: A |] ==> (r```{x} = r```{y}) = ((x,y): r)"; by (blast_tac (claset() addSIs [equiv_class_eq] addDs [eq_equiv_class, equiv_type]) 1); qed "eq_equiv_class_iff"; @@ -85,12 +85,12 @@ (** Introduction/elimination rules -- needed? **) -Goalw [quotient_def] "x:A ==> r^^{x}: A//r"; +Goalw [quotient_def] "x:A ==> r```{x}: A//r"; by (Blast_tac 1); qed "quotientI"; val [major,minor] = Goalw [quotient_def] - "[| X:(A//r); !!x. [| X = r^^{x}; x:A |] ==> P |] \ + "[| X:(A//r); !!x. [| X = r```{x}; x:A |] ==> P |] \ \ ==> P"; by (resolve_tac [major RS UN_E] 1); by (rtac minor 1); @@ -127,7 +127,7 @@ (*Conversion rule*) Goal "[| equiv A r; congruent r b; a: A |] \ -\ ==> (UN x:r^^{a}. b(x)) = b(a)"; +\ ==> (UN x:r```{a}. b(x)) = b(a)"; by (rtac (equiv_class_self RS UN_constant_eq) 1 THEN REPEAT (assume_tac 1)); by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]); by (blast_tac (claset() delrules [equalityI]) 1); @@ -171,7 +171,7 @@ Goalw [congruent_def] "[| equiv A r; congruent2 r b; a: A |] ==> \ -\ congruent r (%x1. UN x2:r^^{a}. b x1 x2)"; +\ congruent r (%x1. UN x2:r```{a}. b x1 x2)"; by (Clarify_tac 1); by (rtac (equiv_type RS subsetD RS SigmaE2) 1 THEN REPEAT (assume_tac 1)); by (asm_simp_tac (simpset() addsimps [UN_equiv_class, @@ -181,7 +181,7 @@ qed "congruent2_implies_congruent_UN"; Goal "[| equiv A r; congruent2 r b; a1: A; a2: A |] \ -\ ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2"; +\ ==> (UN x1:r```{a1}. UN x2:r```{a2}. b x1 x2) = b a1 a2"; by (asm_simp_tac (simpset() addsimps [UN_equiv_class, congruent2_implies_congruent, congruent2_implies_congruent_UN]) 1); diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Integ/Equiv.thy --- a/src/HOL/Integ/Equiv.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Integ/Equiv.thy Fri Jan 05 18:48:18 2001 +0100 @@ -12,7 +12,7 @@ "equiv A r == refl A r & sym(r) & trans(r)" quotient :: "['a set, ('a*'a) set] => 'a set set" (infixl "'/'/" 90) - "A//r == UN x:A. {r^^{x}}" (*set of equiv classes*) + "A//r == UN x:A. {r```{x}}" (*set of equiv classes*) congruent :: "[('a*'a) set, 'a=>'b] => bool" "congruent r b == ALL y z. (y,z):r --> b(y)=b(z)" diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Integ/IntDef.ML --- a/src/HOL/Integ/IntDef.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Integ/IntDef.ML Fri Jan 05 18:48:18 2001 +0100 @@ -23,7 +23,7 @@ [equiv_intrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff); Goalw [Integ_def,intrel_def,quotient_def] - "intrel^^{(x,y)}:Integ"; + "intrel```{(x,y)}:Integ"; by (Fast_tac 1); qed "intrel_in_integ"; @@ -58,18 +58,18 @@ (**** zminus: unary negation on Integ ****) Goalw [congruent_def, intrel_def] - "congruent intrel (%(x,y). intrel^^{(y,x)})"; + "congruent intrel (%(x,y). intrel```{(y,x)})"; by (auto_tac (claset(), simpset() addsimps add_ac)); qed "zminus_congruent"; Goalw [zminus_def] - "- Abs_Integ(intrel^^{(x,y)}) = Abs_Integ(intrel ^^ {(y,x)})"; + "- Abs_Integ(intrel```{(x,y)}) = Abs_Integ(intrel ``` {(y,x)})"; by (simp_tac (simpset() addsimps [equiv_intrel RS UN_equiv_class, zminus_congruent]) 1); qed "zminus"; (*Every integer can be written in the form Abs_Integ(...) *) -val [prem] = Goal "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P"; +val [prem] = Goal "(!!x y. z = Abs_Integ(intrel```{(x,y)}) ==> P) ==> P"; by (res_inst_tac [("x1","z")] (rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1); by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1); @@ -114,8 +114,8 @@ (**** zadd: addition on Integ ****) Goalw [zadd_def] - "Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \ -\ Abs_Integ(intrel^^{(x1+x2, y1+y2)})"; + "Abs_Integ(intrel```{(x1,y1)}) + Abs_Integ(intrel```{(x2,y2)}) = \ +\ Abs_Integ(intrel```{(x1+x2, y1+y2)})"; by (asm_simp_tac (simpset() addsimps [UN_UN_split_split_eq]) 1); by (stac (equiv_intrel RS UN_equiv_class2) 1); by (auto_tac (claset(), simpset() addsimps [congruent2_def])); @@ -232,7 +232,7 @@ (*Congruence property for multiplication*) Goal "congruent2 intrel \ \ (%p1 p2. (%(x1,y1). (%(x2,y2). \ -\ intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"; +\ intrel```{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"; by (rtac (equiv_intrel RS congruent2_commuteI) 1); by (pair_tac "w" 2); by (ALLGOALS Clarify_tac); @@ -249,8 +249,8 @@ qed "zmult_congruent2"; Goalw [zmult_def] - "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) = \ -\ Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})"; + "Abs_Integ((intrel```{(x1,y1)})) * Abs_Integ((intrel```{(x2,y2)})) = \ +\ Abs_Integ(intrel ``` {(x1*x2 + y1*y2, x1*y2 + y1*x2)})"; by (asm_simp_tac (simpset() addsimps [UN_UN_split_split_eq, zmult_congruent2, equiv_intrel RS UN_equiv_class2]) 1); diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Integ/IntDef.thy Fri Jan 05 18:48:18 2001 +0100 @@ -19,12 +19,12 @@ defs zminus_def - "- Z == Abs_Integ(UN (x,y):Rep_Integ(Z). intrel^^{(y,x)})" + "- Z == Abs_Integ(UN (x,y):Rep_Integ(Z). intrel```{(y,x)})" constdefs int :: nat => int - "int m == Abs_Integ(intrel ^^ {(m,0)})" + "int m == Abs_Integ(intrel ``` {(m,0)})" neg :: int => bool "neg(Z) == EX x y. x ('a,'s set)da "nae2da A == ({start A}, - %a Q. Union(next A (Some a) `` ((eps A)^* ^^ Q)), - %Q. ? p: (eps A)^* ^^ Q. fin A p)" + %a Q. Union(next A (Some a) `` ((eps A)^* ``` Q)), + %Q. ? p: (eps A)^* ``` Q. fin A p)" end diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Lex/NAe.thy --- a/src/HOL/Lex/NAe.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Lex/NAe.thy Fri Jan 05 18:48:18 2001 +0100 @@ -25,7 +25,7 @@ (* not really used: consts delta :: "('a,'s)nae => 'a list => 's => 's set" primrec -"delta A [] s = (eps A)^* ^^ {s}" -"delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* ^^ {s}))" +"delta A [] s = (eps A)^* ``` {s}" +"delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* ``` {s}))" *) end diff -r c0bcea781b3a -r 028d22926a41 src/HOL/MicroJava/BV/JType.thy --- a/src/HOL/MicroJava/BV/JType.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/MicroJava/BV/JType.thy Fri Jan 05 18:48:18 2001 +0100 @@ -151,7 +151,7 @@ done lemma closed_err_types: - "[| wf_prog wf_mb G; univalent (subcls1 G); acyclic (subcls1 G) |] + "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) |] ==> closed (err (types G)) (lift2 (sup G))" apply (unfold closed_def plussub_def lift2_def sup_def) apply (auto split: err.split) @@ -163,17 +163,17 @@ lemma err_semilat_JType_esl_lemma: - "[| wf_prog wf_mb G; univalent (subcls1 G); acyclic (subcls1 G) |] + "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) |] ==> err_semilat (esl G)" proof - assume wf_prog: "wf_prog wf_mb G" - assume univalent: "univalent (subcls1 G)" + assume single_valued: "single_valued (subcls1 G)" assume acyclic: "acyclic (subcls1 G)" hence "order (subtype G)" by (rule order_widen) moreover - from wf_prog univalent acyclic + from wf_prog single_valued acyclic have "closed (err (types G)) (lift2 (sup G))" by (rule closed_err_types) moreover @@ -185,10 +185,10 @@ "G \ c1 \C Object" "G \ c2 \C Object" by (blast intro: subcls_C_Object) - with wf_prog univalent + with wf_prog single_valued obtain u where "is_lub ((subcls1 G)^* ) c1 c2 u" - by (blast dest: univalent_has_lubs) + by (blast dest: single_valued_has_lubs) with acyclic have "G \ c1 \C some_lub ((subcls1 G)^* ) c1 c2" by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD) @@ -214,10 +214,10 @@ "G \ c1 \C Object" "G \ c2 \C Object" by (blast intro: subcls_C_Object) - with wf_prog univalent + with wf_prog single_valued obtain u where "is_lub ((subcls1 G)^* ) c2 c1 u" - by (blast dest: univalent_has_lubs) + by (blast dest: single_valued_has_lubs) with acyclic have "G \ c1 \C some_lub ((subcls1 G)^* ) c2 c1" by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD) @@ -242,10 +242,10 @@ "G \ c1 \C Object" "G \ c2 \C Object" by (blast intro: subcls_C_Object) - with wf_prog univalent + with wf_prog single_valued obtain u where lub: "is_lub ((subcls1 G)^* ) c1 c2 u" - by (blast dest: univalent_has_lubs) + by (blast dest: single_valued_has_lubs) with acyclic have "some_lub ((subcls1 G)^* ) c1 c2 = u" by (rule some_lub_conv) @@ -281,14 +281,14 @@ by (unfold esl_def semilat_def sl_def) auto qed -lemma univalent_subcls1: - "wf_prog wf_mb G ==> univalent (subcls1 G)" - by (unfold wf_prog_def unique_def univalent_def subcls1_def) auto +lemma single_valued_subcls1: + "wf_prog wf_mb G ==> single_valued (subcls1 G)" + by (unfold wf_prog_def unique_def single_valued_def subcls1_def) auto ML_setup {* bind_thm ("acyclic_subcls1", acyclic_subcls1) *} theorem err_semilat_JType_esl: "wf_prog wf_mb G ==> err_semilat (esl G)" - by (frule acyclic_subcls1, frule univalent_subcls1, rule err_semilat_JType_esl_lemma) + by (frule acyclic_subcls1, frule single_valued_subcls1, rule err_semilat_JType_esl_lemma) end diff -r c0bcea781b3a -r 028d22926a41 src/HOL/MicroJava/BV/Semilat.thy --- a/src/HOL/MicroJava/BV/Semilat.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/MicroJava/BV/Semilat.thy Fri Jan 05 18:48:18 2001 +0100 @@ -193,23 +193,23 @@ lemma extend_lub: - "[| univalent r; is_lub (r^* ) x y u; (x',x) : r |] + "[| single_valued r; is_lub (r^* ) x y u; (x',x) : r |] ==> EX v. is_lub (r^* ) x' y v" apply (unfold is_lub_def is_ub_def) apply (case_tac "(y,x) : r^*") apply (case_tac "(y,x') : r^*") apply blast apply (blast intro: r_into_rtrancl elim: converse_rtranclE - dest: univalentD) + dest: single_valuedD) apply (rule exI) apply (rule conjI) - apply (blast intro: rtrancl_into_rtrancl2 dest: univalentD) + apply (blast intro: rtrancl_into_rtrancl2 dest: single_valuedD) apply (blast intro: rtrancl_into_rtrancl rtrancl_into_rtrancl2 - elim: converse_rtranclE dest: univalentD) + elim: converse_rtranclE dest: single_valuedD) done -lemma univalent_has_lubs [rule_format]: - "[| univalent r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> +lemma single_valued_has_lubs [rule_format]: + "[| single_valued r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> (EX z. is_lub (r^* ) x y z))" apply (erule converse_rtrancl_induct) apply clarify @@ -228,8 +228,8 @@ done lemma is_lub_some_lub: - "[| univalent r; acyclic r; (x,u):r^*; (y,u):r^* |] + "[| single_valued r; acyclic r; (x,u):r^*; (y,u):r^* |] ==> is_lub (r^* ) x y (some_lub (r^* ) x y)"; - by (fastsimp dest: univalent_has_lubs simp add: some_lub_conv) + by (fastsimp dest: single_valued_has_lubs simp add: some_lub_conv) end diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Real/PRat.ML --- a/src/HOL/Real/PRat.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Real/PRat.ML Fri Jan 05 18:48:18 2001 +0100 @@ -61,7 +61,7 @@ bind_thm ("equiv_ratrel_iff", [equiv_ratrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff); -Goalw [prat_def,ratrel_def,quotient_def] "ratrel^^{(x,y)}:prat"; +Goalw [prat_def,ratrel_def,quotient_def] "ratrel```{(x,y)}:prat"; by (Blast_tac 1); qed "ratrel_in_prat"; @@ -95,7 +95,7 @@ qed "inj_prat_of_pnat"; val [prem] = Goal - "(!!x y. z = Abs_prat(ratrel^^{(x,y)}) ==> P) ==> P"; + "(!!x y. z = Abs_prat(ratrel```{(x,y)}) ==> P) ==> P"; by (res_inst_tac [("x1","z")] (rewrite_rule [prat_def] Rep_prat RS quotientE) 1); by (dres_inst_tac [("f","Abs_prat")] arg_cong 1); @@ -106,12 +106,12 @@ (**** qinv: inverse on prat ****) -Goalw [congruent_def] "congruent ratrel (%(x,y). ratrel^^{(y,x)})"; +Goalw [congruent_def] "congruent ratrel (%(x,y). ratrel```{(y,x)})"; by (auto_tac (claset(), simpset() addsimps [pnat_mult_commute])); qed "qinv_congruent"; Goalw [qinv_def] - "qinv (Abs_prat(ratrel^^{(x,y)})) = Abs_prat(ratrel ^^ {(y,x)})"; + "qinv (Abs_prat(ratrel```{(x,y)})) = Abs_prat(ratrel ``` {(y,x)})"; by (simp_tac (simpset() addsimps [equiv_ratrel RS UN_equiv_class, qinv_congruent]) 1); qed "qinv"; @@ -145,7 +145,7 @@ qed "prat_add_congruent2_lemma"; Goal "congruent2 ratrel (%p1 p2. \ -\ (%(x1,y1). (%(x2,y2). ratrel^^{(x1*y2 + x2*y1, y1*y2)}) p2) p1)"; +\ (%(x1,y1). (%(x2,y2). ratrel```{(x1*y2 + x2*y1, y1*y2)}) p2) p1)"; by (rtac (equiv_ratrel RS congruent2_commuteI) 1); by (auto_tac (claset() delrules [equalityI], simpset() addsimps [prat_add_congruent2_lemma])); @@ -153,8 +153,8 @@ qed "prat_add_congruent2"; Goalw [prat_add_def] - "Abs_prat((ratrel^^{(x1,y1)})) + Abs_prat((ratrel^^{(x2,y2)})) = \ -\ Abs_prat(ratrel ^^ {(x1*y2 + x2*y1, y1*y2)})"; + "Abs_prat((ratrel```{(x1,y1)})) + Abs_prat((ratrel```{(x2,y2)})) = \ +\ Abs_prat(ratrel ``` {(x1*y2 + x2*y1, y1*y2)})"; by (simp_tac (simpset() addsimps [UN_UN_split_split_eq, prat_add_congruent2, equiv_ratrel RS UN_equiv_class2]) 1); qed "prat_add"; @@ -189,7 +189,7 @@ Goalw [congruent2_def] "congruent2 ratrel (%p1 p2. \ -\ (%(x1,y1). (%(x2,y2). ratrel^^{(x1*x2, y1*y2)}) p2) p1)"; +\ (%(x1,y1). (%(x2,y2). ratrel```{(x1*x2, y1*y2)}) p2) p1)"; (*Proof via congruent2_commuteI seems longer*) by (Clarify_tac 1); by (asm_simp_tac (simpset() addsimps [pnat_mult_assoc]) 1); @@ -200,8 +200,8 @@ qed "pnat_mult_congruent2"; Goalw [prat_mult_def] - "Abs_prat(ratrel^^{(x1,y1)}) * Abs_prat(ratrel^^{(x2,y2)}) = \ -\ Abs_prat(ratrel^^{(x1*x2, y1*y2)})"; + "Abs_prat(ratrel```{(x1,y1)}) * Abs_prat(ratrel```{(x2,y2)}) = \ +\ Abs_prat(ratrel```{(x1*x2, y1*y2)})"; by (asm_simp_tac (simpset() addsimps [UN_UN_split_split_eq, pnat_mult_congruent2, equiv_ratrel RS UN_equiv_class2]) 1); @@ -389,7 +389,7 @@ Goal "!(q::prat). EX x. x + x = q"; by (rtac allI 1); by (res_inst_tac [("z","q")] eq_Abs_prat 1); -by (res_inst_tac [("x","Abs_prat (ratrel ^^ {(x, y+y)})")] exI 1); +by (res_inst_tac [("x","Abs_prat (ratrel ``` {(x, y+y)})")] exI 1); by (auto_tac (claset(), simpset() addsimps [prat_add,pnat_mult_assoc RS sym,pnat_add_mult_distrib, @@ -398,7 +398,7 @@ Goal "EX (x::prat). x + x = q"; by (res_inst_tac [("z","q")] eq_Abs_prat 1); -by (res_inst_tac [("x","Abs_prat (ratrel ^^ {(x, y+y)})")] exI 1); +by (res_inst_tac [("x","Abs_prat (ratrel ``` {(x, y+y)})")] exI 1); by (auto_tac (claset(),simpset() addsimps [prat_add,pnat_mult_assoc RS sym,pnat_add_mult_distrib, pnat_add_mult_distrib2])); @@ -454,7 +454,7 @@ (* lemma for proving $< is linear *) Goalw [prat_def,prat_less_def] - "ratrel ^^ {(x, y * ya)} : {p::(pnat*pnat).True}//ratrel"; + "ratrel ``` {(x, y * ya)} : {p::(pnat*pnat).True}//ratrel"; by (asm_full_simp_tac (simpset() addsimps [ratrel_def,quotient_def]) 1); by (Blast_tac 1); qed "lemma_prat_less_linear"; @@ -470,15 +470,15 @@ by (cut_inst_tac [("z1.0","x*ya"), ("z2.0","xa*y")] pnat_linear_Ex_eq 1); by (EVERY1[etac disjE,etac exE]); by (eres_inst_tac - [("x","Abs_prat(ratrel^^{(xb,ya*y)})")] allE 1); + [("x","Abs_prat(ratrel```{(xb,ya*y)})")] allE 1); by (asm_full_simp_tac (simpset() addsimps [prat_add, pnat_mult_assoc RS sym,pnat_add_mult_distrib RS sym]) 1); by (EVERY1[asm_full_simp_tac (simpset() addsimps pnat_mult_ac), etac disjE, assume_tac, etac exE]); -by (thin_tac "!T. Abs_prat (ratrel ^^ {(x, y)}) + T ~= \ -\ Abs_prat (ratrel ^^ {(xa, ya)})" 1); -by (eres_inst_tac [("x","Abs_prat(ratrel^^{(xb,y*ya)})")] allE 1); +by (thin_tac "!T. Abs_prat (ratrel ``` {(x, y)}) + T ~= \ +\ Abs_prat (ratrel ``` {(xa, ya)})" 1); +by (eres_inst_tac [("x","Abs_prat(ratrel```{(xb,y*ya)})")] allE 1); by (asm_full_simp_tac (simpset() addsimps [prat_add, pnat_mult_assoc RS sym,pnat_add_mult_distrib RS sym]) 1); by (asm_full_simp_tac (simpset() addsimps pnat_mult_ac) 1); @@ -696,12 +696,12 @@ (*** lemmas required for lemma_gleason9_34 in PReal : w*y > y/z ***) Goalw [prat_of_pnat_def] - "Abs_prat(ratrel^^{(x,y)}) = (prat_of_pnat x)*qinv(prat_of_pnat y)"; + "Abs_prat(ratrel```{(x,y)}) = (prat_of_pnat x)*qinv(prat_of_pnat y)"; by (auto_tac (claset(),simpset() addsimps [prat_mult,qinv,pnat_mult_1_left, pnat_mult_1])); qed "Abs_prat_mult_qinv"; -Goal "Abs_prat(ratrel^^{(x,y)}) <= Abs_prat(ratrel^^{(x,Abs_pnat 1)})"; +Goal "Abs_prat(ratrel```{(x,y)}) <= Abs_prat(ratrel```{(x,Abs_pnat 1)})"; by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1); by (rtac prat_mult_left_le2_mono1 1); by (rtac qinv_prat_le 1); @@ -713,7 +713,7 @@ pSuc_is_plus_one,pnat_one_def,prat_of_pnat_add])); qed "lemma_Abs_prat_le1"; -Goal "Abs_prat(ratrel^^{(x,Abs_pnat 1)}) <= Abs_prat(ratrel^^{(x*y,Abs_pnat 1)})"; +Goal "Abs_prat(ratrel```{(x,Abs_pnat 1)}) <= Abs_prat(ratrel```{(x*y,Abs_pnat 1)})"; by (simp_tac (simpset() addsimps [Abs_prat_mult_qinv]) 1); by (rtac prat_mult_le2_mono1 1); by (pnat_ind_tac "y" 1); @@ -726,19 +726,19 @@ prat_of_pnat_add,prat_of_pnat_mult])); qed "lemma_Abs_prat_le2"; -Goal "Abs_prat(ratrel^^{(x,z)}) <= Abs_prat(ratrel^^{(x*y,Abs_pnat 1)})"; +Goal "Abs_prat(ratrel```{(x,z)}) <= Abs_prat(ratrel```{(x*y,Abs_pnat 1)})"; by (fast_tac (claset() addIs [prat_le_trans, lemma_Abs_prat_le1,lemma_Abs_prat_le2]) 1); qed "lemma_Abs_prat_le3"; -Goal "Abs_prat(ratrel^^{(x*y,Abs_pnat 1)}) * Abs_prat(ratrel^^{(w,x)}) = \ -\ Abs_prat(ratrel^^{(w*y,Abs_pnat 1)})"; +Goal "Abs_prat(ratrel```{(x*y,Abs_pnat 1)}) * Abs_prat(ratrel```{(w,x)}) = \ +\ Abs_prat(ratrel```{(w*y,Abs_pnat 1)})"; by (full_simp_tac (simpset() addsimps [prat_mult, pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac) 1); qed "pre_lemma_gleason9_34"; -Goal "Abs_prat(ratrel^^{(y*x,Abs_pnat 1*y)}) = \ -\ Abs_prat(ratrel^^{(x,Abs_pnat 1)})"; +Goal "Abs_prat(ratrel```{(y*x,Abs_pnat 1*y)}) = \ +\ Abs_prat(ratrel```{(x,Abs_pnat 1)})"; by (auto_tac (claset(), simpset() addsimps [pnat_mult_1,pnat_mult_1_left] @ pnat_mult_ac)); qed "pre_lemma_gleason9_34b"; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Real/PRat.thy --- a/src/HOL/Real/PRat.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Real/PRat.thy Fri Jan 05 18:48:18 2001 +0100 @@ -20,20 +20,20 @@ constdefs prat_of_pnat :: pnat => prat - "prat_of_pnat m == Abs_prat(ratrel^^{(m,Abs_pnat 1)})" + "prat_of_pnat m == Abs_prat(ratrel```{(m,Abs_pnat 1)})" qinv :: prat => prat - "qinv(Q) == Abs_prat(UN (x,y):Rep_prat(Q). ratrel^^{(y,x)})" + "qinv(Q) == Abs_prat(UN (x,y):Rep_prat(Q). ratrel```{(y,x)})" defs prat_add_def "P + Q == Abs_prat(UN (x1,y1):Rep_prat(P). UN (x2,y2):Rep_prat(Q). - ratrel^^{(x1*y2 + x2*y1, y1*y2)})" + ratrel```{(x1*y2 + x2*y1, y1*y2)})" prat_mult_def "P * Q == Abs_prat(UN (x1,y1):Rep_prat(P). UN (x2,y2):Rep_prat(Q). - ratrel^^{(x1*x2, y1*y2)})" + ratrel```{(x1*x2, y1*y2)})" (*** Gleason p. 119 ***) prat_less_def diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Real/PReal.ML --- a/src/HOL/Real/PReal.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Real/PReal.ML Fri Jan 05 18:48:18 2001 +0100 @@ -582,10 +582,10 @@ prat_of_pnat_add,prat_add_assoc RS sym])); qed "lemma1_gleason9_34"; -Goal "Abs_prat (ratrel ^^ {(y, z)}) < xb + \ -\ Abs_prat (ratrel ^^ {(x*y, Abs_pnat 1)})*Abs_prat (ratrel ^^ {(w, x)})"; -by (res_inst_tac [("j","Abs_prat (ratrel ^^ {(x * y, Abs_pnat 1)}) *\ -\ Abs_prat (ratrel ^^ {(w, x)})")] prat_le_less_trans 1); +Goal "Abs_prat (ratrel ``` {(y, z)}) < xb + \ +\ Abs_prat (ratrel ``` {(x*y, Abs_pnat 1)})*Abs_prat (ratrel ``` {(w, x)})"; +by (res_inst_tac [("j","Abs_prat (ratrel ``` {(x * y, Abs_pnat 1)}) *\ +\ Abs_prat (ratrel ``` {(w, x)})")] prat_le_less_trans 1); by (rtac prat_self_less_add_right 2); by (auto_tac (claset() addIs [lemma_Abs_prat_le3], simpset() addsimps [prat_mult,pre_lemma_gleason9_34b,pnat_mult_assoc])); diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Real/RealDef.ML --- a/src/HOL/Real/RealDef.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Real/RealDef.ML Fri Jan 05 18:48:18 2001 +0100 @@ -57,11 +57,11 @@ addSEs [sym, preal_trans_lemma]) 1); qed "equiv_realrel"; -(* (realrel ^^ {x} = realrel ^^ {y}) = ((x,y) : realrel) *) +(* (realrel ``` {x} = realrel ``` {y}) = ((x,y) : realrel) *) bind_thm ("equiv_realrel_iff", [equiv_realrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff); -Goalw [real_def,realrel_def,quotient_def] "realrel^^{(x,y)}:real"; +Goalw [real_def,realrel_def,quotient_def] "realrel```{(x,y)}:real"; by (Blast_tac 1); qed "realrel_in_real"; @@ -95,7 +95,7 @@ qed "inj_real_of_preal"; val [prem] = Goal - "(!!x y. z = Abs_real(realrel^^{(x,y)}) ==> P) ==> P"; + "(!!x y. z = Abs_real(realrel```{(x,y)}) ==> P) ==> P"; by (res_inst_tac [("x1","z")] (rewrite_rule [real_def] Rep_real RS quotientE) 1); by (dres_inst_tac [("f","Abs_real")] arg_cong 1); @@ -107,13 +107,13 @@ (**** real_minus: additive inverse on real ****) Goalw [congruent_def] - "congruent realrel (%p. (%(x,y). realrel^^{(y,x)}) p)"; + "congruent realrel (%p. (%(x,y). realrel```{(y,x)}) p)"; by (Clarify_tac 1); by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1); qed "real_minus_congruent"; Goalw [real_minus_def] - "- (Abs_real(realrel^^{(x,y)})) = Abs_real(realrel ^^ {(y,x)})"; + "- (Abs_real(realrel```{(x,y)})) = Abs_real(realrel ``` {(y,x)})"; by (res_inst_tac [("f","Abs_real")] arg_cong 1); by (simp_tac (simpset() addsimps [realrel_in_real RS Abs_real_inverse, @@ -150,7 +150,7 @@ (*** Congruence property for addition ***) Goalw [congruent2_def] "congruent2 realrel (%p1 p2. \ -\ (%(x1,y1). (%(x2,y2). realrel^^{(x1+x2, y1+y2)}) p2) p1)"; +\ (%(x1,y1). (%(x2,y2). realrel```{(x1+x2, y1+y2)}) p2) p1)"; by (Clarify_tac 1); by (asm_simp_tac (simpset() addsimps [preal_add_assoc]) 1); by (res_inst_tac [("z1.1","x1a")] (preal_add_left_commute RS ssubst) 1); @@ -159,8 +159,8 @@ qed "real_add_congruent2"; Goalw [real_add_def] - "Abs_real(realrel^^{(x1,y1)}) + Abs_real(realrel^^{(x2,y2)}) = \ -\ Abs_real(realrel^^{(x1+x2, y1+y2)})"; + "Abs_real(realrel```{(x1,y1)}) + Abs_real(realrel```{(x2,y2)}) = \ +\ Abs_real(realrel```{(x1+x2, y1+y2)})"; by (simp_tac (simpset() addsimps [[equiv_realrel, real_add_congruent2] MRS UN_equiv_class2]) 1); qed "real_add"; @@ -301,7 +301,7 @@ Goal "congruent2 realrel (%p1 p2. \ -\ (%(x1,y1). (%(x2,y2). realrel^^{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)"; +\ (%(x1,y1). (%(x2,y2). realrel```{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)"; by (rtac (equiv_realrel RS congruent2_commuteI) 1); by (Clarify_tac 1); by (rewtac split_def); @@ -310,8 +310,8 @@ qed "real_mult_congruent2"; Goalw [real_mult_def] - "Abs_real((realrel^^{(x1,y1)})) * Abs_real((realrel^^{(x2,y2)})) = \ -\ Abs_real(realrel ^^ {(x1*x2+y1*y2,x1*y2+x2*y1)})"; + "Abs_real((realrel```{(x1,y1)})) * Abs_real((realrel```{(x2,y2)})) = \ +\ Abs_real(realrel ``` {(x1*x2+y1*y2,x1*y2+x2*y1)})"; by (simp_tac (simpset() addsimps [[equiv_realrel, real_mult_congruent2] MRS UN_equiv_class2]) 1); qed "real_mult"; @@ -451,7 +451,7 @@ (*** existence of inverse ***) (** lemma -- alternative definition of 0 **) -Goalw [real_zero_def] "0 = Abs_real (realrel ^^ {(x, x)})"; +Goalw [real_zero_def] "0 = Abs_real (realrel ``` {(x, x)})"; by (auto_tac (claset(),simpset() addsimps [preal_add_commute])); qed "real_zero_iff"; @@ -461,10 +461,10 @@ by (cut_inst_tac [("r1.0","xa"),("r2.0","y")] preal_linear 1); by (auto_tac (claset() addSDs [preal_less_add_left_Ex], simpset() addsimps [real_zero_iff RS sym])); -by (res_inst_tac [("x","Abs_real (realrel ^^ \ +by (res_inst_tac [("x","Abs_real (realrel ``` \ \ {(preal_of_prat(prat_of_pnat 1p),pinv(D)+\ \ preal_of_prat(prat_of_pnat 1p))})")] exI 1); -by (res_inst_tac [("x","Abs_real (realrel ^^ \ +by (res_inst_tac [("x","Abs_real (realrel ``` \ \ {(pinv(D)+preal_of_prat(prat_of_pnat 1p),\ \ preal_of_prat(prat_of_pnat 1p))})")] exI 2); by (auto_tac (claset(), @@ -716,13 +716,13 @@ Goalw [real_of_preal_def] "!!(x::preal). y < x ==> \ -\ EX m. Abs_real (realrel ^^ {(x,y)}) = real_of_preal m"; +\ EX m. Abs_real (realrel ``` {(x,y)}) = real_of_preal m"; by (auto_tac (claset() addSDs [preal_less_add_left_Ex], simpset() addsimps preal_add_ac)); qed "real_of_preal_ExI"; Goalw [real_of_preal_def] - "!!(x::preal). EX m. Abs_real (realrel ^^ {(x,y)}) = \ + "!!(x::preal). EX m. Abs_real (realrel ``` {(x,y)}) = \ \ real_of_preal m ==> y < x"; by (auto_tac (claset(), simpset() addsimps @@ -731,7 +731,7 @@ [preal_add_assoc RS sym,preal_self_less_add_left]) 1); qed "real_of_preal_ExD"; -Goal "(EX m. Abs_real (realrel ^^ {(x,y)}) = real_of_preal m) = (y < x)"; +Goal "(EX m. Abs_real (realrel ``` {(x,y)}) = real_of_preal m) = (y < x)"; by (blast_tac (claset() addSIs [real_of_preal_ExI,real_of_preal_ExD]) 1); qed "real_of_preal_iff"; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Real/RealDef.thy --- a/src/HOL/Real/RealDef.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Real/RealDef.thy Fri Jan 05 18:48:18 2001 +0100 @@ -31,14 +31,14 @@ defs real_zero_def - "0 == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p), + "0 == Abs_real(realrel```{(preal_of_prat(prat_of_pnat 1p), preal_of_prat(prat_of_pnat 1p))})" real_one_def - "1r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p) + + "1r == Abs_real(realrel```{(preal_of_prat(prat_of_pnat 1p) + preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})" real_minus_def - "- R == Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})" + "- R == Abs_real(UN (x,y):Rep_real(R). realrel```{(y,x)})" real_diff_def "R - (S::real) == R + - S" @@ -53,7 +53,7 @@ real_of_preal :: preal => real "real_of_preal m == - Abs_real(realrel^^{(m+preal_of_prat(prat_of_pnat 1p), + Abs_real(realrel```{(m+preal_of_prat(prat_of_pnat 1p), preal_of_prat(prat_of_pnat 1p))})" real_of_posnat :: nat => real @@ -66,11 +66,11 @@ real_add_def "P+Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q). - (%(x1,y1). (%(x2,y2). realrel^^{(x1+x2, y1+y2)}) p2) p1)" + (%(x1,y1). (%(x2,y2). realrel```{(x1+x2, y1+y2)}) p2) p1)" real_mult_def "P*Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q). - (%(x1,y1). (%(x2,y2). realrel^^{(x1*x2+y1*y2,x1*y2+x2*y1)}) + (%(x1,y1). (%(x2,y2). realrel```{(x1*x2+y1*y2,x1*y2+x2*y1)}) p2) p1)" real_less_def diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Real/RealInt.ML --- a/src/HOL/Real/RealInt.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Real/RealInt.ML Fri Jan 05 18:48:18 2001 +0100 @@ -7,7 +7,7 @@ Goalw [congruent_def] - "congruent intrel (%p. (%(i,j). realrel ^^ \ + "congruent intrel (%p. (%(i,j). realrel ``` \ \ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \ \ preal_of_prat (prat_of_pnat (pnat_of_nat j)))}) p)"; by (auto_tac (claset(), @@ -16,8 +16,8 @@ qed "real_of_int_congruent"; Goalw [real_of_int_def] - "real_of_int (Abs_Integ (intrel ^^ {(i, j)})) = \ -\ Abs_real(realrel ^^ \ + "real_of_int (Abs_Integ (intrel ``` {(i, j)})) = \ +\ Abs_real(realrel ``` \ \ {(preal_of_prat (prat_of_pnat (pnat_of_nat i)), \ \ preal_of_prat (prat_of_pnat (pnat_of_nat j)))})"; by (res_inst_tac [("f","Abs_real")] arg_cong 1); diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Real/RealInt.thy --- a/src/HOL/Real/RealInt.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Real/RealInt.thy Fri Jan 05 18:48:18 2001 +0100 @@ -9,7 +9,7 @@ constdefs real_of_int :: int => real - "real_of_int z == Abs_real(UN (i,j): Rep_Integ z. realrel ^^ + "real_of_int z == Abs_real(UN (i,j): Rep_Integ z. realrel ``` {(preal_of_prat(prat_of_pnat(pnat_of_nat i)), preal_of_prat(prat_of_pnat(pnat_of_nat j)))})" diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Relation.ML --- a/src/HOL/Relation.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Relation.ML Fri Jan 05 18:48:18 2001 +0100 @@ -333,27 +333,27 @@ overload_1st_set "Relation.Image"; -Goalw [Image_def] "b : r^^A = (? x:A. (x,b):r)"; +Goalw [Image_def] "b : r```A = (? x:A. (x,b):r)"; by (Blast_tac 1); qed "Image_iff"; -Goalw [Image_def] "r^^{a} = {b. (a,b):r}"; +Goalw [Image_def] "r```{a} = {b. (a,b):r}"; by (Blast_tac 1); qed "Image_singleton"; -Goal "(b : r^^{a}) = ((a,b):r)"; +Goal "(b : r```{a}) = ((a,b):r)"; by (rtac (Image_iff RS trans) 1); by (Blast_tac 1); qed "Image_singleton_iff"; AddIffs [Image_singleton_iff]; -Goalw [Image_def] "[| (a,b): r; a:A |] ==> b : r^^A"; +Goalw [Image_def] "[| (a,b): r; a:A |] ==> b : r```A"; by (Blast_tac 1); qed "ImageI"; val major::prems = Goalw [Image_def] - "[| b: r^^A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P"; + "[| b: r```A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P"; by (rtac (major RS CollectE) 1); by (Clarify_tac 1); by (rtac (hd prems) 1); @@ -364,72 +364,72 @@ AddSEs [ImageE]; (*This version's more effective when we already have the required "a"*) -Goal "[| a:A; (a,b): r |] ==> b : r^^A"; +Goal "[| a:A; (a,b): r |] ==> b : r```A"; by (Blast_tac 1); qed "rev_ImageI"; -Goal "R^^{} = {}"; +Goal "R```{} = {}"; by (Blast_tac 1); qed "Image_empty"; Addsimps [Image_empty]; -Goal "Id ^^ A = A"; +Goal "Id ``` A = A"; by (Blast_tac 1); qed "Image_Id"; -Goal "diag A ^^ B = A Int B"; +Goal "diag A ``` B = A Int B"; by (Blast_tac 1); qed "Image_diag"; Addsimps [Image_Id, Image_diag]; -Goal "R ^^ (A Int B) <= R ^^ A Int R ^^ B"; +Goal "R ``` (A Int B) <= R ``` A Int R ``` B"; by (Blast_tac 1); qed "Image_Int_subset"; -Goal "R ^^ (A Un B) = R ^^ A Un R ^^ B"; +Goal "R ``` (A Un B) = R ``` A Un R ``` B"; by (Blast_tac 1); qed "Image_Un"; -Goal "r <= A <*> B ==> r^^C <= B"; +Goal "r <= A <*> B ==> r```C <= B"; by (rtac subsetI 1); by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ; qed "Image_subset"; (*NOT suitable for rewriting*) -Goal "r^^B = (UN y: B. r^^{y})"; +Goal "r```B = (UN y: B. r```{y})"; by (Blast_tac 1); qed "Image_eq_UN"; -Goal "[| r'<=r; A'<=A |] ==> (r' ^^ A') <= (r ^^ A)"; +Goal "[| r'<=r; A'<=A |] ==> (r' ``` A') <= (r ``` A)"; by (Blast_tac 1); qed "Image_mono"; -Goal "(r ^^ (UNION A B)) = (UN x:A.(r ^^ (B x)))"; +Goal "(r ``` (UNION A B)) = (UN x:A.(r ``` (B x)))"; by (Blast_tac 1); qed "Image_UN"; (*Converse inclusion fails*) -Goal "(r ^^ (INTER A B)) <= (INT x:A.(r ^^ (B x)))"; +Goal "(r ``` (INTER A B)) <= (INT x:A.(r ``` (B x)))"; by (Blast_tac 1); qed "Image_INT_subset"; -Goal "(r^^A <= B) = (A <= - ((r^-1) ^^ (-B)))"; +Goal "(r```A <= B) = (A <= - ((r^-1) ``` (-B)))"; by (Blast_tac 1); qed "Image_subset_eq"; -section "univalent"; +section "single_valued"; -Goalw [univalent_def] - "!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> univalent r"; +Goalw [single_valued_def] + "!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> single_valued r"; by (assume_tac 1); -qed "univalentI"; +qed "single_valuedI"; -Goalw [univalent_def] - "[| univalent r; (x,y):r; (x,z):r|] ==> y=z"; +Goalw [single_valued_def] + "[| single_valued r; (x,y):r; (x,z):r|] ==> y=z"; by Auto_tac; -qed "univalentD"; +qed "single_valuedD"; (** Graphs given by Collect **) @@ -442,7 +442,7 @@ by Auto_tac; qed "Range_Collect_split"; -Goal "{(x,y). P x y} ^^ A = {y. EX x:A. P x y}"; +Goal "{(x,y). P x y} ``` A = {y. EX x:A. P x y}"; by Auto_tac; qed "Image_Collect_split"; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Relation.thy --- a/src/HOL/Relation.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Relation.thy Fri Jan 05 18:48:18 2001 +0100 @@ -16,8 +16,8 @@ comp :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr "O" 60) "r O s == {(x,z). ? y. (x,y):s & (y,z):r}" - Image :: "[('a*'b) set,'a set] => 'b set" (infixl "^^" 90) - "r ^^ s == {y. ? x:s. (x,y):r}" + Image :: "[('a*'b) set,'a set] => 'b set" (infixl "```" 90) + "r ``` s == {y. ? x:s. (x,y):r}" Id :: "('a * 'a)set" (*the identity relation*) "Id == {p. ? x. p = (x,x)}" @@ -46,8 +46,8 @@ trans :: "('a * 'a)set => bool" (*transitivity predicate*) "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)" - univalent :: "('a * 'b)set => bool" - "univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)" + single_valued :: "('a * 'b)set => bool" + "single_valued r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)" fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set" "fun_rel_comp f R == {g. !x. (f x, g x) : R}" diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Relation_Power.ML --- a/src/HOL/Relation_Power.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/Relation_Power.ML Fri Jan 05 18:48:18 2001 +0100 @@ -103,12 +103,12 @@ qed "rtrancl_is_UN_rel_pow"; -Goal "!!r::('a * 'a)set. univalent r ==> univalent (r^n)"; -by (rtac univalentI 1); +Goal "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)"; +by (rtac single_valuedI 1); by (induct_tac "n" 1); by (Simp_tac 1); -by (fast_tac (claset() addDs [univalentD] addEs [rel_pow_Suc_E]) 1); -qed_spec_mp "univalent_rel_pow"; +by (fast_tac (claset() addDs [single_valuedD] addEs [rel_pow_Suc_E]) 1); +qed_spec_mp "single_valued_rel_pow"; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/UNITY/Extend.ML --- a/src/HOL/UNITY/Extend.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/UNITY/Extend.ML Fri Jan 05 18:48:18 2001 +0100 @@ -58,7 +58,7 @@ by (Blast_tac 1); qed "Domain_Restrict"; -Goal "(Restrict A r) ^^ B = r ^^ (A Int B)"; +Goal "(Restrict A r) ``` B = r ``` (A Int B)"; by (Blast_tac 1); qed "Image_Restrict"; @@ -308,7 +308,7 @@ qed "inj_extend_act"; Goalw [extend_set_def, extend_act_def] - "extend_act h act ^^ (extend_set h A) = extend_set h (act ^^ A)"; + "extend_act h act ``` (extend_set h A) = extend_set h (act ``` A)"; by (Force_tac 1); qed "extend_act_Image"; Addsimps [extend_act_Image]; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/UNITY/FP.ML --- a/src/HOL/UNITY/FP.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/UNITY/FP.ML Fri Jan 05 18:48:18 2001 +0100 @@ -49,11 +49,11 @@ qed "FP_weakest"; Goalw [FP_def, stable_def, constrains_def] - "-(FP F) = (UN act: Acts F. -{s. act^^{s} <= {s}})"; + "-(FP F) = (UN act: Acts F. -{s. act```{s} <= {s}})"; by (Blast_tac 1); qed "Compl_FP"; -Goal "A - (FP F) = (UN act: Acts F. A - {s. act^^{s} <= {s}})"; +Goal "A - (FP F) = (UN act: Acts F. A - {s. act```{s} <= {s}})"; by (simp_tac (simpset() addsimps [Diff_eq, Compl_FP]) 1); qed "Diff_FP"; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/UNITY/PriorityAux.ML --- a/src/HOL/UNITY/PriorityAux.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/UNITY/PriorityAux.ML Fri Jan 05 18:48:18 2001 +0100 @@ -20,14 +20,14 @@ (* The equalities (above i r = {}) = (A i r = {}) and (reach i r = {}) = (R i r) rely on the following theorem *) -Goal "((r^+)^^{i} = {}) = (r^^{i} = {})"; +Goal "((r^+)```{i} = {}) = (r```{i} = {})"; by Auto_tac; by (etac trancl_induct 1); by Auto_tac; qed "image0_trancl_iff_image0_r"; (* Another form usefull in some situation *) -Goal "(r^^{i}={}) = (ALL x. ((i,x):r^+) = False)"; +Goal "(r```{i}={}) = (ALL x. ((i,x):r^+) = False)"; by Auto_tac; by (dtac (image0_trancl_iff_image0_r RS ssubst) 1); by Auto_tac; @@ -76,7 +76,7 @@ (* Lemma 2 *) Goal -"(z, i):r^+ ==> (ALL y. (y, z):r --> (y, i)~:r^+) = ((r^-1)^^{z}={})"; +"(z, i):r^+ ==> (ALL y. (y, z):r --> (y, i)~:r^+) = ((r^-1)```{z}={})"; by Auto_tac; by (forw_inst_tac [("r", "r")] trancl_into_trancl2 1); by Auto_tac; @@ -86,7 +86,7 @@ "acyclic r ==> A i r~={}-->(EX j:above i r. A j r = {})"; by (full_simp_tac (simpset() addsimps [acyclic_eq_wf, wf_eq_minimal]) 1); -by (dres_inst_tac [("x", "((r^-1)^+)^^{i}")] spec 1); +by (dres_inst_tac [("x", "((r^-1)^+)```{i}")] spec 1); by Auto_tac; by (rotate_tac ~1 1); by (asm_full_simp_tac (simpset() diff -r c0bcea781b3a -r 028d22926a41 src/HOL/UNITY/PriorityAux.thy --- a/src/HOL/UNITY/PriorityAux.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/UNITY/PriorityAux.thy Fri Jan 05 18:48:18 2001 +0100 @@ -18,20 +18,20 @@ (* Neighbors of a vertex i *) neighbors :: "[vertex, (vertex*vertex)set]=>vertex set" - "neighbors i r == ((r Un r^-1)^^{i}) - {i}" + "neighbors i r == ((r Un r^-1)```{i}) - {i}" R :: "[vertex, (vertex*vertex)set]=>vertex set" - "R i r == r^^{i}" + "R i r == r```{i}" A :: "[vertex, (vertex*vertex)set]=>vertex set" - "A i r == (r^-1)^^{i}" + "A i r == (r^-1)```{i}" (* reachable and above vertices: the original notation was R* and A* *) reach :: "[vertex, (vertex*vertex)set]=> vertex set" - "reach i r == (r^+)^^{i}" + "reach i r == (r^+)```{i}" above :: "[vertex, (vertex*vertex)set]=> vertex set" - "above i r == ((r^-1)^+)^^{i}" + "above i r == ((r^-1)^+)```{i}" reverse :: "[vertex, (vertex*vertex) set]=>(vertex*vertex)set" "reverse i r == (r - {(x,y). x=i | y=i} Int r) Un ({(x,y). x=i|y=i} Int r)^-1" diff -r c0bcea781b3a -r 028d22926a41 src/HOL/UNITY/Project.ML --- a/src/HOL/UNITY/Project.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/UNITY/Project.ML Fri Jan 05 18:48:18 2001 +0100 @@ -384,7 +384,7 @@ "[| G : transient (C Int extend_set h A); G : stable C |] \ \ ==> project h C G : transient (project_set h C Int A)"; by (auto_tac (claset(), simpset() addsimps [Domain_project_act])); -by (subgoal_tac "act ^^ (C Int extend_set h A) <= - extend_set h A" 1); +by (subgoal_tac "act ``` (C Int extend_set h A) <= - extend_set h A" 1); by (asm_full_simp_tac (simpset() addsimps [stable_def, constrains_def]) 2); by (Blast_tac 2); @@ -502,8 +502,8 @@ Goalw [project_set_def, extend_set_def, project_act_def] - "act ^^ (C Int extend_set h A) <= B \ -\ ==> project_act h (Restrict C act) ^^ (project_set h C Int A) \ + "act ``` (C Int extend_set h A) <= B \ +\ ==> project_act h (Restrict C act) ``` (project_set h C Int A) \ \ <= project_set h B"; by (Blast_tac 1); qed "act_subset_imp_project_act_subset"; @@ -512,9 +512,9 @@ property upwards. The hard part would be to show that G's action has a big enough domain.*) Goal "[| act: Acts G; \ -\ (project_act h (Restrict C act))^^ \ +\ (project_act h (Restrict C act))``` \ \ (project_set h C Int A - B) <= -(project_set h C Int A - B) |] \ -\ ==> act^^(C Int extend_set h A - extend_set h B) \ +\ ==> act```(C Int extend_set h A - extend_set h B) \ \ <= -(C Int extend_set h A - extend_set h B)"; by (auto_tac (claset(), simpset() addsimps [project_set_def, extend_set_def, project_act_def])); @@ -535,8 +535,8 @@ extend_set_Diff_distrib RS sym])); by (dtac act_subset_imp_project_act_subset 1); by (subgoal_tac - "project_act h (Restrict C act) ^^ (project_set h C Int (A - B)) = {}" 1); -by (REPEAT (thin_tac "?r^^?A <= ?B" 1)); + "project_act h (Restrict C act) ``` (project_set h C Int (A - B)) = {}" 1); +by (REPEAT (thin_tac "?r```?A <= ?B" 1)); by (rewrite_goals_tac [project_set_def, extend_set_def, project_act_def]); by (Blast_tac 2); by (rtac ccontr 1); diff -r c0bcea781b3a -r 028d22926a41 src/HOL/UNITY/SubstAx.ML --- a/src/HOL/UNITY/SubstAx.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/UNITY/SubstAx.ML Fri Jan 05 18:48:18 2001 +0100 @@ -314,7 +314,7 @@ (** Meta or object quantifier ????? **) Goal "[| wf r; \ \ ALL m. F : (A Int f-``{m}) LeadsTo \ -\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \ +\ ((A Int f-``(r^-1 ``` {m})) Un B) |] \ \ ==> F : A LeadsTo B"; by (full_simp_tac (simpset() addsimps [LeadsTo_eq_leadsTo]) 1); by (etac leadsTo_wf_induct 1); @@ -324,7 +324,7 @@ Goal "[| wf r; \ \ ALL m:I. F : (A Int f-``{m}) LeadsTo \ -\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \ +\ ((A Int f-``(r^-1 ``` {m})) Un B) |] \ \ ==> F : A LeadsTo ((A - (f-``I)) Un B)"; by (etac LeadsTo_wf_induct 1); by Safe_tac; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/UNITY/UNITY.ML --- a/src/HOL/UNITY/UNITY.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/UNITY/UNITY.ML Fri Jan 05 18:48:18 2001 +0100 @@ -389,11 +389,11 @@ (** Needed for WF reasoning in WFair.ML **) -Goal "less_than ^^ {k} = greaterThan k"; +Goal "less_than ``` {k} = greaterThan k"; by (Blast_tac 1); qed "Image_less_than"; -Goal "less_than^-1 ^^ {k} = lessThan k"; +Goal "less_than^-1 ``` {k} = lessThan k"; by (Blast_tac 1); qed "Image_inverse_less_than"; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/UNITY/UNITY.thy --- a/src/HOL/UNITY/UNITY.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/UNITY/UNITY.thy Fri Jan 05 18:48:18 2001 +0100 @@ -51,7 +51,7 @@ defs - constrains_def "A co B == {F. ALL act: Acts F. act^^A <= B}" + constrains_def "A co B == {F. ALL act: Acts F. act```A <= B}" unless_def "A unless B == (A-B) co (A Un B)" diff -r c0bcea781b3a -r 028d22926a41 src/HOL/UNITY/WFair.ML --- a/src/HOL/UNITY/WFair.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/UNITY/WFair.ML Fri Jan 05 18:48:18 2001 +0100 @@ -27,14 +27,14 @@ qed "transient_strengthen"; Goalw [transient_def] - "[| act: Acts F; A <= Domain act; act^^A <= -A |] ==> F : transient A"; + "[| act: Acts F; A <= Domain act; act```A <= -A |] ==> F : transient A"; by (Blast_tac 1); qed "transientI"; val major::prems = Goalw [transient_def] "[| F : transient A; \ -\ !!act. [| act: Acts F; A <= Domain act; act^^A <= -A |] ==> P |] \ +\ !!act. [| act: Acts F; A <= Domain act; act```A <= -A |] ==> P |] \ \ ==> P"; by (rtac (major RS CollectD RS bexE) 1); by (blast_tac (claset() addIs prems) 1); @@ -362,10 +362,10 @@ Goal "[| wf r; \ \ ALL m. F : (A Int f-``{m}) leadsTo \ -\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \ +\ ((A Int f-``(r^-1 ``` {m})) Un B) |] \ \ ==> F : (A Int f-``{m}) leadsTo B"; by (eres_inst_tac [("a","m")] wf_induct 1); -by (subgoal_tac "F : (A Int (f -`` (r^-1 ^^ {x}))) leadsTo B" 1); +by (subgoal_tac "F : (A Int (f -`` (r^-1 ``` {x}))) leadsTo B" 1); by (stac vimage_eq_UN 2); by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2); by (blast_tac (claset() addIs [leadsTo_UN]) 2); @@ -376,7 +376,7 @@ (** Meta or object quantifier ? **) Goal "[| wf r; \ \ ALL m. F : (A Int f-``{m}) leadsTo \ -\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \ +\ ((A Int f-``(r^-1 ``` {m})) Un B) |] \ \ ==> F : A leadsTo B"; by (res_inst_tac [("t", "A")] subst 1); by (rtac leadsTo_UN 2); @@ -388,7 +388,7 @@ Goal "[| wf r; \ \ ALL m:I. F : (A Int f-``{m}) leadsTo \ -\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \ +\ ((A Int f-``(r^-1 ``` {m})) Un B) |] \ \ ==> F : A leadsTo ((A - (f-``I)) Un B)"; by (etac leadsTo_wf_induct 1); by Safe_tac; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/UNITY/WFair.thy --- a/src/HOL/UNITY/WFair.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/UNITY/WFair.thy Fri Jan 05 18:48:18 2001 +0100 @@ -15,7 +15,7 @@ (*This definition specifies weak fairness. The rest of the theory is generic to all forms of fairness.*) transient :: "'a set => 'a program set" - "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}" + "transient A == {F. EX act: Acts F. A <= Domain act & act```A <= -A}" ensures :: "['a set, 'a set] => 'a program set" (infixl 60) "A ensures B == (A-B co A Un B) Int transient (A-B)" diff -r c0bcea781b3a -r 028d22926a41 src/HOL/ex/Tarski.ML --- a/src/HOL/ex/Tarski.ML Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/ex/Tarski.ML Fri Jan 05 18:48:18 2001 +0100 @@ -400,7 +400,7 @@ by (simp_tac (simpset() addsimps PO_simp) 1); qed "CLF_E2"; -Goal "f : CLF ^^ {cl} ==> f : CLF ^^ {dual cl}"; +Goal "f : CLF ``` {cl} ==> f : CLF ``` {dual cl}"; by (afs [CLF_def, CL_dualCL, monotone_dual] 1); by (afs [dualA_iff] 1); qed "CLF_dual"; diff -r c0bcea781b3a -r 028d22926a41 src/HOL/ex/Tarski.thy --- a/src/HOL/ex/Tarski.thy Fri Jan 05 18:33:47 2001 +0100 +++ b/src/HOL/ex/Tarski.thy Fri Jan 05 18:48:18 2001 +0100 @@ -94,7 +94,7 @@ "@SL" :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50) translations - "S <<= cl" == "S : sublattice ^^ {cl}" + "S <<= cl" == "S : sublattice ``` {cl}" constdefs dual :: "'a potype => 'a potype" @@ -121,7 +121,7 @@ f :: "'a => 'a" P :: "'a set" assumes - f_cl "f : CLF ^^{cl}" + f_cl "f : CLF```{cl}" defines P_def "P == fix f A"