# HG changeset patch # User nipkow # Date 778233889 -7200 # Node ID 0bba840aa07c9e385194ea0664710fe43ccf3f70 # Parent 89669c58e506ccf820b8faedd8192e9ca4b2453b New version of datatype.ML with primrec (Norbert). Updated treatment of bounded quantifiers in the simplifier. diff -r 89669c58e506 -r 0bba840aa07c Fun.ML --- a/Fun.ML Thu Aug 25 11:01:45 1994 +0200 +++ b/Fun.ML Tue Aug 30 10:04:49 1994 +0200 @@ -188,4 +188,9 @@ "(a : {b}) = (a=b)", "(a : {x.P(x)}) = P(a)" ]; -val set_ss = HOL_ss addsimps mem_simps; +val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs; + +val set_ss = + HOL_ss addsimps mem_simps + addcongs [ball_cong,bex_cong] + setmksimps (mksimps mksimps_pairs); diff -r 89669c58e506 -r 0bba840aa07c Makefile --- a/Makefile Thu Aug 25 11:01:45 1994 +0200 +++ b/Makefile Tue Aug 30 10:04:49 1994 +0200 @@ -24,7 +24,7 @@ Prod.thy Prod.ML Sum.thy Sum.ML WF.thy WF.ML \ mono.thy mono.ML Lfp.thy Lfp.ML Gfp.thy Gfp.ML Nat.thy Nat.ML \ add_ind_def.ML ind_syntax.ML indrule.ML Inductive.ML \ - intr_elim.ML Datatype.ML ../Pure/section_utils.ML\ + intr_elim.ML datatype.ML ../Pure/section_utils.ML\ Finite.ML Finite.thy\ Arith.thy Arith.ML Sexp.thy Sexp.ML Univ.thy Univ.ML \ LList.thy LList.ML List.thy List.ML \ @@ -34,7 +34,7 @@ EX_FILES = ex/ROOT.ML ex/cla.ML \ ex/LexProd.ML ex/LexProd.thy ex/meson.ML ex/mesontest.ML\ ex/MT.ML ex/MT.thy ex/Acc.ML ex/Acc.thy \ - ex/PL.ML ex/PL.thy ex/Puzzle.ML ex/Puzzle.thy\ + ex/PropLog.ML ex/PropLog.thy ex/Puzzle.ML ex/Puzzle.thy\ ex/Qsort.thy ex/Qsort.ML\ ex/Rec.ML ex/Rec.thy ex/rel.ML ex/set.ML ex/Simult.ML ex/Simult.thy\ ex/Term.ML ex/Term.thy diff -r 89669c58e506 -r 0bba840aa07c ROOT.ML --- a/ROOT.ML Thu Aug 25 11:01:45 1994 +0200 +++ b/ROOT.ML Tue Aug 30 10:04:49 1994 +0200 @@ -79,8 +79,8 @@ use_thy "Nat"; (* Add user sections *) -use "Datatype.ML"; use "../Pure/section_utils.ML"; +use "datatype.ML"; use "ind_syntax.ML"; use "add_ind_def.ML"; use "intr_elim.ML"; diff -r 89669c58e506 -r 0bba840aa07c datatype.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/datatype.ML Tue Aug 30 10:04:49 1994 +0200 @@ -0,0 +1,556 @@ +(* Title: HOL/Datatype + ID: $Id$ + Author: Max Breitling, Carsten Clasohm, + Tobias Nipkow, Norbert Voelker + Copyright 1994 TU Muenchen +*) + + +(*choice between Ci_neg1 and Ci_neg2 axioms depends on number of constructors*) +local + + val dtK = 5 + +in + +local open ThyParse in + val datatype_decls = + let + val tvar = type_var >> (fn s => "dtVar" ^ s); + + val type_var_list = + tvar >> (fn s => [s]) || "(" $$-- list1 tvar --$$ ")"; + + val typ = + ident >> (fn s => "dtTyp([]," ^ quote s ^")") + || + type_var_list -- ident >> (fn (ts, id) => "dtTyp(" ^ mk_list ts ^ + "," ^ quote id ^ ")") + || + tvar; + + val typ_list = "(" $$-- list1 typ --$$ ")" || empty; + + val cons = name -- typ_list -- opt_mixfix; + + fun constructs ts = + ( cons --$$ "|" -- constructs >> op:: + || + cons >> (fn c => [c])) ts; + + fun mk_cons cs = + case findrep (map (fst o fst) cs) of + [] => map (fn ((s,ts),syn) => parens(commas [s,mk_list ts,syn])) cs + | c::_ => error("Constructor \"" ^ c ^ "\" occurs twice"); + + (*remove all quotes from a string*) + val rem_quotes = implode o filter (fn c => c <> "\"") o explode; + + (*generate names of distinct axioms*) + fun rules_distinct cs tname = + let val uqcs = map (fn ((s,_),_) => rem_quotes s) cs; + (*combine all constructor names with all others w/o duplicates*) + fun negOne c = map (fn c2 => quote (c ^ "_not_" ^ c2)); + fun neg1 [] = [] + | neg1 (c1 :: cs) = (negOne c1 cs) @ (neg1 cs) + in if length uqcs < dtK then neg1 uqcs + else quote (tname ^ "_ord_distinct") :: + map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs + end; + + fun rules tname cons pre = + " map (get_axiom thy) " ^ + mk_list (map (fn ((s,_),_) => quote(tname ^ pre ^ rem_quotes s)) + cons) + + (*generate string for calling 'add_datatype'*) + fun mk_params ((ts, tname), cons) = + ("val (thy," ^ tname ^ "_add_primrec) = add_datatype\n" ^ + parens (commas [mk_list ts, quote tname, mk_list (mk_cons cons)]) ^ + " thy\n\ + \val thy=thy", + "structure " ^ tname ^ " =\n\ + \struct\n\ + \ val inject = map (get_axiom thy) " ^ + mk_list (map (fn ((s,_), _) => quote ("inject_" ^ rem_quotes s)) + (filter_out (null o snd o fst) cons)) ^ ";\n\ + \ val distinct = " ^ + (if length cons < dtK then "let val distinct' = " else "") ^ + "map (get_axiom thy) " ^ mk_list (rules_distinct cons tname) ^ + (if length cons < dtK then + " in distinct' @ (map (fn t => sym COMP (t RS contrapos))\ + \ distinct') end" + else "") ^ ";\n\ + \ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\ + \ val cases =" ^ rules tname cons "_case_" ^ ";\n\ + \ val recs =" ^ rules tname cons "_rec_" ^ ";\n\ + \ val simps = inject @ distinct @ cases @ recs;\n\ + \ fun induct_tac a =\ + \res_inst_tac[(" ^ quote tname ^ ", a)]induct;\n\ + \end;\n") + in + (type_var_list || empty) -- ident --$$ "=" -- constructs >> mk_params +end + +val primrec_decl = + let fun mkstrings((fname,tname),axms) = + let fun prove (name,eqn) = + "val "^name^"= prove_goalw thy [get_def thy \""^fname^"\"] " + ^ eqn ^"\n\ + \(fn _ => [simp_tac (HOL_ss addsimps " ^ tname^".recs) 1])" + in ("|> " ^ tname^"_add_primrec " ^ mk_list (map snd axms) + , cat_lines(map prove axms)) + end + in ident -- long_id -- repeat1 (ident -- string) >> mkstrings end +end; + +(*used for constructor parameters*) +datatype dt_type = dtVar of string | + dtTyp of dt_type list * string | + dtRek of dt_type list * string; + +local + +val mysort = sort; +open ThyParse +exception Impossible; +exception RecError of string; + +val is_dtRek = (fn dtRek _ => true | _ => false); +fun opt_parens s = if s = "" then "" else enclose "(" ")" s; + +(* ----------------------------------------------------------------------- *) +(* Derivation of the primrec combinator application from the equations *) + +(* subst. applications fname(ls,xk,rs) by yk(ls,rs) for xk in rargs *) + +fun subst_apps (_,_) [] t = t + | subst_apps (fname,cpos) pairs t = + let + fun subst (Abs(a,T,t)) = Abs(a,T,subst t) + | subst (funct $ body) = + let val (f,b) = strip_comb (funct$body) + in + if is_Const f andalso fst(dest_Const f) = fname + then + let val (ls,rest) = (take(cpos,b), drop (cpos,b)); + val (xk,rs) = (hd rest,tl rest) + handle LIST _ => raise RecError "not enough arguments \ + \ in recursive application on rhs" + in + (case assoc (pairs,xk) of + None => raise RecError + ("illegal occurence of " ^ fname ^ " on rhs") + | Some(U) => list_comb(U,ls @ rs)) + end + else list_comb(f, map subst b) + end + | subst(t) = t + in subst t end; + +(* abstract rhs *) + +fun abst_rec (fname,cpos,tc,ls,cargs,rs,rhs) = + let val rargs = (map fst o + (filter (fn (a,T) => is_dtRek T))) (cargs ~~ tc); + val subs = map (fn (s,T) => (s,dummyT)) + (rev(rename_wrt_term rhs rargs)); + val subst_rhs = subst_apps (fname,cpos) + (map Free rargs ~~ map Free subs) rhs; + val res = list_abs_free (cargs @ subs @ ls @ rs, subst_rhs); + in + if fname mem add_term_names (res,[]) + then raise RecError ("illegal occurence of " ^ fname ^ " on rhs") + else res + end; + +(* parsing the prim rec equations *) + +fun dest_eq ( Const("Trueprop",_) $ (Const ("op =",_) $ lhs $ rhs)) + = (lhs, rhs) + | dest_eq _ = raise RecError "not a proper equation"; + +fun dest_rec eq = + let val (lhs,rhs) = dest_eq eq; + val (name,args) = strip_comb lhs; + val (ls',rest) = take_prefix is_Free args; + val (middle,rs') = take_suffix is_Free rest; + val cpos = length ls'; + val (c,cargs') = strip_comb (hd middle) + handle LIST "hd" => raise RecError "constructor missing"; + val (ls,cargs,rs) = (map dest_Free ls', map dest_Free cargs' + , map dest_Free rs') + handle TERM ("dest_Free",_) => + raise RecError "constructor has illegal argument in pattern"; + in + if length middle > 1 then + raise RecError "more than one non-variable in pattern" + else if not(null(findrep (map fst (ls @ rs @ cargs)))) then + raise RecError "repeated variable name in pattern" + else (fst(dest_Const name) handle TERM _ => + raise RecError "function is not declared as constant in theory" + ,cpos,ls,fst( dest_Const c),cargs,rs,rhs) + end; + +(* check function specified for all constructors and sort function terms *) + +fun check_and_sort (n,its) = + if length its = n + then map snd (mysort (fn ((i : int,_),(j,_)) => i + error("Primrec definition error: " ^ s ^ ":\n" + ^ " " ^ Sign.string_of_term (sign_of thy) eq1); + val tcs = map (fn (_,c,T,_) => (c,T)) cs'; + val cs = map fst tcs; + fun trans_recs' _ [] = [] + | trans_recs' cis (eq::eqs) = + let val (name,cpos,ls,c,cargs,rs,rhs) = dest_rec eq; + val tc = assoc(tcs,c); + val i = (1 + find (c,cs)) handle LIST "find" => 0; + in + if name <> name1 then + raise RecError "function names inconsistent" + else if cpos <> cpos1 then + raise RecError "position of rec. argument inconsistent" + else if i = 0 then + raise RecError "illegal argument in pattern" + else if i mem cis then + raise RecError "constructor already occured as pattern " + else (i,abst_rec (name,cpos,the tc,ls,cargs,rs,rhs)) + :: trans_recs' (i::cis) eqs + end + handle RecError s => + error("Primrec definition error\n" ^ s ^ "\n" + ^ " " ^ Sign.string_of_term (sign_of thy) eq); + in ( name1, ls1 + , check_and_sort (length cs, trans_recs' [] (eq1::eqs))) + end ; + + +fun instantiate_types thy t = + let val sg = sign_of thy + val rsg = Sign.rep_sg sg + in fst(Type.infer_types(#tsig rsg, lookup_const sg, K None, K None, + TVar(("",0),[]), t)) + end; + +in + fun add_datatype (typevars, tname, cons_list') thy = + let (*search for free type variables and convert recursive *) + fun analyse_types (cons, typlist, syn) = + let fun analyse(t as dtVar v) = + if t mem typevars then t + else error ("Free type variable " ^ v ^ " on rhs.") + | analyse(dtTyp(typl,s)) = + if tname <> s then dtTyp(analyses typl, s) + else if typevars = typl then dtRek(typl, s) + else error (s ^ " used in different ways") + | analyse(dtRek _) = raise Impossible + and analyses ts = map analyse ts; + in (cons, Syntax.const_name cons syn, analyses typlist, syn) + end; + + (*test if all elements are recursive, i.e. if the type is empty*) + + fun non_empty (cs : ('a * 'b * dt_type list * 'c) list) = + not(forall (exists is_dtRek o #3) cs) orelse + error("Empty datatype not allowed!"); + + val cons_list = map analyse_types cons_list'; + val dummy = non_empty cons_list; + val num_of_cons = length cons_list; + + (* Auxiliary functions to construct argument and equation lists *) + + (*generate 'var_n, ..., var_m'*) + fun Args(var, delim, n, m) = + space_implode delim (map (fn n => var^string_of_int(n)) (n upto m)); + + (*generate 'name_1', ..., 'name_n'*) + fun C_exp(name, n, var) = + if n > 0 then name ^ parens(Args(var, ",", 1, n)) else name; + + (*generate 'x_n = y_n, ..., x_m = y_m'*) + fun Arg_eql(n,m) = + if n=m then "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) + else "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) ^ " & " ^ + Arg_eql(n+1, m); + + (*Pretty printers for type lists; + pp_typlist1: parentheses, pp_typlist2: brackets*) + fun pp_typ (dtVar s) = s + | pp_typ (dtTyp (typvars, id)) = + if null typvars then id else (pp_typlist1 typvars) ^ id + | pp_typ (dtRek (typvars, id)) = (pp_typlist1 typvars) ^ id + and + pp_typlist' ts = commas (map pp_typ ts) + and + pp_typlist1 ts = if null ts then "" else parens (pp_typlist' ts); + + fun pp_typlist2 ts = if null ts then "" else brackets (pp_typlist' ts); + + (* Generate syntax translation for case rules *) + fun calc_xrules c_nr y_nr ((_, name, typlist, _) :: cs) = + let val arity = length typlist; + val body = "z" ^ string_of_int(c_nr); + val args1 = if arity=0 then "" + else parens (Args ("y", ",", y_nr, y_nr+arity-1)); + val args2 = if arity=0 then "" + else "% " ^ Args ("y", " ", y_nr, y_nr+arity-1) + ^ ". "; + val (rest1,rest2) = + if null cs then ("","") + else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs + in (" | " ^ h1, ", " ^ h2) end; + in (name ^ args1 ^ " => " ^ body ^ rest1, args2 ^ body ^ rest2) end + | calc_xrules _ _ [] = raise Impossible; + + val xrules = + let val (first_part, scnd_part) = calc_xrules 1 1 cons_list + in [("logic", "case x of " ^ first_part) <-> + ("logic", tname ^ "_case(" ^ scnd_part ^ ", x)" )] + end; + + (*type declarations for constructors*) + fun const_type (id, _, typlist, syn) = + (id, + (if null typlist then "" else pp_typlist2 typlist ^ " => ") ^ + pp_typlist1 typevars ^ tname, syn); + + + fun assumpt (dtRek _ :: ts, v :: vs ,found) = + let val h = if found then ";P(" ^ v ^ ")" else "[| P(" ^ v ^ ")" + in h ^ (assumpt (ts, vs, true)) end + | assumpt (t :: ts, v :: vs, found) = assumpt (ts, vs, found) + | assumpt ([], [], found) = if found then "|] ==>" else "" + | assumpt _ = raise Impossible; + + (*insert type with suggested name 'varname' into table*) + fun insert typ varname ((tri as (t, s, n)) :: xs) = + if typ = t then (t, s, n+1) :: xs + else tri :: (if varname = s then insert typ (varname ^ "'") xs + else insert typ varname xs) + | insert typ varname [] = [(typ, varname, 1)]; + + fun typid(dtRek(_,id)) = id + | typid(dtVar s) = implode (tl (explode s)) + | typid(dtTyp(_,id)) = id; + + val insert_types = foldl (fn (tab,typ) => insert typ (typid typ) tab); + + fun update(dtRek _, s, v :: vs, (dtRek _) :: ts) = s :: vs + | update(t, s, v :: vs, t1 :: ts) = + if t=t1 then s :: vs else v :: (update (t, s, vs, ts)) + | update _ = raise Impossible; + + fun update_n (dtRek r1, s, v :: vs, (dtRek r2) :: ts, n) = + if r1 = r2 then (s ^ string_of_int n) :: + (update_n (dtRek r1, s, vs, ts, n+1)) + else v :: (update_n (dtRek r1, s, vs, ts, n)) + | update_n (t, s, v :: vs, t1 :: ts, n) = + if t = t1 then (s ^ string_of_int n) :: + (update_n (t, s, vs, ts, n+1)) + else v :: (update_n (t, s, vs, ts, n)) + | update_n (_,_,[],[],_) = [] + | update_n _ = raise Impossible; + + (*insert type variables into table*) + fun convert typs = + let fun conv(vars, (t, s, n)) = + if n=1 then update (t, s, vars, typs) + else update_n (t, s, vars, typs, 1) + in foldl conv + end; + + fun empty_list n = replicate n ""; + + fun t_inducting ((_, name, typl, _) :: cs) = + let val tab = insert_types([],typl); + val arity = length typl; + val var_list = convert typl (empty_list arity,tab); + val h = if arity = 0 then " P(" ^ name ^ ")" + else " !!" ^ (space_implode " " var_list) ^ "." ^ + (assumpt (typl, var_list, false)) ^ "P(" ^ + name ^ "(" ^ (commas var_list) ^ "))"; + val rest = t_inducting cs; + in if rest = "" then h else h ^ "; " ^ rest end + | t_inducting [] = ""; + + fun t_induct cl typ_name = + "[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")"; + + fun gen_typlist typevar f ((_, _, ts, _) :: cs) = + let val h = if (length ts) > 0 + then pp_typlist2(f ts) ^ "=>" + else "" + in h ^ typevar ^ "," ^ (gen_typlist typevar f cs) end + | gen_typlist _ _ [] = ""; + + +(* -------------------------------------------------------------------- *) +(* The case constant and rules *) + + val t_case = tname ^ "_case"; + + fun case_rule n (id, name, ts, _) = + let val args = opt_parens(Args("x", ",", 1, length ts)) + in (t_case ^ "_" ^ id, + t_case ^ "(" ^ Args("f", ",", 1, num_of_cons) + ^ "," ^ name ^ args + ^ ") = f" ^ string_of_int(n) ^ args) + end + + fun case_rules n (c :: cs) = case_rule n c :: case_rules(n+1) cs + | case_rules _ [] = []; + + val datatype_arity = length typevars; + + val types = [(tname, datatype_arity, NoSyn)]; + + val arities = + let val term_list = replicate datatype_arity ["term"]; + in [(tname, term_list, ["term"])] + end; + + val datatype_name = pp_typlist1 typevars ^ tname; + + val new_tvar_name = variant (map (fn dtVar s => s) typevars) "'z"; + + val case_const = + (t_case, + "[" ^ gen_typlist new_tvar_name I cons_list + ^ pp_typlist1 typevars ^ tname ^ "] =>" ^ new_tvar_name, + NoSyn); + + val rules_case = case_rules 1 cons_list; + +(* -------------------------------------------------------------------- *) +(* The prim-rec combinator *) + + val t_rec = tname ^ "_rec" + +(* adding type variables for dtRek types to end of list of dt_types *) + + fun add_reks ts = + ts @ map (fn _ => dtVar new_tvar_name) (filter is_dtRek ts); + +(* positions of the dtRek types in a list of dt_types, starting from 1 *) + + fun rek_pos ts = + map snd (filter (is_dtRek o fst) (ts ~~ (1 upto length ts))) + + fun rec_rule n (id,name,ts,_) = + let val args = Args("x",",",1,length ts) + val fargs = Args("f",",",1,num_of_cons) + fun rarg i = "," ^ t_rec ^ parens(fargs ^ "," ^ "x" ^ + string_of_int(i)) + val rargs = implode (map rarg (rek_pos ts)) + in + ( t_rec ^ "_" ^ id + , t_rec ^ parens(fargs ^ "," ^ name ^ (opt_parens args)) ^ " = f" + ^ string_of_int(n) ^ opt_parens (args ^ rargs)) + end + + fun rec_rules n (c::cs) = rec_rule n c :: rec_rules (n+1) cs + | rec_rules _ [] = []; + + val rec_const = + (t_rec, + "[" ^ (gen_typlist new_tvar_name add_reks cons_list) + ^ (pp_typlist1 typevars) ^ tname ^ "] =>" ^ new_tvar_name, + NoSyn); + + val rules_rec = rec_rules 1 cons_list + +(* -------------------------------------------------------------------- *) + val consts = + map const_type cons_list + @ (if num_of_cons < dtK then [] + else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)]) + @ [case_const,rec_const]; + + + fun Ci_ing ((id, name, typlist, _) :: cs) = + let val arity = length typlist; + in if arity = 0 then Ci_ing cs + else ("inject_" ^ id, + "(" ^ C_exp(name,arity,"x") ^ "=" ^ C_exp(name,arity,"y") + ^ ") = (" ^ Arg_eql (1, arity) ^ ")") :: (Ci_ing cs) + end + | Ci_ing [] = []; + + fun Ci_negOne (id1, name1, tl1, _) (id2, name2, tl2, _) = + let val ax = C_exp(name1, length tl1, "x") ^ "~=" ^ + C_exp(name2, length tl2, "y") + in (id1 ^ "_not_" ^ id2, ax) + end; + + fun Ci_neg1 [] = [] + | Ci_neg1 (c1::cs) = (map (Ci_negOne c1) cs) @ Ci_neg1 cs; + + fun suc_expr n = + if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")"; + + fun Ci_neg2() = + let val ord_t = tname ^ "_ord"; + val cis = cons_list ~~ (0 upto (num_of_cons - 1)) + fun Ci_neg2equals ((id, name, typlist, _), n) = + let val ax = ord_t ^ "(" ^ (C_exp(name, length typlist, "x")) + ^ ") = " ^ (suc_expr n) + in (ord_t ^ "_" ^ id, ax) end + in (ord_t ^ "_distinct", ord_t^"(x) ~= "^ord_t^"(y) ==> x ~= y") :: + (map Ci_neg2equals cis) + end; + + val rules_distinct = if num_of_cons < dtK then Ci_neg1 cons_list + else Ci_neg2(); + + val rules_inject = Ci_ing cons_list; + + val rule_induct = (tname ^ "_induct", t_induct cons_list tname); + + val rules = rule_induct :: + (rules_inject @ rules_distinct @ rules_case @ rules_rec); + + fun add_primrec eqns thy = + let val rec_comb = Const(t_rec,dummyT) + val teqns = map (fn eq => snd(read_axm (sign_of thy) + ("",eq))) eqns + val (fname,ls,fns) = trans_recs thy cons_list teqns + val rhs = + list_abs_free + (ls @ [(tname,dummyT)] + ,list_comb(rec_comb + , fns @ map Bound (0 ::(length ls downto 1)))); + val sg = sign_of thy; + val (defname,def) = mk_defpair (Const(fname,dummyT),rhs) + val tdef as ( _ $ Const(_,T) $ _ ) = instantiate_types thy def; + val varT = Type.varifyT T; + val Some(ftyp) = lookup_const sg fname; + in + if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT) + then add_defs_i [(defname,tdef)] thy + else error("Primrec definition error: \ntype of " ^ fname + ^ " is not instance of type deduced from equations") + end; + + in + (thy + |> add_types types + |> add_arities arities + |> add_consts consts + |> add_trrules xrules + |> add_axioms rules,add_primrec) + end +end +end; + diff -r 89669c58e506 -r 0bba840aa07c simpdata.ML --- a/simpdata.ML Thu Aug 25 11:01:45 1994 +0200 +++ b/simpdata.ML Tue Aug 30 10:04:49 1994 +0200 @@ -18,20 +18,20 @@ val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp; val not_P_imp_P_eq_False = not_P_imp_P_iff_F RS eq_reflection; -fun atomize r = - case concl_of r of - Const("Trueprop",_) $ p => - (case p of - Const("op -->",_)$_$_ => atomize(r RS mp) - | Const("op &",_)$_$_ => atomize(r RS conjunct1) @ - atomize(r RS conjunct2) - | Const("All",_)$_ => atomize(r RS spec) - | Const("True",_) => [] - | Const("False",_) => [] - | _ => [r]) - | _ => [r]; +fun atomize pairs = + let fun atoms th = + (case concl_of th of + Const("Trueprop",_) $ p => + (case head_of p of + Const(a,_) => + (case assoc(pairs,a) of + Some(rls) => flat (map atoms ([th] RL rls)) + | None => [th]) + | _ => [th]) + | _ => [th]) + in atoms end; -fun mk_eq r = case concl_of r of +fun mk_meta_eq r = case concl_of r of Const("==",_)$_$_ => r | _$(Const("op =",_)$_$_) => r RS eq_reflection | _$(Const("not",_)$_) => r RS not_P_imp_P_eq_False @@ -40,8 +40,6 @@ fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; -fun mk_rews thm = map mk_eq (atomize(gen_all thm)); - val imp_cong = impI RSN (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))" (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp); @@ -56,6 +54,7 @@ "(True=P) = P", "(P=True) = P", "(True --> P) = P", "(False --> P) = True", "(P --> True) = True", "(P --> P) = True", + "(P --> False) = (~P)", "(P --> ~P) = (~P)", "(P & True) = P", "(True & P) = P", "(P & False) = False", "(False & P) = False", "(P & P) = P", "(P | True) = True", "(True | P) = True", @@ -97,8 +96,14 @@ infix addcongs; fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]); +val mksimps_pairs = + [("op -->", [mp]), ("op &", [conjunct1,conjunct2]), + ("All", [spec]), ("True", []), ("False", [])]; + +fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all; + val HOL_ss = empty_ss - setmksimps mk_rews + setmksimps (mksimps mksimps_pairs) setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac ORELSE' etac FalseE) setsubgoaler asm_simp_tac @@ -106,7 +111,7 @@ addcongs [imp_cong]; fun split_tac splits = - mk_case_split_tac (meta_eq_to_obj_eq RS iffD2) (map mk_eq splits); + mk_case_split_tac (meta_eq_to_obj_eq RS iffD2) (map mk_meta_eq splits); (* eliminiation of existential quantifiers in assumptions *)