--- a/src/Pure/drule.ML Sat May 15 21:09:54 2010 +0200
+++ b/src/Pure/drule.ML Sat May 15 21:41:32 2010 +0200
@@ -204,11 +204,11 @@
(** Standardization of rules **)
(*Generalization over a list of variables*)
-val forall_intr_list = fold_rev forall_intr;
+val forall_intr_list = fold_rev Thm.forall_intr;
(*Generalization over Vars -- canonical order*)
fun forall_intr_vars th =
- fold forall_intr
+ fold Thm.forall_intr
(map (Thm.cterm_of (Thm.theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th [])) th;
fun outer_params t =
@@ -245,10 +245,10 @@
fun generalize names th = Thm.generalize names (Thm.maxidx_of th + 1) th;
(*specialization over a list of cterms*)
-val forall_elim_list = fold forall_elim;
+val forall_elim_list = fold Thm.forall_elim;
(*maps A1,...,An |- B to [| A1;...;An |] ==> B*)
-val implies_intr_list = fold_rev implies_intr;
+val implies_intr_list = fold_rev Thm.implies_intr;
(*maps [| A1;...;An |] ==> B and [A1,...,An] to B*)
fun implies_elim_list impth ths = fold Thm.elim_implies ths impth;
@@ -278,7 +278,7 @@
This step can lose information.*)
fun flexflex_unique th =
if null (tpairs_of th) then th else
- case distinct Thm.eq_thm (Seq.list_of (flexflex_rule th)) of
+ case distinct Thm.eq_thm (Seq.list_of (Thm.flexflex_rule th)) of
[th] => th
| [] => raise THM("flexflex_unique: impossible constraints", 0, [th])
| _ => raise THM("flexflex_unique: multiple unifiers", 0, [th]);
@@ -464,8 +464,8 @@
fun extensional eq =
let val eq' =
- abstract_rule "x" (Thm.dest_arg (fst (Thm.dest_equals (cprop_of eq)))) eq
- in equal_elim (eta_conversion (cprop_of eq')) eq' end;
+ Thm.abstract_rule "x" (Thm.dest_arg (fst (Thm.dest_equals (cprop_of eq)))) eq
+ in Thm.equal_elim (Thm.eta_conversion (cprop_of eq')) eq' end;
val equals_cong =
store_standard_thm_open (Binding.name "equals_cong")
@@ -478,13 +478,13 @@
val AC = read_prop "A ==> C"
val A = read_prop "A"
in
- store_standard_thm_open (Binding.name "imp_cong") (implies_intr ABC (equal_intr
- (implies_intr AB (implies_intr A
- (equal_elim (implies_elim (assume ABC) (assume A))
- (implies_elim (assume AB) (assume A)))))
- (implies_intr AC (implies_intr A
- (equal_elim (symmetric (implies_elim (assume ABC) (assume A)))
- (implies_elim (assume AC) (assume A)))))))
+ store_standard_thm_open (Binding.name "imp_cong") (Thm.implies_intr ABC (Thm.equal_intr
+ (Thm.implies_intr AB (Thm.implies_intr A
+ (Thm.equal_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A))
+ (Thm.implies_elim (Thm.assume AB) (Thm.assume A)))))
+ (Thm.implies_intr AC (Thm.implies_intr A
+ (Thm.equal_elim (Thm.symmetric (Thm.implies_elim (Thm.assume ABC) (Thm.assume A)))
+ (Thm.implies_elim (Thm.assume AC) (Thm.assume A)))))))
end;
val swap_prems_eq =
@@ -495,11 +495,11 @@
val B = read_prop "B"
in
store_standard_thm_open (Binding.name "swap_prems_eq")
- (equal_intr
- (implies_intr ABC (implies_intr B (implies_intr A
- (implies_elim (implies_elim (assume ABC) (assume A)) (assume B)))))
- (implies_intr BAC (implies_intr A (implies_intr B
- (implies_elim (implies_elim (assume BAC) (assume B)) (assume A))))))
+ (Thm.equal_intr
+ (Thm.implies_intr ABC (Thm.implies_intr B (Thm.implies_intr A
+ (Thm.implies_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A)) (Thm.assume B)))))
+ (Thm.implies_intr BAC (Thm.implies_intr A (Thm.implies_intr B
+ (Thm.implies_elim (Thm.implies_elim (Thm.assume BAC) (Thm.assume B)) (Thm.assume A))))))
end;
val imp_cong_rule = Thm.combination o Thm.combination (Thm.reflexive implies);
@@ -513,16 +513,18 @@
val rhs_of = snd o dest_eq
in
fun beta_eta_conversion t =
- let val thm = beta_conversion true t
- in transitive thm (eta_conversion (rhs_of thm)) end
+ let val thm = Thm.beta_conversion true t
+ in Thm.transitive thm (Thm.eta_conversion (rhs_of thm)) end
end;
-fun eta_long_conversion ct = transitive (beta_eta_conversion ct)
- (symmetric (beta_eta_conversion (cterm_fun (Pattern.eta_long []) ct)));
+fun eta_long_conversion ct =
+ Thm.transitive
+ (beta_eta_conversion ct)
+ (Thm.symmetric (beta_eta_conversion (cterm_fun (Pattern.eta_long []) ct)));
(*Contract all eta-redexes in the theorem, lest they give rise to needless abstractions*)
fun eta_contraction_rule th =
- equal_elim (eta_conversion (cprop_of th)) th;
+ Thm.equal_elim (Thm.eta_conversion (cprop_of th)) th;
(* abs_def *)
@@ -578,7 +580,7 @@
val VW = read_prop "V ==> W";
in
store_standard_thm_open (Binding.name "revcut_rl")
- (implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V))))
+ (Thm.implies_intr V (Thm.implies_intr VW (Thm.implies_elim (Thm.assume VW) (Thm.assume V))))
end;
(*for deleting an unwanted assumption*)
@@ -586,7 +588,7 @@
let
val V = read_prop "V";
val W = read_prop "W";
- val thm = implies_intr V (implies_intr W (assume W));
+ val thm = Thm.implies_intr V (Thm.implies_intr W (Thm.assume W));
in store_standard_thm_open (Binding.name "thin_rl") thm end;
(* (!!x. PROP ?V) == PROP ?V Allows removal of redundant parameters*)
@@ -597,8 +599,8 @@
val x = certify (Free ("x", Term.aT []));
in
store_standard_thm_open (Binding.name "triv_forall_equality")
- (equal_intr (implies_intr QV (forall_elim x (assume QV)))
- (implies_intr V (forall_intr x (assume V))))
+ (Thm.equal_intr (Thm.implies_intr QV (Thm.forall_elim x (Thm.assume QV)))
+ (Thm.implies_intr V (Thm.forall_intr x (Thm.assume V))))
end;
(* (PROP ?Phi ==> PROP ?Phi ==> PROP ?Psi) ==>
@@ -610,7 +612,7 @@
val A = read_prop "Phi";
in
store_standard_thm_open (Binding.name "distinct_prems_rl")
- (implies_intr_list [AAB, A] (implies_elim_list (assume AAB) [assume A, assume A]))
+ (implies_intr_list [AAB, A] (implies_elim_list (Thm.assume AAB) [Thm.assume A, Thm.assume A]))
end;
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
@@ -620,15 +622,15 @@
val swap_prems_rl =
let
val cmajor = read_prop "PhiA ==> PhiB ==> Psi";
- val major = assume cmajor;
+ val major = Thm.assume cmajor;
val cminor1 = read_prop "PhiA";
- val minor1 = assume cminor1;
+ val minor1 = Thm.assume cminor1;
val cminor2 = read_prop "PhiB";
- val minor2 = assume cminor2;
+ val minor2 = Thm.assume cminor2;
in
store_standard_thm_open (Binding.name "swap_prems_rl")
- (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
- (implies_elim (implies_elim major minor1) minor2))))
+ (Thm.implies_intr cmajor (Thm.implies_intr cminor2 (Thm.implies_intr cminor1
+ (Thm.implies_elim (Thm.implies_elim major minor1) minor2))))
end;
(* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
@@ -641,7 +643,7 @@
val QP = read_prop "psi ==> phi";
in
store_standard_thm_open (Binding.name "equal_intr_rule")
- (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
+ (Thm.implies_intr PQ (Thm.implies_intr QP (Thm.equal_intr (Thm.assume PQ) (Thm.assume QP))))
end;
(* PROP ?phi == PROP ?psi ==> PROP ?phi ==> PROP ?psi *)
@@ -651,7 +653,7 @@
val P = read_prop "phi";
in
store_standard_thm_open (Binding.name "equal_elim_rule1")
- (Thm.equal_elim (assume eq) (assume P) |> implies_intr_list [eq, P])
+ (Thm.equal_elim (Thm.assume eq) (Thm.assume P) |> implies_intr_list [eq, P])
end;
(* PROP ?psi == PROP ?phi ==> PROP ?phi ==> PROP ?psi *)
@@ -917,7 +919,7 @@
fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x |> the_default x, T, ren t)
| ren (t $ u) = ren t $ ren u
| ren t = t;
- in equal_elim (reflexive (cert (ren (Thm.prop_of thm)))) thm end;
+ in Thm.equal_elim (Thm.reflexive (cert (ren (Thm.prop_of thm)))) thm end;
(* renaming in left-to-right order *)
@@ -937,7 +939,7 @@
in (xs'', t' $ u') end
| rename xs t = (xs, t);
in case rename xs prop of
- ([], prop') => equal_elim (reflexive (cert prop')) thm
+ ([], prop') => Thm.equal_elim (Thm.reflexive (cert prop')) thm
| _ => error "More names than abstractions in theorem"
end;
--- a/src/Pure/meta_simplifier.ML Sat May 15 21:09:54 2010 +0200
+++ b/src/Pure/meta_simplifier.ML Sat May 15 21:41:32 2010 +0200
@@ -832,9 +832,9 @@
fun check_conv msg ss thm thm' =
let
- val thm'' = transitive thm thm' handle THM _ =>
- transitive thm (transitive
- (symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
+ val thm'' = Thm.transitive thm thm' handle THM _ =>
+ Thm.transitive thm (Thm.transitive
+ (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
handle THM _ =>
let
@@ -972,8 +972,8 @@
| some => some)))
else proc_rews ps;
in case eta_t of
- Abs _ $ _ => SOME (transitive eta_thm
- (beta_conversion false eta_t'), skel0)
+ Abs _ $ _ => SOME (Thm.transitive eta_thm
+ (Thm.beta_conversion false eta_t'), skel0)
| _ => (case rews (sort_rrules (Net.match_term rules eta_t)) of
NONE => proc_rews (Net.match_term procs eta_t)
| some => some)
@@ -1006,7 +1006,7 @@
fun transitive1 NONE NONE = NONE
| transitive1 (SOME thm1) NONE = SOME thm1
| transitive1 NONE (SOME thm2) = SOME thm2
- | transitive1 (SOME thm1) (SOME thm2) = SOME (transitive thm1 thm2)
+ | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2)
fun transitive2 thm = transitive1 (SOME thm);
fun transitive3 thm = transitive1 thm o SOME;
@@ -1020,7 +1020,7 @@
some as SOME thm1 =>
(case rewritec (prover, thy, maxidx) ss (Thm.rhs_of thm1) of
SOME (thm2, skel2) =>
- transitive2 (transitive thm1 thm2)
+ transitive2 (Thm.transitive thm1 thm2)
(botc skel2 ss (Thm.rhs_of thm2))
| NONE => some)
| NONE =>
@@ -1031,7 +1031,7 @@
and try_botc ss t =
(case botc skel0 ss t of
- SOME trec1 => trec1 | NONE => (reflexive t))
+ SOME trec1 => trec1 | NONE => (Thm.reflexive t))
and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 =
(case term_of t0 of
@@ -1048,16 +1048,16 @@
val ss' = add_bound ((b', T), a) ss;
val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
in case botc skel' ss' t' of
- SOME thm => SOME (abstract_rule a v thm)
+ SOME thm => SOME (Thm.abstract_rule a v thm)
| NONE => NONE
end
| t $ _ => (case t of
Const ("==>", _) $ _ => impc t0 ss
| Abs _ =>
- let val thm = beta_conversion false t0
+ let val thm = Thm.beta_conversion false t0
in case subc skel0 ss (Thm.rhs_of thm) of
NONE => SOME thm
- | SOME thm' => SOME (transitive thm thm')
+ | SOME thm' => SOME (Thm.transitive thm thm')
end
| _ =>
let fun appc () =
@@ -1070,11 +1070,11 @@
(case botc tskel ss ct of
SOME thm1 =>
(case botc uskel ss cu of
- SOME thm2 => SOME (combination thm1 thm2)
- | NONE => SOME (combination thm1 (reflexive cu)))
+ SOME thm2 => SOME (Thm.combination thm1 thm2)
+ | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu)))
| NONE =>
(case botc uskel ss cu of
- SOME thm1 => SOME (combination (reflexive ct) thm1)
+ SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1)
| NONE => NONE))
end
val (h, ts) = strip_comb t
@@ -1095,7 +1095,7 @@
in case botc skel ss cl of
NONE => thm
| SOME thm' => transitive3 thm
- (combination thm' (reflexive cr))
+ (Thm.combination thm' (Thm.reflexive cr))
end handle Pattern.MATCH => appc ()))
| _ => appc ()
end)
@@ -1110,7 +1110,7 @@
(fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:")
ss prem; ([], NONE))
else
- let val asm = assume prem
+ let val asm = Thm.assume prem
in (extract_safe_rrules (ss, asm), SOME asm) end
and add_rrules (rrss, asms) ss =
@@ -1119,14 +1119,14 @@
and disch r prem eq =
let
val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
- val eq' = implies_elim (Thm.instantiate
+ val eq' = Thm.implies_elim (Thm.instantiate
([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
- (implies_intr prem eq)
+ (Thm.implies_intr prem eq)
in if not r then eq' else
let
val (prem', concl) = Thm.dest_implies lhs;
val (prem'', _) = Thm.dest_implies rhs
- in transitive (transitive
+ in Thm.transitive (Thm.transitive
(Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
Drule.swap_prems_eq) eq')
(Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)])
@@ -1182,7 +1182,7 @@
in mut_impc prems concl rrss asms (prem' :: prems')
(rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
(take i prems)
- (Drule.imp_cong_rule eqn (reflexive (Drule.list_implies
+ (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies
(drop i prems, concl))))) :: eqns)
ss (length prems') ~1
end
@@ -1197,13 +1197,13 @@
in (case botc skel0 ss1 conc of
NONE => (case thm1 of
NONE => NONE
- | SOME thm1' => SOME (Drule.imp_cong_rule thm1' (reflexive conc)))
+ | SOME thm1' => SOME (Drule.imp_cong_rule thm1' (Thm.reflexive conc)))
| SOME thm2 =>
let val thm2' = disch false prem1 thm2
in (case thm1 of
NONE => SOME thm2'
| SOME thm1' =>
- SOME (transitive (Drule.imp_cong_rule thm1' (reflexive conc)) thm2'))
+ SOME (Thm.transitive (Drule.imp_cong_rule thm1' (Thm.reflexive conc)) thm2'))
end)
end
@@ -1321,7 +1321,7 @@
val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
in map (AList.find (op =) keylist) keys end;
-val rev_defs = sort_lhs_depths o map symmetric;
+val rev_defs = sort_lhs_depths o map Thm.symmetric;
fun fold_rule defs = fold rewrite_rule (rev_defs defs);
fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
--- a/src/Pure/old_goals.ML Sat May 15 21:09:54 2010 +0200
+++ b/src/Pure/old_goals.ML Sat May 15 21:41:32 2010 +0200
@@ -134,7 +134,7 @@
val maxidx = Thm.maxidx_of state
val cterm = Thm.cterm_of (Thm.theory_of_thm state)
val chyps = map cterm hyps
- val hypths = map assume chyps
+ val hypths = map Thm.assume chyps
val subprems = map (Thm.forall_elim_vars 0) hypths
val fparams = map Free params
val cparams = map cterm fparams
@@ -165,7 +165,7 @@
val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
val emBs = map (cterm o embed) (prems_of st')
- val Cth = implies_elim_list st' (map (elim o assume) emBs)
+ val Cth = implies_elim_list st' (map (elim o Thm.assume) emBs)
in (*restore the unknowns to the hypotheses*)
free_instantiate (map swap_ctpair insts @
map mk_subgoal_swap_ctpair subgoal_insts)
@@ -175,7 +175,7 @@
end
(*function to replace the current subgoal*)
fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
- in Seq.maps next (tacf subprems (trivial (cterm concl))) end;
+ in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
end;
@@ -308,7 +308,7 @@
(*discharges assumptions from state in the order they appear in goal;
checks (if requested) that resulting theorem is equivalent to goal. *)
fun mkresult (check,state) =
- let val state = Seq.hd (flexflex_rule state)
+ let val state = Seq.hd (Thm.flexflex_rule state)
handle THM _ => state (*smash flexflex pairs*)
val ngoals = nprems_of state
val ath = implies_intr_list cAs state
@@ -522,7 +522,7 @@
| i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
in
Drule.export_without_context (implies_intr_list As
- (check (Seq.pull (EVERY (f asms) (trivial B)))))
+ (check (Seq.pull (EVERY (f asms) (Thm.trivial B)))))
end;
--- a/src/Pure/tactic.ML Sat May 15 21:09:54 2010 +0200
+++ b/src/Pure/tactic.ML Sat May 15 21:41:32 2010 +0200
@@ -156,7 +156,7 @@
fun dmatch_tac rls = ematch_tac (map make_elim rls);
(*Smash all flex-flex disagreement pairs in the proof state.*)
-val flexflex_tac = PRIMSEQ flexflex_rule;
+val flexflex_tac = PRIMSEQ Thm.flexflex_rule;
(*Remove duplicate subgoals.*)
val perm_tac = PRIMITIVE oo Thm.permute_prems;
@@ -185,7 +185,7 @@
(*Determine print names of goal parameters (reversed)*)
fun innermost_params i st =
- let val (_, _, Bi, _) = dest_state (st, i)
+ let val (_, _, Bi, _) = Thm.dest_state (st, i)
in Term.rename_wrt_term Bi (Logic.strip_params Bi) end;