src/HOL/Nominal/nominal_inductive.ML
changeset 31723 f5cafe803b55
parent 31177 c39994cb152a
child 31938 f193d95b4632
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Jun 18 18:31:14 2009 -0700
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Jun 19 17:23:21 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 NominalPackage.get_nominal_datatype thy tname of
     1.8 +          (case Nominal.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 @@ -148,11 +148,11 @@
    1.13    let
    1.14      val thy = ProofContext.theory_of ctxt;
    1.15      val ({names, ...}, {raw_induct, intrs, elims, ...}) =
    1.16 -      InductivePackage.the_inductive ctxt (Sign.intern_const thy s);
    1.17 -    val ind_params = InductivePackage.params_of raw_induct;
    1.18 +      Inductive.the_inductive ctxt (Sign.intern_const thy s);
    1.19 +    val ind_params = Inductive.params_of raw_induct;
    1.20      val raw_induct = atomize_induct ctxt raw_induct;
    1.21      val elims = map (atomize_induct ctxt) elims;
    1.22 -    val monos = InductivePackage.get_monos ctxt;
    1.23 +    val monos = Inductive.get_monos ctxt;
    1.24      val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
    1.25      val _ = (case names \\ fold (Term.add_const_names o Thm.prop_of) eqvt_thms [] of
    1.26          [] => ()
    1.27 @@ -230,7 +230,7 @@
    1.28            else NONE) xs @ mk_distinct xs;
    1.29  
    1.30      fun mk_fresh (x, T) = HOLogic.mk_Trueprop
    1.31 -      (NominalPackage.fresh_const T fsT $ x $ Bound 0);
    1.32 +      (Nominal.fresh_const T fsT $ x $ Bound 0);
    1.33  
    1.34      val (prems', prems'') = split_list (map (fn (params, bvars, prems, (p, ts)) =>
    1.35        let
    1.36 @@ -254,7 +254,7 @@
    1.37      val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.38        (map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem,
    1.39          HOLogic.list_all (ind_vars, lift_pred p
    1.40 -          (map (fold_rev (NominalPackage.mk_perm ind_Ts)
    1.41 +          (map (fold_rev (Nominal.mk_perm ind_Ts)
    1.42              (map Bound (length atomTs downto 1))) ts)))) concls));
    1.43  
    1.44      val concl' = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.45 @@ -268,7 +268,7 @@
    1.46               else map_term (split_conj (K o I) names) prem prem) prems, q))))
    1.47          (mk_distinct bvars @
    1.48           maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop
    1.49 -           (NominalPackage.fresh_const U T $ u $ t)) bvars)
    1.50 +           (Nominal.fresh_const U T $ u $ t)) bvars)
    1.51               (ts ~~ binder_types (fastype_of p)))) prems;
    1.52  
    1.53      val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
    1.54 @@ -296,7 +296,7 @@
    1.55          val p = foldr1 HOLogic.mk_prod (map protect ts @ freshs1);
    1.56          val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop
    1.57              (HOLogic.exists_const T $ Abs ("x", T,
    1.58 -              NominalPackage.fresh_const T (fastype_of p) $
    1.59 +              Nominal.fresh_const T (fastype_of p) $
    1.60                  Bound 0 $ p)))
    1.61            (fn _ => EVERY
    1.62              [resolve_tac exists_fresh' 1,
    1.63 @@ -325,13 +325,13 @@
    1.64                     (fn (Bound i, T) => (nth params' (length params' - i), T)
    1.65                       | (t, T) => (t, T)) bvars;
    1.66                   val pi_bvars = map (fn (t, _) =>
    1.67 -                   fold_rev (NominalPackage.mk_perm []) pis t) bvars';
    1.68 +                   fold_rev (Nominal.mk_perm []) pis t) bvars';
    1.69                   val (P, ts) = strip_comb (HOLogic.dest_Trueprop (term_of concl));
    1.70                   val (freshs1, freshs2, ctxt'') = fold
    1.71                     (obtain_fresh_name (ts @ pi_bvars))
    1.72                     (map snd bvars') ([], [], ctxt');
    1.73 -                 val freshs2' = NominalPackage.mk_not_sym freshs2;
    1.74 -                 val pis' = map NominalPackage.perm_of_pair (pi_bvars ~~ freshs1);
    1.75 +                 val freshs2' = Nominal.mk_not_sym freshs2;
    1.76 +                 val pis' = map Nominal.perm_of_pair (pi_bvars ~~ freshs1);
    1.77                   fun concat_perm pi1 pi2 =
    1.78                     let val T = fastype_of pi1
    1.79                     in if T = fastype_of pi2 then
    1.80 @@ -343,11 +343,11 @@
    1.81                     (Vartab.empty, Vartab.empty);
    1.82                   val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy))
    1.83                     (map (Envir.subst_vars env) vs ~~
    1.84 -                    map (fold_rev (NominalPackage.mk_perm [])
    1.85 +                    map (fold_rev (Nominal.mk_perm [])
    1.86                        (rev pis' @ pis)) params' @ [z])) ihyp;
    1.87                   fun mk_pi th =
    1.88                     Simplifier.simplify (HOL_basic_ss addsimps [@{thm id_apply}]
    1.89 -                       addsimprocs [NominalPackage.perm_simproc])
    1.90 +                       addsimprocs [Nominal.perm_simproc])
    1.91                       (Simplifier.simplify eqvt_ss
    1.92                         (fold_rev (mk_perm_bool o cterm_of thy)
    1.93                           (rev pis' @ pis) th));
    1.94 @@ -369,13 +369,13 @@
    1.95                         | _ $ (_ $ (_ $ lhs $ rhs)) =>
    1.96                             (curry (HOLogic.mk_not o HOLogic.mk_eq), lhs, rhs));
    1.97                       val th'' = Goal.prove ctxt'' [] [] (HOLogic.mk_Trueprop
    1.98 -                         (bop (fold_rev (NominalPackage.mk_perm []) pis lhs)
    1.99 -                            (fold_rev (NominalPackage.mk_perm []) pis rhs)))
   1.100 +                         (bop (fold_rev (Nominal.mk_perm []) pis lhs)
   1.101 +                            (fold_rev (Nominal.mk_perm []) pis rhs)))
   1.102                         (fn _ => simp_tac (HOL_basic_ss addsimps
   1.103                            (fresh_bij @ perm_bij)) 1 THEN rtac th' 1)
   1.104                     in Simplifier.simplify (eqvt_ss addsimps fresh_atm) th'' end)
   1.105                       vc_compat_ths;
   1.106 -                 val vc_compat_ths'' = NominalPackage.mk_not_sym vc_compat_ths';
   1.107 +                 val vc_compat_ths'' = Nominal.mk_not_sym vc_compat_ths';
   1.108                   (** Since swap_simps simplifies (pi :: 'a prm) o (x :: 'b) to x **)
   1.109                   (** we have to pre-simplify the rewrite rules                   **)
   1.110                   val swap_simps_ss = HOL_ss addsimps swap_simps @
   1.111 @@ -383,14 +383,14 @@
   1.112                        (vc_compat_ths'' @ freshs2');
   1.113                   val th = Goal.prove ctxt'' [] []
   1.114                     (HOLogic.mk_Trueprop (list_comb (P $ hd ts,
   1.115 -                     map (fold (NominalPackage.mk_perm []) pis') (tl ts))))
   1.116 +                     map (fold (Nominal.mk_perm []) pis') (tl ts))))
   1.117                     (fn _ => EVERY ([simp_tac eqvt_ss 1, rtac ihyp' 1,
   1.118                       REPEAT_DETERM_N (nprems_of ihyp - length gprems)
   1.119                         (simp_tac swap_simps_ss 1),
   1.120                       REPEAT_DETERM_N (length gprems)
   1.121                         (simp_tac (HOL_basic_ss
   1.122                            addsimps [inductive_forall_def']
   1.123 -                          addsimprocs [NominalPackage.perm_simproc]) 1 THEN
   1.124 +                          addsimprocs [Nominal.perm_simproc]) 1 THEN
   1.125                          resolve_tac gprems2 1)]));
   1.126                   val final = Goal.prove ctxt'' [] [] (term_of concl)
   1.127                     (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (HOL_ss
   1.128 @@ -435,7 +435,7 @@
   1.129               ((ps, qs, is, map (curry subst_bounds (rev ts)) prems), ctxt')
   1.130             end) (prems ~~ avoids) ctxt')
   1.131        end)
   1.132 -        (InductivePackage.partition_rules' raw_induct (intrs ~~ avoids') ~~
   1.133 +        (Inductive.partition_rules' raw_induct (intrs ~~ avoids') ~~
   1.134           elims);
   1.135  
   1.136      val cases_prems' =
   1.137 @@ -448,7 +448,7 @@
   1.138                    (Logic.list_implies
   1.139                      (mk_distinct qs @
   1.140                       maps (fn (t, T) => map (fn u => HOLogic.mk_Trueprop
   1.141 -                      (NominalPackage.fresh_const T (fastype_of u) $ t $ u))
   1.142 +                      (Nominal.fresh_const T (fastype_of u) $ t $ u))
   1.143                          args) qs,
   1.144                       HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   1.145                         (map HOLogic.dest_Trueprop prems))),
   1.146 @@ -499,13 +499,13 @@
   1.147                      chop (length vc_compat_ths - length args * length qs)
   1.148                        (map (first_order_mrs hyps2) vc_compat_ths);
   1.149                    val vc_compat_ths' =
   1.150 -                    NominalPackage.mk_not_sym vc_compat_ths1 @
   1.151 +                    Nominal.mk_not_sym vc_compat_ths1 @
   1.152                      flat (fst (fold_map inst_fresh hyps1 vc_compat_ths2));
   1.153                    val (freshs1, freshs2, ctxt3) = fold
   1.154                      (obtain_fresh_name (args @ map fst qs @ params'))
   1.155                      (map snd qs) ([], [], ctxt2);
   1.156 -                  val freshs2' = NominalPackage.mk_not_sym freshs2;
   1.157 -                  val pis = map (NominalPackage.perm_of_pair)
   1.158 +                  val freshs2' = Nominal.mk_not_sym freshs2;
   1.159 +                  val pis = map (Nominal.perm_of_pair)
   1.160                      ((freshs1 ~~ map fst qs) @ (params' ~~ freshs1));
   1.161                    val mk_pis = fold_rev mk_perm_bool (map (cterm_of thy) pis);
   1.162                    val obj = cterm_of thy (foldr1 HOLogic.mk_conj (map (map_aterms
   1.163 @@ -513,7 +513,7 @@
   1.164                             if x mem args then x
   1.165                             else (case AList.lookup op = tab x of
   1.166                               SOME y => y
   1.167 -                           | NONE => fold_rev (NominalPackage.mk_perm []) pis x)
   1.168 +                           | NONE => fold_rev (Nominal.mk_perm []) pis x)
   1.169                         | x => x) o HOLogic.dest_Trueprop o prop_of) case_hyps));
   1.170                    val inst = Thm.first_order_match (Thm.dest_arg
   1.171                      (Drule.strip_imp_concl (hd (cprems_of case_hyp))), obj);
   1.172 @@ -522,7 +522,7 @@
   1.173                         rtac (Thm.instantiate inst case_hyp) 1 THEN
   1.174                         SUBPROOF (fn {prems = fresh_hyps, ...} =>
   1.175                           let
   1.176 -                           val fresh_hyps' = NominalPackage.mk_not_sym fresh_hyps;
   1.177 +                           val fresh_hyps' = Nominal.mk_not_sym fresh_hyps;
   1.178                             val case_ss = cases_eqvt_ss addsimps freshs2' @
   1.179                               simp_fresh_atm (vc_compat_ths' @ fresh_hyps');
   1.180                             val fresh_fresh_ss = case_ss addsimps perm_fresh_fresh;
   1.181 @@ -548,13 +548,13 @@
   1.182          val rec_name = space_implode "_" (map Long_Name.base_name names);
   1.183          val rec_qualified = Binding.qualify false rec_name;
   1.184          val ind_case_names = RuleCases.case_names induct_cases;
   1.185 -        val induct_cases' = InductivePackage.partition_rules' raw_induct
   1.186 +        val induct_cases' = Inductive.partition_rules' raw_induct
   1.187            (intrs ~~ induct_cases); 
   1.188          val thss' = map (map atomize_intr) thss;
   1.189 -        val thsss = InductivePackage.partition_rules' raw_induct (intrs ~~ thss');
   1.190 +        val thsss = Inductive.partition_rules' raw_induct (intrs ~~ thss');
   1.191          val strong_raw_induct =
   1.192 -          mk_ind_proof ctxt thss' |> InductivePackage.rulify;
   1.193 -        val strong_cases = map (mk_cases_proof ##> InductivePackage.rulify)
   1.194 +          mk_ind_proof ctxt thss' |> Inductive.rulify;
   1.195 +        val strong_cases = map (mk_cases_proof ##> Inductive.rulify)
   1.196            (thsss ~~ elims ~~ cases_prems ~~ cases_prems');
   1.197          val strong_induct =
   1.198            if length names > 1 then
   1.199 @@ -587,17 +587,17 @@
   1.200    let
   1.201      val thy = ProofContext.theory_of ctxt;
   1.202      val ({names, ...}, {raw_induct, intrs, elims, ...}) =
   1.203 -      InductivePackage.the_inductive ctxt (Sign.intern_const thy s);
   1.204 +      Inductive.the_inductive ctxt (Sign.intern_const thy s);
   1.205      val raw_induct = atomize_induct ctxt raw_induct;
   1.206      val elims = map (atomize_induct ctxt) elims;
   1.207      val intrs = map atomize_intr intrs;
   1.208 -    val monos = InductivePackage.get_monos ctxt;
   1.209 -    val intrs' = InductivePackage.unpartition_rules intrs
   1.210 +    val monos = Inductive.get_monos ctxt;
   1.211 +    val intrs' = Inductive.unpartition_rules intrs
   1.212        (map (fn (((s, ths), (_, k)), th) =>
   1.213 -           (s, ths ~~ InductivePackage.infer_intro_vars th k ths))
   1.214 -         (InductivePackage.partition_rules raw_induct intrs ~~
   1.215 -          InductivePackage.arities_of raw_induct ~~ elims));
   1.216 -    val k = length (InductivePackage.params_of raw_induct);
   1.217 +           (s, ths ~~ Inductive.infer_intro_vars th k ths))
   1.218 +         (Inductive.partition_rules raw_induct intrs ~~
   1.219 +          Inductive.arities_of raw_induct ~~ elims));
   1.220 +    val k = length (Inductive.params_of raw_induct);
   1.221      val atoms' = NominalAtoms.atoms_of thy;
   1.222      val atoms =
   1.223        if null xatoms then atoms' else
   1.224 @@ -635,7 +635,7 @@
   1.225              val prems'' = map (fn th => Simplifier.simplify eqvt_ss
   1.226                (mk_perm_bool (cterm_of thy pi) th)) prems';
   1.227              val intr' = Drule.cterm_instantiate (map (cterm_of thy) vs ~~
   1.228 -               map (cterm_of thy o NominalPackage.mk_perm [] pi o term_of) params)
   1.229 +               map (cterm_of thy o Nominal.mk_perm [] pi o term_of) params)
   1.230                 intr
   1.231            in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1
   1.232            end) ctxt' 1 st
   1.233 @@ -655,7 +655,7 @@
   1.234                val (ts1, ts2) = chop k ts
   1.235              in
   1.236                HOLogic.mk_imp (p, list_comb (h, ts1 @
   1.237 -                map (NominalPackage.mk_perm [] pi') ts2))
   1.238 +                map (Nominal.mk_perm [] pi') ts2))
   1.239              end) ps)))
   1.240            (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>
   1.241                full_simp_tac eqvt_ss 1 THEN