tryres, gen_make_elim moved here;
authorwenzelm
Mon Oct 04 21:37:35 1999 +0200 (1999-10-04 ago)
changeset 769420121c9dc1a6
parent 7693 c3e0c26e7d6f
child 7695 6d7f9f30e6df
tryres, gen_make_elim moved here;
src/ZF/ind_syntax.ML
     1.1 --- a/src/ZF/ind_syntax.ML	Mon Oct 04 21:37:00 1999 +0200
     1.2 +++ b/src/ZF/ind_syntax.ML	Mon Oct 04 21:37:35 1999 +0200
     1.3 @@ -101,8 +101,9 @@
     1.4  
     1.5  fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
     1.6  
     1.7 -val Un          = Const("op Un", [iT,iT]--->iT)
     1.8 -and empty       = Const("0", iT)
     1.9 +fun mk_Un (t1, t2) = Const("op Un", [iT,iT]--->iT) $ t1 $ t2;
    1.10 +
    1.11 +val empty       = Const("0", iT)
    1.12  and univ        = Const("Univ.univ", iT-->iT)
    1.13  and quniv       = Const("QUniv.quniv", iT-->iT);
    1.14  
    1.15 @@ -112,7 +113,7 @@
    1.16        fun is_ind arg = (type_of arg = iT)
    1.17    in  case filter is_ind (args @ cs) of
    1.18           []     => empty
    1.19 -       | u_args => fold_bal (app Un) u_args
    1.20 +       | u_args => fold_bal mk_Un u_args
    1.21    end;
    1.22  
    1.23  (*univ or quniv constitutes the sum domain for mutual recursion;
    1.24 @@ -151,9 +152,18 @@
    1.25                  make_elim succ_inject, 
    1.26                  refl_thin, conjE, exE, disjE];
    1.27  
    1.28 +
    1.29 +(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
    1.30 +fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
    1.31 +  | tryres (th, []) = raise THM("tryres", 0, [th]);
    1.32 +
    1.33 +fun gen_make_elim elim_rls rl = 
    1.34 +      standard (tryres (rl, elim_rls @ [revcut_rl]));
    1.35 +
    1.36  (*Turns iff rules into safe elimination rules*)
    1.37  fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]);
    1.38  
    1.39 +
    1.40  end;
    1.41  
    1.42