# HG changeset patch # User paulson # Date 932390675 -7200 # Node ID 972b5f62f476f55e2e61a7e5ec04f3cfecca0897 # Parent 53934985426a9803dbcd0a9c8a00f06f19d91d94 getting rid of qed_goal diff -r 53934985426a -r 972b5f62f476 src/HOL/Prod.ML --- 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*) diff -r 53934985426a -r 972b5f62f476 src/HOL/Relation.ML --- 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 **) diff -r 53934985426a -r 972b5f62f476 src/HOL/Set.ML --- 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"; diff -r 53934985426a -r 972b5f62f476 src/HOL/Sum.ML --- 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"; diff -r 53934985426a -r 972b5f62f476 src/HOL/Vimage.ML --- 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); diff -r 53934985426a -r 972b5f62f476 src/HOL/WF_Rel.ML --- 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); diff -r 53934985426a -r 972b5f62f476 src/HOL/simpdata.ML --- 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*)