# HG changeset patch # User paulson # Date 932027274 -7200 # Node ID b46ccfee8e59656c524f237ed68d18ff100cd603 # Parent 46048223e0f9014730c85e0ea8250c64a1137517 qed_goal -> Goal diff -r 46048223e0f9 -r b46ccfee8e59 src/HOL/Arith.ML --- a/src/HOL/Arith.ML Wed Jul 14 13:32:21 1999 +0200 +++ b/src/HOL/Arith.ML Thu Jul 15 10:27:54 1999 +0200 @@ -12,16 +12,18 @@ (** Difference **) -qed_goal "diff_0_eq_0" thy - "0 - n = 0" - (fn _ => [induct_tac "n" 1, ALLGOALS Asm_simp_tac]); +Goal "0 - n = 0"; +by (induct_tac "n" 1); +by (ALLGOALS Asm_simp_tac); +qed "diff_0_eq_0"; (*Must simplify BEFORE the induction! (Else we get a critical pair) Suc(m) - Suc(n) rewrites to pred(Suc(m) - n) *) -qed_goal "diff_Suc_Suc" thy - "Suc(m) - Suc(n) = m - n" - (fn _ => - [Simp_tac 1, induct_tac "n" 1, ALLGOALS Asm_simp_tac]); +Goal "Suc(m) - Suc(n) = m - n"; +by (Simp_tac 1); +by (induct_tac "n" 1); +by (ALLGOALS Asm_simp_tac); +qed "diff_Suc_Suc"; Addsimps [diff_0_eq_0, diff_Suc_Suc]; @@ -40,25 +42,36 @@ (*** Addition ***) -qed_goal "add_0_right" thy "m + 0 = m" - (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); +Goal "m + 0 = m"; +by (induct_tac "m" 1); +by (ALLGOALS Asm_simp_tac); +qed "add_0_right"; -qed_goal "add_Suc_right" thy "m + Suc(n) = Suc(m+n)" - (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); +Goal "m + Suc(n) = Suc(m+n)"; +by (induct_tac "m" 1); +by (ALLGOALS Asm_simp_tac); +qed "add_Suc_right"; Addsimps [add_0_right,add_Suc_right]; + (*Associative law for addition*) -qed_goal "add_assoc" thy "(m + n) + k = m + ((n + k)::nat)" - (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); +Goal "(m + n) + k = m + ((n + k)::nat)"; +by (induct_tac "m" 1); +by (ALLGOALS Asm_simp_tac); +qed "add_assoc"; (*Commutative law for addition*) -qed_goal "add_commute" thy "m + n = n + (m::nat)" - (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); +Goal "m + n = n + (m::nat)"; +by (induct_tac "m" 1); +by (ALLGOALS Asm_simp_tac); +qed "add_commute"; -qed_goal "add_left_commute" thy "x+(y+z)=y+((x+z)::nat)" - (fn _ => [rtac (add_commute RS trans) 1, rtac (add_assoc RS trans) 1, - rtac (add_commute RS arg_cong) 1]); +Goal "x+(y+z)=y+((x+z)::nat)"; +by (rtac (add_commute RS trans) 1); +by (rtac (add_assoc RS trans) 1); +by (rtac (add_commute RS arg_cong) 1); +qed "add_left_commute"; (*Addition is an AC-operator*) val add_ac = [add_assoc, add_commute, add_left_commute]; @@ -264,13 +277,16 @@ (*** Multiplication ***) (*right annihilation in product*) -qed_goal "mult_0_right" thy "m * 0 = 0" - (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); +Goal "m * 0 = 0"; +by (induct_tac "m" 1); +by (ALLGOALS Asm_simp_tac); +qed "mult_0_right"; (*right successor law for multiplication*) -qed_goal "mult_Suc_right" thy "m * Suc(n) = m + (m * n)" - (fn _ => [induct_tac "m" 1, - ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]); +Goal "m * Suc(n) = m + (m * n)"; +by (induct_tac "m" 1); +by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))); +qed "mult_Suc_right"; Addsimps [mult_0_right, mult_Suc_right]; @@ -283,26 +299,35 @@ qed "mult_1_right"; (*Commutative law for multiplication*) -qed_goal "mult_commute" thy "m * n = n * (m::nat)" - (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); +Goal "m * n = n * (m::nat)"; +by (induct_tac "m" 1); +by (ALLGOALS Asm_simp_tac); +qed "mult_commute"; (*addition distributes over multiplication*) -qed_goal "add_mult_distrib" thy "(m + n)*k = (m*k) + ((n*k)::nat)" - (fn _ => [induct_tac "m" 1, - ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]); +Goal "(m + n)*k = (m*k) + ((n*k)::nat)"; +by (induct_tac "m" 1); +by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))); +qed "add_mult_distrib"; -qed_goal "add_mult_distrib2" thy "k*(m + n) = (k*m) + ((k*n)::nat)" - (fn _ => [induct_tac "m" 1, - ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]); +Goal "k*(m + n) = (k*m) + ((k*n)::nat)"; +by (induct_tac "m" 1); +by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))); +qed "add_mult_distrib2"; (*Associative law for multiplication*) -qed_goal "mult_assoc" thy "(m * n) * k = m * ((n * k)::nat)" - (fn _ => [induct_tac "m" 1, - ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib]))]); +Goal "(m * n) * k = m * ((n * k)::nat)"; +by (induct_tac "m" 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib]))); +qed "mult_assoc"; -qed_goal "mult_left_commute" thy "x*(y*z) = y*((x*z)::nat)" - (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1, - rtac mult_assoc 1, rtac (mult_commute RS arg_cong) 1]); +Goal "x*(y*z) = y*((x*z)::nat)"; +by (rtac trans 1); +by (rtac mult_commute 1); +by (rtac trans 1); +by (rtac mult_assoc 1); +by (rtac (mult_commute RS arg_cong) 1); +qed "mult_left_commute"; val mult_ac = [mult_assoc,mult_commute,mult_left_commute]; @@ -322,9 +347,11 @@ (*** Difference ***) +Goal "m - m = 0"; +by (induct_tac "m" 1); +by (ALLGOALS Asm_simp_tac); +qed "diff_self_eq_0"; -qed_goal "diff_self_eq_0" thy "m - m = 0" - (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); Addsimps [diff_self_eq_0]; (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *) diff -r 46048223e0f9 -r b46ccfee8e59 src/HOL/Divides.ML --- a/src/HOL/Divides.ML Wed Jul 14 13:32:21 1999 +0200 +++ b/src/HOL/Divides.ML Thu Jul 15 10:27:54 1999 +0200 @@ -97,7 +97,7 @@ (*** Quotient ***) Goal "(%m. m div n) = wfrec (trancl pred_nat) \ - \ (%f j. if j m div n = (if m m*n div n = m"; +Goal "0 (m*n) div n = m"; by (cut_inst_tac [("m", "m*n")] mod_div_equality 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1); diff -r 46048223e0f9 -r b46ccfee8e59 src/HOL/Prod.ML --- a/src/HOL/Prod.ML Wed Jul 14 13:32:21 1999 +0200 +++ b/src/HOL/Prod.ML Thu Jul 15 10:27:54 1999 +0200 @@ -321,24 +321,25 @@ (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]); (** Elimination of (a,b):A*B -- introduces no eigenvariables **) -qed_goal "SigmaD1" Prod.thy "(a,b) : Sigma A B ==> a : A" - (fn [major]=> - [ (rtac (major RS SigmaE) 1), - (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]); + +Goal "(a,b) : Sigma A B ==> a : A"; +by (etac SigmaE 1); +by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ; +qed "SigmaD1"; -qed_goal "SigmaD2" Prod.thy "(a,b) : Sigma A B ==> b : B(a)" - (fn [major]=> - [ (rtac (major RS SigmaE) 1), - (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]); +Goal "(a,b) : Sigma A B ==> b : B(a)"; +by (etac SigmaE 1); +by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ; +qed "SigmaD2"; -qed_goal "SigmaE2" Prod.thy +val [major,minor]= goal Prod.thy "[| (a,b) : Sigma A B; \ \ [| a:A; b:B(a) |] ==> P \ -\ |] ==> P" - (fn [major,minor]=> - [ (rtac minor 1), - (rtac (major RS SigmaD1) 1), - (rtac (major RS SigmaD2) 1) ]); +\ |] ==> P"; +by (rtac minor 1); +by (rtac (major RS SigmaD1) 1); +by (rtac (major RS SigmaD2) 1) ; +qed "SigmaE2"; AddSEs [SigmaE2, SigmaE]; @@ -348,11 +349,13 @@ by (blast_tac (claset() addIs (prems RL [subsetD])) 1); qed "Sigma_mono"; -qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}" - (fn _ => [ (Blast_tac 1) ]); +Goal "Sigma {} B = {}"; +by (Blast_tac 1) ; +qed "Sigma_empty1"; -qed_goal "Sigma_empty2" Prod.thy "A Times {} = {}" - (fn _ => [ (Blast_tac 1) ]); +Goal "A Times {} = {}"; +by (Blast_tac 1) ; +qed "Sigma_empty2"; Addsimps [Sigma_empty1,Sigma_empty2]; diff -r 46048223e0f9 -r b46ccfee8e59 src/HOL/Relation.ML --- a/src/HOL/Relation.ML Wed Jul 14 13:32:21 1999 +0200 +++ b/src/HOL/Relation.ML Thu Jul 15 10:27:54 1999 +0200 @@ -207,14 +207,14 @@ by (Blast_tac 1); qed "Domain_iff"; -qed_goal "DomainI" thy "!!a b r. (a,b): r ==> a: Domain(r)" - (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]); +Goal "(a,b): r ==> a: Domain(r)"; +by (etac (exI RS (Domain_iff RS iffD2)) 1) ; +qed "DomainI"; -qed_goal "DomainE" thy - "[| a : Domain(r); !!y. (a,y): r ==> P |] ==> P" - (fn prems=> - [ (rtac (Domain_iff RS iffD1 RS exE) 1), - (REPEAT (ares_tac prems 1)) ]); +val prems= Goal "[| a : Domain(r); !!y. (a,y): r ==> P |] ==> P"; +by (rtac (Domain_iff RS iffD1 RS exE) 1); +by (REPEAT (ares_tac prems 1)) ; +qed "DomainE"; AddIs [DomainI]; AddSEs [DomainE]; @@ -298,22 +298,23 @@ qed_goalw "Image_iff" thy [Image_def] "b : r^^A = (? x:A. (x,b):r)" - (fn _ => [ Blast_tac 1 ]); + (fn _ => [(Blast_tac 1)]); qed_goalw "Image_singleton" thy [Image_def] "r^^{a} = {b. (a,b):r}" - (fn _ => [ Blast_tac 1 ]); + (fn _ => [(Blast_tac 1)]); -qed_goal "Image_singleton_iff" thy - "(b : r^^{a}) = ((a,b):r)" - (fn _ => [ rtac (Image_iff RS trans) 1, - Blast_tac 1 ]); +Goal + "(b : r^^{a}) = ((a,b):r)"; +by (rtac (Image_iff RS trans) 1); +by (Blast_tac 1); +qed "Image_singleton_iff"; AddIffs [Image_singleton_iff]; -qed_goalw "ImageI" thy [Image_def] - "!!a b r. [| (a,b): r; a:A |] ==> b : r^^A" - (fn _ => [ (Blast_tac 1)]); +Goalw [Image_def] "[| (a,b): r; a:A |] ==> b : r^^A"; +by (Blast_tac 1); +qed "ImageI"; qed_goalw "ImageE" thy [Image_def] "[| b: r^^A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P" @@ -327,9 +328,10 @@ AddSEs [ImageE]; -qed_goal "Image_empty" thy - "R^^{} = {}" - (fn _ => [ Blast_tac 1 ]); +Goal + "R^^{} = {}"; +by (Blast_tac 1); +qed "Image_empty"; Addsimps [Image_empty]; @@ -343,17 +345,18 @@ Addsimps [Image_Id, Image_diag]; -qed_goal "Image_Int_subset" thy - "R ^^ (A Int B) <= R ^^ A Int R ^^ B" - (fn _ => [ Blast_tac 1 ]); +Goal "R ^^ (A Int B) <= R ^^ A Int R ^^ B"; +by (Blast_tac 1); +qed "Image_Int_subset"; -qed_goal "Image_Un" thy "R ^^ (A Un B) = R ^^ A Un R ^^ B" - (fn _ => [ Blast_tac 1 ]); +Goal "R ^^ (A Un B) = R ^^ A Un R ^^ B"; +by (Blast_tac 1); +qed "Image_Un"; -qed_goal "Image_subset" thy "!!A B r. r <= A Times B ==> r^^C <= B" - (fn _ => - [ (rtac subsetI 1), - (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]); +Goal "r <= A Times B ==> r^^C <= B"; +by (rtac subsetI 1); +by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ; +qed "Image_subset"; (*NOT suitable for rewriting*) Goal "r^^B = (UN y: B. r^^{y})"; diff -r 46048223e0f9 -r b46ccfee8e59 src/HOL/Set.ML --- a/src/HOL/Set.ML Wed Jul 14 13:32:21 1999 +0200 +++ b/src/HOL/Set.ML Thu Jul 15 10:27:54 1999 +0200 @@ -71,10 +71,11 @@ by (Blast_tac 1); qed "rev_bexI"; -qed_goal "bexCI" Set.thy - "[| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A. P(x)" (fn prems => - [ (rtac classical 1), - (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]); +val prems = goal Set.thy + "[| ! 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)) ; +qed "bexCI"; val major::prems = Goalw [Bex_def] "[| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q"; @@ -139,17 +140,20 @@ qed "subsetD"; (*The same, with reversed premises for use with etac -- cf rev_mp*) -qed_goal "rev_subsetD" Set.thy "[| c:A; A <= B |] ==> c:B" - (fn prems=> [ (REPEAT (resolve_tac (prems@[subsetD]) 1)) ]); +Goal "[| c:A; A <= B |] ==> c:B"; +by (REPEAT (ares_tac [subsetD] 1)) ; +qed "rev_subsetD"; (*Converts A<=B to x:A ==> x:B*) fun impOfSubs th = th RSN (2, rev_subsetD); -qed_goal "contra_subsetD" Set.thy "!!c. [| A <= B; c ~: B |] ==> c ~: A" - (fn prems=> [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]); +Goal "[| A <= B; c ~: B |] ==> c ~: A"; +by (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ; +qed "contra_subsetD"; -qed_goal "rev_contra_subsetD" Set.thy "!!c. [| c ~: B; A <= B |] ==> c ~: A" - (fn prems=> [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]); +Goal "[| c ~: B; A <= B |] ==> c ~: A"; +by (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ; +qed "rev_contra_subsetD"; (*Classical elimination rule*) val major::prems = Goalw [subset_def] @@ -164,8 +168,9 @@ AddSIs [subsetI]; AddEs [subsetD, subsetCE]; -qed_goal "subset_refl" Set.thy "A <= (A::'a set)" - (fn _=> [Fast_tac 1]); (*Blast_tac would try order_refl and fail*) +Goal "A <= (A::'a set)"; +by (Fast_tac 1); +qed "subset_refl"; (*Blast_tac would try order_refl and fail*) Goal "[| A<=B; B<=C |] ==> A<=(C::'a set)"; by (Blast_tac 1); @@ -242,29 +247,33 @@ section "The empty set -- {}"; -qed_goalw "empty_iff" Set.thy [empty_def] "(c : {}) = False" - (fn _ => [ (Blast_tac 1) ]); +Goalw [empty_def] "(c : {}) = False"; +by (Blast_tac 1) ; +qed "empty_iff"; Addsimps [empty_iff]; -qed_goal "emptyE" Set.thy "!!a. a:{} ==> P" - (fn _ => [Full_simp_tac 1]); +Goal "a:{} ==> P"; +by (Full_simp_tac 1); +qed "emptyE"; AddSEs [emptyE]; -qed_goal "empty_subsetI" Set.thy "{} <= A" - (fn _ => [ (Blast_tac 1) ]); +Goal "{} <= A"; +by (Blast_tac 1) ; +qed "empty_subsetI"; (*One effect is to delete the ASSUMPTION {} <= A*) AddIffs [empty_subsetI]; -qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}" - (fn [prem]=> - [ (blast_tac (claset() addIs [prem RS FalseE]) 1) ]); +val [prem]= goal Set.thy "[| !!y. y:A ==> False |] ==> A={}"; +by (blast_tac (claset() addIs [prem RS FalseE]) 1) ; +qed "equals0I"; (*Use for reasoning about disjointness: A Int B = {} *) -qed_goal "equals0D" Set.thy "!!a. A={} ==> a ~: A" - (fn _ => [ (Blast_tac 1) ]); +Goal "A={} ==> a ~: A"; +by (Blast_tac 1) ; +qed "equals0D"; AddDs [equals0D, sym RS equals0D]; @@ -286,16 +295,20 @@ section "The Powerset operator -- Pow"; -qed_goalw "Pow_iff" Set.thy [Pow_def] "(A : Pow(B)) = (A <= B)" - (fn _ => [ (Asm_simp_tac 1) ]); +Goalw [Pow_def] "(A : Pow(B)) = (A <= B)"; +by (Asm_simp_tac 1); +qed "Pow_iff"; AddIffs [Pow_iff]; -qed_goalw "PowI" Set.thy [Pow_def] "!!A B. A <= B ==> A : Pow(B)" - (fn _ => [ (etac CollectI 1) ]); +Goalw [Pow_def] "!!A B. A <= B ==> A : Pow(B)"; +by (etac CollectI 1); +qed "PowI"; -qed_goalw "PowD" Set.thy [Pow_def] "!!A B. A : Pow(B) ==> A<=B" - (fn _=> [ (etac CollectD 1) ]); +Goalw [Pow_def] "!!A B. A : Pow(B) ==> A<=B"; +by (etac CollectD 1); +qed "PowD"; + val Pow_bottom = empty_subsetI RS PowI; (* {}: Pow(B) *) val Pow_top = subset_refl RS PowI; (* A : Pow(A) *) @@ -341,10 +354,11 @@ qed "UnI2"; (*Classical introduction rule: no commitment to A vs B*) -qed_goal "UnCI" Set.thy "(c~:B ==> c:A) ==> c : A Un B" - (fn prems=> - [ (Simp_tac 1), - (REPEAT (ares_tac (prems@[disjCI]) 1)) ]); + +val prems= goal Set.thy "(c~:B ==> c:A) ==> c : A Un B"; +by (Simp_tac 1); +by (REPEAT (ares_tac (prems@[disjCI]) 1)) ; +qed "UnCI"; val major::prems = Goalw [Un_def] "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"; @@ -392,19 +406,22 @@ Addsimps [Diff_iff]; -qed_goal "DiffI" Set.thy "!!c. [| c : A; c ~: B |] ==> c : A - B" - (fn _=> [ Asm_simp_tac 1 ]); +Goal "[| c : A; c ~: B |] ==> c : A - B"; +by (Asm_simp_tac 1) ; +qed "DiffI"; -qed_goal "DiffD1" Set.thy "!!c. c : A - B ==> c : A" - (fn _=> [ (Asm_full_simp_tac 1) ]); +Goal "c : A - B ==> c : A"; +by (Asm_full_simp_tac 1) ; +qed "DiffD1"; -qed_goal "DiffD2" Set.thy "!!c. [| c : A - B; c : B |] ==> P" - (fn _=> [ (Asm_full_simp_tac 1) ]); +Goal "[| c : A - B; c : B |] ==> P"; +by (Asm_full_simp_tac 1) ; +qed "DiffD2"; -qed_goal "DiffE" Set.thy "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P" - (fn prems=> - [ (resolve_tac prems 1), - (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]); +val prems= goal Set.thy "[| 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"; AddSIs [DiffI]; AddSEs [DiffE]; @@ -417,31 +434,34 @@ Addsimps [insert_iff]; -qed_goal "insertI1" Set.thy "a : insert a B" - (fn _ => [Simp_tac 1]); - -qed_goal "insertI2" Set.thy "!!a. a : B ==> a : insert b B" - (fn _=> [Asm_simp_tac 1]); +val _ = goal Set.thy "a : insert a B"; +by (Simp_tac 1); +qed "insertI1"; -qed_goalw "insertE" Set.thy [insert_def] - "[| a : insert b A; a=b ==> P; a:A ==> P |] ==> P" - (fn major::prems=> - [ (rtac (major RS UnE) 1), - (REPEAT (eresolve_tac (prems @ [CollectE]) 1)) ]); +Goal "!!a. a : B ==> a : insert b B"; +by (Asm_simp_tac 1); +qed "insertI2"; + +val major::prems = Goalw [insert_def] + "[| a : insert b A; a=b ==> P; a:A ==> P |] ==> P"; +by (rtac (major RS UnE) 1); +by (REPEAT (eresolve_tac (prems @ [CollectE]) 1)); +qed "insertE"; (*Classical introduction rule*) -qed_goal "insertCI" Set.thy "(a~:B ==> a=b) ==> a: insert b B" - (fn prems=> - [ (Simp_tac 1), - (REPEAT (ares_tac (prems@[disjCI]) 1)) ]); +val prems= goal Set.thy "(a~:B ==> a=b) ==> a: insert b B"; +by (Simp_tac 1); +by (REPEAT (ares_tac (prems@[disjCI]) 1)) ; +qed "insertCI"; AddSIs [insertCI]; AddSEs [insertE]; section "Singletons, using insert"; -qed_goal "singletonI" Set.thy "a : {a}" - (fn _=> [ (rtac insertI1 1) ]); +Goal "a : {a}"; +by (rtac insertI1 1) ; +qed "singletonI"; Goal "b : {a} ==> b=a"; by (Blast_tac 1); @@ -449,8 +469,9 @@ bind_thm ("singletonE", make_elim singletonD); -qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" -(fn _ => [Blast_tac 1]); +Goal "(b : {a}) = (b=a)"; +by (Blast_tac 1); +qed "singleton_iff"; Goal "{a}={b} ==> a=b"; by (blast_tac (claset() addEs [equalityE]) 1); diff -r 46048223e0f9 -r b46ccfee8e59 src/HOL/Trancl.ML --- a/src/HOL/Trancl.ML Wed Jul 14 13:32:21 1999 +0200 +++ b/src/HOL/Trancl.ML Thu Jul 15 10:27:54 1999 +0200 @@ -251,7 +251,7 @@ \ !!x y. (x,y) : r ==> P x y; \ \ !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z \ \ |] ==> P x y"; -by(blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1); +by (blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1); qed "trancl_trans_induct"; (*elimination of r^+ -- NOT an induction rule*) @@ -326,13 +326,13 @@ qed "converse_trancl_induct"; (*Unused*) -qed_goal "irrefl_tranclI" Trancl.thy - "!!r. r^-1 Int r^+ = {} ==> (x, x) ~: r^+" - (K [subgoal_tac "!y. (x, y) : r^+ --> x~=y" 1, - Fast_tac 1, - strip_tac 1, - etac trancl_induct 1, - auto_tac (claset() addIs [r_into_trancl], simpset())]); +Goal "r^-1 Int r^+ = {} ==> (x, x) ~: r^+"; +by (subgoal_tac "!y. (x, y) : r^+ --> x~=y" 1); +by (Fast_tac 1); +by (strip_tac 1); +by (etac trancl_induct 1); +by (auto_tac (claset() addIs [r_into_trancl], simpset())); +qed "irrefl_tranclI"; Goal "[| (a,b) : r^*; r <= A Times A |] ==> a=b | a:A"; by (etac rtrancl_induct 1); @@ -368,10 +368,13 @@ qed "trancl_reflcl"; Addsimps[trancl_reflcl]; -qed_goal "trancl_empty" Trancl.thy "{}^+ = {}" - (K [auto_tac (claset() addEs [trancl_induct], simpset())]); +Goal "{}^+ = {}"; +by (auto_tac (claset() addEs [trancl_induct], simpset())); +qed "trancl_empty"; Addsimps[trancl_empty]; -qed_goal "rtrancl_empty" Trancl.thy "{}^* = Id" - (K [rtac (reflcl_trancl RS subst) 1, Simp_tac 1]); +Goal "{}^* = Id"; +by (rtac (reflcl_trancl RS subst) 1); +by (Simp_tac 1); +qed "rtrancl_empty"; Addsimps[rtrancl_empty]; diff -r 46048223e0f9 -r b46ccfee8e59 src/HOL/cladata.ML --- a/src/HOL/cladata.ML Wed Jul 14 13:32:21 1999 +0200 +++ b/src/HOL/cladata.ML Thu Jul 15 10:27:54 1999 +0200 @@ -53,15 +53,15 @@ claset_ref() := HOL_cs; (*Better then ex1E for classical reasoner: needs no quantifier duplication!*) -qed_goal "alt_ex1E" thy +val major::prems = goal thy "[| ?! x. P(x); \ \ !!x. [| P(x); ALL y y'. P(y) & P(y') --> y=y' |] ==> R \ -\ |] ==> R" - (fn major::prems => - [ (rtac (major RS ex1E) 1), - (REPEAT (ares_tac (allI::prems) 1)), - (etac (dup_elim allE) 1), - (Fast_tac 1)]); +\ |] ==> R"; +by (rtac (major RS ex1E) 1); +by (REPEAT (ares_tac (allI::prems) 1)); +by (etac (dup_elim allE) 1); +by (Fast_tac 1); +qed "alt_ex1E"; AddSEs [alt_ex1E]; diff -r 46048223e0f9 -r b46ccfee8e59 src/HOL/subset.ML --- a/src/HOL/subset.ML Wed Jul 14 13:32:21 1999 +0200 +++ b/src/HOL/subset.ML Thu Jul 15 10:27:54 1999 +0200 @@ -9,8 +9,10 @@ (*** insert ***) -qed_goal "subset_insertI" Set.thy "B <= insert a B" - (fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]); +Goal "B <= insert a B"; +by (rtac subsetI 1); +by (etac insertI2 1) ; +qed "subset_insertI"; Goal "x ~: A ==> (A <= insert x B) = (A <= B)"; by (Blast_tac 1); @@ -89,8 +91,9 @@ (*** Set difference ***) -qed_goal "Diff_subset" Set.thy "A-B <= (A::'a set)" - (fn _ => [ (Blast_tac 1) ]); +Goal "A-B <= (A::'a set)"; +by (Blast_tac 1) ; +qed "Diff_subset"; (*** Monotonicity ***)