--- a/src/HOL/Hyperreal/HRealAbs.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HRealAbs.ML Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HSeries.ML Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HSeries.thy Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HyperDef.ML Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HyperNat.ML Tue Jan 09 15:32:27 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";
@@ -936,23 +936,23 @@
by Auto_tac;
qed "SHNat_iff";
-Goalw [SHNat_def] "hypnat_of_nat ``(UNIV::nat set) = SNat";
+Goalw [SHNat_def] "hypnat_of_nat `(UNIV::nat set) = SNat";
by Auto_tac;
qed "hypnat_of_nat_image";
-Goalw [SHNat_def] "inv hypnat_of_nat ``SNat = (UNIV::nat set)";
+Goalw [SHNat_def] "inv hypnat_of_nat `SNat = (UNIV::nat set)";
by Auto_tac;
by (rtac (inj_hypnat_of_nat RS inv_f_f RS subst) 1);
by (Blast_tac 1);
qed "inv_hypnat_of_nat_image";
Goalw [SHNat_def]
- "[| EX x. x: P; P <= SNat |] ==> EX Q. P = hypnat_of_nat `` Q";
+ "[| EX x. x: P; P <= SNat |] ==> EX Q. P = hypnat_of_nat ` Q";
by (Best_tac 1);
qed "SHNat_hypnat_of_nat_image";
Goalw [SHNat_def]
- "SNat = hypnat_of_nat `` (UNIV::nat set)";
+ "SNat = hypnat_of_nat ` (UNIV::nat set)";
by Auto_tac;
qed "SHNat_hypnat_of_nat_iff";
@@ -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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HyperPow.ML Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/HyperPow.thy Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/Lim.ML Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/NSA.ML Tue Jan 09 15:32:27 2001 +0100
@@ -94,18 +94,18 @@
by Auto_tac;
qed "SReal_iff";
-Goalw [SReal_def] "hypreal_of_real ``(UNIV::real set) = SReal";
+Goalw [SReal_def] "hypreal_of_real `(UNIV::real set) = SReal";
by Auto_tac;
qed "hypreal_of_real_image";
-Goalw [SReal_def] "inv hypreal_of_real ``SReal = (UNIV::real set)";
+Goalw [SReal_def] "inv hypreal_of_real `SReal = (UNIV::real set)";
by Auto_tac;
by (rtac (inj_hypreal_of_real RS inv_f_f RS subst) 1);
by (Blast_tac 1);
qed "inv_hypreal_of_real_image";
Goalw [SReal_def]
- "[| EX x. x: P; P <= SReal |] ==> EX Q. P = hypreal_of_real `` Q";
+ "[| EX x. x: P; P <= SReal |] ==> EX Q. P = hypreal_of_real ` Q";
by (Best_tac 1);
qed "SReal_hypreal_of_real_image";
@@ -140,13 +140,13 @@
lifting of ub and property of lub
-------------------------------------------------------*)
Goalw [isUb_def,setle_def]
- "(isUb (SReal) (hypreal_of_real `` Q) (hypreal_of_real Y)) = \
+ "(isUb (SReal) (hypreal_of_real ` Q) (hypreal_of_real Y)) = \
\ (isUb (UNIV :: real set) Q Y)";
by Auto_tac;
qed "hypreal_of_real_isUb_iff";
Goalw [isLub_def,leastP_def]
- "isLub SReal (hypreal_of_real `` Q) (hypreal_of_real Y) \
+ "isLub SReal (hypreal_of_real ` Q) (hypreal_of_real Y) \
\ ==> isLub (UNIV :: real set) Q Y";
by (auto_tac (claset() addIs [hypreal_of_real_isUb_iff RS iffD2],
simpset() addsimps [hypreal_of_real_isUb_iff, setge_def]));
@@ -154,7 +154,7 @@
Goalw [isLub_def,leastP_def]
"isLub (UNIV :: real set) Q Y \
-\ ==> isLub SReal (hypreal_of_real `` Q) (hypreal_of_real Y)";
+\ ==> isLub SReal (hypreal_of_real ` Q) (hypreal_of_real Y)";
by (auto_tac (claset(),
simpset() addsimps [hypreal_of_real_isUb_iff, setge_def]));
by (forw_inst_tac [("x2","x")] (isUbD2a RS (SReal_iff RS iffD1) RS exE) 1);
@@ -163,7 +163,7 @@
by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_isUb_iff]));
qed "hypreal_of_real_isLub2";
-Goal "(isLub SReal (hypreal_of_real `` Q) (hypreal_of_real Y)) = \
+Goal "(isLub SReal (hypreal_of_real ` Q) (hypreal_of_real Y)) = \
\ (isLub (UNIV :: real set) Q Y)";
by (blast_tac (claset() addIs [hypreal_of_real_isLub1,
hypreal_of_real_isLub2]) 1);
@@ -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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/NatStar.ML Tue Jan 09 15:32:27 2001 +0100
@@ -117,7 +117,7 @@
simpset()));
qed "NatStar_mem";
-Goalw [starsetNat_def] "hypnat_of_nat `` A <= *sNat* A";
+Goalw [starsetNat_def] "hypnat_of_nat ` A <= *sNat* A";
by (auto_tac (claset(), simpset() addsimps [hypnat_of_nat_def]));
by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
qed "NatStar_hypreal_of_real_image_subset";
@@ -128,7 +128,7 @@
qed "NatStar_SHNat_subset";
Goalw [starsetNat_def]
- "*sNat* X Int SNat = hypnat_of_nat `` X";
+ "*sNat* X Int SNat = hypnat_of_nat ` X";
by (auto_tac (claset(),
simpset() addsimps
[hypnat_of_nat_def,SHNat_def]));
@@ -140,7 +140,7 @@
by (Auto_tac);
qed "NatStar_hypreal_of_real_Int";
-Goal "x ~: hypnat_of_nat `` A ==> ALL y: A. x ~= hypnat_of_nat y";
+Goal "x ~: hypnat_of_nat ` A ==> ALL y: A. x ~= hypnat_of_nat y";
by (Auto_tac);
qed "lemma_not_hypnatA";
@@ -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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/NatStar.thy Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/Star.ML Tue Jan 09 15:32:27 2001 +0100
@@ -83,12 +83,12 @@
by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],simpset()));
qed "STAR_mem";
-Goalw [starset_def] "hypreal_of_real `` A <= *s* A";
+Goalw [starset_def] "hypreal_of_real ` A <= *s* A";
by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def]));
by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
qed "STAR_hypreal_of_real_image_subset";
-Goalw [starset_def] "*s* X Int SReal = hypreal_of_real `` X";
+Goalw [starset_def] "*s* X Int SReal = hypreal_of_real ` X";
by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def,SReal_def]));
by (fold_tac [hypreal_of_real_def]);
by (rtac imageI 1 THEN rtac ccontr 1);
@@ -98,7 +98,7 @@
by (Auto_tac);
qed "STAR_hypreal_of_real_Int";
-Goal "x ~: hypreal_of_real `` A ==> ALL y: A. x ~= hypreal_of_real y";
+Goal "x ~: hypreal_of_real ` A ==> ALL y: A. x ~= hypreal_of_real y";
by (Auto_tac);
qed "lemma_not_hyprealA";
@@ -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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/Star.thy Tue Jan 09 15:32:27 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/IMPP/Hoare.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/IMPP/Hoare.ML Tue Jan 09 15:32:27 2001 +0100
@@ -64,8 +64,8 @@
by (Fast_tac 1);
qed "conseq2";
-Goal "[| G Un (%p. {P p}. BODY p .{Q p})``Procs \
-\ ||- (%p. {P p}. the (body p) .{Q p})``Procs; \
+Goal "[| G Un (%p. {P p}. BODY p .{Q p})`Procs \
+\ ||- (%p. {P p}. the (body p) .{Q p})`Procs; \
\ pn:Procs |] ==> G|-{P pn}. BODY pn .{Q pn}";
bd hoare_derivs.Body 1;
be hoare_derivs.weaken 1;
@@ -129,7 +129,7 @@
Goal "[| finite U; \
\ !p. G |- {P' p}.c0 p.{Q' p} --> G |- {P p}.c0 p.{Q p} |] ==> \
-\ G||-(%p. {P' p}.c0 p.{Q' p}) `` U --> G||-(%p. {P p}.c0 p.{Q p}) `` U";
+\ G||-(%p. {P' p}.c0 p.{Q' p}) ` U --> G||-(%p. {P p}.c0 p.{Q p}) ` U";
be finite_induct 1;
by (ALLGOALS Clarsimp_tac);
bd derivs_insertD 1;
@@ -154,9 +154,9 @@
qed "Loop_sound_lemma";
Goalw [hoare_valids_def]
- "[| G Un (%pn. {P pn}. BODY pn .{Q pn})``Procs \
-\ ||=(%pn. {P pn}. the (body pn) .{Q pn})``Procs |] ==> \
-\ G||=(%pn. {P pn}. BODY pn .{Q pn})``Procs";
+ "[| G Un (%pn. {P pn}. BODY pn .{Q pn})`Procs \
+\ ||=(%pn. {P pn}. the (body pn) .{Q pn})`Procs |] ==> \
+\ G||=(%pn. {P pn}. BODY pn .{Q pn})`Procs";
br allI 1;
by (induct_tac "n" 1);
by (fast_tac (claset() addIs [Body_triple_valid_0]) 1);
@@ -255,12 +255,12 @@
\ !!G pn. P (insert (mgt_call pn) G) {mgt(the(body pn))} ==> P G {mgt_call pn};\
\ !!G c. [| wt c; !pn:U. P G {mgt_call pn} |] ==> P G {mgt c}; \
\ !!pn. pn : U ==> wt (the (body pn)); \
-\ finite U; uG = mgt_call``U |] ==> \
+\ finite U; uG = mgt_call`U |] ==> \
\ !G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})";
by (cut_facts_tac (premises()) 1);
by (induct_tac "n" 1);
by (ALLGOALS Clarsimp_tac);
-by (subgoal_tac "G = mgt_call `` U" 1);
+by (subgoal_tac "G = mgt_call ` U" 1);
by (asm_simp_tac (simpset() addsimps [card_seteq, finite_imageI]) 2);
by (Asm_full_simp_tac 1);
by (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
@@ -308,9 +308,9 @@
(* Version: simultaneous recursion in call rule *)
(* finiteness not really necessary here *)
-Goalw [MGT_def] "[| G Un (%pn. {=}. BODY pn .{->})``Procs \
-\ ||-(%pn. {=}. the (body pn) .{->})``Procs; \
-\ finite Procs |] ==> G ||-(%pn. {=}. BODY pn .{->})``Procs";
+Goalw [MGT_def] "[| G Un (%pn. {=}. BODY pn .{->})`Procs \
+\ ||-(%pn. {=}. the (body pn) .{->})`Procs; \
+\ finite Procs |] ==> G ||-(%pn. {=}. BODY pn .{->})`Procs";
br hoare_derivs.Body 1;
be finite_pointwise 1;
ba 2;
@@ -321,8 +321,8 @@
(* requires empty, insert, com_det *)
Goal "[| state_not_singleton; WT_bodies; \
-\ F<=(%pn. {=}.the (body pn).{->})``dom body |] ==> \
-\ (%pn. {=}. BODY pn .{->})``dom body||-F";
+\ F<=(%pn. {=}.the (body pn).{->})`dom body |] ==> \
+\ (%pn. {=}. BODY pn .{->})`dom body||-F";
by (ftac finite_subset 1);
br (finite_dom_body RS finite_imageI) 1;
by (rotate_tac 2 1);
@@ -344,7 +344,7 @@
ba 1;
ba 2;
by (Clarsimp_tac 1);
-by (subgoal_tac "{}||-(%pn. {=}. BODY pn .{->})``dom body" 1);
+by (subgoal_tac "{}||-(%pn. {=}. BODY pn .{->})`dom body" 1);
be hoare_derivs.weaken 1;
by (fast_tac (claset() addIs [domI]) 1);
br (finite_dom_body RSN (2,MGT_Body)) 1;
--- a/src/HOL/IMPP/Hoare.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/IMPP/Hoare.thy Tue Jan 09 15:32:27 2001 +0100
@@ -88,9 +88,9 @@
|-{P}. the (body pn) .{Q} ==>
G|-{P}. BODY pn .{Q}"
*)
- Body "[| G Un (%p. {P p}. BODY p .{Q p})``Procs
- ||-(%p. {P p}. the (body p) .{Q p})``Procs |]
- ==> G||-(%p. {P p}. BODY p .{Q p})``Procs"
+ Body "[| G Un (%p. {P p}. BODY p .{Q p})`Procs
+ ||-(%p. {P p}. the (body p) .{Q p})`Procs |]
+ ==> G||-(%p. {P p}. BODY p .{Q p})`Procs"
Call "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])}
==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}.
--- a/src/HOL/Induct/LList.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Induct/LList.ML Tue Jan 09 15:32:27 2001 +0100
@@ -420,7 +420,7 @@
\ f(NIL)=g(NIL); \
\ !!x l. [| x:A; l: llist(A) |] ==> \
\ (f(CONS x l),g(CONS x l)) : \
-\ LListD_Fun (diag A) ((%u.(f(u),g(u)))``llist(A) Un \
+\ LListD_Fun (diag A) ((%u.(f(u),g(u)))`llist(A) Un \
\ diag(llist(A))) \
\ |] ==> f(M) = g(M)";
by (rtac LList_equalityI 1);
@@ -461,7 +461,7 @@
qed "Lmap_type";
(*This type checking rule synthesises a sufficiently large set for f*)
-Goal "M: llist(A) ==> Lmap f M: llist(f``A)";
+Goal "M: llist(A) ==> Lmap f M: llist(f`A)";
by (etac Lmap_type 1);
by (etac imageI 1);
qed "Lmap_type2";
@@ -541,7 +541,7 @@
(*strong co-induction: bisimulation and case analysis on one variable*)
Goal "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
-by (res_inst_tac [("X", "(%u. Lappend u N)``llist(A)")] llist_coinduct 1);
+by (res_inst_tac [("X", "(%u. Lappend u N)`llist(A)")] llist_coinduct 1);
by (etac imageI 1);
by (rtac image_subsetI 1);
by (eres_inst_tac [("aa", "x")] llist.elim 1);
@@ -623,21 +623,21 @@
by (Fast_tac 1);
qed "LListD_Fun_subset_Times_llist";
-Goal "prod_fun Rep_LList Rep_LList `` r <= \
+Goal "prod_fun Rep_LList Rep_LList ` r <= \
\ (llist(range Leaf)) <*> (llist(range Leaf))";
by (fast_tac (claset() delrules [image_subsetI]
addIs [Rep_LList RS LListD]) 1);
qed "subset_Times_llist";
Goal "r <= (llist(range Leaf)) <*> (llist(range Leaf)) ==> \
-\ prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) `` r <= r";
+\ prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) ` r <= r";
by Safe_tac;
by (etac (subsetD RS SigmaE2) 1);
by (assume_tac 1);
by (asm_simp_tac (simpset() addsimps [LListI RS Abs_LList_inverse]) 1);
qed "prod_fun_lemma";
-Goal "prod_fun Rep_LList Rep_LList `` range(%x. (x, x)) = \
+Goal "prod_fun Rep_LList Rep_LList ` range(%x. (x, x)) = \
\ diag(llist(range Leaf))";
by (rtac equalityI 1);
by (Blast_tac 1);
@@ -659,7 +659,7 @@
Goalw [llistD_Fun_def]
"[| (l1,l2) : r; r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2";
by (rtac (inj_Rep_LList RS injD) 1);
-by (res_inst_tac [("r", "prod_fun Rep_LList Rep_LList ``r"),
+by (res_inst_tac [("r", "prod_fun Rep_LList Rep_LList `r"),
("A", "range(Leaf)")]
LList_equalityI 1);
by (etac prod_fun_imageI 1);
--- a/src/HOL/Induct/LList.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Induct/LList.thy Tue Jan 09 15:32:27 2001 +0100
@@ -20,7 +20,7 @@
llistD_Fun_def
"llistD_Fun(r) ==
{(LNil,LNil)} Un
- (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
+ (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))`r)"
*)
LList = Main + SList +
@@ -87,9 +87,9 @@
llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
"llistD_Fun(r) ==
- prod_fun Abs_LList Abs_LList ``
+ prod_fun Abs_LList Abs_LList `
LListD_Fun (diag(range Leaf))
- (prod_fun Rep_LList Rep_LList `` r)"
+ (prod_fun Rep_LList Rep_LList ` r)"
--- a/src/HOL/Integ/Equiv.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Integ/Equiv.ML Tue Jan 09 15:32:27 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,13 +127,13 @@
(*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);
qed "UN_equiv_class";
-(*type checking of UN x:r``{a}. b(x) *)
+(*type checking of UN x:r`{a}. b(x) *)
val prems = Goalw [quotient_def]
"[| equiv A r; congruent r b; X: A//r; \
\ !!x. x : A ==> b(x) : B |] \
@@ -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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Integ/Equiv.thy Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Integ/IntDef.ML Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Integ/IntDef.thy Tue Jan 09 15:32:27 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/Integ/int_arith1.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Integ/int_arith1.ML Tue Jan 09 15:32:27 2001 +0100
@@ -436,7 +436,7 @@
simpset = simpset addsimps add_rules
addsimprocs simprocs
addcongs [if_weak_cong]}),
- arith_inj_const ("IntDef.int", HOLogic.natT --> Type("IntDef.int",[])),
+ arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT),
arith_discrete ("IntDef.int", true)];
end;
--- a/src/HOL/Lattice/Bounds.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lattice/Bounds.thy Tue Jan 09 15:32:27 2001 +0100
@@ -100,11 +100,11 @@
by (simp add: is_inf_def is_sup_def dual_all [symmetric] dual_leq)
theorem dual_Inf [iff?]:
- "is_Inf (dual `` A) (dual sup) = is_Sup A sup"
+ "is_Inf (dual ` A) (dual sup) = is_Sup A sup"
by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq)
theorem dual_Sup [iff?]:
- "is_Sup (dual `` A) (dual inf) = is_Inf A inf"
+ "is_Sup (dual ` A) (dual inf) = is_Inf A inf"
by (simp add: is_Inf_def is_Sup_def dual_all [symmetric] dual_leq)
@@ -169,8 +169,8 @@
assume sup: "is_Sup A sup" and sup': "is_Sup A sup'"
have "dual sup = dual sup'"
proof (rule is_Inf_uniq)
- from sup show "is_Inf (dual `` A) (dual sup)" ..
- from sup' show "is_Inf (dual `` A) (dual sup')" ..
+ from sup show "is_Inf (dual ` A) (dual sup)" ..
+ from sup' show "is_Inf (dual ` A) (dual sup')" ..
qed
thus "sup = sup'" ..
qed
@@ -268,9 +268,9 @@
theorem is_Sup_binary: "is_Sup {x, y} sup = is_sup x y sup"
proof -
- have "is_Sup {x, y} sup = is_Inf (dual `` {x, y}) (dual sup)"
+ have "is_Sup {x, y} sup = is_Inf (dual ` {x, y}) (dual sup)"
by (simp only: dual_Inf)
- also have "dual `` {x, y} = {dual x, dual y}"
+ also have "dual ` {x, y} = {dual x, dual y}"
by simp
also have "is_Inf \<dots> (dual sup) = is_inf (dual x) (dual y) (dual sup)"
by (rule is_Inf_binary)
@@ -312,12 +312,12 @@
theorem Sup_Inf: "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf \<Longrightarrow> is_Inf A inf"
proof -
assume "is_Sup {b. \<forall>a \<in> A. b \<sqsubseteq> a} inf"
- hence "is_Inf (dual `` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b}) (dual inf)"
+ hence "is_Inf (dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b}) (dual inf)"
by (simp only: dual_Inf dual_leq)
- also have "dual `` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b} = {b'. \<forall>a' \<in> dual `` A. a' \<sqsubseteq> b'}"
+ also have "dual ` {b. \<forall>a \<in> A. dual a \<sqsubseteq> dual b} = {b'. \<forall>a' \<in> dual ` A. a' \<sqsubseteq> b'}"
by (auto iff: dual_ball dual_Collect) (* FIXME !? *)
finally have "is_Inf \<dots> (dual inf)" .
- hence "is_Sup (dual `` A) (dual inf)"
+ hence "is_Sup (dual ` A) (dual inf)"
by (rule Inf_Sup)
thus ?thesis ..
qed
--- a/src/HOL/Lattice/CompleteLattice.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lattice/CompleteLattice.thy Tue Jan 09 15:32:27 2001 +0100
@@ -201,8 +201,8 @@
fix A' :: "'a::complete_lattice dual set"
show "\<exists>inf'. is_Inf A' inf'"
proof -
- have "\<exists>sup. is_Sup (undual `` A') sup" by (rule ex_Sup)
- hence "\<exists>sup. is_Inf (dual `` undual `` A') (dual sup)" by (simp only: dual_Inf)
+ have "\<exists>sup. is_Sup (undual ` A') sup" by (rule ex_Sup)
+ hence "\<exists>sup. is_Inf (dual ` undual ` A') (dual sup)" by (simp only: dual_Inf)
thus ?thesis by (simp add: dual_ex [symmetric] image_compose [symmetric])
qed
qed
@@ -212,17 +212,17 @@
other.
*}
-theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual `` A)"
+theorem dual_Meet [intro?]: "dual (\<Sqinter>A) = \<Squnion>(dual ` A)"
proof -
- from is_Inf_Meet have "is_Sup (dual `` A) (dual (\<Sqinter>A))" ..
- hence "\<Squnion>(dual `` A) = dual (\<Sqinter>A)" ..
+ from is_Inf_Meet have "is_Sup (dual ` A) (dual (\<Sqinter>A))" ..
+ hence "\<Squnion>(dual ` A) = dual (\<Sqinter>A)" ..
thus ?thesis ..
qed
-theorem dual_Join [intro?]: "dual (\<Squnion>A) = \<Sqinter>(dual `` A)"
+theorem dual_Join [intro?]: "dual (\<Squnion>A) = \<Sqinter>(dual ` A)"
proof -
- from is_Sup_Join have "is_Inf (dual `` A) (dual (\<Squnion>A))" ..
- hence "\<Sqinter>(dual `` A) = dual (\<Squnion>A)" ..
+ from is_Sup_Join have "is_Inf (dual ` A) (dual (\<Squnion>A))" ..
+ hence "\<Sqinter>(dual ` A) = dual (\<Squnion>A)" ..
thus ?thesis ..
qed
@@ -306,8 +306,8 @@
theorem Join_subset_mono: "A \<subseteq> B \<Longrightarrow> \<Squnion>A \<sqsubseteq> \<Squnion>B"
proof -
assume "A \<subseteq> B"
- hence "dual `` A \<subseteq> dual `` B" by blast
- hence "\<Sqinter>(dual `` B) \<sqsubseteq> \<Sqinter>(dual `` A)" by (rule Meet_subset_antimono)
+ hence "dual ` A \<subseteq> dual ` B" by blast
+ hence "\<Sqinter>(dual ` B) \<sqsubseteq> \<Sqinter>(dual ` A)" by (rule Meet_subset_antimono)
hence "dual (\<Squnion>B) \<sqsubseteq> dual (\<Squnion>A)" by (simp only: dual_Join)
thus ?thesis by (simp only: dual_leq)
qed
@@ -352,9 +352,9 @@
theorem Join_Un: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
proof -
- have "dual (\<Squnion>(A \<union> B)) = \<Sqinter>(dual `` A \<union> dual `` B)"
+ have "dual (\<Squnion>(A \<union> B)) = \<Sqinter>(dual ` A \<union> dual ` B)"
by (simp only: dual_Join image_Un)
- also have "\<dots> = \<Sqinter>(dual `` A) \<sqinter> \<Sqinter>(dual `` B)"
+ also have "\<dots> = \<Sqinter>(dual ` A) \<sqinter> \<Sqinter>(dual ` B)"
by (rule Meet_Un)
also have "\<dots> = dual (\<Squnion>A \<squnion> \<Squnion>B)"
by (simp only: dual_join dual_Join)
--- a/src/HOL/Lattice/Orders.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lattice/Orders.thy Tue Jan 09 15:32:27 2001 +0100
@@ -91,15 +91,15 @@
lemma dual_equality [iff?]: "(dual x = dual y) = (x = y)"
by simp
-lemma dual_ball [iff?]: "(\<forall>x \<in> A. P (dual x)) = (\<forall>x' \<in> dual `` A. P x')"
+lemma dual_ball [iff?]: "(\<forall>x \<in> A. P (dual x)) = (\<forall>x' \<in> dual ` A. P x')"
proof
assume a: "\<forall>x \<in> A. P (dual x)"
- show "\<forall>x' \<in> dual `` A. P x'"
+ show "\<forall>x' \<in> dual ` A. P x'"
proof
- fix x' assume x': "x' \<in> dual `` A"
+ fix x' assume x': "x' \<in> dual ` A"
have "undual x' \<in> A"
proof -
- from x' have "undual x' \<in> undual `` dual `` A" by simp
+ from x' have "undual x' \<in> undual ` dual ` A" by simp
thus "undual x' \<in> A" by (simp add: image_compose [symmetric])
qed
with a have "P (dual (undual x'))" ..
@@ -107,16 +107,16 @@
finally show "P x'" .
qed
next
- assume a: "\<forall>x' \<in> dual `` A. P x'"
+ assume a: "\<forall>x' \<in> dual ` A. P x'"
show "\<forall>x \<in> A. P (dual x)"
proof
fix x assume "x \<in> A"
- hence "dual x \<in> dual `` A" by simp
+ hence "dual x \<in> dual ` A" by simp
with a show "P (dual x)" ..
qed
qed
-lemma range_dual [simp]: "dual `` UNIV = UNIV"
+lemma range_dual [simp]: "dual ` UNIV = UNIV"
proof (rule surj_range)
have "\<And>x'. dual (undual x') = x'" by simp
thus "surj dual" by (rule surjI)
@@ -124,7 +124,7 @@
lemma dual_all [iff?]: "(\<forall>x. P (dual x)) = (\<forall>x'. P x')"
proof -
- have "(\<forall>x \<in> UNIV. P (dual x)) = (\<forall>x' \<in> dual `` UNIV. P x')"
+ have "(\<forall>x \<in> UNIV. P (dual x)) = (\<forall>x' \<in> dual ` UNIV. P x')"
by (rule dual_ball)
thus ?thesis by simp
qed
--- a/src/HOL/Lex/Automata.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lex/Automata.ML Tue Jan 09 15:32:27 2001 +0100
@@ -7,7 +7,7 @@
(*** Equivalence of NA and DA ***)
Goalw [na2da_def]
- "!Q. DA.delta (na2da A) w Q = Union(NA.delta A w `` Q)";
+ "!Q. DA.delta (na2da A) w Q = Union(NA.delta A w ` Q)";
by (induct_tac "w" 1);
by Auto_tac;
qed_spec_mp "DA_delta_is_lift_NA_delta";
@@ -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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lex/Automata.thy Tue Jan 09 15:32:27 2001 +0100
@@ -10,11 +10,11 @@
constdefs
na2da :: ('a,'s)na => ('a,'s set)da
-"na2da A == ({start A}, %a Q. Union(next A a `` Q), %Q. ? q:Q. fin A q)"
+"na2da A == ({start A}, %a Q. Union(next A a ` Q), %Q. ? q:Q. fin A q)"
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/NA.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lex/NA.thy Tue Jan 09 15:32:27 2001 +0100
@@ -13,7 +13,7 @@
consts delta :: "('a,'s)na => 'a list => 's => 's set"
primrec
"delta A [] p = {p}"
-"delta A (a#w) p = Union(delta A w `` next A a p)"
+"delta A (a#w) p = Union(delta A w ` next A a p)"
constdefs
accepts :: ('a,'s)na => 'a list => bool
--- a/src/HOL/Lex/NAe.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lex/NAe.ML Tue Jan 09 15:32:27 2001 +0100
@@ -39,7 +39,7 @@
AddIffs [in_steps_append];
(* Equivalence of steps and delta
-(* Use "(? x : f `` A. P x) = (? a:A. P(f x))" ?? *)
+(* Use "(? x : f ` A. P x) = (? a:A. P(f x))" ?? *)
Goal "!p. (p,q) : steps A w = (q : delta A w p)";
by (induct_tac "w" 1);
by (Simp_tac 1);
--- a/src/HOL/Lex/NAe.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lex/NAe.thy Tue Jan 09 15:32:27 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/Lex/RegExp2NA.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lex/RegExp2NA.thy Tue Jan 09 15:32:27 2001 +0100
@@ -12,7 +12,7 @@
types 'a bitsNA = ('a,bool list)na
syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
-translations "x ## S" == "Cons x `` S"
+translations "x ## S" == "Cons x ` S"
constdefs
atom :: 'a => 'a bitsNA
--- a/src/HOL/Lex/RegExp2NAe.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Lex/RegExp2NAe.thy Tue Jan 09 15:32:27 2001 +0100
@@ -12,7 +12,7 @@
types 'a bitsNAe = ('a,bool list)nae
syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
-translations "x ## S" == "Cons x `` S"
+translations "x ## S" == "Cons x ` S"
constdefs
atom :: 'a => 'a bitsNAe
--- a/src/HOL/MicroJava/BV/JVM.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy Tue Jan 09 15:32:27 2001 +0100
@@ -187,7 +187,7 @@
have "set pTs \<subseteq> types G"
by auto
- hence "OK `` set pTs \<subseteq> err (types G)"
+ hence "OK ` set pTs \<subseteq> err (types G)"
by auto
with instrs maxr isclass
@@ -329,7 +329,7 @@
have "set pTs \<subseteq> types G"
by auto
- hence "OK `` set pTs \<subseteq> err (types G)"
+ hence "OK ` set pTs \<subseteq> err (types G)"
by auto
with instrs isclass
--- a/src/HOL/MicroJava/J/JBasis.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/MicroJava/J/JBasis.ML Tue Jan 09 15:32:27 2001 +0100
@@ -25,8 +25,8 @@
section "unique";
-Goal "(x, y) : set l --> x : fst `` set l";
-by (induct_tac "l" 1);
+Goal "(x, y) : set xys --> x : fst ` set xys";
+by (induct_tac "xys" 1);
by Auto_tac;
qed_spec_mp "fst_in_set_lemma";
--- a/src/HOL/NumberTheory/BijectionRel.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/NumberTheory/BijectionRel.ML Tue Jan 09 15:32:27 2001 +0100
@@ -33,12 +33,12 @@
val lemma_induct = result();
Goalw [inj_on_def]
- "[| A <= B; a ~: A ; a : B; inj_on f B |] ==> (f a) ~: f``A";
+ "[| A <= B; a ~: A ; a : B; inj_on f B |] ==> (f a) ~: f`A";
by Auto_tac;
val lemma = result();
Goal "[| ALL a. a:A --> P a (f a); inj_on f A; finite A; F <= A |] \
-\ ==> (F,f``F) : bijR P";
+\ ==> (F,f`F) : bijR P";
by (res_inst_tac [("F","F"),("A","A")] lemma_induct 1);
by (rtac finite_subset 1);
by Auto_tac;
@@ -48,7 +48,7 @@
val lemma = result();
Goal "[| ALL a. a:A --> P a (f a); inj_on f A; finite A |] \
-\ ==> (A,f``A) : bijR P";
+\ ==> (A,f`A) : bijR P";
by (rtac lemma 1);
by Auto_tac;
qed "inj_func_bijR";
--- a/src/HOL/NumberTheory/EulerFermat.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/NumberTheory/EulerFermat.ML Tue Jan 09 15:32:27 2001 +0100
@@ -121,7 +121,7 @@
by Auto_tac;
qed_spec_mp "RRset_gcd";
-Goal "[| A : RsetR m; #0<m; zgcd(x, m) = #1 |] ==> (%a. a*x)``A : RsetR m";
+Goal "[| A : RsetR m; #0<m; zgcd(x, m) = #1 |] ==> (%a. a*x)`A : RsetR m";
by (etac RsetR.induct 1);
by (ALLGOALS Simp_tac);
by (rtac RsetR.insert 1);
@@ -196,7 +196,7 @@
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zcong_sym])));
qed "RRset2norRR_inj";
-Goal "[| #1<m; is_RRset A m |] ==> (RRset2norRR A m)``A = (norRRset m)";
+Goal "[| #1<m; is_RRset A m |] ==> (RRset2norRR A m)`A = (norRRset m)";
by (rtac card_seteq 1);
by (stac card_image 3);
by (rtac RRset2norRR_inj 4);
@@ -207,11 +207,11 @@
by (auto_tac (claset(),simpset() addsimps [RsetR_fin,Bnor_fin]));
qed "RRset2norRR_eq_norR";
-Goalw [inj_on_def] "[| a ~: A ; inj f |] ==> (f a) ~: f``A";
+Goalw [inj_on_def] "[| a ~: A ; inj f |] ==> (f a) ~: f`A";
by Auto_tac;
val lemma = result();
-Goal "x~=#0 ==> a<m --> setprod ((%a. a*x) `` BnorRset(a,m)) = \
+Goal "x~=#0 ==> a<m --> setprod ((%a. a*x) ` BnorRset(a,m)) = \
\ setprod (BnorRset(a,m)) * x^card(BnorRset(a,m))";
by (induct_thm_tac BnorRset_induct "a m" 1);
by (stac BnorRset_eq 2);
--- a/src/HOL/NumberTheory/EulerFermat.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/NumberTheory/EulerFermat.thy Tue Jan 09 15:32:27 2001 +0100
@@ -30,7 +30,7 @@
defs
norRRset_def "norRRset m == BnorRset (m-#1,m)"
- noXRRset_def "noXRRset m x == (%a. a*x)``(norRRset m)"
+ noXRRset_def "noXRRset m x == (%a. a*x)`(norRRset m)"
phi_def "phi m == card (norRRset m)"
--- a/src/HOL/NumberTheory/WilsonBij.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/NumberTheory/WilsonBij.ML Tue Jan 09 15:32:27 2001 +0100
@@ -127,7 +127,7 @@
by (auto_tac (claset() addIs [d22set_g_1,d22set_le,l1,l2,l3,l4],simpset()));
qed "inv_inj";
-Goal "p : zprime ==> (inv p)``(d22set (p-#2)) = (d22set (p-#2))";
+Goal "p : zprime ==> (inv p)`(d22set (p-#2)) = (d22set (p-#2))";
by (rtac endo_inj_surj 1);
by (rtac d22set_fin 1);
by (etac inv_inj 2);
@@ -141,7 +141,7 @@
Goalw [reciR_def] "p:zprime \
\ ==> (d22set(p-#2),d22set(p-#2)) : (bijR (reciR p))";
-by (res_inst_tac [("s","(d22set(p-#2),(inv p)``(d22set(p-#2)))")] subst 1);
+by (res_inst_tac [("s","(d22set(p-#2),(inv p)`(d22set(p-#2)))")] subst 1);
by (asm_simp_tac (simpset() addsimps [inv_d22set_d22set]) 1);
by (rtac inj_func_bijR 1);
by (rtac d22set_fin 3);
--- a/src/HOL/Real/PNat.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/PNat.ML Tue Jan 09 15:32:27 2001 +0100
@@ -6,7 +6,7 @@
The positive naturals -- proofs mainly as in theory Nat.
*)
-Goal "mono(%X. {1} Un (Suc``X))";
+Goal "mono(%X. {1} Un Suc`X)";
by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
qed "pnat_fun_mono";
--- a/src/HOL/Real/PNat.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/PNat.thy Tue Jan 09 15:32:27 2001 +0100
@@ -9,7 +9,7 @@
PNat = Main +
typedef
- pnat = "lfp(%X. {1} Un (Suc``X))" (lfp_def)
+ pnat = "lfp(%X. {1} Un Suc`X)" (lfp_def)
instance
pnat :: {ord, plus, times}
--- a/src/HOL/Real/PRat.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/PRat.ML Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/PRat.thy Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/PReal.ML Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/RealDef.ML Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/RealDef.thy Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/RealInt.ML Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Real/RealInt.thy Tue Jan 09 15:32:27 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/UNITY/Channel.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Channel.ML Tue Jan 09 15:32:27 2001 +0100
@@ -23,7 +23,7 @@
by Auto_tac;
qed_spec_mp "minSet_nonempty";
-Goal "F : (minSet -`` {Some x}) leadsTo (minSet -`` (Some``greaterThan x))";
+Goal "F : (minSet -` {Some x}) leadsTo (minSet -` (Some`greaterThan x))";
by (rtac leadsTo_weaken 1);
by (res_inst_tac [("x1","x")] ([UC2, UC1] MRS psp) 1);
by Safe_tac;
@@ -32,7 +32,7 @@
qed "minSet_greaterThan";
(*The induction*)
-Goal "F : (UNIV-{{}}) leadsTo (minSet -`` (Some``atLeast y))";
+Goal "F : (UNIV-{{}}) leadsTo (minSet -` (Some`atLeast y))";
by (rtac leadsTo_weaken_R 1);
by (res_inst_tac [("l", "y"), ("f", "the o minSet"), ("B", "{}")]
greaterThan_bounded_induct 1);
--- a/src/HOL/UNITY/Channel.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Channel.thy Tue Jan 09 15:32:27 2001 +0100
@@ -21,10 +21,10 @@
rules
- UC1 "F : (minSet -`` {Some x}) co (minSet -`` (Some``atLeast x))"
+ UC1 "F : (minSet -` {Some x}) co (minSet -` (Some`atLeast x))"
(* UC1 "F : {s. minSet s = x} co {s. x <= minSet s}" *)
- UC2 "F : (minSet -`` {Some x}) leadsTo {s. x ~: s}"
+ UC2 "F : (minSet -` {Some x}) leadsTo {s. x ~: s}"
end
--- a/src/HOL/UNITY/ELT.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/ELT.ML Tue Jan 09 15:32:27 2001 +0100
@@ -15,7 +15,7 @@
Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
by Safe_tac;
-by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
+by (res_inst_tac [("x", "v ` ?u")] image_eqI 2);
by Auto_tac;
qed "givenBy_eq_all";
@@ -307,7 +307,7 @@
(*??IS THIS NEEDED?? or is it just an example of what's provable??*)
Goal "[| F: (A leadsTo[givenBy v] B); G : preserves v; \
\ F Join G : stable C |] \
-\ ==> F Join G : ((C Int A) leadsTo[(%D. C Int D) `` givenBy v] B)";
+\ ==> F Join G : ((C Int A) leadsTo[(%D. C Int D) ` givenBy v] B)";
by (etac leadsETo_induct 1);
by (stac Int_Union 3);
by (blast_tac (claset() addIs [leadsETo_UN]) 3);
@@ -368,7 +368,7 @@
Goalw [LeadsETo_def]
"A LeadsTo[CC] B = \
-\ {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) `` CC] \
+\ {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC] \
\ (reachable F Int B)}";
by (blast_tac (claset() addDs [e_psp_stable2] addIs [leadsETo_weaken]) 1);
qed "LeadsETo_eq_leadsETo";
@@ -467,7 +467,7 @@
(*givenBy laws that need to be in the locale*)
-Goal "givenBy (v o f) = extend_set h `` (givenBy v)";
+Goal "givenBy (v o f) = extend_set h ` (givenBy v)";
by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
by (Deepen_tac 0 1);
qed "givenBy_o_eq_extend_set";
@@ -483,7 +483,7 @@
qed "extend_set_givenBy_I";
Goal "F : A leadsTo[CC] B \
-\ ==> extend h F : (extend_set h A) leadsTo[extend_set h `` CC] \
+\ ==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC] \
\ (extend_set h B)";
by (etac leadsETo_induct 1);
by (asm_simp_tac (simpset() addsimps [leadsETo_UN, extend_set_Union]) 3);
@@ -531,11 +531,11 @@
qed "preserves_o_project_transient_empty";
Goal "[| extend h F Join G : stable C; \
-\ F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)``givenBy v] B; \
+\ F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)`givenBy v] B; \
\ G : preserves (v o f) |] \
\ ==> extend h F Join G : \
\ (C Int extend_set h (project_set h C Int A)) \
-\ leadsTo[(%D. C Int extend_set h D)``givenBy v] (extend_set h B)";
+\ leadsTo[(%D. C Int extend_set h D)`givenBy v] (extend_set h B)";
by (etac leadsETo_induct 1);
by (asm_simp_tac (simpset() delsimps UN_simps
addsimps [Int_UN_distrib, leadsETo_UN, extend_set_Union]) 3);
@@ -560,10 +560,10 @@
Goal "[| extend h F Join G : stable C; \
\ F Join project h C G : \
\ (project_set h C Int A) \
-\ leadsTo[(%D. project_set h C Int D)``givenBy v] B; \
+\ leadsTo[(%D. project_set h C Int D)`givenBy v] B; \
\ G : preserves (v o f) |] \
\ ==> extend h F Join G : (C Int extend_set h A) \
-\ leadsTo[(%D. C Int extend_set h D)``givenBy v] (extend_set h B)";
+\ leadsTo[(%D. C Int extend_set h D)`givenBy v] (extend_set h B)";
by (rtac (lemma RS leadsETo_weaken) 1);
by (auto_tac (claset(),
simpset() addsimps [split_extended_all]));
@@ -630,7 +630,7 @@
Goal "[| extend h F Join G : stable C; \
\ extend h F Join G : \
-\ (C Int A) leadsTo[(%D. C Int D)``givenBy f] B |] \
+\ (C Int A) leadsTo[(%D. C Int D)`givenBy f] B |] \
\ ==> F Join project h C G \
\ : (project_set h C Int project_set h (C Int A)) leadsTo (project_set h B)";
by (etac leadsETo_induct 1);
--- a/src/HOL/UNITY/ELT.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/ELT.thy Tue Jan 09 15:32:27 2001 +0100
@@ -44,7 +44,7 @@
(*the set of all sets determined by f alone*)
givenBy :: "['a => 'b] => 'a set set"
- "givenBy f == range (%B. f-`` B)"
+ "givenBy f == range (%B. f-` B)"
(*visible version of the LEADS-TO relation*)
leadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
@@ -54,6 +54,6 @@
LeadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
("(3_/ LeadsTo[_]/ _)" [80,0,80] 80)
"LeadsETo A CC B ==
- {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) `` CC] B}"
+ {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC] B}"
end
--- a/src/HOL/UNITY/Extend.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Extend.ML Tue Jan 09 15:32:27 2001 +0100
@@ -50,7 +50,7 @@
Goalw [Restrict_def, image_def]
"[| s : RR; Restrict A r = Restrict A s |] \
-\ ==> Restrict A r : Restrict A `` RR";
+\ ==> Restrict A r : Restrict A ` RR";
by Auto_tac;
qed "Restrict_imageI";
@@ -58,14 +58,14 @@
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";
Addsimps [Domain_Restrict, Image_Restrict];
-Goal "f Id = Id ==> insert Id (f``Acts F) = f `` Acts F";
+Goal "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F";
by (blast_tac (claset() addIs [sym RS image_eqI]) 1);
qed "insert_Id_image_Acts";
@@ -211,7 +211,7 @@
(*** project_set: basic properties ***)
(*project_set is simply image!*)
-Goal "project_set h C = f `` C";
+Goal "project_set h C = f ` C";
by (auto_tac (claset() addIs [f_h_eq RS sym],
simpset() addsimps [split_extended_all]));
qed "project_set_eq";
@@ -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];
@@ -363,17 +363,17 @@
qed "Init_project";
Addsimps [Init_project];
-Goal "Acts (extend h F) = (extend_act h `` Acts F)";
+Goal "Acts (extend h F) = (extend_act h ` Acts F)";
by (simp_tac (simpset() addsimps [extend_def, insert_Id_image_Acts]) 1);
qed "Acts_extend";
Addsimps [Acts_extend];
-Goal "AllowedActs (extend h F) = project_act h -`` AllowedActs F";
+Goal "AllowedActs (extend h F) = project_act h -` AllowedActs F";
by (simp_tac (simpset() addsimps [extend_def, insert_absorb]) 1);
qed "AllowedActs_extend";
Addsimps [AllowedActs_extend];
-Goal "Acts(project h C F) = insert Id (project_act h `` Restrict C `` Acts F)";
+Goal "Acts(project h C F) = insert Id (project_act h ` Restrict C ` Acts F)";
by (auto_tac (claset(),
simpset() addsimps [project_def, image_iff]));
qed "Acts_project";
@@ -381,7 +381,7 @@
Goal "AllowedActs(project h C F) = \
\ {act. Restrict (project_set h C) act \
-\ : project_act h `` Restrict C `` AllowedActs F}";
+\ : project_act h ` Restrict C ` AllowedActs F}";
by (simp_tac (simpset() addsimps [project_def, image_iff]) 1);
by (stac insert_absorb 1);
by (auto_tac (claset() addSIs [inst "x" "Id" bexI],
@@ -389,7 +389,7 @@
qed "AllowedActs_project";
Addsimps [AllowedActs_project];
-Goal "Allowed (extend h F) = project h UNIV -`` Allowed F";
+Goal "Allowed (extend h F) = project h UNIV -` Allowed F";
by (simp_tac (simpset() addsimps [AllowedActs_extend, Allowed_def]) 1);
by (Blast_tac 1);
qed "Allowed_extend";
@@ -422,8 +422,8 @@
qed "project_act_Restrict_Id_eq";
Goal "project h C (extend h F) = \
-\ mk_program (Init F, Restrict (project_set h C) `` Acts F, \
-\ {act. Restrict (project_set h C) act : project_act h `` Restrict C `` (project_act h -`` AllowedActs F)})";
+\ mk_program (Init F, Restrict (project_set h C) ` Acts F, \
+\ {act. Restrict (project_set h C) act : project_act h ` Restrict C ` (project_act h -` AllowedActs F)})";
by (rtac program_equalityI 1);
by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 2);
by (Simp_tac 1);
@@ -761,14 +761,14 @@
qed "OK_extend_iff";
Goal "F : X guarantees Y ==> \
-\ extend h F : (extend h `` X) guarantees (extend h `` Y)";
+\ extend h F : (extend h ` X) guarantees (extend h ` Y)";
by (rtac guaranteesI 1);
by (Clarify_tac 1);
by (blast_tac (claset() addDs [ok_extend_imp_ok_project,
extend_Join_eq_extend_D, guaranteesD]) 1);
qed "guarantees_imp_extend_guarantees";
-Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
+Goal "extend h F : (extend h ` X) guarantees (extend h ` Y) \
\ ==> F : X guarantees Y";
by (auto_tac (claset(), simpset() addsimps [guar_def]));
by (dres_inst_tac [("x", "extend h G")] spec 1);
@@ -778,7 +778,7 @@
inj_extend RS inj_image_mem_iff]) 1);
qed "extend_guarantees_imp_guarantees";
-Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) = \
+Goal "(extend h F : (extend h ` X) guarantees (extend h ` Y)) = \
\ (F : X guarantees Y)";
by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
extend_guarantees_imp_guarantees]) 1);
--- a/src/HOL/UNITY/Extend.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Extend.thy Tue Jan 09 15:32:27 2001 +0100
@@ -21,7 +21,7 @@
(*Using the locale constant "f", this is f (h (x,y))) = x*)
extend_set :: "['a*'b => 'c, 'a set] => 'c set"
- "extend_set h A == h `` (A <*> UNIV)"
+ "extend_set h A == h ` (A <*> UNIV)"
project_set :: "['a*'b => 'c, 'c set] => 'a set"
"project_set h C == {x. EX y. h(x,y) : C}"
@@ -34,16 +34,16 @@
extend :: "['a*'b => 'c, 'a program] => 'c program"
"extend h F == mk_program (extend_set h (Init F),
- extend_act h `` Acts F,
- project_act h -`` AllowedActs F)"
+ extend_act h ` Acts F,
+ project_act h -` AllowedActs F)"
(*Argument C allows weak safety laws to be projected*)
project :: "['a*'b => 'c, 'c set, 'c program] => 'a program"
"project h C F ==
mk_program (project_set h (Init F),
- project_act h `` Restrict C `` Acts F,
+ project_act h ` Restrict C ` Acts F,
{act. Restrict (project_set h C) act :
- project_act h `` Restrict C `` AllowedActs F})"
+ project_act h ` Restrict C ` AllowedActs F})"
locale Extend =
fixes
--- a/src/HOL/UNITY/FP.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/FP.ML Tue Jan 09 15:32:27 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/Lift_prog.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML Tue Jan 09 15:32:27 2001 +0100
@@ -214,14 +214,14 @@
(** guarantees **)
Goalw [lift_def]
- "(lift i F : (lift i `` X) guarantees (lift i `` Y)) = \
+ "(lift i F : (lift i ` X) guarantees (lift i ` Y)) = \
\ (F : X guarantees Y)";
by (stac (bij_lift_map RS rename_rename_guarantees_eq RS sym) 1);
by (asm_simp_tac (simpset() addsimps [o_def]) 1);
qed "lift_lift_guarantees_eq";
Goal "(lift i F : X guarantees Y) = \
-\ (F : (rename (drop_map i) `` X) guarantees (rename (drop_map i) `` Y))";
+\ (F : (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))";
by (asm_simp_tac
(simpset() addsimps [bij_lift_map RS rename_guarantees_eq_rename_inv,
lift_def]) 1);
@@ -255,11 +255,11 @@
(*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
-Goal "(f o fst) -`` A = (f-``A) <*> UNIV";
+Goal "(f o fst) -` A = (f-`A) <*> UNIV";
by Auto_tac;
qed "vimage_o_fst_eq";
-Goal "(sub i -``A) <*> UNIV = lift_set i (A <*> UNIV)";
+Goal "(sub i -`A) <*> UNIV = lift_set i (A <*> UNIV)";
by Auto_tac;
qed "vimage_sub_eq_lift_set";
@@ -356,7 +356,7 @@
qed "lift_transient_eq_disj";
(*USELESS??*)
-Goal "lift_map i `` (A <*> UNIV) = \
+Goal "lift_map i ` (A <*> UNIV) = \
\ (UN s:A. UN f. {insert_map i s f}) <*> UNIV";
by (auto_tac (claset() addSIs [bexI, image_eqI],
simpset() addsimps [lift_map_def]));
@@ -475,12 +475,12 @@
UNION_OK_lift_I]) 1);
qed "OK_lift_I";
-Goal "Allowed (lift i F) = lift i `` (Allowed F)";
+Goal "Allowed (lift i F) = lift i ` (Allowed F)";
by (simp_tac (simpset() addsimps [lift_def, Allowed_rename]) 1);
qed "Allowed_lift";
Addsimps [Allowed_lift];
-Goal "lift i `` preserves v = preserves (v o drop_map i)";
+Goal "lift i ` preserves v = preserves (v o drop_map i)";
by (simp_tac (simpset() addsimps [rename_image_preserves, lift_def,
inv_lift_map_eq]) 1);
qed "lift_image_preserves";
--- a/src/HOL/UNITY/Lift_prog.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy Tue Jan 09 15:32:27 2001 +0100
@@ -25,7 +25,7 @@
"drop_map i == %(g, uu). (g i, (delete_map i g, uu))"
lift_set :: "[nat, ('b * ((nat=>'b) * 'c)) set] => ((nat=>'b) * 'c) set"
- "lift_set i A == lift_map i `` A"
+ "lift_set i A == lift_map i ` A"
lift :: "[nat, ('b * ((nat=>'b) * 'c)) program] => ((nat=>'b) * 'c) program"
"lift i == rename (lift_map i)"
--- a/src/HOL/UNITY/PPROD.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/PPROD.ML Tue Jan 09 15:32:27 2001 +0100
@@ -127,7 +127,7 @@
by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
qed "guarantees_PLam_I";
-Goal "Allowed (PLam I F) = (INT i:I. lift i `` Allowed(F i))";
+Goal "Allowed (PLam I F) = (INT i:I. lift i ` Allowed(F i))";
by (simp_tac (simpset() addsimps [PLam_def]) 1);
qed "Allowed_PLam";
Addsimps [Allowed_PLam];
--- a/src/HOL/UNITY/PriorityAux.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/PriorityAux.ML Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/PriorityAux.thy Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Project.ML Tue Jan 09 15:32:27 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/Reach.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Reach.ML Tue Jan 09 15:32:27 2001 +0100
@@ -108,7 +108,7 @@
simpset() addsimps [fun_upd_idem]));
qed "metric_le";
-Goal "Rprg : ((metric-``{m}) - fixedpoint) LeadsTo (metric-``(lessThan m))";
+Goal "Rprg : ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))";
by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
by (rtac LeadsTo_UN 1);
by Auto_tac;
@@ -120,7 +120,7 @@
simpset()));
qed "LeadsTo_Diff_fixedpoint";
-Goal "Rprg : (metric-``{m}) LeadsTo (metric-``(lessThan m) Un fixedpoint)";
+Goal "Rprg : (metric-`{m}) LeadsTo (metric-`(lessThan m) Un fixedpoint)";
by (rtac ([LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R,
subset_imp_LeadsTo] MRS LeadsTo_Diff) 1);
by Auto_tac;
--- a/src/HOL/UNITY/Rename.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Rename.ML Tue Jan 09 15:32:27 2001 +0100
@@ -26,18 +26,18 @@
by (etac surj_f_inv_f 1);
qed "fst_o_inv_eq_inv";
-Goal "bij h ==> z : h``A = (inv h z : A)";
+Goal "bij h ==> z : h`A = (inv h z : A)";
by (auto_tac (claset() addSIs [image_eqI],
simpset() addsimps [bij_is_inj, bij_is_surj RS surj_f_inv_f]));
qed "mem_rename_set_iff";
-Goal "extend_set (%(x,u). h x) A = h``A";
+Goal "extend_set (%(x,u). h x) A = h`A";
by (auto_tac (claset() addSIs [image_eqI],
simpset() addsimps [extend_set_def]));
qed "extend_set_eq_image";
Addsimps [extend_set_eq_image];
-Goalw [rename_def] "Init (rename h F) = h``(Init F)";
+Goalw [rename_def] "Init (rename h F) = h`(Init F)";
by (Simp_tac 1);
qed "Init_rename";
@@ -145,7 +145,7 @@
by (asm_simp_tac (simpset() addsimps [export extend_inverse]) 1);
qed "inv_project_eq";
-Goal "bij h ==> Allowed (rename h F) = rename h `` Allowed F";
+Goal "bij h ==> Allowed (rename h F) = rename h ` Allowed F";
by (asm_simp_tac (simpset() addsimps [rename_def, export Allowed_extend]) 1);
by (stac bij_vimage_eq_inv_image 1);
by (rtac bij_project 1);
@@ -209,17 +209,17 @@
(*** Strong Safety: co, stable ***)
Goalw [rename_def]
- "bij h ==> (rename h F : (h``A) co (h``B)) = (F : A co B)";
+ "bij h ==> (rename h F : (h`A) co (h`B)) = (F : A co B)";
by (REPEAT (stac (extend_set_eq_image RS sym) 1));
by (etac (good_map_bij RS export extend_constrains) 1);
qed "rename_constrains";
Goalw [stable_def]
- "bij h ==> (rename h F : stable (h``A)) = (F : stable A)";
+ "bij h ==> (rename h F : stable (h`A)) = (F : stable A)";
by (asm_simp_tac (simpset() addsimps [rename_constrains]) 1);
qed "rename_stable";
-Goal "bij h ==> (rename h F : invariant (h``A)) = (F : invariant A)";
+Goal "bij h ==> (rename h F : invariant (h`A)) = (F : invariant A)";
by (asm_simp_tac (simpset() addsimps [invariant_def, rename_stable,
bij_is_inj RS inj_image_subset_iff]) 1);
qed "rename_invariant";
@@ -234,22 +234,22 @@
(*** Weak Safety: Co, Stable ***)
Goalw [rename_def]
- "bij h ==> reachable (rename h F) = h `` (reachable F)";
+ "bij h ==> reachable (rename h F) = h ` (reachable F)";
by (asm_simp_tac (simpset() addsimps [export reachable_extend_eq]) 1);
qed "reachable_rename_eq";
-Goal "bij h ==> (rename h F : (h``A) Co (h``B)) = (F : A Co B)";
+Goal "bij h ==> (rename h F : (h`A) Co (h`B)) = (F : A Co B)";
by (asm_simp_tac
(simpset() addsimps [Constrains_def, reachable_rename_eq,
rename_constrains, bij_is_inj, image_Int RS sym]) 1);
qed "rename_Constrains";
Goalw [Stable_def]
- "bij h ==> (rename h F : Stable (h``A)) = (F : Stable A)";
+ "bij h ==> (rename h F : Stable (h`A)) = (F : Stable A)";
by (asm_simp_tac (simpset() addsimps [rename_Constrains]) 1);
qed "rename_Stable";
-Goal "bij h ==> (rename h F : Always (h``A)) = (F : Always A)";
+Goal "bij h ==> (rename h F : Always (h`A)) = (F : Always A)";
by (asm_simp_tac (simpset() addsimps [Always_def, rename_Stable,
bij_is_inj RS inj_image_subset_iff]) 1);
qed "rename_Always";
@@ -264,32 +264,32 @@
(*** Progress: transient, ensures ***)
Goalw [rename_def]
- "bij h ==> (rename h F : transient (h``A)) = (F : transient A)";
+ "bij h ==> (rename h F : transient (h`A)) = (F : transient A)";
by (stac (extend_set_eq_image RS sym) 1);
by (etac (good_map_bij RS export extend_transient) 1);
qed "rename_transient";
Goalw [rename_def]
- "bij h ==> (rename h F : (h``A) ensures (h``B)) = (F : A ensures B)";
+ "bij h ==> (rename h F : (h`A) ensures (h`B)) = (F : A ensures B)";
by (REPEAT (stac (extend_set_eq_image RS sym) 1));
by (etac (good_map_bij RS export extend_ensures) 1);
qed "rename_ensures";
Goalw [rename_def]
- "bij h ==> (rename h F : (h``A) leadsTo (h``B)) = (F : A leadsTo B)";
+ "bij h ==> (rename h F : (h`A) leadsTo (h`B)) = (F : A leadsTo B)";
by (REPEAT (stac (extend_set_eq_image RS sym) 1));
by (etac (good_map_bij RS export extend_leadsTo) 1);
qed "rename_leadsTo";
Goalw [rename_def]
- "bij h ==> (rename h F : (h``A) LeadsTo (h``B)) = (F : A LeadsTo B)";
+ "bij h ==> (rename h F : (h`A) LeadsTo (h`B)) = (F : A LeadsTo B)";
by (REPEAT (stac (extend_set_eq_image RS sym) 1));
by (etac (good_map_bij RS export extend_LeadsTo) 1);
qed "rename_LeadsTo";
Goalw [rename_def]
- "bij h ==> (rename h F : (rename h `` X) guarantees \
-\ (rename h `` Y)) = \
+ "bij h ==> (rename h F : (rename h ` X) guarantees \
+\ (rename h ` Y)) = \
\ (F : X guarantees Y)";
by (stac (good_map_bij RS export extend_guarantees_eq RS sym) 1);
by (assume_tac 1);
@@ -297,8 +297,8 @@
qed "rename_rename_guarantees_eq";
Goal "bij h ==> (rename h F : X guarantees Y) = \
-\ (F : (rename (inv h) `` X) guarantees \
-\ (rename (inv h) `` Y))";
+\ (F : (rename (inv h) ` X) guarantees \
+\ (rename (inv h) ` Y))";
by (stac (rename_rename_guarantees_eq RS sym) 1);
by (assume_tac 1);
by (asm_simp_tac
@@ -336,47 +336,47 @@
(auto_tac (claset() addSIs [surj_rename RS surj_f_inv_f RS sym],
simpset() addsimps ths))];
-Goal "bij h ==> rename h `` (A co B) = (h `` A) co (h``B)";
+Goal "bij h ==> rename h ` (A co B) = (h ` A) co (h`B)";
by (rename_image_tac [rename_constrains]);
qed "rename_image_constrains";
-Goal "bij h ==> rename h `` stable A = stable (h `` A)";
+Goal "bij h ==> rename h ` stable A = stable (h ` A)";
by (rename_image_tac [rename_stable]);
qed "rename_image_stable";
-Goal "bij h ==> rename h `` increasing func = increasing (func o inv h)";
+Goal "bij h ==> rename h ` increasing func = increasing (func o inv h)";
by (rename_image_tac [rename_increasing, o_def, bij_is_inj]);
qed "rename_image_increasing";
-Goal "bij h ==> rename h `` invariant A = invariant (h `` A)";
+Goal "bij h ==> rename h ` invariant A = invariant (h ` A)";
by (rename_image_tac [rename_invariant]);
qed "rename_image_invariant";
-Goal "bij h ==> rename h `` (A Co B) = (h `` A) Co (h``B)";
+Goal "bij h ==> rename h ` (A Co B) = (h ` A) Co (h`B)";
by (rename_image_tac [rename_Constrains]);
qed "rename_image_Constrains";
-Goal "bij h ==> rename h `` preserves v = preserves (v o inv h)";
+Goal "bij h ==> rename h ` preserves v = preserves (v o inv h)";
by (asm_simp_tac (simpset() addsimps [o_def, rename_image_stable,
preserves_def, bij_image_INT, bij_image_Collect_eq]) 1);
qed "rename_image_preserves";
-Goal "bij h ==> rename h `` Stable A = Stable (h `` A)";
+Goal "bij h ==> rename h ` Stable A = Stable (h ` A)";
by (rename_image_tac [rename_Stable]);
qed "rename_image_Stable";
-Goal "bij h ==> rename h `` Increasing func = Increasing (func o inv h)";
+Goal "bij h ==> rename h ` Increasing func = Increasing (func o inv h)";
by (rename_image_tac [rename_Increasing, o_def, bij_is_inj]);
qed "rename_image_Increasing";
-Goal "bij h ==> rename h `` Always A = Always (h `` A)";
+Goal "bij h ==> rename h ` Always A = Always (h ` A)";
by (rename_image_tac [rename_Always]);
qed "rename_image_Always";
-Goal "bij h ==> rename h `` (A leadsTo B) = (h `` A) leadsTo (h``B)";
+Goal "bij h ==> rename h ` (A leadsTo B) = (h ` A) leadsTo (h`B)";
by (rename_image_tac [rename_leadsTo]);
qed "rename_image_leadsTo";
-Goal "bij h ==> rename h `` (A LeadsTo B) = (h `` A) LeadsTo (h``B)";
+Goal "bij h ==> rename h ` (A LeadsTo B) = (h ` A) LeadsTo (h`B)";
by (rename_image_tac [rename_LeadsTo]);
qed "rename_image_LeadsTo";
--- a/src/HOL/UNITY/SubstAx.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/SubstAx.ML Tue Jan 09 15:32:27 2001 +0100
@@ -313,8 +313,8 @@
(** Meta or object quantifier ????? **)
Goal "[| wf r; \
-\ ALL m. F : (A Int f-``{m}) LeadsTo \
-\ ((A Int f-``(r^-1 ``` {m})) Un B) |] \
+\ ALL m. F : (A Int f-`{m}) LeadsTo \
+\ ((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);
@@ -323,9 +323,9 @@
Goal "[| wf r; \
-\ ALL m:I. F : (A Int f-``{m}) LeadsTo \
-\ ((A Int f-``(r^-1 ``` {m})) Un B) |] \
-\ ==> F : A LeadsTo ((A - (f-``I)) Un B)";
+\ ALL m:I. F : (A Int f-`{m}) LeadsTo \
+\ ((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;
by (case_tac "m:I" 1);
@@ -335,7 +335,7 @@
val prems =
-Goal "(!!m::nat. F : (A Int f-``{m}) LeadsTo ((A Int f-``(lessThan m)) Un B)) \
+Goal "(!!m::nat. F : (A Int f-`{m}) LeadsTo ((A Int f-`(lessThan m)) Un B)) \
\ ==> F : A LeadsTo B";
by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
by (auto_tac (claset() addIs prems, simpset()));
@@ -353,17 +353,17 @@
by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, nat_less_iff]));
qed "integ_0_le_induct";
-Goal "!!l::nat. [| ALL m:(greaterThan l). F : (A Int f-``{m}) LeadsTo \
-\ ((A Int f-``(lessThan m)) Un B) |] \
-\ ==> F : A LeadsTo ((A Int (f-``(atMost l))) Un B)";
+Goal "!!l::nat. [| ALL m:(greaterThan l). F : (A Int f-`{m}) LeadsTo \
+\ ((A Int f-`(lessThan m)) Un B) |] \
+\ ==> F : A LeadsTo ((A Int (f-`(atMost l))) Un B)";
by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
by (rtac (wf_less_than RS Bounded_induct) 1);
by (Asm_simp_tac 1);
qed "LessThan_bounded_induct";
-Goal "!!l::nat. [| ALL m:(lessThan l). F : (A Int f-``{m}) LeadsTo \
-\ ((A Int f-``(greaterThan m)) Un B) |] \
-\ ==> F : A LeadsTo ((A Int (f-``(atLeast l))) Un B)";
+Goal "!!l::nat. [| ALL m:(lessThan l). F : (A Int f-`{m}) LeadsTo \
+\ ((A Int f-`(greaterThan m)) Un B) |] \
+\ ==> F : A LeadsTo ((A Int (f-`(atLeast l))) Un B)";
by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
(wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1);
by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
--- a/src/HOL/UNITY/Token.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/Token.ML Tue Jan 09 15:32:27 2001 +0100
@@ -74,8 +74,7 @@
by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq]));
qed "TR7_aux";
-Goal "({s. token s < N} Int token -`` {m}) = \
-\ (if m<N then token -`` {m} else {})";
+Goal "({s. token s < N} Int token -` {m}) = (if m<N then token -` {m} else {})";
by Auto_tac;
val token_lemma = result();
--- a/src/HOL/UNITY/UNITY.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/UNITY.ML Tue Jan 09 15:32:27 2001 +0100
@@ -383,17 +383,17 @@
qed "Un_Diff_Diff";
Addsimps [Un_Diff_Diff];
-Goal "Union(B) Int A = Union((%C. C Int A)``B)";
+Goal "Union(B) Int A = Union((%C. C Int A)`B)";
by (Blast_tac 1);
qed "Int_Union_Union";
(** 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/UNITY.thy Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/WFair.ML Tue Jan 09 15:32:27 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);
@@ -361,11 +361,11 @@
(** The most general rule: r is any wf relation; f is any variant function **)
Goal "[| wf r; \
-\ ALL m. F : (A Int f-``{m}) leadsTo \
-\ ((A Int f-``(r^-1 ``` {m})) Un B) |] \
-\ ==> F : (A Int f-``{m}) leadsTo B";
+\ ALL m. F : (A Int f-`{m}) leadsTo \
+\ ((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);
@@ -375,8 +375,8 @@
(** Meta or object quantifier ? **)
Goal "[| wf r; \
-\ ALL m. F : (A Int f-``{m}) leadsTo \
-\ ((A Int f-``(r^-1 ``` {m})) Un B) |] \
+\ ALL m. F : (A Int f-`{m}) leadsTo \
+\ ((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);
@@ -387,9 +387,9 @@
Goal "[| wf r; \
-\ ALL m:I. F : (A Int f-``{m}) leadsTo \
-\ ((A Int f-``(r^-1 ``` {m})) Un B) |] \
-\ ==> F : A leadsTo ((A - (f-``I)) Un B)";
+\ ALL m:I. F : (A Int f-`{m}) leadsTo \
+\ ((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;
by (case_tac "m:I" 1);
@@ -398,9 +398,9 @@
qed "bounded_induct";
-(*Alternative proof is via the lemma F : (A Int f-``(lessThan m)) leadsTo B*)
+(*Alternative proof is via the lemma F : (A Int f-`(lessThan m)) leadsTo B*)
val prems =
-Goal "[| !!m::nat. F : (A Int f-``{m}) leadsTo ((A Int f-``{..m(}) Un B) |] \
+Goal "[| !!m::nat. F : (A Int f-`{m}) leadsTo ((A Int f-`{..m(}) Un B) |] \
\ ==> F : A leadsTo B";
by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
by (Asm_simp_tac 1);
@@ -408,8 +408,8 @@
qed "lessThan_induct";
Goal "!!l::nat. [| ALL m:(greaterThan l). \
-\ F : (A Int f-``{m}) leadsTo ((A Int f-``(lessThan m)) Un B) |] \
-\ ==> F : A leadsTo ((A Int (f-``(atMost l))) Un B)";
+\ F : (A Int f-`{m}) leadsTo ((A Int f-`(lessThan m)) Un B) |] \
+\ ==> F : A leadsTo ((A Int (f-`(atMost l))) Un B)";
by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl,
Compl_greaterThan RS sym]) 1);
by (rtac (wf_less_than RS bounded_induct) 1);
@@ -417,8 +417,8 @@
qed "lessThan_bounded_induct";
Goal "!!l::nat. [| ALL m:(lessThan l). \
-\ F : (A Int f-``{m}) leadsTo ((A Int f-``(greaterThan m)) Un B) |] \
-\ ==> F : A leadsTo ((A Int (f-``(atLeast l))) Un B)";
+\ F : (A Int f-`{m}) leadsTo ((A Int f-`(greaterThan m)) Un B) |] \
+\ ==> F : A leadsTo ((A Int (f-`(atLeast l))) Un B)";
by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
(wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1);
by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
--- a/src/HOL/UNITY/WFair.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/WFair.thy Tue Jan 09 15:32:27 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/Multiquote.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/ex/Multiquote.thy Tue Jan 09 15:32:27 2001 +0100
@@ -13,7 +13,7 @@
syntax
"_quote" :: "'b => ('a => 'b)" (".'(_')." [0] 1000)
- "_antiquote" :: "('a => 'b) => 'b" ("`_" [1000] 1000)
+ "_antiquote" :: "('a => 'b) => 'b" ("´_" [1000] 1000)
parse_translation {*
let
@@ -35,14 +35,14 @@
text {* basic examples *}
term ".(a + b + c)."
-term ".(a + b + c + `x + `y + 1)."
-term ".(`(f w) + `x)."
-term ".(f `x `y z)."
+term ".(a + b + c + ´x + ´y + 1)."
+term ".(´(f w) + ´x)."
+term ".(f ´x ´y z)."
text {* advanced examples *}
-term ".(.(` `x + `y).)."
-term ".(.(` `x + `y). o `f)."
-term ".(`(f o `g))."
-term ".(.( ` `(f o `g) ).)."
+term ".(.(´ ´x + ´y).)."
+term ".(.(´ ´x + ´y). o ´f)."
+term ".(´(f o ´g))."
+term ".(.( ´ ´(f o ´g) ).)."
end
--- a/src/HOL/ex/PiSets.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/ex/PiSets.ML Tue Jan 09 15:32:27 2001 +0100
@@ -38,7 +38,7 @@
-Goal "PiBij A B `` (Pi A B) = Graph A B";
+Goal "PiBij A B ` (Pi A B) = Graph A B";
by (rtac equalityI 1);
by (force_tac (claset(), simpset() addsimps [image_def,PiBij_in_Graph]) 1);
by (rtac subsetI 1);
--- a/src/HOL/ex/Tarski.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/ex/Tarski.ML Tue Jan 09 15:32:27 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 Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/ex/Tarski.thy Tue Jan 09 15:32:27 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"
--- a/src/HOL/ex/set.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/ex/set.ML Tue Jan 09 15:32:27 2001 +0100
@@ -25,12 +25,12 @@
(** Examples for the Blast_tac paper **)
(*Union-image, called Un_Union_image on equalities.ML*)
-Goal "(UN x:C. f(x) Un g(x)) = Union(f``C) Un Union(g``C)";
+Goal "(UN x:C. f(x) Un g(x)) = Union(f`C) Un Union(g`C)";
by (Blast_tac 1);
qed "";
(*Inter-image, called Int_Inter_image on equalities.ML*)
-Goal "(INT x:C. f(x) Int g(x)) = Inter(f``C) Int Inter(g``C)";
+Goal "(INT x:C. f(x) Int g(x)) = Inter(f`C) Int Inter(g`C)";
by (Blast_tac 1);
qed "";
@@ -83,24 +83,24 @@
(*** The Schroeder-Berstein Theorem ***)
-Goal "[| -(f``X) = g``(-X); f(a)=g(b); a:X |] ==> b:X";
+Goal "[| -(f`X) = g`(-X); f(a)=g(b); a:X |] ==> b:X";
by (Blast_tac 1);
qed "disj_lemma";
-Goal "-(f``X) = g``(-X) ==> surj(%z. if z:X then f(z) else g(z))";
+Goal "-(f`X) = g`(-X) ==> surj(%z. if z:X then f(z) else g(z))";
by (asm_simp_tac (simpset() addsimps [surj_def]) 1);
by (Blast_tac 1);
qed "surj_if_then_else";
Goalw [inj_on_def]
- "[| inj_on f X; inj_on g (-X); -(f``X) = g``(-X); \
+ "[| inj_on f X; inj_on g (-X); -(f`X) = g`(-X); \
\ h = (%z. if z:X then f(z) else g(z)) |] \
\ ==> inj(h) & surj(h)";
by (asm_simp_tac (simpset() addsimps [surj_if_then_else]) 1);
by (blast_tac (claset() addDs [disj_lemma, sym]) 1);
qed "bij_if_then_else";
-Goal "EX X. X = - (g``(- (f``X)))";
+Goal "EX X. X = - (g`(- (f`X)))";
by (rtac exI 1);
by (rtac lfp_unfold 1);
by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1));
--- a/src/HOLCF/Cfun1.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Cfun1.ML Tue Jan 09 15:32:27 2001 +0100
@@ -50,15 +50,15 @@
(* lemmas about application of continuous functions *)
(* ------------------------------------------------------------------------ *)
-Goal "[| f=g; x=y |] ==> f`x = g`y";
+Goal "[| f=g; x=y |] ==> f$x = g$y";
by (Asm_simp_tac 1);
qed "cfun_cong";
-Goal "f=g ==> f`x = g`x";
+Goal "f=g ==> f$x = g$x";
by (Asm_simp_tac 1);
qed "cfun_fun_cong";
-Goal "x=y ==> f`x = f`y";
+Goal "x=y ==> f$x = f$y";
by (Asm_simp_tac 1);
qed "cfun_arg_cong";
@@ -77,7 +77,7 @@
(* simplification of application *)
(* ------------------------------------------------------------------------ *)
-Goal "cont f ==> (Abs_CFun f)`x = f x";
+Goal "cont f ==> (Abs_CFun f)$x = f x";
by (etac (Abs_Cfun_inverse2 RS fun_cong) 1);
qed "Cfunapp2";
@@ -85,7 +85,7 @@
(* beta - equality for continuous functions *)
(* ------------------------------------------------------------------------ *)
-Goal "cont(c1) ==> (LAM x .c1 x)`u = c1 u";
+Goal "cont(c1) ==> (LAM x .c1 x)$u = c1 u";
by (rtac Cfunapp2 1);
by (atac 1);
qed "beta_cfun";
--- a/src/HOLCF/Cfun1.thy Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Cfun1.thy Tue Jan 09 15:32:27 2001 +0100
@@ -17,7 +17,7 @@
instance "->" :: (cpo,cpo)sq_ord
syntax
- Rep_CFun :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
+ Rep_CFun :: "('a -> 'b)=>('a => 'b)" ("_$_" [999,1000] 999)
(* application *)
Abs_CFun :: "('a => 'b)=>('a -> 'b)" (binder "LAM " 10)
(* abstraction *)
--- a/src/HOLCF/Cfun2.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOLCF/Cfun2.ML Tue Jan 09 15:32:27 2001 +0100
@@ -63,10 +63,10 @@