--- 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);
--- 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)";
--- 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";
--- 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";
--- 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);
--- 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)
--- 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));
--- 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) &
--- 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],
--- 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) &
--- 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
--- 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
--- 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;
--- 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 ==> [<X 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,
--- 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];
--- 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}"
--- 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(),
--- 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";
--- 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}"
--- 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];
--- 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)";
--- 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);
--- 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)"
--- 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);
--- 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<y & (x,y::nat):Rep_Integ(Z)"
@@ -40,7 +40,7 @@
zadd_def
"z + w ==
Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).
- intrel^^{(x1+x2, y1+y2)})"
+ intrel```{(x1+x2, y1+y2)})"
zdiff_def "z - (w::int) == z + (-w)"
@@ -51,6 +51,6 @@
zmult_def
"z * w ==
Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).
- intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
+ intrel```{(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
end
--- a/src/HOL/Lex/Automata.ML Fri Jan 05 18:33:47 2001 +0100
+++ b/src/HOL/Lex/Automata.ML Fri Jan 05 18:48:18 2001 +0100
@@ -21,7 +21,7 @@
(*** Direct equivalence of NAe and DA ***)
Goalw [nae2da_def]
- "!Q. (eps A)^* ^^ (DA.delta (nae2da A) w Q) = steps A w ^^ Q";
+ "!Q. (eps A)^* ``` (DA.delta (nae2da A) w Q) = steps A w ``` Q";
by (induct_tac "w" 1);
by (Simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [step_def]) 1);
@@ -29,7 +29,7 @@
qed_spec_mp "espclosure_DA_delta_is_steps";
Goalw [nae2da_def]
- "fin (nae2da A) Q = (? q : (eps A)^* ^^ Q. fin A q)";
+ "fin (nae2da A) Q = (? q : (eps A)^* ``` Q. fin A q)";
by (Simp_tac 1);
val lemma = result();
--- a/src/HOL/Lex/Automata.thy Fri Jan 05 18:33:47 2001 +0100
+++ b/src/HOL/Lex/Automata.thy Fri Jan 05 18:48:18 2001 +0100
@@ -14,7 +14,7 @@
nae2da :: ('a,'s)nae => ('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
--- 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
--- 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 \<turnstile> c1 \<preceq>C Object"
"G \<turnstile> c2 \<preceq>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 \<turnstile> c1 \<preceq>C some_lub ((subcls1 G)^* ) c1 c2"
by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD)
@@ -214,10 +214,10 @@
"G \<turnstile> c1 \<preceq>C Object"
"G \<turnstile> c2 \<preceq>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 \<turnstile> c1 \<preceq>C some_lub ((subcls1 G)^* ) c2 c1"
by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD)
@@ -242,10 +242,10 @@
"G \<turnstile> c1 \<preceq>C Object"
"G \<turnstile> c2 \<preceq>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
--- 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
--- 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";
--- 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
--- 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]));
--- 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";
--- 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
--- 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);
--- 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)))})"
--- 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";
--- 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}"
--- 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";
--- 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];
--- 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";
--- 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()
--- 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"
--- 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);
--- 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;
--- 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";
--- 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)"
--- 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;
--- 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)"
--- 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";
--- 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"