--- a/src/HOL/Prod.ML Mon Jul 19 15:19:11 1999 +0200
+++ b/src/HOL/Prod.ML Mon Jul 19 15:24:35 1999 +0200
@@ -61,8 +61,11 @@
by (Asm_simp_tac 1);
qed "surjective_pairing";
-val surj_pair = prove_goal Prod.thy "? x y. z = (x, y)" (K [
- rtac exI 1, rtac exI 1, rtac surjective_pairing 1]);
+Goal "? x y. z = (x, y)";
+by (rtac exI 1);
+by (rtac exI 1);
+by (rtac surjective_pairing 1);
+qed "surj_pair";
Addsimps [surj_pair];
@@ -120,17 +123,20 @@
qed "Pair_fst_snd_eq";
(*Prevents simplification of c: much faster*)
-qed_goal "split_weak_cong" Prod.thy
- "p=q ==> split c p = split c q"
- (fn [prem] => [rtac (prem RS arg_cong) 1]);
+val [prem] = goal Prod.thy
+ "p=q ==> split c p = split c q";
+by (rtac (prem RS arg_cong) 1);
+qed "split_weak_cong";
-qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f"
- (K [rtac ext 1, split_all_tac 1, rtac split 1]);
+Goal "(%(x,y). f(x,y)) = f";
+by (rtac ext 1);
+by (split_all_tac 1);
+by (rtac split 1);
+qed "split_eta";
-qed_goal "cond_split_eta" Prod.thy
- "!!f. (!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g"
- (K [asm_simp_tac (simpset() addsimps [split_eta]) 1]);
-
+val prems = Goal "(!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g";
+by (asm_simp_tac (simpset() addsimps prems@[split_eta]) 1);
+qed "cond_split_eta";
(*simplification procedure for cond_split_eta.
using split_eta a rewrite rule is not general enough, and using
@@ -171,9 +177,9 @@
Addsimprocs [split_eta_proc];
-
-qed_goal "split_beta" Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)"
- (K [stac surjective_pairing 1, stac split 1, rtac refl 1]);
+Goal "(%(x,y). P x y) z = P (fst z) (snd z)";
+by (stac surjective_pairing 1 THEN rtac split 1);
+qed "split_beta";
(*For use with split_tac and the simplifier*)
Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))";
@@ -212,11 +218,12 @@
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
qed "splitE";
-val splitE2 = prove_goal Prod.thy
-"[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
- REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
- rtac (split_beta RS subst) 1,
- rtac (hd prems) 1]);
+val major::prems = goal Prod.thy
+ "[| Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R \
+\ |] ==> R";
+by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
+by (rtac (split_beta RS subst) 1 THEN rtac major 1);
+qed "splitE2";
Goal "split R (a,b) ==> R a b";
by (etac (split RS iffD1) 1);
@@ -305,20 +312,20 @@
(*** Disjoint union of a family of sets - Sigma ***)
-qed_goalw "SigmaI" Prod.thy [Sigma_def]
- "[| a:A; b:B(a) |] ==> (a,b) : Sigma A B"
- (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
+Goalw [Sigma_def] "[| a:A; b:B(a) |] ==> (a,b) : Sigma A B";
+by (REPEAT (ares_tac [singletonI,UN_I] 1));
+qed "SigmaI";
AddSIs [SigmaI];
(*The general elimination rule*)
-qed_goalw "SigmaE" Prod.thy [Sigma_def]
+val major::prems = Goalw [Sigma_def]
"[| c: Sigma A B; \
\ !!x y.[| x:A; y:B(x); c=(x,y) |] ==> P \
-\ |] ==> P"
- (fn major::prems=>
- [ (cut_facts_tac [major] 1),
- (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
+\ |] ==> P";
+by (cut_facts_tac [major] 1);
+by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ;
+qed "SigmaE";
(** Elimination of (a,b):A*B -- introduces no eigenvariables **)
@@ -375,8 +382,10 @@
(*** Complex rules for Sigma ***)
-val Collect_split = prove_goal Prod.thy
- "{(a,b). P a & Q b} = Collect P Times Collect Q" (K [Blast_tac 1]);
+Goal "{(a,b). P a & Q b} = Collect P Times Collect Q";
+by (Blast_tac 1);
+qed "Collect_split";
+
Addsimps [Collect_split];
(*Suggested by Pierre Chartier*)
--- a/src/HOL/Relation.ML Mon Jul 19 15:19:11 1999 +0200
+++ b/src/HOL/Relation.ML Mon Jul 19 15:24:35 1999 +0200
@@ -171,15 +171,15 @@
qed "converseD";
(*More general than converseD, as it "splits" the member of the relation*)
-qed_goalw "converseE" thy [converse_def]
+
+val [major,minor] = Goalw [converse_def]
"[| yx : r^-1; \
\ !!x y. [| yx=(y,x); (x,y):r |] ==> P \
-\ |] ==> P"
- (fn [major,minor]=>
- [ (rtac (major RS CollectE) 1),
- (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
- (assume_tac 1) ]);
-
+\ |] ==> P";
+by (rtac (major RS CollectE) 1);
+by (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1));
+by (assume_tac 1);
+qed "converseE";
AddSEs [converseE];
Goalw [converse_def] "(r^-1)^-1 = r";
@@ -252,15 +252,16 @@
by (Blast_tac 1);
qed "Range_iff";
-qed_goalw "RangeI" thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
- (fn _ => [ (etac (converseI RS DomainI) 1) ]);
+Goalw [Range_def] "(a,b): r ==> b : Range(r)";
+by (etac (converseI RS DomainI) 1);
+qed "RangeI";
-qed_goalw "RangeE" thy [Range_def]
- "[| b : Range(r); !!x. (x,b): r ==> P |] ==> P"
- (fn major::prems=>
- [ (rtac (major RS DomainE) 1),
- (resolve_tac prems 1),
- (etac converseD 1) ]);
+val major::prems = Goalw [Range_def]
+ "[| b : Range(r); !!x. (x,b): r ==> P |] ==> P";
+by (rtac (major RS DomainE) 1);
+by (resolve_tac prems 1);
+by (etac converseD 1) ;
+qed "RangeE";
AddIs [RangeI];
AddSEs [RangeE];
@@ -296,16 +297,15 @@
overload_1st_set "Relation.op ^^";
-qed_goalw "Image_iff" thy [Image_def]
- "b : r^^A = (? x:A. (x,b):r)"
- (fn _ => [(Blast_tac 1)]);
+Goalw [Image_def] "b : r^^A = (? x:A. (x,b):r)";
+by (Blast_tac 1);
+qed "Image_iff";
-qed_goalw "Image_singleton" thy [Image_def]
- "r^^{a} = {b. (a,b):r}"
- (fn _ => [(Blast_tac 1)]);
+Goalw [Image_def] "r^^{a} = {b. (a,b):r}";
+by (Blast_tac 1);
+qed "Image_singleton";
-Goal
- "(b : r^^{a}) = ((a,b):r)";
+Goal "(b : r^^{a}) = ((a,b):r)";
by (rtac (Image_iff RS trans) 1);
by (Blast_tac 1);
qed "Image_singleton_iff";
@@ -316,20 +316,19 @@
by (Blast_tac 1);
qed "ImageI";
-qed_goalw "ImageE" thy [Image_def]
- "[| b: r^^A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P"
- (fn major::prems=>
- [ (rtac (major RS CollectE) 1),
- (Clarify_tac 1),
- (rtac (hd prems) 1),
- (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
+val major::prems = Goalw [Image_def]
+ "[| b: r^^A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P";
+by (rtac (major RS CollectE) 1);
+by (Clarify_tac 1);
+by (rtac (hd prems) 1);
+by (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ;
+qed "ImageE";
AddIs [ImageI];
AddSEs [ImageE];
-Goal
- "R^^{} = {}";
+Goal "R^^{} = {}";
by (Blast_tac 1);
qed "Image_empty";
@@ -366,11 +365,15 @@
section "Univalent";
-qed_goalw "UnivalentI" Relation.thy [Univalent_def]
- "!!r. !x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> Univalent r" (K [atac 1]);
+Goalw [Univalent_def]
+ "!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> Univalent r";
+by (assume_tac 1);
+qed "UnivalentI";
-qed_goalw "UnivalentD" Relation.thy [Univalent_def]
- "!!r. [| Univalent r; (x,y):r; (x,z):r|] ==> y=z" (K [Auto_tac]);
+Goalw [Univalent_def]
+ "[| Univalent r; (x,y):r; (x,z):r|] ==> y=z";
+by Auto_tac;
+qed "UnivalentD";
(** Graphs of partial functions **)
--- a/src/HOL/Set.ML Mon Jul 19 15:19:11 1999 +0200
+++ b/src/HOL/Set.ML Mon Jul 19 15:24:35 1999 +0200
@@ -71,7 +71,7 @@
by (Blast_tac 1);
qed "rev_bexI";
-val prems = goal Set.thy
+val prems = Goal
"[| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A. P(x)";
by (rtac classical 1);
by (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ;
@@ -223,14 +223,18 @@
section "The universal set -- UNIV";
-qed_goalw "UNIV_I" Set.thy [UNIV_def] "x : UNIV"
- (fn _ => [rtac CollectI 1, rtac TrueI 1]);
+Goalw [UNIV_def] "x : UNIV";
+by (rtac CollectI 1);
+by (rtac TrueI 1);
+qed "UNIV_I";
Addsimps [UNIV_I];
AddIs [UNIV_I]; (*unsafe makes it less likely to cause problems*)
-qed_goal "subset_UNIV" Set.thy "A <= UNIV"
- (fn _ => [rtac subsetI 1, rtac UNIV_I 1]);
+Goal "A <= UNIV";
+by (rtac subsetI 1);
+by (rtac UNIV_I 1);
+qed "subset_UNIV";
(** Eta-contracting these two rules (to remove P) causes them to be ignored
because of their interaction with congruence rules. **)
@@ -266,7 +270,7 @@
(*One effect is to delete the ASSUMPTION {} <= A*)
AddIffs [empty_subsetI];
-val [prem]= goal Set.thy "[| !!y. y:A ==> False |] ==> A={}";
+val [prem]= Goal "[| !!y. y:A ==> False |] ==> A={}";
by (blast_tac (claset() addIs [prem RS FalseE]) 1) ;
qed "equals0I";
@@ -301,11 +305,11 @@
AddIffs [Pow_iff];
-Goalw [Pow_def] "!!A B. A <= B ==> A : Pow(B)";
+Goalw [Pow_def] "A <= B ==> A : Pow(B)";
by (etac CollectI 1);
qed "PowI";
-Goalw [Pow_def] "!!A B. A : Pow(B) ==> A<=B";
+Goalw [Pow_def] "A : Pow(B) ==> A<=B";
by (etac CollectD 1);
qed "PowD";
@@ -316,8 +320,9 @@
section "Set complement";
-qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : -A) = (c~:A)"
- (fn _ => [ (Blast_tac 1) ]);
+Goalw [Compl_def] "(c : -A) = (c~:A)";
+by (Blast_tac 1);
+qed "Compl_iff";
Addsimps [Compl_iff];
@@ -340,9 +345,9 @@
section "Binary union -- Un";
-qed_goalw "Un_iff" Set.thy [Un_def] "(c : A Un B) = (c:A | c:B)"
- (fn _ => [ Blast_tac 1 ]);
-
+Goalw [Un_def] "(c : A Un B) = (c:A | c:B)";
+by (Blast_tac 1);
+qed "Un_iff";
Addsimps [Un_iff];
Goal "c:A ==> c : A Un B";
@@ -355,7 +360,7 @@
(*Classical introduction rule: no commitment to A vs B*)
-val prems= goal Set.thy "(c~:B ==> c:A) ==> c : A Un B";
+val prems = Goal "(c~:B ==> c:A) ==> c : A Un B";
by (Simp_tac 1);
by (REPEAT (ares_tac (prems@[disjCI]) 1)) ;
qed "UnCI";
@@ -372,9 +377,9 @@
section "Binary intersection -- Int";
-qed_goalw "Int_iff" Set.thy [Int_def] "(c : A Int B) = (c:A & c:B)"
- (fn _ => [ (Blast_tac 1) ]);
-
+Goalw [Int_def] "(c : A Int B) = (c:A & c:B)";
+by (Blast_tac 1);
+qed "Int_iff";
Addsimps [Int_iff];
Goal "[| c:A; c:B |] ==> c : A Int B";
@@ -401,9 +406,9 @@
section "Set difference";
-qed_goalw "Diff_iff" Set.thy [set_diff_def] "(c : A-B) = (c:A & c~:B)"
- (fn _ => [ (Blast_tac 1) ]);
-
+Goalw [set_diff_def] "(c : A-B) = (c:A & c~:B)";
+by (Blast_tac 1);
+qed "Diff_iff";
Addsimps [Diff_iff];
Goal "[| c : A; c ~: B |] ==> c : A - B";
@@ -418,7 +423,7 @@
by (Asm_full_simp_tac 1) ;
qed "DiffD2";
-val prems= goal Set.thy "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P";
+val prems = Goal "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P";
by (resolve_tac prems 1);
by (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ;
qed "DiffE";
@@ -429,12 +434,12 @@
section "Augmenting a set -- insert";
-qed_goalw "insert_iff" Set.thy [insert_def] "a : insert b A = (a=b | a:A)"
- (fn _ => [Blast_tac 1]);
-
+Goalw [insert_def] "a : insert b A = (a=b | a:A)";
+by (Blast_tac 1);
+qed "insert_iff";
Addsimps [insert_iff];
-val _ = goal Set.thy "a : insert a B";
+Goal "a : insert a B";
by (Simp_tac 1);
qed "insertI1";
@@ -449,7 +454,7 @@
qed "insertE";
(*Classical introduction rule*)
-val prems= goal Set.thy "(a~:B ==> a=b) ==> a: insert b B";
+val prems = Goal "(a~:B ==> a=b) ==> a: insert b B";
by (Simp_tac 1);
by (REPEAT (ares_tac (prems@[disjCI]) 1)) ;
qed "insertCI";
--- a/src/HOL/Sum.ML Mon Jul 19 15:19:11 1999 +0200
+++ b/src/HOL/Sum.ML Mon Jul 19 15:24:35 1999 +0200
@@ -6,8 +6,6 @@
The disjoint sum of two types
*)
-open Sum;
-
(** Inl_Rep and Inr_Rep: Representations of the constructors **)
(*This counts as a non-emptiness result for admitting 'a+'b as a type*)
@@ -157,15 +155,16 @@
by Auto_tac;
qed "split_sum_case";
-qed_goal "split_sum_case_asm" Sum.thy "P (sum_case f g s) = \
-\ (~((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))"
- (K [stac split_sum_case 1,
- Blast_tac 1]);
+Goal "P (sum_case f g s) = \
+\ (~ ((? x. s = Inl x & ~P (f x)) | (? y. s = Inr y & ~P (g y))))";
+by (stac split_sum_case 1);
+by (Blast_tac 1);
+qed "split_sum_case_asm";
(*Prevents simplification of f and g: much faster*)
-qed_goal "sum_case_weak_cong" Sum.thy
- "s=t ==> sum_case f g s = sum_case f g t"
- (fn [prem] => [rtac (prem RS arg_cong) 1]);
+Goal "s=t ==> sum_case f g s = sum_case f g t";
+by (etac arg_cong 1);
+qed "sum_case_weak_cong";
val [p1,p2] = Goal "[| sum_case f1 f2 = sum_case g1 g2; \
\ [| f1 = g1; f2 = g2 |] ==> P |] ==> P";
--- a/src/HOL/Vimage.ML Mon Jul 19 15:19:11 1999 +0200
+++ b/src/HOL/Vimage.ML Mon Jul 19 15:24:35 1999 +0200
@@ -6,33 +6,32 @@
Inverse image of a function
*)
-open Vimage;
-
(** Basic rules **)
-qed_goalw "vimage_eq" thy [vimage_def]
- "(a : f-``B) = (f a : B)"
- (fn _ => [ (Blast_tac 1) ]);
+Goalw [vimage_def] "(a : f-``B) = (f a : B)";
+by (Blast_tac 1) ;
+qed "vimage_eq";
Addsimps [vimage_eq];
-qed_goal "vimage_singleton_eq" thy
- "(a : f-``{b}) = (f a = b)"
- (fn _ => [ simp_tac (simpset() addsimps [vimage_eq]) 1 ]);
+Goal "(a : f-``{b}) = (f a = b)";
+by (simp_tac (simpset() addsimps [vimage_eq]) 1) ;
+qed "vimage_singleton_eq";
-qed_goalw "vimageI" thy [vimage_def]
- "!!A B f. [| f a = b; b:B |] ==> a : f-``B"
- (fn _ => [ (Blast_tac 1) ]);
+Goalw [vimage_def]
+ "!!A B f. [| f a = b; b:B |] ==> a : f-``B";
+by (Blast_tac 1) ;
+qed "vimageI";
Goalw [vimage_def] "f a : A ==> a : f -`` A";
by (Fast_tac 1);
qed "vimageI2";
-qed_goalw "vimageE" thy [vimage_def]
- "[| a: f-``B; !!x.[| f a = x; x:B |] ==> P |] ==> P"
- (fn major::prems=>
- [ (rtac (major RS CollectE) 1),
- (blast_tac (claset() addIs prems) 1) ]);
+val major::prems = Goalw [vimage_def]
+ "[| a: f-``B; !!x.[| f a = x; x:B |] ==> P |] ==> P";
+by (rtac (major RS CollectE) 1);
+by (blast_tac (claset() addIs prems) 1) ;
+qed "vimageE";
Goalw [vimage_def] "a : f -`` A ==> f a : A";
by (Fast_tac 1);
--- a/src/HOL/WF_Rel.ML Mon Jul 19 15:19:11 1999 +0200
+++ b/src/HOL/WF_Rel.ML Mon Jul 19 15:24:35 1999 +0200
@@ -115,10 +115,10 @@
by (Asm_full_simp_tac 1);
qed_spec_mp "finite_acyclic_wf";
-qed_goal "finite_acyclic_wf_converse" thy
- "!!X. [|finite r; acyclic r|] ==> wf (r^-1)" (K [
- etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1,
- etac (acyclic_converse RS iffD2) 1]);
+Goal "[|finite r; acyclic r|] ==> wf (r^-1)";
+by (etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1);
+by (etac (acyclic_converse RS iffD2) 1);
+qed "finite_acyclic_wf_converse";
Goal "finite r ==> wf r = acyclic r";
by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);
--- a/src/HOL/simpdata.ML Mon Jul 19 15:19:11 1999 +0200
+++ b/src/HOL/simpdata.ML Mon Jul 19 15:24:35 1999 +0200
@@ -89,12 +89,14 @@
end;
-qed_goal "meta_eq_to_obj_eq" HOL.thy "x==y ==> x=y"
- (fn [prem] => [rewtac prem, rtac refl 1]);
+val [prem] = goal HOL.thy "x==y ==> x=y";
+by (rewtac prem);
+by (rtac refl 1);
+qed "meta_eq_to_obj_eq";
local
- fun prover s = prove_goal HOL.thy s (K [Blast_tac 1]);
+ fun prover s = prove_goal HOL.thy s (fn _ => [(Blast_tac 1)]);
in
@@ -156,7 +158,7 @@
val imp_cong = impI RSN
(2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
- (fn _=> [Blast_tac 1]) RS mp RS mp);
+ (fn _=> [(Blast_tac 1)]) RS mp RS mp);
(*Miniscoping: pushing in existential quantifiers*)
val ex_simps = map prover
@@ -185,7 +187,7 @@
(fn prems => [resolve_tac prems 1, etac exI 1]);
val lemma2 = prove_goalw HOL.thy [Ex_def]
"(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
- (fn prems => [REPEAT(resolve_tac prems 1)])
+ (fn prems => [(REPEAT(resolve_tac prems 1))])
in equal_intr lemma1 lemma2 end;
end;
@@ -194,11 +196,11 @@
val True_implies_equals = prove_goal HOL.thy
"(True ==> PROP P) == PROP P"
-(K [rtac equal_intr_rule 1, atac 2,
+(fn _ => [rtac equal_intr_rule 1, atac 2,
METAHYPS (fn prems => resolve_tac prems 1) 1,
rtac TrueI 1]);
-fun prove nm thm = qed_goal nm HOL.thy thm (K [Blast_tac 1]);
+fun prove nm thm = qed_goal nm HOL.thy thm (fn _ => [(Blast_tac 1)]);
prove "conj_commute" "(P&Q) = (Q&P)";
prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
@@ -255,19 +257,19 @@
let val th = prove_goal HOL.thy
"(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
- (fn _=> [Blast_tac 1])
+ (fn _=> [(Blast_tac 1)])
in bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp))) end;
let val th = prove_goal HOL.thy
"(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
- (fn _=> [Blast_tac 1])
+ (fn _=> [(Blast_tac 1)])
in bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp))) end;
(* '|' congruence rule: not included by default! *)
let val th = prove_goal HOL.thy
"(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
- (fn _=> [Blast_tac 1])
+ (fn _=> [(Blast_tac 1)])
in bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp))) end;
prove "eq_sym_conv" "(x=y) = (y=x)";
@@ -275,48 +277,58 @@
(** if-then-else rules **)
-qed_goalw "if_True" HOL.thy [if_def] "(if True then x else y) = x"
- (K [Blast_tac 1]);
+Goalw [if_def] "(if True then x else y) = x";
+by (Blast_tac 1);
+qed "if_True";
-qed_goalw "if_False" HOL.thy [if_def] "(if False then x else y) = y"
- (K [Blast_tac 1]);
+Goalw [if_def] "(if False then x else y) = y";
+by (Blast_tac 1);
+qed "if_False";
-qed_goalw "if_P" HOL.thy [if_def] "!!P. P ==> (if P then x else y) = x"
- (K [Blast_tac 1]);
+Goalw [if_def] "!!P. P ==> (if P then x else y) = x";
+by (Blast_tac 1);
+qed "if_P";
-qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y"
- (K [Blast_tac 1]);
+Goalw [if_def] "!!P. ~P ==> (if P then x else y) = y";
+by (Blast_tac 1);
+qed "if_not_P";
-qed_goal "split_if" HOL.thy
- "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (K [
- res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1,
- stac if_P 2,
- stac if_not_P 1,
- ALLGOALS (Blast_tac)]);
+Goal "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))";
+by (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1);
+by (stac if_P 2);
+by (stac if_not_P 1);
+by (ALLGOALS (Blast_tac));
+qed "split_if";
+
(* for backwards compatibility: *)
val expand_if = split_if;
-qed_goal "split_if_asm" HOL.thy
- "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
- (K [stac split_if 1,
- Blast_tac 1]);
+Goal "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))";
+by (stac split_if 1);
+by (Blast_tac 1);
+qed "split_if_asm";
-qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
- (K [stac split_if 1, Blast_tac 1]);
+Goal "(if c then x else x) = x";
+by (stac split_if 1);
+by (Blast_tac 1);
+qed "if_cancel";
-qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
- (K [stac split_if 1, Blast_tac 1]);
+Goal "(if x = y then y else x) = x";
+by (stac split_if 1);
+by (Blast_tac 1);
+qed "if_eq_cancel";
(*This form is useful for expanding IFs on the RIGHT of the ==> symbol*)
-qed_goal "if_bool_eq_conj" HOL.thy
- "(if P then Q else R) = ((P-->Q) & (~P-->R))"
- (K [rtac split_if 1]);
+Goal
+ "(if P then Q else R) = ((P-->Q) & (~P-->R))";
+by (rtac split_if 1);
+qed "if_bool_eq_conj";
(*And this form is useful for expanding IFs on the LEFT*)
-qed_goal "if_bool_eq_disj" HOL.thy
- "(if P then Q else R) = ((P&Q) | (~P&R))"
- (K [stac split_if 1,
- Blast_tac 1]);
+Goal "(if P then Q else R) = ((P&Q) | (~P&R))";
+by (stac split_if 1);
+by (Blast_tac 1);
+qed "if_bool_eq_disj";
(*** make simplification procedures for quantifier elimination ***)
@@ -453,18 +465,18 @@
qed "if_cong";
(*Prevents simplification of x and y: much faster*)
-qed_goal "if_weak_cong" HOL.thy
- "b=c ==> (if b then x else y) = (if c then x else y)"
- (fn [prem] => [rtac (prem RS arg_cong) 1]);
+Goal "b=c ==> (if b then x else y) = (if c then x else y)";
+by (etac arg_cong 1);
+qed "if_weak_cong";
(*Prevents simplification of t: much faster*)
-qed_goal "let_weak_cong" HOL.thy
- "a = b ==> (let x=a in t(x)) = (let x=b in t(x))"
- (fn [prem] => [rtac (prem RS arg_cong) 1]);
+Goal "a = b ==> (let x=a in t(x)) = (let x=b in t(x))";
+by (etac arg_cong 1);
+qed "let_weak_cong";
-qed_goal "if_distrib" HOL.thy
- "f(if c then x else y) = (if c then f x else f y)"
- (K [simp_tac (HOL_ss setloop (split_tac [split_if])) 1]);
+Goal "f(if c then x else y) = (if c then f x else f y)";
+by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1);
+qed "if_distrib";
(*For expand_case_tac*)