# HG changeset patch # User berghofe # Date 999266876 -7200 # Node ID da3a96ab563011d1c10eb488e51655299fecec34 # Parent ec89f5cff390573414d5adee4ecd5db6dc39f258 Some basic rules are now stored with "open" derivations, to facilitate simplification of proof terms. diff -r ec89f5cff390 -r da3a96ab5630 src/Pure/drule.ML --- a/src/Pure/drule.ML Fri Aug 31 16:06:21 2001 +0200 +++ b/src/Pure/drule.ML Fri Aug 31 16:07:56 2001 +0200 @@ -39,6 +39,7 @@ (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm val zero_var_indexes : thm -> thm val standard : thm -> thm + val standard' : thm -> thm val rotate_prems : int -> thm -> thm val rearrange_prems : int list -> thm -> thm val assume_ax : theory -> string -> thm @@ -62,6 +63,7 @@ val transitive_thm : thm val refl_implies : thm val symmetric_fun : thm -> thm + val extensional : thm -> thm val imp_cong : thm val swap_prems_eq : thm val equal_abs_elim : cterm -> thm -> thm @@ -88,7 +90,6 @@ val tag : tag -> 'a attribute val untag : string -> 'a attribute val tag_lemma : 'a attribute - val tag_assumption : 'a attribute val tag_internal : 'a attribute val has_internal : tag list -> bool val close_derivation : thm -> thm @@ -249,7 +250,6 @@ fun simple_tag name x = tag (name, []) x; fun tag_lemma x = simple_tag "lemma" x; -fun tag_assumption x = simple_tag "assumption" x; val internal_tag = ("internal", []); fun tag_internal x = tag internal_tag x; @@ -329,15 +329,17 @@ if Thm.get_name_tags thm = ("", []) then Thm.name_thm ("", thm) else thm; -fun standard th = +fun standard' th = let val {maxidx,...} = rep_thm th in th |> implies_intr_hyps |> forall_intr_frees |> forall_elim_vars (maxidx + 1) |> strip_shyps_warning - |> zero_var_indexes |> Thm.varifyT |> Thm.compress |> close_derivation + |> zero_var_indexes |> Thm.varifyT |> Thm.compress end; +val standard = close_derivation o standard'; + (*Convert all Vars in a theorem to Frees. Also return a function for reversing that operation. DOES NOT WORK FOR TYPE VARIABLES. @@ -480,6 +482,8 @@ fun store_thm name thm = hd (PureThy.smart_store_thms (name, [thm])); fun store_standard_thm name thm = store_thm name (standard thm); +fun open_store_thm name thm = hd (PureThy.open_smart_store_thms (name, [thm])); +fun open_store_standard_thm name thm = open_store_thm name (standard' thm); val reflexive_thm = let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),logicS))) @@ -497,6 +501,11 @@ fun symmetric_fun thm = thm RS symmetric_thm; +fun extensional eq = + let val eq' = + abstract_rule "x" (snd (Thm.dest_comb (fst (dest_equals (cprop_of eq))))) eq + in equal_elim (eta_conversion (cprop_of eq')) eq' end; + val imp_cong = let val ABC = read_prop "PROP A ==> PROP B == PROP C" @@ -504,7 +513,7 @@ val AC = read_prop "PROP A ==> PROP C" val A = read_prop "PROP A" in - store_standard_thm "imp_cong" (implies_intr ABC (equal_intr + open_store_standard_thm "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))))) @@ -520,7 +529,7 @@ val A = read_prop "PROP A" val B = read_prop "PROP B" in - store_standard_thm "swap_prems_eq" (equal_intr + open_store_standard_thm "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 @@ -533,12 +542,12 @@ (*** Some useful meta-theorems ***) (*The rule V/V, obtains assumption solving for eresolve_tac*) -val asm_rl = store_standard_thm "asm_rl" (Thm.trivial (read_prop "PROP ?psi")); +val asm_rl = open_store_standard_thm "asm_rl" (Thm.trivial (read_prop "PROP ?psi")); val _ = store_thm "_" asm_rl; (*Meta-level cut rule: [| V==>W; V |] ==> W *) val cut_rl = - store_standard_thm "cut_rl" + open_store_standard_thm "cut_rl" (Thm.trivial (read_prop "PROP ?psi ==> PROP ?theta")); (*Generalized elim rule for one conclusion; cut_rl with reversed premises: @@ -547,7 +556,7 @@ let val V = read_prop "PROP V" and VW = read_prop "PROP V ==> PROP W"; in - store_standard_thm "revcut_rl" + open_store_standard_thm "revcut_rl" (implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V)))) end; @@ -555,7 +564,7 @@ val thin_rl = let val V = read_prop "PROP V" and W = read_prop "PROP W"; - in store_standard_thm "thin_rl" (implies_intr V (implies_intr W (assume W))) + in open_store_standard_thm "thin_rl" (implies_intr V (implies_intr W (assume W))) end; (* (!!x. PROP ?V) == PROP ?V Allows removal of redundant parameters*) @@ -564,9 +573,9 @@ and QV = read_prop "!!x::'a. PROP V" and x = read_cterm proto_sign ("x", TypeInfer.logicT); in - store_standard_thm "triv_forall_equality" - (standard (equal_intr (implies_intr QV (forall_elim x (assume QV))) - (implies_intr V (forall_intr x (assume V))))) + open_store_standard_thm "triv_forall_equality" + (equal_intr (implies_intr QV (forall_elim x (assume QV))) + (implies_intr V (forall_intr x (assume V)))) end; (* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> @@ -580,7 +589,7 @@ val minor1 = assume cminor1; val cminor2 = read_prop "PROP PhiB"; val minor2 = assume cminor2; - in store_standard_thm "swap_prems_rl" + in open_store_standard_thm "swap_prems_rl" (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1 (implies_elim (implies_elim major minor1) minor2)))) end; @@ -593,7 +602,7 @@ let val PQ = read_prop "PROP phi ==> PROP psi" and QP = read_prop "PROP psi ==> PROP phi" in - store_standard_thm "equal_intr_rule" + open_store_standard_thm "equal_intr_rule" (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP)))) end;