Numerous simplifications and removal of HOL-isms
authorpaulson
Thu Jun 05 13:27:28 1997 +0200 (1997-06-05)
changeset 34052cccd0e3e9ea
parent 3404 91a91790899a
child 3406 131262e21ada
Numerous simplifications and removal of HOL-isms
Addition of the "simpset" feature (replacing references to \!simpset)
TFL/dcterm.sml
TFL/post.sml
TFL/rules.new.sml
TFL/rules.sig
TFL/tfl.sig
TFL/tfl.sml
TFL/thry.sig
TFL/thry.sml
TFL/usyntax.sig
TFL/usyntax.sml
     1.1 --- a/TFL/dcterm.sml	Thu Jun 05 13:26:09 1997 +0200
     1.2 +++ b/TFL/dcterm.sml	Thu Jun 05 13:27:28 1997 +0200
     1.3 @@ -35,8 +35,6 @@
     1.4      val is_let : cterm -> bool
     1.5      val is_neg : cterm -> bool
     1.6      val is_pair : cterm -> bool
     1.7 -    val list_mk_abs : cterm list -> cterm -> cterm
     1.8 -    val list_mk_exists : cterm list * cterm -> cterm
     1.9      val list_mk_disj : cterm list -> cterm
    1.10      val strip_abs : cterm -> cterm list * cterm
    1.11      val strip_comb : cterm -> cterm * cterm list
    1.12 @@ -57,14 +55,6 @@
    1.13  val can = Utils.can;
    1.14  fun swap (x,y) = (y,x);
    1.15  
    1.16 -fun itlist f L base_value =
    1.17 -   let fun it [] = base_value
    1.18 -         | it (a::rst) = f a (it rst)
    1.19 -   in it L 
    1.20 -   end;
    1.21 -
    1.22 -val end_itlist = Utils.end_itlist;
    1.23 -
    1.24  
    1.25  (*---------------------------------------------------------------------------
    1.26   * Some simple constructor functions.
    1.27 @@ -164,10 +154,7 @@
    1.28  (*---------------------------------------------------------------------------
    1.29   * Iterated creation.
    1.30   *---------------------------------------------------------------------------*)
    1.31 -val list_mk_abs = itlist cabs;
    1.32 -
    1.33 -fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v, b)) V t;
    1.34 -val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1, tm))
    1.35 +val list_mk_disj = Utils.end_itlist(fn d1 => fn tm => mk_disj(d1, tm))
    1.36  
    1.37  (*---------------------------------------------------------------------------
    1.38   * Iterated destruction. (To the "right" in a term.)
     2.1 --- a/TFL/post.sml	Thu Jun 05 13:26:09 1997 +0200
     2.2 +++ b/TFL/post.sml	Thu Jun 05 13:27:28 1997 +0200
     2.3 @@ -6,13 +6,6 @@
     2.4  Postprocessing of TFL definitions
     2.5  *)
     2.6  
     2.7 -(*-------------------------------------------------------------------------
     2.8 -Three postprocessors are applied to the definition:
     2.9 -    - a wellfoundedness prover (WF_TAC)
    2.10 -    - a simplifier (tries to eliminate the language of termination expressions)
    2.11 -    - a termination prover
    2.12 -*-------------------------------------------------------------------------*)
    2.13 -
    2.14  signature TFL = 
    2.15    sig
    2.16     structure Prim : TFL_sig
    2.17 @@ -20,20 +13,17 @@
    2.18     val tgoalw : theory -> thm list -> thm list -> thm list
    2.19     val tgoal: theory -> thm list -> thm list
    2.20  
    2.21 -   val WF_TAC : thm list -> tactic
    2.22 -
    2.23 -   val simplifier : thm -> thm
    2.24 -   val std_postprocessor : theory 
    2.25 +   val std_postprocessor : simpset -> theory 
    2.26                             -> {induction:thm, rules:thm, TCs:term list list} 
    2.27                             -> {induction:thm, rules:thm, nested_tcs:thm list}
    2.28  
    2.29     val define_i : theory -> string -> term -> term list
    2.30 -                  -> theory * (thm * Prim.pattern list)
    2.31 +                  -> theory * Prim.pattern list
    2.32  
    2.33     val define   : theory -> string -> string -> string list 
    2.34                    -> theory * Prim.pattern list
    2.35  
    2.36 -   val simplify_defn : theory * (string * Prim.pattern list)
    2.37 +   val simplify_defn : simpset -> theory * (string * Prim.pattern list)
    2.38                          -> {rules:thm list, induct:thm, tcs:term list}
    2.39  
    2.40    (*-------------------------------------------------------------------------
    2.41 @@ -56,51 +46,38 @@
    2.42   * have a tactic directly applied to them.
    2.43   *--------------------------------------------------------------------------*)
    2.44  fun termination_goals rules = 
    2.45 -    map (Logic.freeze_vars o HOLogic.dest_Trueprop)
    2.46 +    map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop)
    2.47        (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, []));
    2.48  
    2.49 - (*---------------------------------------------------------------------------
    2.50 -  * Finds the termination conditions in (highly massaged) definition and 
    2.51 -  * puts them into a goalstack.
    2.52 -  *--------------------------------------------------------------------------*)
    2.53 - fun tgoalw thy defs rules = 
    2.54 -    let val L = termination_goals rules
    2.55 -        open USyntax
    2.56 -        val g = cterm_of (sign_of thy) (HOLogic.mk_Trueprop(list_mk_conj L))
    2.57 -    in goalw_cterm defs g
    2.58 -    end;
    2.59 +(*---------------------------------------------------------------------------
    2.60 + * Finds the termination conditions in (highly massaged) definition and 
    2.61 + * puts them into a goalstack.
    2.62 + *--------------------------------------------------------------------------*)
    2.63 +fun tgoalw thy defs rules = 
    2.64 +   let val L = termination_goals rules
    2.65 +       open USyntax
    2.66 +       val g = cterm_of (sign_of thy) (HOLogic.mk_Trueprop(list_mk_conj L))
    2.67 +   in goalw_cterm defs g
    2.68 +   end;
    2.69  
    2.70 - fun tgoal thy = tgoalw thy [];
    2.71 -
    2.72 - (*---------------------------------------------------------------------------
    2.73 -  * Simple wellfoundedness prover.
    2.74 -  *--------------------------------------------------------------------------*)
    2.75 - fun WF_TAC thms = REPEAT(FIRST1(map rtac thms))
    2.76 - val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, wf_less_than, 
    2.77 -                    wf_trancl];
    2.78 +fun tgoal thy = tgoalw thy [];
    2.79  
    2.80 - val terminator = simp_tac(!simpset addsimps [less_Suc_eq]) 1
    2.81 -                  THEN TRY(best_tac
    2.82 -                           (!claset addSDs [not0_implies_Suc]
    2.83 -                                    addss (!simpset)) 1);
    2.84 -
    2.85 - val simpls = [less_eq RS eq_reflection,
    2.86 -               lex_prod_def, measure_def, inv_image_def];
    2.87 +(*---------------------------------------------------------------------------
    2.88 +* Three postprocessors are applied to the definition.  It
    2.89 +* attempts to prove wellfoundedness of the given relation, simplifies the
    2.90 +* non-proved termination conditions, and finally attempts to prove the 
    2.91 +* simplified termination conditions.
    2.92 +*--------------------------------------------------------------------------*)
    2.93 +fun std_postprocessor ss =
    2.94 +  Prim.postprocess
    2.95 +   {WFtac      = REPEAT (ares_tac [wf_measure, wf_inv_image, wf_lex_prod, 
    2.96 +				   wf_less_than, wf_trancl] 1),
    2.97 +    terminator = asm_simp_tac ss 1
    2.98 +		 THEN TRY(best_tac
    2.99 +			  (!claset addSDs [not0_implies_Suc] addss ss) 1),
   2.100 +    simplifier = Rules.simpl_conv ss []};
   2.101  
   2.102 - (*---------------------------------------------------------------------------
   2.103 -  * Does some standard things with the termination conditions of a definition:
   2.104 -  * attempts to prove wellfoundedness of the given relation; simplifies the
   2.105 -  * non-proven termination conditions; and finally attempts to prove the 
   2.106 -  * simplified termination conditions.
   2.107 -  *--------------------------------------------------------------------------*)
   2.108 - val std_postprocessor = Prim.postprocess{WFtac = WFtac,
   2.109 -                                    terminator = terminator, 
   2.110 -                                    simplifier = Rules.simpl_conv simpls};
   2.111 -
   2.112 - val simplifier = rewrite_rule (simpls @ #simps(rep_ss (!simpset)) @ 
   2.113 -                                [pred_list_def]);
   2.114 -
   2.115 - fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));
   2.116 +fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));
   2.117  
   2.118  
   2.119  val concl = #2 o Rules.dest_thm;
   2.120 @@ -111,17 +88,14 @@
   2.121  fun define_i thy fid R eqs = 
   2.122    let val dummy = require_thy thy "WF_Rel" "recursive function definitions"
   2.123        val {functional,pats} = Prim.mk_functional thy eqs
   2.124 -      val (thm,thry) = Prim.wfrec_definition0 thy fid R functional
   2.125 -  in (thry,(thm,pats))
   2.126 +  in (Prim.wfrec_definition0 thy fid R functional, pats)
   2.127    end;
   2.128  
   2.129  (*lcp's version: takes strings; doesn't return "thm" 
   2.130          (whose signature is a draft and therefore useless) *)
   2.131  fun define thy fid R eqs = 
   2.132    let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[])) 
   2.133 -      val (thy',(_,pats)) =
   2.134 -             define_i thy fid (read thy R) (map (read thy) eqs)
   2.135 -  in  (thy',pats)  end
   2.136 +  in  define_i thy fid (read thy R) (map (read thy) eqs)  end
   2.137    handle Utils.ERR {mesg,...} => error mesg;
   2.138  
   2.139  (*---------------------------------------------------------------------------
   2.140 @@ -147,8 +121,9 @@
   2.141       Const("==",_)$_$_ => r
   2.142    |   _$(Const("op =",_)$_$_) => r RS eq_reflection
   2.143    |   _ => r RS P_imp_P_eq_True
   2.144 +
   2.145 +(*Is this the best way to invoke the simplifier??*)
   2.146  fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L))
   2.147 -fun reducer thl = rewrite (map standard thl @ #simps(rep_ss (!simpset)))
   2.148  
   2.149  fun join_assums th = 
   2.150    let val {sign,...} = rep_thm th
   2.151 @@ -164,17 +139,12 @@
   2.152    end
   2.153    val gen_all = S.gen_all
   2.154  in
   2.155 -(*---------------------------------------------------------------------------
   2.156 - * The "reducer" argument is 
   2.157 - *  (fn thl => rewrite (map standard thl @ #simps(rep_ss (!simpset)))); 
   2.158 - *---------------------------------------------------------------------------*)
   2.159 -fun proof_stage theory reducer {f, R, rules, full_pats_TCs, TCs} =
   2.160 +fun proof_stage ss theory {f, R, rules, full_pats_TCs, TCs} =
   2.161    let val dummy = prs "Proving induction theorem..  "
   2.162        val ind = Prim.mk_induction theory f R full_pats_TCs
   2.163 -      val dummy = writeln "Proved induction theorem."
   2.164 -      val pp = std_postprocessor theory
   2.165 -      val dummy = prs "Postprocessing..  "
   2.166 -      val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs}
   2.167 +      val dummy = prs "Proved induction theorem.\nPostprocessing..  "
   2.168 +      val {rules, induction, nested_tcs} = 
   2.169 +	  std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs}
   2.170    in
   2.171    case nested_tcs
   2.172    of [] => (writeln "Postprocessing done.";
   2.173 @@ -186,8 +156,9 @@
   2.174                       if (solved th) then (th::So, Si, St) 
   2.175                       else (So, th::Si, St)) nested_tcs ([],[],[])
   2.176                val simplified' = map join_assums simplified
   2.177 -              val induction' = reducer (solved@simplified') induction
   2.178 -              val rules' = reducer (solved@simplified') rules
   2.179 +              val rewr = rewrite (solved @ simplified' @ #simps(rep_ss ss))
   2.180 +              val induction' = rewr induction
   2.181 +              and rules'     = rewr rules
   2.182                val dummy = writeln "Postprocessing done."
   2.183            in
   2.184            {induction = induction',
   2.185 @@ -212,18 +183,20 @@
   2.186  (*Strip off the outer !P*)
   2.187  val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
   2.188  
   2.189 +val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def];
   2.190  
   2.191 -fun simplify_defn (thy,(id,pats)) =
   2.192 +fun simplify_defn ss (thy,(id,pats)) =
   2.193     let val dummy = deny (id  mem  map ! (stamps_of_thy thy))
   2.194                          ("Recursive definition " ^ id ^ 
   2.195                           " would clash with the theory of the same name!")
   2.196 -       val def = freezeT(get_def thy id  RS  meta_eq_to_obj_eq)
   2.197 +       val def =  freezeT(get_def thy id)   RS   meta_eq_to_obj_eq
   2.198 +       val ss' = ss addsimps ((less_Suc_eq RS iffD2) :: wf_rel_defs)
   2.199         val {theory,rules,TCs,full_pats_TCs,patterns} = 
   2.200 -                Prim.post_definition (thy,(def,pats))
   2.201 +                Prim.post_definition ss' (thy,(def,pats))
   2.202         val {lhs=f,rhs} = S.dest_eq(concl def)
   2.203         val (_,[R,_]) = S.strip_comb rhs
   2.204         val {induction, rules, tcs} = 
   2.205 -             proof_stage theory reducer
   2.206 +             proof_stage ss' theory 
   2.207                 {f = f, R = R, rules = rules,
   2.208                  full_pats_TCs = full_pats_TCs,
   2.209                  TCs = TCs}
   2.210 @@ -235,8 +208,7 @@
   2.211     end
   2.212    handle Utils.ERR {mesg,func,module} => 
   2.213                 error (mesg ^ 
   2.214 -		      "\n    (In TFL function " ^ module ^ "." ^ func ^ ")")
   2.215 -       |  e => print_exn e;
   2.216 +		      "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");
   2.217  end;
   2.218  
   2.219  (*---------------------------------------------------------------------------
   2.220 @@ -260,7 +232,6 @@
   2.221   in {theory = theory, 
   2.222       eq_ind = standard (induction RS (rules RS conjI))}
   2.223   end
   2.224 - handle    e              => print_exn e
   2.225  end;
   2.226  
   2.227  
     3.1 --- a/TFL/rules.new.sml	Thu Jun 05 13:26:09 1997 +0200
     3.2 +++ b/TFL/rules.new.sml	Thu Jun 05 13:27:28 1997 +0200
     3.3 @@ -282,19 +282,6 @@
     3.4    end;
     3.5  
     3.6  
     3.7 -local fun string_of(s,_) = s
     3.8 -in
     3.9 -fun freeze th =
    3.10 -  let val fth = freezeT th
    3.11 -      val {prop,sign,...} = rep_thm fth
    3.12 -      fun mk_inst (Var(v,T)) = 
    3.13 -          (cterm_of sign (Var(v,T)),
    3.14 -           cterm_of sign (Free(string_of v, T)))
    3.15 -      val insts = map mk_inst (term_vars prop)
    3.16 -  in  instantiate ([],insts) fth  
    3.17 -  end
    3.18 -end;
    3.19 -
    3.20  fun MATCH_MP th1 th2 = 
    3.21     if (D.is_forall (D.drop_prop(cconcl th1)))
    3.22     then MATCH_MP (th1 RS spec) th2
    3.23 @@ -326,8 +313,8 @@
    3.24  fun CHOOSE(fvar,exth) fact =
    3.25     let val lam = #2(dest_comb(D.drop_prop(cconcl exth)))
    3.26         val redex = capply lam fvar
    3.27 -       val {sign,t,...} = rep_cterm redex
    3.28 -       val residue = cterm_of sign (S.beta_conv t)
    3.29 +       val {sign, t = t$u,...} = rep_cterm redex
    3.30 +       val residue = cterm_of sign (betapply(t,u))
    3.31      in GEN fvar (DISCH residue fact)  RS (exth RS choose_thm)
    3.32     end
    3.33  end;
    3.34 @@ -403,12 +390,10 @@
    3.35  fun SUBS thl = 
    3.36     rewrite_rule (map (fn th => (th RS eq_reflection) handle _ => th) thl);
    3.37  
    3.38 -val simplify = rewrite_rule;
    3.39 -
    3.40  local fun rew_conv mss = rewrite_cterm (true,false) mss (K(K None))
    3.41  in
    3.42 -fun simpl_conv thl ctm = 
    3.43 - rew_conv (Thm.mss_of (#simps(rep_ss (!simpset))@thl)) ctm
    3.44 +fun simpl_conv ss thl ctm = 
    3.45 + rew_conv (Thm.mss_of (#simps(rep_ss ss)@thl)) ctm
    3.46   RS meta_eq_to_obj_eq
    3.47  end;
    3.48  
    3.49 @@ -449,13 +434,6 @@
    3.50  
    3.51  fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
    3.52  
    3.53 -fun variants FV vlist =
    3.54 -  rev(#1(U.rev_itlist (fn v => fn (V,W) =>
    3.55 -                        let val v' = S.variant W v
    3.56 -                        in (v'::V, v'::W) end) 
    3.57 -                     vlist ([],FV)));
    3.58 -
    3.59 -
    3.60  fun dest_all(Const("all",_) $ (a as Abs _)) = S.dest_abs a
    3.61    | dest_all _ = raise RULES_ERR{func = "dest_all", mesg = "not a !!"};
    3.62  
    3.63 @@ -501,8 +479,8 @@
    3.64              let val eq = Logic.strip_imp_concl body
    3.65                  val (f,args) = S.strip_comb (get_lhs eq)
    3.66                  val (vstrl,_) = S.strip_abs f
    3.67 -                val names  = map (#1 o dest_Free)
    3.68 -                                 (variants (term_frees body) vstrl)
    3.69 +                val names  = variantlist (map (#1 o dest_Free) vstrl,
    3.70 +					  add_term_names(body, []))
    3.71              in get (rst, n+1, (names,n)::L)
    3.72              end handle _ => get (rst, n+1, L);
    3.73  
    3.74 @@ -648,12 +626,13 @@
    3.75    in (ants,get_lhs eq)
    3.76    end;
    3.77  
    3.78 -val pbeta_reduce = simpl_conv [split RS eq_reflection];
    3.79 -val restricted = U.can(S.find_term
    3.80 -                       (U.holds(fn c => (#Name(S.dest_const c)="cut"))))
    3.81 +fun restricted t = is_some (S.find_term
    3.82 +			    (fn (Const("cut",_)) =>true | _ => false) 
    3.83 +			    t)
    3.84  
    3.85 -fun CONTEXT_REWRITE_RULE(func,R){cut_lemma, congs, th} =
    3.86 - let val tc_list = ref[]: term list ref
    3.87 +fun CONTEXT_REWRITE_RULE (ss, func, R, cut_lemma, congs) th =
    3.88 + let val pbeta_reduce = simpl_conv ss [split RS eq_reflection];
    3.89 +     val tc_list = ref[]: term list ref
    3.90       val dummy = term_ref := []
    3.91       val dummy = thm_ref  := []
    3.92       val dummy = mss_ref  := []
    3.93 @@ -761,11 +740,9 @@
    3.94                 * term "f v1..vn" which is a pattern that any full application
    3.95                 * of "f" will match.
    3.96                 *-------------------------------------------------------------*)
    3.97 -              val func_name = #1(dest_Const func handle _ => dest_Free func)
    3.98 -              fun is_func tm = (#1(dest_Const tm handle _ => dest_Free tm) 
    3.99 -				= func_name)
   3.100 -                               handle _ => false
   3.101 -              val nested = U.can(S.find_term is_func)
   3.102 +              val func_name = #1(dest_Const func)
   3.103 +              fun is_func (Const (name,_)) = (name = func_name)
   3.104 +		| is_func _                = false
   3.105                val rcontext = rev cntxt
   3.106                val cncl = HOLogic.dest_Trueprop o #prop o rep_thm
   3.107                val antl = case rcontext of [] => [] 
   3.108 @@ -775,7 +752,7 @@
   3.109                val dummy = print_cterms "TC:\n" 
   3.110  		              [cterm_of sign (HOLogic.mk_Trueprop TC)]
   3.111                val dummy = tc_list := (TC :: !tc_list)
   3.112 -              val nestedp = nested TC
   3.113 +              val nestedp = is_some (S.find_term is_func TC)
   3.114                val dummy = if nestedp then say"nested\n" else say"not_nested\n"
   3.115                val dummy = term_ref := ([func,TC]@(!term_ref))
   3.116                val th' = if nestedp then raise RULES_ERR{func = "solver", 
   3.117 @@ -803,12 +780,8 @@
   3.118  
   3.119  
   3.120  
   3.121 -fun prove (tm,tac) = 
   3.122 -  let val {t,sign,...} = rep_cterm tm
   3.123 -      val ptm = cterm_of sign(HOLogic.mk_Trueprop t)
   3.124 -  in
   3.125 -  freeze(prove_goalw_cterm [] ptm (fn _ => [tac]))
   3.126 -  end;
   3.127 +fun prove (ptm,tac) = 
   3.128 +    #1 (freeze_thaw (prove_goalw_cterm [] ptm (fn _ => [tac])));
   3.129  
   3.130  
   3.131  end; (* Rules *)
     4.1 --- a/TFL/rules.sig	Thu Jun 05 13:26:09 1997 +0200
     4.2 +++ b/TFL/rules.sig	Thu Jun 05 13:27:28 1997 +0200
     4.3 @@ -46,17 +46,15 @@
     4.4    val DISJ_CASESL : thm -> thm list -> thm
     4.5  
     4.6    val SUBS : thm list -> thm -> thm
     4.7 -  val simplify : thm list -> thm -> thm
     4.8 -  val simpl_conv : thm list -> cterm -> thm
     4.9 +  val simpl_conv : simpset -> thm list -> cterm -> thm
    4.10  
    4.11  (* For debugging my isabelle solver in the conditional rewriter *)
    4.12    val term_ref : term list ref
    4.13    val thm_ref : thm list ref
    4.14    val mss_ref : meta_simpset list ref
    4.15    val tracing :bool ref
    4.16 -  val CONTEXT_REWRITE_RULE : term * term
    4.17 -                             -> {cut_lemma:thm, congs: thm list, th:thm} 
    4.18 -                             -> thm * term list
    4.19 +  val CONTEXT_REWRITE_RULE : simpset * term * term * thm * thm list 
    4.20 +                             -> thm -> thm * term list
    4.21    val RIGHT_ASSOC : thm -> thm 
    4.22  
    4.23    val prove : cterm * tactic -> thm
     5.1 --- a/TFL/tfl.sig	Thu Jun 05 13:26:09 1997 +0200
     5.2 +++ b/TFL/tfl.sig	Thu Jun 05 13:27:28 1997 +0200
     5.3 @@ -15,23 +15,22 @@
     5.4                         -> {functional:term,
     5.5                             pats: pattern list}
     5.6  
     5.7 -   val wfrec_definition0 : theory -> string -> term -> term -> thm * theory
     5.8 +   val wfrec_definition0 : theory -> string -> term -> term -> theory
     5.9  
    5.10 -   val post_definition : theory * (thm * pattern list)
    5.11 -                              -> {theory : theory,
    5.12 -                                  rules  : thm, 
    5.13 -                                    TCs  : term list list,
    5.14 -                          full_pats_TCs  : (term * term list) list, 
    5.15 -                               patterns  : pattern list}
    5.16 +   val post_definition : simpset -> theory * (thm * pattern list)
    5.17 +				 -> {theory : theory,
    5.18 +				     rules  : thm, 
    5.19 +				       TCs  : term list list,
    5.20 +			     full_pats_TCs  : (term * term list) list, 
    5.21 +				  patterns  : pattern list}
    5.22  
    5.23 -
    5.24 +(*CURRENTLY UNUSED
    5.25     val wfrec_eqns : theory -> term list
    5.26                       -> {WFR : term, 
    5.27                           proto_def : term,
    5.28                           extracta :(thm * term list) list,
    5.29                           pats  : pattern list}
    5.30  
    5.31 -
    5.32     val lazyR_def : theory
    5.33                     -> term list
    5.34                     -> {theory:theory,
    5.35 @@ -39,11 +38,9 @@
    5.36                             R :term,
    5.37                         full_pats_TCs :(term * term list) list, 
    5.38                         patterns: pattern list}
    5.39 +---------------------*)
    5.40  
    5.41 -   val mk_induction : theory 
    5.42 -                       -> term -> term 
    5.43 -                         -> (term * term list) list
    5.44 -                           -> thm
    5.45 +   val mk_induction : theory -> term -> term -> (term * term list) list -> thm
    5.46  
    5.47     val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm}
    5.48                       -> theory 
     6.1 --- a/TFL/tfl.sml	Thu Jun 05 13:26:09 1997 +0200
     6.2 +++ b/TFL/tfl.sml	Thu Jun 05 13:27:28 1997 +0200
     6.3 @@ -43,12 +43,12 @@
     6.4   * proof of completeness of cases for the induction theorem.
     6.5   *
     6.6   * The curried function "gvvariant" returns a function to generate distinct
     6.7 - * variables that are guaranteed not to be in vlist.  The names of
     6.8 + * variables that are guaranteed not to be in names.  The names of
     6.9   * the variables go u, v, ..., z, aa, ..., az, ...  The returned 
    6.10   * function contains embedded refs!
    6.11   *---------------------------------------------------------------------------*)
    6.12 -fun gvvariant vlist =
    6.13 -  let val slist = ref (map (#1 o dest_Free) vlist)
    6.14 +fun gvvariant names =
    6.15 +  let val slist = ref names
    6.16        val vname = ref "u"
    6.17        fun new() = 
    6.18           if !vname mem_string (!slist)
    6.19 @@ -189,10 +189,10 @@
    6.20   * incomplete set of patterns is given.
    6.21   *---------------------------------------------------------------------------*)
    6.22  
    6.23 -fun mk_case ty_info ty_match FV range_ty =
    6.24 +fun mk_case ty_info ty_match usednames range_ty =
    6.25   let 
    6.26   fun mk_case_fail s = raise TFL_ERR{func = "mk_case", mesg = s}
    6.27 - val fresh_var = gvvariant FV 
    6.28 + val fresh_var = gvvariant usednames 
    6.29   val divide = partition fresh_var ty_match
    6.30   fun expand constructors ty ((_,[]), _) = mk_case_fail"expand_var_row"
    6.31     | expand constructors ty (row as ((prefix, p::rst), rhs)) = 
    6.32 @@ -285,19 +285,18 @@
    6.33   let val (L,R) = ListPair.unzip 
    6.34                      (map (fn (Const("op =",_) $ t $ u) => (t,u)) clauses)
    6.35       val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
    6.36 -     val f = single (gen_distinct (op aconv) funcs)
    6.37 -     (**??why change the Const to a Free??????????????**)
    6.38 -     val fvar = if (is_Free f) then f else Free(dest_Const f)
    6.39 +     val fcon as Const (fname, ftype) = single (gen_distinct (op aconv) funcs)
    6.40       val dummy = map (no_repeat_vars thy) pats
    6.41       val rows = ListPair.zip (map (fn x => ([],[x])) pats,
    6.42                                map GIVEN (enumerate R))
    6.43 -     val fvs = S.free_varsl R
    6.44 -     val a = S.variant fvs (Free("a",type_of(hd pats)))
    6.45 -     val FV = a::fvs
    6.46 +     val names = foldr add_term_names (R,[])
    6.47 +     val atype = type_of(hd pats)
    6.48 +     and aname = variant names "a"
    6.49 +     val a = Free(aname,atype)
    6.50       val ty_info = Thry.match_info thy
    6.51       val ty_match = Thry.match_type thy
    6.52       val range_ty = type_of (hd R)
    6.53 -     val (patts, case_tm) = mk_case ty_info ty_match FV range_ty 
    6.54 +     val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty 
    6.55                                      {path=[a], rows=rows}
    6.56       val patts1 = map (fn (_,(tag,i),[pat]) => tag (pat,i)) patts 
    6.57  	  handle _ => mk_functional_err "error in pattern-match translation"
    6.58 @@ -308,8 +307,9 @@
    6.59               of [] => ()
    6.60            | L => mk_functional_err("The following rows (counting from zero)\
    6.61                                     \ are inaccessible: "^stringize L)
    6.62 -     val case_tm' = subst_free [(f,fvar)] case_tm
    6.63 - in {functional = S.list_mk_abs ([fvar,a], case_tm'),
    6.64 + in {functional = Abs(fname, ftype, 
    6.65 +		      abstract_over (fcon, 
    6.66 +				     absfree(aname,atype, case_tm))),
    6.67       pats = patts2}
    6.68  end end;
    6.69  
    6.70 @@ -326,10 +326,6 @@
    6.71    | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
    6.72    | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
    6.73  
    6.74 -
    6.75 -(*---------------------------------------------------------------------------
    6.76 - * R is already assumed to be type-copacetic with M
    6.77 - *---------------------------------------------------------------------------*)
    6.78  local val f_eq_wfrec_R_M = 
    6.79             #ant(S.dest_imp(#2(S.strip_forall (concl Thms.WFREC_COROLLARY))))
    6.80        val {lhs=f, rhs} = S.dest_eq f_eq_wfrec_R_M
    6.81 @@ -348,12 +344,9 @@
    6.82  	              $ functional
    6.83       val (_, def_term, _) = 
    6.84  	 Sign.infer_types (sign_of thy) (K None) (K None) [] false
    6.85 -	       ([HOLogic.mk_eq(Const(Name,Ty), wfrec_R_M)], 
    6.86 -		HOLogic.boolT)
    6.87 -		    
    6.88 -  in 
    6.89 -  Thry.make_definition thy def_name def_term
    6.90 -  end
    6.91 +	       ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], 
    6.92 +		propT)
    6.93 +  in  add_defs_i [(def_name, def_term)] thy  end
    6.94  end;
    6.95  
    6.96  
    6.97 @@ -396,15 +389,11 @@
    6.98  end;
    6.99  
   6.100  
   6.101 -(*Replace all TFrees by TVars [CURRENTLY UNUSED]*)
   6.102 -val tvars_of_tfrees = 
   6.103 -    map_term_types (map_type_tfree (fn (a,sort) => TVar ((a, 0), sort)));
   6.104 -
   6.105  fun givens [] = []
   6.106    | givens (GIVEN(tm,_)::pats) = tm :: givens pats
   6.107    | givens (OMITTED _::pats)   = givens pats;
   6.108  
   6.109 -fun post_definition (theory, (def, pats)) =
   6.110 +fun post_definition ss (theory, (def, pats)) =
   6.111   let val tych = Thry.typecheck theory 
   6.112       val f = #lhs(S.dest_eq(concl def))
   6.113       val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
   6.114 @@ -415,14 +404,14 @@
   6.115       val corollaries = map (fn pat => R.SPEC (tych pat) corollary') 
   6.116  	                   given_pats
   6.117       val (case_rewrites,context_congs) = extraction_thms theory
   6.118 -     val corollaries' = map(R.simplify case_rewrites) corollaries
   6.119 -     fun xtract th = R.CONTEXT_REWRITE_RULE(f,R)
   6.120 -                         {cut_lemma = R.ISPECL (map tych [f,R]) Thms.CUT_LEMMA,
   6.121 -			  congs = context_congs,
   6.122 -			  th = th}
   6.123 -     val (rules, TCs) = ListPair.unzip (map xtract corollaries')
   6.124 -     val rules0 = map (R.simplify [Thms.CUT_DEF]) rules
   6.125 -     val mk_cond_rule = R.FILTER_DISCH_ALL(not o S.aconv WFR)
   6.126 +     val corollaries' = map(rewrite_rule case_rewrites) corollaries
   6.127 +     val extract = R.CONTEXT_REWRITE_RULE 
   6.128 +	             (ss, f, R,
   6.129 +		      R.ISPECL (map tych [f,R]) Thms.CUT_LEMMA,
   6.130 +		      context_congs)
   6.131 +     val (rules, TCs) = ListPair.unzip (map extract corollaries')
   6.132 +     val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
   6.133 +     val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
   6.134       val rules1 = R.LIST_CONJ(map mk_cond_rule rules0)
   6.135   in
   6.136   {theory = theory,   (* holds def, if it's needed *)
   6.137 @@ -437,8 +426,8 @@
   6.138   * Perform the extraction without making the definition. Definition and
   6.139   * extraction commute for the non-nested case. For hol90 users, this 
   6.140   * function can be invoked without being in draft mode.
   6.141 - *---------------------------------------------------------------------------*)
   6.142 -fun wfrec_eqns thy eqns =
   6.143 + * CURRENTLY UNUSED
   6.144 +fun wfrec_eqns ss thy eqns =
   6.145   let val {functional,pats} = mk_functional thy eqns
   6.146       val given_pats = givens pats
   6.147       val {Bvar = f, Body} = S.dest_abs functional
   6.148 @@ -447,23 +436,25 @@
   6.149       val (case_rewrites,context_congs) = extraction_thms thy
   6.150       val tych = Thry.typecheck thy
   6.151       val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
   6.152 -     val R = S.variant(foldr add_term_frees (eqns,[])) 
   6.153 -                      (#Bvar(S.dest_forall(concl WFREC_THM0)))
   6.154 +     val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
   6.155 +     val R = Free (variant (foldr add_term_names (eqns,[])) Rname,
   6.156 +		   Rtype)
   6.157       val WFREC_THM = R.ISPECL [tych R, tych f] WFREC_THM0
   6.158       val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
   6.159       val R1 = S.rand WFR
   6.160       val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
   6.161 -     val corollaries = map (U.C R.SPEC corollary' o tych) given_pats
   6.162 -     val corollaries' = map (R.simplify case_rewrites) corollaries
   6.163 -     fun extract th = R.CONTEXT_REWRITE_RULE(f,R1)
   6.164 -                        {cut_lemma = R.ISPECL (map tych [f,R1]) Thms.CUT_LEMMA,
   6.165 -			 congs = context_congs,
   6.166 -			 th  = th}
   6.167 +     val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats
   6.168 +     val corollaries' = map (rewrite_rule case_rewrites) corollaries
   6.169 +     val extract = R.CONTEXT_REWRITE_RULE 
   6.170 +	               (ss, f, R1, 
   6.171 +		        R.ISPECL (map tych [f,R1]) Thms.CUT_LEMMA, 
   6.172 +			context_congs)
   6.173   in {proto_def=proto_def, 
   6.174       WFR=WFR, 
   6.175       pats=pats,
   6.176       extracta = map extract corollaries'}
   6.177   end;
   6.178 + *---------------------------------------------------------------------------*)
   6.179  
   6.180  
   6.181  (*---------------------------------------------------------------------------
   6.182 @@ -471,9 +462,9 @@
   6.183   * wellfounded relation used in the definition is computed by using the
   6.184   * choice operator on the extracted conditions (plus the condition that
   6.185   * such a relation must be wellfounded).
   6.186 - *---------------------------------------------------------------------------*)
   6.187 -fun lazyR_def thy eqns =
   6.188 - let val {proto_def,WFR,pats,extracta} = wfrec_eqns thy eqns
   6.189 + * CURRENTLY UNUSED
   6.190 +fun lazyR_def ss thy eqns =
   6.191 + let val {proto_def,WFR,pats,extracta} = wfrec_eqns ss thy eqns
   6.192       val R1 = S.rand WFR
   6.193       val f = S.lhs proto_def
   6.194       val (Name,_) = dest_Free f
   6.195 @@ -482,8 +473,9 @@
   6.196       val full_rqt = WFR::TCs
   6.197       val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
   6.198       val R'abs = S.rand R'
   6.199 -     val (def,theory) = Thry.make_definition thy (Name ^ "_def") 
   6.200 -                                               (subst_free[(R1,R')] proto_def)
   6.201 +     val theory = add_defs_i [(Name ^ "_def", subst_free[(R1,R')] proto_def)]
   6.202 +	                     thy
   6.203 +     val def = freezeT((get_axiom theory (Name ^ "_def")) RS meta_eq_to_obj_eq)
   6.204       val fconst = #lhs(S.dest_eq(concl def)) 
   6.205       val tych = Thry.typecheck theory
   6.206       val baz = R.DISCH (tych proto_def)
   6.207 @@ -499,6 +491,7 @@
   6.208       full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
   6.209       patterns = pats}
   6.210   end;
   6.211 + *---------------------------------------------------------------------------*)
   6.212  
   6.213  
   6.214  
   6.215 @@ -535,10 +528,10 @@
   6.216        val args = map (fn qv => the (gen_assoc (op aconv) (plist, qv))) qvars
   6.217                     handle OPTION _ => error 
   6.218                         "TFL fault [alpha_ex_unroll]: no correspondence"
   6.219 -      fun build ex [] = []
   6.220 -        | build ex (v::rst) =
   6.221 -           let val ex1 = S.beta_conv(S.mk_comb{Rator=S.rand ex, Rand=v})
   6.222 -           in ex1::build ex1 rst
   6.223 +      fun build ex      []   = []
   6.224 +        | build (_$rex) (v::rst) =
   6.225 +           let val ex1 = betapply(rex, v)
   6.226 +           in  ex1 :: build ex1 rst
   6.227             end
   6.228       val (nex::exl) = rev (tm::build tm args)
   6.229    in 
   6.230 @@ -553,9 +546,9 @@
   6.231   *
   6.232   *---------------------------------------------------------------------------*)
   6.233  
   6.234 -fun mk_case ty_info FV thy =
   6.235 +fun mk_case ty_info usednames thy =
   6.236   let 
   6.237 - val divide = ipartition (gvvariant FV)
   6.238 + val divide = ipartition (gvvariant usednames)
   6.239   val tych = Thry.typecheck thy
   6.240   fun tych_binding(x,y) = (tych x, tych y)
   6.241   fun fail s = raise TFL_ERR{func = "mk_case", mesg = s}
   6.242 @@ -608,11 +601,12 @@
   6.243   let val tych = Thry.typecheck thy
   6.244       val ty_info = Thry.induct_info thy
   6.245   in fn pats =>
   6.246 - let val FV0 = S.free_varsl pats
   6.247 + let val names = foldr add_term_names (pats,[])
   6.248       val T = type_of (hd pats)
   6.249 -     val a = S.variant FV0 (Free ("a", T))
   6.250 -     val v = S.variant (a::FV0) (Free ("v", T))
   6.251 -     val FV = a::v::FV0
   6.252 +     val aname = Term.variant names "a"
   6.253 +     val vname = Term.variant (aname::names) "v"
   6.254 +     val a = Free (aname, T)
   6.255 +     val v = Free (vname, T)
   6.256       val a_eq_v = HOLogic.mk_eq(a,v)
   6.257       val ex_th0 = R.EXISTS (tych (S.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
   6.258                             (R.REFL (tych a))
   6.259 @@ -622,7 +616,8 @@
   6.260   R.GEN (tych a) 
   6.261         (R.RIGHT_ASSOC
   6.262            (R.CHOOSE(tych v, ex_th0)
   6.263 -                (mk_case ty_info FV thy {path=[v], rows=rows})))
   6.264 +                (mk_case ty_info (vname::aname::names)
   6.265 +		 thy {path=[v], rows=rows})))
   6.266   end end;
   6.267  
   6.268  
   6.269 @@ -636,29 +631,28 @@
   6.270   * Note. When the context is empty, there can be no local variables.
   6.271   *---------------------------------------------------------------------------*)
   6.272  
   6.273 -local nonfix ^ ;   infix 9 ^  ;     infix 5 ==>
   6.274 -      fun (tm1 ^ tm2)   = S.mk_comb{Rator = tm1, Rand = tm2}
   6.275 +local infix 5 ==>
   6.276        fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
   6.277  in
   6.278  fun build_ih f P (pat,TCs) = 
   6.279   let val globals = S.free_vars_lr pat
   6.280 -     fun nested tm = U.can(S.find_term (S.aconv f)) tm handle _ => false
   6.281 +     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
   6.282       fun dest_TC tm = 
   6.283           let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
   6.284               val (R,y,_) = S.dest_relation R_y_pat
   6.285 -             val P_y = if (nested tm) then R_y_pat ==> P^y else P^y
   6.286 +             val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
   6.287           in case cntxt 
   6.288                of [] => (P_y, (tm,[]))
   6.289                 | _  => let 
   6.290                      val imp = S.list_mk_conj cntxt ==> P_y
   6.291                      val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals)
   6.292 -                    val locals = #2(U.pluck (S.aconv P) lvs) handle _ => lvs
   6.293 +                    val locals = #2(U.pluck (curry (op aconv) P) lvs) handle _ => lvs
   6.294                      in (S.list_mk_forall(locals,imp), (tm,locals)) end
   6.295           end
   6.296   in case TCs
   6.297 -    of [] => (S.list_mk_forall(globals, P^pat), [])
   6.298 +    of [] => (S.list_mk_forall(globals, P$pat), [])
   6.299       |  _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
   6.300 -                 val ind_clause = S.list_mk_conj ihs ==> P^pat
   6.301 +                 val ind_clause = S.list_mk_conj ihs ==> P$pat
   6.302               in (S.list_mk_forall(globals,ind_clause), TCs_locals)
   6.303               end
   6.304   end
   6.305 @@ -678,7 +672,7 @@
   6.306   let val tych = Thry.typecheck thy
   6.307       val antc = tych(#ant(S.dest_imp tm))
   6.308       val thm' = R.SPEC_ALL thm
   6.309 -     fun nested tm = U.can(S.find_term (S.aconv f)) tm handle _ => false
   6.310 +     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
   6.311       fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC)))))
   6.312       fun mk_ih ((TC,locals),th2,nested) =
   6.313           R.GENL (map tych locals)
   6.314 @@ -723,9 +717,6 @@
   6.315    in  #2 (U.itlist CHOOSER L (veq,thm))  end;
   6.316  
   6.317  
   6.318 -fun combize M N = S.mk_comb{Rator=M,Rand=N};
   6.319 -
   6.320 -
   6.321  (*----------------------------------------------------------------------------
   6.322   * Input : f, R,  and  [(pat1,TCs1),..., (patn,TCsn)]
   6.323   *
   6.324 @@ -739,18 +730,20 @@
   6.325      val (pats,TCsl) = ListPair.unzip pat_TCs_list
   6.326      val case_thm = complete_cases thy pats
   6.327      val domain = (type_of o hd) pats
   6.328 -    val P = S.variant (S.all_varsl (pats @ List_.concat TCsl))
   6.329 -                      (Free("P",domain --> HOLogic.boolT))
   6.330 +    val Pname = Term.variant (foldr (foldr add_term_names) 
   6.331 +			      (pats::TCsl, [])) "P"
   6.332 +    val P = Free(Pname, domain --> HOLogic.boolT)
   6.333      val Sinduct = R.SPEC (tych P) Sinduction
   6.334      val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct)
   6.335      val Rassums_TCl' = map (build_ih f P) pat_TCs_list
   6.336      val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
   6.337      val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
   6.338 -    val cases = map (S.beta_conv o combize Sinduct_assumf) pats
   6.339 +    val cases = map (fn pat => betapply (Sinduct_assumf, pat)) pats
   6.340      val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
   6.341      val proved_cases = map (prove_case f thy) tasks
   6.342 -    val v = S.variant (S.free_varsl (map concl proved_cases))
   6.343 -                      (Free("v",domain))
   6.344 +    val v = Free (variant (foldr add_term_names (map concl proved_cases, []))
   6.345 +		    "v",
   6.346 +		  domain)
   6.347      val vtyped = tych v
   6.348      val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
   6.349      val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]th') 
   6.350 @@ -759,7 +752,7 @@
   6.351      val dant = R.GEN vtyped (R.DISJ_CASESL (R.ISPEC vtyped case_thm) abs_cases)
   6.352      val dc = R.MP Sinduct dant
   6.353      val Parg_ty = type_of(#Bvar(S.dest_forall(concl dc)))
   6.354 -    val vars = map (gvvariant[P]) (S.strip_prod_type Parg_ty)
   6.355 +    val vars = map (gvvariant[Pname]) (S.strip_prod_type Parg_ty)
   6.356      val dc' = U.itlist (R.GEN o tych) vars
   6.357                         (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc)
   6.358  in 
   6.359 @@ -809,7 +802,9 @@
   6.360      * Attempt to eliminate WF condition. It's the only assumption of rules
   6.361      *---------------------------------------------------------------------*)
   6.362     val (rules1,induction1)  = 
   6.363 -       let val thm = R.prove(tych(hd(#1(R.dest_thm rules))),WFtac)
   6.364 +       let val thm = R.prove(tych(HOLogic.mk_Trueprop 
   6.365 +				  (hd(#1(R.dest_thm rules)))),
   6.366 +			     WFtac)
   6.367         in (R.PROVE_HYP thm rules,  R.PROVE_HYP thm induction)
   6.368         end handle _ => (rules,induction)
   6.369  
   6.370 @@ -827,7 +822,8 @@
   6.371         elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
   6.372         handle _ => 
   6.373          (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
   6.374 -                            (R.prove(tych(S.rhs(concl tc_eq)),terminator)))
   6.375 +		  (R.prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))), 
   6.376 +			   terminator)))
   6.377                   (r,ind)
   6.378           handle _ => 
   6.379            (R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq), 
   6.380 @@ -854,7 +850,8 @@
   6.381         (R.MATCH_MP Thms.eqT tc_eq
   6.382          handle _
   6.383          => (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
   6.384 -                      (R.prove(tych(S.rhs(concl tc_eq)),terminator))
   6.385 +                      (R.prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))),
   6.386 +			       terminator))
   6.387              handle _ => tc_eq))
   6.388        end
   6.389  
     7.1 --- a/TFL/thry.sig	Thu Jun 05 13:26:09 1997 +0200
     7.2 +++ b/TFL/thry.sig	Thu Jun 05 13:27:28 1997 +0200
     7.3 @@ -6,7 +6,6 @@
     7.4  
     7.5  signature Thry_sig =
     7.6  sig
     7.7 -  structure USyntax : USyntax_sig
     7.8    val match_term : theory -> term -> term 
     7.9                      -> (term*term)list * (typ*typ)list
    7.10  
    7.11 @@ -14,8 +13,6 @@
    7.12  
    7.13    val typecheck : theory -> term -> cterm
    7.14  
    7.15 -  val make_definition: theory -> string -> term -> thm * theory
    7.16 -
    7.17    (* Datatype facts of various flavours *)
    7.18    val match_info: theory -> string -> {constructors:term list,
    7.19                                       case_const:term} option
     8.1 --- a/TFL/thry.sml	Thu Jun 05 13:26:09 1997 +0200
     8.2 +++ b/TFL/thry.sml	Thu Jun 05 13:27:28 1997 +0200
     8.3 @@ -7,7 +7,6 @@
     8.4  structure Thry : Thry_sig (* LThry_sig *) = 
     8.5  struct
     8.6  
     8.7 -structure USyntax  = USyntax;
     8.8  structure S = USyntax;
     8.9  
    8.10  fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
    8.11 @@ -37,55 +36,6 @@
    8.12  fun typecheck thry = cterm_of (sign_of thry);
    8.13  
    8.14  
    8.15 -
    8.16 -(*----------------------------------------------------------------------------
    8.17 - * Making a definition. The argument "tm" looks like "f = WFREC R M". This 
    8.18 - * entrypoint is specialized for interactive use, since it closes the theory
    8.19 - * after making the definition. This allows later interactive definitions to
    8.20 - * refer to previous ones. The name for the new theory is automatically 
    8.21 - * generated from the name of the argument theory.
    8.22 - *---------------------------------------------------------------------------*)
    8.23 -
    8.24 -
    8.25 -(*---------------------------------------------------------------------------
    8.26 - * TFL attempts to make definitions where the lhs is a variable. Isabelle
    8.27 - * wants it to be a constant, so here we map it to a constant. Moreover, the
    8.28 - * theory should already have the constant, so we refrain from adding the
    8.29 - * constant to the theory. We just add the axiom and return the theory.
    8.30 - *---------------------------------------------------------------------------*)
    8.31 -local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection))
    8.32 -      val Const(eeq_name, ty) = eeq
    8.33 -      val prop = body_type ty
    8.34 -in
    8.35 -fun make_definition parent s tm = 
    8.36 -   let val {lhs,rhs} = S.dest_eq tm
    8.37 -       val (_,Ty) = dest_Const lhs
    8.38 -       val eeq1 = Const(eeq_name, Ty --> Ty --> prop)
    8.39 -       val dtm = list_comb(eeq1,[lhs,rhs])      (* Rename "=" to "==" *)
    8.40 -       val (_, tm', _) = Sign.infer_types (sign_of parent)
    8.41 -                     (K None) (K None) [] true ([dtm],propT)
    8.42 -       val new_thy = add_defs_i [(s,tm')] parent
    8.43 -   in 
    8.44 -   (freezeT((get_axiom new_thy s) RS meta_eq_to_obj_eq), new_thy)
    8.45 -   end;
    8.46 -end;
    8.47 -
    8.48 -(*---------------------------------------------------------------------------
    8.49 - * Utility routine. Insert into list ordered by the key (a string). If two 
    8.50 - * keys are equal, the new element replaces the old. A more efficient option 
    8.51 - * for the future is needed. In fact, having the list of datatype facts be 
    8.52 - * ordered is useless, since the lookup should never fail!
    8.53 - *---------------------------------------------------------------------------*)
    8.54 -fun insert (el as (x:string, _)) = 
    8.55 - let fun canfind[] = [el] 
    8.56 -       | canfind(alist as ((y as (k,_))::rst)) = 
    8.57 -           if (x<k) then el::alist
    8.58 -           else if (x=k) then el::rst
    8.59 -           else y::canfind rst 
    8.60 - in canfind
    8.61 - end;
    8.62 -
    8.63 -
    8.64  (*---------------------------------------------------------------------------
    8.65   *     A collection of facts about datatypes
    8.66   *---------------------------------------------------------------------------*)
     9.1 --- a/TFL/usyntax.sig	Thu Jun 05 13:26:09 1997 +0200
     9.2 +++ b/TFL/usyntax.sig	Thu Jun 05 13:27:28 1997 +0200
     9.3 @@ -25,21 +25,14 @@
     9.4    val strip_prod_type : typ -> typ list
     9.5  
     9.6    (* Terms *)
     9.7 -  val free_varsl : term list -> term list
     9.8    val free_vars_lr : term -> term list
     9.9 -  val all_vars   : term -> term list
    9.10 -  val all_varsl  : term list -> term list
    9.11 -  val variant    : term list -> term -> term
    9.12    val type_vars_in_term : term -> typ list
    9.13    val dest_term  : term -> lambda
    9.14    
    9.15    (* Prelogic *)
    9.16 -  val aconv     : term -> term -> bool
    9.17    val inst      : (typ*typ) list -> term -> term
    9.18 -  val beta_conv : term -> term
    9.19  
    9.20    (* Construction routines *)
    9.21 -  val mk_comb   :{Rator : term, Rand : term} -> term
    9.22    val mk_abs    :{Bvar  : term, Body : term} -> term
    9.23  
    9.24    val mk_imp    :{ant : term, conseq :  term} -> term
    9.25 @@ -66,14 +59,9 @@
    9.26  
    9.27    val lhs   : term -> term
    9.28    val rhs   : term -> term
    9.29 -  val rator : term -> term
    9.30    val rand  : term -> term
    9.31 -  val bvar  : term -> term
    9.32 -  val body  : term -> term
    9.33 -  
    9.34  
    9.35    (* Query routines *)
    9.36 -  val is_eq     : term -> bool
    9.37    val is_imp    : term -> bool
    9.38    val is_forall : term -> bool 
    9.39    val is_exists : term -> bool 
    9.40 @@ -87,7 +75,6 @@
    9.41    val list_mk_abs    : (term list * term) -> term
    9.42    val list_mk_imp    : (term list * term) -> term
    9.43    val list_mk_forall : (term list * term) -> term
    9.44 -  val list_mk_exists : (term list * term) -> term
    9.45    val list_mk_conj   : term list -> term
    9.46    val list_mk_disj   : term list -> term
    9.47  
    9.48 @@ -102,8 +89,7 @@
    9.49    (* Miscellaneous *)
    9.50    val mk_vstruct : typ -> term list -> term
    9.51    val gen_all    : term -> term
    9.52 -  val find_term  : (term -> bool) -> term -> term
    9.53 -  val find_terms : (term -> bool) -> term -> term list
    9.54 +  val find_term  : (term -> bool) -> term -> term option
    9.55    val dest_relation : term -> term * term * term
    9.56    val is_WFR : term -> bool
    9.57    val ARB : typ -> term
    10.1 --- a/TFL/usyntax.sml	Thu Jun 05 13:26:09 1997 +0200
    10.2 +++ b/TFL/usyntax.sml	Thu Jun 05 13:27:28 1997 +0200
    10.3 @@ -49,9 +49,6 @@
    10.4   *                              Terms 
    10.5   *
    10.6   *---------------------------------------------------------------------------*)
    10.7 -nonfix aconv;
    10.8 -val aconv = curry (op aconv);
    10.9 -
   10.10  
   10.11  (* Free variables, in order of occurrence, from left to right in the 
   10.12   * syntax tree. *)
   10.13 @@ -67,52 +64,17 @@
   10.14  
   10.15  
   10.16  
   10.17 -fun free_varsl L = gen_distinct Term.aconv
   10.18 -                      (Utils.rev_itlist (curry op @ o term_frees) L []);
   10.19 -
   10.20  val type_vars_in_term = map mk_prim_vartype o term_tvars;
   10.21  
   10.22 -fun all_vars tm = 
   10.23 -  let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end
   10.24 -      fun add (t, A) = case t of
   10.25 -            Free   _ => if (memb t A) then A else t::A
   10.26 -          | Abs (s,ty,body) => add(body, add(Free(s,ty),A))
   10.27 -          | f$t =>  add(t, add(f, A))
   10.28 -          | _ => A
   10.29 -  in rev(add(tm,[]))
   10.30 -  end;
   10.31 -fun all_varsl L = gen_distinct Term.aconv
   10.32 -                      (Utils.rev_itlist (curry op @ o all_vars) L []);
   10.33  
   10.34  
   10.35  (* Prelogic *)
   10.36  fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty)
   10.37  fun inst theta = subst_vars (map dest_tybinding theta,[])
   10.38  
   10.39 -fun beta_conv((t1 as Abs _ ) $ t2) = betapply(t1,t2)
   10.40 -  | beta_conv _ = raise USYN_ERR{func = "beta_conv", mesg = "Not a beta-redex"};
   10.41 -
   10.42  
   10.43  (* Construction routines *)
   10.44  
   10.45 -val string_variant = variant;
   10.46 -
   10.47 -local fun var_name(Var((Name,_),_)) = Name
   10.48 -        | var_name(Free(s,_)) = s
   10.49 -        | var_name _ = raise USYN_ERR{func = "variant",
   10.50 -                                 mesg = "list elem. is not a variable"}
   10.51 -in
   10.52 -fun variant [] v = v
   10.53 -  | variant vlist (Var((Name,i),ty)) = 
   10.54 -       Var((string_variant (map var_name vlist) Name,i),ty)
   10.55 -  | variant vlist (Free(Name,ty)) =
   10.56 -       Free(string_variant (map var_name vlist) Name,ty)
   10.57 -  | variant _ _ = raise USYN_ERR{func = "variant",
   10.58 -                            mesg = "2nd arg. should be a variable"}
   10.59 -end;
   10.60 -
   10.61 -fun mk_comb{Rator,Rand} = Rator $ Rand;
   10.62 -
   10.63  fun mk_abs{Bvar as Var((s,_),ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
   10.64    | mk_abs{Bvar as Free(s,ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
   10.65    | mk_abs _ = raise USYN_ERR{func = "mk_abs", mesg = "Bvar is not a variable"};
   10.66 @@ -166,8 +128,8 @@
   10.67         if (is_var varstruct)
   10.68         then mk_abs{Bvar = varstruct, Body = body}
   10.69         else let val {fst,snd} = dest_pair varstruct
   10.70 -            in mk_comb{Rator= mk_uncurry(type_of fst,type_of snd,type_of body),
   10.71 -                       Rand = mpa(fst,mpa(snd,body))}
   10.72 +            in mk_uncurry(type_of fst,type_of snd,type_of body) $
   10.73 +	       mpa(fst,mpa(snd,body))
   10.74              end
   10.75   in mpa(varstruct,body)
   10.76   end
   10.77 @@ -255,16 +217,10 @@
   10.78  (* Garbage - ought to be dropped *)
   10.79  val lhs   = #lhs o dest_eq
   10.80  val rhs   = #rhs o dest_eq
   10.81 -val rator = #Rator o dest_comb
   10.82  val rand  = #Rand o dest_comb
   10.83 -val bvar  = #Bvar o dest_abs
   10.84 -val body  = #Body o dest_abs
   10.85    
   10.86  
   10.87  (* Query routines *)
   10.88 -val is_comb   = can dest_comb
   10.89 -val is_abs    = can dest_abs
   10.90 -val is_eq     = can dest_eq
   10.91  val is_imp    = can dest_imp
   10.92  val is_forall = can dest_forall
   10.93  val is_exists = can dest_exists
   10.94 @@ -281,7 +237,6 @@
   10.95  
   10.96  (* These others are almost never used *)
   10.97  fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
   10.98 -fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists{Bvar=v, Body=b})V t;
   10.99  fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
  10.100  val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
  10.101  val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj{disj1=d1, disj2=tm})
  10.102 @@ -352,35 +307,14 @@
  10.103  (* Search a term for a sub-term satisfying the predicate p. *)
  10.104  fun find_term p =
  10.105     let fun find tm =
  10.106 -      if (p tm)
  10.107 -      then tm 
  10.108 -      else if (is_abs tm)
  10.109 -           then find (#Body(dest_abs tm))
  10.110 -           else let val {Rator,Rand} = dest_comb tm
  10.111 -                in find Rator handle _ => find Rand
  10.112 -                end handle _ => raise USYN_ERR{func = "find_term",mesg = ""}
  10.113 +      if (p tm) then Some tm 
  10.114 +      else case tm of
  10.115 +	  Abs(_,_,body) => find body
  10.116 +	| (t$u)         => (Some (the (find t)) handle _ => find u)
  10.117 +	| _             => None
  10.118     in find
  10.119     end;
  10.120  
  10.121 -(*******************************************************************
  10.122 - * find_terms: (term -> HOLogic.boolT) -> term -> term list
  10.123 - * 
  10.124 - *  Find all subterms in a term that satisfy a given predicate p.
  10.125 - *
  10.126 - *******************************************************************)
  10.127 -fun find_terms p =
  10.128 -   let fun accum tl tm =
  10.129 -      let val tl' = if (p tm) then (tm::tl) else tl 
  10.130 -      in if (is_abs tm)
  10.131 -         then accum tl' (#Body(dest_abs tm))
  10.132 -         else let val {Rator,Rand} = dest_comb tm
  10.133 -              in accum (accum tl' Rator) Rand
  10.134 -              end handle _ => tl'
  10.135 -      end
  10.136 -   in accum []
  10.137 -   end;
  10.138 -
  10.139 -
  10.140  fun dest_relation tm =
  10.141     if (type_of tm = HOLogic.boolT)
  10.142     then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
  10.143 @@ -389,7 +323,8 @@
  10.144                                    mesg="unexpected term structure"}
  10.145     else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"};
  10.146  
  10.147 -fun is_WFR tm = (#Name(dest_const(rator tm)) = "wf") handle _ => false;
  10.148 +fun is_WFR (Const("wf",_)$_) = true
  10.149 +  | is_WFR _                 = false;
  10.150  
  10.151  fun ARB ty = mk_select{Bvar=Free("v",ty),
  10.152                         Body=Const("True",HOLogic.boolT)};