# HG changeset patch # User wenzelm # Date 1273952492 -7200 # Node ID dbf831a50e4a02d761d8e6ee4fada49b50d7af37 # Parent ae740b96b9144067f36f4e2c4885245634a5d395 less pervasive names from structure Thm; diff -r ae740b96b914 -r dbf831a50e4a src/Pure/drule.ML --- 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; diff -r ae740b96b914 -r dbf831a50e4a src/Pure/meta_simplifier.ML --- 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)); diff -r ae740b96b914 -r dbf831a50e4a src/Pure/old_goals.ML --- 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; diff -r ae740b96b914 -r dbf831a50e4a src/Pure/tactic.ML --- 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;