# HG changeset patch # User nipkow # Date 979050747 -3600 # Node ID a7897aebbffc6ba75e5f9a688b7b6bdb0fa4da8e # Parent c0844a30ea4ea5a7834325c9ba33e18d8f5ed6af *** empty log message *** diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Hyperreal/HRealAbs.ML --- 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"; diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Hyperreal/HSeries.ML --- 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); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Hyperreal/HSeries.thy --- 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) diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Hyperreal/HyperDef.ML --- 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)); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Hyperreal/HyperDef.thy --- 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) & diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Hyperreal/HyperNat.ML --- 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], diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Hyperreal/HyperNat.thy --- 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) & diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Hyperreal/HyperPow.ML --- 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 diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Hyperreal/HyperPow.thy --- 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 diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Hyperreal/Lim.ML --- 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; diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Hyperreal/NSA.ML --- 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 ==> [] - hypreal_of_real x|: Infinitesimal -----------------------------------------------------*) Goal "ALL n. abs(X n + -x) < inverse(real_of_nat(Suc n)) \ -\ ==> Abs_hypreal(hyprel```{X}) + -hypreal_of_real x : Infinitesimal"; +\ ==> Abs_hypreal(hyprel``{X}) + -hypreal_of_real x : Infinitesimal"; by (auto_tac (claset() addSIs [bexI] addDs [rename_numerals FreeUltrafilterNat_inverse_real_of_posnat, FreeUltrafilterNat_all,FreeUltrafilterNat_Int] @@ -2203,21 +2203,21 @@ qed "real_seq_to_hypreal_Infinitesimal"; Goal "ALL n. abs(X n + -x) < inverse(real_of_nat(Suc n)) \ -\ ==> Abs_hypreal(hyprel```{X}) @= hypreal_of_real x"; +\ ==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x"; by (rtac (inf_close_minus_iff RS ssubst) 1); by (rtac (mem_infmal_iff RS subst) 1); by (etac real_seq_to_hypreal_Infinitesimal 1); qed "real_seq_to_hypreal_inf_close"; Goal "ALL n. abs(x + -X n) < inverse(real_of_nat(Suc n)) \ -\ ==> Abs_hypreal(hyprel```{X}) @= hypreal_of_real x"; +\ ==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x"; by (asm_full_simp_tac (simpset() addsimps [abs_minus_add_cancel, real_seq_to_hypreal_inf_close]) 1); qed "real_seq_to_hypreal_inf_close2"; Goal "ALL n. abs(X n + -Y n) < inverse(real_of_nat(Suc n)) \ -\ ==> Abs_hypreal(hyprel```{X}) + \ -\ -Abs_hypreal(hyprel```{Y}) : Infinitesimal"; +\ ==> Abs_hypreal(hyprel``{X}) + \ +\ -Abs_hypreal(hyprel``{Y}) : Infinitesimal"; by (auto_tac (claset() addSIs [bexI] addDs [rename_numerals FreeUltrafilterNat_inverse_real_of_posnat, diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Hyperreal/NatStar.ML --- 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]; diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Hyperreal/NatStar.thy --- 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}" diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Hyperreal/SEQ.ML --- 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(), diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Hyperreal/Star.ML --- 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"; diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Hyperreal/Star.thy --- 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}" diff -r c0844a30ea4e -r a7897aebbffc src/HOL/IMPP/Hoare.ML --- 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; diff -r c0844a30ea4e -r a7897aebbffc src/HOL/IMPP/Hoare.thy --- 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])} ==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}. diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Induct/LList.ML --- 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); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Induct/LList.thy --- 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)" diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Integ/Equiv.ML --- 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); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Integ/Equiv.thy --- 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)" diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Integ/IntDef.ML --- 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); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Integ/IntDef.thy --- 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 Type("IntDef.int",[])), + arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT), arith_discrete ("IntDef.int", true)]; end; diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Lattice/Bounds.thy --- 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 \ (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. \a \ A. b \ a} inf \ is_Inf A inf" proof - assume "is_Sup {b. \a \ A. b \ a} inf" - hence "is_Inf (dual `` {b. \a \ A. dual a \ dual b}) (dual inf)" + hence "is_Inf (dual ` {b. \a \ A. dual a \ dual b}) (dual inf)" by (simp only: dual_Inf dual_leq) - also have "dual `` {b. \a \ A. dual a \ dual b} = {b'. \a' \ dual `` A. a' \ b'}" + also have "dual ` {b. \a \ A. dual a \ dual b} = {b'. \a' \ dual ` A. a' \ b'}" by (auto iff: dual_ball dual_Collect) (* FIXME !? *) finally have "is_Inf \ (dual inf)" . - hence "is_Sup (dual `` A) (dual inf)" + hence "is_Sup (dual ` A) (dual inf)" by (rule Inf_Sup) thus ?thesis .. qed diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Lattice/CompleteLattice.thy --- 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 "\inf'. is_Inf A' inf'" proof - - have "\sup. is_Sup (undual `` A') sup" by (rule ex_Sup) - hence "\sup. is_Inf (dual `` undual `` A') (dual sup)" by (simp only: dual_Inf) + have "\sup. is_Sup (undual ` A') sup" by (rule ex_Sup) + hence "\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 (\A) = \(dual `` A)" +theorem dual_Meet [intro?]: "dual (\A) = \(dual ` A)" proof - - from is_Inf_Meet have "is_Sup (dual `` A) (dual (\A))" .. - hence "\(dual `` A) = dual (\A)" .. + from is_Inf_Meet have "is_Sup (dual ` A) (dual (\A))" .. + hence "\(dual ` A) = dual (\A)" .. thus ?thesis .. qed -theorem dual_Join [intro?]: "dual (\A) = \(dual `` A)" +theorem dual_Join [intro?]: "dual (\A) = \(dual ` A)" proof - - from is_Sup_Join have "is_Inf (dual `` A) (dual (\A))" .. - hence "\(dual `` A) = dual (\A)" .. + from is_Sup_Join have "is_Inf (dual ` A) (dual (\A))" .. + hence "\(dual ` A) = dual (\A)" .. thus ?thesis .. qed @@ -306,8 +306,8 @@ theorem Join_subset_mono: "A \ B \ \A \ \B" proof - assume "A \ B" - hence "dual `` A \ dual `` B" by blast - hence "\(dual `` B) \ \(dual `` A)" by (rule Meet_subset_antimono) + hence "dual ` A \ dual ` B" by blast + hence "\(dual ` B) \ \(dual ` A)" by (rule Meet_subset_antimono) hence "dual (\B) \ dual (\A)" by (simp only: dual_Join) thus ?thesis by (simp only: dual_leq) qed @@ -352,9 +352,9 @@ theorem Join_Un: "\(A \ B) = \A \ \B" proof - - have "dual (\(A \ B)) = \(dual `` A \ dual `` B)" + have "dual (\(A \ B)) = \(dual ` A \ dual ` B)" by (simp only: dual_Join image_Un) - also have "\ = \(dual `` A) \ \(dual `` B)" + also have "\ = \(dual ` A) \ \(dual ` B)" by (rule Meet_Un) also have "\ = dual (\A \ \B)" by (simp only: dual_join dual_Join) diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Lattice/Orders.thy --- 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?]: "(\x \ A. P (dual x)) = (\x' \ dual `` A. P x')" +lemma dual_ball [iff?]: "(\x \ A. P (dual x)) = (\x' \ dual ` A. P x')" proof assume a: "\x \ A. P (dual x)" - show "\x' \ dual `` A. P x'" + show "\x' \ dual ` A. P x'" proof - fix x' assume x': "x' \ dual `` A" + fix x' assume x': "x' \ dual ` A" have "undual x' \ A" proof - - from x' have "undual x' \ undual `` dual `` A" by simp + from x' have "undual x' \ undual ` dual ` A" by simp thus "undual x' \ 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: "\x' \ dual `` A. P x'" + assume a: "\x' \ dual ` A. P x'" show "\x \ A. P (dual x)" proof fix x assume "x \ A" - hence "dual x \ dual `` A" by simp + hence "dual x \ 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 "\x'. dual (undual x') = x'" by simp thus "surj dual" by (rule surjI) @@ -124,7 +124,7 @@ lemma dual_all [iff?]: "(\x. P (dual x)) = (\x'. P x')" proof - - have "(\x \ UNIV. P (dual x)) = (\x' \ dual `` UNIV. P x')" + have "(\x \ UNIV. P (dual x)) = (\x' \ dual ` UNIV. P x')" by (rule dual_ball) thus ?thesis by simp qed diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Lex/Automata.ML --- 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(); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Lex/Automata.thy --- 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 diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Lex/NA.thy --- 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 diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Lex/NAe.ML --- 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); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Lex/NAe.thy --- 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 diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Lex/RegExp2NA.thy --- 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 diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Lex/RegExp2NAe.thy --- 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 diff -r c0844a30ea4e -r a7897aebbffc src/HOL/MicroJava/BV/JVM.thy --- 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 \ types G" by auto - hence "OK `` set pTs \ err (types G)" + hence "OK ` set pTs \ err (types G)" by auto with instrs maxr isclass @@ -329,7 +329,7 @@ have "set pTs \ types G" by auto - hence "OK `` set pTs \ err (types G)" + hence "OK ` set pTs \ err (types G)" by auto with instrs isclass diff -r c0844a30ea4e -r a7897aebbffc src/HOL/MicroJava/J/JBasis.ML --- 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"; diff -r c0844a30ea4e -r a7897aebbffc src/HOL/NumberTheory/BijectionRel.ML --- 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"; diff -r c0844a30ea4e -r a7897aebbffc src/HOL/NumberTheory/EulerFermat.ML --- 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 (%a. a*x)``A : RsetR m"; +Goal "[| A : RsetR m; #0 (%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 (RRset2norRR A m)``A = (norRRset m)"; +Goal "[| #1 (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 setprod ((%a. a*x) `` BnorRset(a,m)) = \ +Goal "x~=#0 ==> a 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); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/NumberTheory/EulerFermat.thy --- 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)" diff -r c0844a30ea4e -r a7897aebbffc src/HOL/NumberTheory/WilsonBij.ML --- 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); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Real/PNat.ML --- 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"; diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Real/PNat.thy --- 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} diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Real/PRat.ML --- 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"; diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Real/PRat.thy --- 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 diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Real/PReal.ML --- 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])); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Real/RealDef.ML --- 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"; diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Real/RealDef.thy --- 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 diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Real/RealInt.ML --- 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); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Real/RealInt.thy --- 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)))})" diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/Channel.ML --- 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); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/Channel.thy --- 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 diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/ELT.ML --- 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); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/ELT.thy --- 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 diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/Extend.ML --- 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); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/Extend.thy --- 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 diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/FP.ML --- 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"; diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/Lift_prog.ML --- 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"; diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/Lift_prog.thy --- 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)" diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/PPROD.ML --- 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]; diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/PriorityAux.ML --- 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() diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/PriorityAux.thy --- 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" diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/Project.ML --- 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); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/Reach.ML --- 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; diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/Rename.ML --- 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"; diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/SubstAx.ML --- 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); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/Token.ML --- 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 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); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/UNITY/WFair.thy --- 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)" diff -r c0844a30ea4e -r a7897aebbffc src/HOL/ex/Multiquote.thy --- 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 diff -r c0844a30ea4e -r a7897aebbffc src/HOL/ex/PiSets.ML --- 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); diff -r c0844a30ea4e -r a7897aebbffc src/HOL/ex/Tarski.ML --- 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"; diff -r c0844a30ea4e -r a7897aebbffc src/HOL/ex/Tarski.thy --- 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" diff -r c0844a30ea4e -r a7897aebbffc src/HOL/ex/set.ML --- 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)); diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Cfun1.ML --- 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"; diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Cfun1.thy --- 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 *) diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Cfun2.ML --- 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 @@ (* ------------------------------------------------------------------------ *) bind_thm ("cont_cfun_arg", (cont_Rep_CFun2 RS contE RS spec RS mp)); -(* chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1)) *) +(* chain(?x1) ==> range (%i. ?fo3$(?x1 i)) <<| ?fo3$(lub (range ?x1)) *) bind_thm ("contlub_cfun_arg", (contlub_Rep_CFun2 RS contlubE RS spec RS mp)); -(* chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *) +(* chain(?x1) ==> ?fo4$(lub (range ?x1)) = lub (range (%i. ?fo4$(?x1 i))) *) (* ------------------------------------------------------------------------ *) @@ -83,7 +83,7 @@ (* monotonicity of application Rep_CFun in mixfix syntax [_]_ *) (* ------------------------------------------------------------------------ *) -Goal "f1 << f2 ==> f1`x << f2`x"; +Goal "f1 << f2 ==> f1$x << f2$x"; by (res_inst_tac [("x","x")] spec 1); by (rtac (less_fun RS subst) 1); by (etac (monofun_Rep_CFun1 RS monofunE RS spec RS spec RS mp) 1); @@ -91,20 +91,20 @@ bind_thm ("monofun_cfun_arg", monofun_Rep_CFun2 RS monofunE RS spec RS spec RS mp); -(* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1 *) +(* ?x2 << ?x1 ==> ?fo5$?x2 << ?fo5$?x1 *) (* ------------------------------------------------------------------------ *) (* monotonicity of Rep_CFun in both arguments in mixfix syntax [_]_ *) (* ------------------------------------------------------------------------ *) -Goal "[|f1< f1`x1 << f2`x2"; +Goal "[|f1< f1$x1 << f2$x2"; by (rtac trans_less 1); by (etac monofun_cfun_arg 1); by (etac monofun_cfun_fun 1); qed "monofun_cfun"; -Goal "f`x = UU ==> f`UU = UU"; +Goal "f$x = UU ==> f$UU = UU"; by (rtac (eq_UU_iff RS iffD2) 1); by (etac subst 1); by (rtac (minimal RS monofun_cfun_arg) 1); @@ -116,13 +116,13 @@ (* use MF2 lemmas from Cont.ML *) (* ------------------------------------------------------------------------ *) -Goal "chain(Y) ==> chain(%i. f`(Y i))"; +Goal "chain(Y) ==> chain(%i. f$(Y i))"; by (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1); qed "ch2ch_Rep_CFunR"; bind_thm ("ch2ch_Rep_CFunL", monofun_Rep_CFun1 RS ch2ch_MF2L); -(* chain(?F) ==> chain (%i. ?F i`?x) *) +(* chain(?F) ==> chain (%i. ?F i$?x) *) (* ------------------------------------------------------------------------ *) @@ -130,7 +130,7 @@ (* use MF2 lemmas from Cont.ML *) (* ------------------------------------------------------------------------ *) -Goal "chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))"; +Goal "chain(F) ==> monofun(% x. lub(range(% j.(F j)$x)))"; by (rtac lub_MF2_mono 1); by (rtac monofun_Rep_CFun1 1); by (rtac (monofun_Rep_CFun2 RS allI) 1); @@ -143,8 +143,8 @@ (* ------------------------------------------------------------------------ *) Goal "[| chain(F); chain(Y) |] ==>\ -\ lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\ -\ lub(range(%i. lub(range(%j. F(j)`(Y i)))))"; +\ lub(range(%j. lub(range(%i. F(j)$(Y i))))) =\ +\ lub(range(%i. lub(range(%j. F(j)$(Y i)))))"; by (rtac ex_lubMF2 1); by (rtac monofun_Rep_CFun1 1); by (rtac (monofun_Rep_CFun2 RS allI) 1); @@ -156,7 +156,7 @@ (* the lub of a chain of cont. functions is continuous *) (* ------------------------------------------------------------------------ *) -Goal "chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))"; +Goal "chain(F) ==> cont(% x. lub(range(% j. F(j)$x)))"; by (rtac monocontlub2cont 1); by (etac lub_cfun_mono 1); by (rtac contlubI 1); @@ -171,7 +171,7 @@ (* type 'a -> 'b is chain complete *) (* ------------------------------------------------------------------------ *) -Goal "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))"; +Goal "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)$x)))"; by (rtac is_lubI 1); by (rtac ub_rangeI 1); by (stac less_cfun 1); @@ -189,7 +189,7 @@ bind_thm ("thelub_cfun", lub_cfun RS thelubI); (* -chain(?CCF1) ==> lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x))) +chain(?CCF1) ==> lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i$x))) *) Goal "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x"; @@ -202,7 +202,7 @@ (* Extensionality in 'a -> 'b *) (* ------------------------------------------------------------------------ *) -val prems = Goal "(!!x. f`x = g`x) ==> f = g"; +val prems = Goal "(!!x. f$x = g$x) ==> f = g"; by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1); by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1); by (res_inst_tac [("f","Abs_CFun")] arg_cong 1); @@ -227,7 +227,7 @@ (* Extenionality wrt. << in 'a -> 'b *) (* ------------------------------------------------------------------------ *) -val prems = Goal "(!!x. f`x << g`x) ==> f << g"; +val prems = Goal "(!!x. f$x << g$x) ==> f << g"; by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1); by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1); by (rtac semi_monofun_Abs_CFun 1); diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Cfun3.ML --- a/src/HOLCF/Cfun3.ML Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Cfun3.ML Tue Jan 09 15:32:27 2001 +0100 @@ -47,7 +47,7 @@ Goal "chain(FY) ==>\ -\ lub(range FY)`x = lub(range (%i. FY(i)`x))"; +\ lub(range FY)$x = lub(range (%i. FY(i)$x))"; by (rtac trans 1); by (etac (contlub_Rep_CFun1 RS contlubE RS spec RS mp RS fun_cong) 1); by (stac thelub_fun 1); @@ -58,7 +58,7 @@ Goal "chain(FY) ==>\ -\ range(%i. FY(i)`x) <<| lub(range FY)`x"; +\ range(%i. FY(i)$x) <<| lub(range FY)$x"; by (rtac thelubE 1); by (etac ch2ch_Rep_CFunL 1); by (etac (contlub_cfun_fun RS sym) 1); @@ -71,7 +71,7 @@ Goal "[|chain(FY);chain(TY)|] ==>\ -\ (lub(range FY))`(lub(range TY)) = lub(range(%i. FY(i)`(TY i)))"; +\ (lub(range FY))$(lub(range TY)) = lub(range(%i. FY(i)$(TY i)))"; by (rtac contlub_CF2 1); by (rtac cont_Rep_CFun1 1); by (rtac allI 1); @@ -82,7 +82,7 @@ Goal "[|chain(FY);chain(TY)|] ==>\ -\ range(%i.(FY i)`(TY i)) <<| (lub (range FY))`(lub(range TY))"; +\ range(%i.(FY i)$(TY i)) <<| (lub (range FY))$(lub(range TY))"; by (rtac thelubE 1); by (rtac (monofun_Rep_CFun1 RS ch2ch_MF2LR) 1); by (rtac allI 1); @@ -98,7 +98,7 @@ (* cont2cont lemma for Rep_CFun *) (* ------------------------------------------------------------------------ *) -Goal "[|cont(%x. ft x);cont(%x. tt x)|] ==> cont(%x. (ft x)`(tt x))"; +Goal "[|cont(%x. ft x);cont(%x. tt x)|] ==> cont(%x. (ft x)$(tt x))"; by (best_tac (claset() addIs [cont2cont_app2, cont_const, cont_Rep_CFun1, cont_Rep_CFun2]) 1); qed "cont2cont_Rep_CFun"; @@ -162,7 +162,7 @@ (* function application _[_] is strict in its first arguments *) (* ------------------------------------------------------------------------ *) -Goal "(UU::'a::cpo->'b)`x = (UU::'b)"; +Goal "(UU::'a::cpo->'b)$x = (UU::'b)"; by (stac inst_cfun_pcpo 1); by (stac beta_cfun 1); by (Simp_tac 1); @@ -180,7 +180,7 @@ qed "Istrictify1"; Goalw [Istrictify_def] - "~x=UU ==> Istrictify(f)(x)=f`x"; + "~x=UU ==> Istrictify(f)(x)=f$x"; by (Asm_simp_tac 1); qed "Istrictify2"; @@ -251,7 +251,7 @@ by (asm_simp_tac (simpset() addsimps [Istrictify1, chain_UU_I_inverse, chain_UU_I, Istrictify1]) 1); by (stac Istrictify2 1); by (atac 1); -by (res_inst_tac [("s","lub(range(%i. f`(Y i)))")] trans 1); +by (res_inst_tac [("s","lub(range(%i. f$(Y i)))")] trans 1); by (rtac contlub_cfun_arg 1); by (atac 1); by (rtac lub_equal2 1); @@ -271,7 +271,7 @@ (monofun_Istrictify2 RS monocontlub2cont)); -Goalw [strictify_def] "strictify`f`UU=UU"; +Goalw [strictify_def] "strictify$f$UU=UU"; by (stac beta_cfun 1); by (simp_tac (simpset() addsimps [cont_Istrictify2,cont_Istrictify1, cont2cont_CF1L]) 1); by (stac beta_cfun 1); @@ -279,7 +279,7 @@ by (rtac Istrictify1 1); qed "strictify1"; -Goalw [strictify_def] "~x=UU ==> strictify`f`x=f`x"; +Goalw [strictify_def] "~x=UU ==> strictify$f$x=f$x"; by (stac beta_cfun 1); by (simp_tac (simpset() addsimps [cont_Istrictify2,cont_Istrictify1, cont2cont_CF1L]) 1); by (stac beta_cfun 1); @@ -307,7 +307,7 @@ (* ------------------------------------------------------------------------ *) Goal "chain (Y::nat => 'a::cpo->'b::chfin) \ -\ ==> !s. ? n. lub(range(Y))`s = Y n`s"; +\ ==> !s. ? n. lub(range(Y))$s = Y n$s"; by (rtac allI 1); by (stac contlub_cfun_fun 1); by (atac 1); @@ -320,21 +320,21 @@ (* ------------------------------------------------------------------------ *) Goal -"!!f g.[|!y. f`(g`y)=(y::'b) ; !x. g`(f`x)=(x::'a) |] \ -\ ==> f`UU=UU & g`UU=UU"; +"!!f g.[|!y. f$(g$y)=(y::'b) ; !x. g$(f$x)=(x::'a) |] \ +\ ==> f$UU=UU & g$UU=UU"; by (rtac conjI 1); by (rtac UU_I 1); -by (res_inst_tac [("s","f`(g`(UU::'b))"),("t","UU::'b")] subst 1); +by (res_inst_tac [("s","f$(g$(UU::'b))"),("t","UU::'b")] subst 1); by (etac spec 1); by (rtac (minimal RS monofun_cfun_arg) 1); by (rtac UU_I 1); -by (res_inst_tac [("s","g`(f`(UU::'a))"),("t","UU::'a")] subst 1); +by (res_inst_tac [("s","g$(f$(UU::'a))"),("t","UU::'a")] subst 1); by (etac spec 1); by (rtac (minimal RS monofun_cfun_arg) 1); qed "iso_strict"; -Goal "[|!x. rep`(ab`x)=x;!y. ab`(rep`y)=y; z~=UU|] ==> rep`z ~= UU"; +Goal "[|!x. rep$(ab$x)=x;!y. ab$(rep$y)=y; z~=UU|] ==> rep$z ~= UU"; by (etac contrapos_nn 1); by (dres_inst_tac [("f","ab")] cfun_arg_cong 1); by (etac box_equals 1); @@ -343,7 +343,7 @@ by (atac 1); qed "isorep_defined"; -Goal "[|!x. rep`(ab`x) = x;!y. ab`(rep`y)=y ; z~=UU|] ==> ab`z ~= UU"; +Goal "[|!x. rep$(ab$x) = x;!y. ab$(rep$y)=y ; z~=UU|] ==> ab$z ~= UU"; by (etac contrapos_nn 1); by (dres_inst_tac [("f","rep")] cfun_arg_cong 1); by (etac box_equals 1); @@ -357,19 +357,19 @@ (* ------------------------------------------------------------------------ *) Goal "!!f g.[|! Y::nat=>'a. chain Y --> (? n. max_in_chain n Y); \ -\ !y. f`(g`y)=(y::'b) ; !x. g`(f`x)=(x::'a::chfin) |] \ +\ !y. f$(g$y)=(y::'b) ; !x. g$(f$x)=(x::'a::chfin) |] \ \ ==> ! Y::nat=>'b. chain Y --> (? n. max_in_chain n Y)"; by (rewtac max_in_chain_def); by (strip_tac 1); by (rtac exE 1); -by (res_inst_tac [("P","chain(%i. g`(Y i))")] mp 1); +by (res_inst_tac [("P","chain(%i. g$(Y i))")] mp 1); by (etac spec 1); by (etac ch2ch_Rep_CFunR 1); by (rtac exI 1); by (strip_tac 1); -by (res_inst_tac [("s","f`(g`(Y x))"),("t","Y(x)")] subst 1); +by (res_inst_tac [("s","f$(g$(Y x))"),("t","Y(x)")] subst 1); by (etac spec 1); -by (res_inst_tac [("s","f`(g`(Y j))"),("t","Y(j)")] subst 1); +by (res_inst_tac [("s","f$(g$(Y j))"),("t","Y(j)")] subst 1); by (etac spec 1); by (rtac cfun_arg_cong 1); by (rtac mp 1); @@ -379,25 +379,25 @@ Goal "!!f g.[|!x y::'a. x< x=UU | x=y; \ -\ !y. f`(g`y)=(y::'b); !x. g`(f`x)=(x::'a)|] ==> !x y::'b. x< x=UU | x=y"; +\ !y. f$(g$y)=(y::'b); !x. g$(f$x)=(x::'a)|] ==> !x y::'b. x< x=UU | x=y"; by (strip_tac 1); by (rtac disjE 1); -by (res_inst_tac [("P","g`x< f`(UU::'a)=(UU::'b) | (!z. f`(z::'a)=c)"; -by (case_tac "f`(x::'a)=(UU::'b)" 1); +Goal "f$(x::'a)=(c::'b::flat) ==> f$(UU::'a)=(UU::'b) | (!z. f$(z::'a)=c)"; +by (case_tac "f$(x::'a)=(UU::'b)" 1); by (rtac disjI1 1); by (rtac UU_I 1); -by (res_inst_tac [("s","f`(x)"),("t","UU::'b")] subst 1); +by (res_inst_tac [("s","f$(x)"),("t","UU::'b")] subst 1); by (atac 1); by (rtac (minimal RS monofun_cfun_arg) 1); -by (case_tac "f`(UU::'a)=(UU::'b)" 1); +by (case_tac "f$(UU::'a)=(UU::'b)" 1); by (etac disjI1 1); by (rtac disjI2 1); by (rtac allI 1); by (hyp_subst_tac 1); -by (res_inst_tac [("a","f`(UU::'a)")] (refl RS box_equals) 1); +by (res_inst_tac [("a","f$(UU::'a)")] (refl RS box_equals) 1); by (res_inst_tac [("fo5","f")] ((minimal RS monofun_cfun_arg) RS (ax_flat RS spec RS spec RS mp) RS disjE) 1); by (contr_tac 1); by (atac 1); @@ -433,13 +433,13 @@ (* ------------------------------------------------------------------------ *) -Goalw [ID_def] "ID`x=x"; +Goalw [ID_def] "ID$x=x"; by (stac beta_cfun 1); by (rtac cont_id 1); by (rtac refl 1); qed "ID1"; -Goalw [oo_def] "(f oo g)=(LAM x. f`(g`x))"; +Goalw [oo_def] "(f oo g)=(LAM x. f$(g$x))"; by (stac beta_cfun 1); by (Simp_tac 1); by (stac beta_cfun 1); @@ -447,7 +447,7 @@ by (rtac refl 1); qed "cfcomp1"; -Goal "(f oo g)`x=f`(g`x)"; +Goal "(f oo g)$x=f$(g$x)"; by (stac cfcomp1 1); by (stac beta_cfun 1); by (Simp_tac 1); @@ -481,7 +481,7 @@ Goal "f oo (g oo h) = (f oo g) oo h"; by (rtac ext_cfun 1); -by (res_inst_tac [("s","f`(g`(h`x))")] trans 1); +by (res_inst_tac [("s","f$(g$(h$x))")] trans 1); by (stac cfcomp2 1); by (stac cfcomp2 1); by (rtac refl 1); diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Cfun3.thy --- a/src/HOLCF/Cfun3.thy Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Cfun3.thy Tue Jan 09 15:32:27 2001 +0100 @@ -19,7 +19,7 @@ strictify :: "('a->'b)->'a->'b" defs -Istrictify_def "Istrictify f x == if x=UU then UU else f`x" +Istrictify_def "Istrictify f x == if x=UU then UU else f$x" strictify_def "strictify == (LAM f x. Istrictify f x)" consts @@ -28,11 +28,11 @@ syntax "@oo" :: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100) -translations "f1 oo f2" == "cfcomp`f1`f2" +translations "f1 oo f2" == "cfcomp$f1$f2" defs ID_def "ID ==(LAM x. x)" - oo_def "cfcomp == (LAM f g x. f`(g`x))" + oo_def "cfcomp == (LAM f g x. f$(g$x))" end diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Cprod3.ML --- a/src/HOLCF/Cprod3.ML Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Cprod3.ML Tue Jan 09 15:32:27 2001 +0100 @@ -125,7 +125,7 @@ (* ------------------------------------------------------------------------ *) Goalw [cpair_def] - "(LAM x y.(x,y))`a`b = (a,b)"; + "(LAM x y.(x,y))$a$b = (a,b)"; by (stac beta_cfun 1); by (simp_tac (simpset() addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1); by (stac beta_cfun 1); @@ -170,7 +170,7 @@ qed "cprodE"; Goalw [cfst_def,cpair_def] - "cfst`=x"; + "cfst$=x"; by (stac beta_cfun_cprod 1); by (stac beta_cfun 1); by (rtac cont_fst 1); @@ -178,22 +178,22 @@ qed "cfst2"; Goalw [csnd_def,cpair_def] - "csnd`=y"; + "csnd$=y"; by (stac beta_cfun_cprod 1); by (stac beta_cfun 1); by (rtac cont_snd 1); by (Simp_tac 1); qed "csnd2"; -Goal "cfst`UU = UU"; +Goal "cfst$UU = UU"; by (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,cfst2]) 1); qed "cfst_strict"; -Goal "csnd`UU = UU"; +Goal "csnd$UU = UU"; by (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,csnd2]) 1); qed "csnd_strict"; -Goalw [cfst_def,csnd_def,cpair_def] " = p"; +Goalw [cfst_def,csnd_def,cpair_def] " = p"; by (stac beta_cfun_cprod 1); by (stac beta_cfun 1); by (rtac cont_snd 1); @@ -212,7 +212,7 @@ Goalw [cfst_def,csnd_def,cpair_def] "[|chain(S)|] ==> range(S) <<| \ -\ <(lub(range(%i. cfst`(S i)))) , lub(range(%i. csnd`(S i)))>"; +\ <(lub(range(%i. cfst$(S i)))) , lub(range(%i. csnd$(S i)))>"; by (stac beta_cfun_cprod 1); by (stac (beta_cfun RS ext) 1); by (rtac cont_snd 1); @@ -226,17 +226,17 @@ (* chain ?S1 ==> lub (range ?S1) = - " + " *) Goalw [csplit_def] - "csplit`f` = f`x`y"; + "csplit$f$ = f$x$y"; by (stac beta_cfun 1); by (Simp_tac 1); by (simp_tac (simpset() addsimps [cfst2,csnd2]) 1); qed "csplit2"; Goalw [csplit_def] - "csplit`cpair`z=z"; + "csplit$cpair$z=z"; by (stac beta_cfun 1); by (Simp_tac 1); by (simp_tac (simpset() addsimps [surjective_pairing_Cprod2]) 1); diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Cprod3.thy --- a/src/HOLCF/Cprod3.thy Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Cprod3.thy Tue Jan 09 15:32:27 2001 +0100 @@ -22,13 +22,13 @@ translations "" == ">" - "" == "cpair`x`y" + "" == "cpair$x$y" defs cpair_def "cpair == (LAM x y.(x,y))" cfst_def "cfst == (LAM p. fst(p))" csnd_def "csnd == (LAM p. snd(p))" -csplit_def "csplit == (LAM f p. f`(cfst`p)`(csnd`p))" +csplit_def "csplit == (LAM f p. f$(cfst$p)$(csnd$p))" @@ -43,7 +43,7 @@ constdefs CLet :: "'a -> ('a -> 'b) -> 'b" - "CLet == LAM s f. f`s" + "CLet == LAM s f. f$s" (* syntax for Let *) @@ -59,7 +59,7 @@ translations "_CLet (_Cbinds b bs) e" == "_CLet b (_CLet bs e)" - "Let x = a in e" == "CLet`a`(LAM x. e)" + "Let x = a in e" == "CLet$a$(LAM x. e)" (* syntax for LAM .e *) @@ -68,9 +68,9 @@ "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3LAM <_>./ _)" [0, 10] 10) translations - "LAM .b" == "csplit`(LAM x. LAM .b)" - "LAM . LAM zs. b" <= "csplit`(LAM x y zs. b)" - "LAM .b" == "csplit`(LAM x y. b)" + "LAM .b" == "csplit$(LAM x. LAM .b)" + "LAM . LAM zs. b" <= "csplit$(LAM x y zs. b)" + "LAM .b" == "csplit$(LAM x y. b)" syntax (symbols) "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3\\()<_>./ _)" [0, 10] 10) diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Fix.ML --- a/src/HOLCF/Fix.ML Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Fix.ML Tue Jan 09 15:32:27 2001 +0100 @@ -10,7 +10,7 @@ (* derive inductive properties of iterate from primitive recursion *) (* ------------------------------------------------------------------------ *) -Goal "iterate (Suc n) F x = iterate n F (F`x)"; +Goal "iterate (Suc n) F x = iterate n F (F$x)"; by (induct_tac "n" 1); by Auto_tac; qed "iterate_Suc2"; @@ -20,7 +20,7 @@ (* This property is essential since monotonicity of iterate makes no sense *) (* ------------------------------------------------------------------------ *) -Goalw [chain] "x << F`x ==> chain (%i. iterate i F x)"; +Goalw [chain] "x << F$x ==> chain (%i. iterate i F x)"; by (strip_tac 1); by (induct_tac "i" 1); by Auto_tac; @@ -40,7 +40,7 @@ (* ------------------------------------------------------------------------ *) -Goalw [Ifix_def] "Ifix F =F`(Ifix F)"; +Goalw [Ifix_def] "Ifix F =F$(Ifix F)"; by (stac contlub_cfun_arg 1); by (rtac chain_iterate 1); by (rtac antisym_less 1); @@ -61,7 +61,7 @@ qed "Ifix_eq"; -Goalw [Ifix_def] "F`x=x ==> Ifix(F) << x"; +Goalw [Ifix_def] "F$x=x ==> Ifix(F) << x"; by (rtac is_lub_thelub 1); by (rtac chain_iterate 1); by (rtac ub_rangeI 1); @@ -250,19 +250,19 @@ (* propagate properties of Ifix to its continuous counterpart *) (* ------------------------------------------------------------------------ *) -Goalw [fix_def] "fix`F = F`(fix`F)"; +Goalw [fix_def] "fix$F = F$(fix$F)"; by (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1); by (rtac Ifix_eq 1); qed "fix_eq"; -Goalw [fix_def] "F`x = x ==> fix`F << x"; +Goalw [fix_def] "F$x = x ==> fix$F << x"; by (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1); by (etac Ifix_least 1); qed "fix_least"; Goal -"[| F`x = x; !z. F`z = z --> x << z |] ==> x = fix`F"; +"[| F$x = x; !z. F$z = z --> x << z |] ==> x = fix$F"; by (rtac antisym_less 1); by (etac allE 1); by (etac mp 1); @@ -271,22 +271,22 @@ qed "fix_eqI"; -Goal "f == fix`F ==> f = F`f"; +Goal "f == fix$F ==> f = F$f"; by (asm_simp_tac (simpset() addsimps [fix_eq RS sym]) 1); qed "fix_eq2"; -Goal "f == fix`F ==> f`x = F`f`x"; +Goal "f == fix$F ==> f$x = F$f$x"; by (etac (fix_eq2 RS cfun_fun_cong) 1); qed "fix_eq3"; fun fix_tac3 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i)); -Goal "f = fix`F ==> f = F`f"; +Goal "f = fix$F ==> f = F$f"; by (hyp_subst_tac 1); by (rtac fix_eq 1); qed "fix_eq4"; -Goal "f = fix`F ==> f`x = F`f`x"; +Goal "f = fix$F ==> f$x = F$f$x"; by (rtac trans 1); by (etac (fix_eq4 RS cfun_fun_cong) 1); by (rtac refl 1); @@ -294,7 +294,7 @@ fun fix_tac5 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq5) i)); -(* proves the unfolding theorem for function equations f = fix`... *) +(* proves the unfolding theorem for function equations f = fix$... *) fun fix_prover thy fixeq s = prove_goal thy s (fn prems => [ (rtac trans 1), (rtac (fixeq RS fix_eq4) 1), @@ -303,7 +303,7 @@ (Simp_tac 1) ]); -(* proves the unfolding theorem for function definitions f == fix`... *) +(* proves the unfolding theorem for function definitions f == fix$... *) fun fix_prover2 thy fixdef s = prove_goal thy s (fn prems => [ (rtac trans 1), (rtac (fix_eq2) 1), @@ -335,7 +335,7 @@ (* direct connection between fix and iteration without Ifix *) (* ------------------------------------------------------------------------ *) -Goalw [fix_def] "fix`F = lub(range(%i. iterate i F UU))"; +Goalw [fix_def] "fix$F = lub(range(%i. iterate i F UU))"; by (fold_goals_tac [Ifix_def]); by (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1); qed "fix_def2"; @@ -379,7 +379,7 @@ (* ------------------------------------------------------------------------ *) val major::prems = Goal - "[| adm(P); P(UU); !!x. P(x) ==> P(F`x)|] ==> P(fix`F)"; + "[| adm(P); P(UU); !!x. P(x) ==> P(F$x)|] ==> P(fix$F)"; by (stac fix_def2 1); by (rtac (major RS admD) 1); by (rtac chain_iterate 1); @@ -389,8 +389,8 @@ by (asm_simp_tac (simpset() addsimps (iterate_Suc::prems)) 1); qed "fix_ind"; -val prems = Goal "[| f == fix`F; adm(P); \ -\ P(UU); !!x. P(x) ==> P(F`x)|] ==> P f"; +val prems = Goal "[| f == fix$F; adm(P); \ +\ P(UU); !!x. P(x) ==> P(F$x)|] ==> P f"; by (cut_facts_tac prems 1); by (asm_simp_tac HOL_ss 1); by (etac fix_ind 1); @@ -402,7 +402,7 @@ (* computational induction for weak admissible formulae *) (* ------------------------------------------------------------------------ *) -Goal "[| admw(P); !n. P(iterate n F UU)|] ==> P(fix`F)"; +Goal "[| admw(P); !n. P(iterate n F UU)|] ==> P(fix$F)"; by (stac fix_def2 1); by (rtac (admw_def2 RS iffD1 RS spec RS mp) 1); by (atac 1); @@ -410,7 +410,7 @@ by (etac spec 1); qed "wfix_ind"; -Goal "[| f == fix`F; admw(P); \ +Goal "[| f == fix$F; admw(P); \ \ !n. P(iterate n F UU) |] ==> P f"; by (asm_simp_tac HOL_ss 1); by (etac wfix_ind 1); @@ -440,7 +440,7 @@ (* some lemmata for functions with flat/chfin domain/range types *) (* ------------------------------------------------------------------------ *) -val _ = goalw thy [adm_def] "adm (%(u::'a::cpo->'b::chfin). P(u`s))"; +val _ = goalw thy [adm_def] "adm (%(u::'a::cpo->'b::chfin). P(u$s))"; by (strip_tac 1); by (dtac chfin_Rep_CFunR 1); by (eres_inst_tac [("x","s")] allE 1); diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Fix.thy --- a/src/HOLCF/Fix.thy Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Fix.thy Tue Jan 09 15:32:27 2001 +0100 @@ -20,7 +20,7 @@ primrec iterate_0 "iterate 0 F x = x" - iterate_Suc "iterate (Suc n) F x = F`(iterate n F x)" + iterate_Suc "iterate (Suc n) F x = F$(iterate n F x)" defs diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Lift.ML --- a/src/HOLCF/Lift.ML Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Lift.ML Tue Jan 09 15:32:27 2001 +0100 @@ -81,25 +81,25 @@ (* ---------------------------------------------------------- *) -Goal "flift1 f`(Def x) = (f x)"; +Goal "flift1 f$(Def x) = (f x)"; by (simp_tac (simpset() addsimps [flift1_def]) 1); qed"flift1_Def"; -Goal "flift2 f`(Def x) = Def (f x)"; +Goal "flift2 f$(Def x) = Def (f x)"; by (simp_tac (simpset() addsimps [flift2_def]) 1); qed"flift2_Def"; -Goal "flift1 f`UU = UU"; +Goal "flift1 f$UU = UU"; by (simp_tac (simpset() addsimps [flift1_def]) 1); qed"flift1_UU"; -Goal "flift2 f`UU = UU"; +Goal "flift2 f$UU = UU"; by (simp_tac (simpset() addsimps [flift2_def]) 1); qed"flift2_UU"; Addsimps [flift1_Def,flift2_Def,flift1_UU,flift2_UU]; -Goal "x~=UU ==> (flift2 f)`x~=UU"; +Goal "x~=UU ==> (flift2 f)$x~=UU"; by (def_tac 1); qed"flift2_nUU"; diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Lift3.ML --- a/src/HOLCF/Lift3.ML Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Lift3.ML Tue Jan 09 15:32:27 2001 +0100 @@ -134,13 +134,13 @@ (* Two specific lemmas for the combination of LCF and HOL terms *) -Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)"; +Goal "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s)"; by (rtac cont2cont_CF1L 1); by (REPEAT (resolve_tac cont_lemmas1 1)); by Auto_tac; qed"cont_Rep_CFun_app"; -Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)"; +Goal "[|cont g; cont f|] ==> cont(%x. ((f x)$(g x)) s t)"; by (rtac cont2cont_CF1L 1); by (etac cont_Rep_CFun_app 1); by (assume_tac 1); diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Lift3.thy --- a/src/HOLCF/Lift3.thy Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Lift3.thy Tue Jan 09 15:32:27 2001 +0100 @@ -29,9 +29,9 @@ Undef => UU | Def y => Def (f y)))" liftpair_def - "liftpair x == (case (cfst`x) of + "liftpair x == (case (cfst$x) of Undef => UU - | Def x1 => (case (csnd`x) of + | Def x1 => (case (csnd$x) of Undef => UU | Def x2 => Def (x1,x2)))" diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Sprod3.ML --- a/src/HOLCF/Sprod3.ML Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Sprod3.ML Tue Jan 09 15:32:27 2001 +0100 @@ -240,7 +240,7 @@ (* ------------------------------------------------------------------------ *) Goalw [spair_def] - "(LAM x y. Ispair x y)`a`b = Ispair a b"; + "(LAM x y. Ispair x y)$a$b = Ispair a b"; by (stac beta_cfun 1); by (simp_tac (simpset() addsimps [cont_Ispair2, cont_Ispair1, cont2cont_CF1L]) 1); by (stac beta_cfun 1); @@ -343,7 +343,7 @@ Goalw [sfst_def] - "p=UU==>sfst`p=UU"; + "p=UU==>sfst$p=UU"; by (stac beta_cfun 1); by (rtac cont_Isfst 1); by (rtac strict_Isfst 1); @@ -352,7 +352,7 @@ qed "strict_sfst"; Goalw [sfst_def,spair_def] - "sfst`(:UU,y:) = UU"; + "sfst$(:UU,y:) = UU"; by (stac beta_cfun_sprod 1); by (stac beta_cfun 1); by (rtac cont_Isfst 1); @@ -360,7 +360,7 @@ qed "strict_sfst1"; Goalw [sfst_def,spair_def] - "sfst`(:x,UU:) = UU"; + "sfst$(:x,UU:) = UU"; by (stac beta_cfun_sprod 1); by (stac beta_cfun 1); by (rtac cont_Isfst 1); @@ -368,7 +368,7 @@ qed "strict_sfst2"; Goalw [ssnd_def] - "p=UU==>ssnd`p=UU"; + "p=UU==>ssnd$p=UU"; by (stac beta_cfun 1); by (rtac cont_Issnd 1); by (rtac strict_Issnd 1); @@ -377,7 +377,7 @@ qed "strict_ssnd"; Goalw [ssnd_def,spair_def] - "ssnd`(:UU,y:) = UU"; + "ssnd$(:UU,y:) = UU"; by (stac beta_cfun_sprod 1); by (stac beta_cfun 1); by (rtac cont_Issnd 1); @@ -385,7 +385,7 @@ qed "strict_ssnd1"; Goalw [ssnd_def,spair_def] - "ssnd`(:x,UU:) = UU"; + "ssnd$(:x,UU:) = UU"; by (stac beta_cfun_sprod 1); by (stac beta_cfun 1); by (rtac cont_Issnd 1); @@ -393,7 +393,7 @@ qed "strict_ssnd2"; Goalw [sfst_def,spair_def] - "y~=UU ==>sfst`(:x,y:)=x"; + "y~=UU ==>sfst$(:x,y:)=x"; by (stac beta_cfun_sprod 1); by (stac beta_cfun 1); by (rtac cont_Isfst 1); @@ -401,7 +401,7 @@ qed "sfst2"; Goalw [ssnd_def,spair_def] - "x~=UU ==>ssnd`(:x,y:)=y"; + "x~=UU ==>ssnd$(:x,y:)=y"; by (stac beta_cfun_sprod 1); by (stac beta_cfun 1); by (rtac cont_Issnd 1); @@ -410,7 +410,7 @@ Goalw [sfst_def,ssnd_def,spair_def] - "p~=UU ==> sfst`p ~=UU & ssnd`p ~=UU"; + "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU"; by (stac beta_cfun 1); by (rtac cont_Issnd 1); by (stac beta_cfun 1); @@ -420,7 +420,7 @@ by (atac 1); qed "defined_sfstssnd"; -Goalw [sfst_def,ssnd_def,spair_def] "(:sfst`p , ssnd`p:) = p"; +Goalw [sfst_def,ssnd_def,spair_def] "(:sfst$p , ssnd$p:) = p"; by (stac beta_cfun_sprod 1); by (stac beta_cfun 1); by (rtac cont_Issnd 1); @@ -431,7 +431,7 @@ Goalw [sfst_def,ssnd_def,spair_def] "chain(S) ==> range(S) <<| \ -\ (: lub(range(%i. sfst`(S i))), lub(range(%i. ssnd`(S i))) :)"; +\ (: lub(range(%i. sfst$(S i))), lub(range(%i. ssnd$(S i))) :)"; by (stac beta_cfun_sprod 1); by (stac (beta_cfun RS ext) 1); by (rtac cont_Issnd 1); @@ -445,11 +445,11 @@ (* "chain ?S1 ==> lub (range ?S1) = - (:lub (range (%i. sfst`(?S1 i))), lub (range (%i. ssnd`(?S1 i))):)" : thm + (:lub (range (%i. sfst$(?S1 i))), lub (range (%i. ssnd$(?S1 i))):)" : thm *) Goalw [ssplit_def] - "ssplit`f`UU=UU"; + "ssplit$f$UU=UU"; by (stac beta_cfun 1); by (Simp_tac 1); by (stac strictify1 1); @@ -457,7 +457,7 @@ qed "ssplit1"; Goalw [ssplit_def] - "[|x~=UU;y~=UU|] ==> ssplit`f`(:x,y:)= f`x`y"; + "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y"; by (stac beta_cfun 1); by (Simp_tac 1); by (stac strictify2 1); @@ -475,7 +475,7 @@ Goalw [ssplit_def] - "ssplit`spair`z=z"; + "ssplit$spair$z=z"; by (stac beta_cfun 1); by (Simp_tac 1); by (case_tac "z=UU" 1); diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Sprod3.thy --- a/src/HOLCF/Sprod3.thy Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Sprod3.thy Tue Jan 09 15:32:27 2001 +0100 @@ -21,12 +21,12 @@ translations "(:x, y, z:)" == "(:x, (:y, z:):)" - "(:x, y:)" == "spair`x`y" + "(:x, y:)" == "spair$x$y" defs spair_def "spair == (LAM x y. Ispair x y)" sfst_def "sfst == (LAM p. Isfst p)" ssnd_def "ssnd == (LAM p. Issnd p)" -ssplit_def "ssplit == (LAM f. strictify`(LAM p. f`(sfst`p)`(ssnd`p)))" +ssplit_def "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))" end diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Ssum0.ML --- a/src/HOLCF/Ssum0.ML Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Ssum0.ML Tue Jan 09 15:32:27 2001 +0100 @@ -237,7 +237,7 @@ Goalw [Iwhen_def] - "x~=UU ==> Iwhen f g (Isinl x) = f`x"; + "x~=UU ==> Iwhen f g (Isinl x) = f$x"; by (rtac some_equality 1); by (fast_tac HOL_cs 2); by (rtac conjI 1); @@ -260,7 +260,7 @@ qed "Iwhen2"; Goalw [Iwhen_def] - "y~=UU ==> Iwhen f g (Isinr y) = g`y"; + "y~=UU ==> Iwhen f g (Isinr y) = g$y"; by (rtac some_equality 1); by (fast_tac HOL_cs 2); by (rtac conjI 1); diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Ssum0.thy --- a/src/HOLCF/Ssum0.thy Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Ssum0.thy Tue Jan 09 15:32:27 2001 +0100 @@ -31,7 +31,7 @@ Iwhen_def "Iwhen(f)(g)(s) == @z. (s=Isinl(UU) --> z=UU) - &(!a. a~=UU & s=Isinl(a) --> z=f`a) - &(!b. b~=UU & s=Isinr(b) --> z=g`b)" + &(!a. a~=UU & s=Isinl(a) --> z=f$a) + &(!b. b~=UU & s=Isinr(b) --> z=g$b)" end diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Ssum3.ML --- a/src/HOLCF/Ssum3.ML Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Ssum3.ML Tue Jan 09 15:32:27 2001 +0100 @@ -319,43 +319,43 @@ (* continuous versions of lemmas for 'a ++ 'b *) (* ------------------------------------------------------------------------ *) -Goalw [sinl_def] "sinl`UU =UU"; +Goalw [sinl_def] "sinl$UU =UU"; by (simp_tac (Ssum0_ss addsimps [cont_Isinl]) 1); by (rtac (inst_ssum_pcpo RS sym) 1); qed "strict_sinl"; Addsimps [strict_sinl]; -Goalw [sinr_def] "sinr`UU=UU"; +Goalw [sinr_def] "sinr$UU=UU"; by (simp_tac (Ssum0_ss addsimps [cont_Isinr]) 1); by (rtac (inst_ssum_pcpo RS sym) 1); qed "strict_sinr"; Addsimps [strict_sinr]; Goalw [sinl_def,sinr_def] - "sinl`a=sinr`b ==> a=UU & b=UU"; + "sinl$a=sinr$b ==> a=UU & b=UU"; by (auto_tac (claset() addSDs [noteq_IsinlIsinr], simpset())); qed "noteq_sinlsinr"; Goalw [sinl_def,sinr_def] - "sinl`a1=sinl`a2==> a1=a2"; + "sinl$a1=sinl$a2==> a1=a2"; by Auto_tac; qed "inject_sinl"; Goalw [sinl_def,sinr_def] - "sinr`a1=sinr`a2==> a1=a2"; + "sinr$a1=sinr$a2==> a1=a2"; by Auto_tac; qed "inject_sinr"; AddSDs [inject_sinl, inject_sinr]; -Goal "x~=UU ==> sinl`x ~= UU"; +Goal "x~=UU ==> sinl$x ~= UU"; by (etac contrapos_nn 1); by (rtac inject_sinl 1); by Auto_tac; qed "defined_sinl"; Addsimps [defined_sinl]; -Goal "x~=UU ==> sinr`x ~= UU"; +Goal "x~=UU ==> sinr$x ~= UU"; by (etac contrapos_nn 1); by (rtac inject_sinr 1); by Auto_tac; @@ -363,7 +363,7 @@ Addsimps [defined_sinr]; Goalw [sinl_def,sinr_def] - "z=UU | (? a. z=sinl`a & a~=UU) | (? b. z=sinr`b & b~=UU)"; + "z=UU | (? a. z=sinl$a & a~=UU) | (? b. z=sinr$b & b~=UU)"; by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1); by (stac inst_ssum_pcpo 1); by (rtac Exh_Ssum 1); @@ -372,8 +372,8 @@ val [major,prem2,prem3] = Goalw [sinl_def,sinr_def] "[|p=UU ==> Q ;\ -\ !!x.[|p=sinl`x; x~=UU |] ==> Q;\ -\ !!y.[|p=sinr`y; y~=UU |] ==> Q|] ==> Q"; +\ !!x.[|p=sinl$x; x~=UU |] ==> Q;\ +\ !!y.[|p=sinr$y; y~=UU |] ==> Q|] ==> Q"; by (rtac (major RS IssumE) 1); by (stac inst_ssum_pcpo 1); by (atac 1); @@ -387,8 +387,8 @@ val [preml,premr] = Goalw [sinl_def,sinr_def] - "[|!!x.[|p=sinl`x|] ==> Q;\ -\ !!y.[|p=sinr`y|] ==> Q|] ==> Q"; + "[|!!x.[|p=sinl$x|] ==> Q;\ +\ !!y.[|p=sinr$y|] ==> Q|] ==> Q"; by (rtac IssumE2 1); by (rtac preml 1); by (rtac premr 2); @@ -399,7 +399,7 @@ cont_Iwhen3,cont2cont_CF1L]) 1)); Goalw [sscase_def,sinl_def,sinr_def] - "sscase`f`g`UU = UU"; + "sscase$f$g$UU = UU"; by (stac inst_ssum_pcpo 1); by (stac beta_cfun 1); by tac; @@ -416,7 +416,7 @@ cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)); Goalw [sscase_def,sinl_def,sinr_def] - "x~=UU==> sscase`f`g`(sinl`x) = f`x"; + "x~=UU==> sscase$f$g$(sinl$x) = f$x"; by (stac beta_cfun 1); by tac; by (stac beta_cfun 1); @@ -430,7 +430,7 @@ Addsimps [sscase2]; Goalw [sscase_def,sinl_def,sinr_def] - "x~=UU==> sscase`f`g`(sinr`x) = g`x"; + "x~=UU==> sscase$f$g$(sinr$x) = g$x"; by (stac beta_cfun 1); by tac; by (stac beta_cfun 1); @@ -445,7 +445,7 @@ Goalw [sinl_def,sinr_def] - "(sinl`x << sinl`y) = (x << y)"; + "(sinl$x << sinl$y) = (x << y)"; by (stac beta_cfun 1); by tac; by (stac beta_cfun 1); @@ -454,7 +454,7 @@ qed "less_ssum4a"; Goalw [sinl_def,sinr_def] - "(sinr`x << sinr`y) = (x << y)"; + "(sinr$x << sinr$y) = (x << y)"; by (stac beta_cfun 1); by tac; by (stac beta_cfun 1); @@ -463,7 +463,7 @@ qed "less_ssum4b"; Goalw [sinl_def,sinr_def] - "(sinl`x << sinr`y) = (x = UU)"; + "(sinl$x << sinr$y) = (x = UU)"; by (stac beta_cfun 1); by tac; by (stac beta_cfun 1); @@ -472,7 +472,7 @@ qed "less_ssum4c"; Goalw [sinl_def,sinr_def] - "(sinr`x << sinl`y) = (x = UU)"; + "(sinr$x << sinl$y) = (x = UU)"; by (stac beta_cfun 1); by tac; by (stac beta_cfun 1); @@ -481,15 +481,15 @@ qed "less_ssum4d"; Goalw [sinl_def,sinr_def] - "chain(Y) ==> (!i.? x.(Y i)=sinl`x)|(!i.? y.(Y i)=sinr`y)"; + "chain(Y) ==> (!i.? x.(Y i)=sinl$x)|(!i.? y.(Y i)=sinr$y)"; by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1); by (etac ssum_lemma4 1); qed "ssum_chainE"; Goalw [sinl_def,sinr_def,sscase_def] -"[| chain(Y); !i.? x. Y(i) = sinl`x |] ==>\ -\ lub(range(Y)) = sinl`(lub(range(%i. sscase`(LAM x. x)`(LAM y. UU)`(Y i))))"; +"[| chain(Y); !i.? x. Y(i) = sinl$x |] ==>\ +\ lub(range(Y)) = sinl$(lub(range(%i. sscase$(LAM x. x)$(LAM y. UU)$(Y i))))"; by (stac beta_cfun 1); by tac; by (stac beta_cfun 1); @@ -510,8 +510,8 @@ qed "thelub_ssum2a"; Goalw [sinl_def,sinr_def,sscase_def] -"[| chain(Y); !i.? x. Y(i) = sinr`x |] ==>\ -\ lub(range(Y)) = sinr`(lub(range(%i. sscase`(LAM y. UU)`(LAM x. x)`(Y i))))"; +"[| chain(Y); !i.? x. Y(i) = sinr$x |] ==>\ +\ lub(range(Y)) = sinr$(lub(range(%i. sscase$(LAM y. UU)$(LAM x. x)$(Y i))))"; by (stac beta_cfun 1); by tac; by (stac beta_cfun 1); @@ -532,22 +532,22 @@ qed "thelub_ssum2b"; Goalw [sinl_def,sinr_def] - "[| chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x. Y(i)=sinl`x"; + "[| chain(Y); lub(range(Y)) = sinl$x|] ==> !i.? x. Y(i)=sinl$x"; by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1); by (etac ssum_lemma9 1); by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1); qed "thelub_ssum2a_rev"; Goalw [sinl_def,sinr_def] - "[| chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x. Y(i)=sinr`x"; + "[| chain(Y); lub(range(Y)) = sinr$x|] ==> !i.? x. Y(i)=sinr$x"; by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1); by (etac ssum_lemma10 1); by (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, cont_Iwhen3]) 1); qed "thelub_ssum2b_rev"; Goal "chain(Y) ==>\ -\ lub(range(Y)) = sinl`(lub(range(%i. sscase`(LAM x. x)`(LAM y. UU)`(Y i))))\ -\ | lub(range(Y)) = sinr`(lub(range(%i. sscase`(LAM y. UU)`(LAM x. x)`(Y i))))"; +\ lub(range(Y)) = sinl$(lub(range(%i. sscase$(LAM x. x)$(LAM y. UU)$(Y i))))\ +\ | lub(range(Y)) = sinr$(lub(range(%i. sscase$(LAM y. UU)$(LAM x. x)$(Y i))))"; by (rtac (ssum_chainE RS disjE) 1); by (atac 1); by (rtac disjI1 1); @@ -558,7 +558,7 @@ by (atac 1); qed "thelub_ssum3"; -Goal "sscase`sinl`sinr`z=z"; +Goal "sscase$sinl$sinr$z=z"; by (res_inst_tac [("p","z")] ssumE 1); by Auto_tac; qed "sscase4"; diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Ssum3.thy --- a/src/HOLCF/Ssum3.thy Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Ssum3.thy Tue Jan 09 15:32:27 2001 +0100 @@ -22,6 +22,6 @@ sscase_def "sscase == (LAM f g s. Iwhen(f)(g)(s))" translations -"case s of sinl`x => t1 | sinr`y => t2" == "sscase`(LAM x. t1)`(LAM y. t2)`s" +"case s of sinl$x => t1 | sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s" end diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Tr.ML --- a/src/HOLCF/Tr.ML Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Tr.ML Tue Jan 09 15:32:27 2001 +0100 @@ -72,9 +72,9 @@ "(y orelse y) = y"]); bind_thms ("neg_thms", map prover [ - "neg`TT = FF", - "neg`FF = TT", - "neg`UU = UU" + "neg$TT = FF", + "neg$FF = TT", + "neg$UU = UU" ]); bind_thms ("ifte_thms", map prover [ diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Tr.thy --- a/src/HOLCF/Tr.thy Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Tr.thy Tue Jan 09 15:32:27 2001 +0100 @@ -27,14 +27,14 @@ "@orelse" :: "tr => tr => tr" ("_ orelse _" [31,30] 30) translations - "x andalso y" == "trand`x`y" - "x orelse y" == "tror`x`y" - "If b then e1 else e2 fi" == "Icifte`b`e1`e2" + "x andalso y" == "trand$x$y" + "x orelse y" == "tror$x$y" + "If b then e1 else e2 fi" == "Icifte$b$e1$e2" defs TT_def "TT==Def True" FF_def "FF==Def False" neg_def "neg == flift2 Not" - ifte_def "Icifte == (LAM b t e. flift1(%b. if b then t else e)`b)" + ifte_def "Icifte == (LAM b t e. flift1(%b. if b then t else e)$b)" andalso_def "trand == (LAM x y. If x then y else FF fi)" orelse_def "tror == (LAM x y. If x then TT else y fi)" If2_def "If2 Q x y == If Q then x else y fi" diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Up1.ML --- a/src/HOLCF/Up1.ML Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Up1.ML Tue Jan 09 15:32:27 2001 +0100 @@ -64,7 +64,7 @@ qed "Ifup1"; Goalw [Ifup_def,Iup_def] - "Ifup(f)(Iup(x))=f`x"; + "Ifup(f)(Iup(x))=f$x"; by (stac Abs_Up_inverse2 1); by (stac sum_case_Inr 1); by (rtac refl 1); diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Up1.thy --- a/src/HOLCF/Up1.thy Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Up1.thy Tue Jan 09 15:32:27 2001 +0100 @@ -22,7 +22,7 @@ defs Iup_def "Iup x == Abs_Up(Inr(x))" - Ifup_def "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f`z" + Ifup_def "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f$z" less_up_def "(op <<) == (%x1 x2. case Rep_Up(x1) of Inl(y1) => True | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Up3.ML --- a/src/HOLCF/Up3.ML Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Up3.ML Tue Jan 09 15:32:27 2001 +0100 @@ -133,23 +133,23 @@ (* continuous versions of lemmas for ('a)u *) (* ------------------------------------------------------------------------ *) -Goalw [up_def] "z = UU | (EX x. z = up`x)"; +Goalw [up_def] "z = UU | (EX x. z = up$x)"; by (simp_tac (Up0_ss addsimps [cont_Iup]) 1); by (stac inst_up_pcpo 1); by (rtac Exh_Up 1); qed "Exh_Up1"; -Goalw [up_def] "up`x=up`y ==> x=y"; +Goalw [up_def] "up$x=up$y ==> x=y"; by (rtac inject_Iup 1); by Auto_tac; qed "inject_up"; -Goalw [up_def] " up`x ~= UU"; +Goalw [up_def] " up$x ~= UU"; by Auto_tac; qed "defined_up"; val prems = Goalw [up_def] - "[| p=UU ==> Q; !!x. p=up`x==>Q|] ==>Q"; + "[| p=UU ==> Q; !!x. p=up$x==>Q|] ==>Q"; by (rtac upE 1); by (resolve_tac prems 1); by (etac (inst_up_pcpo RS ssubst) 1); @@ -160,7 +160,7 @@ val tac = (simp_tac (simpset() addsimps [cont_Iup,cont_Ifup1, cont_Ifup2,cont2cont_CF1L]) 1); -Goalw [up_def,fup_def] "fup`f`UU=UU"; +Goalw [up_def,fup_def] "fup$f$UU=UU"; by (stac inst_up_pcpo 1); by (stac beta_cfun 1); by tac; @@ -169,7 +169,7 @@ by (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1); qed "fup1"; -Goalw [up_def,fup_def] "fup`f`(up`x)=f`x"; +Goalw [up_def,fup_def] "fup$f$(up$x)=f$x"; by (stac beta_cfun 1); by (rtac cont_Iup 1); by (stac beta_cfun 1); @@ -179,20 +179,20 @@ by (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1); qed "fup2"; -Goalw [up_def,fup_def] "~ up`x << UU"; +Goalw [up_def,fup_def] "~ up$x << UU"; by (simp_tac (Up0_ss addsimps [cont_Iup]) 1); by (rtac less_up3b 1); qed "less_up4b"; Goalw [up_def,fup_def] - "(up`x << up`y) = (x<\ -\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"; +"[| chain(Y); EX i x. Y(i) = up$x |] ==>\ +\ lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))"; by (stac beta_cfun 1); by tac; by (stac beta_cfun 1); @@ -213,7 +213,7 @@ Goalw [up_def,fup_def] -"[| chain(Y); ! i x. Y(i) ~= up`x |] ==> lub(range(Y)) = UU"; +"[| chain(Y); ! i x. Y(i) ~= up$x |] ==> lub(range(Y)) = UU"; by (stac inst_up_pcpo 1); by (rtac thelub_up1b 1); by (atac 1); @@ -224,7 +224,7 @@ qed "thelub_up2b"; -Goal "(EX x. z = up`x) = (z~=UU)"; +Goal "(EX x. z = up$x) = (z~=UU)"; by (rtac iffI 1); by (etac exE 1); by (hyp_subst_tac 1); @@ -236,7 +236,7 @@ qed "up_lemma2"; -Goal "[| chain(Y); lub(range(Y)) = up`x |] ==> EX i x. Y(i) = up`x"; +Goal "[| chain(Y); lub(range(Y)) = up$x |] ==> EX i x. Y(i) = up$x"; by (rtac exE 1); by (rtac chain_UU_I_inverse2 1); by (rtac (up_lemma2 RS iffD1) 1); @@ -246,14 +246,14 @@ by (atac 1); qed "thelub_up2a_rev"; -Goal "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up`x"; +Goal "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up$x"; by (blast_tac (claset() addSDs [chain_UU_I RS spec, exI RS (up_lemma2 RS iffD1)]) 1); qed "thelub_up2b_rev"; Goal "chain(Y) ==> lub(range(Y)) = UU | \ -\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"; +\ lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))"; by (rtac disjE 1); by (rtac disjI1 2); by (rtac thelub_up2b 2); @@ -266,7 +266,7 @@ by (fast_tac HOL_cs 1); qed "thelub_up3"; -Goal "fup`up`x=x"; +Goal "fup$up$x=x"; by (res_inst_tac [("p","x")] upE1 1); by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1); by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1); diff -r c0844a30ea4e -r a7897aebbffc src/HOLCF/Up3.thy --- a/src/HOLCF/Up3.thy Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOLCF/Up3.thy Tue Jan 09 15:32:27 2001 +0100 @@ -19,7 +19,7 @@ "fup == (LAM f p. Ifup(f)(p))" translations -"case l of up`x => t1" == "fup`(LAM x. t1)`l" +"case l of up$x => t1" == "fup$(LAM x. t1)$l" end