# HG changeset patch # User oheimb # Date 906650313 -7200 # Node ID 4b93862240841f721cfd641a0c29017ae19814b5 # Parent 3cae5d6510c2c07b2d095837a1aed1fb2de7ab81 simplified CLASIMP_DATA renamed mk_meta_eq to mk_eq introduced new mk_meta_eq, simplified addcongs and delcongs, introducing mk_meta_cong diff -r 3cae5d6510c2 -r 4b9386224084 src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Thu Sep 24 17:17:56 1998 +0200 +++ b/src/FOL/simpdata.ML Thu Sep 24 17:18:33 1998 +0200 @@ -76,21 +76,31 @@ val iff_reflection_T = P_iff_T RS iff_reflection; (*Make meta-equalities. The operator below is Trueprop*) + fun mk_meta_eq th = case concl_of th of + _ $ (Const("op =",_)$_$_) => th RS eq_reflection + | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection + | _ => + error("conclusion must be a =-equality or <->");; + +fun mk_eq th = case concl_of th of Const("==",_)$_$_ => th - | _ $ (Const("op =",_)$_$_) => th RS eq_reflection - | _ $ (Const("op <->",_)$_$_) => th RS iff_reflection + | _ $ (Const("op =",_)$_$_) => mk_meta_eq th + | _ $ (Const("op <->",_)$_$_) => mk_meta_eq th | _ $ (Const("Not",_)$_) => th RS iff_reflection_F | _ => th RS iff_reflection_T; +fun mk_meta_cong rl = standard (mk_meta_eq rl); +(*FIXME: how about the premises?*) + val mksimps_pairs = [("op -->", [mp]), ("op &", [conjunct1,conjunct2]), ("All", [spec]), ("True", []), ("False", [])]; -(* FIXME: move to Provers/simplifier.ML +(* ###FIXME: move to Provers/simplifier.ML val mk_atomize: (string * thm list) list -> thm -> thm list *) -(* FIXME: move to Provers/simplifier.ML*) +(* ###FIXME: move to Provers/simplifier.ML *) fun mk_atomize pairs = let fun atoms th = (case concl_of th of @@ -104,7 +114,7 @@ | _ => [th]) in atoms end; -fun mksimps pairs = (map mk_meta_eq o mk_atomize pairs o gen_all); +fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all); (*** Classical laws ***) @@ -252,7 +262,7 @@ structure SplitterData = struct structure Simplifier = Simplifier - val mk_meta_eq = mk_meta_eq + val mk_eq = mk_eq val meta_eq_to_iff = meta_eq_to_iff val iffD = iffD2 val disjE = disjE @@ -280,13 +290,14 @@ open Induction; -(*Add congruence rules for = or <-> (instead of ==) *) + +(* Add congruence rules for = or <-> (instead of ==) *) + +(* ###FIXME: Move to simplifier, + taking mk_meta_cong as input, eliminating addeqcongs and deleqcongs *) infix 4 addcongs delcongs; -fun ss addcongs congs = - ss addeqcongs (map standard (congs RL [eq_reflection,iff_reflection])); -fun ss delcongs congs = - ss deleqcongs (map standard (congs RL [eq_reflection,iff_reflection])); - +fun ss addcongs congs = ss addeqcongs (map mk_meta_cong congs); +fun ss delcongs congs = ss deleqcongs (map mk_meta_cong congs); fun Addcongs congs = (simpset_ref() := simpset() addcongs congs); fun Delcongs congs = (simpset_ref() := simpset() delcongs congs); @@ -342,10 +353,9 @@ (*** integration of simplifier with classical reasoner ***) structure Clasimp = ClasimpFun - (structure Simplifier = Simplifier and Classical = Cla and Blast = Blast - val op addcongs = op addcongs and op delcongs = op delcongs - and op addSaltern = op addSaltern and op addbefore = op addbefore); - + (structure Simplifier = Simplifier + and Classical = Cla + and Blast = Blast); open Clasimp; val FOL_css = (FOL_cs, FOL_ss);