SUBPROOF/Obtain.result: named params;
authorwenzelm
Sun Jul 26 18:57:11 2009 +0200 (2009-07-26)
changeset 32202443d5cfaba1b
parent 32201 3689b647356d
child 32209 9a829b9ef003
SUBPROOF/Obtain.result: named params;
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sun Jul 26 13:21:12 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Jul 26 18:57:11 2009 +0200
     1.3 @@ -1257,7 +1257,7 @@
     1.4              [resolve_tac exists_fresh' 1,
     1.5               simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms @
     1.6                 fin_set_supp @ ths)) 1]);
     1.7 -        val (([cx], ths), ctxt') = Obtain.result
     1.8 +        val (([(_, cx)], ths), ctxt') = Obtain.result
     1.9            (fn _ => EVERY
    1.10              [etac exE 1,
    1.11               full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
    1.12 @@ -1324,7 +1324,7 @@
    1.13                         val _ $ (_ $ _ $ u) = concl';
    1.14                         val U = fastype_of u;
    1.15                         val (xs, params') =
    1.16 -                         chop (length cargs) (map term_of params);
    1.17 +                         chop (length cargs) (map (term_of o #2) params);
    1.18                         val Ts = map fastype_of xs;
    1.19                         val cnstr = Const (cname, Ts ---> U);
    1.20                         val (pis, z) = split_last params';
    1.21 @@ -1640,7 +1640,7 @@
    1.22                      REPEAT_DETERM (resolve_tac [allI, impI] 1),
    1.23                      REPEAT_DETERM (etac conjE 1),
    1.24                      rtac unique 1,
    1.25 -                    SUBPROOF (fn {prems = prems', params = [a, b], ...} => EVERY
    1.26 +                    SUBPROOF (fn {prems = prems', params = [(_, a), (_, b)], ...} => EVERY
    1.27                        [cut_facts_tac [rec_prem] 1,
    1.28                         rtac (Thm.instantiate ([],
    1.29                           [(cterm_of thy11 (Var (("pi", 0), mk_permT aT)),
    1.30 @@ -1693,7 +1693,7 @@
    1.31               REPEAT_DETERM (dresolve_tac (the (AList.lookup op = rec_fin_supp T)) 1),
    1.32               resolve_tac exists_fresh' 1,
    1.33               asm_simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms)) 1]);
    1.34 -        val (([cx], ths), ctxt') = Obtain.result
    1.35 +        val (([(_, cx)], ths), ctxt') = Obtain.result
    1.36            (fn _ => EVERY
    1.37              [etac exE 1,
    1.38               full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
    1.39 @@ -1763,7 +1763,7 @@
    1.40                      val cargsr' = partition_cargs idxs cargsr;
    1.41                      val boundsr = List.concat (map fst cargsr');
    1.42                      val (params1, _ :: params2) =
    1.43 -                      chop (length params div 2) (map term_of params);
    1.44 +                      chop (length params div 2) (map (term_of o #2) params);
    1.45                      val params' = params1 @ params2;
    1.46                      val rec_prems = filter (fn th => case prop_of th of
    1.47                          _ $ p => (case head_of p of
     2.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sun Jul 26 13:21:12 2009 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Jul 26 18:57:11 2009 +0200
     2.3 @@ -301,7 +301,7 @@
     2.4            (fn _ => EVERY
     2.5              [resolve_tac exists_fresh' 1,
     2.6               resolve_tac fs_atoms 1]);
     2.7 -        val (([cx], ths), ctxt') = Obtain.result
     2.8 +        val (([(_, cx)], ths), ctxt') = Obtain.result
     2.9            (fn _ => EVERY
    2.10              [etac exE 1,
    2.11               full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
    2.12 @@ -319,7 +319,7 @@
    2.13               SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} =>
    2.14                 let
    2.15                   val (params', (pis, z)) =
    2.16 -                   chop (length params - length atomTs - 1) (map term_of params) ||>
    2.17 +                   chop (length params - length atomTs - 1) (map (term_of o #2) params) ||>
    2.18                     split_last;
    2.19                   val bvars' = map
    2.20                     (fn (Bound i, T) => (nth params' (length params' - i), T)
    2.21 @@ -474,7 +474,7 @@
    2.22                  rtac (first_order_mrs case_hyps case_hyp) 1
    2.23                else
    2.24                  let
    2.25 -                  val params' = map (term_of o nth (rev params)) is;
    2.26 +                  val params' = map (term_of o #2 o nth (rev params)) is;
    2.27                    val tab = params' ~~ map fst qs;
    2.28                    val (hyps1, hyps2) = chop (length args) case_hyps;
    2.29                    (* turns a = t and [x1 # t, ..., xn # t] *)
    2.30 @@ -635,7 +635,7 @@
    2.31              val prems'' = map (fn th => Simplifier.simplify eqvt_ss
    2.32                (mk_perm_bool (cterm_of thy pi) th)) prems';
    2.33              val intr' = Drule.cterm_instantiate (map (cterm_of thy) vs ~~
    2.34 -               map (cterm_of thy o NominalDatatype.mk_perm [] pi o term_of) params)
    2.35 +               map (cterm_of thy o NominalDatatype.mk_perm [] pi o term_of o #2) params)
    2.36                 intr
    2.37            in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1
    2.38            end) ctxt' 1 st
     3.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Sun Jul 26 13:21:12 2009 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Sun Jul 26 18:57:11 2009 +0200
     3.3 @@ -323,7 +323,7 @@
     3.4          val avoid_th = Drule.instantiate'
     3.5            [SOME (ctyp_of thy (fastype_of p))] [SOME (cterm_of thy p)]
     3.6            ([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding});
     3.7 -        val (([cx], th1 :: th2 :: ths), ctxt') = Obtain.result
     3.8 +        val (([(_, cx)], th1 :: th2 :: ths), ctxt') = Obtain.result
     3.9            (fn _ => EVERY
    3.10              [rtac avoid_th 1,
    3.11               full_simp_tac (HOL_ss addsimps [@{thm fresh_star_prod_set}]) 1,
    3.12 @@ -359,7 +359,7 @@
    3.13               SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} =>
    3.14                 let
    3.15                   val (cparams', (pis, z)) =
    3.16 -                   chop (length params - length atomTs - 1) params ||>
    3.17 +                   chop (length params - length atomTs - 1) (map #2 params) ||>
    3.18                     (map term_of #> split_last);
    3.19                   val params' = map term_of cparams'
    3.20                   val sets' = map (apfst (curry subst_bounds (rev params'))) sets;