# HG changeset patch # User paulson # Date 938518674 -7200 # Node ID 6680b3b8944b4a4f0bf1dec71d1e48ecbd50018c # Parent e783adccf39e9524b14ad4a4742cc684e53fb81c more tidying diff -r e783adccf39e -r 6680b3b8944b src/HOL/HOL_lemmas.ML --- a/src/HOL/HOL_lemmas.ML Mon Sep 27 10:25:10 1999 +0200 +++ b/src/HOL/HOL_lemmas.ML Tue Sep 28 13:37:54 1999 +0200 @@ -37,15 +37,17 @@ (** Equality **) section "="; -qed_goal "sym" (the_context ()) "s=t ==> t=s" - (fn prems => [cut_facts_tac prems 1, etac subst 1, rtac refl 1]); +Goal "s=t ==> t=s"; +by (etac subst 1); +by (rtac refl 1); +qed "sym"; (*calling "standard" reduces maxidx to 0*) -bind_thm ("ssubst", (sym RS subst)); +bind_thm ("ssubst", sym RS subst); -qed_goal "trans" (the_context ()) "[| r=s; s=t |] ==> r=t" - (fn prems => - [rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]); +Goal "[| r=s; s=t |] ==> r=t"; +by (etac subst 1 THEN assume_tac 1); +qed "trans"; val prems = goal (the_context ()) "(A == B) ==> A = B"; by (rewrite_goals_tac prems); @@ -63,58 +65,67 @@ by (REPEAT (assume_tac 1)) ; qed "box_equals"; - (** Congruence rules for meta-application **) section "Congruence"; (*similar to AP_THM in Gordon's HOL*) -qed_goal "fun_cong" (the_context ()) "(f::'a=>'b) = g ==> f(x)=g(x)" - (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]); +Goal "(f::'a=>'b) = g ==> f(x)=g(x)"; +by (etac subst 1); +by (rtac refl 1); +qed "fun_cong"; (*similar to AP_TERM in Gordon's HOL and FOL's subst_context*) -qed_goal "arg_cong" (the_context ()) "x=y ==> f(x)=f(y)" - (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]); +Goal "x=y ==> f(x)=f(y)"; +by (etac subst 1); +by (rtac refl 1); +qed "arg_cong"; -qed_goal "cong" (the_context ()) - "[| f = g; (x::'a) = y |] ==> f(x) = g(y)" - (fn [prem1,prem2] => - [rtac (prem1 RS subst) 1, rtac (prem2 RS subst) 1, rtac refl 1]); - +Goal "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"; +by (etac subst 1); +by (etac subst 1); +by (rtac refl 1); +qed "cong"; (** Equality of booleans -- iff **) section "iff"; -val prems = Goal - "[| P ==> Q; Q ==> P |] ==> P=Q"; +val prems = Goal "[| P ==> Q; Q ==> P |] ==> P=Q"; by (REPEAT (ares_tac (prems@[impI, iff RS mp RS mp]) 1)); qed "iffI"; -qed_goal "iffD2" (the_context ()) "[| P=Q; Q |] ==> P" - (fn prems => - [rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]); +Goal "[| P=Q; Q |] ==> P"; +by (etac ssubst 1); +by (assume_tac 1); +qed "iffD2"; -qed_goal "rev_iffD2" (the_context ()) "!!P. [| Q; P=Q |] ==> P" - (fn _ => [etac iffD2 1, assume_tac 1]); +Goal "[| Q; P=Q |] ==> P"; +by (etac iffD2 1); +by (assume_tac 1); +qed "rev_iffD2"; bind_thm ("iffD1", sym RS iffD2); bind_thm ("rev_iffD1", sym RSN (2, rev_iffD2)); -qed_goal "iffE" (the_context ()) - "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R" - (fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2, p1 RS iffD1, p2, impI])1)]); +val [p1,p2] = Goal "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R"; +by (REPEAT (ares_tac [p1 RS iffD2, p1 RS iffD1, p2, impI] 1)); +qed "iffE"; (** True **) section "True"; -qed_goalw "TrueI" (the_context ()) [True_def] "True" - (fn _ => [(rtac refl 1)]); +Goalw [True_def] "True"; +by (rtac refl 1); +qed "TrueI"; -qed_goal "eqTrueI" (the_context ()) "P ==> P=True" - (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]); +Goal "P ==> P=True"; +by (REPEAT (ares_tac [iffI,TrueI] 1)); +qed "eqTrueI"; -qed_goal "eqTrueE" (the_context ()) "P=True ==> P" - (fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]); +Goal "P=True ==> P"; +by (etac iffD2 1); +by (rtac TrueI 1); +qed "eqTrueE"; (** Universal quantifier **)