More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
Changed the TFL functor to a structure (currently called Prim)
--- 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;
(*---------------------------------------------------------------------------
--- 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;
*
*
*---------------------------------------------------------------------------*)
--- 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
(*--------------------------------------------------------------
--- 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";
--- 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,
--- 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
--- 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
--- 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
--- 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 *)
--- 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
--- 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) =