# HG changeset patch # User paulson # Date 865328888 -7200 # Node ID 5e45dd3b64e98f3aedab3408890d393660b182c6 # Parent 0c7625196d95e94d3e8bd752b75ba65f576f8153 More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const Changed the TFL functor to a structure (currently called Prim) diff -r 0c7625196d95 -r 5e45dd3b64e9 TFL/dcterm.sml --- a/TFL/dcterm.sml Tue Jun 03 10:56:04 1997 +0200 +++ b/TFL/dcterm.sml Tue Jun 03 11:08:08 1997 +0200 @@ -12,8 +12,6 @@ sig val mk_conj : cterm * cterm -> cterm val mk_disj : cterm * cterm -> cterm - val mk_select : cterm * cterm -> cterm - val mk_forall : cterm * cterm -> cterm val mk_exists : cterm * cterm -> cterm val dest_conj : cterm -> cterm * cterm @@ -26,7 +24,6 @@ val dest_let : cterm -> cterm * cterm val dest_neg : cterm -> cterm val dest_pair : cterm -> cterm * cterm - val dest_select : cterm -> cterm * cterm val dest_var : cterm -> {Name:string, Ty:typ} val is_conj : cterm -> bool val is_cons : cterm -> bool @@ -38,19 +35,15 @@ val is_let : cterm -> bool val is_neg : cterm -> bool val is_pair : cterm -> bool - val is_select : cterm -> bool val list_mk_abs : cterm list -> cterm -> cterm val list_mk_exists : cterm list * cterm -> cterm - val list_mk_forall : cterm list * cterm -> cterm val list_mk_disj : cterm list -> cterm val strip_abs : cterm -> cterm list * cterm val strip_comb : cterm -> cterm * cterm list - val strip_conj : cterm -> cterm list val strip_disj : cterm -> cterm list val strip_exists : cterm -> cterm list * cterm val strip_forall : cterm -> cterm list * cterm val strip_imp : cterm -> cterm list * cterm - val strip_pair : cterm -> cterm list val drop_prop : cterm -> cterm val mk_prop : cterm -> cterm end = @@ -80,18 +73,6 @@ fun mk_const sign pr = cterm_of sign (Const pr); val mk_hol_const = mk_const (sign_of HOL.thy); -fun mk_select (r as (Bvar,Body)) = - let val ty = #T(rep_cterm Bvar) - val c = mk_hol_const("Eps", (ty --> HOLogic.boolT) --> ty) - in capply c (uncurry cabs r) - end; - -fun mk_forall (r as (Bvar,Body)) = - let val ty = #T(rep_cterm Bvar) - val c = mk_hol_const("All", (ty --> HOLogic.boolT) --> HOLogic.boolT) - in capply c (uncurry cabs r) - end; - fun mk_exists (r as (Bvar,Body)) = let val ty = #T(rep_cterm Bvar) val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT) @@ -186,7 +167,6 @@ val list_mk_abs = itlist cabs; fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v, b)) V t; -fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall(v, b)) V t; val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1, tm)) (*--------------------------------------------------------------------------- @@ -208,9 +188,7 @@ val strip_forall = rev2swap o strip dest_forall val strip_exists = rev2swap o strip dest_exists -val strip_conj = rev o (op::) o strip dest_conj val strip_disj = rev o (op::) o strip dest_disj -val strip_pair = rev o (op::) o strip dest_pair; (*--------------------------------------------------------------------------- diff -r 0c7625196d95 -r 5e45dd3b64e9 TFL/post.sml --- a/TFL/post.sml Tue Jun 03 10:56:04 1997 +0200 +++ b/TFL/post.sml Tue Jun 03 11:08:08 1997 +0200 @@ -27,7 +27,7 @@ -> {induction:thm, rules:thm, TCs:term list list} -> {induction:thm, rules:thm, nested_tcs:thm list} - val define_i : theory -> string -> term -> term + val define_i : theory -> string -> term -> term list -> theory * (thm * Prim.pattern list) val define : theory -> string -> string -> string list @@ -49,7 +49,7 @@ structure Tfl: TFL = struct structure Prim = Prim - structure S = Prim.USyntax + structure S = USyntax (*--------------------------------------------------------------------------- * Extract termination goals so that they can be put it into a goalstack, or @@ -95,7 +95,7 @@ *--------------------------------------------------------------------------*) val std_postprocessor = Prim.postprocess{WFtac = WFtac, terminator = terminator, - simplifier = Prim.Rules.simpl_conv simpls}; + simplifier = Rules.simpl_conv simpls}; val simplifier = rewrite_rule (simpls @ #simps(rep_ss (!simpset)) @ [pred_list_def]); @@ -103,7 +103,7 @@ fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy)); -val concl = #2 o Prim.Rules.dest_thm; +val concl = #2 o Rules.dest_thm; (*--------------------------------------------------------------------------- * Defining a function with an associated termination relation. @@ -120,8 +120,7 @@ fun define thy fid R eqs = let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[])) val (thy',(_,pats)) = - define_i thy fid (read thy R) - (fold_bal (app Ind_Syntax.conj) (map (read thy) eqs)) + define_i thy fid (read thy R) (map (read thy) eqs) in (thy',pats) end handle Utils.ERR {mesg,...} => error mesg; @@ -130,7 +129,7 @@ * processing from the definition stage. *---------------------------------------------------------------------------*) local -structure R = Prim.Rules +structure R = Rules structure U = Utils (* The rest of these local definitions are for the tricky nested case *) @@ -138,7 +137,7 @@ fun id_thm th = let val {lhs,rhs} = S.dest_eq(#2(S.strip_forall(#2 (R.dest_thm th)))) - in S.aconv lhs rhs + in lhs aconv rhs end handle _ => false fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]); @@ -196,8 +195,7 @@ tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl) (simplified@stubborn)} end - end handle (e as Utils.ERR _) => Utils.Raise e - | e => print_exn e; + end; (*lcp: curry the predicate of the induction rule*) @@ -235,7 +233,10 @@ rules = rules', tcs = (termination_goals rules') @ tcs} end - handle Utils.ERR {mesg,...} => error mesg + handle Utils.ERR {mesg,func,module} => + error (mesg ^ + "\n (In TFL function " ^ module ^ "." ^ func ^ ")") + | e => print_exn e; end; (*--------------------------------------------------------------------------- @@ -246,7 +247,7 @@ * inference at theory-construction time. * -local structure R = Prim.Rules +local structure R = Rules in fun function theory eqs = let val dummy = prs "Making definition.. " @@ -259,8 +260,7 @@ in {theory = theory, eq_ind = standard (induction RS (rules RS conjI))} end - handle (e as Utils.ERR _) => Utils.Raise e - | e => print_exn e + handle e => print_exn e end; @@ -268,8 +268,7 @@ let val {rules,theory, ...} = Prim.lazyR_def theory eqs in {eqns=rules, theory=theory} end - handle (e as Utils.ERR _) => Utils.Raise e - | e => print_exn e; + handle e => print_exn e; * * *---------------------------------------------------------------------------*) diff -r 0c7625196d95 -r 5e45dd3b64e9 TFL/rules.new.sml --- a/TFL/rules.new.sml Tue Jun 03 10:56:04 1997 +0200 +++ b/TFL/rules.new.sml Tue Jun 03 11:08:08 1997 +0200 @@ -6,7 +6,7 @@ Emulation of HOL inference rules for TFL *) -structure FastRules : Rules_sig = +structure Rules : Rules_sig = struct open Utils; @@ -17,7 +17,7 @@ structure D = Dcterm; -fun RULES_ERR{func,mesg} = Utils.ERR{module = "FastRules",func=func,mesg=mesg}; +fun RULES_ERR{func,mesg} = Utils.ERR{module = "Rules",func=func,mesg=mesg}; fun cconcl thm = D.drop_prop(#prop(crep_thm thm)); @@ -502,7 +502,7 @@ val (f,args) = S.strip_comb (get_lhs eq) val (vstrl,_) = S.strip_abs f val names = map (#1 o dest_Free) - (variants (S.free_vars body) vstrl) + (variants (term_frees body) vstrl) in get (rst, n+1, (names,n)::L) end handle _ => get (rst, n+1, L); @@ -750,8 +750,8 @@ val dummy = print_thms "cntxt:\n" cntxt val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _, sign,...} = rep_thm thm - fun genl tm = let val vlist = U.set_diff (curry(op aconv)) - (add_term_frees(tm,[])) [func,R] + fun genl tm = let val vlist = gen_rems (op aconv) + (add_term_frees(tm,[]), [func,R]) in U.itlist Forall vlist tm end (*-------------------------------------------------------------- diff -r 0c7625196d95 -r 5e45dd3b64e9 TFL/sys.sml --- a/TFL/sys.sml Tue Jun 03 10:56:04 1997 +0200 +++ b/TFL/sys.sml Tue Jun 03 11:08:08 1997 +0200 @@ -12,20 +12,11 @@ (* Establish a base of common and/or helpful functions. *) use "utils.sig"; -(* Get the specifications - these are independent of any system *) use "usyntax.sig"; use "rules.sig"; use "thry.sig"; use "thms.sig"; use "tfl.sig"; - -(*---------------------------------------------------------------------------- - * Load the TFL functor - this is defined totally in terms of the - * above interfaces. - *---------------------------------------------------------------------------*) - -use "tfl.sml"; - use "utils.sml"; (*---------------------------------------------------------------------------- @@ -42,8 +33,5 @@ (*---------------------------------------------------------------------------- * Link system and specialize for Isabelle *---------------------------------------------------------------------------*) -structure Prim = TFL(structure Rules = FastRules - structure Thms = Thms - structure Thry = Thry); - +use "tfl.sml"; use"post.sml"; diff -r 0c7625196d95 -r 5e45dd3b64e9 TFL/tfl.sig --- a/TFL/tfl.sig Tue Jun 03 10:56:04 1997 +0200 +++ b/TFL/tfl.sig Tue Jun 03 11:08:08 1997 +0200 @@ -3,20 +3,15 @@ Author: Konrad Slind, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge -Main TFL functor +Main module *) signature TFL_sig = sig - structure Rules: Rules_sig - structure Thms : Thms_sig - structure Thry : Thry_sig - structure USyntax : USyntax_sig - datatype pattern = GIVEN of term * int | OMITTED of term * int - val mk_functional : theory -> term + val mk_functional : theory -> term list -> {functional:term, pats: pattern list} @@ -30,7 +25,7 @@ patterns : pattern list} - val wfrec_eqns : theory -> term + val wfrec_eqns : theory -> term list -> {WFR : term, proto_def : term, extracta :(thm * term list) list, @@ -38,7 +33,7 @@ val lazyR_def : theory - -> term + -> term list -> {theory:theory, rules :thm, R :term, diff -r 0c7625196d95 -r 5e45dd3b64e9 TFL/tfl.sml --- a/TFL/tfl.sml Tue Jun 03 10:56:04 1997 +0200 +++ b/TFL/tfl.sml Tue Jun 03 11:08:08 1997 +0200 @@ -3,31 +3,17 @@ Author: Konrad Slind, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge -Main TFL functor +Main module *) -functor TFL(structure Rules : Rules_sig - structure Thry : Thry_sig - structure Thms : Thms_sig) : TFL_sig = +structure Prim : TFL_sig = struct -(* Declarations *) -structure Thms = Thms; -structure Rules = Rules; -structure Thry = Thry; -structure USyntax = Thry.USyntax; - - (* Abbreviations *) structure R = Rules; structure S = USyntax; structure U = S.Utils; -nonfix mem -->; -val --> = S.-->; - -infixr 3 -->; - val concl = #2 o R.dest_thm; val hyp = #1 o R.dest_thm; @@ -83,13 +69,13 @@ | part {constrs = [], rows = _::_, A} = pfail"extra cases in defn" | part {constrs = _::_, rows = [], A} = pfail"cases missing in defn" | part {constrs = c::crst, rows, A} = - let val {Name,Ty} = S.dest_const c - val (L,_) = S.strip_type Ty + let val (Name,Ty) = dest_Const c + val L = binder_types Ty val (in_group, not_in_group) = U.itlist (fn (row as (p::rst, rhs)) => fn (in_group,not_in_group) => let val (pc,args) = S.strip_comb p - in if (#Name(S.dest_const pc) = Name) + in if (#1(dest_Const pc) = Name) then ((args@rst, rhs)::in_group, not_in_group) else (in_group, row::not_in_group) end) rows ([],[]) @@ -112,8 +98,10 @@ datatype pattern = GIVEN of term * int | OMITTED of term * int -fun psubst theta (GIVEN (tm,i)) = GIVEN(subst_free theta tm, i) - | psubst theta (OMITTED (tm,i)) = OMITTED(subst_free theta tm, i); +fun pattern_map f (GIVEN (tm,i)) = GIVEN(f tm, i) + | pattern_map f (OMITTED (tm,i)) = OMITTED(f tm, i); + +fun pattern_subst theta = pattern_map (subst_free theta); fun dest_pattern (GIVEN (tm,i)) = ((GIVEN,i),tm) | dest_pattern (OMITTED (tm,i)) = ((OMITTED,i),tm); @@ -125,8 +113,9 @@ * Produce an instance of a constructor, plus genvars for its arguments. *---------------------------------------------------------------------------*) fun fresh_constr ty_match colty gv c = - let val {Ty,...} = S.dest_const c - val (L,ty) = S.strip_type Ty + let val (_,Ty) = dest_Const c + val L = binder_types Ty + and ty = body_type Ty val ty_theta = ty_match ty colty val c' = S.inst ty_theta c val gvars = map (S.inst ty_theta o gv) L @@ -142,7 +131,7 @@ U.itlist (fn (row as ((prefix, p::rst), rhs)) => fn (in_group,not_in_group) => let val (pc,args) = S.strip_comb p - in if ((#Name(S.dest_const pc) = Name) handle _ => false) + in if ((#1(dest_Const pc) = Name) handle _ => false) then (((prefix,args@rst), rhs)::in_group, not_in_group) else (in_group, row::not_in_group) end) rows ([],[]); @@ -157,7 +146,7 @@ fun part {constrs = [], rows, A} = rev A | part {constrs = c::crst, rows, A} = let val (c',gvars) = fresh c - val {Name,Ty} = S.dest_const c' + val (Name,Ty) = dest_Const c' val (in_group, not_in_group) = mk_group Name rows val in_group' = if (null in_group) (* Constructor not given *) @@ -178,7 +167,7 @@ *---------------------------------------------------------------------------*) fun mk_pat (c,l) = - let val L = length(#1(S.strip_type(type_of c))) + let val L = length (binder_types (type_of c)) fun build (prefix,tag,plist) = let val args = take (L,plist) and plist' = drop(L,plist) @@ -211,7 +200,7 @@ then let val fresh = fresh_constr ty_match ty fresh_var fun expnd (c,gvs) = let val capp = list_comb(c,gvs) - in ((prefix, capp::rst), psubst[(p,capp)] rhs) + in ((prefix, capp::rst), pattern_subst[(p,capp)] rhs) end in map expnd (map fresh constructors) end else [row] @@ -229,7 +218,7 @@ val col0 = map(hd o #2) pat_rectangle in if (forall is_Free col0) - then let val rights' = map (fn(v,e) => psubst[(v,u)] e) + then let val rights' = map (fn(v,e) => pattern_subst[(v,u)] e) (ListPair.zip (col0, rights)) val pat_rectangle' = map v_to_prefix pat_rectangle val (pref_patl,tm) = mk{path = rstp, @@ -243,7 +232,7 @@ case (ty_info ty_name) of None => mk_case_fail("Not a known datatype: "^ty_name) | Some{case_const,constructors} => - let val case_const_name = #Name(S.dest_const case_const) + let val case_const_name = #1(dest_Const case_const) val nrows = List_.concat (map (expand constructors pty) rows) val subproblems = divide(constructors, pty, range_ty, nrows) val groups = map #group subproblems @@ -256,8 +245,7 @@ val case_functions = map S.list_mk_abs (ListPair.zip (new_formals, dtrees)) val types = map type_of (case_functions@[u]) @ [range_ty] - val case_const' = S.mk_const{Name = case_const_name, - Ty = list_mk_type types} + val case_const' = Const(case_const_name, list_mk_type types) val tree = list_comb(case_const', case_functions@[u]) val pat_rect1 = List_.concat (ListPair.map mk_pat (constructors', pat_rect)) @@ -271,7 +259,7 @@ (* Repeated variable occurrences in a pattern are not allowed. *) fun FV_multiset tm = case (S.dest_term tm) - of S.VAR v => [S.mk_var v] + of S.VAR{Name,Ty} => [Free(Name,Ty)] | S.CONST _ => [] | S.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand | S.LAMB _ => raise TFL_ERR{func = "FV_multiset", mesg = "lambda"}; @@ -288,39 +276,35 @@ in check (FV_multiset pat) end; -local fun paired1{lhs,rhs} = (lhs,rhs) - and paired2{Rator,Rand} = (Rator,Rand) - fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s} +local fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s} fun single [f] = f | single fs = mk_functional_err (Int.toString (length fs) ^ " distinct function names!") in -fun mk_functional thy eqs = - let val clauses = S.strip_conj eqs - val (L,R) = ListPair.unzip - (map (paired1 o S.dest_eq o #2 o S.strip_forall) - clauses) - val (funcs,pats) = ListPair.unzip(map (paired2 o S.dest_comb) L) - val f = single (U.mk_set (S.aconv) funcs) - val fvar = if (is_Free f) then f else S.mk_var(S.dest_const f) +fun mk_functional thy clauses = + let val (L,R) = ListPair.unzip + (map (fn (Const("op =",_) $ t $ u) => (t,u)) clauses) + val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L) + val f = single (gen_distinct (op aconv) funcs) + (**??why change the Const to a Free??????????????**) + val fvar = if (is_Free f) then f else Free(dest_Const f) val dummy = map (no_repeat_vars thy) pats val rows = ListPair.zip (map (fn x => ([],[x])) pats, map GIVEN (enumerate R)) val fvs = S.free_varsl R - val a = S.variant fvs (S.mk_var{Name="a", Ty = type_of(hd pats)}) + val a = S.variant fvs (Free("a",type_of(hd pats))) val FV = a::fvs val ty_info = Thry.match_info thy val ty_match = Thry.match_type thy val range_ty = type_of (hd R) val (patts, case_tm) = mk_case ty_info ty_match FV range_ty {path=[a], rows=rows} - val patts1 = map (fn (_,(tag,i),[pat]) => tag (pat,i)) patts handle _ - => mk_functional_err "error in pattern-match translation" + val patts1 = map (fn (_,(tag,i),[pat]) => tag (pat,i)) patts + handle _ => mk_functional_err "error in pattern-match translation" val patts2 = U.sort(fn p1=>fn p2=> row_of_pat p1 < row_of_pat p2) patts1 val finals = map row_of_pat patts2 val originals = map (row_of_pat o #2) rows - fun int_eq i1 (i2:int) = (i1=i2) - val dummy = case (U.set_diff int_eq originals finals) + val dummy = case (originals\\finals) of [] => () | L => mk_functional_err("The following rows (counting from zero)\ \ are inaccessible: "^stringize L) @@ -352,20 +336,19 @@ val (fname,_) = dest_Free f val (wfrec,_) = S.strip_comb rhs in -fun wfrec_definition0 thy fid R functional = - let val {Bvar,...} = S.dest_abs functional - val (Name, Ty) = dest_Free Bvar - val def_name = if Name<>fid then +fun wfrec_definition0 thy fid R (functional as Abs(Name, Ty, _)) = + let val def_name = if Name<>fid then raise TFL_ERR{func = "wfrec_definition0", mesg = "Expected a definition of " ^ quote fid ^ " but found one of " ^ quote Name} else Name ^ "_def" - val wfrec_R_M = map_term_types poly_tvars - (wfrec $ R $ (map_term_types poly_tvars functional)) + val wfrec_R_M = map_term_types poly_tvars + (wfrec $ map_term_types poly_tvars R) + $ functional val (_, def_term, _) = Sign.infer_types (sign_of thy) (K None) (K None) [] false - ([HOLogic.mk_eq(Bvar, wfrec_R_M)], + ([HOLogic.mk_eq(Const(Name,Ty), wfrec_R_M)], HOLogic.boolT) in @@ -401,9 +384,10 @@ fun merge full_pats TCs = let fun insert (p,TCs) = let fun insrt ((x as (h,[]))::rst) = - if (S.aconv p h) then (p,TCs)::rst else x::insrt rst + if (p aconv h) then (p,TCs)::rst else x::insrt rst | insrt (x::rst) = x::insrt rst - | insrt[] = raise TFL_ERR{func="merge.insert",mesg="pat not found"} + | insrt[] = raise TFL_ERR{func="merge.insert", + mesg="pattern not found"} in insrt end fun pass ([],ptcl_final) = ptcl_final | pass (ptcs::tcl, ptcl) = pass(tcl, insert ptcs ptcl) @@ -411,10 +395,14 @@ pass (TCs, map (fn p => (p,[])) full_pats) end; -fun not_omitted (GIVEN(tm,_)) = tm - | not_omitted (OMITTED _) = raise TFL_ERR{func="not_omitted",mesg=""} -val givens = U.mapfilter not_omitted; +(*Replace all TFrees by TVars [CURRENTLY UNUSED]*) +val tvars_of_tfrees = + map_term_types (map_type_tfree (fn (a,sort) => TVar ((a, 0), sort))); + +fun givens [] = [] + | givens (GIVEN(tm,_)::pats) = tm :: givens pats + | givens (OMITTED _::pats) = givens pats; fun post_definition (theory, (def, pats)) = let val tych = Thry.typecheck theory @@ -424,7 +412,8 @@ val WFR = #ant(S.dest_imp(concl corollary)) val R = #Rand(S.dest_comb WFR) val corollary' = R.UNDISCH corollary (* put WF R on assums *) - val corollaries = map (U.C R.SPEC corollary' o tych) given_pats + val corollaries = map (fn pat => R.SPEC (tych pat) corollary') + given_pats val (case_rewrites,context_congs) = extraction_thms theory val corollaries' = map(R.simplify case_rewrites) corollaries fun xtract th = R.CONTEXT_REWRITE_RULE(f,R) @@ -438,7 +427,8 @@ in {theory = theory, (* holds def, if it's needed *) rules = rules1, - full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)), + full_pats_TCs = merge (map pat_of pats) + (ListPair.zip (given_pats, TCs)), TCs = TCs, patterns = pats} end; @@ -457,7 +447,7 @@ val (case_rewrites,context_congs) = extraction_thms thy val tych = Thry.typecheck thy val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY - val R = S.variant(S.free_vars eqns) + val R = S.variant(foldr add_term_frees (eqns,[])) (#Bvar(S.dest_forall(concl WFREC_THM0))) val WFREC_THM = R.ISPECL [tych R, tych f] WFREC_THM0 val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM) @@ -616,12 +606,12 @@ fun complete_cases thy = let val tych = Thry.typecheck thy - fun pmk_var n ty = S.mk_var{Name = n,Ty = ty} val ty_info = Thry.induct_info thy in fn pats => let val FV0 = S.free_varsl pats - val a = S.variant FV0 (pmk_var "a" (type_of(hd pats))) - val v = S.variant (a::FV0) (pmk_var "v" (type_of a)) + val T = type_of (hd pats) + val a = S.variant FV0 (Free ("a", T)) + val v = S.variant (a::FV0) (Free ("v", T)) val FV = a::v::FV0 val a_eq_v = HOLogic.mk_eq(a,v) val ex_th0 = R.EXISTS (tych (S.mk_exists{Bvar=v,Body=a_eq_v}), tych a) @@ -661,7 +651,7 @@ of [] => (P_y, (tm,[])) | _ => let val imp = S.list_mk_conj cntxt ==> P_y - val lvs = U.set_diff S.aconv (S.free_vars_lr imp) globals + val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals) val locals = #2(U.pluck (S.aconv P) lvs) handle _ => lvs in (S.list_mk_forall(locals,imp), (tm,locals)) end end @@ -750,7 +740,7 @@ val case_thm = complete_cases thy pats val domain = (type_of o hd) pats val P = S.variant (S.all_varsl (pats @ List_.concat TCsl)) - (S.mk_var{Name="P", Ty=domain --> HOLogic.boolT}) + (Free("P",domain --> HOLogic.boolT)) val Sinduct = R.SPEC (tych P) Sinduction val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct) val Rassums_TCl' = map (build_ih f P) pat_TCs_list @@ -760,7 +750,7 @@ val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum) val proved_cases = map (prove_case f thy) tasks val v = S.variant (S.free_varsl (map concl proved_cases)) - (S.mk_var{Name="v", Ty=domain}) + (Free("v",domain)) val vtyped = tych v val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]th') @@ -774,11 +764,12 @@ (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc) in R.GEN (tych P) (R.DISCH (tych(concl Rinduct_assum)) dc') -end +end handle _ => raise TFL_ERR{func = "mk_induction", mesg = "failed derivation"}; + (*--------------------------------------------------------------------------- * * POST PROCESSING @@ -875,7 +866,7 @@ fun loop ([],extras,R,ind) = (rev R, ind, extras) | loop ((r,ftcs)::rst, nthms, R, ind) = let val tcs = #1(strip_imp (concl r)) - val extra_tcs = U.set_diff S.aconv ftcs tcs + val extra_tcs = gen_rems (op aconv) (ftcs, tcs) val extra_tc_thms = map simplify_nested_tc extra_tcs val (r1,ind1) = U.rev_itlist simplify_tc tcs (r,ind) val r2 = R.FILTER_DISCH_ALL(not o S.is_WFR) r1 diff -r 0c7625196d95 -r 5e45dd3b64e9 TFL/thry.sml --- a/TFL/thry.sml Tue Jun 03 10:56:04 1997 +0200 +++ b/TFL/thry.sml Tue Jun 03 11:08:08 1997 +0200 @@ -55,14 +55,13 @@ *---------------------------------------------------------------------------*) local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection)) val Const(eeq_name, ty) = eeq - val prop = #2 (S.strip_type ty) + val prop = body_type ty in fun make_definition parent s tm = let val {lhs,rhs} = S.dest_eq tm - val (Name,Ty) = dest_Const lhs - val lhs1 = S.mk_const{Name = Name, Ty = Ty} - val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop} - val dtm = list_comb(eeq1,[lhs1,rhs]) (* Rename "=" to "==" *) + val (_,Ty) = dest_Const lhs + val eeq1 = Const(eeq_name, Ty --> Ty --> prop) + val dtm = list_comb(eeq1,[lhs,rhs]) (* Rename "=" to "==" *) val (_, tm', _) = Sign.infer_types (sign_of parent) (K None) (K None) [] true ([dtm],propT) val new_thy = add_defs_i [(s,tm')] parent diff -r 0c7625196d95 -r 5e45dd3b64e9 TFL/usyntax.sig --- a/TFL/usyntax.sig Tue Jun 03 10:56:04 1997 +0200 +++ b/TFL/usyntax.sig Tue Jun 03 11:08:08 1997 +0200 @@ -16,19 +16,15 @@ | LAMB of {Bvar : term, Body : term} val alpha : typ - val mk_preterm : cterm -> term (* Types *) val type_vars : typ -> typ list val type_varsl : typ list -> typ list val mk_vartype : string -> typ val is_vartype : typ -> bool - val --> : typ * typ -> typ - val strip_type : typ -> typ list * typ val strip_prod_type : typ -> typ list (* Terms *) - val free_vars : term -> term list val free_varsl : term list -> term list val free_vars_lr : term -> term list val all_vars : term -> term list @@ -43,8 +39,6 @@ val beta_conv : term -> term (* Construction routines *) - val mk_var :{Name : string, Ty : typ} -> term - val mk_const :{Name : string, Ty : typ} -> term val mk_comb :{Rator : term, Rand : term} -> term val mk_abs :{Bvar : term, Body : term} -> term @@ -62,7 +56,6 @@ val dest_abs : term -> {Bvar : term, Body : term} val dest_eq : term -> {lhs : term, rhs : term} val dest_imp : term -> {ant : term, conseq : term} - val dest_select : term -> {Bvar : term, Body : term} val dest_forall : term -> {Bvar : term, Body : term} val dest_exists : term -> {Bvar : term, Body : term} val dest_neg : term -> term @@ -104,9 +97,7 @@ val strip_imp : term -> (term list * term) val strip_forall : term -> (term list * term) val strip_exists : term -> (term list * term) - val strip_conj : term -> term list val strip_disj : term -> term list - val strip_pair : term -> term list (* Miscellaneous *) val mk_vstruct : typ -> term list -> term diff -r 0c7625196d95 -r 5e45dd3b64e9 TFL/usyntax.sml --- a/TFL/usyntax.sml Tue Jun 03 10:56:04 1997 +0200 +++ b/TFL/usyntax.sml Tue Jun 03 11:08:08 1997 +0200 @@ -33,21 +33,11 @@ val is_vartype = Utils.can dest_vtype; val type_vars = map mk_prim_vartype o typ_tvars -fun type_varsl L = Utils.mk_set (curry op=) - (Utils.rev_itlist (curry op @ o type_vars) L []); +fun type_varsl L = distinct (Utils.rev_itlist (curry op @ o type_vars) L []); val alpha = mk_vartype "'a" val beta = mk_vartype "'b" - - -(* What nonsense *) -nonfix -->; -val --> = -->; -infixr 3 -->; - -fun strip_type ty = (binder_types ty, body_type ty); - fun strip_prod_type (Type("*", [ty1,ty2])) = strip_prod_type ty1 @ strip_prod_type ty2 | strip_prod_type ty = [ty]; @@ -62,8 +52,6 @@ nonfix aconv; val aconv = curry (op aconv); -fun free_vars tm = add_term_frees(tm,[]); - (* Free variables, in order of occurrence, from left to right in the * syntax tree. *) @@ -79,12 +67,11 @@ -fun free_varsl L = Utils.mk_set aconv - (Utils.rev_itlist (curry op @ o free_vars) L []); +fun free_varsl L = gen_distinct Term.aconv + (Utils.rev_itlist (curry op @ o term_frees) L []); val type_vars_in_term = map mk_prim_vartype o term_tvars; -(* Can't really be very exact in Isabelle *) fun all_vars tm = let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end fun add (t, A) = case t of @@ -94,7 +81,7 @@ | _ => A in rev(add(tm,[])) end; -fun all_varsl L = Utils.mk_set aconv +fun all_varsl L = gen_distinct Term.aconv (Utils.rev_itlist (curry op @ o all_vars) L []); @@ -107,8 +94,6 @@ (* Construction routines *) -fun mk_var{Name,Ty} = Free(Name,Ty); -val mk_prim_var = Var; val string_variant = variant; @@ -126,7 +111,6 @@ mesg = "2nd arg. should be a variable"} end; -fun mk_const{Name,Ty} = Const(Name,Ty) fun mk_comb{Rator,Rand} = Rator $ Rand; fun mk_abs{Bvar as Var((s,_),ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) @@ -135,36 +119,36 @@ fun mk_imp{ant,conseq} = - let val c = mk_const{Name = "op -->", Ty = HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT} + let val c = Const("op -->",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) in list_comb(c,[ant,conseq]) end; fun mk_select (r as {Bvar,Body}) = let val ty = type_of Bvar - val c = mk_const{Name = "Eps", Ty = (ty --> HOLogic.boolT) --> ty} + val c = Const("Eps",(ty --> HOLogic.boolT) --> ty) in list_comb(c,[mk_abs r]) end; fun mk_forall (r as {Bvar,Body}) = let val ty = type_of Bvar - val c = mk_const{Name = "All", Ty = (ty --> HOLogic.boolT) --> HOLogic.boolT} + val c = Const("All",(ty --> HOLogic.boolT) --> HOLogic.boolT) in list_comb(c,[mk_abs r]) end; fun mk_exists (r as {Bvar,Body}) = let val ty = type_of Bvar - val c = mk_const{Name = "Ex", Ty = (ty --> HOLogic.boolT) --> HOLogic.boolT} + val c = Const("Ex",(ty --> HOLogic.boolT) --> HOLogic.boolT) in list_comb(c,[mk_abs r]) end; fun mk_conj{conj1,conj2} = - let val c = mk_const{Name = "op &", Ty = HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT} + let val c = Const("op &",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) in list_comb(c,[conj1,conj2]) end; fun mk_disj{disj1,disj2} = - let val c = mk_const{Name = "op |", Ty = HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT} + let val c = Const("op |",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) in list_comb(c,[disj1,disj2]) end; @@ -172,7 +156,7 @@ local fun mk_uncurry(xt,yt,zt) = - mk_const{Name = "split", Ty = (xt --> yt --> zt) --> prod_ty xt yt --> zt} + Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt) fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} | dest_pair _ = raise USYN_ERR{func = "dest_pair", mesg = "not a pair"} fun is_var(Var(_)) = true | is_var (Free _) = true | is_var _ = false @@ -202,7 +186,7 @@ | dest_term(Free(s,ty)) = VAR{Name = s, Ty = ty} | dest_term(Const(s,ty)) = CONST{Name = s, Ty = ty} | dest_term(M$N) = COMB{Rator=M,Rand=N} - | dest_term(Abs(s,ty,M)) = let val v = mk_var{Name = s, Ty = ty} + | dest_term(Abs(s,ty,M)) = let val v = Free(s,ty) in LAMB{Bvar = v, Body = betapply (M,v)} end | dest_term(Bound _) = raise USYN_ERR{func = "dest_term",mesg = "Bound"}; @@ -214,7 +198,7 @@ | dest_comb _ = raise USYN_ERR{func = "dest_comb", mesg = "not a comb"}; fun dest_abs(a as Abs(s,ty,M)) = - let val v = mk_var{Name = s, Ty = ty} + let val v = Free(s,ty) in {Bvar = v, Body = betapply (a,v)} end | dest_abs _ = raise USYN_ERR{func = "dest_abs", mesg = "not an abstraction"}; @@ -225,9 +209,6 @@ fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N} | dest_imp _ = raise USYN_ERR{func = "dest_imp", mesg = "not an implication"}; -fun dest_select(Const("Eps",_) $ (a as Abs _)) = dest_abs a - | dest_select _ = raise USYN_ERR{func = "dest_select", mesg = "not a select"}; - fun dest_forall(Const("All",_) $ (a as Abs _)) = dest_abs a | dest_forall _ = raise USYN_ERR{func = "dest_forall", mesg = "not a forall"}; @@ -246,7 +227,7 @@ fun mk_pair{fst,snd} = let val ty1 = type_of fst val ty2 = type_of snd - val c = mk_const{Name = "Pair", Ty = ty1 --> ty2 --> prod_ty ty1 ty2} + val c = Const("Pair",ty1 --> ty2 --> prod_ty ty1 ty2) in list_comb(c,[fst,snd]) end; @@ -307,7 +288,7 @@ (* Need to reverse? *) -fun gen_all tm = list_mk_forall(free_vars tm, tm); +fun gen_all tm = list_mk_forall(term_frees tm, tm); (* Destructing a cterm to a list of Terms *) fun strip_comb tm = @@ -349,13 +330,6 @@ end else ([],fm); -fun strip_conj w = - if (is_conj w) - then let val {conj1,conj2} = dest_conj w - in (strip_conj conj1@strip_conj conj2) - end - else [w]; - fun strip_disj w = if (is_disj w) then let val {disj1,disj2} = dest_disj w @@ -363,21 +337,6 @@ end else [w]; -fun strip_pair tm = - if (is_pair tm) - then let val {fst,snd} = dest_pair tm - fun dtuple t = - if (is_pair t) - then let val{fst,snd} = dest_pair t - in (fst :: dtuple snd) - end - else [t] - in fst::dtuple snd - end - else [tm]; - - -fun mk_preterm tm = #t(rep_cterm tm); (* Miscellaneous *) @@ -432,7 +391,7 @@ fun is_WFR tm = (#Name(dest_const(rator tm)) = "wf") handle _ => false; -fun ARB ty = mk_select{Bvar=mk_var{Name="v",Ty=ty}, - Body=mk_const{Name="True",Ty=HOLogic.boolT}}; +fun ARB ty = mk_select{Bvar=Free("v",ty), + Body=Const("True",HOLogic.boolT)}; end; (* Syntax *) diff -r 0c7625196d95 -r 5e45dd3b64e9 TFL/utils.sig --- a/TFL/utils.sig Tue Jun 03 10:56:04 1997 +0200 +++ b/TFL/utils.sig Tue Jun 03 11:08:08 1997 +0200 @@ -8,26 +8,17 @@ signature Utils_sig = sig - (* General error format and reporting mechanism *) exception ERR of {module:string,func:string, mesg:string} - val Raise : exn -> 'a val can : ('a -> 'b) -> 'a -> bool val holds : ('a -> bool) -> 'a -> bool val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c - (* Set operations *) - val mem : ('a -> 'a -> bool) -> 'a -> 'a list -> bool - val set_diff : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list - val mk_set : ('a -> 'a -> bool) -> 'a list -> 'a list - val itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b val rev_itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b val end_itlist : ('a -> 'a -> 'a) -> 'a list -> 'a val itlist2 :('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c - val mapfilter : ('a -> 'b) -> 'a list -> 'b list val pluck : ('a -> bool) -> 'a list -> 'a * 'a list - val front_back : 'a list -> 'a list * 'a val zip3 : 'a list -> 'b list -> 'c list -> ('a*'b*'c) list val take : ('a -> 'b) -> int * 'a list -> 'b list val sort : ('a -> 'a -> bool) -> 'a list -> 'a list diff -r 0c7625196d95 -r 5e45dd3b64e9 TFL/utils.sml --- a/TFL/utils.sml Tue Jun 03 10:56:04 1997 +0200 +++ b/TFL/utils.sml Tue Jun 03 11:08:08 1997 +0200 @@ -13,18 +13,6 @@ exception ERR of {module:string,func:string, mesg:string}; fun UTILS_ERR{func,mesg} = ERR{module = "Utils",func=func,mesg=mesg}; -local -fun info_string s {module,func,mesg} = - (s^" at "^module^"."^func^":\n"^mesg^"\n") -in -val ERR_string = info_string "Exception raised" -val MESG_string = info_string "Message" -end; - -fun Raise (e as ERR sss) = (TextIO.output(TextIO.stdOut, ERR_string sss); - raise e) - | Raise e = raise e; - (* Simple combinators *) @@ -58,21 +46,12 @@ in it (L1,L2) end; -fun mapfilter f alist = itlist (fn i=>fn L=> (f i::L) handle _ => L) alist []; - fun pluck p = let fun remv ([],_) = raise UTILS_ERR{func="pluck",mesg = "item not found"} | remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A) in fn L => remv(L,[]) end; -fun front_back [] = raise UTILS_ERR{func="front_back",mesg="empty list"} - | front_back [x] = ([],x) - | front_back (h::t) = - let val (L,b) = front_back t - in (h::L,b) - end; - fun take f = let fun grab(0,L) = [] | grab(n, x::rst) = f x::grab(n-1,rst) @@ -88,26 +67,6 @@ fun holds P x = P x handle _ => false; -(* Set ops *) -nonfix mem; (* Gag Barf Choke *) -fun mem eq_func i = - let val eqi = eq_func i - fun mm [] = false - | mm (a::rst) = eqi a orelse mm rst - in mm - end; - -fun mk_set eq_func = - let val mem = mem eq_func - fun mk [] = [] - | mk (a::rst) = if (mem a rst) then mk rst else a::(mk rst) - in mk - end; - -(* All the elements in the first set that are not also in the second set. *) -fun set_diff eq_func S1 S2 = filter (fn x => not (mem eq_func x S2)) S1 - - fun sort R = let fun part (m, []) = ([],[]) | part (m, h::rst) =