--- a/src/HOL/Nominal/nominal_inductive.ML Fri Jul 03 16:51:56 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Fri Jul 03 23:29:03 2009 +0200
@@ -53,7 +53,7 @@
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
@@ -230,7 +230,7 @@
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
@@ -254,7 +254,7 @@
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
@@ -268,7 +268,7 @@
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";
@@ -296,7 +296,7 @@
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,
@@ -325,13 +325,13 @@
(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
@@ -343,11 +343,11 @@
(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));
@@ -369,13 +369,13 @@
| _ $ (_ $ (_ $ 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 @
@@ -383,14 +383,14 @@
(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
@@ -448,7 +448,7 @@
(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))),
@@ -499,13 +499,13 @@
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
@@ -513,7 +513,7 @@
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);
@@ -522,7 +522,7 @@
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;
@@ -635,7 +635,7 @@
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
@@ -655,7 +655,7 @@
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
--- a/src/HOL/Nominal/nominal_inductive2.ML Fri Jul 03 16:51:56 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Jul 03 23:29:03 2009 +0200
@@ -56,7 +56,7 @@
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
@@ -249,7 +249,7 @@
| lift_prem t = t;
fun mk_fresh (x, T) = HOLogic.mk_Trueprop
- (Nominal.fresh_star_const T fsT $ x $ Bound 0);
+ (NominalDatatype.fresh_star_const T fsT $ x $ Bound 0);
val (prems', prems'') = split_list (map (fn (params, sets, prems, (p, ts)) =>
let
@@ -270,7 +270,7 @@
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
@@ -283,7 +283,7 @@
if null (preds_of ps prem) then SOME prem
else map_term (split_conj (K o I) names) prem prem) prems, q))))
(maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop
- (Nominal.fresh_star_const U T $ u $ t)) sets)
+ (NominalDatatype.fresh_star_const U T $ u $ t)) sets)
(ts ~~ binder_types (fastype_of p)) @
map (fn (u, U) => HOLogic.mk_Trueprop (Const (@{const_name finite},
HOLogic.mk_setT U --> HOLogic.boolT) $ u)) sets) |>
@@ -339,7 +339,7 @@
val th2' =
Goal.prove ctxt [] []
(list_all (map (pair "pi") pTs, HOLogic.mk_Trueprop
- (f $ fold_rev (Nominal.mk_perm (rev pTs))
+ (f $ fold_rev (NominalDatatype.mk_perm (rev pTs))
(pis1 @ pi :: pis2) l $ r)))
(fn _ => cut_facts_tac [th2] 1 THEN
full_simp_tac (HOL_basic_ss addsimps perm_set_forget) 1) |>
@@ -364,7 +364,7 @@
val params' = map term_of cparams'
val sets' = map (apfst (curry subst_bounds (rev params'))) sets;
val pi_sets = map (fn (t, _) =>
- fold_rev (Nominal.mk_perm []) pis t) sets';
+ fold_rev (NominalDatatype.mk_perm []) pis t) sets';
val (P, ts) = strip_comb (HOLogic.dest_Trueprop (term_of concl));
val gprems1 = List.mapPartial (fn (th, t) =>
if null (preds_of ps t) then SOME th
@@ -380,7 +380,7 @@
in
Goal.prove ctxt' [] []
(HOLogic.mk_Trueprop (list_comb (h,
- map (fold_rev (Nominal.mk_perm []) pis) ts)))
+ map (fold_rev (NominalDatatype.mk_perm []) pis) ts)))
(fn _ => simp_tac (HOL_basic_ss addsimps
(fresh_star_bij @ finite_ineq)) 1 THEN rtac th' 1)
end) vc_compat_ths vc_compat_vs;
@@ -400,11 +400,11 @@
end;
val pis'' = fold_rev (concat_perm #> map) pis' pis;
val ihyp' = inst_params thy vs_ihypt ihyp
- (map (fold_rev (Nominal.mk_perm [])
+ (map (fold_rev (NominalDatatype.mk_perm [])
(pis' @ pis) #> cterm_of thy) params' @ [cterm_of thy z]);
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)
(pis' @ pis) th));
@@ -419,13 +419,13 @@
(fresh_ths2 ~~ sets);
val th = Goal.prove ctxt'' [] []
(HOLogic.mk_Trueprop (list_comb (P $ hd ts,
- map (fold_rev (Nominal.mk_perm []) pis') (tl ts))))
+ map (fold_rev (NominalDatatype.mk_perm []) pis') (tl ts))))
(fn _ => EVERY ([simp_tac eqvt_ss 1, rtac ihyp' 1] @
map (fn th => rtac th 1) fresh_ths3 @
[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
--- a/src/HOL/Nominal/nominal_primrec.ML Fri Jul 03 16:51:56 2009 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Fri Jul 03 23:29:03 2009 +0200
@@ -223,7 +223,7 @@
(* find datatypes which contain all datatypes in tnames' *)
-fun find_dts (dt_info : Nominal.nominal_datatype_info Symtab.table) _ [] = []
+fun find_dts (dt_info : NominalDatatype.nominal_datatype_info Symtab.table) _ [] = []
| find_dts dt_info tnames' (tname::tnames) =
(case Symtab.lookup dt_info tname of
NONE => primrec_err (quote tname ^ " is not a nominal datatype")
@@ -247,7 +247,7 @@
val eqns' = map unquantify spec'
val eqns = fold_rev (process_eqn lthy (fn v => Variable.is_fixed lthy v
orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) spec' [];
- val dt_info = Nominal.get_nominal_datatypes (ProofContext.theory_of lthy);
+ val dt_info = NominalDatatype.get_nominal_datatypes (ProofContext.theory_of lthy);
val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns
val _ =