src/HOL/Tools/inductive_package.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -124,7 +124,7 @@
     1.4  fun put_inductives names info thy =
     1.5    let
     1.6      fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
     1.7 -    val tab_monos = foldl upd (InductiveData.get thy, names)
     1.8 +    val tab_monos = Library.foldl upd (InductiveData.get thy, names)
     1.9        handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
    1.10    in InductiveData.put tab_monos thy end;
    1.11  
    1.12 @@ -183,16 +183,16 @@
    1.13      fun varify (t, (i, ts)) =
    1.14        let val t' = map_term_types (incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
    1.15        in (maxidx_of_term t', t'::ts) end;
    1.16 -    val (i, cs') = foldr varify (cs, (~1, []));
    1.17 -    val (i', intr_ts') = foldr varify (intr_ts, (i, []));
    1.18 -    val rec_consts = foldl add_term_consts_2 ([], cs');
    1.19 -    val intr_consts = foldl add_term_consts_2 ([], intr_ts');
    1.20 +    val (i, cs') = Library.foldr varify (cs, (~1, []));
    1.21 +    val (i', intr_ts') = Library.foldr varify (intr_ts, (i, []));
    1.22 +    val rec_consts = Library.foldl add_term_consts_2 ([], cs');
    1.23 +    val intr_consts = Library.foldl add_term_consts_2 ([], intr_ts');
    1.24      fun unify (env, (cname, cT)) =
    1.25 -      let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
    1.26 -      in foldl (fn ((env', j'), Tp) => (Type.unify tsig (env', j') Tp))
    1.27 +      let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
    1.28 +      in Library.foldl (fn ((env', j'), Tp) => (Type.unify tsig (env', j') Tp))
    1.29            (env, (replicate (length consts) cT) ~~ consts)
    1.30        end;
    1.31 -    val (env, _) = foldl unify ((Vartab.empty, i'), rec_consts);
    1.32 +    val (env, _) = Library.foldl unify ((Vartab.empty, i'), rec_consts);
    1.33      fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T
    1.34        in if T = T' then T else typ_subst_TVars_2 env T' end;
    1.35      val subst = fst o Type.freeze_thaw o
    1.36 @@ -237,7 +237,7 @@
    1.37  
    1.38  fun mg_prod_factors ts (fs, t $ u) = if t mem ts then
    1.39          let val f = prod_factors [] u
    1.40 -        in overwrite (fs, (t, f inter if_none (assoc (fs, t)) f)) end
    1.41 +        in overwrite (fs, (t, f inter (curry getOpt) (assoc (fs, t)) f)) end
    1.42        else mg_prod_factors ts (mg_prod_factors ts (fs, t), u)
    1.43    | mg_prod_factors ts (fs, Abs (_, _, t)) = mg_prod_factors ts (fs, t)
    1.44    | mg_prod_factors ts (fs, _) = fs;
    1.45 @@ -256,7 +256,7 @@
    1.46  
    1.47  fun mk_tuple p ps (Type ("*", [T1, T2])) (tms as t::_) =
    1.48        if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms, 
    1.49 -        mk_tuple (2::p) ps T2 (drop (length (prodT_factors (1::p) ps T1), tms)))
    1.50 +        mk_tuple (2::p) ps T2 (Library.drop (length (prodT_factors (1::p) ps T1), tms)))
    1.51        else t
    1.52    | mk_tuple _ _ _ (t::_) = t;
    1.53  
    1.54 @@ -271,12 +271,12 @@
    1.55  
    1.56  val remove_split = rewrite_rule [split_conv RS eq_reflection];
    1.57  
    1.58 -fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
    1.59 +fun split_rule_vars vs rl = standard (remove_split (Library.foldr split_rule_var'
    1.60    (mg_prod_factors vs ([], Thm.prop_of rl), rl)));
    1.61  
    1.62 -fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
    1.63 -  (mapfilter (fn (t as Var ((a, _), _)) =>
    1.64 -    apsome (pair t) (assoc (vs, a))) (term_vars (Thm.prop_of rl)), rl)));
    1.65 +fun split_rule vs rl = standard (remove_split (Library.foldr split_rule_var'
    1.66 +  (List.mapPartial (fn (t as Var ((a, _), _)) =>
    1.67 +    Option.map (pair t) (assoc (vs, a))) (term_vars (Thm.prop_of rl)), rl)));
    1.68  
    1.69  
    1.70  (** process rules **)
    1.71 @@ -315,7 +315,7 @@
    1.72          if u mem cs then
    1.73            if exists (Logic.occs o rpair t) cs then
    1.74              err_in_rule sg name rule "Recursion term on left of member symbol"
    1.75 -          else seq check_prem (prems ~~ aprems)
    1.76 +          else List.app check_prem (prems ~~ aprems)
    1.77          else err_in_rule sg name rule bad_concl
    1.78        | Const ("all", _) $ _ => err_in_rule sg name rule all_not_allowed
    1.79        | _ => err_in_rule sg name rule bad_concl);
    1.80 @@ -337,7 +337,7 @@
    1.81  
    1.82  fun mk_elims cs cTs params intr_ts intr_names =
    1.83    let
    1.84 -    val used = foldr add_term_names (intr_ts, []);
    1.85 +    val used = Library.foldr add_term_names (intr_ts, []);
    1.86      val [aname, pname] = variantlist (["a", "P"], used);
    1.87      val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
    1.88  
    1.89 @@ -353,9 +353,9 @@
    1.90          val a = Free (aname, T);
    1.91  
    1.92          fun mk_elim_prem (_, t, ts) =
    1.93 -          list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
    1.94 +          list_all_free (map dest_Free ((Library.foldr add_term_frees (t::ts, [])) \\ params),
    1.95              Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
    1.96 -        val c_intrs = (filter (equal c o #1 o #1) intrs);
    1.97 +        val c_intrs = (List.filter (equal c o #1 o #1) intrs);
    1.98        in
    1.99          (Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
   1.100            map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs)
   1.101 @@ -369,7 +369,7 @@
   1.102  
   1.103  fun mk_indrule cs cTs params intr_ts =
   1.104    let
   1.105 -    val used = foldr add_term_names (intr_ts, []);
   1.106 +    val used = Library.foldr add_term_names (intr_ts, []);
   1.107  
   1.108      (* predicates for induction rule *)
   1.109  
   1.110 @@ -407,22 +407,22 @@
   1.111            HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   1.112  
   1.113        in list_all_free (frees,
   1.114 -           Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
   1.115 +           Logic.list_implies (map HOLogic.mk_Trueprop (Library.foldr mk_prem
   1.116               (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
   1.117 -               HOLogic.mk_Trueprop (the (pred_of u) $ t)))
   1.118 +               HOLogic.mk_Trueprop (valOf (pred_of u) $ t)))
   1.119        end;
   1.120  
   1.121      val ind_prems = map mk_ind_prem intr_ts;
   1.122  
   1.123 -    val factors = foldl (mg_prod_factors preds) ([], ind_prems);
   1.124 +    val factors = Library.foldl (mg_prod_factors preds) ([], ind_prems);
   1.125  
   1.126      (* make conclusions for induction rules *)
   1.127  
   1.128      fun mk_ind_concl ((c, P), (ts, x)) =
   1.129        let val T = HOLogic.dest_setT (fastype_of c);
   1.130 -          val ps = if_none (assoc (factors, P)) [];
   1.131 +          val ps = getOpt (assoc (factors, P), []);
   1.132            val Ts = prodT_factors [] ps T;
   1.133 -          val (frees, x') = foldr (fn (T', (fs, s)) =>
   1.134 +          val (frees, x') = Library.foldr (fn (T', (fs, s)) =>
   1.135              ((Free (s, T'))::fs, Symbol.bump_string s)) (Ts, ([], x));
   1.136            val tuple = mk_tuple [] ps T frees;
   1.137        in ((HOLogic.mk_binop "op -->"
   1.138 @@ -430,7 +430,7 @@
   1.139        end;
   1.140  
   1.141      val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   1.142 -        (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
   1.143 +        (fst (Library.foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
   1.144  
   1.145    in (preds, ind_prems, mutual_ind_concl,
   1.146      map (apfst (fst o dest_Free)) factors)
   1.147 @@ -481,7 +481,7 @@
   1.148    Goals.prove_goalw_cterm []      (*NO quick_and_dirty_prove_goalw_cterm here!*)
   1.149      (Thm.cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
   1.150        (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
   1.151 -    (fn _ => [rtac monoI 1, REPEAT (ares_tac (flat (map mk_mono monos) @ get_monos thy) 1)]));
   1.152 +    (fn _ => [rtac monoI 1, REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)]));
   1.153  
   1.154  
   1.155  (* prove introduction rules *)
   1.156 @@ -628,7 +628,7 @@
   1.157  
   1.158      val dummy = if !trace then
   1.159  		(writeln "ind_prems = ";
   1.160 -		 seq (writeln o Sign.string_of_term sign) ind_prems)
   1.161 +		 List.app (writeln o Sign.string_of_term sign) ind_prems)
   1.162  	    else ();
   1.163  
   1.164      (* make predicate for instantiation of abstract induction rule *)
   1.165 @@ -639,7 +639,7 @@
   1.166               val Type (_, [T1, T2]) = T
   1.167           in Const ("Datatype.sum.sum_case",
   1.168             [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
   1.169 -             mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
   1.170 +             mk_ind_pred T1 (Library.take (n, Ps)) $ mk_ind_pred T2 (Library.drop (n, Ps))
   1.171           end;
   1.172  
   1.173      val ind_pred = mk_ind_pred sumT preds;
   1.174 @@ -655,7 +655,7 @@
   1.175          (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.176            (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
   1.177             HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
   1.178 -             nth_elem (find_index_eq c cs, preds)))))
   1.179 +             List.nth (preds, find_index_eq c cs)))))
   1.180          (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
   1.181  
   1.182      val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
   1.183 @@ -707,7 +707,7 @@
   1.184  
   1.185      val fp_name = if coind then gfp_name else lfp_name;
   1.186  
   1.187 -    val used = foldr add_term_names (intr_ts, []);
   1.188 +    val used = Library.foldr add_term_names (intr_ts, []);
   1.189      val [sname, xname] = variantlist (["S", "x"], used);
   1.190  
   1.191      (* transform an introduction rule into a conjunction  *)
   1.192 @@ -723,7 +723,7 @@
   1.193          val Const ("op :", _) $ t $ u =
   1.194            HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   1.195  
   1.196 -      in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
   1.197 +      in Library.foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
   1.198          (frees, foldr1 HOLogic.mk_conj
   1.199            (((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
   1.200              (map (subst o HOLogic.dest_Trueprop)