Konrad Slind's TFL
authorpaulson
Fri Oct 18 12:41:04 1996 +0200 (1996-10-18)
changeset 21123902e9af752f
parent 2111 81c8d46edfa3
child 2113 21266526ac42
Konrad Slind's TFL
TFL/README
TFL/WF1.ML
TFL/WF1.thy
TFL/dcterm.sml
TFL/mask.sig
TFL/mask.sml
TFL/post.sml
TFL/rules.new.sml
TFL/rules.sig
TFL/sys.sml
TFL/test.sml
TFL/test1.sml
TFL/tfl.sig
TFL/tfl.sml
TFL/thms.sig
TFL/thms.sml
TFL/thry.sig
TFL/thry.sml
TFL/usyntax.sig
TFL/usyntax.sml
TFL/utils.sig
TFL/utils.sml
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/TFL/README	Fri Oct 18 12:41:04 1996 +0200
     1.3 @@ -0,0 +1,6 @@
     1.4 +How to build TFL and run the Unify example.
     1.5 +
     1.6 +1. Invoke the current version of Isabelle-HOL.
     1.7 +2. use "sys.sml";  
     1.8 +3. cd examples/Subst
     1.9 +4. use "ROOT.ML";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/TFL/WF1.ML	Fri Oct 18 12:41:04 1996 +0200
     2.3 @@ -0,0 +1,232 @@
     2.4 +(*  Title: 	HOL/WF.ML
     2.5 +    ID:         $Id$
     2.6 +    Author: 	Konrad Slind
     2.7 +    Copyright   1996  TU Munich
     2.8 +
     2.9 +For WF1.thy.  
    2.10 +*)
    2.11 +
    2.12 +open WF1;
    2.13 +
    2.14 +(* TFL variants *)
    2.15 +goal WF.thy
    2.16 +    "!R. wf R --> (!P. (!x. (!y. (y,x):R --> P y) --> P x) --> (!x. P x))";
    2.17 +by (strip_tac 1);
    2.18 +by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1);
    2.19 +by (assume_tac 1);
    2.20 +by (fast_tac HOL_cs 1);
    2.21 +qed"tfl_wf_induct";
    2.22 +
    2.23 +goal WF.thy "!f R. (x,a):R --> (cut f R a)(x) = f(x)";
    2.24 +by (strip_tac 1);
    2.25 +by (rtac cut_apply 1);
    2.26 +by (assume_tac 1);
    2.27 +qed"tfl_cut_apply";
    2.28 +
    2.29 +goal WF.thy "!M R f. (f=wfrec R M) --> wf R --> (!x. f x = M (cut f R x) x)";
    2.30 +by (strip_tac 1);
    2.31 +by (res_inst_tac [("r","R"), ("H","M"),
    2.32 +                  ("a","x"), ("f","f")] (eq_reflection RS def_wfrec) 1);
    2.33 +by (assume_tac 1);
    2.34 +by (assume_tac 1);
    2.35 +qed "tfl_wfrec";
    2.36 +
    2.37 +(*----------------------------------------------------------------------------
    2.38 + * Proof that the inverse image into a wellfounded relation is wellfounded.
    2.39 + * The proof is relatively sloppy - I map to another version of 
    2.40 + * wellfoundedness (every n.e. set has an R-minimal element) and transport 
    2.41 + * the proof for that formulation over. I also didn't remember the existence
    2.42 + *  of "set_cs" so no doubt the proof can be dramatically shortened!
    2.43 + *---------------------------------------------------------------------------*)
    2.44 +goal HOL.thy "(~(!x. P x)) = (? x. ~(P x))";
    2.45 +by (fast_tac HOL_cs 1);
    2.46 +val th1 = result();
    2.47 +
    2.48 +goal HOL.thy "(~(? x. P x)) = (!x. ~(P x))";
    2.49 +by (fast_tac HOL_cs 1);
    2.50 +val th2 = result();
    2.51 +
    2.52 +goal HOL.thy "(~(x-->y)) = (x & (~ y))";
    2.53 +by (fast_tac HOL_cs 1);
    2.54 +val th3 = result();
    2.55 +
    2.56 +goal HOL.thy "((~ x) | y) = (x --> y)";
    2.57 +by (fast_tac HOL_cs 1);
    2.58 +val th4 = result();
    2.59 +
    2.60 +goal HOL.thy "(~(x & y)) = ((~ x) | (~ y))";
    2.61 +by (fast_tac HOL_cs 1);
    2.62 +val th5 = result();
    2.63 +
    2.64 +goal HOL.thy "(~(x | y)) = ((~ x) & (~ y))";
    2.65 +by (fast_tac HOL_cs 1);
    2.66 +val th6 = result();
    2.67 +
    2.68 +goal HOL.thy "(~(~x)) = x";
    2.69 +by (fast_tac HOL_cs 1);
    2.70 +val th7 = result();
    2.71 +
    2.72 +(* Using [th1,th2,th3,th4,th5,th6,th7] as rewrites drives negation inwards. *)
    2.73 +val NNF_rews = map (fn th => th RS eq_reflection)[th1,th2,th3,th4,th5,th6,th7];
    2.74 +
    2.75 +(* The name "contrapos" is already taken. *)
    2.76 +goal HOL.thy "(P --> Q) = ((~ Q) --> (~ P))";
    2.77 +by (fast_tac HOL_cs 1);
    2.78 +val ol_contrapos = result();
    2.79 +
    2.80 +(* Maps to another version of wellfoundedness *)
    2.81 +val [p1] = goalw WF.thy [wf_def]
    2.82 +"wf(R) ==> (!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b))))";
    2.83 +by (rtac allI 1);
    2.84 +by (rtac (ol_contrapos RS ssubst) 1);
    2.85 +by (rewrite_tac NNF_rews);
    2.86 +by (rtac impI 1);
    2.87 +by (rtac ((p1 RS spec) RS mp) 1);
    2.88 +by (fast_tac HOL_cs 1);
    2.89 +val wf_minimal = result();
    2.90 +
    2.91 +goalw WF.thy [wf_def]
    2.92 +"(!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b)))) --> wf R";
    2.93 +by (rtac impI 1);
    2.94 +by (rtac allI 1);
    2.95 +by (rtac (ol_contrapos RS ssubst) 1);
    2.96 +by (rewrite_tac NNF_rews);
    2.97 +by (rtac impI 1);
    2.98 +by (etac allE 1);
    2.99 +by (dtac mp 1);
   2.100 +by (assume_tac 1);
   2.101 +by (fast_tac HOL_cs 1);
   2.102 +val minimal_wf = result();
   2.103 +
   2.104 +val wf_eq_minimal = 
   2.105 +  standard ((wf_minimal COMP ((minimal_wf RS mp) COMP iffI)) RS sym);
   2.106 +
   2.107 +goalw WF1.thy [inv_image_def,wf_eq_minimal RS eq_reflection] 
   2.108 +"wf(R) --> wf(inv_image R (f::'a=>'b))"; 
   2.109 +by (strip_tac 1);
   2.110 +by (etac exE 1);
   2.111 +by (subgoal_tac "? (w::'b). ? (x::'a). Q x & (f x = w)" 1);
   2.112 +by (rtac exI 2);
   2.113 +by (rtac exI 2);
   2.114 +by (rtac conjI 2);
   2.115 +by (assume_tac 2);
   2.116 +by (rtac refl 2);
   2.117 +
   2.118 +by (etac allE 1);
   2.119 +by (dtac mp 1);
   2.120 +by (assume_tac 1);
   2.121 +by (eres_inst_tac [("P","? min. (? x. Q x & f x = min) & \
   2.122 +                \ (! b. (b, min) : R --> ~ (? x. Q x & f x = b))")] rev_mp 1);
   2.123 +by (etac thin_rl 1);
   2.124 +by (etac thin_rl 1);
   2.125 +by (rewrite_tac NNF_rews);
   2.126 +by (rtac impI 1);
   2.127 +by (etac exE 1);
   2.128 +by (etac conjE 1);
   2.129 +by (etac exE 1);
   2.130 +by (rtac exI 1);
   2.131 +by (etac conjE 1);
   2.132 +by (rtac conjI 1);
   2.133 +by (assume_tac 1);
   2.134 +by (hyp_subst_tac 1);
   2.135 +by (rtac allI 1);
   2.136 +by (rtac impI 1);
   2.137 +by (etac CollectE 1);
   2.138 +by (etac allE 1);
   2.139 +by (dtac mp 1);
   2.140 +by (rewrite_tac[fst_conv RS eq_reflection,snd_conv RS eq_reflection]);
   2.141 +by (assume_tac 1);
   2.142 +by (fast_tac HOL_cs 1);
   2.143 +val wf_inv_image = result() RS mp;
   2.144 +
   2.145 +(* from Nat.ML *)
   2.146 +goalw WF1.thy [wf_def] "wf(pred_nat)";
   2.147 +by (strip_tac 1);
   2.148 +by (nat_ind_tac "x" 1);
   2.149 +by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, 
   2.150 +                             make_elim Suc_inject]) 2);
   2.151 +by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, Zero_neq_Suc]) 1);
   2.152 +val wf_pred_nat = result();
   2.153 +
   2.154 +goalw WF1.thy [wf_def,pred_list_def] "wf(pred_list)";
   2.155 +by (strip_tac 1);
   2.156 +by (List.list.induct_tac "x" 1);
   2.157 +by (etac allE 1);
   2.158 +by (etac impE 1);
   2.159 +by (assume_tac 2);
   2.160 +by (strip_tac 1);
   2.161 +by (etac CollectE 1);
   2.162 +by (asm_full_simp_tac (!simpset) 1);
   2.163 +
   2.164 +by (etac allE 1);
   2.165 +by (etac impE 1);
   2.166 +by (assume_tac 2);
   2.167 +by (strip_tac 1);
   2.168 +by (etac CollectE 1);
   2.169 +by (etac exE 1);
   2.170 +by (asm_full_simp_tac (!simpset) 1);
   2.171 +by (etac conjE 1);
   2.172 +by (hyp_subst_tac 1);
   2.173 +by (assume_tac 1);
   2.174 +qed "wf_pred_list";
   2.175 +
   2.176 +(*----------------------------------------------------------------------------
   2.177 + * All measures are wellfounded.
   2.178 + *---------------------------------------------------------------------------*)
   2.179 +
   2.180 +goalw WF1.thy [measure_def] "wf (measure f)";
   2.181 +by (rtac wf_inv_image 1);
   2.182 +by (rtac wf_trancl 1);
   2.183 +by (rtac wf_pred_nat 1);
   2.184 +qed "wf_measure";
   2.185 +
   2.186 +(*----------------------------------------------------------------------------
   2.187 + * Wellfoundedness of lexicographic combinations
   2.188 + *---------------------------------------------------------------------------*)
   2.189 +
   2.190 +val prems = goal Prod.thy "!a b. P((a,b)) ==> !p. P(p)";
   2.191 +by (cut_facts_tac prems 1);
   2.192 +by (rtac allI 1);
   2.193 +by (rtac (surjective_pairing RS ssubst) 1);
   2.194 +by (fast_tac HOL_cs 1);
   2.195 +qed "split_all_pair";
   2.196 +
   2.197 +val [wfa,wfb] = goalw WF1.thy [wf_def,lex_prod_def]
   2.198 + "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
   2.199 +by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
   2.200 +by (rtac (wfa RS spec RS mp) 1);
   2.201 +by (EVERY1 [rtac allI,rtac impI]);
   2.202 +by (rtac (wfb RS spec RS mp) 1);
   2.203 +by (fast_tac (set_cs addSEs [Pair_inject]) 1);
   2.204 +qed "wf_lex_prod";
   2.205 +
   2.206 +(*----------------------------------------------------------------------------
   2.207 + * Wellfoundedness of relational product
   2.208 + *---------------------------------------------------------------------------*)
   2.209 +val [wfa,wfb] = goalw WF1.thy [wf_def,rprod_def]
   2.210 + "[| wf(ra); wf(rb) |] ==> wf(rprod ra rb)";
   2.211 +by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
   2.212 +by (rtac (wfa RS spec RS mp) 1);
   2.213 +by (EVERY1 [rtac allI,rtac impI]);
   2.214 +by (rtac (wfb RS spec RS mp) 1);
   2.215 +by (fast_tac (set_cs addSEs [Pair_inject]) 1);
   2.216 +qed "wf_rel_prod";
   2.217 +
   2.218 +
   2.219 +(*---------------------------------------------------------------------------
   2.220 + * Wellfoundedness of subsets
   2.221 + *---------------------------------------------------------------------------*)
   2.222 +
   2.223 +goalw WF1.thy [wf_eq_minimal RS eq_reflection] 
   2.224 +     "wf(r) --> (!x y. (x,y):p --> (x,y):r) --> wf(p)";
   2.225 +by (fast_tac set_cs 1);
   2.226 +qed "wf_subset";
   2.227 +
   2.228 +(*---------------------------------------------------------------------------
   2.229 + * Wellfoundedness of the empty relation.
   2.230 + *---------------------------------------------------------------------------*)
   2.231 +
   2.232 +goalw WF1.thy [wf_eq_minimal RS eq_reflection,emptyr_def] 
   2.233 +     "wf(emptyr)";
   2.234 +by (fast_tac set_cs 1);
   2.235 +qed "wf_emptyr";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/TFL/WF1.thy	Fri Oct 18 12:41:04 1996 +0200
     3.3 @@ -0,0 +1,27 @@
     3.4 +(* Derived wellfounded relations, plus customized-for-TFL theorems from WF *)
     3.5 +
     3.6 +WF1 = List +
     3.7 +consts
     3.8 + inv_image  :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
     3.9 + measure    :: "('a => nat) => ('a * 'a)set"
    3.10 +    "**"    :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
    3.11 +   rprod    :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
    3.12 +   emptyr   :: "('a * 'b) set"
    3.13 + pred_list  :: "('a list * 'a list) set"
    3.14 +
    3.15 +defs
    3.16 +  inv_image_def "inv_image R f == {p. (f(fst p), f(snd p)) : R}"
    3.17 +
    3.18 +  measure_def   "measure == inv_image (trancl pred_nat)"
    3.19 +
    3.20 +  lex_prod_def  "ra**rb == {p. ? a a' b b'. 
    3.21 +                                p = ((a,b),(a',b')) & 
    3.22 +                               ((a,a') : ra | a=a' & (b,b') : rb)}"
    3.23 +
    3.24 +  rprod_def     "rprod ra rb == {p. ? a a' b b'. 
    3.25 +                                p = ((a,b),(a',b')) & 
    3.26 +                               ((a,a') : ra & (b,b') : rb)}"
    3.27 +
    3.28 +  emptyr_def    "emptyr == {}"
    3.29 +  pred_list_def "pred_list == {p. ? h. snd p = h#(fst p)}"
    3.30 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/TFL/dcterm.sml	Fri Oct 18 12:41:04 1996 +0200
     4.3 @@ -0,0 +1,271 @@
     4.4 +(*---------------------------------------------------------------------------
     4.5 + * Derived efficient cterm destructors.
     4.6 + *---------------------------------------------------------------------------*)
     4.7 +
     4.8 +structure Dcterm :
     4.9 +sig
    4.10 +    val caconv : cterm -> cterm -> bool
    4.11 +    val mk_eq : cterm * cterm -> cterm
    4.12 +    val mk_imp : cterm * cterm -> cterm
    4.13 +    val mk_conj : cterm * cterm -> cterm
    4.14 +    val mk_disj : cterm * cterm -> cterm
    4.15 +    val mk_select : cterm * cterm -> cterm
    4.16 +    val mk_forall : cterm * cterm -> cterm
    4.17 +    val mk_exists : cterm * cterm -> cterm
    4.18 +
    4.19 +    val dest_conj : cterm -> cterm * cterm
    4.20 +    val dest_const : cterm -> {Name:string, Ty:typ}
    4.21 +    val dest_disj : cterm -> cterm * cterm
    4.22 +    val dest_eq : cterm -> cterm * cterm
    4.23 +    val dest_exists : cterm -> cterm * cterm
    4.24 +    val dest_forall : cterm -> cterm * cterm
    4.25 +    val dest_imp : cterm -> cterm * cterm
    4.26 +    val dest_let : cterm -> cterm * cterm
    4.27 +    val dest_neg : cterm -> cterm
    4.28 +    val dest_pair : cterm -> cterm * cterm
    4.29 +    val dest_select : cterm -> cterm * cterm
    4.30 +    val dest_var : cterm -> {Name:string, Ty:typ}
    4.31 +    val is_abs : cterm -> bool
    4.32 +    val is_comb : cterm -> bool
    4.33 +    val is_conj : cterm -> bool
    4.34 +    val is_cons : cterm -> bool
    4.35 +    val is_const : cterm -> bool
    4.36 +    val is_disj : cterm -> bool
    4.37 +    val is_eq : cterm -> bool
    4.38 +    val is_exists : cterm -> bool
    4.39 +    val is_forall : cterm -> bool
    4.40 +    val is_imp : cterm -> bool
    4.41 +    val is_let : cterm -> bool
    4.42 +    val is_neg : cterm -> bool
    4.43 +    val is_pair : cterm -> bool
    4.44 +    val is_select : cterm -> bool
    4.45 +    val is_var : cterm -> bool
    4.46 +    val list_mk_comb : cterm * cterm list -> cterm
    4.47 +    val list_mk_abs : cterm list -> cterm -> cterm
    4.48 +    val list_mk_imp : cterm list * cterm -> cterm
    4.49 +    val list_mk_exists : cterm list * cterm -> cterm
    4.50 +    val list_mk_forall : cterm list * cterm -> cterm
    4.51 +    val list_mk_conj : cterm list -> cterm
    4.52 +    val list_mk_disj : cterm list -> cterm
    4.53 +    val strip_abs : cterm -> cterm list * cterm
    4.54 +    val strip_comb : cterm -> cterm * cterm list
    4.55 +    val strip_conj : cterm -> cterm list
    4.56 +    val strip_disj : cterm -> cterm list
    4.57 +    val strip_exists : cterm -> cterm list * cterm
    4.58 +    val strip_forall : cterm -> cterm list * cterm
    4.59 +    val strip_imp : cterm -> cterm list * cterm
    4.60 +    val strip_pair : cterm -> cterm list
    4.61 +    val drop_prop : cterm -> cterm
    4.62 +    val mk_prop : cterm -> cterm
    4.63 +  end =
    4.64 +struct
    4.65 +
    4.66 +fun ERR func mesg = Utils.ERR{module = "Dcterm", func = func, mesg = mesg};
    4.67 +
    4.68 +(*---------------------------------------------------------------------------
    4.69 + * General support routines
    4.70 + *---------------------------------------------------------------------------*)
    4.71 +val can = Utils.can;
    4.72 +val quote = Utils.quote;
    4.73 +fun swap (x,y) = (y,x);
    4.74 +val bool = Type("bool",[]);
    4.75 +
    4.76 +fun itlist f L base_value =
    4.77 +   let fun it [] = base_value
    4.78 +         | it (a::rst) = f a (it rst)
    4.79 +   in it L 
    4.80 +   end;
    4.81 +
    4.82 +fun end_itlist f =
    4.83 +let fun endit [] = raise ERR"end_itlist" "list too short"
    4.84 +      | endit alist = 
    4.85 +         let val (base::ralist) = rev alist
    4.86 +         in itlist f (rev ralist) base  end
    4.87 +in endit
    4.88 +end;
    4.89 +
    4.90 +fun rev_itlist f =
    4.91 +   let fun rev_it [] base = base
    4.92 +         | rev_it (a::rst) base = rev_it rst (f a base)
    4.93 +   in rev_it
    4.94 +   end;
    4.95 +
    4.96 +(*---------------------------------------------------------------------------
    4.97 + * Alpha conversion.
    4.98 + *---------------------------------------------------------------------------*)
    4.99 +fun caconv ctm1 ctm2 = Term.aconv(#t(rep_cterm ctm1),#t(rep_cterm ctm2));
   4.100 +
   4.101 +
   4.102 +(*---------------------------------------------------------------------------
   4.103 + * Some simple constructor functions.
   4.104 + *---------------------------------------------------------------------------*)
   4.105 +
   4.106 +fun mk_const sign pr = cterm_of sign (Const pr);
   4.107 +val mk_hol_const = mk_const (sign_of HOL.thy);
   4.108 +
   4.109 +fun list_mk_comb (h,[]) = h
   4.110 +  | list_mk_comb (h,L) = rev_itlist (fn t1 => fn t2 => capply t2 t1) L h;
   4.111 +
   4.112 +
   4.113 +fun mk_eq(lhs,rhs) = 
   4.114 +   let val ty = #T(rep_cterm lhs)
   4.115 +       val c = mk_hol_const("op =", ty --> ty --> bool)
   4.116 +   in list_mk_comb(c,[lhs,rhs])
   4.117 +   end;
   4.118 +
   4.119 +local val c = mk_hol_const("op -->", bool --> bool --> bool)
   4.120 +in fun mk_imp(ant,conseq) = list_mk_comb(c,[ant,conseq])
   4.121 +end;
   4.122 +
   4.123 +fun mk_select (r as (Bvar,Body)) = 
   4.124 +  let val ty = #T(rep_cterm Bvar)
   4.125 +      val c = mk_hol_const("Eps", (ty --> bool) --> ty)
   4.126 +  in capply c (uncurry cabs r)
   4.127 +  end;
   4.128 +
   4.129 +fun mk_forall (r as (Bvar,Body)) = 
   4.130 +  let val ty = #T(rep_cterm Bvar)
   4.131 +      val c = mk_hol_const("All", (ty --> bool) --> bool)
   4.132 +  in capply c (uncurry cabs r)
   4.133 +  end;
   4.134 +
   4.135 +fun mk_exists (r as (Bvar,Body)) = 
   4.136 +  let val ty = #T(rep_cterm Bvar)
   4.137 +      val c = mk_hol_const("Ex", (ty --> bool) --> bool)
   4.138 +  in capply c (uncurry cabs r)
   4.139 +  end;
   4.140 +
   4.141 +
   4.142 +local val c = mk_hol_const("op &", bool --> bool --> bool)
   4.143 +in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
   4.144 +end;
   4.145 +
   4.146 +local val c = mk_hol_const("op |", bool --> bool --> bool)
   4.147 +in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
   4.148 +end;
   4.149 +
   4.150 +
   4.151 +(*---------------------------------------------------------------------------
   4.152 + * The primitives.
   4.153 + *---------------------------------------------------------------------------*)
   4.154 +fun dest_const ctm = 
   4.155 +   (case #t(rep_cterm ctm)
   4.156 +      of Const(s,ty) => {Name = s, Ty = ty}
   4.157 +       | _ => raise ERR "dest_const" "not a constant");
   4.158 +
   4.159 +fun dest_var ctm = 
   4.160 +   (case #t(rep_cterm ctm)
   4.161 +      of Var((s,i),ty) => {Name=s, Ty=ty}
   4.162 +       | Free(s,ty)    => {Name=s, Ty=ty}
   4.163 +       |             _ => raise ERR "dest_var" "not a variable");
   4.164 +
   4.165 +
   4.166 +(*---------------------------------------------------------------------------
   4.167 + * Derived destructor operations. 
   4.168 + *---------------------------------------------------------------------------*)
   4.169 +
   4.170 +fun dest_monop expected tm = 
   4.171 + let exception Fail
   4.172 +     val (c,N) = dest_comb tm
   4.173 + in if (#Name(dest_const c) = expected) then N else raise Fail
   4.174 + end handle e => raise ERR "dest_monop" ("Not a(n) "^quote expected);
   4.175 +
   4.176 +fun dest_binop expected tm =
   4.177 + let val (M,N) = dest_comb tm
   4.178 + in (dest_monop expected M, N)
   4.179 + end handle e => raise ERR "dest_binop" ("Not a(n) "^quote expected);
   4.180 +
   4.181 +(* For "if-then-else" 
   4.182 +fun dest_triop expected tm =
   4.183 + let val (MN,P) = dest_comb tm
   4.184 +     val (M,N) = dest_binop expected MN
   4.185 + in (M,N,P)
   4.186 + end handle e => raise ERR "dest_triop" ("Not a(n) "^quote expected);
   4.187 +*)
   4.188 +
   4.189 +fun dest_binder expected tm = 
   4.190 +  dest_abs(dest_monop expected tm)
   4.191 +  handle e => raise ERR "dest_binder" ("Not a(n) "^quote expected);
   4.192 +
   4.193 +
   4.194 +val dest_neg    = dest_monop "not"
   4.195 +val dest_pair   = dest_binop "Pair";
   4.196 +val dest_eq     = dest_binop "op ="
   4.197 +val dest_imp    = dest_binop "op -->"
   4.198 +val dest_conj   = dest_binop "op &"
   4.199 +val dest_disj   = dest_binop "op |"
   4.200 +val dest_cons   = dest_binop "op #"
   4.201 +val dest_let    = swap o dest_binop "Let";
   4.202 +(* val dest_cond   = dest_triop "if" *)
   4.203 +val dest_select = dest_binder "Eps"
   4.204 +val dest_exists = dest_binder "Ex"
   4.205 +val dest_forall = dest_binder "All"
   4.206 +
   4.207 +(* Query routines *)
   4.208 +
   4.209 +val is_var    = can dest_var
   4.210 +val is_const  = can dest_const
   4.211 +val is_comb   = can dest_comb
   4.212 +val is_abs    = can dest_abs
   4.213 +val is_eq     = can dest_eq
   4.214 +val is_imp    = can dest_imp
   4.215 +val is_select = can dest_select
   4.216 +val is_forall = can dest_forall
   4.217 +val is_exists = can dest_exists
   4.218 +val is_neg    = can dest_neg
   4.219 +val is_conj   = can dest_conj
   4.220 +val is_disj   = can dest_disj
   4.221 +(* val is_cond   = can dest_cond *)
   4.222 +val is_pair   = can dest_pair
   4.223 +val is_let    = can dest_let
   4.224 +val is_cons   = can dest_cons
   4.225 +
   4.226 +
   4.227 +(*---------------------------------------------------------------------------
   4.228 + * Iterated creation.
   4.229 + *---------------------------------------------------------------------------*)
   4.230 +val list_mk_abs = itlist cabs;
   4.231 +
   4.232 +fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp(a,tm)) A c;
   4.233 +fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v, b)) V t;
   4.234 +fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall(v, b)) V t;
   4.235 +val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj(c1, tm))
   4.236 +val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1, tm))
   4.237 +
   4.238 +(*---------------------------------------------------------------------------
   4.239 + * Iterated destruction. (To the "right" in a term.)
   4.240 + *---------------------------------------------------------------------------*)
   4.241 +fun strip break tm = 
   4.242 +  let fun dest (p as (ctm,accum)) = 
   4.243 +        let val (M,N) = break ctm
   4.244 +        in dest (N, M::accum)
   4.245 +        end handle _ => p
   4.246 +  in dest (tm,[])
   4.247 +  end;
   4.248 +
   4.249 +fun rev2swap (x,l) = (rev l, x);
   4.250 +
   4.251 +val strip_comb   = strip (swap o dest_comb)  (* Goes to the "left" *)
   4.252 +val strip_imp    = rev2swap o strip dest_imp
   4.253 +val strip_abs    = rev2swap o strip dest_abs
   4.254 +val strip_forall = rev2swap o strip dest_forall
   4.255 +val strip_exists = rev2swap o strip dest_exists
   4.256 +
   4.257 +val strip_conj   = rev o (op::) o strip dest_conj
   4.258 +val strip_disj   = rev o (op::) o strip dest_disj
   4.259 +val strip_pair   = rev o (op::) o strip dest_pair;
   4.260 +
   4.261 +
   4.262 +(*---------------------------------------------------------------------------
   4.263 + * Going into and out of prop
   4.264 + *---------------------------------------------------------------------------*)
   4.265 +local val prop = cterm_of (sign_of HOL.thy) (read"Trueprop")
   4.266 +in fun mk_prop ctm =
   4.267 +     case (#t(rep_cterm ctm))
   4.268 +       of (Const("Trueprop",_)$_) => ctm
   4.269 +        |  _ => capply prop ctm
   4.270 +end;
   4.271 +
   4.272 +fun drop_prop ctm = dest_monop "Trueprop" ctm handle _ => ctm;
   4.273 +
   4.274 +end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/TFL/mask.sig	Fri Oct 18 12:41:04 1996 +0200
     5.3 @@ -0,0 +1,8 @@
     5.4 +signature Mask_sig =
     5.5 +sig
     5.6 + datatype 'a binding = |-> of ('a * 'a)  (* infix 7 |->; *)
     5.7 +
     5.8 + type mask
     5.9 + val ERR : mask
    5.10 +
    5.11 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/TFL/mask.sml	Fri Oct 18 12:41:04 1996 +0200
     6.3 @@ -0,0 +1,16 @@
     6.4 +(*---------------------------------------------------------------------------
     6.5 + * This structure is intended to shield TFL from any constructors already 
     6.6 + * declared in the environment. In the Isabelle port, for example, there
     6.7 + * was already a datatype with "|->" being a constructor. In TFL we were
     6.8 + * trying to define a function "|->", but it failed in PolyML (which conforms
     6.9 + * better to the Standard) while the definition was accepted in NJ/SML
    6.10 + * (which doesn't always conform so well to the standard).
    6.11 + *---------------------------------------------------------------------------*)
    6.12 +
    6.13 +structure Mask : Mask_sig =
    6.14 +struct
    6.15 +
    6.16 + datatype 'a binding = |-> of ('a * 'a)   (* infix 7 |->; *)
    6.17 +
    6.18 + datatype mask = ERR 
    6.19 +end;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/TFL/post.sml	Fri Oct 18 12:41:04 1996 +0200
     7.3 @@ -0,0 +1,193 @@
     7.4 +structure Tfl
     7.5 + :sig
     7.6 +   structure Prim : TFL_sig
     7.7 +
     7.8 +   val tgoalw : theory -> thm list -> thm -> thm list
     7.9 +   val tgoal: theory -> thm -> thm list
    7.10 +
    7.11 +   val WF_TAC : thm list -> tactic
    7.12 +
    7.13 +   val simplifier : thm -> thm
    7.14 +   val std_postprocessor : theory 
    7.15 +                           -> {induction:thm, rules:thm, TCs:term list list} 
    7.16 +                           -> {induction:thm, rules:thm, nested_tcs:thm list}
    7.17 +
    7.18 +   val rfunction  : theory
    7.19 +                     -> (thm list -> thm -> thm)
    7.20 +                        -> term -> term  
    7.21 +                          -> {induction:thm, rules:thm, 
    7.22 +                              tcs:term list, theory:theory}
    7.23 +
    7.24 +   val Rfunction : theory -> term -> term  
    7.25 +                   -> {induction:thm, rules:thm, 
    7.26 +                       theory:theory, tcs:term list}
    7.27 +
    7.28 +   val function : theory -> term -> {theory:theory, eq_ind : thm}
    7.29 +   val lazyR_def : theory -> term -> {theory:theory, eqns : thm}
    7.30 +
    7.31 +   val tflcongs : theory -> thm list
    7.32 +
    7.33 +  end = 
    7.34 +struct
    7.35 + structure Prim = Prim
    7.36 +
    7.37 + fun tgoalw thy defs thm = 
    7.38 +    let val L = Prim.termination_goals thm
    7.39 +        open USyntax
    7.40 +        val g = cterm_of (sign_of thy) (mk_prop(list_mk_conj L))
    7.41 +    in goalw_cterm defs g
    7.42 +    end;
    7.43 +
    7.44 + val tgoal = Utils.C tgoalw [];
    7.45 +
    7.46 + fun WF_TAC thms = REPEAT(FIRST1(map rtac thms))
    7.47 + val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, 
    7.48 +                    wf_pred_nat, wf_pred_list, wf_trancl];
    7.49 +
    7.50 + val terminator = simp_tac(HOL_ss addsimps[pred_nat_def,pred_list_def,
    7.51 +                                           fst_conv,snd_conv,
    7.52 +                                           mem_Collect_eq,lessI]) 1
    7.53 +                  THEN TRY(fast_tac set_cs 1);
    7.54 +
    7.55 + val simpls = [less_eq RS eq_reflection,
    7.56 +               lex_prod_def, measure_def, inv_image_def, 
    7.57 +               fst_conv RS eq_reflection, snd_conv RS eq_reflection,
    7.58 +               mem_Collect_eq RS eq_reflection(*, length_Cons RS eq_reflection*)];
    7.59 +
    7.60 + val std_postprocessor = Prim.postprocess{WFtac = WFtac,
    7.61 +                                    terminator = terminator, 
    7.62 +                                    simplifier = Prim.Rules.simpl_conv simpls};
    7.63 +
    7.64 + val simplifier = rewrite_rule (simpls @ #simps(rep_ss HOL_ss) @ 
    7.65 +                                [pred_nat_def,pred_list_def]);
    7.66 + fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));
    7.67 +
    7.68 +
    7.69 +local structure S = Prim.USyntax
    7.70 +in
    7.71 +fun func_of_cond_eqn tm =
    7.72 +  #1(S.strip_comb(#lhs(S.dest_eq(#2(S.strip_forall(#2(S.strip_imp tm)))))))
    7.73 +end;
    7.74 +
    7.75 +
    7.76 +val concl = #2 o Prim.Rules.dest_thm;
    7.77 +
    7.78 +(*---------------------------------------------------------------------------
    7.79 + * Defining a function with an associated termination relation. Lots of
    7.80 + * postprocessing takes place.
    7.81 + *---------------------------------------------------------------------------*)
    7.82 +local 
    7.83 +structure S = Prim.USyntax
    7.84 +structure R = Prim.Rules
    7.85 +structure U = Utils
    7.86 +
    7.87 +val solved = not o U.can S.dest_eq o #2 o S.strip_forall o concl
    7.88 +
    7.89 +fun id_thm th = 
    7.90 +   let val {lhs,rhs} = S.dest_eq(#2(S.strip_forall(#2 (R.dest_thm th))))
    7.91 +   in S.aconv lhs rhs
    7.92 +   end handle _ => false
    7.93 +
    7.94 +fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
    7.95 +val P_imp_P_iff_True = prover "P --> (P= True)" RS mp;
    7.96 +val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
    7.97 +fun mk_meta_eq r = case concl_of r of
    7.98 +     Const("==",_)$_$_ => r
    7.99 +  |   _$(Const("op =",_)$_$_) => r RS eq_reflection
   7.100 +  |   _ => r RS P_imp_P_eq_True
   7.101 +fun rewrite L = rewrite_rule (map mk_meta_eq (Utils.filter(not o id_thm) L))
   7.102 +
   7.103 +fun join_assums th = 
   7.104 +  let val {sign,...} = rep_thm th
   7.105 +      val tych = cterm_of sign
   7.106 +      val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
   7.107 +      val cntxtl = (#1 o S.strip_imp) lhs  (* cntxtl should = cntxtr *)
   7.108 +      val cntxtr = (#1 o S.strip_imp) rhs  (* but union is solider *)
   7.109 +      val cntxt = U.union S.aconv cntxtl cntxtr
   7.110 +  in 
   7.111 +  R.GEN_ALL 
   7.112 +  (R.DISCH_ALL 
   7.113 +    (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))
   7.114 +  end
   7.115 +  val gen_all = S.gen_all
   7.116 +in
   7.117 +fun rfunction theory reducer R eqs = 
   7.118 + let val _ = output(std_out, "Making definition..  ")
   7.119 +     val _ = flush_out std_out
   7.120 +     val {rules,theory, full_pats_TCs,
   7.121 +          TCs,...} = Prim.gen_wfrec_definition theory {R=R,eqs=eqs} 
   7.122 +     val f = func_of_cond_eqn(concl(R.CONJUNCT1 rules handle _ => rules))
   7.123 +     val _ = output(std_out, "Definition made.\n")
   7.124 +     val _ = output(std_out, "Proving induction theorem..  ")
   7.125 +     val _ = flush_out std_out
   7.126 +     val ind = Prim.mk_induction theory f R full_pats_TCs
   7.127 +     val _ = output(std_out, "Proved induction theorem.\n")
   7.128 +     val pp = std_postprocessor theory
   7.129 +     val _ = output(std_out, "Postprocessing..  ")
   7.130 +     val _ = flush_out std_out
   7.131 +     val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs}
   7.132 +     val normal_tcs = Prim.termination_goals rules
   7.133 + in
   7.134 + case nested_tcs
   7.135 + of [] => (output(std_out, "Postprocessing done.\n");
   7.136 +           {theory=theory, induction=induction, rules=rules,tcs=normal_tcs})
   7.137 +  | L  => let val _ = output(std_out, "Simplifying nested TCs..  ")
   7.138 +              val (solved,simplified,stubborn) =
   7.139 +               U.itlist (fn th => fn (So,Si,St) =>
   7.140 +                     if (id_thm th) then (So, Si, th::St) else
   7.141 +                     if (solved th) then (th::So, Si, St) 
   7.142 +                     else (So, th::Si, St)) nested_tcs ([],[],[])
   7.143 +              val simplified' = map join_assums simplified
   7.144 +              val induction' = reducer (solved@simplified') induction
   7.145 +              val rules' = reducer (solved@simplified') rules
   7.146 +              val _ = output(std_out, "Postprocessing done.\n")
   7.147 +          in
   7.148 +          {induction = induction',
   7.149 +               rules = rules',
   7.150 +                 tcs = normal_tcs @
   7.151 +                      map (gen_all o S.rhs o #2 o S.strip_forall o concl)
   7.152 +                           (simplified@stubborn),
   7.153 +              theory = theory}
   7.154 +          end
   7.155 + end
   7.156 + handle (e as Utils.ERR _) => Utils.Raise e
   7.157 +     |     e               => print_exn e
   7.158 +
   7.159 +
   7.160 +fun Rfunction thry = 
   7.161 +     rfunction thry 
   7.162 +       (fn thl => rewrite (map standard thl @ #simps(rep_ss HOL_ss)));
   7.163 +
   7.164 +
   7.165 +end;
   7.166 +
   7.167 +
   7.168 +local structure R = Prim.Rules
   7.169 +in
   7.170 +fun function theory eqs = 
   7.171 + let val _ = output(std_out, "Making definition..  ")
   7.172 +     val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs
   7.173 +     val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules))
   7.174 +     val _ = output(std_out, "Definition made.\n")
   7.175 +     val _ = output(std_out, "Proving induction theorem..  ")
   7.176 +     val induction = Prim.mk_induction theory f R full_pats_TCs
   7.177 +      val _ = output(std_out, "Induction theorem proved.\n")
   7.178 + in {theory = theory, 
   7.179 +     eq_ind = standard (induction RS (rules RS conjI))}
   7.180 + end
   7.181 + handle (e as Utils.ERR _) => Utils.Raise e
   7.182 +      |     e              => print_exn e
   7.183 +end;
   7.184 +
   7.185 +
   7.186 +fun lazyR_def theory eqs = 
   7.187 +   let val {rules,theory, ...} = Prim.lazyR_def theory eqs
   7.188 +   in {eqns=rules, theory=theory}
   7.189 +   end
   7.190 +   handle (e as Utils.ERR _) => Utils.Raise e
   7.191 +        |     e              => print_exn e;
   7.192 +
   7.193 +
   7.194 + val () = Prim.Context.write[Thms.LET_CONG, Thms.COND_CONG];
   7.195 +
   7.196 +end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/TFL/rules.new.sml	Fri Oct 18 12:41:04 1996 +0200
     8.3 @@ -0,0 +1,825 @@
     8.4 +structure FastRules : Rules_sig = 
     8.5 +struct
     8.6 +
     8.7 +open Utils;
     8.8 +open Mask;
     8.9 +infix 7 |->;
    8.10 +
    8.11 +structure USyntax  = USyntax;
    8.12 +structure S  = USyntax;
    8.13 +structure U  = Utils;
    8.14 +structure D = Dcterm;
    8.15 +
    8.16 +type Type = USyntax.Type
    8.17 +type Preterm  = USyntax.Preterm
    8.18 +type Term = USyntax.Term
    8.19 +type Thm = Thm.thm
    8.20 +type Tactic = tactic;
    8.21 +
    8.22 +fun RULES_ERR{func,mesg} = Utils.ERR{module = "FastRules",func=func,mesg=mesg};
    8.23 +
    8.24 +nonfix ##;    val ## = Utils.##;      infix  4 ##; 
    8.25 +
    8.26 +fun cconcl thm = D.drop_prop(#prop(crep_thm thm));
    8.27 +fun chyps thm = map D.drop_prop(#hyps(crep_thm thm));
    8.28 +
    8.29 +fun dest_thm thm = 
    8.30 +   let val drop = S.drop_Trueprop
    8.31 +       val {prop,hyps,...} = rep_thm thm
    8.32 +   in (map drop hyps, drop prop)
    8.33 +   end;
    8.34 +
    8.35 +
    8.36 +
    8.37 +(* Inference rules *)
    8.38 +
    8.39 +(*---------------------------------------------------------------------------
    8.40 + *        Equality (one step)
    8.41 + *---------------------------------------------------------------------------*)
    8.42 +fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq;
    8.43 +fun SYM thm = thm RS sym;
    8.44 +
    8.45 +fun ALPHA thm ctm1 =
    8.46 +   let val ctm2 = cprop_of thm
    8.47 +       val ctm2_eq = reflexive ctm2
    8.48 +       val ctm1_eq = reflexive ctm1
    8.49 +   in equal_elim (transitive ctm2_eq ctm1_eq) thm
    8.50 +   end;
    8.51 +
    8.52 +val BETA_RULE = Utils.I;
    8.53 +
    8.54 +
    8.55 +(*----------------------------------------------------------------------------
    8.56 + *        Type instantiation
    8.57 + *---------------------------------------------------------------------------*)
    8.58 +fun INST_TYPE blist thm = 
    8.59 +  let val {sign,...} = rep_thm thm
    8.60 +      val blist' = map (fn (TVar(idx,_) |-> B) => (idx, ctyp_of sign B)) blist
    8.61 +  in Thm.instantiate (blist',[]) thm
    8.62 +  end
    8.63 +  handle _ => raise RULES_ERR{func = "INST_TYPE", mesg = ""};
    8.64 +
    8.65 +
    8.66 +(*----------------------------------------------------------------------------
    8.67 + *        Implication and the assumption list
    8.68 + *
    8.69 + * Assumptions get stuck on the meta-language assumption list. Implications 
    8.70 + * are in the object language, so discharging an assumption "A" from theorem
    8.71 + * "B" results in something that looks like "A --> B".
    8.72 + *---------------------------------------------------------------------------*)
    8.73 +fun ASSUME ctm = Thm.assume (D.mk_prop ctm);
    8.74 +
    8.75 +
    8.76 +(*---------------------------------------------------------------------------
    8.77 + * Implication in TFL is -->. Meta-language implication (==>) is only used
    8.78 + * in the implementation of some of the inference rules below.
    8.79 + *---------------------------------------------------------------------------*)
    8.80 +fun MP th1 th2 = th2 RS (th1 RS mp);
    8.81 +
    8.82 +fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI;
    8.83 +
    8.84 +fun DISCH_ALL thm = Utils.itlist DISCH (#hyps (crep_thm thm)) thm;
    8.85 +
    8.86 +
    8.87 +fun FILTER_DISCH_ALL P thm =
    8.88 + let fun check tm = U.holds P (S.drop_Trueprop (#t(rep_cterm tm)))
    8.89 + in  U.itlist (fn tm => fn th => if (check tm) then DISCH tm th else th)
    8.90 +              (chyps thm) thm
    8.91 + end;
    8.92 +
    8.93 +(* freezeT expensive! *)
    8.94 +fun UNDISCH thm = 
    8.95 +   let val tm = D.mk_prop(#1(D.dest_imp(cconcl (freezeT thm))))
    8.96 +   in implies_elim (thm RS mp) (ASSUME tm)
    8.97 +   end
    8.98 +   handle _ => raise RULES_ERR{func = "UNDISCH", mesg = ""};
    8.99 +
   8.100 +fun PROVE_HYP ath bth =  MP (DISCH (cconcl ath) bth) ath;
   8.101 +
   8.102 +local val [p1,p2] = goal HOL.thy "(A-->B) ==> (B --> C) ==> (A-->C)"
   8.103 +      val _ = by (rtac impI 1)
   8.104 +      val _ = by (rtac (p2 RS mp) 1)
   8.105 +      val _ = by (rtac (p1 RS mp) 1)
   8.106 +      val _ = by (assume_tac 1)
   8.107 +      val imp_trans = result()
   8.108 +in
   8.109 +fun IMP_TRANS th1 th2 = th2 RS (th1 RS imp_trans)
   8.110 +end;
   8.111 +
   8.112 +(*----------------------------------------------------------------------------
   8.113 + *        Conjunction
   8.114 + *---------------------------------------------------------------------------*)
   8.115 +fun CONJUNCT1 thm = (thm RS conjunct1)
   8.116 +fun CONJUNCT2 thm = (thm RS conjunct2);
   8.117 +fun CONJUNCTS th  = (CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th))
   8.118 +                    handle _ => [th];
   8.119 +
   8.120 +fun LIST_CONJ [] = raise RULES_ERR{func = "LIST_CONJ", mesg = "empty list"}
   8.121 +  | LIST_CONJ [th] = th
   8.122 +  | LIST_CONJ (th::rst) = MP(MP(conjI COMP (impI RS impI)) th) (LIST_CONJ rst);
   8.123 +
   8.124 +
   8.125 +(*----------------------------------------------------------------------------
   8.126 + *        Disjunction
   8.127 + *---------------------------------------------------------------------------*)
   8.128 +local val {prop,sign,...} = rep_thm disjI1
   8.129 +      val [P,Q] = term_vars prop
   8.130 +      val disj1 = forall_intr (cterm_of sign Q) disjI1
   8.131 +in
   8.132 +fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1)
   8.133 +end;
   8.134 +
   8.135 +local val {prop,sign,...} = rep_thm disjI2
   8.136 +      val [P,Q] = term_vars prop
   8.137 +      val disj2 = forall_intr (cterm_of sign P) disjI2
   8.138 +in
   8.139 +fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2)
   8.140 +end;
   8.141 +
   8.142 +
   8.143 +(*----------------------------------------------------------------------------
   8.144 + *
   8.145 + *                   A1 |- M1, ..., An |- Mn
   8.146 + *     ---------------------------------------------------
   8.147 + *     [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn]
   8.148 + *
   8.149 + *---------------------------------------------------------------------------*)
   8.150 +
   8.151 +
   8.152 +fun EVEN_ORS thms =
   8.153 +  let fun blue ldisjs [] _ = []
   8.154 +        | blue ldisjs (th::rst) rdisjs =
   8.155 +            let val tail = tl rdisjs
   8.156 +                val rdisj_tl = D.list_mk_disj tail
   8.157 +            in itlist DISJ2 ldisjs (DISJ1 th rdisj_tl)
   8.158 +               :: blue (ldisjs@[cconcl th]) rst tail
   8.159 +            end handle _ => [itlist DISJ2 ldisjs th]
   8.160 +   in
   8.161 +   blue [] thms (map cconcl thms)
   8.162 +   end;
   8.163 +
   8.164 +
   8.165 +(*----------------------------------------------------------------------------
   8.166 + *
   8.167 + *         A |- P \/ Q   B,P |- R    C,Q |- R
   8.168 + *     ---------------------------------------------------
   8.169 + *                     A U B U C |- R
   8.170 + *
   8.171 + *---------------------------------------------------------------------------*)
   8.172 +local val [p1,p2,p3] = goal HOL.thy "(P | Q) ==> (P --> R) ==> (Q --> R) ==> R"
   8.173 +      val _ = by (rtac (p1 RS disjE) 1)
   8.174 +      val _ = by (rtac (p2 RS mp) 1)
   8.175 +      val _ = by (assume_tac 1)
   8.176 +      val _ = by (rtac (p3 RS mp) 1)
   8.177 +      val _ = by (assume_tac 1)
   8.178 +      val tfl_exE = result()
   8.179 +in
   8.180 +fun DISJ_CASES th1 th2 th3 = 
   8.181 +   let val c = D.drop_prop(cconcl th1)
   8.182 +       val (disj1,disj2) = D.dest_disj c
   8.183 +       val th2' = DISCH disj1 th2
   8.184 +       val th3' = DISCH disj2 th3
   8.185 +   in
   8.186 +   th3' RS (th2' RS (th1 RS tfl_exE))
   8.187 +   end
   8.188 +end;
   8.189 +
   8.190 +
   8.191 +(*-----------------------------------------------------------------------------
   8.192 + *
   8.193 + *       |- A1 \/ ... \/ An     [A1 |- M, ..., An |- M]
   8.194 + *     ---------------------------------------------------
   8.195 + *                           |- M
   8.196 + *
   8.197 + * Note. The list of theorems may be all jumbled up, so we have to 
   8.198 + * first organize it to align with the first argument (the disjunctive 
   8.199 + * theorem).
   8.200 + *---------------------------------------------------------------------------*)
   8.201 +
   8.202 +fun organize eq =    (* a bit slow - analogous to insertion sort *)
   8.203 + let fun extract a alist =
   8.204 +     let fun ex (_,[]) = raise RULES_ERR{func = "organize",
   8.205 +                                         mesg = "not a permutation.1"}
   8.206 +           | ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t)
   8.207 +     in ex ([],alist)
   8.208 +     end
   8.209 +     fun place [] [] = []
   8.210 +       | place (a::rst) alist =
   8.211 +           let val (item,next) = extract a alist
   8.212 +           in item::place rst next
   8.213 +           end
   8.214 +       | place _ _ = raise RULES_ERR{func = "organize",
   8.215 +                                     mesg = "not a permutation.2"}
   8.216 + in place
   8.217 + end;
   8.218 +(* freezeT expensive! *)
   8.219 +fun DISJ_CASESL disjth thl =
   8.220 +   let val c = cconcl disjth
   8.221 +       fun eq th atm = exists (D.caconv atm) (chyps th)
   8.222 +       val tml = D.strip_disj c
   8.223 +       fun DL th [] = raise RULES_ERR{func="DISJ_CASESL",mesg="no cases"}
   8.224 +         | DL th [th1] = PROVE_HYP th th1
   8.225 +         | DL th [th1,th2] = DISJ_CASES th th1 th2
   8.226 +         | DL th (th1::rst) = 
   8.227 +            let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
   8.228 +             in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
   8.229 +   in DL (freezeT disjth) (organize eq tml thl)
   8.230 +   end;
   8.231 +
   8.232 +
   8.233 +(*----------------------------------------------------------------------------
   8.234 + *        Universals
   8.235 + *---------------------------------------------------------------------------*)
   8.236 +local (* this is fragile *)
   8.237 +      val {prop,sign,...} = rep_thm spec
   8.238 +      val x = hd (tl (term_vars prop))
   8.239 +      val (TVar (indx,_)) = type_of x
   8.240 +      val gspec = forall_intr (cterm_of sign x) spec
   8.241 +in
   8.242 +fun SPEC tm thm = 
   8.243 +   let val {sign,T,...} = rep_cterm tm
   8.244 +       val gspec' = instantiate([(indx,ctyp_of sign T)],[]) gspec
   8.245 +   in thm RS (forall_elim tm gspec')
   8.246 +   end
   8.247 +end;
   8.248 +
   8.249 +fun SPEC_ALL thm = rev_itlist SPEC (#1(D.strip_forall(cconcl thm))) thm;
   8.250 +
   8.251 +val ISPEC = SPEC
   8.252 +val ISPECL = rev_itlist ISPEC;
   8.253 +
   8.254 +(* Not optimized! Too complicated. *)
   8.255 +local val {prop,sign,...} = rep_thm allI
   8.256 +      val [P] = add_term_vars (prop, [])
   8.257 +      fun cty_theta s = map (fn (i,ty) => (i, ctyp_of s ty))
   8.258 +      fun ctm_theta s = map (fn (i,tm2) => 
   8.259 +                             let val ctm2 = cterm_of s tm2
   8.260 +                             in (cterm_of s (Var(i,#T(rep_cterm ctm2))), ctm2)
   8.261 +                             end)
   8.262 +      fun certify s (ty_theta,tm_theta) = (cty_theta s ty_theta, 
   8.263 +                                           ctm_theta s tm_theta)
   8.264 +in
   8.265 +fun GEN v th =
   8.266 +   let val gth = forall_intr v th
   8.267 +       val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth
   8.268 +       val P' = Abs(x,ty, S.drop_Trueprop rst)  (* get rid of trueprop *)
   8.269 +       val tsig = #tsig(Sign.rep_sg sign)
   8.270 +       val theta = Pattern.match tsig (P,P')
   8.271 +       val allI2 = instantiate (certify sign theta) allI
   8.272 +       val thm = implies_elim allI2 gth
   8.273 +       val {prop = tp $ (A $ Abs(_,_,M)),sign,...} = rep_thm thm
   8.274 +       val prop' = tp $ (A $ Abs(x,ty,M))
   8.275 +   in ALPHA thm (cterm_of sign prop')
   8.276 +   end
   8.277 +end;
   8.278 +
   8.279 +val GENL = itlist GEN;
   8.280 +
   8.281 +fun GEN_ALL thm = 
   8.282 +   let val {prop,sign,...} = rep_thm thm
   8.283 +       val tycheck = cterm_of sign
   8.284 +       val vlist = map tycheck (add_term_vars (prop, []))
   8.285 +  in GENL vlist thm
   8.286 +  end;
   8.287 +
   8.288 +
   8.289 +local fun string_of(s,_) = s
   8.290 +in
   8.291 +fun freeze th =
   8.292 +  let val fth = freezeT th
   8.293 +      val {prop,sign,...} = rep_thm fth
   8.294 +      fun mk_inst (Var(v,T)) = 
   8.295 +	  (cterm_of sign (Var(v,T)),
   8.296 +	   cterm_of sign (Free(string_of v, T)))
   8.297 +      val insts = map mk_inst (term_vars prop)
   8.298 +  in  instantiate ([],insts) fth  
   8.299 +  end
   8.300 +end;
   8.301 +
   8.302 +fun MATCH_MP th1 th2 = 
   8.303 +   if (D.is_forall (D.drop_prop(cconcl th1)))
   8.304 +   then MATCH_MP (th1 RS spec) th2
   8.305 +   else MP th1 th2;
   8.306 +
   8.307 +
   8.308 +(*----------------------------------------------------------------------------
   8.309 + *        Existentials
   8.310 + *---------------------------------------------------------------------------*)
   8.311 +
   8.312 +
   8.313 +
   8.314 +(*--------------------------------------------------------------------------- 
   8.315 + * Existential elimination
   8.316 + *
   8.317 + *      A1 |- ?x.t[x]   ,   A2, "t[v]" |- t'
   8.318 + *      ------------------------------------     (variable v occurs nowhere)
   8.319 + *                A1 u A2 |- t'
   8.320 + *
   8.321 + *---------------------------------------------------------------------------*)
   8.322 +
   8.323 +local val [p1,p2] = goal HOL.thy "(? x. P x) ==> (!x. P x --> Q) ==> Q"
   8.324 +      val _ = by (rtac (p1 RS exE) 1)
   8.325 +      val _ = by (rtac ((p2 RS allE) RS mp) 1)
   8.326 +      val _ = by (assume_tac 2)
   8.327 +      val _ = by (assume_tac 1)
   8.328 +      val choose_thm = result()
   8.329 +in
   8.330 +fun CHOOSE(fvar,exth) fact =
   8.331 +   let val lam = #2(dest_comb(D.drop_prop(cconcl exth)))
   8.332 +       val redex = capply lam fvar
   8.333 +       val {sign,t,...} = rep_cterm redex
   8.334 +       val residue = cterm_of sign (S.beta_conv t)
   8.335 +    in GEN fvar (DISCH residue fact)  RS (exth RS choose_thm)
   8.336 +   end
   8.337 +end;
   8.338 +
   8.339 +
   8.340 +local val {prop,sign,...} = rep_thm exI
   8.341 +      val [P,x] = term_vars prop
   8.342 +in
   8.343 +fun EXISTS (template,witness) thm =
   8.344 +   let val {prop,sign,...} = rep_thm thm
   8.345 +       val P' = cterm_of sign P
   8.346 +       val x' = cterm_of sign x
   8.347 +       val abstr = #2(dest_comb template)
   8.348 +   in
   8.349 +   thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)
   8.350 +   end
   8.351 +end;
   8.352 +
   8.353 +(*----------------------------------------------------------------------------
   8.354 + *
   8.355 + *         A |- M
   8.356 + *   -------------------   [v_1,...,v_n]
   8.357 + *    A |- ?v1...v_n. M
   8.358 + *
   8.359 + *---------------------------------------------------------------------------*)
   8.360 +
   8.361 +fun EXISTL vlist th = 
   8.362 +  U.itlist (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm)
   8.363 +           vlist th;
   8.364 +
   8.365 +
   8.366 +(*----------------------------------------------------------------------------
   8.367 + *
   8.368 + *       A |- M[x_1,...,x_n]
   8.369 + *   ----------------------------   [(x |-> y)_1,...,(x |-> y)_n]
   8.370 + *       A |- ?y_1...y_n. M
   8.371 + *
   8.372 + *---------------------------------------------------------------------------*)
   8.373 +(* Could be improved, but needs "subst" for certified terms *)
   8.374 +
   8.375 +fun IT_EXISTS blist th = 
   8.376 +   let val {sign,...} = rep_thm th
   8.377 +       val tych = cterm_of sign
   8.378 +       val detype = #t o rep_cterm
   8.379 +       val blist' = map (fn (x|->y) => (detype x |-> detype y)) blist
   8.380 +       fun ?v M  = cterm_of sign (S.mk_exists{Bvar=v,Body = M})
   8.381 +       
   8.382 +  in
   8.383 +  U.itlist (fn (b as (r1 |-> r2)) => fn thm => 
   8.384 +        EXISTS(?r2(S.subst[b] (S.drop_Trueprop(#prop(rep_thm thm)))), tych r1)
   8.385 +              thm)
   8.386 +       blist' th
   8.387 +  end;
   8.388 +
   8.389 +(*---------------------------------------------------------------------------
   8.390 + *  Faster version, that fails for some as yet unknown reason
   8.391 + * fun IT_EXISTS blist th = 
   8.392 + *    let val {sign,...} = rep_thm th
   8.393 + *        val tych = cterm_of sign
   8.394 + *        fun detype (x |-> y) = ((#t o rep_cterm) x |-> (#t o rep_cterm) y)
   8.395 + *   in
   8.396 + *  fold (fn (b as (r1|->r2), thm) => 
   8.397 + *  EXISTS(D.mk_exists(r2, tych(S.subst[detype b](#t(rep_cterm(cconcl thm))))),
   8.398 + *           r1) thm)  blist th
   8.399 + *   end;
   8.400 + *---------------------------------------------------------------------------*)
   8.401 +
   8.402 +(*----------------------------------------------------------------------------
   8.403 + *        Rewriting
   8.404 + *---------------------------------------------------------------------------*)
   8.405 +
   8.406 +fun SUBS thl = 
   8.407 +   rewrite_rule (map (fn th => (th RS eq_reflection) handle _ => th) thl);
   8.408 +
   8.409 +val simplify = rewrite_rule;
   8.410 +
   8.411 +local fun rew_conv mss = rewrite_cterm (true,false) mss (K(K None))
   8.412 +in
   8.413 +fun simpl_conv thl ctm = 
   8.414 + rew_conv (Thm.mss_of (#simps(rep_ss HOL_ss)@thl)) ctm
   8.415 + RS meta_eq_to_obj_eq
   8.416 +end;
   8.417 +
   8.418 +local fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1])
   8.419 +in
   8.420 +val RIGHT_ASSOC = rewrite_rule [prover"((a|b)|c) = (a|(b|c))" RS eq_reflection]
   8.421 +val ASM = refl RS iffD1
   8.422 +end;
   8.423 +
   8.424 +
   8.425 +
   8.426 +
   8.427 +(*---------------------------------------------------------------------------
   8.428 + *                  TERMINATION CONDITION EXTRACTION
   8.429 + *---------------------------------------------------------------------------*)
   8.430 +
   8.431 +
   8.432 +
   8.433 +val bool = S.bool
   8.434 +val prop = Type("prop",[]);
   8.435 +
   8.436 +(* Object language quantifier, i.e., "!" *)
   8.437 +fun Forall v M = S.mk_forall{Bvar=v, Body=M};
   8.438 +
   8.439 +
   8.440 +(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
   8.441 +fun is_cong thm = 
   8.442 +  let val {prop, ...} = rep_thm thm
   8.443 +  in case prop 
   8.444 +     of (Const("==>",_)$(Const("Trueprop",_)$ _) $
   8.445 +         (Const("==",_) $ (Const ("cut",_) $ f $ R $ a $ x) $ _)) => false
   8.446 +      | _ => true
   8.447 +  end;
   8.448 +
   8.449 +
   8.450 +   
   8.451 +fun dest_equal(Const ("==",_) $ 
   8.452 +              (Const ("Trueprop",_) $ lhs) 
   8.453 +            $ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs}
   8.454 +  | dest_equal(Const ("==",_) $ lhs $ rhs)  = {lhs=lhs, rhs=rhs}
   8.455 +  | dest_equal tm = S.dest_eq tm;
   8.456 +
   8.457 +
   8.458 +fun get_rhs tm = #rhs(dest_equal (S.drop_Trueprop tm));
   8.459 +fun get_lhs tm = #lhs(dest_equal (S.drop_Trueprop tm));
   8.460 +
   8.461 +fun variants FV vlist =
   8.462 +  rev(#1(U.rev_itlist (fn v => fn (V,W) =>
   8.463 +                        let val v' = S.variant W v
   8.464 +                        in (v'::V, v'::W) end) 
   8.465 +                     vlist ([],FV)));
   8.466 +
   8.467 +
   8.468 +fun dest_all(Const("all",_) $ (a as Abs _)) = S.dest_abs a
   8.469 +  | dest_all _ = raise RULES_ERR{func = "dest_all", mesg = "not a !!"};
   8.470 +
   8.471 +val is_all = Utils.can dest_all;
   8.472 +
   8.473 +fun strip_all fm =
   8.474 +   if (is_all fm)
   8.475 +   then let val {Bvar,Body} = dest_all fm
   8.476 +            val (bvs,core)  = strip_all Body
   8.477 +        in ((Bvar::bvs), core)
   8.478 +        end
   8.479 +   else ([],fm);
   8.480 +
   8.481 +fun break_all(Const("all",_) $ Abs (_,_,body)) = body
   8.482 +  | break_all _ = raise RULES_ERR{func = "break_all", mesg = "not a !!"};
   8.483 +
   8.484 +fun list_break_all(Const("all",_) $ Abs (s,ty,body)) = 
   8.485 +     let val (L,core) = list_break_all body
   8.486 +     in ((s,ty)::L, core)
   8.487 +     end
   8.488 +  | list_break_all tm = ([],tm);
   8.489 +
   8.490 +(*---------------------------------------------------------------------------
   8.491 + * Rename a term of the form
   8.492 + *
   8.493 + *      !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn 
   8.494 + *                  ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn.
   8.495 + * to one of
   8.496 + *
   8.497 + *      !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn 
   8.498 + *      ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn.
   8.499 + * 
   8.500 + * This prevents name problems in extraction, and helps the result to read
   8.501 + * better. There is a problem with varstructs, since they can introduce more
   8.502 + * than n variables, and some extra reasoning needs to be done.
   8.503 + *---------------------------------------------------------------------------*)
   8.504 +
   8.505 +fun get ([],_,L) = rev L
   8.506 +  | get (ant::rst,n,L) =  
   8.507 +      case (list_break_all ant)
   8.508 +        of ([],_) => get (rst, n+1,L)
   8.509 +         | (vlist,body) =>
   8.510 +            let val eq = Logic.strip_imp_concl body
   8.511 +                val (f,args) = S.strip_comb (get_lhs eq)
   8.512 +                val (vstrl,_) = S.strip_abs f
   8.513 +                val names  = map (#Name o S.dest_var)
   8.514 +                                 (variants (S.free_vars body) vstrl)
   8.515 +            in get (rst, n+1, (names,n)::L)
   8.516 +            end handle _ => get (rst, n+1, L);
   8.517 +
   8.518 +(* Note: rename_params_rule counts from 1, not 0 *)
   8.519 +fun rename thm = 
   8.520 +  let val {prop,sign,...} = rep_thm thm
   8.521 +      val tych = cterm_of sign
   8.522 +      val ants = Logic.strip_imp_prems prop
   8.523 +      val news = get (ants,1,[])
   8.524 +  in 
   8.525 +  U.rev_itlist rename_params_rule news thm
   8.526 +  end;
   8.527 +
   8.528 +
   8.529 +(*---------------------------------------------------------------------------
   8.530 + * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml)
   8.531 + *---------------------------------------------------------------------------*)
   8.532 +
   8.533 +fun list_beta_conv tm =
   8.534 +  let fun rbeta th = transitive th (beta_conversion(#2(D.dest_eq(cconcl th))))
   8.535 +      fun iter [] = reflexive tm
   8.536 +        | iter (v::rst) = rbeta (combination(iter rst) (reflexive v))
   8.537 +  in iter  end;
   8.538 +
   8.539 +
   8.540 +(*---------------------------------------------------------------------------
   8.541 + * Trace information for the rewriter
   8.542 + *---------------------------------------------------------------------------*)
   8.543 +val term_ref = ref[] : term list ref
   8.544 +val mss_ref = ref [] : meta_simpset list ref;
   8.545 +val thm_ref = ref [] : thm list ref;
   8.546 +val tracing = ref false;
   8.547 +
   8.548 +fun say s = if !tracing then (output(std_out,s); flush_out std_out) else ();
   8.549 +
   8.550 +fun print_thms s L = 
   8.551 +   (say s; 
   8.552 +    map (fn th => say (string_of_thm th ^"\n")) L;
   8.553 +    say"\n");
   8.554 +
   8.555 +fun print_cterms s L = 
   8.556 +   (say s; 
   8.557 +    map (fn th => say (string_of_cterm th ^"\n")) L;
   8.558 +    say"\n");
   8.559 +
   8.560 +(*---------------------------------------------------------------------------
   8.561 + * General abstraction handlers, should probably go in USyntax.
   8.562 + *---------------------------------------------------------------------------*)
   8.563 +fun mk_aabs(vstr,body) = S.mk_abs{Bvar=vstr,Body=body}
   8.564 +                         handle _ => S.mk_pabs{varstruct = vstr, body = body};
   8.565 +
   8.566 +fun list_mk_aabs (vstrl,tm) =
   8.567 +    U.itlist (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
   8.568 +
   8.569 +fun dest_aabs tm = 
   8.570 +   let val {Bvar,Body} = S.dest_abs tm
   8.571 +   in (Bvar,Body)
   8.572 +   end handle _ => let val {varstruct,body} = S.dest_pabs tm
   8.573 +                   in (varstruct,body)
   8.574 +                   end;
   8.575 +
   8.576 +fun strip_aabs tm =
   8.577 +   let val (vstr,body) = dest_aabs tm
   8.578 +       val (bvs, core) = strip_aabs body
   8.579 +   in (vstr::bvs, core)
   8.580 +   end
   8.581 +   handle _ => ([],tm);
   8.582 +
   8.583 +fun dest_combn tm 0 = (tm,[])
   8.584 +  | dest_combn tm n = 
   8.585 +     let val {Rator,Rand} = S.dest_comb tm
   8.586 +         val (f,rands) = dest_combn Rator (n-1)
   8.587 +     in (f,Rand::rands)
   8.588 +     end;
   8.589 +
   8.590 +
   8.591 +
   8.592 +
   8.593 +local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
   8.594 +      fun mk_fst tm = 
   8.595 +          let val ty = S.type_of tm
   8.596 +              val {Tyop="*",Args=[fty,sty]} = S.dest_type ty
   8.597 +              val fst = S.mk_const{Name="fst",Ty = ty --> fty}
   8.598 +          in S.mk_comb{Rator=fst, Rand=tm}
   8.599 +          end
   8.600 +      fun mk_snd tm = 
   8.601 +          let val ty = S.type_of tm
   8.602 +              val {Tyop="*",Args=[fty,sty]} = S.dest_type ty
   8.603 +              val snd = S.mk_const{Name="snd",Ty = ty --> sty}
   8.604 +          in S.mk_comb{Rator=snd, Rand=tm}
   8.605 +          end
   8.606 +in
   8.607 +fun XFILL tych x vstruct = 
   8.608 +  let fun traverse p xocc L =
   8.609 +        if (S.is_var p)
   8.610 +        then tych xocc::L
   8.611 +        else let val (p1,p2) = dest_pair p
   8.612 +             in traverse p1 (mk_fst xocc) (traverse p2  (mk_snd xocc) L)
   8.613 +             end
   8.614 +  in 
   8.615 +  traverse vstruct x []
   8.616 +end end;
   8.617 +
   8.618 +(*---------------------------------------------------------------------------
   8.619 + * Replace a free tuple (vstr) by a universally quantified variable (a).
   8.620 + * Note that the notion of "freeness" for a tuple is different than for a
   8.621 + * variable: if variables in the tuple also occur in any other place than
   8.622 + * an occurrences of the tuple, they aren't "free" (which is thus probably
   8.623 + *  the wrong word to use).
   8.624 + *---------------------------------------------------------------------------*)
   8.625 +
   8.626 +fun VSTRUCT_ELIM tych a vstr th = 
   8.627 +  let val L = S.free_vars_lr vstr
   8.628 +      val bind1 = tych (S.mk_prop (S.mk_eq{lhs=a, rhs=vstr}))
   8.629 +      val thm1 = implies_intr bind1 (SUBS [SYM(assume bind1)] th)
   8.630 +      val thm2 = forall_intr_list (map tych L) thm1
   8.631 +      val thm3 = forall_elim_list (XFILL tych a vstr) thm2
   8.632 +  in refl RS
   8.633 +     rewrite_rule[symmetric (surjective_pairing RS eq_reflection)] thm3
   8.634 +  end;
   8.635 +
   8.636 +fun PGEN tych a vstr th = 
   8.637 +  let val a1 = tych a
   8.638 +      val vstr1 = tych vstr
   8.639 +  in
   8.640 +  forall_intr a1 
   8.641 +     (if (S.is_var vstr) 
   8.642 +      then cterm_instantiate [(vstr1,a1)] th
   8.643 +      else VSTRUCT_ELIM tych a vstr th)
   8.644 +  end;
   8.645 +
   8.646 +
   8.647 +(*---------------------------------------------------------------------------
   8.648 + * Takes apart a paired beta-redex, looking like "(\(x,y).N) vstr", into
   8.649 + *
   8.650 + *     (([x,y],N),vstr)
   8.651 + *---------------------------------------------------------------------------*)
   8.652 +fun dest_pbeta_redex M n = 
   8.653 +  let val (f,args) = dest_combn M n
   8.654 +      val _ = dest_aabs f
   8.655 +  in (strip_aabs f,args)
   8.656 +  end;
   8.657 +
   8.658 +fun pbeta_redex M n = U.can (U.C dest_pbeta_redex n) M;
   8.659 +
   8.660 +fun dest_impl tm = 
   8.661 +  let val ants = Logic.strip_imp_prems tm
   8.662 +      val eq = Logic.strip_imp_concl tm
   8.663 +  in (ants,get_lhs eq)
   8.664 +  end;
   8.665 +
   8.666 +val pbeta_reduce = simpl_conv [split RS eq_reflection];
   8.667 +val restricted = U.can(S.find_term
   8.668 +                       (U.holds(fn c => (#Name(S.dest_const c)="cut"))))
   8.669 +
   8.670 +fun CONTEXT_REWRITE_RULE(func,R){thms=[cut_lemma],congs,th} =
   8.671 + let val tc_list = ref[]: term list ref
   8.672 +     val _ = term_ref := []
   8.673 +     val _ = thm_ref  := []
   8.674 +     val _ = mss_ref  := []
   8.675 +     val cut_lemma' = (cut_lemma RS mp) RS eq_reflection
   8.676 +     fun prover mss thm =
   8.677 +     let fun cong_prover mss thm =
   8.678 +         let val _ = say "cong_prover:\n"
   8.679 +             val cntxt = prems_of_mss mss
   8.680 +             val _ = print_thms "cntxt:\n" cntxt
   8.681 +             val _ = say "cong rule:\n"
   8.682 +             val _ = say (string_of_thm thm^"\n")
   8.683 +             val _ = thm_ref := (thm :: !thm_ref)
   8.684 +             val _ = mss_ref := (mss :: !mss_ref)
   8.685 +             (* Unquantified eliminate *)
   8.686 +             fun uq_eliminate (thm,imp,sign) = 
   8.687 +                 let val tych = cterm_of sign
   8.688 +                     val _ = print_cterms "To eliminate:\n" [tych imp]
   8.689 +                     val ants = map tych (Logic.strip_imp_prems imp)
   8.690 +                     val eq = Logic.strip_imp_concl imp
   8.691 +                     val lhs = tych(get_lhs eq)
   8.692 +                     val mss' = add_prems(mss, map ASSUME ants)
   8.693 +                     val lhs_eq_lhs1 = rewrite_cterm(false,true)mss' prover lhs
   8.694 +                       handle _ => reflexive lhs
   8.695 +                     val _ = print_thms "proven:\n" [lhs_eq_lhs1]
   8.696 +                     val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
   8.697 +                     val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
   8.698 +                  in
   8.699 +                  lhs_eeq_lhs2 COMP thm
   8.700 +                  end
   8.701 +             fun pq_eliminate (thm,sign,vlist,imp_body,lhs_eq) =
   8.702 +              let val ((vstrl,_),args) = dest_pbeta_redex lhs_eq(length vlist)
   8.703 +                  val true = forall (fn (tm1,tm2) => S.aconv tm1 tm2)
   8.704 +                                   (Utils.zip vlist args)
   8.705 +(*                val fbvs1 = variants (S.free_vars imp) fbvs *)
   8.706 +                  val imp_body1 = S.subst (map (op|->) (U.zip args vstrl))
   8.707 +                                          imp_body
   8.708 +                  val tych = cterm_of sign
   8.709 +                  val ants1 = map tych (Logic.strip_imp_prems imp_body1)
   8.710 +                  val eq1 = Logic.strip_imp_concl imp_body1
   8.711 +                  val Q = get_lhs eq1
   8.712 +                  val QeqQ1 = pbeta_reduce (tych Q)
   8.713 +                  val Q1 = #2(D.dest_eq(cconcl QeqQ1))
   8.714 +                  val mss' = add_prems(mss, map ASSUME ants1)
   8.715 +                  val Q1eeqQ2 = rewrite_cterm (false,true) mss' prover Q1
   8.716 +                                handle _ => reflexive Q1
   8.717 +                  val Q2 = get_rhs(S.drop_Trueprop(#prop(rep_thm Q1eeqQ2)))
   8.718 +                  val Q3 = tych(S.list_mk_comb(list_mk_aabs(vstrl,Q2),vstrl))
   8.719 +                  val Q2eeqQ3 = symmetric(pbeta_reduce Q3 RS eq_reflection)
   8.720 +                  val thA = transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
   8.721 +                  val QeeqQ3 = transitive thA Q2eeqQ3 handle _ =>
   8.722 +                               ((Q2eeqQ3 RS meta_eq_to_obj_eq) 
   8.723 +                                RS ((thA RS meta_eq_to_obj_eq) RS trans))
   8.724 +                                RS eq_reflection
   8.725 +                  val impth = implies_intr_list ants1 QeeqQ3
   8.726 +                  val impth1 = impth RS meta_eq_to_obj_eq
   8.727 +                  (* Need to abstract *)
   8.728 +                  val ant_th = U.itlist2 (PGEN tych) args vstrl impth1
   8.729 +              in ant_th COMP thm
   8.730 +              end
   8.731 +             fun q_eliminate (thm,imp,sign) =
   8.732 +              let val (vlist,imp_body) = strip_all imp
   8.733 +                  val (ants,Q) = dest_impl imp_body
   8.734 +              in if (pbeta_redex Q) (length vlist)
   8.735 +                 then pq_eliminate (thm,sign,vlist,imp_body,Q)
   8.736 +                 else 
   8.737 +                 let val tych = cterm_of sign
   8.738 +                     val ants1 = map tych ants
   8.739 +                     val mss' = add_prems(mss, map ASSUME ants1)
   8.740 +                     val Q_eeq_Q1 = rewrite_cterm(false,true) mss' 
   8.741 +                                                     prover (tych Q)
   8.742 +                      handle _ => reflexive (tych Q)
   8.743 +                     val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
   8.744 +                     val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
   8.745 +                     val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
   8.746 +                 in
   8.747 +                 ant_th COMP thm
   8.748 +              end end
   8.749 +
   8.750 +             fun eliminate thm = 
   8.751 +               case (rep_thm thm)
   8.752 +               of {prop = (Const("==>",_) $ imp $ _), sign, ...} =>
   8.753 +                   eliminate
   8.754 +                    (if not(is_all imp)
   8.755 +                     then uq_eliminate (thm,imp,sign)
   8.756 +                     else q_eliminate (thm,imp,sign))
   8.757 +                            (* Assume that the leading constant is ==,   *)
   8.758 +                | _ => thm  (* if it is not a ==>                        *)
   8.759 +         in Some(eliminate (rename thm))
   8.760 +         end handle _ => None
   8.761 +
   8.762 +        fun restrict_prover mss thm =
   8.763 +          let val _ = say "restrict_prover:\n"
   8.764 +              val cntxt = rev(prems_of_mss mss)
   8.765 +              val _ = print_thms "cntxt:\n" cntxt
   8.766 +              val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
   8.767 +                   sign,...} = rep_thm thm
   8.768 +              fun genl tm = let val vlist = U.set_diff (U.curry(op aconv))
   8.769 +                                           (add_term_frees(tm,[])) [func,R]
   8.770 +                            in U.itlist Forall vlist tm
   8.771 +                            end
   8.772 +              (*--------------------------------------------------------------
   8.773 +               * This actually isn't quite right, since it will think that
   8.774 +               * not-fully applied occs. of "f" in the context mean that the
   8.775 +               * current call is nested. The real solution is to pass in a
   8.776 +               * term "f v1..vn" which is a pattern that any full application
   8.777 +               * of "f" will match.
   8.778 +               *-------------------------------------------------------------*)
   8.779 +              val func_name = #Name(S.dest_const func handle _ => 
   8.780 +                                    S.dest_var func)
   8.781 +              fun is_func tm = (#Name(S.dest_const tm handle _ =>
   8.782 +                                      S.dest_var tm) = func_name)
   8.783 +                               handle _ => false
   8.784 +              val nested = U.can(S.find_term is_func)
   8.785 +              val rcontext = rev cntxt
   8.786 +              val cncl = S.drop_Trueprop o #prop o rep_thm
   8.787 +              val antl = case rcontext of [] => [] 
   8.788 +                         | _   => [S.list_mk_conj(map cncl rcontext)]
   8.789 +              val TC = genl(S.list_mk_imp(antl, A))
   8.790 +              val _ = print_cterms "func:\n" [cterm_of sign func]
   8.791 +              val _ = print_cterms "TC:\n" [cterm_of sign (S.mk_prop TC)]
   8.792 +              val _ = tc_list := (TC :: !tc_list)
   8.793 +              val nestedp = nested TC
   8.794 +              val _ = if nestedp then say "nested\n" else say "not_nested\n"
   8.795 +              val _ = term_ref := ([func,TC]@(!term_ref))
   8.796 +              val th' = if nestedp then raise RULES_ERR{func = "solver", 
   8.797 +                                                      mesg = "nested function"}
   8.798 +                        else let val cTC = cterm_of sign (S.mk_prop TC)
   8.799 +                             in case rcontext of
   8.800 +                                [] => SPEC_ALL(ASSUME cTC)
   8.801 +                               | _ => MP (SPEC_ALL (ASSUME cTC)) 
   8.802 +                                         (LIST_CONJ rcontext)
   8.803 +                             end
   8.804 +              val th'' = th' RS thm
   8.805 +          in Some (th'')
   8.806 +          end handle _ => None
   8.807 +    in
   8.808 +    (if (is_cong thm) then cong_prover else restrict_prover) mss thm
   8.809 +    end
   8.810 +    val ctm = cprop_of th
   8.811 +    val th1 = rewrite_cterm(false,true) (add_congs(mss_of [cut_lemma'], congs))
   8.812 +                            prover ctm
   8.813 +    val th2 = equal_elim th1 th
   8.814 + in
   8.815 + (th2, U.filter (not o restricted) (!tc_list))
   8.816 + end;
   8.817 +
   8.818 +
   8.819 +
   8.820 +fun prove (tm,tac) = 
   8.821 +  let val {t,sign,...} = rep_cterm tm
   8.822 +      val ptm = cterm_of sign(S.mk_prop t)
   8.823 +  in
   8.824 +  freeze(prove_goalw_cterm [] ptm (fn _ => [tac]))
   8.825 +  end;
   8.826 +
   8.827 +
   8.828 +end; (* Rules *)
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/TFL/rules.sig	Fri Oct 18 12:41:04 1996 +0200
     9.3 @@ -0,0 +1,65 @@
     9.4 +signature Rules_sig =
     9.5 +sig
     9.6 +(*  structure USyntax : USyntax_sig *)
     9.7 +  type Type
     9.8 +  type Preterm
     9.9 +  type Term
    9.10 +  type Thm
    9.11 +  type Tactic
    9.12 +  type 'a binding
    9.13 +
    9.14 +  val dest_thm : Thm -> Preterm list * Preterm
    9.15 +
    9.16 +  (* Inference rules *)
    9.17 +  val REFL      :Term -> Thm
    9.18 +  val ASSUME    :Term -> Thm
    9.19 +  val MP        :Thm -> Thm -> Thm
    9.20 +  val MATCH_MP  :Thm -> Thm -> Thm
    9.21 +  val CONJUNCT1 :Thm -> Thm
    9.22 +  val CONJUNCT2 :Thm -> Thm
    9.23 +  val CONJUNCTS :Thm -> Thm list
    9.24 +  val DISCH     :Term -> Thm -> Thm
    9.25 +  val UNDISCH   :Thm  -> Thm
    9.26 +  val INST_TYPE :Type binding list -> Thm -> Thm
    9.27 +  val SPEC      :Term -> Thm -> Thm
    9.28 +  val ISPEC     :Term -> Thm -> Thm
    9.29 +  val ISPECL    :Term list -> Thm -> Thm
    9.30 +  val GEN       :Term -> Thm -> Thm
    9.31 +  val GENL      :Term list -> Thm -> Thm
    9.32 +  val BETA_RULE :Thm -> Thm
    9.33 +  val LIST_CONJ :Thm list -> Thm
    9.34 +
    9.35 +  val SYM : Thm -> Thm
    9.36 +  val DISCH_ALL : Thm -> Thm
    9.37 +  val FILTER_DISCH_ALL : (Preterm -> bool) -> Thm -> Thm
    9.38 +  val SPEC_ALL  : Thm -> Thm
    9.39 +  val GEN_ALL   : Thm -> Thm
    9.40 +  val IMP_TRANS : Thm -> Thm -> Thm
    9.41 +  val PROVE_HYP : Thm -> Thm -> Thm
    9.42 +
    9.43 +  val CHOOSE : Term * Thm -> Thm -> Thm
    9.44 +  val EXISTS : Term * Term -> Thm -> Thm
    9.45 +  val EXISTL : Term list -> Thm -> Thm
    9.46 +  val IT_EXISTS : Term binding list -> Thm -> Thm
    9.47 +
    9.48 +  val EVEN_ORS : Thm list -> Thm list
    9.49 +  val DISJ_CASESL : Thm -> Thm list -> Thm
    9.50 +
    9.51 +  val SUBS : Thm list -> Thm -> Thm
    9.52 +  val simplify : Thm list -> Thm -> Thm
    9.53 +  val simpl_conv : Thm list -> Term -> Thm
    9.54 +
    9.55 +(* For debugging my isabelle solver in the conditional rewriter *)
    9.56 +(*
    9.57 +  val term_ref : Preterm list ref
    9.58 +  val thm_ref : Thm list ref
    9.59 +  val mss_ref : meta_simpset list ref
    9.60 +  val tracing :bool ref
    9.61 +*)
    9.62 +  val CONTEXT_REWRITE_RULE : Preterm * Preterm
    9.63 +                             -> {thms:Thm list,congs: Thm list, th:Thm} 
    9.64 +                             -> Thm * Preterm list
    9.65 +  val RIGHT_ASSOC : Thm -> Thm 
    9.66 +
    9.67 +  val prove : Term * Tactic -> Thm
    9.68 +end;
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/TFL/sys.sml	Fri Oct 18 12:41:04 1996 +0200
    10.3 @@ -0,0 +1,48 @@
    10.4 +(* Compile the TFL system *)
    10.5 +
    10.6 +(* Portability stuff *)
    10.7 +nonfix prefix;
    10.8 +use"mask.sig";
    10.9 +use"mask.sml";
   10.10 +
   10.11 +(* Establish a base of common and/or helpful functions. *)
   10.12 +use "utils.sig";
   10.13 +use "utils.sml";
   10.14 +
   10.15 +(* Get the specifications - these are independent of any system *)
   10.16 +use "usyntax.sig";
   10.17 +use "rules.sig";
   10.18 +use "thry.sig";
   10.19 +use "thms.sig";
   10.20 +use "tfl.sig";
   10.21 +
   10.22 +(*----------------------------------------------------------------------------
   10.23 + * Load the TFL functor - this is defined totally in terms of the 
   10.24 + * above interfaces.
   10.25 + *---------------------------------------------------------------------------*)
   10.26 +
   10.27 +use "tfl.sml";
   10.28 +
   10.29 +structure Utils = UTILS(val int_to_string = string_of_int);
   10.30 +
   10.31 +(*----------------------------------------------------------------------------
   10.32 + *      Supply implementations
   10.33 + *---------------------------------------------------------------------------*)
   10.34 +
   10.35 +val _ = use_thy"WF1";          (* Wellfoundedness theory *)
   10.36 +
   10.37 +use "usyntax.sml";
   10.38 +use "thms.sml";
   10.39 +use"dcterm.sml"; use"rules.new.sml";
   10.40 +use "thry.sml";
   10.41 +
   10.42 +
   10.43 +(*----------------------------------------------------------------------------
   10.44 + *      Link system and specialize for Isabelle 
   10.45 + *---------------------------------------------------------------------------*)
   10.46 +structure Prim = TFL(structure Rules = FastRules 
   10.47 +                     structure Thms  = Thms
   10.48 +                     structure Thry  = Thry);
   10.49 +
   10.50 +use"post.sml";
   10.51 +
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/TFL/test.sml	Fri Oct 18 12:41:04 1996 +0200
    11.3 @@ -0,0 +1,301 @@
    11.4 +fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[])));
    11.5 +fun read thy = term_of o cread thy;
    11.6 +fun Term s = read WF1.thy s;
    11.7 +
    11.8 +fun Rfunc thy R eqs =
    11.9 +   let val {induction,rules,theory,tcs} = 
   11.10 +              timeit(fn () => Tfl.Rfunction thy (read thy R) (read thy eqs))
   11.11 +   in {induction=induction, rules=rules, theory=theory, 
   11.12 +       tcs = map (cterm_of (sign_of theory)) tcs}
   11.13 +   end;
   11.14 +
   11.15 +val Rfunction = Rfunc WF1.thy;
   11.16 +
   11.17 +fun function tm = timeit (fn () => Tfl.function WF1.thy (Term tm));
   11.18 +
   11.19 +
   11.20 +(*---------------------------------------------------------------------------
   11.21 + * Factorial. Notice how functions without pattern matching are often harder 
   11.22 + * to deal with than those with! Unfortunately, not all functions can be 
   11.23 + * described purely by pattern matching, e.g., "variant" as below.
   11.24 + *---------------------------------------------------------------------------*)
   11.25 +function "fact x = (if (x = 0) then Suc 0 else x * fact (x - Suc 0))";
   11.26 +
   11.27 +Rfunction"pred_nat"
   11.28 +         "fact x = (if (x = 0) then Suc 0 else x * fact (x - Suc 0))";
   11.29 +
   11.30 +function "(Fact 0 = (Suc 0)) & \
   11.31 +     \    (Fact (Suc x) = (Fact x * Suc x))";
   11.32 +
   11.33 +Rfunction "pred_nat"
   11.34 +          "(Fact 0 = (Suc 0)) & \
   11.35 +      \    (Fact (Suc x) = (Fact x * Suc x))";
   11.36 +
   11.37 +(*---------------------------------------------------------------------------
   11.38 + * Fibonacci.
   11.39 + *---------------------------------------------------------------------------*)
   11.40 +function "(Fib 0 = (Suc 0)) &  \
   11.41 +     \    (Fib (Suc 0) = (Suc 0)) & \
   11.42 +     \    (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))";
   11.43 +
   11.44 +(* "<" doesn't currently work smoothly *)
   11.45 +Rfunction"{p::(nat*nat). fst p < snd p}"
   11.46 +         "(Fib 0 = (Suc 0)) & \
   11.47 +     \    (Fib (Suc 0) = (Suc 0)) & \
   11.48 +     \    (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))";
   11.49 +
   11.50 +
   11.51 +(* "trancl pred" means "<" and works better *)
   11.52 +Rfunction"trancl pred_nat"
   11.53 +         "(Fib 0 = (Suc 0)) & \
   11.54 +     \    (Fib (Suc 0) = (Suc 0)) & \
   11.55 +     \    (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))";
   11.56 +
   11.57 +(*---------------------------------------------------------------------------
   11.58 + * Ackermann.
   11.59 + *---------------------------------------------------------------------------*)
   11.60 +Rfunction"pred_nat ** pred_nat"
   11.61 +         "(Ack (0,n) =  (n + Suc 0)) & \
   11.62 +    \    (Ack (Suc m,0) = (Ack (m, Suc 0))) & \
   11.63 +    \    (Ack (Suc m, Suc n) = Ack (m, Ack (Suc m, n)))";
   11.64 +
   11.65 +(*---------------------------------------------------------------------------
   11.66 + * Almost primitive recursion. 
   11.67 + *---------------------------------------------------------------------------*)
   11.68 +function"(map2(f, [], L) = []) & \
   11.69 +    \    (map2(f, h#t, []) = []) & \
   11.70 +    \    (map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2))";
   11.71 +
   11.72 +(* Swap arguments *)
   11.73 +function"(map2(([],L), f) = []) & \
   11.74 +    \    (map2((h#t, []), f) = []) &  \
   11.75 +    \    (map2((h1#t1, h2#t2), f) = f h1 h2 # map2((t1,t2),f))";
   11.76 +
   11.77 +Rfunction
   11.78 +   "measure((length o fst o snd)::('a=>'b=>'c)*'a list*'b list => nat)"
   11.79 +    "(map2((f::'a=>'b=>'c), ([]::'a list), (L::'b list)) = [])  & \
   11.80 +\    (map2(f, h#t, []) = []) & \
   11.81 +\    (map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2))";
   11.82 +
   11.83 +(*---------------------------------------------------------------------------
   11.84 + * Relation "R" holds stepwise in a list
   11.85 + *---------------------------------------------------------------------------*)
   11.86 +function"(finiteRchain ((R::'a=>'a=>bool),  ([]::'a list)) = True) & \
   11.87 +    \    (finiteRchain (R, [x]) = True) & \
   11.88 +    \    (finiteRchain (R, x#y#rst) = (R x y & finiteRchain(R, y#rst)))";
   11.89 +
   11.90 +
   11.91 +Rfunction"measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
   11.92 +         "(finiteRchain((R::'a=>'a=>bool),  ([]::'a list)) = True) & \
   11.93 +     \    (finiteRchain(R, [x]) = True) & \
   11.94 +     \    (finiteRchain(R, x#y#rst) = (R x y & finiteRchain(R, y#rst)))";
   11.95 +
   11.96 +(*---------------------------------------------------------------------------
   11.97 + * Quicksort.
   11.98 + *---------------------------------------------------------------------------*)
   11.99 +function"(qsort(ord,  []) = []) & \
  11.100 +    \    (qsort(ord, x#rst) = \
  11.101 +    \       qsort(ord,filter(not o ord x) rst) \
  11.102 +    \       @[x]@      \
  11.103 +    \       qsort(ord,filter(ord x) rst))";
  11.104 +
  11.105 +Rfunction"measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
  11.106 +         "(qsort((ord::'a=>'a=>bool),  ([]::'a list))  = []) & \
  11.107 +     \    (qsort(ord, x#rst) = \
  11.108 +     \       qsort(ord,filter(not o ord x) rst) \
  11.109 +     \       @[x]@  \
  11.110 +     \       qsort(ord,filter(ord x) rst))";
  11.111 +
  11.112 +(*---------------------------------------------------------------------------
  11.113 + * Variant.
  11.114 + *---------------------------------------------------------------------------*)
  11.115 +function"variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)";
  11.116 +
  11.117 +Rfunction
  11.118 + "measure(%(p::nat*nat list). length(filter(%y. fst(p) <= y) (snd p)))"
  11.119 + "variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)";
  11.120 +
  11.121 +(*---------------------------------------------------------------------------
  11.122 + * Euclid's algorithm
  11.123 + *---------------------------------------------------------------------------*)
  11.124 +function"(gcd ((0::nat),(y::nat)) = y) & \
  11.125 +    \    (gcd (Suc x, 0) = Suc x) & \
  11.126 +    \    (gcd (Suc x, Suc y) =      \
  11.127 +    \        (if (y <= x) then gcd(x - y, Suc y) \
  11.128 +    \                     else gcd(Suc x, y - x)))";
  11.129 +
  11.130 +
  11.131 +(*---------------------------------------------------------------------------
  11.132 + * Wrong answer because Isabelle rewriter (going bottom-up) attempts to
  11.133 + * apply congruence rule for split to "split" but can't because split is only
  11.134 + * partly applied. It then fails, instead of just not doing the rewrite.
  11.135 + * Tobias has said he'll fix it.
  11.136 + *
  11.137 + * ... July 96 ... seems to have been fixed.
  11.138 + *---------------------------------------------------------------------------*)
  11.139 + 
  11.140 +Rfunction"measure (split (op+) ::nat*nat=>nat)"
  11.141 +         "(gcd ((0::nat),(y::nat)) = y) & \
  11.142 +        \ (gcd (Suc x, 0) = Suc x) & \
  11.143 +        \ (gcd (Suc x, Suc y) = \
  11.144 +        \     (if (y <= x) then gcd(x - y, Suc y) \
  11.145 +        \                  else gcd(Suc x, y - x)))";
  11.146 +
  11.147 +(*---------------------------------------------------------------------------
  11.148 + * A simple nested function.
  11.149 + *---------------------------------------------------------------------------*)
  11.150 +Rfunction"trancl pred_nat"
  11.151 +         "(g 0 = 0) & \
  11.152 +        \ (g(Suc x) = g(g x))";
  11.153 +
  11.154 +(*---------------------------------------------------------------------------
  11.155 + * A clever division algorithm. Primitive recursive.
  11.156 + *---------------------------------------------------------------------------*)
  11.157 +function"(Div(0,x) = (0,0)) & \
  11.158 +       \ (Div(Suc x, y) =     \
  11.159 +       \     (let (q,r) = Div(x,y) \
  11.160 +       \      in if (y <= Suc r) then (Suc q,0) else (q, Suc r)))";
  11.161 +
  11.162 +Rfunction"inv_image pred_nat (fst::nat*nat=>nat)"
  11.163 +         "(Div(0,x) = (0,0)) & \
  11.164 +        \ (Div(Suc x, y) =     \
  11.165 +        \    (let q = fst(Div(x,y)); \
  11.166 +        \         r = snd(Div(x,y))  \
  11.167 +        \     in                     \
  11.168 +        \     if (y <= Suc r) then (Suc q,0) else (q, Suc r)))";
  11.169 +
  11.170 +(*---------------------------------------------------------------------------
  11.171 + * Testing nested contexts.
  11.172 + *---------------------------------------------------------------------------*)
  11.173 +function"(f(0,x) = (0,0)) & \
  11.174 +       \ (f(Suc x, y) = \
  11.175 +       \     (let z = x \
  11.176 +       \      in        \
  11.177 +       \      if (0<y) then (0,0) else f(z,y)))";
  11.178 +
  11.179 +
  11.180 +function"(f(0,x) = (0,0)) & \
  11.181 +       \ (f(Suc x, y) =     \
  11.182 +       \      (if y = x     \
  11.183 +       \       then (if (0<y) then (0,0) else f(x,y)) \
  11.184 +       \       else (x,y)))";
  11.185 +
  11.186 +
  11.187 +(*---------------------------------------------------------------------------
  11.188 + * Naming trickery in lets.
  11.189 + *---------------------------------------------------------------------------*)
  11.190 +
  11.191 +(* No trick *)
  11.192 +function "(test(x, []) = x) & \
  11.193 +        \ (test(x,h#t) = (let y = Suc x in test(y,t)))";
  11.194 +
  11.195 +(* Trick *)
  11.196 +function"(test(x, []) = x) & \
  11.197 +       \ (test(x,h#t) =      \
  11.198 +       \     (let x = Suc x  \
  11.199 +       \      in             \
  11.200 +       \      test(x,t)))";
  11.201 +
  11.202 +(* Tricky naming, plus nested contexts *)
  11.203 +function "vary(x, L) =  \
  11.204 +        \   (if (x mem L) \
  11.205 +        \    then (let x = Suc x \
  11.206 +        \          in vary(x,L)) \
  11.207 +        \    else x)";
  11.208 +
  11.209 +
  11.210 +(*---------------------------------------------------------------------------
  11.211 + * Handling paired lets of various kinds
  11.212 + *---------------------------------------------------------------------------*)
  11.213 +function
  11.214 +    "(Fib(0) = Suc 0) &  \
  11.215 +   \ (Fib (Suc 0) = Suc 0) & \
  11.216 +   \ (Fib (Suc (Suc n)) =    \
  11.217 +   \     (let (x,y) = (Fib (Suc n), Fib n) in x+y))";
  11.218 +
  11.219 +
  11.220 +function
  11.221 +   "(qsort((ord::'a=>'a=>bool),  ([]::'a list))   = []) &  \
  11.222 +  \ (qsort(ord, x#rst) = \
  11.223 +  \     (let (L1,L2) = (filter(not o ord x) rst, \
  11.224 +  \                     filter (ord x) rst) \
  11.225 +  \      in  \
  11.226 +  \      qsort(ord,L1)@[x]@qsort(ord,L2)))";
  11.227 +
  11.228 +function"(qsort((ord::'a=>'a=>bool),  ([]::'a list))   = []) & \
  11.229 +       \ (qsort(ord, x#rst) = \
  11.230 +       \    (let (L1,L2,P) = (filter(not o ord x) rst, \
  11.231 +       \                      filter (ord x) rst, x)   \
  11.232 +       \     in \
  11.233 +       \     qsort(ord,L1)@[x]@qsort(ord,L2)))";
  11.234 +
  11.235 +function"(qsort((ord::'a=>'a=>bool),  ([]::'a list))   = []) & \
  11.236 +       \ (qsort(ord, x#rst) = \
  11.237 +       \     (let (L1,L2) = (filter(not o ord x) rst, \
  11.238 +       \                     filter (ord x) rst);     \
  11.239 +       \            (p,q) = (x,rst) \
  11.240 +       \      in \
  11.241 +       \      qsort(ord,L1)@[x]@qsort(ord,L2)))";
  11.242 +
  11.243 +
  11.244 +(*---------------------------------------------------------------------------
  11.245 + * A biggish function
  11.246 + *---------------------------------------------------------------------------*)
  11.247 +
  11.248 +function"(acc1(A,[],s,xss,zs,xs) = \
  11.249 +\              (if xs=[] then (xss, zs) \
  11.250 +\                        else acc1(A, zs,s,(xss @ [xs]),[],[]))) & \
  11.251 +\         (acc1(A,(y#ys), s, xss, zs, xs) = \
  11.252 +\              (let s' = s; \
  11.253 +\                  zs' = (if fst A s' then [] else zs@[y]); \
  11.254 +\                  xs' = (if fst A s' then xs@zs@[y] else xs) \
  11.255 +\               in  \
  11.256 +\               acc1(A, ys, s', xss, zs', xs')))";
  11.257 +
  11.258 +
  11.259 +(*---------------------------------------------------------------------------
  11.260 + * Nested, with context.
  11.261 + *---------------------------------------------------------------------------*)
  11.262 +Rfunction"pred_nat"
  11.263 +  "(k 0 = 0) & \
  11.264 +\  (k (Suc n) = (let x = k (Suc 0)  \
  11.265 +\                in if (0=Suc 0) then k (Suc(Suc 0)) else n))";
  11.266 +
  11.267 +
  11.268 +(*---------------------------------------------------------------------------
  11.269 + * A function that partitions a list into two around a predicate "P".
  11.270 + *---------------------------------------------------------------------------*)
  11.271 +val {theory,induction,rules,tcs} = 
  11.272 +  Rfunction
  11.273 +   "inv_image pred_list \
  11.274 +    \  ((fst o snd)::('a=>bool)*'a list*'a list*'a list => 'a list)"
  11.275 +
  11.276 +  "(part(P::'a=>bool, [], l1,l2) = (l1,l2)) & \
  11.277 +\  (part(P, h#rst, l1,l2) = \
  11.278 +\       (if P h then part(P,rst, h#l1,  l2) \
  11.279 +\               else part(P,rst,  l1,  h#l2)))";
  11.280 +
  11.281 +  
  11.282 +(*---------------------------------------------------------------------------
  11.283 + * Another quicksort. 
  11.284 + *---------------------------------------------------------------------------*)
  11.285 +Rfunc theory "measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
  11.286 + "(fqsort(ord,[]) = []) & \
  11.287 +\ (fqsort(ord, x#rst) = \
  11.288 + \   (let less = fst(part((%y. ord y x), rst,([],[]))); \
  11.289 +  \       more = snd(part((%y. ord y x), rst,([],[]))) \
  11.290 +   \  in \
  11.291 +    \ fqsort(ord,less)@[x]@fqsort(ord,more)))";
  11.292 +
  11.293 +Rfunc theory "measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
  11.294 + "(fqsort(ord,[]) = []) & \
  11.295 +\  (fqsort(ord, x#rst) = \
  11.296 + \   (let (less,more) = part((%y. ord y x), rst,([],[])) \
  11.297 +  \   in \
  11.298 +   \  fqsort(ord,less)@[x]@fqsort(ord,more)))";
  11.299 +
  11.300 +
  11.301 +(* Should fail on repeated variables. *)
  11.302 +function"(And(x,[]) = x) & \
  11.303 +      \  (And(y, y#t) = And(y, t))";
  11.304 +
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/TFL/test1.sml	Fri Oct 18 12:41:04 1996 +0200
    12.3 @@ -0,0 +1,83 @@
    12.4 +(*---------------------------------------------------------------------------
    12.5 + * Pattern matching extensions.
    12.6 + *---------------------------------------------------------------------------*)
    12.7 +
    12.8 +fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[])));
    12.9 +fun read thy = term_of o cread thy;
   12.10 +fun Term s = read WF1.thy s;
   12.11 +
   12.12 +fun Rfunc thy R eqs =
   12.13 +   let val {induction,rules,theory,tcs} = 
   12.14 +              timeit(fn () => Tfl.Rfunction thy (read thy R) (read thy eqs))
   12.15 +   in {induction=induction, rules=rules, theory=theory, 
   12.16 +       tcs = map (cterm_of (sign_of theory)) tcs}
   12.17 +   end;
   12.18 +
   12.19 +fun def tm = timeit (fn () => Tfl.function WF1.thy (Term tm));
   12.20 +
   12.21 +
   12.22 +
   12.23 +
   12.24 +(*---------------------------------------------------------------------------
   12.25 + * Normal patterns
   12.26 + *---------------------------------------------------------------------------*)
   12.27 +def "(f(x,y) = x+y)";
   12.28 +
   12.29 +def "(f1 0 = 1) & (f1 (Suc n) = 2)";
   12.30 +
   12.31 +(*---------------------------------------------------------------------------
   12.32 + * Omitted patterns
   12.33 + *---------------------------------------------------------------------------*)
   12.34 +def "(f2 0 = 1)";
   12.35 +
   12.36 +def "(f3 (h#t) = h)";
   12.37 +
   12.38 +def "(f4 [a,b] = a)  &  (f4 [b] = b)";
   12.39 +
   12.40 +def "(f5 (0,0) = 0)";
   12.41 +
   12.42 +def "(f6 (0,0) = 0) & (f6 (0,Suc x) = x) & (f6 (Suc x, y) = y+x)"; 
   12.43 +
   12.44 +def "(f7 (Suc 0, h#t) = 1) & (f7 (Suc(Suc n),h1#h2#t) = h1)";
   12.45 +
   12.46 +def "(f8 (Suc(Suc n),h1#h2#t) = h1)";
   12.47 +
   12.48 +
   12.49 +(*---------------------------------------------------------------------------
   12.50 + * Overlapping patterns 
   12.51 + *---------------------------------------------------------------------------*)
   12.52 +def "(f9 (h1#h2#t) = t) & (f9 x = x)";
   12.53 +
   12.54 +def "(g (x,0) = 1) & (g (0,x) = 2)"; 
   12.55 +
   12.56 +def "(g1 (0,x) = x) & (g1 (x,0) = x)"; 
   12.57 +
   12.58 +def "(g2 ([], a#b#x) = 1) & (g2 (a#b#x, y) = 2) & (g2 (z, a#y) = a)";	
   12.59 +
   12.60 +def "(g3 (x,y,0) = 1) & (g3 (x,0,y) = 2) & (g3 (0,x,y) = x)";
   12.61 +
   12.62 +def "(g4 (0,y,z) = 1) & (g4 (x,0,z) = 2) & (g4 (x,y,0) = x)";
   12.63 +
   12.64 +def "(g5(0,x,y,z) = 1) & (g5(w,0,y,z) = 2) & (g5(w,x,0,z) = z) & \
   12.65 +  \  (g5(w,x,y,0) = y)";
   12.66 +
   12.67 +def "(g6 (0,w,x,y,z) = 1) & (g6 (v,0,x,y,z) = 2) & (g6 (v,w,0,y,z) = z) & \
   12.68 +  \  (g6 (v,w,x,0,z) = z) & (g6 (v,w,x,y,0) = 0)";
   12.69 +
   12.70 +def "(g7 [x, 0] = x) & (g7 [Suc v] = 1) & (g7 z = 2)";
   12.71 +
   12.72 +def "(g8 (h1#h2#h3#h4#h5#h6) = [h1,h2,h3,h4,h5]# g8 h6) & (g8 x = [x])";
   12.73 +
   12.74 +(* Normal *)
   12.75 +def "(g9 (Suc(Suc x)) = 1) & (g9 (Suc x) = 2) & (g9 0 = 0)";
   12.76 +
   12.77 +(*---------------------------------------------------------------------------
   12.78 + * Inaccessible patterns
   12.79 + *---------------------------------------------------------------------------*)
   12.80 +def "(h x = 1) & (h x = 2)";
   12.81 +
   12.82 +def "(h1 (x,0) = 1) & (h1 (x,Suc y) = 2) & \
   12.83 +  \  (h1 (x,y) = x) & (h1 (x,y) = y)";
   12.84 +
   12.85 +def "(h2 (x,0) = 1) & (h2 (0,x) = 2) & \
   12.86 +  \  (h2 (0,0) = 0) & (h2 (x,y) = x)"; 
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/TFL/tfl.sig	Fri Oct 18 12:41:04 1996 +0200
    13.3 @@ -0,0 +1,65 @@
    13.4 +signature TFL_sig =
    13.5 +sig
    13.6 +   structure Rules: Rules_sig
    13.7 +   structure Thms : Thms_sig
    13.8 +   structure Thry : Thry_sig
    13.9 +   structure USyntax : USyntax_sig
   13.10 +
   13.11 +   type Preterm
   13.12 +   type Term
   13.13 +   type Thm
   13.14 +   type Thry
   13.15 +   type Tactic
   13.16 +   
   13.17 +   datatype pattern = GIVEN of Preterm * int
   13.18 +                    | OMITTED of Preterm * int
   13.19 +
   13.20 +   val mk_functional : Thry -> Preterm
   13.21 +                       -> {functional:Preterm,
   13.22 +                           pats: pattern list}
   13.23 +
   13.24 +   val prim_wfrec_definition : Thry 
   13.25 +                                -> {R:Preterm, functional:Preterm}
   13.26 +                                -> {def:Thm, corollary:Thm, theory:Thry}
   13.27 +
   13.28 +   val wfrec_eqns : Thry -> Preterm
   13.29 +                     -> {WFR : Preterm, 
   13.30 +                         proto_def : Preterm,
   13.31 +                         extracta :(Thm * Preterm list) list,
   13.32 +                         pats  : pattern list}
   13.33 +
   13.34 +
   13.35 +   val gen_wfrec_definition : Thry 
   13.36 +                               -> {R:Preterm, eqs:Preterm}
   13.37 +                               -> {theory:Thry,
   13.38 +                                   rules :Thm, 
   13.39 +                                     TCs : Preterm list list,
   13.40 +                           full_pats_TCs :(Preterm * Preterm list) list, 
   13.41 +                                   patterns : pattern list}
   13.42 +
   13.43 +   val lazyR_def : Thry
   13.44 +                   -> Preterm
   13.45 +                   -> {theory:Thry,
   13.46 +                       rules :Thm,
   13.47 +                           R :Preterm,
   13.48 +                       full_pats_TCs :(Preterm * Preterm list) list, 
   13.49 +                       patterns: pattern list}
   13.50 +
   13.51 +   val mk_induction : Thry 
   13.52 +                       -> Preterm -> Preterm 
   13.53 +                         -> (Preterm * Preterm list) list
   13.54 +                           -> Thm
   13.55 +
   13.56 +   val postprocess: {WFtac:Tactic, terminator:Tactic, simplifier:Term -> Thm}
   13.57 +                     -> Thry 
   13.58 +                      -> {rules:Thm, induction:Thm, TCs:Preterm list list}
   13.59 +                       -> {rules:Thm, induction:Thm, nested_tcs:Thm list}
   13.60 +
   13.61 +   val termination_goals : Thm -> Preterm list
   13.62 +
   13.63 +   structure Context
   13.64 +     : sig
   13.65 +         val read : unit -> Thm list
   13.66 +         val write : Thm list -> unit
   13.67 +       end
   13.68 +end;
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/TFL/tfl.sml	Fri Oct 18 12:41:04 1996 +0200
    14.3 @@ -0,0 +1,922 @@
    14.4 +functor TFL(structure Rules : Rules_sig
    14.5 +            structure Thry  : Thry_sig
    14.6 +            structure Thms  : Thms_sig
    14.7 +            sharing type Rules.binding = Thry.binding = 
    14.8 +                         Thry.USyntax.binding = Mask.binding
    14.9 +            sharing type Rules.Type = Thry.Type = Thry.USyntax.Type
   14.10 +            sharing type Rules.Preterm = Thry.Preterm = Thry.USyntax.Preterm
   14.11 +            sharing type Rules.Term = Thry.Term = Thry.USyntax.Term
   14.12 +            sharing type Thms.Thm = Rules.Thm = Thry.Thm) : TFL_sig  =
   14.13 +struct
   14.14 +
   14.15 +(* Declarations *)
   14.16 +structure Thms = Thms;
   14.17 +structure Rules = Rules;
   14.18 +structure Thry = Thry;
   14.19 +structure USyntax = Thry.USyntax;
   14.20 +
   14.21 +type Preterm = Thry.USyntax.Preterm;
   14.22 +type Term = Thry.USyntax.Term;
   14.23 +type Thm = Thms.Thm;
   14.24 +type Thry = Thry.Thry;
   14.25 +type Tactic = Rules.Tactic;
   14.26 +   
   14.27 +
   14.28 +(* Abbreviations *)
   14.29 +structure R = Rules;
   14.30 +structure S = USyntax;
   14.31 +structure U = S.Utils;
   14.32 +
   14.33 +(* Declares 'a binding datatype *)
   14.34 +open Mask;
   14.35 +
   14.36 +nonfix mem --> |-> ##;
   14.37 +val --> = S.-->;
   14.38 +val ##    = U.##;
   14.39 +
   14.40 +infixr 3 -->;
   14.41 +infixr 7 |->;
   14.42 +infix  4 ##; 
   14.43 +
   14.44 +val concl = #2 o R.dest_thm;
   14.45 +val hyp = #1 o R.dest_thm;
   14.46 +
   14.47 +val list_mk_type = U.end_itlist (U.curry(op -->));
   14.48 +
   14.49 +fun flatten [] = []
   14.50 +  | flatten (h::t) = h@flatten t;
   14.51 +
   14.52 +
   14.53 +fun gtake f =
   14.54 +  let fun grab(0,rst) = ([],rst)
   14.55 +        | grab(n, x::rst) = 
   14.56 +             let val (taken,left) = grab(n-1,rst)
   14.57 +             in (f x::taken, left) end
   14.58 +  in grab
   14.59 +  end;
   14.60 +
   14.61 +fun enumerate L = 
   14.62 + rev(#1(U.rev_itlist (fn x => fn (alist,i) => ((x,i)::alist, i+1)) L ([],0)));
   14.63 +
   14.64 +fun stringize [] = ""
   14.65 +  | stringize [i] = U.int_to_string i
   14.66 +  | stringize (h::t) = (U.int_to_string h^", "^stringize t);
   14.67 +
   14.68 +
   14.69 +fun TFL_ERR{func,mesg} = U.ERR{module = "Tfl", func = func, mesg = mesg};
   14.70 +
   14.71 +
   14.72 +(*---------------------------------------------------------------------------
   14.73 + * The next function is common to pattern-match translation and 
   14.74 + * proof of completeness of cases for the induction theorem.
   14.75 + *
   14.76 + * "gvvariant" make variables that are guaranteed not to be in vlist and
   14.77 + * furthermore, are guaranteed not to be equal to each other. The names of
   14.78 + * the variables will start with "v" and end in a number.
   14.79 + *---------------------------------------------------------------------------*)
   14.80 +local val counter = ref 0
   14.81 +in
   14.82 +fun gvvariant vlist =
   14.83 +  let val slist = ref (map (#Name o S.dest_var) vlist)
   14.84 +      val mem = U.mem (U.curry (op=))
   14.85 +      val _ = counter := 0
   14.86 +      fun pass str = 
   14.87 +         if (mem str (!slist)) 
   14.88 +         then ( counter := !counter + 1;
   14.89 +                pass (U.concat"v" (U.int_to_string(!counter))))
   14.90 +         else (slist := str :: !slist; str)
   14.91 +  in 
   14.92 +  fn ty => S.mk_var{Name=pass "v",  Ty=ty}
   14.93 +  end
   14.94 +end;
   14.95 +
   14.96 +
   14.97 +(*---------------------------------------------------------------------------
   14.98 + * Used in induction theorem production. This is the simple case of
   14.99 + * partitioning up pattern rows by the leading constructor.
  14.100 + *---------------------------------------------------------------------------*)
  14.101 +fun ipartition gv (constructors,rows) =
  14.102 +  let fun pfail s = raise TFL_ERR{func = "partition.part", mesg = s}
  14.103 +      fun part {constrs = [],   rows = [],   A} = rev A
  14.104 +        | part {constrs = [],   rows = _::_, A} = pfail"extra cases in defn"
  14.105 +        | part {constrs = _::_, rows = [],   A} = pfail"cases missing in defn"
  14.106 +        | part {constrs = c::crst, rows,     A} =
  14.107 +          let val {Name,Ty} = S.dest_const c
  14.108 +              val (L,_) = S.strip_type Ty
  14.109 +              val (in_group, not_in_group) =
  14.110 +               U.itlist (fn (row as (p::rst, rhs)) =>
  14.111 +                         fn (in_group,not_in_group) =>
  14.112 +                  let val (pc,args) = S.strip_comb p
  14.113 +                  in if (#Name(S.dest_const pc) = Name)
  14.114 +                     then ((args@rst, rhs)::in_group, not_in_group)
  14.115 +                     else (in_group, row::not_in_group)
  14.116 +                  end)      rows ([],[])
  14.117 +              val col_types = U.take S.type_of (length L, #1(hd in_group))
  14.118 +          in 
  14.119 +          part{constrs = crst, rows = not_in_group, 
  14.120 +               A = {constructor = c, 
  14.121 +                    new_formals = map gv col_types,
  14.122 +                    group = in_group}::A}
  14.123 +          end
  14.124 +  in part{constrs = constructors, rows = rows, A = []}
  14.125 +  end;
  14.126 +
  14.127 +
  14.128 +
  14.129 +(*---------------------------------------------------------------------------
  14.130 + * This datatype carries some information about the origin of a
  14.131 + * clause in a function definition.
  14.132 + *---------------------------------------------------------------------------*)
  14.133 +datatype pattern = GIVEN   of S.Preterm * int
  14.134 +                 | OMITTED of S.Preterm * int
  14.135 +
  14.136 +fun psubst theta (GIVEN (tm,i)) = GIVEN(S.subst theta tm, i)
  14.137 +  | psubst theta (OMITTED (tm,i)) = OMITTED(S.subst theta tm, i);
  14.138 +
  14.139 +fun dest_pattern (GIVEN (tm,i)) = ((GIVEN,i),tm)
  14.140 +  | dest_pattern (OMITTED (tm,i)) = ((OMITTED,i),tm);
  14.141 +
  14.142 +val pat_of = #2 o dest_pattern;
  14.143 +val row_of_pat = #2 o #1 o dest_pattern;
  14.144 +
  14.145 +(*---------------------------------------------------------------------------
  14.146 + * Produce an instance of a constructor, plus genvars for its arguments.
  14.147 + *---------------------------------------------------------------------------*)
  14.148 +fun fresh_constr ty_match colty gv c =
  14.149 +  let val {Ty,...} = S.dest_const c
  14.150 +      val (L,ty) = S.strip_type Ty
  14.151 +      val ty_theta = ty_match ty colty
  14.152 +      val c' = S.inst ty_theta c
  14.153 +      val gvars = map (S.inst ty_theta o gv) L
  14.154 +  in (c', gvars)
  14.155 +  end;
  14.156 +
  14.157 +
  14.158 +(*---------------------------------------------------------------------------
  14.159 + * Goes through a list of rows and picks out the ones beginning with a
  14.160 + * pattern with constructor = Name.
  14.161 + *---------------------------------------------------------------------------*)
  14.162 +fun mk_group Name rows =
  14.163 +  U.itlist (fn (row as ((prefix, p::rst), rhs)) =>
  14.164 +            fn (in_group,not_in_group) =>
  14.165 +               let val (pc,args) = S.strip_comb p
  14.166 +               in if ((#Name(S.dest_const pc) = Name) handle _ => false)
  14.167 +                  then (((prefix,args@rst), rhs)::in_group, not_in_group)
  14.168 +                  else (in_group, row::not_in_group) end)
  14.169 +      rows ([],[]);
  14.170 +
  14.171 +(*---------------------------------------------------------------------------
  14.172 + * Partition the rows. Not efficient: we should use hashing.
  14.173 + *---------------------------------------------------------------------------*)
  14.174 +fun partition _ _ (_,_,_,[]) = raise TFL_ERR{func="partition", mesg="no rows"}
  14.175 +  | partition gv ty_match
  14.176 +              (constructors, colty, res_ty, rows as (((prefix,_),_)::_)) =
  14.177 +let val fresh = fresh_constr ty_match colty gv
  14.178 +     fun part {constrs = [],      rows, A} = rev A
  14.179 +       | part {constrs = c::crst, rows, A} =
  14.180 +         let val (c',gvars) = fresh c
  14.181 +             val {Name,Ty} = S.dest_const c'
  14.182 +             val (in_group, not_in_group) = mk_group Name rows
  14.183 +             val in_group' =
  14.184 +                 if (null in_group)  (* Constructor not given *)
  14.185 +                 then [((prefix, #2(fresh c)), OMITTED (S.ARB res_ty, ~1))]
  14.186 +                 else in_group
  14.187 +         in 
  14.188 +         part{constrs = crst, 
  14.189 +              rows = not_in_group, 
  14.190 +              A = {constructor = c', 
  14.191 +                   new_formals = gvars,
  14.192 +                   group = in_group'}::A}
  14.193 +         end
  14.194 +in part{constrs=constructors, rows=rows, A=[]}
  14.195 +end;
  14.196 +
  14.197 +(*---------------------------------------------------------------------------
  14.198 + * Misc. routines used in mk_case
  14.199 + *---------------------------------------------------------------------------*)
  14.200 +
  14.201 +fun mk_pat c =
  14.202 +  let val L = length(#1(S.strip_type(S.type_of c)))
  14.203 +      fun build (prefix,tag,plist) =
  14.204 +          let val (args,plist') = gtake U.I (L, plist)
  14.205 +           in (prefix,tag,S.list_mk_comb(c,args)::plist') end
  14.206 +  in map build 
  14.207 +  end;
  14.208 +
  14.209 +fun v_to_prefix (prefix, v::pats) = (v::prefix,pats)
  14.210 +  | v_to_prefix _ = raise TFL_ERR{func="mk_case", mesg="v_to_prefix"};
  14.211 +
  14.212 +fun v_to_pats (v::prefix,tag, pats) = (prefix, tag, v::pats)
  14.213 +  | v_to_pats _ = raise TFL_ERR{func="mk_case", mesg="v_to_pats"};
  14.214 + 
  14.215 +
  14.216 +(*----------------------------------------------------------------------------
  14.217 + * Translation of pattern terms into nested case expressions.
  14.218 + *
  14.219 + * This performs the translation and also builds the full set of patterns. 
  14.220 + * Thus it supports the construction of induction theorems even when an 
  14.221 + * incomplete set of patterns is given.
  14.222 + *---------------------------------------------------------------------------*)
  14.223 +
  14.224 +fun mk_case ty_info ty_match FV range_ty =
  14.225 + let 
  14.226 + fun mk_case_fail s = raise TFL_ERR{func = "mk_case", mesg = s}
  14.227 + val fresh_var = gvvariant FV 
  14.228 + val divide = partition fresh_var ty_match
  14.229 + fun expand constructors ty ((_,[]), _) = mk_case_fail"expand_var_row"
  14.230 +   | expand constructors ty (row as ((prefix, p::rst), rhs)) = 
  14.231 +       if (S.is_var p) 
  14.232 +       then let val fresh = fresh_constr ty_match ty fresh_var
  14.233 +                fun expnd (c,gvs) = 
  14.234 +                  let val capp = S.list_mk_comb(c,gvs)
  14.235 +                  in ((prefix, capp::rst), psubst[p |-> capp] rhs)
  14.236 +                  end
  14.237 +            in map expnd (map fresh constructors)  end
  14.238 +       else [row]
  14.239 + fun mk{rows=[],...} = mk_case_fail"no rows"
  14.240 +   | mk{path=[], rows = ((prefix, []), rhs)::_} =  (* Done *)
  14.241 +        let val (tag,tm) = dest_pattern rhs
  14.242 +        in ([(prefix,tag,[])], tm)
  14.243 +        end
  14.244 +   | mk{path=[], rows = _::_} = mk_case_fail"blunder"
  14.245 +   | mk{path as u::rstp, rows as ((prefix, []), rhs)::rst} = 
  14.246 +        mk{path = path, 
  14.247 +           rows = ((prefix, [fresh_var(S.type_of u)]), rhs)::rst}
  14.248 +   | mk{path = u::rstp, rows as ((_, p::_), _)::_} =
  14.249 +     let val (pat_rectangle,rights) = U.unzip rows
  14.250 +         val col0 = map(hd o #2) pat_rectangle
  14.251 +     in 
  14.252 +     if (U.all S.is_var col0) 
  14.253 +     then let val rights' = map(fn(v,e) => psubst[v|->u] e) (U.zip col0 rights)
  14.254 +              val pat_rectangle' = map v_to_prefix pat_rectangle
  14.255 +              val (pref_patl,tm) = mk{path = rstp,
  14.256 +                                      rows = U.zip pat_rectangle' rights'}
  14.257 +          in (map v_to_pats pref_patl, tm)
  14.258 +          end
  14.259 +     else
  14.260 +     let val pty = S.type_of p
  14.261 +         val ty_name = (#Tyop o S.dest_type) pty
  14.262 +     in
  14.263 +     case (ty_info ty_name)
  14.264 +     of U.NONE => mk_case_fail("Not a known datatype: "^ty_name)
  14.265 +      | U.SOME{case_const,constructors} =>
  14.266 +        let val case_const_name = #Name(S.dest_const case_const)
  14.267 +            val nrows = flatten (map (expand constructors pty) rows)
  14.268 +            val subproblems = divide(constructors, pty, range_ty, nrows)
  14.269 +            val groups      = map #group subproblems
  14.270 +            and new_formals = map #new_formals subproblems
  14.271 +            and constructors' = map #constructor subproblems
  14.272 +            val news = map (fn (nf,rows) => {path = nf@rstp, rows=rows})
  14.273 +                           (U.zip new_formals groups)
  14.274 +            val rec_calls = map mk news
  14.275 +            val (pat_rect,dtrees) = U.unzip rec_calls
  14.276 +            val case_functions = map S.list_mk_abs(U.zip new_formals dtrees)
  14.277 +            val types = map S.type_of (case_functions@[u]) @ [range_ty]
  14.278 +            val case_const' = S.mk_const{Name = case_const_name,
  14.279 +                                         Ty   = list_mk_type types}
  14.280 +            val tree = S.list_mk_comb(case_const', case_functions@[u])
  14.281 +            val pat_rect1 = flatten(U.map2 mk_pat constructors' pat_rect)
  14.282 +        in (pat_rect1,tree)
  14.283 +        end 
  14.284 +     end end
  14.285 + in mk
  14.286 + end;
  14.287 +
  14.288 +
  14.289 +(* Repeated variable occurrences in a pattern are not allowed. *)
  14.290 +fun FV_multiset tm = 
  14.291 +   case (S.dest_term tm)
  14.292 +     of S.VAR v => [S.mk_var v]
  14.293 +      | S.CONST _ => []
  14.294 +      | S.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand
  14.295 +      | S.LAMB _ => raise TFL_ERR{func = "FV_multiset", mesg = "lambda"};
  14.296 +
  14.297 +fun no_repeat_vars thy pat =
  14.298 + let fun check [] = true
  14.299 +       | check (v::rst) =
  14.300 +         if (U.mem S.aconv v rst) 
  14.301 +         then raise TFL_ERR{func = "no_repeat_vars",
  14.302 +             mesg = U.concat(U.quote(#Name(S.dest_var v)))
  14.303 +                     (U.concat" occurs repeatedly in the pattern "
  14.304 +                         (U.quote(S.Term_to_string (Thry.typecheck thy pat))))}
  14.305 +         else check rst
  14.306 + in check (FV_multiset pat)
  14.307 + end;
  14.308 +
  14.309 +local fun paired1{lhs,rhs} = (lhs,rhs) 
  14.310 +      and paired2{Rator,Rand} = (Rator,Rand)
  14.311 +      fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s}
  14.312 +in
  14.313 +fun mk_functional thy eqs =
  14.314 + let val clauses = S.strip_conj eqs
  14.315 +     val (L,R) = U.unzip (map (paired1 o S.dest_eq o U.snd o S.strip_forall)
  14.316 +                              clauses)
  14.317 +     val (funcs,pats) = U.unzip(map (paired2 o S.dest_comb) L)
  14.318 +     val [f] = U.mk_set (S.aconv) funcs 
  14.319 +               handle _ => mk_functional_err "function name not unique"
  14.320 +     val _ = map (no_repeat_vars thy) pats
  14.321 +     val rows = U.zip (map (fn x => ([],[x])) pats) (map GIVEN (enumerate R))
  14.322 +     val fvs = S.free_varsl R
  14.323 +     val a = S.variant fvs (S.mk_var{Name="a", Ty = S.type_of(hd pats)})
  14.324 +     val FV = a::fvs
  14.325 +     val ty_info = Thry.match_info thy
  14.326 +     val ty_match = Thry.match_type thy
  14.327 +     val range_ty = S.type_of (hd R)
  14.328 +     val (patts, case_tm) = mk_case ty_info ty_match FV range_ty 
  14.329 +                                    {path=[a], rows=rows}
  14.330 +     val patts1 = map (fn (_,(tag,i),[pat]) => tag (pat,i)) patts handle _ 
  14.331 +                  => mk_functional_err "error in pattern-match translation"
  14.332 +     val patts2 = U.sort(fn p1=>fn p2=> row_of_pat p1 < row_of_pat p2) patts1
  14.333 +     val finals = map row_of_pat patts2
  14.334 +     val originals = map (row_of_pat o #2) rows
  14.335 +     fun int_eq i1 (i2:int) =  (i1=i2)
  14.336 +     val _ = case (U.set_diff int_eq originals finals)
  14.337 +             of [] => ()
  14.338 +          | L => mk_functional_err("The following rows (counting from zero)\
  14.339 +                                   \ are inaccessible: "^stringize L)
  14.340 + in {functional = S.list_mk_abs ([f,a], case_tm),
  14.341 +     pats = patts2}
  14.342 +end end;
  14.343 +
  14.344 +
  14.345 +(*----------------------------------------------------------------------------
  14.346 + *
  14.347 + *                    PRINCIPLES OF DEFINITION
  14.348 + *
  14.349 + *---------------------------------------------------------------------------*)
  14.350 +
  14.351 +
  14.352 +(*----------------------------------------------------------------------------
  14.353 + * This basic principle of definition takes a functional M and a relation R
  14.354 + * and specializes the following theorem
  14.355 + *
  14.356 + *    |- !M R f. (f = WFREC R M) ==> WF R ==> !x. f x = M (f%R,x) x
  14.357 + *
  14.358 + * to them (getting "th1", say). Then we make the definition "f = WFREC R M" 
  14.359 + * and instantiate "th1" to the constant "f" (getting th2). Then we use the
  14.360 + * definition to delete the first antecedent to th2. Hence the result in
  14.361 + * the "corollary" field is 
  14.362 + *
  14.363 + *    |-  WF R ==> !x. f x = M (f%R,x) x
  14.364 + *
  14.365 + *---------------------------------------------------------------------------*)
  14.366 +
  14.367 +fun prim_wfrec_definition thy {R, functional} =
  14.368 + let val tych = Thry.typecheck thy
  14.369 +     val {Bvar,...} = S.dest_abs functional
  14.370 +     val {Name,...} = S.dest_var Bvar  (* Intended name of definition *)
  14.371 +     val cor1 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
  14.372 +     val cor2 = R.ISPEC (tych R) cor1
  14.373 +     val f_eq_WFREC_R_M = (#ant o S.dest_imp o #Body 
  14.374 +                           o S.dest_forall o concl) cor2
  14.375 +     val {lhs,rhs} = S.dest_eq f_eq_WFREC_R_M
  14.376 +     val {Ty, ...} = S.dest_var lhs
  14.377 +     val def_term = S.mk_eq{lhs = S.mk_var{Name=Name,Ty=Ty}, rhs=rhs}
  14.378 +     val (def_thm,thy1) = Thry.make_definition thy 
  14.379 +                                  (U.concat Name "_def") def_term
  14.380 +     val (_,[f,_]) = (S.strip_comb o concl) def_thm
  14.381 +     val cor3 = R.ISPEC (Thry.typecheck thy1 f) cor2
  14.382 + in 
  14.383 + {theory = thy1, def=def_thm, corollary=R.MP cor3 def_thm}
  14.384 + end;
  14.385 +
  14.386 +
  14.387 +(*---------------------------------------------------------------------------
  14.388 + * This structure keeps track of congruence rules that aren't derived
  14.389 + * from a datatype definition.
  14.390 + *---------------------------------------------------------------------------*)
  14.391 +structure Context =
  14.392 +struct
  14.393 +  val non_datatype_context = ref []:Rules.Thm list ref
  14.394 +  fun read() = !non_datatype_context
  14.395 +  fun write L = (non_datatype_context := L)
  14.396 +end;
  14.397 +
  14.398 +fun extraction_thms thy = 
  14.399 + let val {case_rewrites,case_congs} = Thry.extract_info thy
  14.400 + in (case_rewrites, case_congs@Context.read())
  14.401 + end;
  14.402 +
  14.403 +
  14.404 +(*---------------------------------------------------------------------------
  14.405 + * Pair patterns with termination conditions. The full list of patterns for
  14.406 + * a definition is merged with the TCs arising from the user-given clauses.
  14.407 + * There can be fewer clauses than the full list, if the user omitted some 
  14.408 + * cases. This routine is used to prepare input for mk_induction.
  14.409 + *---------------------------------------------------------------------------*)
  14.410 +fun merge full_pats TCs =
  14.411 +let fun insert (p,TCs) =
  14.412 +      let fun insrt ((x as (h,[]))::rst) = 
  14.413 +                 if (S.aconv p h) then (p,TCs)::rst else x::insrt rst
  14.414 +            | insrt (x::rst) = x::insrt rst
  14.415 +            | insrt[] = raise TFL_ERR{func="merge.insert",mesg="pat not found"}
  14.416 +      in insrt end
  14.417 +    fun pass ([],ptcl_final) = ptcl_final
  14.418 +      | pass (ptcs::tcl, ptcl) = pass(tcl, insert ptcs ptcl)
  14.419 +in 
  14.420 +  pass (TCs, map (fn p => (p,[])) full_pats)
  14.421 +end;
  14.422 +
  14.423 +fun not_omitted (GIVEN(tm,_)) = tm
  14.424 +  | not_omitted (OMITTED _) = raise TFL_ERR{func="not_omitted",mesg=""}
  14.425 +val givens = U.mapfilter not_omitted;
  14.426 +
  14.427 +
  14.428 +(*--------------------------------------------------------------------------
  14.429 + * This is a wrapper for "prim_wfrec_definition": it builds a functional,
  14.430 + * calls "prim_wfrec_definition", then specializes the result. This gives a
  14.431 + * list of rewrite rules where the right hand sides are quite ugly, so we 
  14.432 + * simplify to get rid of the case statements. In essence, this function
  14.433 + * performs pre- and post-processing for patterns. As well, after
  14.434 + * simplification, termination conditions are extracted.
  14.435 + *-------------------------------------------------------------------------*)
  14.436 +
  14.437 +fun gen_wfrec_definition thy {R, eqs} =
  14.438 + let val {functional,pats}  = mk_functional thy eqs
  14.439 +     val given_pats = givens pats
  14.440 +     val {def,corollary,theory} = prim_wfrec_definition thy
  14.441 +                                        {R=R, functional=functional}
  14.442 +     val tych = Thry.typecheck theory 
  14.443 +     val {lhs=f,...} = S.dest_eq(concl def)
  14.444 +     val WFR = #ant(S.dest_imp(concl corollary))
  14.445 +     val corollary' = R.UNDISCH corollary  (* put WF R on assums *)
  14.446 +     val corollaries = map (U.C R.SPEC corollary' o tych) given_pats
  14.447 +     val (case_rewrites,context_congs) = extraction_thms thy
  14.448 +     val corollaries' = map(R.simplify case_rewrites) corollaries
  14.449 +     fun xtract th = R.CONTEXT_REWRITE_RULE(f,R)
  14.450 +                         {thms = [(R.ISPECL o map tych)[f,R] Thms.CUT_LEMMA],
  14.451 +                         congs = context_congs,
  14.452 +                            th = th}
  14.453 +     val (rules, TCs) = U.unzip (map xtract corollaries')
  14.454 +     val rules0 = map (R.simplify [Thms.CUT_DEF]) rules
  14.455 +     val mk_cond_rule = R.FILTER_DISCH_ALL(not o S.aconv WFR)
  14.456 +     val rules1 = R.LIST_CONJ(map mk_cond_rule rules0)
  14.457 + in
  14.458 + {theory = theory,   (* holds def, if it's needed *)
  14.459 +  rules = rules1,
  14.460 +  full_pats_TCs = merge (map pat_of pats) (U.zip given_pats TCs), 
  14.461 +  TCs = TCs, 
  14.462 +  patterns = pats}
  14.463 + end;
  14.464 +
  14.465 +
  14.466 +(*---------------------------------------------------------------------------
  14.467 + * Perform the extraction without making the definition. Definition and
  14.468 + * extraction commute for the non-nested case. For hol90 users, this 
  14.469 + * function can be invoked without being in draft mode.
  14.470 + *---------------------------------------------------------------------------*)
  14.471 +fun wfrec_eqns thy eqns =
  14.472 + let val {functional,pats} = mk_functional thy eqns
  14.473 +     val given_pats = givens pats
  14.474 +     val {Bvar = f, Body} = S.dest_abs functional
  14.475 +     val {Bvar = x, ...} = S.dest_abs Body
  14.476 +     val {Name,Ty = fty} = S.dest_var f
  14.477 +     val {Tyop="fun", Args = [f_dty, f_rty]} = S.dest_type fty
  14.478 +     val (case_rewrites,context_congs) = extraction_thms thy
  14.479 +     val tych = Thry.typecheck thy
  14.480 +     val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
  14.481 +     val R = S.variant(S.free_vars eqns) 
  14.482 +                      (#Bvar(S.dest_forall(concl WFREC_THM0)))
  14.483 +     val WFREC_THM = R.ISPECL [tych R, tych f] WFREC_THM0
  14.484 +     val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
  14.485 +     val R1 = S.rand WFR
  14.486 +     val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
  14.487 +     val corollaries = map (U.C R.SPEC corollary' o tych) given_pats
  14.488 +     val corollaries' = map (R.simplify case_rewrites) corollaries
  14.489 +     fun extract th = R.CONTEXT_REWRITE_RULE(f,R1)
  14.490 +                        {thms = [(R.ISPECL o map tych)[f,R1] Thms.CUT_LEMMA], 
  14.491 +                        congs = context_congs,
  14.492 +                          th  = th}
  14.493 + in {proto_def=proto_def, 
  14.494 +     WFR=WFR, 
  14.495 +     pats=pats,
  14.496 +     extracta = map extract corollaries'}
  14.497 + end;
  14.498 +
  14.499 +
  14.500 +(*---------------------------------------------------------------------------
  14.501 + * Define the constant after extracting the termination conditions. The 
  14.502 + * wellfounded relation used in the definition is computed by using the
  14.503 + * choice operator on the extracted conditions (plus the condition that
  14.504 + * such a relation must be wellfounded).
  14.505 + *---------------------------------------------------------------------------*)
  14.506 +fun lazyR_def thy eqns =
  14.507 + let val {proto_def,WFR,pats,extracta} = wfrec_eqns thy eqns
  14.508 +     val R1 = S.rand WFR
  14.509 +     val f = S.lhs proto_def
  14.510 +     val {Name,...} = S.dest_var f
  14.511 +     val (extractants,TCl) = U.unzip extracta
  14.512 +     val TCs = U.Union S.aconv TCl
  14.513 +     val full_rqt = WFR::TCs
  14.514 +     val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
  14.515 +     val R'abs = S.rand R'
  14.516 +     val (def,theory) = Thry.make_definition thy (U.concat Name "_def") 
  14.517 +                                                 (S.subst[R1 |-> R'] proto_def)
  14.518 +     val fconst = #lhs(S.dest_eq(concl def)) 
  14.519 +     val tych = Thry.typecheck theory
  14.520 +     val baz = R.DISCH (tych proto_def)
  14.521 +                 (U.itlist (R.DISCH o tych) full_rqt (R.LIST_CONJ extractants))
  14.522 +     val def' = R.MP (R.SPEC (tych fconst) 
  14.523 +                             (R.SPEC (tych R') (R.GENL[tych R1, tych f] baz)))
  14.524 +                     def
  14.525 +     val body_th = R.LIST_CONJ (map (R.ASSUME o tych) full_rqt)
  14.526 +     val bar = R.MP (R.BETA_RULE(R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX))
  14.527 +                     body_th
  14.528 + in {theory = theory, R=R1,
  14.529 +     rules = U.rev_itlist (U.C R.MP) (R.CONJUNCTS bar) def',
  14.530 +     full_pats_TCs = merge (map pat_of pats) (U.zip (givens pats) TCl),
  14.531 +     patterns = pats}
  14.532 + end;
  14.533 +
  14.534 +
  14.535 +
  14.536 +(*----------------------------------------------------------------------------
  14.537 + *
  14.538 + *                           INDUCTION THEOREM
  14.539 + *
  14.540 + *---------------------------------------------------------------------------*)
  14.541 +
  14.542 +
  14.543 +(*------------------------  Miscellaneous function  --------------------------
  14.544 + *
  14.545 + *           [x_1,...,x_n]     ?v_1...v_n. M[v_1,...,v_n]
  14.546 + *     -----------------------------------------------------------
  14.547 + *     ( M[x_1,...,x_n], [(x_i,?v_1...v_n. M[v_1,...,v_n]),
  14.548 + *                        ... 
  14.549 + *                        (x_j,?v_n. M[x_1,...,x_(n-1),v_n])] )
  14.550 + *
  14.551 + * This function is totally ad hoc. Used in the production of the induction 
  14.552 + * theorem. The nchotomy theorem can have clauses that look like
  14.553 + *
  14.554 + *     ?v1..vn. z = C vn..v1
  14.555 + *
  14.556 + * in which the order of quantification is not the order of occurrence of the
  14.557 + * quantified variables as arguments to C. Since we have no control over this
  14.558 + * aspect of the nchotomy theorem, we make the correspondence explicit by
  14.559 + * pairing the incoming new variable with the term it gets beta-reduced into.
  14.560 + *---------------------------------------------------------------------------*)
  14.561 +
  14.562 +fun alpha_ex_unroll xlist tm =
  14.563 +  let val (qvars,body) = S.strip_exists tm
  14.564 +      val vlist = #2(S.strip_comb (S.rhs body))
  14.565 +      val plist = U.zip vlist xlist
  14.566 +      val args = map (U.C (U.assoc1 (U.uncurry S.aconv)) plist) qvars
  14.567 +      val args' = map (fn U.SOME(_,v) => v 
  14.568 +                        | U.NONE => raise TFL_ERR{func = "alpha_ex_unroll",
  14.569 +                                       mesg = "no correspondence"}) args
  14.570 +      fun build ex [] = []
  14.571 +        | build ex (v::rst) =
  14.572 +           let val ex1 = S.beta_conv(S.mk_comb{Rator=S.rand ex, Rand=v})
  14.573 +           in ex1::build ex1 rst
  14.574 +           end
  14.575 +     val (nex::exl) = rev (tm::build tm args')
  14.576 +  in 
  14.577 +  (nex, U.zip args' (rev exl))
  14.578 +  end;
  14.579 +
  14.580 +
  14.581 +
  14.582 +(*----------------------------------------------------------------------------
  14.583 + *
  14.584 + *             PROVING COMPLETENESS OF PATTERNS
  14.585 + *
  14.586 + *---------------------------------------------------------------------------*)
  14.587 +
  14.588 +fun mk_case ty_info FV thy =
  14.589 + let 
  14.590 + val divide = ipartition (gvvariant FV)
  14.591 + val tych = Thry.typecheck thy
  14.592 + fun tych_binding(x|->y) = (tych x |-> tych y)
  14.593 + fun fail s = raise TFL_ERR{func = "mk_case", mesg = s}
  14.594 + fun mk{rows=[],...} = fail"no rows"
  14.595 +   | mk{path=[], rows = [([], (thm, bindings))]} = 
  14.596 +                         R.IT_EXISTS (map tych_binding bindings) thm
  14.597 +   | mk{path = u::rstp, rows as (p::_, _)::_} =
  14.598 +     let val (pat_rectangle,rights) = U.unzip rows
  14.599 +         val col0 = map hd pat_rectangle
  14.600 +         val pat_rectangle' = map tl pat_rectangle
  14.601 +     in 
  14.602 +     if (U.all S.is_var col0) (* column 0 is all variables *)
  14.603 +     then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[u|->v]))
  14.604 +                                (U.zip rights col0)
  14.605 +          in mk{path = rstp, rows = U.zip pat_rectangle' rights'}
  14.606 +          end
  14.607 +     else                     (* column 0 is all constructors *)
  14.608 +     let val ty_name = (#Tyop o S.dest_type o S.type_of) p
  14.609 +     in
  14.610 +     case (ty_info ty_name)
  14.611 +     of U.NONE => fail("Not a known datatype: "^ty_name)
  14.612 +      | U.SOME{constructors,nchotomy} =>
  14.613 +        let val thm' = R.ISPEC (tych u) nchotomy
  14.614 +            val disjuncts = S.strip_disj (concl thm')
  14.615 +            val subproblems = divide(constructors, rows)
  14.616 +            val groups      = map #group subproblems
  14.617 +            and new_formals = map #new_formals subproblems
  14.618 +            val existentials = U.map2 alpha_ex_unroll new_formals disjuncts
  14.619 +            val constraints = map #1 existentials
  14.620 +            val vexl = map #2 existentials
  14.621 +            fun expnd tm (pats,(th,b)) = (pats,(R.SUBS[R.ASSUME(tych tm)]th,b))
  14.622 +            val news = map (fn (nf,rows,c) => {path = nf@rstp, 
  14.623 +                                               rows = map (expnd c) rows})
  14.624 +                           (U.zip3 new_formals groups constraints)
  14.625 +            val recursive_thms = map mk news
  14.626 +            val build_exists = U.itlist(R.CHOOSE o (tych##(R.ASSUME o tych)))
  14.627 +            val thms' = U.map2 build_exists vexl recursive_thms
  14.628 +            val same_concls = R.EVEN_ORS thms'
  14.629 +        in R.DISJ_CASESL thm' same_concls
  14.630 +        end 
  14.631 +     end end
  14.632 + in mk
  14.633 + end;
  14.634 +
  14.635 +
  14.636 +fun complete_cases thy =
  14.637 + let val tych = Thry.typecheck thy
  14.638 +     fun pmk_var n ty = S.mk_var{Name = n,Ty = ty}
  14.639 +     val ty_info = Thry.induct_info thy
  14.640 + in fn pats =>
  14.641 + let val FV0 = S.free_varsl pats
  14.642 +     val a = S.variant FV0 (pmk_var "a" (S.type_of(hd pats)))
  14.643 +     val v = S.variant (a::FV0) (pmk_var "v" (S.type_of a))
  14.644 +     val FV = a::v::FV0
  14.645 +     val a_eq_v = S.mk_eq{lhs = a, rhs = v}
  14.646 +     val ex_th0 = R.EXISTS ((tych##tych) (S.mk_exists{Bvar=v,Body=a_eq_v},a))
  14.647 +                           (R.REFL (tych a))
  14.648 +     val th0 = R.ASSUME (tych a_eq_v)
  14.649 +     val rows = map (fn x => ([x], (th0,[]))) pats
  14.650 + in
  14.651 + R.GEN (tych a) 
  14.652 +       (R.RIGHT_ASSOC
  14.653 +          (R.CHOOSE(tych v, ex_th0)
  14.654 +                (mk_case ty_info FV thy {path=[v], rows=rows})))
  14.655 + end end;
  14.656 +
  14.657 +
  14.658 +(*---------------------------------------------------------------------------
  14.659 + * Constructing induction hypotheses: one for each recursive call.
  14.660 + *
  14.661 + * Note. R will never occur as a variable in the ind_clause, because
  14.662 + * to do so, it would have to be from a nested definition, and we don't
  14.663 + * allow nested defns to have R variable.
  14.664 + *
  14.665 + * Note. When the context is empty, there can be no local variables.
  14.666 + *---------------------------------------------------------------------------*)
  14.667 +
  14.668 +local nonfix ^ ;   infix 9 ^  ;     infix 5 ==>
  14.669 +      fun (tm1 ^ tm2)   = S.mk_comb{Rator = tm1, Rand = tm2}
  14.670 +      fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
  14.671 +in
  14.672 +fun build_ih f P (pat,TCs) = 
  14.673 + let val globals = S.free_vars_lr pat
  14.674 +     fun nested tm = U.can(S.find_term (S.aconv f)) tm handle _ => false
  14.675 +     fun dest_TC tm = 
  14.676 +         let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
  14.677 +             val (R,y,_) = S.dest_relation R_y_pat
  14.678 +             val P_y = if (nested tm) then R_y_pat ==> P^y else P^y
  14.679 +         in case cntxt 
  14.680 +              of [] => (P_y, (tm,[]))
  14.681 +               | _  => let 
  14.682 +                    val imp = S.list_mk_conj cntxt ==> P_y
  14.683 +                    val lvs = U.set_diff S.aconv (S.free_vars_lr imp) globals
  14.684 +                    val locals = #2(U.pluck (S.aconv P) lvs) handle _ => lvs
  14.685 +                    in (S.list_mk_forall(locals,imp), (tm,locals)) end
  14.686 +         end
  14.687 + in case TCs
  14.688 +    of [] => (S.list_mk_forall(globals, P^pat), [])
  14.689 +     |  _ => let val (ihs, TCs_locals) = U.unzip(map dest_TC TCs)
  14.690 +                 val ind_clause = S.list_mk_conj ihs ==> P^pat
  14.691 +             in (S.list_mk_forall(globals,ind_clause), TCs_locals)
  14.692 +             end
  14.693 + end
  14.694 +end;
  14.695 +
  14.696 +
  14.697 +
  14.698 +(*---------------------------------------------------------------------------
  14.699 + * This function makes good on the promise made in "build_ih: we prove
  14.700 + * <something>.
  14.701 + *
  14.702 + * Input  is tm = "(!y. R y pat ==> P y) ==> P pat",  
  14.703 + *           TCs = TC_1[pat] ... TC_n[pat]
  14.704 + *           thm = ih1 /\ ... /\ ih_n |- ih[pat]
  14.705 + *---------------------------------------------------------------------------*)
  14.706 +fun prove_case f thy (tm,TCs_locals,thm) =
  14.707 + let val tych = Thry.typecheck thy
  14.708 +     val antc = tych(#ant(S.dest_imp tm))
  14.709 +     val thm' = R.SPEC_ALL thm
  14.710 +     fun nested tm = U.can(S.find_term (S.aconv f)) tm handle _ => false
  14.711 +     fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC)))))
  14.712 +     fun mk_ih ((TC,locals),th2,nested) =
  14.713 +         R.GENL (map tych locals)
  14.714 +            (if nested 
  14.715 +              then R.DISCH (get_cntxt TC) th2 handle _ => th2
  14.716 +               else if S.is_imp(concl TC) 
  14.717 +                     then R.IMP_TRANS TC th2 
  14.718 +                      else R.MP th2 TC)
  14.719 + in 
  14.720 + R.DISCH antc
  14.721 + (if S.is_imp(concl thm') (* recursive calls in this clause *)
  14.722 +  then let val th1 = R.ASSUME antc
  14.723 +           val TCs = map #1 TCs_locals
  14.724 +           val ylist = map (#2 o S.dest_relation o #2 o S.strip_imp o 
  14.725 +                            #2 o S.strip_forall) TCs
  14.726 +           val TClist = map (fn(TC,lvs) => (R.SPEC_ALL(R.ASSUME(tych TC)),lvs))
  14.727 +                            TCs_locals
  14.728 +           val th2list = map (U.C R.SPEC th1 o tych) ylist
  14.729 +           val nlist = map nested TCs
  14.730 +           val triples = U.zip3 TClist th2list nlist
  14.731 +           val Pylist = map mk_ih triples
  14.732 +       in R.MP thm' (R.LIST_CONJ Pylist) end
  14.733 +  else thm')
  14.734 + end;
  14.735 +
  14.736 +
  14.737 +(*---------------------------------------------------------------------------
  14.738 + *
  14.739 + *         x = (v1,...,vn)  |- M[x]
  14.740 + *    ---------------------------------------------
  14.741 + *      ?v1 ... vn. x = (v1,...,vn) |- M[x]
  14.742 + *
  14.743 + *---------------------------------------------------------------------------*)
  14.744 +fun LEFT_ABS_VSTRUCT tych thm = 
  14.745 +  let fun CHOOSER v (tm,thm) = 
  14.746 +        let val ex_tm = S.mk_exists{Bvar=v,Body=tm}
  14.747 +        in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm)
  14.748 +        end
  14.749 +      val [veq] = U.filter (U.can S.dest_eq) (#1 (R.dest_thm thm))
  14.750 +      val {lhs,rhs} = S.dest_eq veq
  14.751 +      val L = S.free_vars_lr rhs
  14.752 +  in U.snd(U.itlist CHOOSER L (veq,thm))
  14.753 +  end;
  14.754 +
  14.755 +
  14.756 +fun combize M N = S.mk_comb{Rator=M,Rand=N};
  14.757 +fun eq v tm = S.mk_eq{lhs=v,rhs=tm};
  14.758 +
  14.759 +
  14.760 +(*----------------------------------------------------------------------------
  14.761 + * Input : f, R,  and  [(pat1,TCs1),..., (patn,TCsn)]
  14.762 + *
  14.763 + * Instantiates WF_INDUCTION_THM, getting Sinduct and then tries to prove
  14.764 + * recursion induction (Rinduct) by proving the antecedent of Sinduct from 
  14.765 + * the antecedent of Rinduct.
  14.766 + *---------------------------------------------------------------------------*)
  14.767 +fun mk_induction thy f R pat_TCs_list =
  14.768 +let val tych = Thry.typecheck thy
  14.769 +    val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM)
  14.770 +    val (pats,TCsl) = U.unzip pat_TCs_list
  14.771 +    val case_thm = complete_cases thy pats
  14.772 +    val domain = (S.type_of o hd) pats
  14.773 +    val P = S.variant (S.all_varsl (pats@flatten TCsl))
  14.774 +                      (S.mk_var{Name="P", Ty=domain --> S.bool})
  14.775 +    val Sinduct = R.SPEC (tych P) Sinduction
  14.776 +    val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct)
  14.777 +    val Rassums_TCl' = map (build_ih f P) pat_TCs_list
  14.778 +    val (Rassums,TCl') = U.unzip Rassums_TCl'
  14.779 +    val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
  14.780 +    val cases = map (S.beta_conv o combize Sinduct_assumf) pats
  14.781 +    val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
  14.782 +    val proved_cases = map (prove_case f thy) tasks
  14.783 +    val v = S.variant (S.free_varsl (map concl proved_cases))
  14.784 +                      (S.mk_var{Name="v", Ty=domain})
  14.785 +    val vtyped = tych v
  14.786 +    val substs = map (R.SYM o R.ASSUME o tych o eq v) pats
  14.787 +    val proved_cases1 = U.map2 (fn th => R.SUBS[th]) substs proved_cases
  14.788 +    val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1
  14.789 +    val dant = R.GEN vtyped (R.DISJ_CASESL (R.ISPEC vtyped case_thm) abs_cases)
  14.790 +    val dc = R.MP Sinduct dant
  14.791 +    val Parg_ty = S.type_of(#Bvar(S.dest_forall(concl dc)))
  14.792 +    val vars = map (gvvariant[P]) (S.strip_prod_type Parg_ty)
  14.793 +    val dc' = U.itlist (R.GEN o tych) vars
  14.794 +                       (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc)
  14.795 +in 
  14.796 +   R.GEN (tych P) (R.DISCH (tych(concl Rinduct_assum)) dc')
  14.797 +end 
  14.798 +handle _ => raise TFL_ERR{func = "mk_induction", mesg = "failed derivation"};
  14.799 +
  14.800 +
  14.801 +
  14.802 +(*---------------------------------------------------------------------------
  14.803 + * 
  14.804 + *                        POST PROCESSING
  14.805 + *
  14.806 + *---------------------------------------------------------------------------*)
  14.807 +
  14.808 +
  14.809 +fun simplify_induction thy hth ind = 
  14.810 +  let val tych = Thry.typecheck thy
  14.811 +      val (asl,_) = R.dest_thm ind
  14.812 +      val (_,tc_eq_tc') = R.dest_thm hth
  14.813 +      val tc = S.lhs tc_eq_tc'
  14.814 +      fun loop [] = ind
  14.815 +        | loop (asm::rst) = 
  14.816 +          if (U.can (Thry.match_term thy asm) tc)
  14.817 +          then R.UNDISCH
  14.818 +                 (R.MATCH_MP
  14.819 +                     (R.MATCH_MP Thms.simp_thm (R.DISCH (tych asm) ind)) 
  14.820 +                     hth)
  14.821 +         else loop rst
  14.822 +  in loop asl
  14.823 +end;
  14.824 +
  14.825 +
  14.826 +(*---------------------------------------------------------------------------
  14.827 + * The termination condition is an antecedent to the rule, and an 
  14.828 + * assumption to the theorem.
  14.829 + *---------------------------------------------------------------------------*)
  14.830 +fun elim_tc tcthm (rule,induction) = 
  14.831 +   (R.MP rule tcthm, R.PROVE_HYP tcthm induction)
  14.832 +
  14.833 +
  14.834 +fun postprocess{WFtac, terminator, simplifier} theory {rules,induction,TCs} =
  14.835 +let val tych = Thry.typecheck theory
  14.836 +
  14.837 +   (*---------------------------------------------------------------------
  14.838 +    * Attempt to eliminate WF condition. It's the only assumption of rules
  14.839 +    *---------------------------------------------------------------------*)
  14.840 +   val (rules1,induction1)  = 
  14.841 +       let val thm = R.prove(tych(hd(#1(R.dest_thm rules))),WFtac)
  14.842 +       in (R.PROVE_HYP thm rules,  R.PROVE_HYP thm induction)
  14.843 +       end handle _ => (rules,induction)
  14.844 +
  14.845 +   (*----------------------------------------------------------------------
  14.846 +    * The termination condition (tc) is simplified to |- tc = tc' (there
  14.847 +    * might not be a change!) and then 3 attempts are made:
  14.848 +    *
  14.849 +    *   1. if |- tc = T, then eliminate it with eqT; otherwise,
  14.850 +    *   2. apply the terminator to tc'. If |- tc' = T then eliminate; else
  14.851 +    *   3. replace tc by tc' in both the rules and the induction theorem.
  14.852 +    *---------------------------------------------------------------------*)
  14.853 +   fun simplify_tc tc (r,ind) =
  14.854 +       let val tc_eq = simplifier (tych tc)
  14.855 +       in 
  14.856 +       elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
  14.857 +       handle _ => 
  14.858 +        (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
  14.859 +                            (R.prove(tych(S.rhs(concl tc_eq)),terminator)))
  14.860 +                 (r,ind)
  14.861 +         handle _ => 
  14.862 +          (R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq), 
  14.863 +           simplify_induction theory tc_eq ind))
  14.864 +       end
  14.865 +
  14.866 +   (*----------------------------------------------------------------------
  14.867 +    * Nested termination conditions are harder to get at, since they are
  14.868 +    * left embedded in the body of the function (and in induction 
  14.869 +    * theorem hypotheses). Our "solution" is to simplify them, and try to 
  14.870 +    * prove termination, but leave the application of the resulting theorem 
  14.871 +    * to a higher level. So things go much as in "simplify_tc": the 
  14.872 +    * termination condition (tc) is simplified to |- tc = tc' (there might 
  14.873 +    * not be a change) and then 2 attempts are made:
  14.874 +    *
  14.875 +    *   1. if |- tc = T, then return |- tc; otherwise,
  14.876 +    *   2. apply the terminator to tc'. If |- tc' = T then return |- tc; else
  14.877 +    *   3. return |- tc = tc'
  14.878 +    *---------------------------------------------------------------------*)
  14.879 +   fun simplify_nested_tc tc =
  14.880 +      let val tc_eq = simplifier (tych (#2 (S.strip_forall tc)))
  14.881 +      in
  14.882 +      R.GEN_ALL
  14.883 +       (R.MATCH_MP Thms.eqT tc_eq
  14.884 +        handle _
  14.885 +        => (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
  14.886 +                      (R.prove(tych(S.rhs(concl tc_eq)),terminator))
  14.887 +            handle _ => tc_eq))
  14.888 +      end
  14.889 +
  14.890 +   (*-------------------------------------------------------------------
  14.891 +    * Attempt to simplify the termination conditions in each rule and 
  14.892 +    * in the induction theorem.
  14.893 +    *-------------------------------------------------------------------*)
  14.894 +   fun strip_imp tm = if S.is_neg tm then ([],tm) else S.strip_imp tm
  14.895 +   fun loop ([],extras,R,ind) = (rev R, ind, extras)
  14.896 +     | loop ((r,ftcs)::rst, nthms, R, ind) =
  14.897 +        let val tcs = #1(strip_imp (concl r))
  14.898 +            val extra_tcs = U.set_diff S.aconv ftcs tcs
  14.899 +            val extra_tc_thms = map simplify_nested_tc extra_tcs
  14.900 +            val (r1,ind1) = U.rev_itlist simplify_tc tcs (r,ind)
  14.901 +            val r2 = R.FILTER_DISCH_ALL(not o S.is_WFR) r1
  14.902 +        in loop(rst, nthms@extra_tc_thms, r2::R, ind1)
  14.903 +        end
  14.904 +   val rules_tcs = U.zip (R.CONJUNCTS rules1) TCs
  14.905 +   val (rules2,ind2,extras) = loop(rules_tcs,[],[],induction1)
  14.906 +in
  14.907 +  {induction = ind2, rules = R.LIST_CONJ rules2, nested_tcs = extras}
  14.908 +end;
  14.909 +
  14.910 +
  14.911 +(*---------------------------------------------------------------------------
  14.912 + * Extract termination goals so that they can be put it into a goalstack, or 
  14.913 + * have a tactic directly applied to them.
  14.914 + *--------------------------------------------------------------------------*)
  14.915 +local exception IS_NEG 
  14.916 +      fun strip_imp tm = if S.is_neg tm then raise IS_NEG else S.strip_imp tm
  14.917 +in
  14.918 +fun termination_goals rules = 
  14.919 +    U.itlist (fn th => fn A =>
  14.920 +        let val tcl = (#1 o S.strip_imp o #2 o S.strip_forall o concl) th
  14.921 +        in tcl@A
  14.922 +        end handle _ => A) (R.CONJUNCTS rules) (hyp rules)
  14.923 +end;
  14.924 +
  14.925 +end; (* TFL *)
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/TFL/thms.sig	Fri Oct 18 12:41:04 1996 +0200
    15.3 @@ -0,0 +1,16 @@
    15.4 +signature Thms_sig =
    15.5 +sig
    15.6 +   type Thm
    15.7 +   val WF_INDUCTION_THM:Thm
    15.8 +   val WFREC_COROLLARY :Thm
    15.9 +   val CUT_DEF         :Thm
   15.10 +   val CUT_LEMMA       :Thm
   15.11 +   val SELECT_AX       :Thm
   15.12 +   
   15.13 +   val COND_CONG :Thm
   15.14 +   val LET_CONG  :Thm
   15.15 +
   15.16 +   val eqT       :Thm
   15.17 +   val rev_eq_mp :Thm
   15.18 +   val simp_thm  :Thm
   15.19 +end;
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/TFL/thms.sml	Fri Oct 18 12:41:04 1996 +0200
    16.3 @@ -0,0 +1,39 @@
    16.4 +structure Thms : Thms_sig =
    16.5 +struct
    16.6 +   type Thm = Thm.thm
    16.7 +
    16.8 +   val WFREC_COROLLARY = get_thm WF1.thy "tfl_wfrec"
    16.9 +   val WF_INDUCTION_THM = get_thm WF1.thy "tfl_wf_induct"
   16.10 +   val CUT_LEMMA = get_thm WF1.thy "tfl_cut_apply"
   16.11 +   val CUT_DEF = cut_def
   16.12 +
   16.13 +   local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"
   16.14 +         val _ = by (strip_tac 1)
   16.15 +         val _ = by (rtac selectI 1)
   16.16 +         val _ = by (assume_tac 1)
   16.17 +   in val SELECT_AX = result()
   16.18 +   end;
   16.19 +
   16.20 +  (*-------------------------------------------------------------------------
   16.21 +   *  A useful congruence rule
   16.22 +   *-------------------------------------------------------------------------*)
   16.23 +   local val [p1,p2] = goal HOL.thy "(M = N) ==> \
   16.24 +                          \ (!!x. ((x = N) ==> (f x = g x))) ==> \
   16.25 +                          \ (Let M f = Let N g)";
   16.26 +         val _ = by (simp_tac (HOL_ss addsimps[Let_def,p1]) 1);
   16.27 +         val _ = by (rtac p2 1);
   16.28 +         val _ = by (rtac refl 1);
   16.29 +   in val LET_CONG = result() RS eq_reflection
   16.30 +   end;
   16.31 +
   16.32 +   val COND_CONG = if_cong RS eq_reflection;
   16.33 +
   16.34 +   fun C f x y = f y x;
   16.35 +   fun prover thl = [fast_tac HOL_cs 1];
   16.36 +   val P = C (prove_goal HOL.thy) prover;
   16.37 +
   16.38 +   val eqT       = P"(x = True) --> x"
   16.39 +   val rev_eq_mp = P"(x = y) --> y --> x"
   16.40 +   val simp_thm  = P"(x-->y) --> (x = x') --> (x' --> y)"
   16.41 +
   16.42 +end;
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/TFL/thry.sig	Fri Oct 18 12:41:04 1996 +0200
    17.3 @@ -0,0 +1,31 @@
    17.4 +signature Thry_sig =
    17.5 +sig
    17.6 +  type Type
    17.7 +  type Preterm
    17.8 +  type Term
    17.9 +  type Thm
   17.10 +  type Thry
   17.11 +  type 'a binding
   17.12 +
   17.13 +  structure USyntax : USyntax_sig
   17.14 +  val match_term : Thry -> Preterm -> Preterm 
   17.15 +                    -> Preterm binding list * Type binding list
   17.16 +
   17.17 +  val match_type : Thry -> Type -> Type -> Type binding list
   17.18 +
   17.19 +  val typecheck : Thry -> Preterm -> Term
   17.20 +
   17.21 +  val make_definition: Thry -> string -> Preterm -> Thm * Thry
   17.22 +
   17.23 +  (* Datatype facts of various flavours *)
   17.24 +  val match_info: Thry -> string -> {constructors:Preterm list,
   17.25 +                                     case_const:Preterm} USyntax.Utils.option
   17.26 +
   17.27 +  val induct_info: Thry -> string -> {constructors:Preterm list,
   17.28 +                                      nchotomy:Thm} USyntax.Utils.option
   17.29 +
   17.30 +  val extract_info: Thry -> {case_congs:Thm list, case_rewrites:Thm list}
   17.31 +
   17.32 +end;
   17.33 +
   17.34 +
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/TFL/thry.sml	Fri Oct 18 12:41:04 1996 +0200
    18.3 @@ -0,0 +1,139 @@
    18.4 +structure Thry : Thry_sig (* LThry_sig *) = 
    18.5 +struct
    18.6 +
    18.7 +structure USyntax  = USyntax;
    18.8 +type Type = USyntax.Type
    18.9 +type Preterm = USyntax.Preterm
   18.10 +type Term = USyntax.Term
   18.11 +type Thm = Thm.thm
   18.12 +type Thry = theory;
   18.13 +
   18.14 +open Mask;
   18.15 +structure S = USyntax;
   18.16 +
   18.17 +
   18.18 +fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
   18.19 +
   18.20 +(*---------------------------------------------------------------------------
   18.21 + *    Matching 
   18.22 + *---------------------------------------------------------------------------*)
   18.23 +
   18.24 +local open Utils
   18.25 +      infix 3 |->
   18.26 +      fun tybind (x,y) = TVar (x,["term"])  |-> y
   18.27 +      fun tmbind (x,y) = Var  (x,type_of y) |-> y
   18.28 +in
   18.29 + fun match_term thry pat ob = 
   18.30 +    let val tsig = #tsig(Sign.rep_sg(sign_of thry))
   18.31 +        val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
   18.32 +    in (map tmbind tm_theta, map tybind ty_theta)
   18.33 +    end
   18.34 +
   18.35 + fun match_type thry pat ob = 
   18.36 +    map tybind(Type.typ_match (#tsig(Sign.rep_sg(sign_of thry))) ([],(pat,ob)))
   18.37 +end;
   18.38 +
   18.39 +
   18.40 +(*---------------------------------------------------------------------------
   18.41 + * Typing 
   18.42 + *---------------------------------------------------------------------------*)
   18.43 +
   18.44 +fun typecheck thry = cterm_of (sign_of thry);
   18.45 +
   18.46 +
   18.47 +
   18.48 +(*----------------------------------------------------------------------------
   18.49 + * Making a definition. The argument "tm" looks like "f = WFREC R M". This 
   18.50 + * entrypoint is specialized for interactive use, since it closes the theory
   18.51 + * after making the definition. This allows later interactive definitions to
   18.52 + * refer to previous ones. The name for the new theory is automatically 
   18.53 + * generated from the name of the argument theory.
   18.54 + *---------------------------------------------------------------------------*)
   18.55 +local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection))
   18.56 +      val Const(eeq_name, ty) = eeq
   18.57 +      val prop = #2 (S.strip_type ty)
   18.58 +in
   18.59 +fun make_definition parent s tm = 
   18.60 +   let val {lhs,rhs} = S.dest_eq tm
   18.61 +       val {Name,Ty} = S.dest_var lhs
   18.62 +       val lhs1 = S.mk_const{Name = Name, Ty = Ty}
   18.63 +       val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop}
   18.64 +       val dtm = S.list_mk_comb(eeq1,[lhs1,rhs])      (* Rename "=" to "==" *)
   18.65 +       val thry1 = add_consts_i [(Name,Ty,NoSyn)] parent
   18.66 +       val thry2 = add_defs_i [(s,dtm)] thry1
   18.67 +       val parent_names = map ! (stamps_of_thy parent)
   18.68 +       val newthy_name = variant parent_names (hd parent_names)
   18.69 +       val new_thy = add_thyname newthy_name thry2
   18.70 +   in 
   18.71 +   ((get_axiom new_thy s) RS meta_eq_to_obj_eq, new_thy)
   18.72 +   end
   18.73 +end;
   18.74 +
   18.75 +
   18.76 +(*---------------------------------------------------------------------------
   18.77 + * Utility routine. Insert into list ordered by the key (a string). If two 
   18.78 + * keys are equal, the new element replaces the old. A more efficient option 
   18.79 + * for the future is needed. In fact, having the list of datatype facts be 
   18.80 + * ordered is useless, since the lookup should never fail!
   18.81 + *---------------------------------------------------------------------------*)
   18.82 +fun insert (el as (x:string, _)) = 
   18.83 + let fun canfind[] = [el] 
   18.84 +       | canfind(alist as ((y as (k,_))::rst)) = 
   18.85 +           if (x<k) then el::alist
   18.86 +           else if (x=k) then el::rst
   18.87 +           else y::canfind rst 
   18.88 + in canfind
   18.89 + end;
   18.90 +
   18.91 +
   18.92 +(*---------------------------------------------------------------------------
   18.93 + *     A collection of facts about datatypes
   18.94 + *---------------------------------------------------------------------------*)
   18.95 +val nat_record = Dtype.build_record (Nat.thy, ("nat",["0","Suc"]), nat_ind_tac)
   18.96 +val prod_record =
   18.97 +    let val prod_case_thms = Dtype.case_thms (sign_of Prod.thy) [split] 
   18.98 +                                 (fn s => res_inst_tac [("p",s)] PairE_lemma)
   18.99 +         fun const s = Const(s, the(Sign.const_type (sign_of Prod.thy) s))
  18.100 +     in ("*", 
  18.101 +         {constructors = [const "Pair"],
  18.102 +            case_const = const "split",
  18.103 +         case_rewrites = [split RS eq_reflection],
  18.104 +             case_cong = #case_cong prod_case_thms,
  18.105 +              nchotomy = #nchotomy prod_case_thms}) 
  18.106 +     end;
  18.107 +
  18.108 +(*---------------------------------------------------------------------------
  18.109 + * Hacks to make interactive mode work. Referring to "datatypes" directly
  18.110 + * is temporary, I hope!
  18.111 + *---------------------------------------------------------------------------*)
  18.112 +val match_info = fn thy =>
  18.113 +    fn "*" => Utils.SOME({case_const = #case_const (#2 prod_record),
  18.114 +                     constructors = #constructors (#2 prod_record)})
  18.115 +     | "nat" => Utils.SOME({case_const = #case_const (#2 nat_record),
  18.116 +                       constructors = #constructors (#2 nat_record)})
  18.117 +     | ty => case assoc(!datatypes,ty)
  18.118 +               of None => Utils.NONE
  18.119 +                | Some{case_const,constructors, ...} =>
  18.120 +                   Utils.SOME{case_const=case_const, constructors=constructors}
  18.121 +
  18.122 +val induct_info = fn thy =>
  18.123 +    fn "*" => Utils.SOME({nchotomy = #nchotomy (#2 prod_record),
  18.124 +                     constructors = #constructors (#2 prod_record)})
  18.125 +     | "nat" => Utils.SOME({nchotomy = #nchotomy (#2 nat_record),
  18.126 +                       constructors = #constructors (#2 nat_record)})
  18.127 +     | ty => case assoc(!datatypes,ty)
  18.128 +               of None => Utils.NONE
  18.129 +                | Some{nchotomy,constructors, ...} =>
  18.130 +                  Utils.SOME{nchotomy=nchotomy, constructors=constructors}
  18.131 +
  18.132 +val extract_info = fn thy => 
  18.133 + let val case_congs = map (#case_cong o #2) (!datatypes)
  18.134 +         val case_rewrites = flat(map (#case_rewrites o #2) (!datatypes))
  18.135 + in {case_congs = #case_cong (#2 prod_record)::
  18.136 +                  #case_cong (#2 nat_record)::case_congs,
  18.137 +     case_rewrites = #case_rewrites(#2 prod_record)@
  18.138 +                     #case_rewrites(#2 nat_record)@case_rewrites}
  18.139 + end;
  18.140 +
  18.141 +
  18.142 +end; (* Thry *)
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/TFL/usyntax.sig	Fri Oct 18 12:41:04 1996 +0200
    19.3 @@ -0,0 +1,134 @@
    19.4 +signature USyntax_sig =
    19.5 +sig
    19.6 +  structure Utils : Utils_sig
    19.7 +
    19.8 +  type Type
    19.9 +  type Term
   19.10 +  type Preterm
   19.11 +  type 'a binding
   19.12 +
   19.13 +  datatype lambda = VAR   of {Name : string, Ty : Type}
   19.14 +                  | CONST of {Name : string, Ty : Type}
   19.15 +                  | COMB  of {Rator: Preterm, Rand : Preterm}
   19.16 +                  | LAMB  of {Bvar : Preterm, Body : Preterm}
   19.17 +
   19.18 +  val alpha : Type
   19.19 +  val bool  : Type
   19.20 +  val mk_preterm : Term -> Preterm
   19.21 +  val drop_Trueprop : Preterm -> Preterm
   19.22 +
   19.23 +  (* Types *)
   19.24 +  val type_vars  : Type -> Type list
   19.25 +  val type_varsl : Type list -> Type list
   19.26 +  val mk_type    : {Tyop: string, Args:Type list} -> Type
   19.27 +  val dest_type  : Type -> {Tyop : string, Args : Type list}
   19.28 +  val mk_vartype : string -> Type
   19.29 +  val is_vartype : Type -> bool
   19.30 +  val -->        : Type * Type -> Type
   19.31 +  val strip_type : Type -> Type list * Type
   19.32 +  val strip_prod_type : Type -> Type list
   19.33 +  val match_type: Type -> Type -> Type binding list
   19.34 +
   19.35 +  (* Terms *)
   19.36 +  val free_vars  : Preterm -> Preterm list
   19.37 +  val free_varsl : Preterm list -> Preterm list
   19.38 +  val free_vars_lr : Preterm -> Preterm list
   19.39 +  val all_vars   : Preterm -> Preterm list
   19.40 +  val all_varsl  : Preterm list -> Preterm list
   19.41 +  val variant    : Preterm list -> Preterm -> Preterm
   19.42 +  val type_of    : Preterm -> Type
   19.43 +  val type_vars_in_term : Preterm -> Type list
   19.44 +  val dest_term  : Preterm -> lambda
   19.45 +  
   19.46 +  (* Prelogic *)
   19.47 +  val aconv     : Preterm -> Preterm -> bool
   19.48 +  val subst     : Preterm binding list -> Preterm -> Preterm
   19.49 +  val inst      : Type binding list -> Preterm -> Preterm
   19.50 +  val beta_conv : Preterm -> Preterm
   19.51 +
   19.52 +  (* Construction routines *)
   19.53 +  val mk_prop   :Preterm -> Preterm
   19.54 +  val mk_var    :{Name : string, Ty : Type} -> Preterm
   19.55 +  val mk_const  :{Name : string, Ty : Type} -> Preterm
   19.56 +  val mk_comb   :{Rator : Preterm, Rand : Preterm} -> Preterm
   19.57 +  val mk_abs    :{Bvar  : Preterm, Body : Preterm} -> Preterm
   19.58 +
   19.59 +  val mk_eq     :{lhs : Preterm, rhs : Preterm} -> Preterm
   19.60 +  val mk_imp    :{ant : Preterm, conseq :  Preterm} -> Preterm
   19.61 +  val mk_select :{Bvar : Preterm, Body : Preterm} -> Preterm
   19.62 +  val mk_forall :{Bvar : Preterm, Body : Preterm} -> Preterm
   19.63 +  val mk_exists :{Bvar : Preterm, Body : Preterm} -> Preterm
   19.64 +  val mk_conj   :{conj1 : Preterm, conj2 : Preterm} -> Preterm
   19.65 +  val mk_disj   :{disj1 : Preterm, disj2 : Preterm} -> Preterm
   19.66 +  val mk_pabs   :{varstruct : Preterm, body : Preterm} -> Preterm
   19.67 +
   19.68 +  (* Destruction routines *)
   19.69 +  val dest_var  : Preterm -> {Name : string, Ty : Type}
   19.70 +  val dest_const: Preterm -> {Name : string, Ty : Type}
   19.71 +  val dest_comb : Preterm -> {Rator : Preterm, Rand : Preterm}
   19.72 +  val dest_abs  : Preterm -> {Bvar : Preterm, Body : Preterm}
   19.73 +  val dest_eq     : Preterm -> {lhs : Preterm, rhs : Preterm}
   19.74 +  val dest_imp    : Preterm -> {ant : Preterm, conseq : Preterm}
   19.75 +  val dest_select : Preterm -> {Bvar : Preterm, Body : Preterm}
   19.76 +  val dest_forall : Preterm -> {Bvar : Preterm, Body : Preterm}
   19.77 +  val dest_exists : Preterm -> {Bvar : Preterm, Body : Preterm}
   19.78 +  val dest_neg    : Preterm -> Preterm
   19.79 +  val dest_conj   : Preterm -> {conj1 : Preterm, conj2 : Preterm}
   19.80 +  val dest_disj   : Preterm -> {disj1 : Preterm, disj2 : Preterm}
   19.81 +  val dest_pair   : Preterm -> {fst : Preterm, snd : Preterm}
   19.82 +  val dest_pabs   : Preterm -> {varstruct : Preterm, body : Preterm}
   19.83 +
   19.84 +  val lhs   : Preterm -> Preterm
   19.85 +  val rhs   : Preterm -> Preterm
   19.86 +  val rator : Preterm -> Preterm
   19.87 +  val rand  : Preterm -> Preterm
   19.88 +  val bvar  : Preterm -> Preterm
   19.89 +  val body  : Preterm -> Preterm
   19.90 +  
   19.91 +
   19.92 +  (* Query routines *)
   19.93 +  val is_var  : Preterm -> bool
   19.94 +  val is_const: Preterm -> bool
   19.95 +  val is_comb : Preterm -> bool
   19.96 +  val is_abs  : Preterm -> bool
   19.97 +  val is_eq     : Preterm -> bool
   19.98 +  val is_imp    : Preterm -> bool
   19.99 +  val is_forall : Preterm -> bool 
  19.100 +  val is_exists : Preterm -> bool 
  19.101 +  val is_neg    : Preterm -> bool
  19.102 +  val is_conj   : Preterm -> bool
  19.103 +  val is_disj   : Preterm -> bool
  19.104 +  val is_pair   : Preterm -> bool
  19.105 +  val is_pabs   : Preterm -> bool
  19.106 +
  19.107 +  (* Construction of a Preterm from a list of Preterms *)
  19.108 +  val list_mk_comb   : (Preterm * Preterm list) -> Preterm
  19.109 +  val list_mk_abs    : (Preterm list * Preterm) -> Preterm
  19.110 +  val list_mk_imp    : (Preterm list * Preterm) -> Preterm
  19.111 +  val list_mk_forall : (Preterm list * Preterm) -> Preterm
  19.112 +  val list_mk_exists : (Preterm list * Preterm) -> Preterm
  19.113 +  val list_mk_conj   : Preterm list -> Preterm
  19.114 +  val list_mk_disj   : Preterm list -> Preterm
  19.115 +
  19.116 +  (* Destructing a Preterm to a list of Preterms *)
  19.117 +  val strip_comb     : Preterm -> (Preterm * Preterm list)
  19.118 +  val strip_abs      : Preterm -> (Preterm list * Preterm)
  19.119 +  val strip_imp      : Preterm -> (Preterm list * Preterm)
  19.120 +  val strip_forall   : Preterm -> (Preterm list * Preterm)
  19.121 +  val strip_exists   : Preterm -> (Preterm list * Preterm)
  19.122 +  val strip_conj     : Preterm -> Preterm list
  19.123 +  val strip_disj     : Preterm -> Preterm list
  19.124 +  val strip_pair     : Preterm -> Preterm list
  19.125 +
  19.126 +  (* Miscellaneous *)
  19.127 +  val mk_vstruct : Type -> Preterm list -> Preterm
  19.128 +  val gen_all    : Preterm -> Preterm
  19.129 +  val find_term  : (Preterm -> bool) -> Preterm -> Preterm
  19.130 +  val find_terms : (Preterm -> bool) -> Preterm -> Preterm list
  19.131 +  val dest_relation : Preterm -> Preterm * Preterm * Preterm
  19.132 +  val is_WFR : Preterm -> bool
  19.133 +  val ARB : Type -> Preterm
  19.134 +
  19.135 +  (* Prettyprinting *)
  19.136 +  val Term_to_string : Term -> string
  19.137 +end;
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/TFL/usyntax.sml	Fri Oct 18 12:41:04 1996 +0200
    20.3 @@ -0,0 +1,482 @@
    20.4 +structure USyntax : USyntax_sig =
    20.5 +struct
    20.6 +
    20.7 +structure Utils = Utils;
    20.8 +open Utils;
    20.9 +open Mask;
   20.10 +
   20.11 +infix 7 |->;
   20.12 +infix 4 ##;
   20.13 +
   20.14 +fun ERR{func,mesg} = Utils.ERR{module = "USyntax", func = func, mesg = mesg};
   20.15 +
   20.16 +type Type = typ
   20.17 +type Term = cterm
   20.18 +type Preterm = term
   20.19 +
   20.20 +
   20.21 +(*---------------------------------------------------------------------------
   20.22 + *
   20.23 + *                            Types 
   20.24 + *
   20.25 + *---------------------------------------------------------------------------*)
   20.26 +fun mk_type{Tyop, Args} = Type(Tyop,Args);
   20.27 +val mk_prim_vartype = TVar;
   20.28 +fun mk_vartype s = mk_prim_vartype((s,0),["term"]);
   20.29 +
   20.30 +fun dest_type(Type(ty,args)) = {Tyop = ty, Args = args}
   20.31 +  | dest_type _ = raise ERR{func = "dest_type", mesg = "Not a compound type"};
   20.32 +
   20.33 +
   20.34 +(* But internally, it's useful *)
   20.35 +fun dest_vtype (TVar x) = x
   20.36 +  | dest_vtype _ = raise ERR{func = "dest_vtype", 
   20.37 +                             mesg = "not a flexible type variable"};
   20.38 +
   20.39 +val is_vartype = Utils.can dest_vtype;
   20.40 +
   20.41 +val type_vars  = map mk_prim_vartype o typ_tvars
   20.42 +fun type_varsl L = Utils.mk_set (Utils.curry op=)
   20.43 +                      (Utils.rev_itlist (Utils.curry op @ o type_vars) L []);
   20.44 +
   20.45 +val alpha  = mk_vartype "'a"
   20.46 +val beta   = mk_vartype "'b"
   20.47 +
   20.48 +val bool = Type("bool",[]);
   20.49 +
   20.50 +fun match_type ty1 ty2 = raise ERR{func="match_type",mesg="not implemented"};
   20.51 +
   20.52 +
   20.53 +(* What nonsense *)
   20.54 +nonfix -->; 
   20.55 +val --> = -->;
   20.56 +infixr 3 -->;
   20.57 +
   20.58 +(* hol_type -> hol_type list * hol_type *)
   20.59 +fun strip_type ty =
   20.60 +   let val {Tyop = "fun", Args = [ty1,ty2]} = dest_type ty
   20.61 +       val (D,r) = strip_type ty2
   20.62 +   in (ty1::D, r)
   20.63 +   end
   20.64 +   handle _ => ([],ty);
   20.65 +
   20.66 +(* hol_type -> hol_type list *)
   20.67 +fun strip_prod_type ty =
   20.68 +   let val {Tyop = "*", Args = [ty1,ty2]} = dest_type ty
   20.69 +   in strip_prod_type ty1 @ strip_prod_type ty2
   20.70 +   end handle _ => [ty];
   20.71 +
   20.72 +
   20.73 +
   20.74 +(*---------------------------------------------------------------------------
   20.75 + *
   20.76 + *                              Terms 
   20.77 + *
   20.78 + *---------------------------------------------------------------------------*)
   20.79 +nonfix aconv;
   20.80 +val aconv = Utils.curry (op aconv);
   20.81 +
   20.82 +fun free_vars tm = add_term_frees(tm,[]);
   20.83 +
   20.84 +
   20.85 +(* Free variables, in order of occurrence, from left to right in the 
   20.86 + * syntax tree. *)
   20.87 +fun free_vars_lr tm = 
   20.88 +  let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end
   20.89 +      fun add (t, frees) = case t of
   20.90 +            Free   _ => if (memb t frees) then frees else t::frees
   20.91 +          | Abs (_,_,body) => add(body,frees)
   20.92 +          | f$t =>  add(t, add(f, frees))
   20.93 +          | _ => frees
   20.94 +  in rev(add(tm,[]))
   20.95 +  end;
   20.96 +
   20.97 +
   20.98 +
   20.99 +fun free_varsl L = Utils.mk_set aconv
  20.100 +                      (Utils.rev_itlist (Utils.curry op @ o free_vars) L []);
  20.101 +
  20.102 +val type_of =  type_of;
  20.103 +val type_vars_in_term = map mk_prim_vartype o term_tvars;
  20.104 +
  20.105 +(* Can't really be very exact in Isabelle *)
  20.106 +fun all_vars tm = 
  20.107 +  let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end
  20.108 +      fun add (t, A) = case t of
  20.109 +            Free   _ => if (memb t A) then A else t::A
  20.110 +          | Abs (s,ty,body) => add(body, add(Free(s,ty),A))
  20.111 +          | f$t =>  add(t, add(f, A))
  20.112 +          | _ => A
  20.113 +  in rev(add(tm,[]))
  20.114 +  end;
  20.115 +fun all_varsl L = Utils.mk_set aconv
  20.116 +                      (Utils.rev_itlist (Utils.curry op @ o all_vars) L []);
  20.117 +
  20.118 +
  20.119 +(* Prelogic *)
  20.120 +val subst = subst_free o map (fn (a |-> b) => (a,b));
  20.121 +
  20.122 +fun dest_tybinding (v |-> ty) = (#1(dest_vtype v),ty)
  20.123 +fun inst theta = subst_vars (map dest_tybinding theta,[])
  20.124 +
  20.125 +fun beta_conv((t1 as Abs _ ) $ t2) = betapply(t1,t2)
  20.126 +  | beta_conv _ = raise ERR{func = "beta_conv", mesg = "Not a beta-redex"};
  20.127 +
  20.128 +
  20.129 +(* Construction routines *)
  20.130 +(* fun mk_var{Name,Ty} = Var((Name,0),Ty); *)
  20.131 +fun mk_var{Name,Ty} = Free(Name,Ty);
  20.132 +val mk_prim_var = Var;
  20.133 +
  20.134 +val string_variant = variant;
  20.135 +
  20.136 +local fun var_name(Var((Name,_),_)) = Name
  20.137 +        | var_name(Free(s,_)) = s
  20.138 +        | var_name _ = raise ERR{func = "variant",
  20.139 +                                 mesg = "list elem. is not a variable"}
  20.140 +in
  20.141 +fun variant [] v = v
  20.142 +  | variant vlist (Var((Name,i),ty)) = 
  20.143 +       Var((string_variant (map var_name vlist) Name,i),ty)
  20.144 +  | variant vlist (Free(Name,ty)) =
  20.145 +       Free(string_variant (map var_name vlist) Name,ty)
  20.146 +  | variant _ _ = raise ERR{func = "variant",
  20.147 +                            mesg = "2nd arg. should be a variable"}
  20.148 +end;
  20.149 +
  20.150 +fun mk_const{Name,Ty} = Const(Name,Ty)
  20.151 +fun mk_comb{Rator,Rand} = Rator $ Rand;
  20.152 +
  20.153 +fun mk_abs{Bvar as Var((s,_),ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
  20.154 +  | mk_abs{Bvar as Free(s,ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
  20.155 +  | mk_abs _ = raise ERR{func = "mk_abs", mesg = "Bvar is not a variable"};
  20.156 +
  20.157 +fun list_mk_comb (h,[]) = h
  20.158 +  | list_mk_comb (h,L) =
  20.159 +      rev_itlist (fn t1 => fn t2 => mk_comb{Rator = t2, Rand = t1}) L h;
  20.160 +
  20.161 +
  20.162 +fun mk_eq{lhs,rhs} = 
  20.163 +   let val ty = type_of lhs
  20.164 +       val c = mk_const{Name = "op =", Ty = ty --> ty --> bool}
  20.165 +   in list_mk_comb(c,[lhs,rhs])
  20.166 +   end
  20.167 +
  20.168 +fun mk_imp{ant,conseq} = 
  20.169 +   let val c = mk_const{Name = "op -->", Ty = bool --> bool --> bool}
  20.170 +   in list_mk_comb(c,[ant,conseq])
  20.171 +   end;
  20.172 +
  20.173 +fun mk_select (r as {Bvar,Body}) = 
  20.174 +  let val ty = type_of Bvar
  20.175 +      val c = mk_const{Name = "Eps", Ty = (ty --> bool) --> ty}
  20.176 +  in list_mk_comb(c,[mk_abs r])
  20.177 +  end;
  20.178 +
  20.179 +fun mk_forall (r as {Bvar,Body}) = 
  20.180 +  let val ty = type_of Bvar
  20.181 +      val c = mk_const{Name = "All", Ty = (ty --> bool) --> bool}
  20.182 +  in list_mk_comb(c,[mk_abs r])
  20.183 +  end;
  20.184 +
  20.185 +fun mk_exists (r as {Bvar,Body}) = 
  20.186 +  let val ty = type_of Bvar 
  20.187 +      val c = mk_const{Name = "Ex", Ty = (ty --> bool) --> bool}
  20.188 +  in list_mk_comb(c,[mk_abs r])
  20.189 +  end;
  20.190 +
  20.191 +
  20.192 +fun mk_conj{conj1,conj2} =
  20.193 +   let val c = mk_const{Name = "op &", Ty = bool --> bool --> bool}
  20.194 +   in list_mk_comb(c,[conj1,conj2])
  20.195 +   end;
  20.196 +
  20.197 +fun mk_disj{disj1,disj2} =
  20.198 +   let val c = mk_const{Name = "op |", Ty = bool --> bool --> bool}
  20.199 +   in list_mk_comb(c,[disj1,disj2])
  20.200 +   end;
  20.201 +
  20.202 +fun prod_ty ty1 ty2 = mk_type{Tyop = "*", Args = [ty1,ty2]};
  20.203 +
  20.204 +local
  20.205 +fun mk_uncurry(xt,yt,zt) =
  20.206 +    mk_const{Name = "split", Ty = (xt --> yt --> zt) --> prod_ty xt yt --> zt}
  20.207 +fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
  20.208 +  | dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"}
  20.209 +fun is_var(Var(_)) = true | is_var (Free _) = true | is_var _ = false
  20.210 +in
  20.211 +fun mk_pabs{varstruct,body} = 
  20.212 + let fun mpa(varstruct,body) =
  20.213 +       if (is_var varstruct)
  20.214 +       then mk_abs{Bvar = varstruct, Body = body}
  20.215 +       else let val {fst,snd} = dest_pair varstruct
  20.216 +            in mk_comb{Rator= mk_uncurry(type_of fst,type_of snd,type_of body),
  20.217 +                       Rand = mpa(fst,mpa(snd,body))}
  20.218 +            end
  20.219 + in mpa(varstruct,body)
  20.220 + end
  20.221 + handle _ => raise ERR{func = "mk_pabs", mesg = ""};
  20.222 +end;
  20.223 +
  20.224 +(* Destruction routines *)
  20.225 +
  20.226 +datatype lambda = VAR   of {Name : string, Ty : Type}
  20.227 +                | CONST of {Name : string, Ty : Type}
  20.228 +                | COMB  of {Rator: Preterm, Rand : Preterm}
  20.229 +                | LAMB  of {Bvar : Preterm, Body : Preterm};
  20.230 +
  20.231 +
  20.232 +fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty}
  20.233 +  | dest_term(Free(s,ty))    = VAR{Name = s, Ty = ty}
  20.234 +  | dest_term(Const(s,ty))   = CONST{Name = s, Ty = ty}
  20.235 +  | dest_term(M$N)           = COMB{Rator=M,Rand=N}
  20.236 +  | dest_term(Abs(s,ty,M))   = let  val v = mk_var{Name = s, Ty = ty}
  20.237 +                               in LAMB{Bvar = v, Body = betapply (M,v)}
  20.238 +                               end
  20.239 +  | dest_term(Bound _)       = raise ERR{func = "dest_term",mesg = "Bound"};
  20.240 +
  20.241 +fun dest_var(Var((s,i),ty)) = {Name = s, Ty = ty}
  20.242 +  | dest_var(Free(s,ty))    = {Name = s, Ty = ty}
  20.243 +  | dest_var _ = raise ERR{func = "dest_var", mesg = "not a variable"};
  20.244 +
  20.245 +fun dest_const(Const(s,ty)) = {Name = s, Ty = ty}
  20.246 +  | dest_const _ = raise ERR{func = "dest_const", mesg = "not a constant"};
  20.247 +
  20.248 +fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2}
  20.249 +  | dest_comb _ =  raise ERR{func = "dest_comb", mesg = "not a comb"};
  20.250 +
  20.251 +fun dest_abs(a as Abs(s,ty,M)) = 
  20.252 +     let val v = mk_var{Name = s, Ty = ty}
  20.253 +     in {Bvar = v, Body = betapply (a,v)}
  20.254 +     end
  20.255 +  | dest_abs _ =  raise ERR{func = "dest_abs", mesg = "not an abstraction"};
  20.256 +
  20.257 +fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N}
  20.258 +  | dest_eq _ = raise ERR{func = "dest_eq", mesg = "not an equality"};
  20.259 +
  20.260 +fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N}
  20.261 +  | dest_imp _ = raise ERR{func = "dest_imp", mesg = "not an implication"};
  20.262 +
  20.263 +fun dest_select(Const("Eps",_) $ (a as Abs _)) = dest_abs a
  20.264 +  | dest_select _ = raise ERR{func = "dest_select", mesg = "not a select"};
  20.265 +
  20.266 +fun dest_forall(Const("All",_) $ (a as Abs _)) = dest_abs a
  20.267 +  | dest_forall _ = raise ERR{func = "dest_forall", mesg = "not a forall"};
  20.268 +
  20.269 +fun dest_exists(Const("Ex",_) $ (a as Abs _)) = dest_abs a
  20.270 +  | dest_exists _ = raise ERR{func = "dest_exists", mesg="not an existential"};
  20.271 +
  20.272 +fun dest_neg(Const("not",_) $ M) = M
  20.273 +  | dest_neg _ = raise ERR{func = "dest_neg", mesg = "not a negation"};
  20.274 +
  20.275 +fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N}
  20.276 +  | dest_conj _ = raise ERR{func = "dest_conj", mesg = "not a conjunction"};
  20.277 +
  20.278 +fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N}
  20.279 +  | dest_disj _ = raise ERR{func = "dest_disj", mesg = "not a disjunction"};
  20.280 +
  20.281 +fun mk_pair{fst,snd} = 
  20.282 +   let val ty1 = type_of fst
  20.283 +       val ty2 = type_of snd
  20.284 +       val c = mk_const{Name = "Pair", Ty = ty1 --> ty2 --> prod_ty ty1 ty2}
  20.285 +   in list_mk_comb(c,[fst,snd])
  20.286 +   end;
  20.287 +
  20.288 +fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
  20.289 +  | dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"};
  20.290 +
  20.291 +
  20.292 +local  val ucheck = Utils.assert (curry (op =) "split" o #Name o dest_const)
  20.293 +in
  20.294 +fun dest_pabs tm =
  20.295 +   let val {Bvar,Body} = dest_abs tm
  20.296 +   in {varstruct = Bvar, body = Body}
  20.297 +   end handle _ 
  20.298 +   => let val {Rator,Rand} = dest_comb tm
  20.299 +          val _ = ucheck Rator
  20.300 +          val {varstruct = lv,body} = dest_pabs Rand
  20.301 +          val {varstruct = rv,body} = dest_pabs body
  20.302 +      in {varstruct = mk_pair{fst = lv, snd = rv}, body = body}
  20.303 +      end
  20.304 +end;
  20.305 +
  20.306 +
  20.307 +(* Garbage - ought to be dropped *)
  20.308 +val lhs   = #lhs o dest_eq
  20.309 +val rhs   = #rhs o dest_eq
  20.310 +val rator = #Rator o dest_comb
  20.311 +val rand  = #Rand o dest_comb
  20.312 +val bvar  = #Bvar o dest_abs
  20.313 +val body  = #Body o dest_abs
  20.314 +  
  20.315 +
  20.316 +(* Query routines *)
  20.317 +val is_var    = can dest_var
  20.318 +val is_const  = can dest_const
  20.319 +val is_comb   = can dest_comb
  20.320 +val is_abs    = can dest_abs
  20.321 +val is_eq     = can dest_eq
  20.322 +val is_imp    = can dest_imp
  20.323 +val is_forall = can dest_forall
  20.324 +val is_exists = can dest_exists
  20.325 +val is_neg    = can dest_neg
  20.326 +val is_conj   = can dest_conj
  20.327 +val is_disj   = can dest_disj
  20.328 +val is_pair   = can dest_pair
  20.329 +val is_pabs   = can dest_pabs
  20.330 +
  20.331 +
  20.332 +(* Construction of a Term from a list of Terms *)
  20.333 +
  20.334 +fun list_mk_abs(L,tm) = itlist (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
  20.335 +
  20.336 +(* These others are almost never used *)
  20.337 +fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
  20.338 +fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists{Bvar=v, Body=b})V t;
  20.339 +fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
  20.340 +val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
  20.341 +val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj{disj1=d1, disj2=tm})
  20.342 +
  20.343 +
  20.344 +(* Need to reverse? *)
  20.345 +fun gen_all tm = list_mk_forall(free_vars tm, tm);
  20.346 +
  20.347 +(* Destructing a Term to a list of Terms *)
  20.348 +fun strip_comb tm = 
  20.349 +   let fun dest(M$N, A) = dest(M, N::A)
  20.350 +         | dest x = x
  20.351 +   in dest(tm,[])
  20.352 +   end;
  20.353 +
  20.354 +fun strip_abs(tm as Abs _) =
  20.355 +       let val {Bvar,Body} = dest_abs tm
  20.356 +           val (bvs, core) = strip_abs Body
  20.357 +       in (Bvar::bvs, core)
  20.358 +       end
  20.359 +  | strip_abs M = ([],M);
  20.360 +
  20.361 +
  20.362 +fun strip_imp fm =
  20.363 +   if (is_imp fm)
  20.364 +   then let val {ant,conseq} = dest_imp fm
  20.365 +	    val (was,wb) = strip_imp conseq
  20.366 +        in ((ant::was), wb)
  20.367 +        end
  20.368 +   else ([],fm);
  20.369 +
  20.370 +fun strip_forall fm =
  20.371 +   if (is_forall fm)
  20.372 +   then let val {Bvar,Body} = dest_forall fm
  20.373 +            val (bvs,core) = strip_forall Body
  20.374 +        in ((Bvar::bvs), core)
  20.375 +        end
  20.376 +   else ([],fm);
  20.377 +
  20.378 +
  20.379 +fun strip_exists fm =
  20.380 +   if (is_exists fm)
  20.381 +   then let val {Bvar, Body} = dest_exists fm 
  20.382 +            val (bvs,core) = strip_exists Body
  20.383 +        in (Bvar::bvs, core)
  20.384 +        end
  20.385 +   else ([],fm);
  20.386 +
  20.387 +fun strip_conj w = 
  20.388 +   if (is_conj w)
  20.389 +   then let val {conj1,conj2} = dest_conj w
  20.390 +        in (strip_conj conj1@strip_conj conj2)
  20.391 +        end
  20.392 +   else [w];
  20.393 +
  20.394 +fun strip_disj w =
  20.395 +   if (is_disj w)
  20.396 +   then let val {disj1,disj2} = dest_disj w 
  20.397 +        in (strip_disj disj1@strip_disj disj2)
  20.398 +        end
  20.399 +   else [w];
  20.400 +
  20.401 +fun strip_pair tm = 
  20.402 +   if (is_pair tm) 
  20.403 +   then let val {fst,snd} = dest_pair tm
  20.404 +            fun dtuple t =
  20.405 +               if (is_pair t)
  20.406 +               then let val{fst,snd} = dest_pair t
  20.407 +                    in (fst :: dtuple snd)
  20.408 +                    end
  20.409 +               else [t]
  20.410 +        in fst::dtuple snd
  20.411 +        end
  20.412 +   else [tm];
  20.413 +
  20.414 +
  20.415 +fun mk_preterm tm = #t(rep_cterm tm);
  20.416 +
  20.417 +fun mk_prop (tm as Const("Trueprop",_) $ _) = tm
  20.418 +  | mk_prop tm = mk_comb{Rator=mk_const{Name = "Trueprop", 
  20.419 +                           Ty = bool --> mk_type{Tyop = "prop",Args=[]}},
  20.420 +                         Rand = tm};
  20.421 +
  20.422 +fun drop_Trueprop (Const("Trueprop",_) $ X) = X
  20.423 +  | drop_Trueprop X = X;
  20.424 +
  20.425 +(* Miscellaneous *)
  20.426 +
  20.427 +fun mk_vstruct ty V =
  20.428 +  let fun follow_prod_type ty vs =
  20.429 +      let val {Tyop = "*", Args = [ty1,ty2]} = dest_type ty
  20.430 +          val (ltm,vs1) = follow_prod_type ty1 vs
  20.431 +          val (rtm,vs2) = follow_prod_type ty2 vs1
  20.432 +      in (mk_pair{fst=ltm, snd=rtm}, vs2)
  20.433 +      end handle _ => (hd vs, tl vs)
  20.434 + in fst(follow_prod_type ty V)
  20.435 + end;
  20.436 +
  20.437 +
  20.438 +(* Search a term for a sub-term satisfying the predicate p. *)
  20.439 +fun find_term p =
  20.440 +   let fun find tm =
  20.441 +      if (p tm)
  20.442 +      then tm 
  20.443 +      else if (is_abs tm)
  20.444 +           then find (#Body(dest_abs tm))
  20.445 +           else let val {Rator,Rand} = dest_comb tm
  20.446 +                in find Rator handle _ => find Rand
  20.447 +                end handle _ => raise ERR{func = "find_term",mesg = ""}
  20.448 +   in find
  20.449 +   end;
  20.450 +
  20.451 +(*******************************************************************
  20.452 + * find_terms: (term -> bool) -> term -> term list
  20.453 + * 
  20.454 + *  Find all subterms in a term that satisfy a given predicate p.
  20.455 + *
  20.456 + *******************************************************************)
  20.457 +fun find_terms p =
  20.458 +   let fun accum tl tm =
  20.459 +      let val tl' = if (p tm) then (tm::tl) else tl 
  20.460 +      in if (is_abs tm)
  20.461 +         then accum tl' (#Body(dest_abs tm))
  20.462 +         else let val {Rator,Rand} = dest_comb tm
  20.463 +              in accum (accum tl' Rator) Rand
  20.464 +              end handle _ => tl'
  20.465 +      end
  20.466 +   in accum []
  20.467 +   end;
  20.468 +
  20.469 +
  20.470 +val Term_to_string = string_of_cterm;
  20.471 +
  20.472 +fun dest_relation tm =
  20.473 +   if (type_of tm = bool)
  20.474 +   then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
  20.475 +        in (R,y,x)
  20.476 +        end handle _ => raise ERR{func="dest_relation",
  20.477 +                                  mesg="unexpected term structure"}
  20.478 +   else raise ERR{func="dest_relation",mesg="not a boolean term"};
  20.479 +
  20.480 +fun is_WFR tm = (#Name(dest_const(rator tm)) = "wf") handle _ => false;
  20.481 +
  20.482 +fun ARB ty = mk_select{Bvar=mk_var{Name="v",Ty=ty},
  20.483 +                       Body=mk_const{Name="True",Ty=bool}};
  20.484 +
  20.485 +end; (* Syntax *)
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/TFL/utils.sig	Fri Oct 18 12:41:04 1996 +0200
    21.3 @@ -0,0 +1,55 @@
    21.4 +signature Utils_sig =
    21.5 +sig
    21.6 +  (* General error format and reporting mechanism *)
    21.7 +  exception ERR of {module:string,func:string, mesg:string}
    21.8 +  val Raise : exn -> 'a
    21.9 +
   21.10 +  (* infix 3 ## *)
   21.11 +  val ## : ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd
   21.12 +  val can   : ('a -> 'b) -> 'a -> bool
   21.13 +  val holds : ('a -> bool) -> 'a -> bool
   21.14 +  val assert: ('a -> bool) -> 'a -> 'a
   21.15 +  val W : ('a -> 'a -> 'b) -> 'a -> 'b
   21.16 +  val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
   21.17 +  val I : 'a -> 'a
   21.18 +  val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
   21.19 +  val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c
   21.20 +  val fst : 'a * 'b -> 'a
   21.21 +  val snd : 'a * 'b -> 'b
   21.22 +
   21.23 +  (* option type *)
   21.24 +  datatype 'a option = SOME of 'a | NONE
   21.25 +
   21.26 +  (* Set operations *)
   21.27 +  val mem : ('a -> 'a -> bool) -> 'a -> 'a list -> bool
   21.28 +  val union : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
   21.29 +  val Union : ('a -> 'a -> bool) -> 'a list list ->  'a list
   21.30 +  val intersect : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
   21.31 +  val set_diff : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list
   21.32 +  val mk_set : ('a -> 'a -> bool) -> 'a list -> 'a list
   21.33 +  val set_eq : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
   21.34 +
   21.35 +  val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   21.36 +  val itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   21.37 +  val rev_itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   21.38 +  val end_itlist : ('a -> 'a -> 'a) -> 'a list -> 'a
   21.39 +  val itlist2 :('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   21.40 +  val filter : ('a -> bool) -> 'a list -> 'a list
   21.41 +  val mapfilter : ('a -> 'b) -> 'a list -> 'b list
   21.42 +  val pluck : ('a -> bool) -> 'a list -> 'a * 'a list
   21.43 +  val assoc1 : ('a*'a->bool) -> 'a -> ('a * 'b) list -> ('a * 'b) option
   21.44 +  val front_back : 'a list -> 'a list * 'a
   21.45 +  val all : ('a -> bool) -> 'a list -> bool
   21.46 +  val exists : ('a -> bool) -> 'a list -> bool
   21.47 +  val zip : 'a list -> 'b list -> ('a*'b) list
   21.48 +  val zip3 : 'a list -> 'b list -> 'c list -> ('a*'b*'c) list
   21.49 +  val unzip : ('a*'b) list -> ('a list * 'b list)
   21.50 +  val take  : ('a -> 'b) -> int * 'a list -> 'b list
   21.51 +  val sort  : ('a -> 'a -> bool) -> 'a list -> 'a list
   21.52 +
   21.53 +  val int_to_string : int -> string
   21.54 +  val concat : string -> string -> string
   21.55 +  val quote : string -> string
   21.56 +
   21.57 +end;
   21.58 +
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/TFL/utils.sml	Fri Oct 18 12:41:04 1996 +0200
    22.3 @@ -0,0 +1,197 @@
    22.4 +(*---------------------------------------------------------------------------
    22.5 + * Some common utilities. This strucuture is parameterized over
    22.6 + * "int_to_string" because there is a difference between the string 
    22.7 + * operations of SML/NJ versions 93 and 109.
    22.8 + *---------------------------------------------------------------------------*)
    22.9 +
   22.10 +functor UTILS (val int_to_string : int -> string) :Utils_sig = 
   22.11 +struct
   22.12 +
   22.13 +(* Standard exception for TFL. *)
   22.14 +exception ERR of {module:string,func:string, mesg:string};
   22.15 +fun UTILS_ERR{func,mesg} = ERR{module = "Utils",func=func,mesg=mesg};
   22.16 +
   22.17 +local 
   22.18 +fun info_string s {module,func,mesg} =
   22.19 +       (s^" at "^module^"."^func^":\n"^mesg^"\n")
   22.20 +in
   22.21 +val ERR_string = info_string "Exception raised"
   22.22 +val MESG_string = info_string "Message"
   22.23 +end;
   22.24 +
   22.25 +fun Raise (e as ERR sss) = (output(std_out, ERR_string sss);  raise e)
   22.26 +  | Raise e = raise e;
   22.27 +
   22.28 +
   22.29 +(* option type *)
   22.30 +datatype 'a option = SOME of 'a | NONE
   22.31 +
   22.32 +
   22.33 +(* Simple combinators *)
   22.34 +
   22.35 +infix 3 ##
   22.36 +fun f ## g = (fn (x,y) => (f x, g y))
   22.37 +
   22.38 +fun W f x = f x x
   22.39 +fun C f x y = f y x
   22.40 +fun I x = x
   22.41 +
   22.42 +fun curry f x y = f(x,y)
   22.43 +fun uncurry f (x,y) = f x y
   22.44 +
   22.45 +fun fst(x,y) = x
   22.46 +fun snd(x,y) = y;
   22.47 +
   22.48 +val concat = curry (op ^)
   22.49 +fun quote s = "\""^s^"\"";
   22.50 +
   22.51 +fun map2 f L1 L2 =
   22.52 + let fun mp2 [] [] L = rev L
   22.53 +       | mp2 (a1::rst1) (a2::rst2) L = mp2 rst1 rst2 (f a1 a2::L)
   22.54 +       | mp2 _ _ _ = raise UTILS_ERR{func="map2",mesg="different length lists"}
   22.55 +   in mp2 L1 L2 []
   22.56 +   end;
   22.57 +
   22.58 +
   22.59 +fun itlist f L base_value =
   22.60 +   let fun it [] = base_value
   22.61 +         | it (a::rst) = f a (it rst)
   22.62 +   in it L 
   22.63 +   end;
   22.64 +
   22.65 +fun rev_itlist f =
   22.66 +   let fun rev_it [] base = base
   22.67 +         | rev_it (a::rst) base = rev_it rst (f a base)
   22.68 +   in rev_it
   22.69 +   end;
   22.70 +
   22.71 +fun end_itlist f =
   22.72 +   let fun endit [] = raise UTILS_ERR{func="end_itlist", mesg="list too short"}
   22.73 +         | endit alist = 
   22.74 +            let val (base::ralist) = rev alist
   22.75 +            in itlist f (rev ralist) base
   22.76 +            end
   22.77 +   in endit
   22.78 +   end;
   22.79 +
   22.80 +fun itlist2 f L1 L2 base_value =
   22.81 + let fun it ([],[]) = base_value
   22.82 +       | it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2))
   22.83 +       | it _ = raise UTILS_ERR{func="itlist2",mesg="different length lists"}
   22.84 + in  it (L1,L2)
   22.85 + end;
   22.86 +
   22.87 +fun filter p L = itlist (fn x => fn y => if (p x) then x::y else y) L []
   22.88 +
   22.89 +fun mapfilter f alist = itlist (fn i=>fn L=> (f i::L) handle _ => L) alist [];
   22.90 +
   22.91 +fun pluck p  =
   22.92 +  let fun remv ([],_) = raise UTILS_ERR{func="pluck",mesg = "item not found"}
   22.93 +        | remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A)
   22.94 +  in fn L => remv(L,[])
   22.95 +  end;
   22.96 +
   22.97 +fun front_back [] = raise UTILS_ERR{func="front_back",mesg="empty list"}
   22.98 +  | front_back [x] = ([],x)
   22.99 +  | front_back (h::t) = 
  22.100 +       let val (L,b) = front_back t
  22.101 +       in (h::L,b)
  22.102 +       end;
  22.103 +
  22.104 +fun take f =
  22.105 +  let fun grab(0,L) = []
  22.106 +        | grab(n, x::rst) = f x::grab(n-1,rst)
  22.107 +  in grab
  22.108 +  end;
  22.109 +
  22.110 +fun all p =
  22.111 +   let fun every [] = true
  22.112 +         | every (a::rst) = (p a) andalso every rst       
  22.113 +   in every 
  22.114 +   end;
  22.115 +
  22.116 +fun exists p =
  22.117 +   let fun ex [] = false
  22.118 +         | ex (a::rst) = (p a) orelse ex rst       
  22.119 +   in ex 
  22.120 +   end;
  22.121 +
  22.122 +fun zip [] [] = []
  22.123 +  | zip (a::b) (c::d) = (a,c)::(zip b d)
  22.124 +  | zip _ _ = raise UTILS_ERR{func = "zip",mesg = "different length lists"};
  22.125 +
  22.126 +fun unzip L = itlist (fn (x,y) => fn (l1,l2) =>((x::l1),(y::l2))) L ([],[]);
  22.127 +
  22.128 +fun zip3 [][][] = []
  22.129 +  | zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3
  22.130 +  | zip3 _ _ _ = raise UTILS_ERR{func="zip3",mesg="different lengths"};
  22.131 +
  22.132 +
  22.133 +fun can f x = (f x ; true) handle _ => false;
  22.134 +fun holds P x = P x handle _ => false;
  22.135 +
  22.136 +
  22.137 +fun assert p x = 
  22.138 + if (p x) then x else raise UTILS_ERR{func="assert", mesg="predicate not true"}
  22.139 +
  22.140 +fun assoc1 eq item =
  22.141 +   let fun assc ((entry as (key,_))::rst) = 
  22.142 +             if eq(item,key) then SOME entry else assc rst
  22.143 +         | assc [] = NONE
  22.144 +    in assc
  22.145 +    end;
  22.146 +
  22.147 +(* Set ops *)
  22.148 +nonfix mem union;  (* Gag Barf Choke *)
  22.149 +fun mem eq_func i =
  22.150 +   let val eqi = eq_func i
  22.151 +       fun mm [] = false
  22.152 +         | mm (a::rst) = eqi a orelse mm rst
  22.153 +   in mm
  22.154 +   end;
  22.155 +
  22.156 +fun union eq_func =
  22.157 +   let val mem = mem eq_func
  22.158 +       fun un S1 []  = S1
  22.159 +         | un [] S1  = S1
  22.160 +         | un (a::rst) S2 = if (mem a S2) then (un rst S2) else (a::un rst S2)
  22.161 +   in un
  22.162 +   end;
  22.163 +
  22.164 +fun mk_set eq_func =
  22.165 +   let val mem = mem eq_func
  22.166 +       fun mk [] = []
  22.167 +         | mk (a::rst) = if (mem a rst) then mk rst else a::(mk rst)
  22.168 +   in mk
  22.169 +   end;
  22.170 +
  22.171 +(* Union of a family of sets *)
  22.172 +fun Union eq_func set_o_sets = itlist (union eq_func) set_o_sets [];
  22.173 +
  22.174 +fun intersect eq_func S1 S2 = mk_set eq_func (filter (C (mem eq_func) S2) S1);
  22.175 +
  22.176 +(* All the elements in the first set that are not also in the second set. *)
  22.177 +fun set_diff eq_func S1 S2 = filter (fn x => not (mem eq_func x S2)) S1
  22.178 +
  22.179 +fun set_eq eq_func S1 S2 = 
  22.180 +   null(set_diff eq_func S1 S2) andalso null(set_diff eq_func S2 S1);
  22.181 +
  22.182 +
  22.183 +fun sort R = 
  22.184 +let fun part (m, []) = ([],[])
  22.185 +      | part (m, h::rst) =
  22.186 +         let val (l1,l2) = part (m,rst)
  22.187 +         in if (R h m) then (h::l1, l2)
  22.188 +                       else (l1,  h::l2) end
  22.189 +    fun qsort [] = []
  22.190 +      | qsort (h::rst) = 
  22.191 +        let val (l1,l2) = part(h,rst)
  22.192 +        in qsort l1@ [h] @qsort l2
  22.193 +        end
  22.194 +in qsort
  22.195 +end;
  22.196 +
  22.197 +
  22.198 +val int_to_string = int_to_string;
  22.199 +
  22.200 +end; (* Utils *)