--- a/src/HOL/HOL.ML Wed Aug 25 20:46:40 1999 +0200
+++ b/src/HOL/HOL.ML Wed Aug 25 20:49:02 1999 +0200
@@ -1,456 +1,31 @@
-(* Title: HOL/HOL.ML
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1991 University of Cambridge
-Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68
-*)
-
-
-(** Equality **)
-section "=";
-
-qed_goal "sym" HOL.thy "s=t ==> t=s"
- (fn prems => [cut_facts_tac prems 1, etac subst 1, rtac refl 1]);
-
-(*calling "standard" reduces maxidx to 0*)
-bind_thm ("ssubst", (sym RS subst));
-
-qed_goal "trans" HOL.thy "[| r=s; s=t |] ==> r=t"
- (fn prems =>
- [rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]);
-
-val prems = goal thy "(A == B) ==> A = B";
-by (rewrite_goals_tac prems);
-by (rtac refl 1);
-qed "def_imp_eq";
-
-(*Useful with eresolve_tac for proving equalties from known equalities.
- a = b
- | |
- c = d *)
-Goal "[| a=b; a=c; b=d |] ==> c=d";
-by (rtac trans 1);
-by (rtac trans 1);
-by (rtac sym 1);
-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" HOL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
- (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
-
-(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
-qed_goal "arg_cong" HOL.thy "x=y ==> f(x)=f(y)"
- (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
-
-qed_goal "cong" HOL.thy
- "[| 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]);
-
-
-(** Equality of booleans -- iff **)
-section "iff";
-
-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" HOL.thy "[| P=Q; Q |] ==> P"
- (fn prems =>
- [rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]);
-
-qed_goal "rev_iffD2" HOL.thy "!!P. [| Q; P=Q |] ==> P"
- (fn _ => [etac iffD2 1, assume_tac 1]);
-
-bind_thm ("iffD1", sym RS iffD2);
-bind_thm ("rev_iffD1", sym RSN (2, rev_iffD2));
-
-qed_goal "iffE" HOL.thy
- "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R"
- (fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2, p1 RS iffD1, p2, impI])1)]);
-
-
-(** True **)
-section "True";
-
-qed_goalw "TrueI" HOL.thy [True_def] "True"
- (fn _ => [(rtac refl 1)]);
-
-qed_goal "eqTrueI" HOL.thy "P ==> P=True"
- (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
-
-qed_goal "eqTrueE" HOL.thy "P=True ==> P"
- (fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]);
-
-
-(** Universal quantifier **)
-section "!";
-
-qed_goalw "allI" HOL.thy [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
- (fn prems => [(resolve_tac (prems RL [eqTrueI RS ext]) 1)]);
-
-qed_goalw "spec" HOL.thy [All_def] "! x::'a. P(x) ==> P(x)"
- (fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]);
-
-val major::prems= goal HOL.thy "[| !x. P(x); P(x) ==> R |] ==> R";
-by (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ;
-qed "allE";
-
-val prems = goal HOL.thy
- "[| ! x. P(x); [| P(x); ! x. P(x) |] ==> R |] ==> R";
-by (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ;
-qed "all_dupE";
-
-
-(** False ** Depends upon spec; it is impossible to do propositional logic
- before quantifiers! **)
-section "False";
-
-qed_goalw "FalseE" HOL.thy [False_def] "False ==> P"
- (fn [major] => [rtac (major RS spec) 1]);
-
-qed_goal "False_neq_True" HOL.thy "False=True ==> P"
- (fn [prem] => [rtac (prem RS eqTrueE RS FalseE) 1]);
-
-
-(** Negation **)
-section "~";
-
-qed_goalw "notI" HOL.thy [not_def] "(P ==> False) ==> ~P"
- (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
-
-qed_goal "False_not_True" HOL.thy "False ~= True"
- (fn _ => [rtac notI 1, etac False_neq_True 1]);
-
-qed_goal "True_not_False" HOL.thy "True ~= False"
- (fn _ => [rtac notI 1, dtac sym 1, etac False_neq_True 1]);
-
-qed_goalw "notE" HOL.thy [not_def] "[| ~P; P |] ==> R"
- (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
-
-bind_thm ("classical2", notE RS notI);
-
-qed_goal "rev_notE" HOL.thy "!!P R. [| P; ~P |] ==> R"
- (fn _ => [REPEAT (ares_tac [notE] 1)]);
-
-
-(** Implication **)
-section "-->";
-
-val prems = Goal "[| P-->Q; P; Q ==> R |] ==> R";
-by (REPEAT (resolve_tac (prems@[mp]) 1));
-qed "impE";
-
-(* Reduces Q to P-->Q, allowing substitution in P. *)
-Goal "[| P; P --> Q |] ==> Q";
-by (REPEAT (ares_tac [mp] 1)) ;
-qed "rev_mp";
-
-val [major,minor] = Goal "[| ~Q; P==>Q |] ==> ~P";
-by (rtac (major RS notE RS notI) 1);
-by (etac minor 1) ;
-qed "contrapos";
-
-val [major,minor] = Goal "[| P==>Q; ~Q |] ==> ~P";
-by (rtac (minor RS contrapos) 1);
-by (etac major 1) ;
-qed "rev_contrapos";
-
-(* ~(?t = ?s) ==> ~(?s = ?t) *)
-bind_thm("not_sym", sym COMP rev_contrapos);
-
-
-(** Existential quantifier **)
-section "?";
-
-qed_goalw "exI" HOL.thy [Ex_def] "P x ==> ? x::'a. P x"
- (fn prems => [rtac selectI 1, resolve_tac prems 1]);
-
-qed_goalw "exE" HOL.thy [Ex_def]
- "[| ? x::'a. P(x); !!x. P(x) ==> Q |] ==> Q"
- (fn prems => [REPEAT(resolve_tac prems 1)]);
-
-
-(** Conjunction **)
-section "&";
-
-qed_goalw "conjI" HOL.thy [and_def] "[| P; Q |] ==> P&Q"
- (fn prems =>
- [REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)]);
-
-qed_goalw "conjunct1" HOL.thy [and_def] "[| P & Q |] ==> P"
- (fn prems =>
- [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
-
-qed_goalw "conjunct2" HOL.thy [and_def] "[| P & Q |] ==> Q"
- (fn prems =>
- [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
-
-qed_goal "conjE" HOL.thy "[| P&Q; [| P; Q |] ==> R |] ==> R"
- (fn prems =>
- [cut_facts_tac prems 1, resolve_tac prems 1,
- etac conjunct1 1, etac conjunct2 1]);
-
-qed_goal "context_conjI" HOL.thy "[| P; P ==> Q |] ==> P & Q"
- (fn prems => [REPEAT(resolve_tac (conjI::prems) 1)]);
-
-
-(** Disjunction *)
-section "|";
-
-qed_goalw "disjI1" HOL.thy [or_def] "P ==> P|Q"
- (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
-
-qed_goalw "disjI2" HOL.thy [or_def] "Q ==> P|Q"
- (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
-
-qed_goalw "disjE" HOL.thy [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R"
- (fn [a1,a2,a3] =>
- [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
- rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]);
-
-
-(** CCONTR -- classical logic **)
-section "classical logic";
-
-qed_goalw "classical" HOL.thy [not_def] "(~P ==> P) ==> P"
- (fn [prem] =>
- [rtac (True_or_False RS (disjE RS eqTrueE)) 1, assume_tac 1,
- rtac (impI RS prem RS eqTrueI) 1,
- etac subst 1, assume_tac 1]);
-
-val ccontr = FalseE RS classical;
-
-(*Double negation law*)
-Goal "~~P ==> P";
-by (rtac classical 1);
-by (etac notE 1);
-by (assume_tac 1);
-qed "notnotD";
-
-val [p1,p2] = Goal "[| Q; ~ P ==> ~ Q |] ==> P";
-by (rtac classical 1);
-by (dtac p2 1);
-by (etac notE 1);
-by (rtac p1 1);
-qed "contrapos2";
-
-val [p1,p2] = Goal "[| P; Q ==> ~ P |] ==> ~ Q";
-by (rtac notI 1);
-by (dtac p2 1);
-by (etac notE 1);
-by (rtac p1 1);
-qed "swap2";
-
-(** Unique existence **)
-section "?!";
-
-qed_goalw "ex1I" HOL.thy [Ex1_def]
- "[| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
- (fn prems =>
- [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
-
-(*Sometimes easier to use: the premises have no shared variables. Safe!*)
-val [ex,eq] = Goal
- "[| ? x. P(x); !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)";
-by (rtac (ex RS exE) 1);
-by (REPEAT (ares_tac [ex1I,eq] 1)) ;
-qed "ex_ex1I";
-
-qed_goalw "ex1E" HOL.thy [Ex1_def]
- "[| ?! x. P(x); !!x. [| P(x); ! y. P(y) --> y=x |] ==> R |] ==> R"
- (fn major::prems =>
- [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
-
-Goal "?! x. P x ==> ? x. P x";
-by (etac ex1E 1);
-by (rtac exI 1);
-by (assume_tac 1);
-qed "ex1_implies_ex";
-
-
-(** Select: Hilbert's Epsilon-operator **)
-section "@";
-
-(*Easier to apply than selectI: conclusion has only one occurrence of P*)
-val prems = Goal
- "[| P a; !!x. P x ==> Q x |] ==> Q (@x. P x)";
-by (resolve_tac prems 1);
-by (rtac selectI 1);
-by (resolve_tac prems 1) ;
-qed "selectI2";
-
-(*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
-qed_goal "selectI2EX" HOL.thy
- "[| ? a. P a; !!x. P x ==> Q x |] ==> Q (Eps P)"
-(fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
-
-val prems = Goal
- "[| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a";
-by (rtac selectI2 1);
-by (REPEAT (ares_tac prems 1)) ;
-qed "select_equality";
-
-Goalw [Ex1_def] "[| ?!x. P x; P a |] ==> (@x. P x) = a";
-by (rtac select_equality 1);
-by (atac 1);
-by (etac exE 1);
-by (etac conjE 1);
-by (rtac allE 1);
-by (atac 1);
-by (etac impE 1);
-by (atac 1);
-by (etac ssubst 1);
-by (etac allE 1);
-by (etac mp 1);
-by (atac 1);
-qed "select1_equality";
-
-Goal "P (@ x. P x) = (? x. P x)";
-by (rtac iffI 1);
-by (etac exI 1);
-by (etac exE 1);
-by (etac selectI 1);
-qed "select_eq_Ex";
-
-Goal "(@y. y=x) = x";
-by (rtac select_equality 1);
-by (rtac refl 1);
-by (atac 1);
-qed "Eps_eq";
-
-Goal "(Eps (op = x)) = x";
-by (rtac select_equality 1);
-by (rtac refl 1);
-by (etac sym 1);
-qed "Eps_sym_eq";
-
-(** Classical intro rules for disjunction and existential quantifiers *)
-section "classical intro rules";
-
-val prems= Goal "(~Q ==> P) ==> P|Q";
-by (rtac classical 1);
-by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
-by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
-qed "disjCI";
-
-Goal "~P | P";
-by (REPEAT (ares_tac [disjCI] 1)) ;
-qed "excluded_middle";
-
-(*For disjunctive case analysis*)
-fun excluded_middle_tac sP =
- res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
-
-(*Classical implies (-->) elimination. *)
-val major::prems = Goal "[| P-->Q; ~P ==> R; Q ==> R |] ==> R";
-by (rtac (excluded_middle RS disjE) 1);
-by (REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1)));
-qed "impCE";
-
-(*This version of --> elimination works on Q before P. It works best for
- those cases in which P holds "almost everywhere". Can't install as
- default: would break old proofs.*)
-val major::prems = Goal
- "[| P-->Q; Q ==> R; ~P ==> R |] ==> R";
-by (resolve_tac [excluded_middle RS disjE] 1);
-by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
-qed "impCE'";
-
-(*Classical <-> elimination. *)
-val major::prems = Goal
- "[| P=Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R";
-by (rtac (major RS iffE) 1);
-by (REPEAT (DEPTH_SOLVE_1
- (eresolve_tac ([asm_rl,impCE,notE]@prems) 1)));
-qed "iffCE";
-
-val prems = Goal "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)";
-by (rtac ccontr 1);
-by (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1)) ;
-qed "exCI";
-
-
-(* case distinction *)
-
-qed_goal "case_split_thm" HOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
- (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
- etac p2 1, etac p1 1]);
-
-fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
-
-
-(** Standard abbreviations **)
-
-(*Apply an equality or definition ONCE.
- Fails unless the substitution has an effect*)
-fun stac th =
- let val th' = th RS def_imp_eq handle THM _ => th
- in CHANGED_GOAL (rtac (th' RS ssubst))
- end;
-
-fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);
-
-
-(** strip ! and --> from proved goal while preserving !-bound var names **)
-
-local
-
-(* Use XXX to avoid forall_intr failing because of duplicate variable name *)
-val myspec = read_instantiate [("P","?XXX")] spec;
-val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
-val cvx = cterm_of (#sign(rep_thm myspec)) vx;
-val aspec = forall_intr cvx myspec;
-
-in
-
-fun RSspec th =
- (case concl_of th of
- _ $ (Const("All",_) $ Abs(a,_,_)) =>
- let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
- in th RS forall_elim ca aspec end
- | _ => raise THM("RSspec",0,[th]));
-
-fun RSmp th =
- (case concl_of th of
- _ $ (Const("op -->",_)$_$_) => th RS mp
- | _ => raise THM("RSmp",0,[th]));
-
-fun normalize_thm funs =
- let fun trans [] th = th
- | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
- in zero_var_indexes o trans funs end;
-
-fun qed_spec_mp name =
- let val thm = normalize_thm [RSspec,RSmp] (result())
- in ThmDatabase.ml_store_thm(name, thm) end;
-
-fun qed_goal_spec_mp name thy s p =
- bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
-
-fun qed_goalw_spec_mp name thy defs s p =
- bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
-
+structure HOL =
+struct
+ val thy = the_context ();
+ val plusI = plusI;
+ val minusI = minusI;
+ val timesI = timesI;
+ val powerI = powerI;
+ val eq_reflection = eq_reflection;
+ val refl = refl;
+ val subst = subst;
+ val ext = ext;
+ val selectI = selectI;
+ val impI = impI;
+ val mp = mp;
+ val True_def = True_def;
+ val All_def = All_def;
+ val Ex_def = Ex_def;
+ val False_def = False_def;
+ val not_def = not_def;
+ val and_def = and_def;
+ val or_def = or_def;
+ val Ex1_def = Ex1_def;
+ val iff = iff;
+ val True_or_False = True_or_False;
+ val Let_def = Let_def;
+ val if_def = if_def;
+ val arbitrary_def = arbitrary_def;
end;
-
-(* attributes *)
-
-local
-
-fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (fn _ => (normalize_thm [RSspec, RSmp]))) x;
-
-in
-
-val hol_setup =
- [Attrib.add_attributes
- [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
-
-end;
+open HOL;
--- a/src/HOL/HOL.thy Wed Aug 25 20:46:40 1999 +0200
+++ b/src/HOL/HOL.thy Wed Aug 25 20:49:02 1999 +0200
@@ -6,72 +6,63 @@
Higher-Order Logic.
*)
-HOL = CPure +
+theory HOL = CPure
+files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML"):
(** Core syntax **)
global
-classes
- term < logic
+classes "term" < logic
+defaultsort "term"
-default
- term
-
-types
- bool
+typedecl bool
arities
- fun :: (term, term) term
- bool :: term
+ bool :: "term"
+ fun :: ("term", "term") "term"
consts
(* Constants *)
- Trueprop :: bool => prop ("(_)" 5)
- Not :: bool => bool ("~ _" [40] 40)
- True, False :: bool
- If :: [bool, 'a, 'a] => 'a ("(if (_)/ then (_)/ else (_))" 10)
+ Trueprop :: "bool => prop" ("(_)" 5)
+ Not :: "bool => bool" ("~ _" [40] 40)
+ True :: bool
+ False :: bool
+ If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10)
arbitrary :: 'a
(* Binders *)
- Eps :: ('a => bool) => 'a
- All :: ('a => bool) => bool (binder "ALL " 10)
- Ex :: ('a => bool) => bool (binder "EX " 10)
- Ex1 :: ('a => bool) => bool (binder "EX! " 10)
- Let :: ['a, 'a => 'b] => 'b
+ Eps :: "('a => bool) => 'a"
+ All :: "('a => bool) => bool" (binder "ALL " 10)
+ Ex :: "('a => bool) => bool" (binder "EX " 10)
+ Ex1 :: "('a => bool) => bool" (binder "EX! " 10)
+ Let :: "['a, 'a => 'b] => 'b"
(* Infixes *)
- "=" :: ['a, 'a] => bool (infixl 50)
- "&" :: [bool, bool] => bool (infixr 35)
- "|" :: [bool, bool] => bool (infixr 30)
- "-->" :: [bool, bool] => bool (infixr 25)
+ "=" :: "['a, 'a] => bool" (infixl 50)
+ & :: "[bool, bool] => bool" (infixr 35)
+ "|" :: "[bool, bool] => bool" (infixr 30)
+ --> :: "[bool, bool] => bool" (infixr 25)
(* Overloaded Constants *)
-axclass
- plus < term
-
-axclass
- minus < term
-
-axclass
- times < term
-
-axclass
- power < term
+axclass plus < "term"
+axclass minus < "term"
+axclass times < "term"
+axclass power < "term"
consts
- "+" :: ['a::plus, 'a] => 'a (infixl 65)
- "-" :: ['a::minus, 'a] => 'a (infixl 65)
- uminus :: ['a::minus] => 'a ("- _" [81] 80)
- "*" :: ['a::times, 'a] => 'a (infixl 70)
+ "+" :: "['a::plus, 'a] => 'a" (infixl 65)
+ - :: "['a::minus, 'a] => 'a" (infixl 65)
+ uminus :: "['a::minus] => 'a" ("- _" [81] 80)
+ "*" :: "['a::times, 'a] => 'a" (infixl 70)
(*See Nat.thy for "^"*)
@@ -83,22 +74,22 @@
case_syn cases_syn
syntax
- "~=" :: ['a, 'a] => bool (infixl 50)
- "_Eps" :: [pttrn, bool] => 'a ("(3SOME _./ _)" [0, 10] 10)
+ ~= :: "['a, 'a] => bool" (infixl 50)
+ "_Eps" :: "[pttrn, bool] => 'a" ("(3SOME _./ _)" [0, 10] 10)
(* Let expressions *)
- "_bind" :: [pttrn, 'a] => letbind ("(2_ =/ _)" 10)
- "" :: letbind => letbinds ("_")
- "_binds" :: [letbind, letbinds] => letbinds ("_;/ _")
- "_Let" :: [letbinds, 'a] => 'a ("(let (_)/ in (_))" 10)
+ "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10)
+ "" :: "letbind => letbinds" ("_")
+ "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _")
+ "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
(* Case expressions *)
- "@case" :: ['a, cases_syn] => 'b ("(case _ of/ _)" 10)
- "@case1" :: ['a, 'b] => case_syn ("(2_ =>/ _)" 10)
- "" :: case_syn => cases_syn ("_")
- "@case2" :: [case_syn, cases_syn] => cases_syn ("_/ | _")
+ "@case" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10)
+ "@case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10)
+ "" :: "case_syn => cases_syn" ("_")
+ "@case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _")
translations
"x ~= y" == "~ (x = y)"
@@ -107,37 +98,37 @@
"let x = a in e" == "Let a (%x. e)"
syntax ("" output)
- "op =" :: ['a, 'a] => bool ("(_ =/ _)" [51, 51] 50)
- "op ~=" :: ['a, 'a] => bool ("(_ ~=/ _)" [51, 51] 50)
+ "op =" :: "['a, 'a] => bool" ("(_ =/ _)" [51, 51] 50)
+ "op ~=" :: "['a, 'a] => bool" ("(_ ~=/ _)" [51, 51] 50)
syntax (symbols)
- Not :: bool => bool ("\\<not> _" [40] 40)
- "op &" :: [bool, bool] => bool (infixr "\\<and>" 35)
- "op |" :: [bool, bool] => bool (infixr "\\<or>" 30)
- "op -->" :: [bool, bool] => bool (infixr "\\<midarrow>\\<rightarrow>" 25)
- "op o" :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl "\\<circ>" 55)
- "op ~=" :: ['a, 'a] => bool (infixl "\\<noteq>" 50)
- "_Eps" :: [pttrn, bool] => 'a ("(3\\<epsilon>_./ _)" [0, 10] 10)
- "ALL " :: [idts, bool] => bool ("(3\\<forall>_./ _)" [0, 10] 10)
- "EX " :: [idts, bool] => bool ("(3\\<exists>_./ _)" [0, 10] 10)
- "EX! " :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10)
- "@case1" :: ['a, 'b] => case_syn ("(2_ \\<Rightarrow>/ _)" 10)
-(*"@case2" :: [case_syn, cases_syn] => cases_syn ("_/ \\<orelse> _")*)
+ Not :: "bool => bool" ("\\<not> _" [40] 40)
+ "op &" :: "[bool, bool] => bool" (infixr "\\<and>" 35)
+ "op |" :: "[bool, bool] => bool" (infixr "\\<or>" 30)
+ "op -->" :: "[bool, bool] => bool" (infixr "\\<midarrow>\\<rightarrow>" 25)
+ "op o" :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "\\<circ>" 55)
+ "op ~=" :: "['a, 'a] => bool" (infixl "\\<noteq>" 50)
+ "_Eps" :: "[pttrn, bool] => 'a" ("(3\\<epsilon>_./ _)" [0, 10] 10)
+ "ALL " :: "[idts, bool] => bool" ("(3\\<forall>_./ _)" [0, 10] 10)
+ "EX " :: "[idts, bool] => bool" ("(3\\<exists>_./ _)" [0, 10] 10)
+ "EX! " :: "[idts, bool] => bool" ("(3\\<exists>!_./ _)" [0, 10] 10)
+ "@case1" :: "['a, 'b] => case_syn" ("(2_ \\<Rightarrow>/ _)" 10)
+(*"@case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \\<orelse> _")*)
syntax (symbols output)
- "op ~=" :: ['a, 'a] => bool ("(_ \\<noteq>/ _)" [51, 51] 50)
+ "op ~=" :: "['a, 'a] => bool" ("(_ \\<noteq>/ _)" [51, 51] 50)
syntax (xsymbols)
- "op -->" :: [bool, bool] => bool (infixr "\\<longrightarrow>" 25)
+ "op -->" :: "[bool, bool] => bool" (infixr "\\<longrightarrow>" 25)
syntax (HTML output)
- Not :: bool => bool ("\\<not> _" [40] 40)
+ Not :: "bool => bool" ("\\<not> _" [40] 40)
syntax (HOL)
- "_Eps" :: [pttrn, bool] => 'a ("(3@ _./ _)" [0, 10] 10)
- "ALL " :: [idts, bool] => bool ("(3! _./ _)" [0, 10] 10)
- "EX " :: [idts, bool] => bool ("(3? _./ _)" [0, 10] 10)
- "EX! " :: [idts, bool] => bool ("(3?! _./ _)" [0, 10] 10)
+ "_Eps" :: "[pttrn, bool] => 'a" ("(3@ _./ _)" [0, 10] 10)
+ "ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10)
+ "EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10)
+ "EX! " :: "[idts, bool] => bool" ("(3?! _./ _)" [0, 10] 10)
@@ -145,57 +136,59 @@
local
-rules
+axioms
- eq_reflection "(x=y) ==> (x==y)"
+ eq_reflection: "(x=y) ==> (x==y)"
(* Basic Rules *)
- refl "t = (t::'a)"
- subst "[| s = t; P(s) |] ==> P(t::'a)"
+ refl: "t = (t::'a)"
+ subst: "[| s = t; P(s) |] ==> P(t::'a)"
(*Extensionality is built into the meta-logic, and this rule expresses
a related property. It is an eta-expanded version of the traditional
rule, and similar to the ABS rule of HOL.*)
- ext "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
+ ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
- selectI "P (x::'a) ==> P (@x. P x)"
+ selectI: "P (x::'a) ==> P (@x. P x)"
- impI "(P ==> Q) ==> P-->Q"
- mp "[| P-->Q; P |] ==> Q"
+ impI: "(P ==> Q) ==> P-->Q"
+ mp: "[| P-->Q; P |] ==> Q"
defs
- True_def "True == ((%x::bool. x) = (%x. x))"
- All_def "All(P) == (P = (%x. True))"
- Ex_def "Ex(P) == P(@x. P(x))"
- False_def "False == (!P. P)"
- not_def "~ P == P-->False"
- and_def "P & Q == !R. (P-->Q-->R) --> R"
- or_def "P | Q == !R. (P-->R) --> (Q-->R) --> R"
- Ex1_def "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)"
+ True_def: "True == ((%x::bool. x) = (%x. x))"
+ All_def: "All(P) == (P = (%x. True))"
+ Ex_def: "Ex(P) == P(@x. P(x))"
+ False_def: "False == (!P. P)"
+ not_def: "~ P == P-->False"
+ and_def: "P & Q == !R. (P-->Q-->R) --> R"
+ or_def: "P | Q == !R. (P-->R) --> (Q-->R) --> R"
+ Ex1_def: "Ex1(P) == ? x. P(x) & (! y. P(y) --> y=x)"
-rules
+axioms
(* Axioms *)
- iff "(P-->Q) --> (Q-->P) --> (P=Q)"
- True_or_False "(P=True) | (P=False)"
+ iff: "(P-->Q) --> (Q-->P) --> (P=Q)"
+ True_or_False: "(P=True) | (P=False)"
defs
(*misc definitions*)
- Let_def "Let s f == f(s)"
- if_def "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
+ Let_def: "Let s f == f(s)"
+ if_def: "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
(*arbitrary is completely unspecified, but is made to appear as a
definition syntactically*)
- arbitrary_def "False ==> arbitrary == (@x. False)"
+ arbitrary_def: "False ==> arbitrary == (@x. False)"
-(** initial HOL theory setup **)
+(* theory and package setup *)
-setup Simplifier.setup
-setup ClasetThyData.setup
+use "HOL_lemmas.ML" setup attrib_setup
+use "cladata.ML" setup Classical.setup setup clasetup
+use "blastdata.ML" setup Blast.setup
+use "simpdata.ML" setup Simplifier.setup setup simpsetup setup Clasimp.setup
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOL_lemmas.ML Wed Aug 25 20:49:02 1999 +0200
@@ -0,0 +1,484 @@
+(* Title: HOL/HOL_lemmas.ML
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1991 University of Cambridge
+
+Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68.
+*)
+
+(* ML bindings *)
+
+val plusI = thm "plusI";
+val minusI = thm "minusI";
+val timesI = thm "timesI";
+val powerI = thm "powerI";
+val eq_reflection = thm "eq_reflection";
+val refl = thm "refl";
+val subst = thm "subst";
+val ext = thm "ext";
+val selectI = thm "selectI";
+val impI = thm "impI";
+val mp = thm "mp";
+val True_def = thm "True_def";
+val All_def = thm "All_def";
+val Ex_def = thm "Ex_def";
+val False_def = thm "False_def";
+val not_def = thm "not_def";
+val and_def = thm "and_def";
+val or_def = thm "or_def";
+val Ex1_def = thm "Ex1_def";
+val iff = thm "iff";
+val True_or_False = thm "True_or_False";
+val Let_def = thm "Let_def";
+val if_def = thm "if_def";
+val arbitrary_def = thm "arbitrary_def";
+
+
+(** Equality **)
+section "=";
+
+qed_goal "sym" (the_context ()) "s=t ==> t=s"
+ (fn prems => [cut_facts_tac prems 1, etac subst 1, rtac refl 1]);
+
+(*calling "standard" reduces maxidx to 0*)
+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]);
+
+val prems = goal (the_context ()) "(A == B) ==> A = B";
+by (rewrite_goals_tac prems);
+by (rtac refl 1);
+qed "def_imp_eq";
+
+(*Useful with eresolve_tac for proving equalties from known equalities.
+ a = b
+ | |
+ c = d *)
+Goal "[| a=b; a=c; b=d |] ==> c=d";
+by (rtac trans 1);
+by (rtac trans 1);
+by (rtac sym 1);
+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]);
+
+(*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]);
+
+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]);
+
+
+(** Equality of booleans -- iff **)
+section "iff";
+
+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]);
+
+qed_goal "rev_iffD2" (the_context ()) "!!P. [| Q; P=Q |] ==> P"
+ (fn _ => [etac iffD2 1, assume_tac 1]);
+
+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)]);
+
+
+(** True **)
+section "True";
+
+qed_goalw "TrueI" (the_context ()) [True_def] "True"
+ (fn _ => [(rtac refl 1)]);
+
+qed_goal "eqTrueI" (the_context ()) "P ==> P=True"
+ (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
+
+qed_goal "eqTrueE" (the_context ()) "P=True ==> P"
+ (fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]);
+
+
+(** Universal quantifier **)
+section "!";
+
+qed_goalw "allI" (the_context ()) [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
+ (fn prems => [(resolve_tac (prems RL [eqTrueI RS ext]) 1)]);
+
+qed_goalw "spec" (the_context ()) [All_def] "! x::'a. P(x) ==> P(x)"
+ (fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]);
+
+val major::prems= goal (the_context ()) "[| !x. P(x); P(x) ==> R |] ==> R";
+by (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ;
+qed "allE";
+
+val prems = goal (the_context ())
+ "[| ! x. P(x); [| P(x); ! x. P(x) |] ==> R |] ==> R";
+by (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ;
+qed "all_dupE";
+
+
+(** False ** Depends upon spec; it is impossible to do propositional logic
+ before quantifiers! **)
+section "False";
+
+qed_goalw "FalseE" (the_context ()) [False_def] "False ==> P"
+ (fn [major] => [rtac (major RS spec) 1]);
+
+qed_goal "False_neq_True" (the_context ()) "False=True ==> P"
+ (fn [prem] => [rtac (prem RS eqTrueE RS FalseE) 1]);
+
+
+(** Negation **)
+section "~";
+
+qed_goalw "notI" (the_context ()) [not_def] "(P ==> False) ==> ~P"
+ (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
+
+qed_goal "False_not_True" (the_context ()) "False ~= True"
+ (fn _ => [rtac notI 1, etac False_neq_True 1]);
+
+qed_goal "True_not_False" (the_context ()) "True ~= False"
+ (fn _ => [rtac notI 1, dtac sym 1, etac False_neq_True 1]);
+
+qed_goalw "notE" (the_context ()) [not_def] "[| ~P; P |] ==> R"
+ (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
+
+bind_thm ("classical2", notE RS notI);
+
+qed_goal "rev_notE" (the_context ()) "!!P R. [| P; ~P |] ==> R"
+ (fn _ => [REPEAT (ares_tac [notE] 1)]);
+
+
+(** Implication **)
+section "-->";
+
+val prems = Goal "[| P-->Q; P; Q ==> R |] ==> R";
+by (REPEAT (resolve_tac (prems@[mp]) 1));
+qed "impE";
+
+(* Reduces Q to P-->Q, allowing substitution in P. *)
+Goal "[| P; P --> Q |] ==> Q";
+by (REPEAT (ares_tac [mp] 1)) ;
+qed "rev_mp";
+
+val [major,minor] = Goal "[| ~Q; P==>Q |] ==> ~P";
+by (rtac (major RS notE RS notI) 1);
+by (etac minor 1) ;
+qed "contrapos";
+
+val [major,minor] = Goal "[| P==>Q; ~Q |] ==> ~P";
+by (rtac (minor RS contrapos) 1);
+by (etac major 1) ;
+qed "rev_contrapos";
+
+(* ~(?t = ?s) ==> ~(?s = ?t) *)
+bind_thm("not_sym", sym COMP rev_contrapos);
+
+
+(** Existential quantifier **)
+section "?";
+
+qed_goalw "exI" (the_context ()) [Ex_def] "P x ==> ? x::'a. P x"
+ (fn prems => [rtac selectI 1, resolve_tac prems 1]);
+
+qed_goalw "exE" (the_context ()) [Ex_def]
+ "[| ? x::'a. P(x); !!x. P(x) ==> Q |] ==> Q"
+ (fn prems => [REPEAT(resolve_tac prems 1)]);
+
+
+(** Conjunction **)
+section "&";
+
+qed_goalw "conjI" (the_context ()) [and_def] "[| P; Q |] ==> P&Q"
+ (fn prems =>
+ [REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)]);
+
+qed_goalw "conjunct1" (the_context ()) [and_def] "[| P & Q |] ==> P"
+ (fn prems =>
+ [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
+
+qed_goalw "conjunct2" (the_context ()) [and_def] "[| P & Q |] ==> Q"
+ (fn prems =>
+ [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
+
+qed_goal "conjE" (the_context ()) "[| P&Q; [| P; Q |] ==> R |] ==> R"
+ (fn prems =>
+ [cut_facts_tac prems 1, resolve_tac prems 1,
+ etac conjunct1 1, etac conjunct2 1]);
+
+qed_goal "context_conjI" (the_context ()) "[| P; P ==> Q |] ==> P & Q"
+ (fn prems => [REPEAT(resolve_tac (conjI::prems) 1)]);
+
+
+(** Disjunction *)
+section "|";
+
+qed_goalw "disjI1" (the_context ()) [or_def] "P ==> P|Q"
+ (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
+
+qed_goalw "disjI2" (the_context ()) [or_def] "Q ==> P|Q"
+ (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
+
+qed_goalw "disjE" (the_context ()) [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R"
+ (fn [a1,a2,a3] =>
+ [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
+ rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]);
+
+
+(** CCONTR -- classical logic **)
+section "classical logic";
+
+qed_goalw "classical" (the_context ()) [not_def] "(~P ==> P) ==> P"
+ (fn [prem] =>
+ [rtac (True_or_False RS (disjE RS eqTrueE)) 1, assume_tac 1,
+ rtac (impI RS prem RS eqTrueI) 1,
+ etac subst 1, assume_tac 1]);
+
+val ccontr = FalseE RS classical;
+
+(*Double negation law*)
+Goal "~~P ==> P";
+by (rtac classical 1);
+by (etac notE 1);
+by (assume_tac 1);
+qed "notnotD";
+
+val [p1,p2] = Goal "[| Q; ~ P ==> ~ Q |] ==> P";
+by (rtac classical 1);
+by (dtac p2 1);
+by (etac notE 1);
+by (rtac p1 1);
+qed "contrapos2";
+
+val [p1,p2] = Goal "[| P; Q ==> ~ P |] ==> ~ Q";
+by (rtac notI 1);
+by (dtac p2 1);
+by (etac notE 1);
+by (rtac p1 1);
+qed "swap2";
+
+(** Unique existence **)
+section "?!";
+
+qed_goalw "ex1I" (the_context ()) [Ex1_def]
+ "[| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
+ (fn prems =>
+ [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
+
+(*Sometimes easier to use: the premises have no shared variables. Safe!*)
+val [ex,eq] = Goal
+ "[| ? x. P(x); !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)";
+by (rtac (ex RS exE) 1);
+by (REPEAT (ares_tac [ex1I,eq] 1)) ;
+qed "ex_ex1I";
+
+qed_goalw "ex1E" (the_context ()) [Ex1_def]
+ "[| ?! x. P(x); !!x. [| P(x); ! y. P(y) --> y=x |] ==> R |] ==> R"
+ (fn major::prems =>
+ [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
+
+Goal "?! x. P x ==> ? x. P x";
+by (etac ex1E 1);
+by (rtac exI 1);
+by (assume_tac 1);
+qed "ex1_implies_ex";
+
+
+(** Select: Hilbert's Epsilon-operator **)
+section "@";
+
+(*Easier to apply than selectI: conclusion has only one occurrence of P*)
+val prems = Goal
+ "[| P a; !!x. P x ==> Q x |] ==> Q (@x. P x)";
+by (resolve_tac prems 1);
+by (rtac selectI 1);
+by (resolve_tac prems 1) ;
+qed "selectI2";
+
+(*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
+qed_goal "selectI2EX" (the_context ())
+ "[| ? a. P a; !!x. P x ==> Q x |] ==> Q (Eps P)"
+(fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
+
+val prems = Goal
+ "[| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a";
+by (rtac selectI2 1);
+by (REPEAT (ares_tac prems 1)) ;
+qed "select_equality";
+
+Goalw [Ex1_def] "[| ?!x. P x; P a |] ==> (@x. P x) = a";
+by (rtac select_equality 1);
+by (atac 1);
+by (etac exE 1);
+by (etac conjE 1);
+by (rtac allE 1);
+by (atac 1);
+by (etac impE 1);
+by (atac 1);
+by (etac ssubst 1);
+by (etac allE 1);
+by (etac mp 1);
+by (atac 1);
+qed "select1_equality";
+
+Goal "P (@ x. P x) = (? x. P x)";
+by (rtac iffI 1);
+by (etac exI 1);
+by (etac exE 1);
+by (etac selectI 1);
+qed "select_eq_Ex";
+
+Goal "(@y. y=x) = x";
+by (rtac select_equality 1);
+by (rtac refl 1);
+by (atac 1);
+qed "Eps_eq";
+
+Goal "(Eps (op = x)) = x";
+by (rtac select_equality 1);
+by (rtac refl 1);
+by (etac sym 1);
+qed "Eps_sym_eq";
+
+(** Classical intro rules for disjunction and existential quantifiers *)
+section "classical intro rules";
+
+val prems= Goal "(~Q ==> P) ==> P|Q";
+by (rtac classical 1);
+by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
+by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
+qed "disjCI";
+
+Goal "~P | P";
+by (REPEAT (ares_tac [disjCI] 1)) ;
+qed "excluded_middle";
+
+(*For disjunctive case analysis*)
+fun excluded_middle_tac sP =
+ res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
+
+(*Classical implies (-->) elimination. *)
+val major::prems = Goal "[| P-->Q; ~P ==> R; Q ==> R |] ==> R";
+by (rtac (excluded_middle RS disjE) 1);
+by (REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1)));
+qed "impCE";
+
+(*This version of --> elimination works on Q before P. It works best for
+ those cases in which P holds "almost everywhere". Can't install as
+ default: would break old proofs.*)
+val major::prems = Goal
+ "[| P-->Q; Q ==> R; ~P ==> R |] ==> R";
+by (resolve_tac [excluded_middle RS disjE] 1);
+by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
+qed "impCE'";
+
+(*Classical <-> elimination. *)
+val major::prems = Goal
+ "[| P=Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R";
+by (rtac (major RS iffE) 1);
+by (REPEAT (DEPTH_SOLVE_1
+ (eresolve_tac ([asm_rl,impCE,notE]@prems) 1)));
+qed "iffCE";
+
+val prems = Goal "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)";
+by (rtac ccontr 1);
+by (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1)) ;
+qed "exCI";
+
+
+(* case distinction *)
+
+qed_goal "case_split_thm" (the_context ()) "[| P ==> Q; ~P ==> Q |] ==> Q"
+ (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
+ etac p2 1, etac p1 1]);
+
+fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
+
+
+(** Standard abbreviations **)
+
+(*Apply an equality or definition ONCE.
+ Fails unless the substitution has an effect*)
+fun stac th =
+ let val th' = th RS def_imp_eq handle THM _ => th
+ in CHANGED_GOAL (rtac (th' RS ssubst))
+ end;
+
+fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);
+
+
+(** strip ! and --> from proved goal while preserving !-bound var names **)
+
+local
+
+(* Use XXX to avoid forall_intr failing because of duplicate variable name *)
+val myspec = read_instantiate [("P","?XXX")] spec;
+val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
+val cvx = cterm_of (#sign(rep_thm myspec)) vx;
+val aspec = forall_intr cvx myspec;
+
+in
+
+fun RSspec th =
+ (case concl_of th of
+ _ $ (Const("All",_) $ Abs(a,_,_)) =>
+ let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
+ in th RS forall_elim ca aspec end
+ | _ => raise THM("RSspec",0,[th]));
+
+fun RSmp th =
+ (case concl_of th of
+ _ $ (Const("op -->",_)$_$_) => th RS mp
+ | _ => raise THM("RSmp",0,[th]));
+
+fun normalize_thm funs =
+ let fun trans [] th = th
+ | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
+ in zero_var_indexes o trans funs end;
+
+fun qed_spec_mp name =
+ let val thm = normalize_thm [RSspec,RSmp] (result())
+ in ThmDatabase.ml_store_thm(name, thm) end;
+
+fun qed_goal_spec_mp name thy s p =
+ bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
+
+fun qed_goalw_spec_mp name thy defs s p =
+ bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
+
+end;
+
+
+(* attributes *)
+
+local
+
+fun gen_rulify x =
+ Attrib.no_args (Drule.rule_attribute (fn _ => (normalize_thm [RSspec, RSmp]))) x;
+
+in
+
+val attrib_setup =
+ [Attrib.add_attributes
+ [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
+
+end;
--- a/src/HOL/Inductive.thy Wed Aug 25 20:46:40 1999 +0200
+++ b/src/HOL/Inductive.thy Wed Aug 25 20:49:02 1999 +0200
@@ -1,5 +1,6 @@
-Inductive = Gfp + Prod + Sum +
+theory Inductive = Gfp + Prod + Sum
+files "Tools/inductive_package.ML":
setup InductivePackage.setup
--- a/src/HOL/IsaMakefile Wed Aug 25 20:46:40 1999 +0200
+++ b/src/HOL/IsaMakefile Wed Aug 25 20:49:02 1999 +0200
@@ -32,9 +32,9 @@
@cd $(SRC)/Pure; $(ISATOOL) make Pure
$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
- $(SRC)/Provers/Arith/cancel_sums.ML \
- $(SRC)/Provers/Arith/assoc_fold.ML \
- $(SRC)/Provers/Arith/combine_coeff.ML \
+ $(SRC)/Provers/Arith/cancel_sums.ML \
+ $(SRC)/Provers/Arith/assoc_fold.ML \
+ $(SRC)/Provers/Arith/combine_coeff.ML \
$(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
$(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
@@ -47,24 +47,25 @@
$(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy \
Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML \
Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
- Inductive.thy Integ/Bin.ML Integ/Bin.thy Integ/Equiv.ML \
- Integ/Equiv.thy Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML \
- Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML \
- Integ/NatBin.thy Integ/simproc.ML Lfp.ML Lfp.thy List.ML List.thy \
- Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy \
- Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy \
- Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
- Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
- SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
- Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
- Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
- Tools/induct_method.ML Tools/inductive_package.ML \
- Tools/numeral_syntax.ML Tools/primrec_package.ML \
- Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
- Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
- Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy cladata.ML \
- equalities.ML equalities.thy hologic.ML mono.ML mono.thy simpdata.ML \
- subset.ML subset.thy thy_syntax.ML
+ HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
+ Integ/Equiv.ML Integ/Equiv.thy Integ/IntDef.ML Integ/IntDef.thy \
+ Integ/Int.ML Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy \
+ Integ/NatBin.ML Integ/NatBin.thy Integ/simproc.ML Lfp.ML Lfp.thy \
+ List.ML List.thy Main.thy Map.ML Map.thy Nat.ML Nat.thy NatDef.ML \
+ NatDef.thy Numeral.thy Option.ML Option.thy Ord.ML Ord.thy Power.ML \
+ Power.thy Prod.ML Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML \
+ RelPow.thy Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy \
+ String.thy SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.thy \
+ Tools/datatype_aux.ML Tools/datatype_abs_proofs.ML \
+ Tools/datatype_package.ML Tools/datatype_prop.ML \
+ Tools/datatype_rep_proofs.ML Tools/induct_method.ML \
+ Tools/inductive_package.ML Tools/numeral_syntax.ML \
+ Tools/primrec_package.ML Tools/recdef_package.ML \
+ Tools/record_package.ML Tools/svc_funcs.ML Tools/typedef_package.ML \
+ Trancl.ML Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML \
+ WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML cladata.ML equalities.ML \
+ equalities.thy hologic.ML mono.ML mono.thy simpdata.ML subset.ML \
+ subset.thy thy_syntax.ML
@$(ISATOOL) usedir -b $(OUT)/Pure HOL
--- a/src/HOL/Ord.thy Wed Aug 25 20:46:40 1999 +0200
+++ b/src/HOL/Ord.thy Wed Aug 25 20:49:02 1999 +0200
@@ -8,13 +8,6 @@
Ord = HOL +
-(*FIXME move to HOL.thy*)
-setup hol_setup
-setup Classical.setup
-setup Blast.setup
-setup Clasimp.setup
-setup simpdata_setup
-
axclass
ord < term
--- a/src/HOL/ROOT.ML Wed Aug 25 20:46:40 1999 +0200
+++ b/src/HOL/ROOT.ML Wed Aug 25 20:49:02 1999 +0200
@@ -15,6 +15,7 @@
(*old-style theory syntax*)
use "~~/src/Pure/section_utils.ML";
use "thy_syntax.ML";
+use "hologic.ML";
use "~~/src/Provers/simplifier.ML";
use "~~/src/Provers/split_paired_all.ML";
@@ -29,24 +30,14 @@
use "~~/src/Provers/Arith/abel_cancel.ML";
use "~~/src/Provers/Arith/assoc_fold.ML";
use "~~/src/Provers/quantifier1.ML";
+use "~~/src/Provers/Arith/combine_coeff.ML";
-use_thy "HOL";
-use "hologic.ML";
-use "~~/src/Provers/Arith/combine_coeff.ML";
-use "cladata.ML";
-use "simpdata.ML";
-
-use_thy "Ord";
use_thy "subset";
use "Tools/typedef_package.ML";
-use_thy "Sum";
-use_thy "Gfp";
+use_thy "Inductive";
use_thy "NatDef";
-use "Tools/inductive_package.ML";
-use_thy "Inductive";
-
use "Tools/datatype_aux.ML";
use "Tools/datatype_prop.ML";
use "Tools/datatype_rep_proofs.ML";
@@ -54,20 +45,13 @@
use "Tools/datatype_package.ML";
use "Tools/primrec_package.ML";
use_thy "Datatype";
-use_thy "Numeral";
-
-use "Tools/record_package.ML";
-use_thy "Record";
(*TFL: recursive function definitions*)
use_thy "WF_Rel";
-cd "../TFL";
-use "sys.sml";
-cd "../HOL";
-use "Tools/recdef_package.ML";
-use "Tools/induct_method.ML";
+cd "../TFL"; use "sys.sml"; cd "../HOL";
use_thy "Recdef";
+use_thy "Numeral";
cd "Integ";
use_thy "IntDef";
use "simproc.ML";
--- a/src/HOL/Recdef.thy Wed Aug 25 20:46:40 1999 +0200
+++ b/src/HOL/Recdef.thy Wed Aug 25 20:49:02 1999 +0200
@@ -1,5 +1,6 @@
-Recdef = WF_Rel +
+theory Recdef = WF_Rel
+files "Tools/recdef_package.ML" "Tools/induct_method.ML":
setup RecdefPackage.setup
setup InductMethod.setup
--- a/src/HOL/Record.thy Wed Aug 25 20:46:40 1999 +0200
+++ b/src/HOL/Record.thy Wed Aug 25 20:49:02 1999 +0200
@@ -6,7 +6,8 @@
Tools/record_package.ML for the actual implementation.
*)
-Record = Datatype +
+theory Record = Datatype
+files "Tools/record_package.ML":
(* concrete syntax *)
@@ -42,8 +43,9 @@
(* type class for record extensions *)
-axclass more < term
+axclass more < "term"
instance unit :: more
+ by intro_classes
(* initialize the package *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/blastdata.ML Wed Aug 25 20:49:02 1999 +0200
@@ -0,0 +1,34 @@
+
+(*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
+val major::prems = goal (the_context ())
+ "[| ?! x. P(x); \
+\ !!x. [| P(x); ALL y y'. P(y) & P(y') --> y=y' |] ==> R \
+\ |] ==> 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];
+
+(*** Applying BlastFun to create Blast_tac ***)
+structure Blast_Data =
+ struct
+ type claset = Classical.claset
+ val notE = notE
+ val ccontr = ccontr
+ val contr_tac = Classical.contr_tac
+ val dup_intr = Classical.dup_intr
+ val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
+ val claset = Classical.claset
+ val rep_cs = Classical.rep_cs
+ val cla_modifiers = Classical.cla_modifiers;
+ val cla_meth' = Classical.cla_meth'
+ end;
+
+structure Blast = BlastFun(Blast_Data);
+Blast.overloaded ("op =", domain_type); (*overloading of equality as iff*)
+
+val Blast_tac = Blast.Blast_tac
+and blast_tac = Blast.blast_tac;
--- a/src/HOL/cladata.ML Wed Aug 25 20:46:40 1999 +0200
+++ b/src/HOL/cladata.ML Wed Aug 25 20:49:02 1999 +0200
@@ -22,7 +22,7 @@
val rev_mp = rev_mp
val subst = subst
val sym = sym
- val thin_refl = prove_goal HOL.thy
+ val thin_refl = prove_goal (the_context ())
"!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
end;
@@ -40,7 +40,8 @@
end;
structure Classical = ClassicalFun(Classical_Data);
-open Classical;
+structure BasicClassical: BASIC_CLASSICAL = Classical;
+open BasicClassical;
(*Propositional rules*)
val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
@@ -50,38 +51,4 @@
val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, select_equality]
addSEs [exE] addEs [allE];
-claset_ref() := HOL_cs;
-
-(*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
-val major::prems = goal thy
- "[| ?! x. P(x); \
-\ !!x. [| P(x); ALL y y'. P(y) & P(y') --> y=y' |] ==> R \
-\ |] ==> 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];
-
-(*** Applying BlastFun to create Blast_tac ***)
-structure Blast_Data =
- struct
- type claset = Classical.claset
- val notE = notE
- val ccontr = ccontr
- val contr_tac = Classical.contr_tac
- val dup_intr = Classical.dup_intr
- val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
- val claset = Classical.claset
- val rep_cs = Classical.rep_cs
- val cla_modifiers = Classical.cla_modifiers;
- val cla_meth' = Classical.cla_meth'
- end;
-
-structure Blast = BlastFun(Blast_Data);
-Blast.overloaded ("op =", domain_type); (*overloading of equality as iff*)
-
-val Blast_tac = Blast.Blast_tac
-and blast_tac = Blast.blast_tac;
+val clasetup = [fn thy => (claset_ref_of thy := HOL_cs; thy)];
--- a/src/HOL/simpdata.ML Wed Aug 25 20:46:40 1999 +0200
+++ b/src/HOL/simpdata.ML Wed Aug 25 20:49:02 1999 +0200
@@ -89,14 +89,14 @@
end;
-val [prem] = goal HOL.thy "x==y ==> x=y";
+val [prem] = goal (the_context ()) "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 (fn _ => [(Blast_tac 1)]);
+ fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]);
in
@@ -157,7 +157,7 @@
val imp_cong = impI RSN
- (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
+ (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
(fn _=> [(Blast_tac 1)]) RS mp RS mp);
(*Miniscoping: pushing in existential quantifiers*)
@@ -182,10 +182,10 @@
(* elimination of existential quantifiers in assumptions *)
val ex_all_equiv =
- let val lemma1 = prove_goal HOL.thy
+ let val lemma1 = prove_goal (the_context ())
"(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)"
(fn prems => [resolve_tac prems 1, etac exI 1]);
- val lemma2 = prove_goalw HOL.thy [Ex_def]
+ val lemma2 = prove_goalw (the_context ()) [Ex_def]
"(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
(fn prems => [(REPEAT(resolve_tac prems 1))])
in equal_intr lemma1 lemma2 end;
@@ -194,13 +194,13 @@
(* Elimination of True from asumptions: *)
-val True_implies_equals = prove_goal HOL.thy
+val True_implies_equals = prove_goal (the_context ())
"(True ==> PROP P) == PROP P"
(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 (fn _ => [(Blast_tac 1)]);
+fun prove nm thm = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]);
prove "conj_commute" "(P&Q) = (Q&P)";
prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
@@ -255,19 +255,19 @@
(* '&' congruence rule: not included by default!
May slow rewrite proofs down by as much as 50% *)
-let val th = prove_goal HOL.thy
+let val th = prove_goal (the_context ())
"(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
(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
+let val th = prove_goal (the_context ())
"(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
(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
+let val th = prove_goal (the_context ())
"(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
(fn _=> [(Blast_tac 1)])
in bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp))) end;
@@ -358,10 +358,10 @@
local
val ex_pattern =
- Thm.read_cterm (Theory.sign_of HOL.thy) ("EX x. P(x) & Q(x)",HOLogic.boolT)
+ Thm.read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)",HOLogic.boolT)
val all_pattern =
- Thm.read_cterm (Theory.sign_of HOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
+ Thm.read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
in
val defEX_regroup =
@@ -478,7 +478,7 @@
(*For expand_case_tac*)
-val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
+val prems = goal (the_context ()) "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
by (case_tac "P" 1);
by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems)));
val expand_case = result();
@@ -491,9 +491,8 @@
Simp_tac i;
-(* install implicit simpset *)
-
-simpset_ref() := HOL_ss addcongs [if_weak_cong];
+(* default simpset *)
+val simpsetup = [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; thy)];
(*** integration of simplifier with classical reasoner ***)