# HG changeset patch # User wenzelm # Date 968172396 -7200 # Node ID e22db9397e171da200225edab097001a9412c99d # Parent bee6eb4b6a42659d76ac7d1e93795cb263fae06f iff declarations moved to clasimp.ML; diff -r bee6eb4b6a42 -r e22db9397e17 src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Tue Sep 05 18:45:51 2000 +0200 +++ b/src/FOL/simpdata.ML Tue Sep 05 18:46:36 2000 +0200 @@ -6,49 +6,6 @@ Simplification data for FOL *) -(*** Addition of rules to simpsets and clasets simultaneously ***) (* FIXME move to Provers/clasimp.ML? *) - -infix 4 addIffs delIffs; - -(*Takes UNCONDITIONAL theorems of the form A<->B to - the Safe Intr rule B==>A and - the Safe Destruct rule A==>B. - Also ~A goes to the Safe Elim rule A ==> ?R - Failing other cases, A is added as a Safe Intr rule*) -local - fun addIff ((cla, simp), th) = - (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of - (Const("Not", _) $ A) => - cla addSEs [zero_var_indexes (th RS notE)] - | (Const("op <->", _) $ _ $ _) => - cla addSIs [zero_var_indexes (th RS iffD2)] - addSDs [zero_var_indexes (th RS iffD1)] - | _ => cla addSIs [th], - simp addsimps [th]) - handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^ - string_of_thm th); - - fun delIff ((cla, simp), th) = - (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of - (Const ("Not", _) $ A) => - cla delrules [zero_var_indexes (th RS notE)] - | (Const("op <->", _) $ _ $ _) => - cla delrules [zero_var_indexes (th RS iffD2), - cla_make_elim (zero_var_indexes (th RS iffD1))] - | _ => cla delrules [th], - simp delsimps [th]) - handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ - string_of_thm th); (cla, simp)); - - fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp) -in -val op addIffs = foldl addIff; -val op delIffs = foldl delIff; -fun AddIffs thms = store_clasimp ((claset (), simpset ()) addIffs thms); -fun DelIffs thms = store_clasimp ((claset (), simpset ()) delIffs thms); -end; - - (* Elimination of True from asumptions: *) @@ -391,7 +348,11 @@ structure Clasimp = ClasimpFun (structure Simplifier = Simplifier and Splitter = Splitter - and Classical = Cla and Blast = Blast); + and Classical = Cla and Blast = Blast + val dest_Trueprop = FOLogic.dest_Trueprop + val iff_const = FOLogic.iff val not_const = FOLogic.not + val notE = notE val iffD1 = iffD1 val iffD2 = iffD2 + val cla_make_elim = cla_make_elim); open Clasimp; val FOL_css = (FOL_cs, FOL_ss); diff -r bee6eb4b6a42 -r e22db9397e17 src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Tue Sep 05 18:45:51 2000 +0200 +++ b/src/HOL/simpdata.ML Tue Sep 05 18:46:36 2000 +0200 @@ -8,56 +8,6 @@ section "Simplifier"; -(*** Addition of rules to simpsets and clasets simultaneously ***) (* FIXME move to Provers/clasimp.ML? *) - -infix 4 addIffs delIffs; - -(*Takes UNCONDITIONAL theorems of the form A<->B to - the Safe Intr rule B==>A and - the Safe Destruct rule A==>B. - Also ~A goes to the Safe Elim rule A ==> ?R - Failing other cases, A is added as a Safe Intr rule*) -local - val iff_const = HOLogic.eq_const HOLogic.boolT; - - fun addIff ((cla, simp), th) = - (case HOLogic.dest_Trueprop (#prop (rep_thm th)) of - (Const("Not", _) $ A) => - cla addSEs [zero_var_indexes (th RS notE)] - | (con $ _ $ _) => - if con = iff_const - then cla addSIs [zero_var_indexes (th RS iffD2)] - addSDs [zero_var_indexes (th RS iffD1)] - else cla addSIs [th] - | _ => cla addSIs [th], - simp addsimps [th]) - handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^ - string_of_thm th); - - fun delIff ((cla, simp), th) = - (case HOLogic.dest_Trueprop (#prop (rep_thm th)) of - (Const ("Not", _) $ A) => - cla delrules [zero_var_indexes (th RS notE)] - | (con $ _ $ _) => - if con = iff_const - then cla delrules - [zero_var_indexes (th RS iffD2), - cla_make_elim (zero_var_indexes (th RS iffD1))] - else cla delrules [th] - | _ => cla delrules [th], - simp delsimps [th]) - handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ - string_of_thm th); (cla, simp)); - - fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp) -in -val op addIffs = foldl addIff; -val op delIffs = foldl delIff; -fun AddIffs thms = store_clasimp ((claset (), simpset ()) addIffs thms); -fun DelIffs thms = store_clasimp ((claset (), simpset ()) delIffs thms); -end; - - val [prem] = goal (the_context ()) "x==y ==> x=y"; by (rewtac prem); by (rtac refl 1); @@ -306,8 +256,8 @@ (*** make simplification procedures for quantifier elimination ***) -structure Quantifier1 = Quantifier1Fun( -struct +structure Quantifier1 = Quantifier1Fun +(struct (*abstract syntax*) fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t) | dest_eq _ = None; @@ -507,7 +457,7 @@ in -val attrib_setup = +val rulify_attrib_setup = [Attrib.add_attributes [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]]; @@ -517,26 +467,17 @@ structure Clasimp = ClasimpFun (structure Simplifier = Simplifier and Splitter = Splitter - and Classical = Classical and Blast = Blast); + and Classical = Classical and Blast = Blast + val dest_Trueprop = HOLogic.dest_Trueprop + val iff_const = HOLogic.eq_const HOLogic.boolT + val not_const = HOLogic.not_const + val notE = notE val iffD1 = iffD1 val iffD2 = iffD2 + val cla_make_elim = cla_make_elim); open Clasimp; val HOL_css = (HOL_cs, HOL_ss); -(* "iff" attribute *) - -val iff_add_global = Clasimp.change_global_css (op addIffs); -val iff_del_global = Clasimp.change_global_css (op delIffs); -val iff_add_local = Clasimp.change_local_css (op addIffs); -val iff_del_local = Clasimp.change_local_css (op delIffs); - -val iff_attrib_setup = - [Attrib.add_attributes - [("iff", (Attrib.add_del_args iff_add_global iff_del_global, - Attrib.add_del_args iff_add_local iff_del_local), - "declare simplifier / classical rules")]]; - - (*** A general refutation procedure ***)