--- a/src/HOL/Quot/FRACT.ML Fri Nov 13 13:29:50 1998 +0100
+++ b/src/HOL/Quot/FRACT.ML Fri Nov 13 13:41:53 1998 +0100
@@ -4,15 +4,14 @@
Copyright 1997 Technische Universitaet Muenchen
*)
-open FRACT;
Goalw [per_def,per_NP_def]
"(op ===)=(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))";
-fr refl;
+br refl 1;
qed "inst_NP_per";
Goalw [half_def] "half = <[abs_NP(n,2*n)]>";
-fr per_class_eqI;
+br per_class_eqI 1;
by (simp_tac (simpset() addsimps [inst_NP_per]) 1);
qed "test";
--- a/src/HOL/Quot/HQUOT.ML Fri Nov 13 13:29:50 1998 +0100
+++ b/src/HOL/Quot/HQUOT.ML Fri Nov 13 13:41:53 1998 +0100
@@ -4,24 +4,21 @@
Copyright 1997 Technische Universitaet Muenchen
*)
-open HQUOT;
(* first prove some helpful lemmas *)
Goalw [quot_def] "{y. y===x}:quot";
by (Asm_simp_tac 1);
-by (fast_tac (set_cs addIs [per_sym]) 1);
+by (blast_tac (claset() addIs [per_sym]) 1);
qed "per_class_rep_quot";
-val prems = goal thy "Rep_quot a = Rep_quot b ==> a=b";
-by (cut_facts_tac prems 1);
+Goal "Rep_quot a = Rep_quot b ==> a=b";
by (rtac (Rep_quot_inverse RS subst) 1);
by (res_inst_tac [("t","a")] (Rep_quot_inverse RS subst) 1);
by (Asm_simp_tac 1);
qed "quot_eq";
(* prepare induction and exhaustiveness *)
-val prems = goal thy "!s. s:quot --> P (Abs_quot s) ==> P x";
-by (cut_facts_tac prems 1);
+Goal "!s. s:quot --> P (Abs_quot s) ==> P x";
by (rtac (Abs_quot_inverse RS subst) 1);
by (rtac Rep_quot 1);
by (dres_inst_tac [("x","Rep_quot x")] spec 1);
@@ -36,8 +33,7 @@
(* some lemmas for the equivalence classes *)
(* equality and symmetry for equivalence classes *)
-val prems = goalw thy [peclass_def] "x===y==><[x]>=<[y]>";
-by (cut_facts_tac prems 1);
+Goalw [peclass_def] "x===y==><[x]>=<[y]>";
by (res_inst_tac [("f","Abs_quot")] arg_cong 1);
by (rtac Collect_cong 1);
by (rtac iffI 1);
@@ -46,22 +42,20 @@
by (etac per_sym 1);
qed "per_class_eqI";
-val prems = goalw thy [peclass_def] "<[(x::'a::er)]>=<[y]>==>x===y";
-by (cut_facts_tac prems 1);
+Goalw [peclass_def] "<[(x::'a::er)]>=<[y]>==>x===y";
by (dres_inst_tac [("f","Rep_quot")] arg_cong 1);
by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
by (dres_inst_tac [("c","x")] equalityCE 1);by (assume_tac 3);
-by (safe_tac set_cs);
-by (fast_tac (set_cs addIs [er_refl]) 1);
+by Safe_tac;
+by (blast_tac (claset() addIs [er_refl]) 1);
qed "er_class_eqE";
-val prems = goalw thy [peclass_def] "[|x:D;<[x]>=<[y]>|]==>x===y";
-by (cut_facts_tac prems 1);
+Goalw [peclass_def] "[|x:D;<[x]>=<[y]>|]==>x===y";
by (dtac DomainD 1);
by (dres_inst_tac [("f","Rep_quot")] arg_cong 1);
by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
by (dres_inst_tac [("c","x")] equalityCE 1);by (assume_tac 3);
-by (safe_tac set_cs);
+by Auto_tac;
qed "per_class_eqE";
Goal "<[(x::'a::er)]>=<[y]>=x===y";
@@ -70,37 +64,32 @@
by (etac per_class_eqI 1);
qed "er_class_eq";
-val prems = goal thy "x:D==><[x]>=<[y]>=x===y";
-by (cut_facts_tac prems 1);
+Goal "x:D==><[x]>=<[y]>=x===y";
by (rtac iffI 1);
by (etac per_class_eqE 1);by (assume_tac 1);
by (etac per_class_eqI 1);
qed "per_class_eq";
(* inequality *)
-val prems = goal thy "[|x:D;~x===y|]==><[x]>~=<[y]>";
-by (cut_facts_tac prems 1);
+Goal "[|x:D;~x===y|]==><[x]>~=<[y]>";
by (rtac notI 1);
by (dtac per_class_eqE 1);
by Auto_tac;
qed "per_class_neqI";
-val prems = goal thy "~(x::'a::er)===y==><[x]>~=<[y]>";
-by (cut_facts_tac prems 1);
+Goal "~(x::'a::er)===y==><[x]>~=<[y]>";
by (rtac notI 1);
by (dtac er_class_eqE 1);
by Auto_tac;
qed "er_class_neqI";
-val prems = goal thy "<[x]>~=<[y]>==>~x===y";
-by (cut_facts_tac prems 1);
+Goal "<[x]>~=<[y]>==>~x===y";
by (rtac notI 1);
by (etac notE 1);
by (etac per_class_eqI 1);
qed "per_class_neqE";
-val prems = goal thy "x:D==><[x]>~=<[y]>=(~x===y)";
-by (cut_facts_tac prems 1);
+Goal "x:D==><[x]>~=<[y]>=(~x===y)";
by (rtac iffI 1);
by (etac per_class_neqE 1);
by (etac per_class_neqI 1);by (assume_tac 1);
@@ -123,49 +112,45 @@
by (subgoal_tac "s:quot" 1);
by (asm_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
by (rtac set_ext 1);
-by (fast_tac set_cs 1);
+by (Blast_tac 1);
by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1);
-by (fast_tac set_cs 1);
+by (Blast_tac 1);
qed "per_class_exh";
-val prems = goal thy "!x. P<[x]> ==> P s";
-by (cut_facts_tac (prems@[
- read_instantiate[("x","s::'a::per quot")] per_class_exh]) 1);
-by (fast_tac set_cs 1);
+Goal "!x. P<[x]> ==> P s";
+by (cut_facts_tac [read_instantiate[("x","s::'a::per quot")] per_class_exh] 1);
+by (Blast_tac 1);
qed "per_class_all";
(* theorems for any_in *)
Goalw [any_in_def,peclass_def] "any_in<[(s::'a::er)]>===s";
-fr selectI2;
-fr refl;
+br selectI2 1;
+br refl 1;
by (fold_goals_tac [peclass_def]);
-fe er_class_eqE;
+be er_class_eqE 1;
qed "er_any_in_class";
-val prems = goalw thy [any_in_def,peclass_def] "s:D==>any_in<[s]>===s";
-by (cut_facts_tac prems 1);
-fr selectI2;
-fr refl;
+Goalw [any_in_def,peclass_def] "s:D==>any_in<[s]>===s";
+br selectI2 1;
+br refl 1;
by (fold_goals_tac [peclass_def]);
-fr per_sym;
-fe per_class_eqE;
-fe sym;
+br per_sym 1;
+be per_class_eqE 1;
+be sym 1;
qed "per_any_in_class";
-val prems = goal thy "<[any_in (s::'a::er quot)]> = s";
-by (cut_facts_tac prems 1);
-fr per_class_all;
-fr allI;
-fr (er_any_in_class RS per_class_eqI);
+Goal "<[any_in (s::'a::er quot)]> = s";
+br per_class_all 1;
+br allI 1;
+br (er_any_in_class RS per_class_eqI) 1;
qed "er_class_any_in";
(* equivalent theorem for per would need !x.x:D *)
-val prems = goal thy "!x::'a::per. x:D==><[any_in (q::'a::per quot)]> = q";
-by (cut_facts_tac prems 1);
-fr per_class_all;
-fr allI;
-fr (per_any_in_class RS per_class_eqI);
-fe spec;
+Goal "!x::'a::per. x:D==><[any_in (q::'a::per quot)]> = q";
+br per_class_all 1;
+br allI 1;
+br (per_any_in_class RS per_class_eqI) 1;
+be spec 1;
qed "per_class_any_in";
-(* is like theorem for class er *)
\ No newline at end of file
+(* is like theorem for class er *)
--- a/src/HOL/Quot/NPAIR.ML Fri Nov 13 13:29:50 1998 +0100
+++ b/src/HOL/Quot/NPAIR.ML Fri Nov 13 13:41:53 1998 +0100
@@ -12,8 +12,7 @@
Addsimps [rep_abs_NP];
-val prems = goalw thy [per_NP_def] "eqv (x::NP) y ==> eqv y x";
-by (cut_facts_tac prems 1);
+Goalw [per_NP_def] "eqv (x::NP) y ==> eqv y x";
by Auto_tac;
qed "per_sym_NP";
--- a/src/HOL/Quot/PER.ML Fri Nov 13 13:29:50 1998 +0100
+++ b/src/HOL/Quot/PER.ML Fri Nov 13 13:41:53 1998 +0100
@@ -12,7 +12,7 @@
(* Witness that quot is not empty *)
Goal "?z:{s.? r.!y. y:s=y===r}";
-fr CollectI;
+br CollectI 1;
by (res_inst_tac [("x","x")] exI 1);
by (rtac allI 1);
by (rtac mem_Collect_eq 1);
--- a/src/HOL/Quot/PER0.ML Fri Nov 13 13:29:50 1998 +0100
+++ b/src/HOL/Quot/PER0.ML Fri Nov 13 13:41:53 1998 +0100
@@ -7,13 +7,11 @@
open PER0;
(* derive the characteristic axioms *)
-val prems = goalw thy [per_def] "x === y ==> y === x";
-by (cut_facts_tac prems 1);
+Goalw [per_def] "x === y ==> y === x";
by (etac ax_per_sym 1);
qed "per_sym";
-val prems = goalw thy [per_def] "[| x === y; y === z |] ==> x === z";
-by (cut_facts_tac prems 1);
+Goalw [per_def] "[| x === y; y === z |] ==> x === z";
by (etac ax_per_trans 1);
by (assume_tac 1);
qed "per_trans";
@@ -30,26 +28,22 @@
by (etac per_sym 1);
qed "per_sym2";
-val prems = goal thy "x===y ==> x===x";
-by (cut_facts_tac prems 1);
+Goal "x===y ==> x===x";
by (rtac per_trans 1);by (assume_tac 1);
by (etac per_sym 1);
qed "sym2refl1";
-val prems = goal thy "x===y ==> y===y";
-by (cut_facts_tac prems 1);
+Goal "x===y ==> y===y";
by (rtac per_trans 1);by (assume_tac 2);
by (etac per_sym 1);
qed "sym2refl2";
-val prems = goalw thy [Dom] "x:D ==> x === x";
-by (cut_facts_tac prems 1);
-by (fast_tac set_cs 1);
+Goalw [Dom] "x:D ==> x === x";
+by (Blast_tac 1);
qed "DomainD";
-val prems = goalw thy [Dom] "x === x ==> x:D";
-by (cut_facts_tac prems 1);
-by (fast_tac set_cs 1);
+Goalw [Dom] "x === x ==> x:D";
+by (Blast_tac 1);
qed "DomainI";
Goal "x:D = x===x";
@@ -63,28 +57,26 @@
qed "per_not_sym";
(* show that PER work only on D *)
-val prems = goal thy "x===y ==> x:D";
-by (cut_facts_tac prems 1);
+Goal "x===y ==> x:D";
by (etac (sym2refl1 RS DomainI) 1);
qed "DomainI_left";
-val prems = goal thy "x===y ==> y:D";
-by (cut_facts_tac prems 1);
+Goal "x===y ==> y:D";
by (etac (sym2refl2 RS DomainI) 1);
qed "DomainI_right";
-val prems = goalw thy [Dom] "x~:D ==> ~x===y";
-by (cut_facts_tac prems 1);
-by (res_inst_tac [("Q","x===y")] (excluded_middle RS disjE) 1);by (assume_tac 1);
+Goalw [Dom] "x~:D ==> ~x===y";
+by (res_inst_tac [("Q","x===y")] (excluded_middle RS disjE) 1);
+by (assume_tac 1);
by (dtac sym2refl1 1);
-by (fast_tac set_cs 1);
+by (Blast_tac 1);
qed "notDomainE1";
-val prems = goalw thy [Dom] "x~:D ==> ~y===x";
-by (cut_facts_tac prems 1);
-by (res_inst_tac [("Q","y===x")] (excluded_middle RS disjE) 1);by (assume_tac 1);
+Goalw [Dom] "x~:D ==> ~y===x";
+by (res_inst_tac [("Q","y===x")] (excluded_middle RS disjE) 1);
+by (assume_tac 1);
by (dtac sym2refl2 1);
-by (fast_tac set_cs 1);
+by (Blast_tac 1);
qed "notDomainE2";
(* theorems for equivalence relations *)
@@ -94,16 +86,12 @@
qed "er_Domain";
(* witnesses for "=>" ::(per,per)per *)
-val prems = goalw thy [fun_per_def]"eqv (x::'a::per => 'b::per) y ==> eqv y x";
-by (cut_facts_tac prems 1);
-by (safe_tac HOL_cs);
-by (asm_full_simp_tac (HOL_ss addsimps [per_sym2]) 1);
+Goalw [fun_per_def]"eqv (x::'a::per => 'b::per) y ==> eqv y x";
+by (auto_tac (claset(), simpset() addsimps [per_sym2]));
qed "per_sym_fun";
-val prems = goalw thy [fun_per_def]
- "[| eqv (f::'a::per=>'b::per) g;eqv g h|] ==> eqv f h";
-by (cut_facts_tac prems 1);
-by (safe_tac HOL_cs);
+Goalw [fun_per_def] "[| eqv (f::'a::per=>'b::per) g;eqv g h|] ==> eqv f h";
+by Safe_tac;
by (REPEAT (dtac spec 1));
by (res_inst_tac [("y","g y")] per_trans 1);
by (rtac mp 1);by (assume_tac 1);