# HG changeset patch # User haftmann # Date 1246656543 -7200 # Node ID f193d95b4632789ac853247ec92c826f6a362767 # Parent 904f93c76650637bbb441cb307c2d050d91c353b nominal.ML is nominal_datatype.ML diff -r 904f93c76650 -r f193d95b4632 src/HOL/Nominal/nominal_inductive.ML --- 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 diff -r 904f93c76650 -r f193d95b4632 src/HOL/Nominal/nominal_inductive2.ML --- 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 diff -r 904f93c76650 -r f193d95b4632 src/HOL/Nominal/nominal_primrec.ML --- 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 _ =