nominal.ML is nominal_datatype.ML
authorhaftmann
Fri Jul 03 23:29:03 2009 +0200 (2009-07-03)
changeset 31938f193d95b4632
parent 31937 904f93c76650
child 31939 e1ac7ab73bb1
nominal.ML is nominal_datatype.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_primrec.ML
     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
     2.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Jul 03 16:51:56 2009 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Jul 03 23:29:03 2009 +0200
     2.3 @@ -56,7 +56,7 @@
     2.4  fun add_binders thy i (t as (_ $ _)) bs = (case strip_comb t of
     2.5        (Const (s, T), ts) => (case strip_type T of
     2.6          (Ts, Type (tname, _)) =>
     2.7 -          (case Nominal.get_nominal_datatype thy tname of
     2.8 +          (case NominalDatatype.get_nominal_datatype thy tname of
     2.9               NONE => fold (add_binders thy i) ts bs
    2.10             | SOME {descr, index, ...} => (case AList.lookup op =
    2.11                   (#3 (the (AList.lookup op = descr index))) s of
    2.12 @@ -249,7 +249,7 @@
    2.13        | lift_prem t = t;
    2.14  
    2.15      fun mk_fresh (x, T) = HOLogic.mk_Trueprop
    2.16 -      (Nominal.fresh_star_const T fsT $ x $ Bound 0);
    2.17 +      (NominalDatatype.fresh_star_const T fsT $ x $ Bound 0);
    2.18  
    2.19      val (prems', prems'') = split_list (map (fn (params, sets, prems, (p, ts)) =>
    2.20        let
    2.21 @@ -270,7 +270,7 @@
    2.22      val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    2.23        (map (fn (prem, (p, ts)) => HOLogic.mk_imp (prem,
    2.24          HOLogic.list_all (ind_vars, lift_pred p
    2.25 -          (map (fold_rev (Nominal.mk_perm ind_Ts)
    2.26 +          (map (fold_rev (NominalDatatype.mk_perm ind_Ts)
    2.27              (map Bound (length atomTs downto 1))) ts)))) concls));
    2.28  
    2.29      val concl' = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    2.30 @@ -283,7 +283,7 @@
    2.31               if null (preds_of ps prem) then SOME prem
    2.32               else map_term (split_conj (K o I) names) prem prem) prems, q))))
    2.33          (maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop
    2.34 -           (Nominal.fresh_star_const U T $ u $ t)) sets)
    2.35 +           (NominalDatatype.fresh_star_const U T $ u $ t)) sets)
    2.36               (ts ~~ binder_types (fastype_of p)) @
    2.37           map (fn (u, U) => HOLogic.mk_Trueprop (Const (@{const_name finite},
    2.38             HOLogic.mk_setT U --> HOLogic.boolT) $ u)) sets) |>
    2.39 @@ -339,7 +339,7 @@
    2.40          val th2' =
    2.41            Goal.prove ctxt [] []
    2.42              (list_all (map (pair "pi") pTs, HOLogic.mk_Trueprop
    2.43 -               (f $ fold_rev (Nominal.mk_perm (rev pTs))
    2.44 +               (f $ fold_rev (NominalDatatype.mk_perm (rev pTs))
    2.45                    (pis1 @ pi :: pis2) l $ r)))
    2.46              (fn _ => cut_facts_tac [th2] 1 THEN
    2.47                 full_simp_tac (HOL_basic_ss addsimps perm_set_forget) 1) |>
    2.48 @@ -364,7 +364,7 @@
    2.49                   val params' = map term_of cparams'
    2.50                   val sets' = map (apfst (curry subst_bounds (rev params'))) sets;
    2.51                   val pi_sets = map (fn (t, _) =>
    2.52 -                   fold_rev (Nominal.mk_perm []) pis t) sets';
    2.53 +                   fold_rev (NominalDatatype.mk_perm []) pis t) sets';
    2.54                   val (P, ts) = strip_comb (HOLogic.dest_Trueprop (term_of concl));
    2.55                   val gprems1 = List.mapPartial (fn (th, t) =>
    2.56                     if null (preds_of ps t) then SOME th
    2.57 @@ -380,7 +380,7 @@
    2.58                     in
    2.59                       Goal.prove ctxt' [] []
    2.60                         (HOLogic.mk_Trueprop (list_comb (h,
    2.61 -                          map (fold_rev (Nominal.mk_perm []) pis) ts)))
    2.62 +                          map (fold_rev (NominalDatatype.mk_perm []) pis) ts)))
    2.63                         (fn _ => simp_tac (HOL_basic_ss addsimps
    2.64                            (fresh_star_bij @ finite_ineq)) 1 THEN rtac th' 1)
    2.65                     end) vc_compat_ths vc_compat_vs;
    2.66 @@ -400,11 +400,11 @@
    2.67                     end;
    2.68                   val pis'' = fold_rev (concat_perm #> map) pis' pis;
    2.69                   val ihyp' = inst_params thy vs_ihypt ihyp
    2.70 -                   (map (fold_rev (Nominal.mk_perm [])
    2.71 +                   (map (fold_rev (NominalDatatype.mk_perm [])
    2.72                        (pis' @ pis) #> cterm_of thy) params' @ [cterm_of thy z]);
    2.73                   fun mk_pi th =
    2.74                     Simplifier.simplify (HOL_basic_ss addsimps [@{thm id_apply}]
    2.75 -                       addsimprocs [Nominal.perm_simproc])
    2.76 +                       addsimprocs [NominalDatatype.perm_simproc])
    2.77                       (Simplifier.simplify eqvt_ss
    2.78                         (fold_rev (mk_perm_bool o cterm_of thy)
    2.79                           (pis' @ pis) th));
    2.80 @@ -419,13 +419,13 @@
    2.81                       (fresh_ths2 ~~ sets);
    2.82                   val th = Goal.prove ctxt'' [] []
    2.83                     (HOLogic.mk_Trueprop (list_comb (P $ hd ts,
    2.84 -                     map (fold_rev (Nominal.mk_perm []) pis') (tl ts))))
    2.85 +                     map (fold_rev (NominalDatatype.mk_perm []) pis') (tl ts))))
    2.86                     (fn _ => EVERY ([simp_tac eqvt_ss 1, rtac ihyp' 1] @
    2.87                       map (fn th => rtac th 1) fresh_ths3 @
    2.88                       [REPEAT_DETERM_N (length gprems)
    2.89                         (simp_tac (HOL_basic_ss
    2.90                            addsimps [inductive_forall_def']
    2.91 -                          addsimprocs [Nominal.perm_simproc]) 1 THEN
    2.92 +                          addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
    2.93                          resolve_tac gprems2 1)]));
    2.94                   val final = Goal.prove ctxt'' [] [] (term_of concl)
    2.95                     (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (HOL_ss
     3.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Fri Jul 03 16:51:56 2009 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Jul 03 23:29:03 2009 +0200
     3.3 @@ -223,7 +223,7 @@
     3.4  
     3.5  (* find datatypes which contain all datatypes in tnames' *)
     3.6  
     3.7 -fun find_dts (dt_info : Nominal.nominal_datatype_info Symtab.table) _ [] = []
     3.8 +fun find_dts (dt_info : NominalDatatype.nominal_datatype_info Symtab.table) _ [] = []
     3.9    | find_dts dt_info tnames' (tname::tnames) =
    3.10        (case Symtab.lookup dt_info tname of
    3.11            NONE => primrec_err (quote tname ^ " is not a nominal datatype")
    3.12 @@ -247,7 +247,7 @@
    3.13      val eqns' = map unquantify spec'
    3.14      val eqns = fold_rev (process_eqn lthy (fn v => Variable.is_fixed lthy v
    3.15        orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) spec' [];
    3.16 -    val dt_info = Nominal.get_nominal_datatypes (ProofContext.theory_of lthy);
    3.17 +    val dt_info = NominalDatatype.get_nominal_datatypes (ProofContext.theory_of lthy);
    3.18      val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
    3.19        map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns
    3.20      val _ =