src/HOL/Nominal/nominal_inductive.ML
changeset 31938 f193d95b4632
parent 31723 f5cafe803b55
child 32035 8e77b6a250d5
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Jul 03 16:51:56 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Jul 03 23:29:03 2009 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4  fun add_binders thy i (t as (_ $ _)) bs = (case strip_comb t of
     1.5        (Const (s, T), ts) => (case strip_type T of
     1.6          (Ts, Type (tname, _)) =>
     1.7 -          (case Nominal.get_nominal_datatype thy tname of
     1.8 +          (case NominalDatatype.get_nominal_datatype thy tname of
     1.9               NONE => fold (add_binders thy i) ts bs
    1.10             | SOME {descr, index, ...} => (case AList.lookup op =
    1.11                   (#3 (the (AList.lookup op = descr index))) s of
    1.12 @@ -230,7 +230,7 @@
    1.13            else NONE) xs @ mk_distinct xs;
    1.14  
    1.15      fun mk_fresh (x, T) = HOLogic.mk_Trueprop
    1.16 -      (Nominal.fresh_const T fsT $ x $ Bound 0);
    1.17 +      (NominalDatatype.fresh_const T fsT $ x $ Bound 0);
    1.18  
    1.19      val (prems', prems'') = split_list (map (fn (params, bvars, prems, (p, ts)) =>
    1.20        let
    1.21 @@ -254,7 +254,7 @@
    1.22      val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.23        (map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem,
    1.24          HOLogic.list_all (ind_vars, lift_pred p
    1.25 -          (map (fold_rev (Nominal.mk_perm ind_Ts)
    1.26 +          (map (fold_rev (NominalDatatype.mk_perm ind_Ts)
    1.27              (map Bound (length atomTs downto 1))) ts)))) concls));
    1.28  
    1.29      val concl' = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.30 @@ -268,7 +268,7 @@
    1.31               else map_term (split_conj (K o I) names) prem prem) prems, q))))
    1.32          (mk_distinct bvars @
    1.33           maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop
    1.34 -           (Nominal.fresh_const U T $ u $ t)) bvars)
    1.35 +           (NominalDatatype.fresh_const U T $ u $ t)) bvars)
    1.36               (ts ~~ binder_types (fastype_of p)))) prems;
    1.37  
    1.38      val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
    1.39 @@ -296,7 +296,7 @@
    1.40          val p = foldr1 HOLogic.mk_prod (map protect ts @ freshs1);
    1.41          val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop
    1.42              (HOLogic.exists_const T $ Abs ("x", T,
    1.43 -              Nominal.fresh_const T (fastype_of p) $
    1.44 +              NominalDatatype.fresh_const T (fastype_of p) $
    1.45                  Bound 0 $ p)))
    1.46            (fn _ => EVERY
    1.47              [resolve_tac exists_fresh' 1,
    1.48 @@ -325,13 +325,13 @@
    1.49                     (fn (Bound i, T) => (nth params' (length params' - i), T)
    1.50                       | (t, T) => (t, T)) bvars;
    1.51                   val pi_bvars = map (fn (t, _) =>
    1.52 -                   fold_rev (Nominal.mk_perm []) pis t) bvars';
    1.53 +                   fold_rev (NominalDatatype.mk_perm []) pis t) bvars';
    1.54                   val (P, ts) = strip_comb (HOLogic.dest_Trueprop (term_of concl));
    1.55                   val (freshs1, freshs2, ctxt'') = fold
    1.56                     (obtain_fresh_name (ts @ pi_bvars))
    1.57                     (map snd bvars') ([], [], ctxt');
    1.58 -                 val freshs2' = Nominal.mk_not_sym freshs2;
    1.59 -                 val pis' = map Nominal.perm_of_pair (pi_bvars ~~ freshs1);
    1.60 +                 val freshs2' = NominalDatatype.mk_not_sym freshs2;
    1.61 +                 val pis' = map NominalDatatype.perm_of_pair (pi_bvars ~~ freshs1);
    1.62                   fun concat_perm pi1 pi2 =
    1.63                     let val T = fastype_of pi1
    1.64                     in if T = fastype_of pi2 then
    1.65 @@ -343,11 +343,11 @@
    1.66                     (Vartab.empty, Vartab.empty);
    1.67                   val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy))
    1.68                     (map (Envir.subst_vars env) vs ~~
    1.69 -                    map (fold_rev (Nominal.mk_perm [])
    1.70 +                    map (fold_rev (NominalDatatype.mk_perm [])
    1.71                        (rev pis' @ pis)) params' @ [z])) ihyp;
    1.72                   fun mk_pi th =
    1.73                     Simplifier.simplify (HOL_basic_ss addsimps [@{thm id_apply}]
    1.74 -                       addsimprocs [Nominal.perm_simproc])
    1.75 +                       addsimprocs [NominalDatatype.perm_simproc])
    1.76                       (Simplifier.simplify eqvt_ss
    1.77                         (fold_rev (mk_perm_bool o cterm_of thy)
    1.78                           (rev pis' @ pis) th));
    1.79 @@ -369,13 +369,13 @@
    1.80                         | _ $ (_ $ (_ $ lhs $ rhs)) =>
    1.81                             (curry (HOLogic.mk_not o HOLogic.mk_eq), lhs, rhs));
    1.82                       val th'' = Goal.prove ctxt'' [] [] (HOLogic.mk_Trueprop
    1.83 -                         (bop (fold_rev (Nominal.mk_perm []) pis lhs)
    1.84 -                            (fold_rev (Nominal.mk_perm []) pis rhs)))
    1.85 +                         (bop (fold_rev (NominalDatatype.mk_perm []) pis lhs)
    1.86 +                            (fold_rev (NominalDatatype.mk_perm []) pis rhs)))
    1.87                         (fn _ => simp_tac (HOL_basic_ss addsimps
    1.88                            (fresh_bij @ perm_bij)) 1 THEN rtac th' 1)
    1.89                     in Simplifier.simplify (eqvt_ss addsimps fresh_atm) th'' end)
    1.90                       vc_compat_ths;
    1.91 -                 val vc_compat_ths'' = Nominal.mk_not_sym vc_compat_ths';
    1.92 +                 val vc_compat_ths'' = NominalDatatype.mk_not_sym vc_compat_ths';
    1.93                   (** Since swap_simps simplifies (pi :: 'a prm) o (x :: 'b) to x **)
    1.94                   (** we have to pre-simplify the rewrite rules                   **)
    1.95                   val swap_simps_ss = HOL_ss addsimps swap_simps @
    1.96 @@ -383,14 +383,14 @@
    1.97                        (vc_compat_ths'' @ freshs2');
    1.98                   val th = Goal.prove ctxt'' [] []
    1.99                     (HOLogic.mk_Trueprop (list_comb (P $ hd ts,
   1.100 -                     map (fold (Nominal.mk_perm []) pis') (tl ts))))
   1.101 +                     map (fold (NominalDatatype.mk_perm []) pis') (tl ts))))
   1.102                     (fn _ => EVERY ([simp_tac eqvt_ss 1, rtac ihyp' 1,
   1.103                       REPEAT_DETERM_N (nprems_of ihyp - length gprems)
   1.104                         (simp_tac swap_simps_ss 1),
   1.105                       REPEAT_DETERM_N (length gprems)
   1.106                         (simp_tac (HOL_basic_ss
   1.107                            addsimps [inductive_forall_def']
   1.108 -                          addsimprocs [Nominal.perm_simproc]) 1 THEN
   1.109 +                          addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
   1.110                          resolve_tac gprems2 1)]));
   1.111                   val final = Goal.prove ctxt'' [] [] (term_of concl)
   1.112                     (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (HOL_ss
   1.113 @@ -448,7 +448,7 @@
   1.114                    (Logic.list_implies
   1.115                      (mk_distinct qs @
   1.116                       maps (fn (t, T) => map (fn u => HOLogic.mk_Trueprop
   1.117 -                      (Nominal.fresh_const T (fastype_of u) $ t $ u))
   1.118 +                      (NominalDatatype.fresh_const T (fastype_of u) $ t $ u))
   1.119                          args) qs,
   1.120                       HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   1.121                         (map HOLogic.dest_Trueprop prems))),
   1.122 @@ -499,13 +499,13 @@
   1.123                      chop (length vc_compat_ths - length args * length qs)
   1.124                        (map (first_order_mrs hyps2) vc_compat_ths);
   1.125                    val vc_compat_ths' =
   1.126 -                    Nominal.mk_not_sym vc_compat_ths1 @
   1.127 +                    NominalDatatype.mk_not_sym vc_compat_ths1 @
   1.128                      flat (fst (fold_map inst_fresh hyps1 vc_compat_ths2));
   1.129                    val (freshs1, freshs2, ctxt3) = fold
   1.130                      (obtain_fresh_name (args @ map fst qs @ params'))
   1.131                      (map snd qs) ([], [], ctxt2);
   1.132 -                  val freshs2' = Nominal.mk_not_sym freshs2;
   1.133 -                  val pis = map (Nominal.perm_of_pair)
   1.134 +                  val freshs2' = NominalDatatype.mk_not_sym freshs2;
   1.135 +                  val pis = map (NominalDatatype.perm_of_pair)
   1.136                      ((freshs1 ~~ map fst qs) @ (params' ~~ freshs1));
   1.137                    val mk_pis = fold_rev mk_perm_bool (map (cterm_of thy) pis);
   1.138                    val obj = cterm_of thy (foldr1 HOLogic.mk_conj (map (map_aterms
   1.139 @@ -513,7 +513,7 @@
   1.140                             if x mem args then x
   1.141                             else (case AList.lookup op = tab x of
   1.142                               SOME y => y
   1.143 -                           | NONE => fold_rev (Nominal.mk_perm []) pis x)
   1.144 +                           | NONE => fold_rev (NominalDatatype.mk_perm []) pis x)
   1.145                         | x => x) o HOLogic.dest_Trueprop o prop_of) case_hyps));
   1.146                    val inst = Thm.first_order_match (Thm.dest_arg
   1.147                      (Drule.strip_imp_concl (hd (cprems_of case_hyp))), obj);
   1.148 @@ -522,7 +522,7 @@
   1.149                         rtac (Thm.instantiate inst case_hyp) 1 THEN
   1.150                         SUBPROOF (fn {prems = fresh_hyps, ...} =>
   1.151                           let
   1.152 -                           val fresh_hyps' = Nominal.mk_not_sym fresh_hyps;
   1.153 +                           val fresh_hyps' = NominalDatatype.mk_not_sym fresh_hyps;
   1.154                             val case_ss = cases_eqvt_ss addsimps freshs2' @
   1.155                               simp_fresh_atm (vc_compat_ths' @ fresh_hyps');
   1.156                             val fresh_fresh_ss = case_ss addsimps perm_fresh_fresh;
   1.157 @@ -635,7 +635,7 @@
   1.158              val prems'' = map (fn th => Simplifier.simplify eqvt_ss
   1.159                (mk_perm_bool (cterm_of thy pi) th)) prems';
   1.160              val intr' = Drule.cterm_instantiate (map (cterm_of thy) vs ~~
   1.161 -               map (cterm_of thy o Nominal.mk_perm [] pi o term_of) params)
   1.162 +               map (cterm_of thy o NominalDatatype.mk_perm [] pi o term_of) params)
   1.163                 intr
   1.164            in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1
   1.165            end) ctxt' 1 st
   1.166 @@ -655,7 +655,7 @@
   1.167                val (ts1, ts2) = chop k ts
   1.168              in
   1.169                HOLogic.mk_imp (p, list_comb (h, ts1 @
   1.170 -                map (Nominal.mk_perm [] pi') ts2))
   1.171 +                map (NominalDatatype.mk_perm [] pi') ts2))
   1.172              end) ps)))
   1.173            (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>
   1.174                full_simp_tac eqvt_ss 1 THEN