--- a/src/HOL/Nominal/nominal_inductive2.ML Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Mar 04 10:45:52 2009 +0100
@@ -8,7 +8,7 @@
signature NOMINAL_INDUCTIVE2 =
sig
- val prove_strong_ind: string -> (string * string list) list -> theory -> Proof.state
+ val prove_strong_ind: string -> (string * string list) list -> local_theory -> Proof.state
end
structure NominalInductive2 : NOMINAL_INDUCTIVE2 =
@@ -28,6 +28,13 @@
fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
(Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
+val fresh_postprocess =
+ Simplifier.full_simplify (HOL_basic_ss addsimps
+ [@{thm fresh_star_set_eq}, @{thm fresh_star_Un_elim},
+ @{thm fresh_star_insert_elim}, @{thm fresh_star_empty_elim}]);
+
+fun preds_of ps t = gen_inter (op = o apfst dest_Free) (ps, Term.add_frees t []);
+
val perm_bool = mk_meta_eq (thm "perm_bool");
val perm_boolI = thm "perm_boolI";
val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
@@ -148,9 +155,9 @@
map (Envir.subst_vars env #> cterm_of thy) vs ~~ cts) th
end;
-fun prove_strong_ind s avoids thy =
+fun prove_strong_ind s avoids ctxt =
let
- val ctxt = ProofContext.init thy;
+ val thy = ProofContext.theory_of ctxt;
val ({names, ...}, {raw_induct, intrs, elims, ...}) =
InductivePackage.the_inductive ctxt (Sign.intern_const thy s);
val ind_params = InductivePackage.params_of raw_induct;
@@ -166,8 +173,7 @@
(Induct.lookup_inductP ctxt (hd names)))));
val induct_cases' = if null induct_cases then replicate (length intrs) ""
else induct_cases;
- val raw_induct' = Logic.unvarify (prop_of raw_induct);
- val elims' = map (Logic.unvarify o prop_of) elims;
+ val ([raw_induct'], ctxt') = Variable.import_terms false [prop_of raw_induct] ctxt;
val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);
val ps = map (fst o snd) concls;
@@ -191,12 +197,15 @@
handle TERM _ =>
error ("Expression " ^ quote s ^ " to be avoided in case " ^
quote name ^ " is not a set type");
- val ps = map mk sets
+ fun add_set p [] = [p]
+ | add_set (t, T) ((u, U) :: ps) =
+ if T = U then
+ let val S = HOLogic.mk_setT T
+ in (Const (@{const_name "op Un"}, S --> S --> S) $ u $ t, T) :: ps
+ end
+ else (u, U) :: add_set (t, T) ps
in
- case duplicates op = (map snd ps) of
- [] => ps
- | Ts => error ("More than one set in case " ^ quote name ^
- " for type(s) " ^ commas_quote (map (Syntax.string_of_typ ctxt') Ts))
+ fold (mk #> add_set) sets []
end;
val prems = map (fn (prem, name) =>
@@ -221,8 +230,8 @@
val ind_sort = if null atomTs then HOLogic.typeS
else Sign.certify_sort thy (map (fn a => Sign.intern_class thy
("fs_" ^ Sign.base_name a)) atoms);
- val fs_ctxt_tyname = Name.variant (map fst (OldTerm.term_tfrees raw_induct')) "'n";
- val fs_ctxt_name = Name.variant (OldTerm.add_term_names (raw_induct', [])) "z";
+ val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
+ val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
val fsT = TFree (fs_ctxt_tyname, ind_sort);
val inductive_forall_def' = Drule.instantiate'
@@ -253,7 +262,7 @@
val prem = Logic.list_implies
(map mk_fresh sets @
map (fn prem =>
- if null (OldTerm.term_frees prem inter ps) then prem
+ if null (preds_of ps prem) then prem
else lift_prem prem) prems,
HOLogic.mk_Trueprop (lift_pred p ts));
in abs_params params' prem end) prems);
@@ -276,7 +285,7 @@
val (vc_compat, vc_compat') = map (fn (params, sets, prems, (p, ts)) =>
map (fn q => abs_params params (incr_boundvars ~1 (Logic.list_implies
(List.mapPartial (fn prem =>
- if null (ps inter OldTerm.term_frees prem) then SOME prem
+ 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
(NominalPackage.fresh_star_const U T $ u $ t)) sets)
@@ -345,8 +354,8 @@
ths1 @ ths, ths2 @ [th1], ths3 @ [th2'], ctxt')
end;
- fun mk_ind_proof thy thss =
- Goal.prove_global thy [] prems' concl' (fn {prems = ihyps, context = ctxt} =>
+ fun mk_ind_proof ctxt' thss =
+ Goal.prove ctxt' [] prems' concl' (fn {prems = ihyps, context = ctxt} =>
let val th = Goal.prove ctxt [] [] concl (fn {context, ...} =>
rtac raw_induct 1 THEN
EVERY (maps (fn (((((_, sets, oprems, _),
@@ -363,7 +372,7 @@
fold_rev (NominalPackage.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 (OldTerm.term_frees t inter ps) then SOME th
+ if null (preds_of ps t) then SOME th
else
map_thm ctxt' (split_conj (K o I) names)
(etac conjunct1 1) monos NONE th)
@@ -405,7 +414,7 @@
(fold_rev (mk_perm_bool o cterm_of thy)
(pis' @ pis) th));
val gprems2 = map (fn (th, t) =>
- if null (OldTerm.term_frees t inter ps) then mk_pi th
+ if null (preds_of ps t) then mk_pi th
else
mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis''))
(inst_conj_all_tac (length pis'')) monos (SOME t) th)))
@@ -435,38 +444,42 @@
REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN
asm_full_simp_tac (simpset_of thy) 1)
- end);
+ end) |>
+ fresh_postprocess |>
+ singleton (ProofContext.export ctxt' ctxt);
in
- thy |>
- ProofContext.init |>
- Proof.theorem_i NONE (fn thss => ProofContext.theory (fn thy =>
+ ctxt'' |>
+ Proof.theorem_i NONE (fn thss => fn ctxt =>
let
- val ctxt = ProofContext.init thy;
val rec_name = space_implode "_" (map Sign.base_name names);
+ val rec_qualified = Binding.qualify false rec_name;
val ind_case_names = RuleCases.case_names induct_cases;
val induct_cases' = InductivePackage.partition_rules' raw_induct
(intrs ~~ induct_cases);
val thss' = map (map atomize_intr) thss;
val thsss = InductivePackage.partition_rules' raw_induct (intrs ~~ thss');
val strong_raw_induct =
- mk_ind_proof thy thss' |> InductivePackage.rulify;
+ mk_ind_proof ctxt thss' |> InductivePackage.rulify;
val strong_induct =
if length names > 1 then
(strong_raw_induct, [ind_case_names, RuleCases.consumes 0])
else (strong_raw_induct RSN (2, rev_mp),
[ind_case_names, RuleCases.consumes 1]);
- val ([strong_induct'], thy') = thy |>
- Sign.add_path rec_name |>
- PureThy.add_thms [((Binding.name "strong_induct", #1 strong_induct), #2 strong_induct)];
+ val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.theoremK
+ ((rec_qualified (Binding.name "strong_induct"),
+ map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
+ ctxt;
val strong_inducts =
- ProjectRule.projects ctxt (1 upto length names) strong_induct'
+ ProjectRule.projects ctxt' (1 upto length names) strong_induct'
in
- thy' |>
- PureThy.add_thmss [((Binding.name "strong_inducts", strong_inducts),
- [ind_case_names, RuleCases.consumes 1])] |> snd |>
- Sign.parent_path
- end))
+ ctxt' |>
+ LocalTheory.note Thm.theoremK
+ ((rec_qualified (Binding.name "strong_inducts"),
+ [Attrib.internal (K ind_case_names),
+ Attrib.internal (K (RuleCases.consumes 1))]),
+ strong_inducts) |> snd
+ end)
(map (map (rulify_term thy #> rpair [])) vc_compat)
end;
@@ -476,11 +489,11 @@
local structure P = OuterParse and K = OuterKeyword in
val _ =
- OuterSyntax.command "nominal_inductive2"
+ OuterSyntax.local_theory_to_proof "nominal_inductive2"
"prove strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
- (P.name -- Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name --
+ (P.xname -- Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name --
(P.$$$ ":" |-- P.and_list1 P.term))) [] >> (fn (name, avoids) =>
- Toplevel.print o Toplevel.theory_to_proof (prove_strong_ind name avoids)));
+ prove_strong_ind name avoids));
end;