src/HOL/Nominal/nominal_inductive.ML

   | transp xs = map hd xs :: transp (map tl xs);
 
 fun add_binders thy i (t as (_ $ _)) bs = (case strip_comb t of
       (Const (s, T), ts) => (case strip_type T of
         (Ts, Type (tname, _)) =>
-          (case Nominal.get_nominal_datatype thy tname of
+          (case NominalDatatype.get_nominal_datatype thy tname of
              NONE => fold (add_binders thy i) ts bs
            | SOME {descr, index, ...} => (case AList.lookup op =
                  (#3 (the (AList.lookup op = descr index))) s of
                NONE => fold (add_binders thy i) ts bs
              | SOME cargs => fst (fold (fn (xs, x) => fn (bs', cargs') =>

           if T = U then SOME (HOLogic.mk_Trueprop
             (HOLogic.mk_not (HOLogic.eq_const T $ x $ y)))
           else NONE) xs @ mk_distinct xs;
 
     fun mk_fresh (x, T) = HOLogic.mk_Trueprop
-      (Nominal.fresh_const T fsT $ x $ Bound 0);
+      (NominalDatatype.fresh_const T fsT $ x $ Bound 0);
 
     val (prems', prems'') = split_list (map (fn (params, bvars, prems, (p, ts)) =>
       let
         val params' = params @ [("y", fsT)];
         val prem = Logic.list_implies

     val ind_Ts = rev (map snd ind_vars);
 
     val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
       (map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem,
         HOLogic.list_all (ind_vars, lift_pred p
-          (map (fold_rev (Nominal.mk_perm ind_Ts)
+          (map (fold_rev (NominalDatatype.mk_perm ind_Ts)
             (map Bound (length atomTs downto 1))) ts)))) concls));
 
     val concl' = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
       (map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem,
         lift_pred' (Free (fs_ctxt_name, fsT)) p ts)) concls));

           (List.mapPartial (fn prem =>
              if null (preds_of ps prem) then SOME prem
              else map_term (split_conj (K o I) names) prem prem) prems, q))))
         (mk_distinct bvars @
          maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop
-           (Nominal.fresh_const U T $ u $ t)) bvars)
+           (NominalDatatype.fresh_const U T $ u $ t)) bvars)
              (ts ~~ binder_types (fastype_of p)))) prems;
 
     val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
     val pt2_atoms = map (fn aT => PureThy.get_thm thy
       ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;

         fun protect t =
           let val T = fastype_of t in Const ("Fun.id", T --> T) $ t end;
         val p = foldr1 HOLogic.mk_prod (map protect ts @ freshs1);
         val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop
             (HOLogic.exists_const T $ Abs ("x", T,
-              Nominal.fresh_const T (fastype_of p) $
+              NominalDatatype.fresh_const T (fastype_of p) $
                 Bound 0 $ p)))
           (fn _ => EVERY
             [resolve_tac exists_fresh' 1,
              resolve_tac fs_atoms 1]);
         val (([cx], ths), ctxt') = Obtain.result

                    split_last;
                  val bvars' = map
                    (fn (Bound i, T) => (nth params' (length params' - i), T)
                      | (t, T) => (t, T)) bvars;
                  val pi_bvars = map (fn (t, _) =>
-                   fold_rev (Nominal.mk_perm []) pis t) bvars';
+                   fold_rev (NominalDatatype.mk_perm []) pis t) bvars';
                  val (P, ts) = strip_comb (HOLogic.dest_Trueprop (term_of concl));
                  val (freshs1, freshs2, ctxt'') = fold
                    (obtain_fresh_name (ts @ pi_bvars))
                    (map snd bvars') ([], [], ctxt');
-                 val freshs2' = Nominal.mk_not_sym freshs2;
-                 val pis' = map Nominal.perm_of_pair (pi_bvars ~~ freshs1);
+                 val freshs2' = NominalDatatype.mk_not_sym freshs2;
+                 val pis' = map NominalDatatype.perm_of_pair (pi_bvars ~~ freshs1);
                  fun concat_perm pi1 pi2 =
                    let val T = fastype_of pi1
                    in if T = fastype_of pi2 then
                        Const ("List.append", T --> T --> T) $ pi1 $ pi2
                      else pi2

                  val pis'' = fold (concat_perm #> map) pis' pis;
                  val env = Pattern.first_order_match thy (ihypt, prop_of ihyp)
                    (Vartab.empty, Vartab.empty);
                  val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy))
                    (map (Envir.subst_vars env) vs ~~
-                    map (fold_rev (Nominal.mk_perm [])
+                    map (fold_rev (NominalDatatype.mk_perm [])
                       (rev pis' @ pis)) params' @ [z])) ihyp;
                  fun mk_pi th =
                    Simplifier.simplify (HOL_basic_ss addsimps [@{thm id_apply}]
-                       addsimprocs [Nominal.perm_simproc])
+                       addsimprocs [NominalDatatype.perm_simproc])
                      (Simplifier.simplify eqvt_ss
                        (fold_rev (mk_perm_bool o cterm_of thy)
                          (rev pis' @ pis) th));
                  val (gprems1, gprems2) = split_list
                    (map (fn (th, t) =>

                          _ $ (fresh $ lhs $ rhs) =>
                            (fn t => fn u => fresh $ t $ u, lhs, rhs)
                        | _ $ (_ $ (_ $ lhs $ rhs)) =>
                            (curry (HOLogic.mk_not o HOLogic.mk_eq), lhs, rhs));
                      val th'' = Goal.prove ctxt'' [] [] (HOLogic.mk_Trueprop
-                         (bop (fold_rev (Nominal.mk_perm []) pis lhs)
-                            (fold_rev (Nominal.mk_perm []) pis rhs)))
+                         (bop (fold_rev (NominalDatatype.mk_perm []) pis lhs)
+                            (fold_rev (NominalDatatype.mk_perm []) pis rhs)))
                        (fn _ => simp_tac (HOL_basic_ss addsimps
                           (fresh_bij @ perm_bij)) 1 THEN rtac th' 1)
                    in Simplifier.simplify (eqvt_ss addsimps fresh_atm) th'' end)
                      vc_compat_ths;
-                 val vc_compat_ths'' = Nominal.mk_not_sym vc_compat_ths';
+                 val vc_compat_ths'' = NominalDatatype.mk_not_sym vc_compat_ths';
                  (** Since swap_simps simplifies (pi :: 'a prm) o (x :: 'b) to x **)
                  (** we have to pre-simplify the rewrite rules                   **)
                  val swap_simps_ss = HOL_ss addsimps swap_simps @
                     map (Simplifier.simplify (HOL_ss addsimps swap_simps))
                       (vc_compat_ths'' @ freshs2');
                  val th = Goal.prove ctxt'' [] []
                    (HOLogic.mk_Trueprop (list_comb (P $ hd ts,
-                     map (fold (Nominal.mk_perm []) pis') (tl ts))))
+                     map (fold (NominalDatatype.mk_perm []) pis') (tl ts))))
                    (fn _ => EVERY ([simp_tac eqvt_ss 1, rtac ihyp' 1,
                      REPEAT_DETERM_N (nprems_of ihyp - length gprems)
                        (simp_tac swap_simps_ss 1),
                      REPEAT_DETERM_N (length gprems)
                        (simp_tac (HOL_basic_ss
                           addsimps [inductive_forall_def']
-                          addsimprocs [Nominal.perm_simproc]) 1 THEN
+                          addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
                         resolve_tac gprems2 1)]));
                  val final = Goal.prove ctxt'' [] [] (term_of concl)
                    (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (HOL_ss
                      addsimps vc_compat_ths'' @ freshs2' @
                        perm_fresh_fresh @ fresh_atm) 1);

             | mk_prem (ps, qs, _, prems) =
                 list_all (ps, Logic.mk_implies
                   (Logic.list_implies
                     (mk_distinct qs @
                      maps (fn (t, T) => map (fn u => HOLogic.mk_Trueprop
-                      (Nominal.fresh_const T (fastype_of u) $ t $ u))
+                      (NominalDatatype.fresh_const T (fastype_of u) $ t $ u))
                         args) qs,
                      HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
                        (map HOLogic.dest_Trueprop prems))),
                    concl))
           in map mk_prem prems end) cases_prems;

                     end;
                   val (vc_compat_ths1, vc_compat_ths2) =
                     chop (length vc_compat_ths - length args * length qs)
                       (map (first_order_mrs hyps2) vc_compat_ths);
                   val vc_compat_ths' =
-                    Nominal.mk_not_sym vc_compat_ths1 @
+                    NominalDatatype.mk_not_sym vc_compat_ths1 @
                     flat (fst (fold_map inst_fresh hyps1 vc_compat_ths2));
                   val (freshs1, freshs2, ctxt3) = fold
                     (obtain_fresh_name (args @ map fst qs @ params'))
                     (map snd qs) ([], [], ctxt2);
-                  val freshs2' = Nominal.mk_not_sym freshs2;
-                  val pis = map (Nominal.perm_of_pair)
+                  val freshs2' = NominalDatatype.mk_not_sym freshs2;
+                  val pis = map (NominalDatatype.perm_of_pair)
                     ((freshs1 ~~ map fst qs) @ (params' ~~ freshs1));
                   val mk_pis = fold_rev mk_perm_bool (map (cterm_of thy) pis);
                   val obj = cterm_of thy (foldr1 HOLogic.mk_conj (map (map_aterms
                      (fn x as Free _ =>
                            if x mem args then x
                            else (case AList.lookup op = tab x of
                              SOME y => y
-                           | NONE => fold_rev (Nominal.mk_perm []) pis x)
+                           | NONE => fold_rev (NominalDatatype.mk_perm []) pis x)
                        | x => x) o HOLogic.dest_Trueprop o prop_of) case_hyps));
                   val inst = Thm.first_order_match (Thm.dest_arg
                     (Drule.strip_imp_concl (hd (cprems_of case_hyp))), obj);
                   val th = Goal.prove ctxt3 [] [] (term_of concl)
                     (fn {context = ctxt4, ...} =>
                        rtac (Thm.instantiate inst case_hyp) 1 THEN
                        SUBPROOF (fn {prems = fresh_hyps, ...} =>
                          let
-                           val fresh_hyps' = Nominal.mk_not_sym fresh_hyps;
+                           val fresh_hyps' = NominalDatatype.mk_not_sym fresh_hyps;
                            val case_ss = cases_eqvt_ss addsimps freshs2' @
                              simp_fresh_atm (vc_compat_ths' @ fresh_hyps');
                            val fresh_fresh_ss = case_ss addsimps perm_fresh_fresh;
                            val hyps1' = map
                              (mk_pis #> Simplifier.simplify fresh_fresh_ss) hyps1;

             val prems' = map (fn th => the_default th (map_thm ctxt'
               (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems;
             val prems'' = map (fn th => Simplifier.simplify eqvt_ss
               (mk_perm_bool (cterm_of thy pi) th)) prems';
             val intr' = Drule.cterm_instantiate (map (cterm_of thy) vs ~~
-               map (cterm_of thy o Nominal.mk_perm [] pi o term_of) params)
+               map (cterm_of thy o NominalDatatype.mk_perm [] pi o term_of) params)
                intr
           in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1
           end) ctxt' 1 st
       in
         case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of

             let
               val (h, ts) = strip_comb p;
               val (ts1, ts2) = chop k ts
             in
               HOLogic.mk_imp (p, list_comb (h, ts1 @
-                map (Nominal.mk_perm [] pi') ts2))
+                map (NominalDatatype.mk_perm [] pi') ts2))
             end) ps)))
           (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>
               full_simp_tac eqvt_ss 1 THEN
               eqvt_tac context pi' intr_vs) intrs')) |>
           singleton (ProofContext.export ctxt' ctxt)))