# HG changeset patch # User berghofe # Date 1235558945 -3600 # Node ID 7b25295489b65fb356db30d63ba0964cb9b2cf67 # Parent 3d6aab74a1841aecb4a9aa417e41e8224a5fbbcd# Parent f631fb528277cfc6d742812de22652e47471daec merged diff -r 3d6aab74a184 -r 7b25295489b6 src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Wed Feb 25 10:24:58 2009 +0100 +++ b/src/HOL/Nominal/Nominal.thy Wed Feb 25 11:49:05 2009 +0100 @@ -1645,6 +1645,31 @@ apply(rule at) done +lemma pt_fresh_star_eqvt: + fixes pi :: "'x prm" + and x :: "'a" + and a :: "'x set" + and b :: "'x list" + assumes pt: "pt TYPE('a) TYPE('x)" + and at: "at TYPE('x)" + shows "pi\(a\*x) = (pi\a)\*(pi\x)" + and "pi\(b\*x) = (pi\b)\*(pi\x)" + by (simp_all add: perm_bool pt_fresh_star_bij[OF pt, OF at]) + +lemma pt_fresh_star_eqvt_ineq: + fixes pi::"'x prm" + and a::"'y set" + and b::"'y list" + and x::"'a" + assumes pta: "pt TYPE('a) TYPE('x)" + and ptb: "pt TYPE('y) TYPE('x)" + and at: "at TYPE('x)" + and cp: "cp TYPE('a) TYPE('x) TYPE('y)" + and dj: "disjoint TYPE('y) TYPE('x)" + shows "pi\(a\*x) = (pi\a)\*(pi\x)" + and "pi\(b\*x) = (pi\b)\*(pi\x)" + by (simp_all add: pt_fresh_star_bij_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool) + lemma pt_fresh_bij1: fixes pi :: "'x prm" and x :: "'a" diff -r 3d6aab74a184 -r 7b25295489b6 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Wed Feb 25 10:24:58 2009 +0100 +++ b/src/HOL/Nominal/nominal_atoms.ML Wed Feb 25 11:49:05 2009 +0100 @@ -1,5 +1,4 @@ (* title: HOL/Nominal/nominal_atoms.ML - ID: $Id$ Author: Christian Urban and Stefan Berghofer, TU Muenchen Declaration of atom types to be used in nominal datatypes. @@ -784,6 +783,8 @@ val fresh_star_bij = @{thms "Nominal.pt_fresh_star_bij"}; val fresh_eqvt = @{thm "Nominal.pt_fresh_eqvt"}; val fresh_eqvt_ineq = @{thm "Nominal.pt_fresh_eqvt_ineq"}; + val fresh_star_eqvt = @{thms "Nominal.pt_fresh_star_eqvt"}; + val fresh_star_eqvt_ineq= @{thms "Nominal.pt_fresh_star_eqvt_ineq"}; val set_diff_eqvt = @{thm "Nominal.pt_set_diff_eqvt"}; val in_eqvt = @{thm "Nominal.pt_in_eqvt"}; val eq_eqvt = @{thm "Nominal.pt_eq_eqvt"}; @@ -947,13 +948,17 @@ in [(("fresh_bij", thms1 @ thms2),[])] end ||>> add_thmss_string let val thms1 = inst_pt_at fresh_star_bij - and thms2 = flat (map (fn ti => inst_pt_pt_at_cp [ti]) fresh_star_bij_ineq); + and thms2 = maps (fn ti => inst_pt_pt_at_cp [ti]) fresh_star_bij_ineq in [(("fresh_star_bij", thms1 @ thms2),[])] end ||>> add_thmss_string let val thms1 = inst_pt_at [fresh_eqvt] and thms2 = inst_pt_pt_at_cp_dj [fresh_eqvt_ineq] in [(("fresh_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end ||>> add_thmss_string + let val thms1 = inst_pt_at fresh_star_eqvt + and thms2 = maps (fn ti => inst_pt_pt_at_cp_dj [ti]) fresh_star_eqvt_ineq + in [(("fresh_star_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end + ||>> add_thmss_string let val thms1 = inst_pt_at [in_eqvt] in [(("in_eqvt", thms1),[NominalThmDecls.eqvt_add])] end ||>> add_thmss_string diff -r 3d6aab74a184 -r 7b25295489b6 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Wed Feb 25 10:24:58 2009 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Wed Feb 25 11:49:05 2009 +0100 @@ -7,8 +7,8 @@ signature NOMINAL_INDUCTIVE = sig - val prove_strong_ind: string -> (string * string list) list -> theory -> Proof.state - val prove_eqvt: string -> string list -> theory -> theory + val prove_strong_ind: string -> (string * string list) list -> local_theory -> Proof.state + val prove_eqvt: string -> string list -> local_theory -> local_theory end structure NominalInductive : NOMINAL_INDUCTIVE = @@ -28,6 +28,8 @@ fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); +fun preds_of ps t = gen_inter (op = o apfst dest_Free) (ps, Term.add_frees t []); + val fresh_prod = thm "fresh_prod"; val perm_bool = mk_meta_eq (thm "perm_bool"); @@ -142,9 +144,9 @@ fun first_order_mrs ths th = ths MRS Thm.instantiate (first_order_matchs (cprems_of th) (map cprop_of ths)) th; -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; @@ -158,8 +160,7 @@ commas_quote xs)); val induct_cases = map fst (fst (RuleCases.get (the (Induct.lookup_inductP ctxt (hd names))))); - 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; @@ -199,8 +200,8 @@ val ind_sort = if null atomTs then HOLogic.typeS else Sign.certify_sort thy (map (fn T => Sign.intern_class thy ("fs_" ^ Sign.base_name (fst (dest_Type T)))) atomTs); - 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' @@ -237,7 +238,7 @@ val prem = Logic.list_implies (map mk_fresh bvars @ mk_distinct bvars @ 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)); val vs = map (Var o apfst (rpair 0)) (Term.rename_wrt_term prem params') @@ -263,7 +264,7 @@ val vc_compat = map (fn (params, bvars, prems, (p, ts)) => map (fn q => list_all (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)))) (mk_distinct bvars @ maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop @@ -309,8 +310,8 @@ [ex] ctxt in (freshs1 @ [term_of cx], freshs2 @ ths, 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 ((((_, bvars, oprems, _), vc_compat_ths), ihyp), (vs, ihypt)) => @@ -352,7 +353,7 @@ (rev pis' @ pis) th)); val (gprems1, gprems2) = split_list (map (fn (th, t) => - if null (OldTerm.term_frees t inter ps) then (SOME th, mk_pi th) + if null (preds_of ps t) then (SOME th, mk_pi th) else (map_thm ctxt (split_conj (K o I) names) (etac conjunct1 1) monos NONE th, @@ -403,42 +404,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) |> singleton (ProofContext.export ctxt' ctxt); (** strong case analysis rule **) val cases_prems = map (fn ((name, avoids), rule) => let - val prem :: prems = Logic.strip_imp_prems rule; - val concl = Logic.strip_imp_concl rule; - val used = Term.add_free_names rule []; + val ([rule'], ctxt') = Variable.import_terms false [prop_of rule] ctxt; + val prem :: prems = Logic.strip_imp_prems rule'; + val concl = Logic.strip_imp_concl rule' in (prem, List.drop (snd (strip_comb (HOLogic.dest_Trueprop prem)), length ind_params), concl, - fst (fold_map (fn (prem, (_, avoid)) => fn used => + fold_map (fn (prem, (_, avoid)) => fn ctxt => let val prems = Logic.strip_assums_hyp prem; val params = Logic.strip_params prem; val bnds = fold (add_binders thy 0) prems [] @ mk_avoids params avoid; - fun mk_subst (p as (s, T)) (i, j, used, ps, qs, is, ts) = + fun mk_subst (p as (s, T)) (i, j, ctxt, ps, qs, is, ts) = if member (op = o apsnd fst) bnds (Bound i) then let - val s' = Name.variant used s; + val ([s'], ctxt') = Variable.variant_fixes [s] ctxt; val t = Free (s', T) - in (i + 1, j, s' :: used, ps, (t, T) :: qs, i :: is, t :: ts) end - else (i + 1, j + 1, used, p :: ps, qs, is, Bound j :: ts); - val (_, _, used', ps, qs, is, ts) = fold_rev mk_subst params - (0, 0, used, [], [], [], []) + in (i + 1, j, ctxt', ps, (t, T) :: qs, i :: is, t :: ts) end + else (i + 1, j + 1, ctxt, p :: ps, qs, is, Bound j :: ts); + val (_, _, ctxt', ps, qs, is, ts) = fold_rev mk_subst params + (0, 0, ctxt, [], [], [], []) in - ((ps, qs, is, map (curry subst_bounds (rev ts)) prems), used') - end) (prems ~~ avoids) used)) + ((ps, qs, is, map (curry subst_bounds (rev ts)) prems), ctxt') + end) (prems ~~ avoids) ctxt') end) (InductivePackage.partition_rules' raw_induct (intrs ~~ avoids') ~~ - elims'); + elims); val cases_prems' = - map (fn (prem, args, concl, prems) => + map (fn (prem, args, concl, (prems, _)) => let fun mk_prem (ps, [], _, prems) = list_all (ps, Logic.list_implies (prems, concl)) @@ -462,9 +463,9 @@ val simp_fresh_atm = map (Simplifier.simplify (HOL_basic_ss addsimps fresh_atm)); - fun mk_cases_proof thy ((((name, thss), elim), (prem, args, concl, prems)), + fun mk_cases_proof ((((name, thss), elim), (prem, args, concl, (prems, ctxt'))), prems') = - (name, Goal.prove_global thy [] (prem :: prems') concl + (name, Goal.prove ctxt' [] (prem :: prems') concl (fn {prems = hyp :: hyps, context = ctxt1} => EVERY (rtac (hyp RS elim) 1 :: map (fn (((_, vc_compat_ths), case_hyp), (_, qs, is, _)) => @@ -537,52 +538,54 @@ end) ctxt4 1) val final = ProofContext.export ctxt3 ctxt2 [th] in resolve_tac final 1 end) ctxt1 1) - (thss ~~ hyps ~~ prems)))) + (thss ~~ hyps ~~ prems))) |> + 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 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; - val strong_cases = map (mk_cases_proof thy ##> InductivePackage.rulify) + mk_ind_proof ctxt thss' |> InductivePackage.rulify; + val strong_cases = map (mk_cases_proof ##> InductivePackage.rulify) (thsss ~~ elims ~~ cases_prems ~~ cases_prems'); 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' in - thy' |> - PureThy.add_thmss [((Binding.name "strong_inducts", strong_inducts), - [ind_case_names, RuleCases.consumes 1])] |> snd |> - Sign.parent_path |> - fold (fn ((name, elim), (_, cases)) => - Sign.add_path (Sign.base_name name) #> - PureThy.add_thms [((Binding.name "strong_cases", elim), - [RuleCases.case_names (map snd cases), - RuleCases.consumes 1])] #> snd #> - Sign.parent_path) (strong_cases ~~ induct_cases') - 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 |> + LocalTheory.notes Thm.theoremK (map (fn ((name, elim), (_, cases)) => + ((Binding.name (NameSpace.qualified (Sign.base_name name) "strong_cases"), + [Attrib.internal (K (RuleCases.case_names (map snd cases))), + Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])])) + (strong_cases ~~ induct_cases')) |> snd + end) (map (map (rulify_term thy #> rpair [])) vc_compat) end; -fun prove_eqvt s xatoms thy = +fun prove_eqvt s xatoms 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 raw_induct = atomize_induct ctxt raw_induct; @@ -594,6 +597,7 @@ (s, ths ~~ InductivePackage.infer_intro_vars th k ths)) (InductivePackage.partition_rules raw_induct intrs ~~ InductivePackage.arities_of raw_induct ~~ elims)); + val k = length (InductivePackage.params_of raw_induct); val atoms' = NominalAtoms.atoms_of thy; val atoms = if null xatoms then atoms' else @@ -612,19 +616,21 @@ (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs [mk_perm_bool_simproc names, NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; - val t = Logic.unvarify (concl_of raw_induct); - val pi = Name.variant (OldTerm.add_term_names (t, [])) "pi"; + val (([t], [pi]), ctxt') = ctxt |> + Variable.import_terms false [concl_of raw_induct] ||>> + Variable.variant_fixes ["pi"]; val ps = map (fst o HOLogic.dest_imp) (HOLogic.dest_conj (HOLogic.dest_Trueprop t)); - fun eqvt_tac pi (intr, vs) st = + fun eqvt_tac ctxt'' pi (intr, vs) st = let - fun eqvt_err s = error - ("Could not prove equivariance for introduction rule\n" ^ - Syntax.string_of_term_global (theory_of_thm intr) - (Logic.unvarify (prop_of intr)) ^ "\n" ^ s); + fun eqvt_err s = + let val ([t], ctxt''') = Variable.import_terms true [prop_of intr] ctxt + in error ("Could not prove equivariance for introduction rule\n" ^ + Syntax.string_of_term ctxt''' t ^ "\n" ^ s) + end; val res = SUBPROOF (fn {prems, params, ...} => let - val prems' = map (fn th => the_default th (map_thm ctxt + val prems' = map (fn th => the_default th (map_thm ctxt' (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems; val prems'' = map (fn th => Simplifier.simplify eqvt_ss (mk_perm_bool (cterm_of thy pi) th)) prems'; @@ -632,29 +638,36 @@ map (cterm_of thy o NominalPackage.mk_perm [] pi o term_of) params) intr in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1 - end) ctxt 1 st + end) ctxt' 1 st in case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of NONE => eqvt_err ("Rule does not match goal\n" ^ - Syntax.string_of_term_global (theory_of_thm st) (hd (prems_of st))) + Syntax.string_of_term ctxt'' (hd (prems_of st))) | SOME (th, _) => Seq.single th end; val thss = map (fn atom => let val pi' = Free (pi, NominalAtoms.mk_permT (Type (atom, []))) in map (fn th => zero_var_indexes (th RS mp)) - (DatatypeAux.split_conj_thm (Goal.prove_global thy [] [] + (DatatypeAux.split_conj_thm (Goal.prove ctxt' [] [] (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p => - HOLogic.mk_imp (p, list_comb - (apsnd (map (NominalPackage.mk_perm [] pi')) (strip_comb p)))) ps))) - (fn _ => EVERY (rtac raw_induct 1 :: map (fn intr_vs => + let + val (h, ts) = strip_comb p; + val (ts1, ts2) = chop k ts + in + HOLogic.mk_imp (p, list_comb (h, ts1 @ + map (NominalPackage.mk_perm [] pi') ts2)) + end) ps))) + (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs => full_simp_tac eqvt_ss 1 THEN - eqvt_tac pi' intr_vs) intrs')))) + eqvt_tac context pi' intr_vs) intrs')) |> + singleton (ProofContext.export ctxt' ctxt))) end) atoms in - fold (fn (name, ths) => - Sign.add_path (Sign.base_name name) #> - PureThy.add_thmss [((Binding.name "eqvt", ths), [NominalThmDecls.eqvt_add])] #> snd #> - Sign.parent_path) (names ~~ transp thss) thy + ctxt |> + LocalTheory.notes Thm.theoremK (map (fn (name, ths) => + ((Binding.name (NameSpace.qualified (Sign.base_name name) "eqvt"), + [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])])) + (names ~~ transp thss)) |> snd end; @@ -665,17 +678,17 @@ val _ = OuterKeyword.keyword "avoids"; val _ = - OuterSyntax.command "nominal_inductive" + OuterSyntax.local_theory_to_proof "nominal_inductive" "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal - (P.name -- Scan.optional (P.$$$ "avoids" |-- P.and_list1 (P.name -- + (P.xname -- Scan.optional (P.$$$ "avoids" |-- P.and_list1 (P.name -- (P.$$$ ":" |-- Scan.repeat1 P.name))) [] >> (fn (name, avoids) => - Toplevel.print o Toplevel.theory_to_proof (prove_strong_ind name avoids))); + prove_strong_ind name avoids)); val _ = - OuterSyntax.command "equivariance" + OuterSyntax.local_theory "equivariance" "prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl - (P.name -- Scan.optional (P.$$$ "[" |-- P.list1 P.name --| P.$$$ "]") [] >> - (fn (name, atoms) => Toplevel.theory (prove_eqvt name atoms))); + (P.xname -- Scan.optional (P.$$$ "[" |-- P.list1 P.name --| P.$$$ "]") [] >> + (fn (name, atoms) => prove_eqvt name atoms)); end; diff -r 3d6aab74a184 -r 7b25295489b6 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Wed Feb 25 10:24:58 2009 +0100 +++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Feb 25 11:49:05 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,8 @@ fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); +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 +150,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 +168,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; @@ -221,8 +222,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 +254,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 +277,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 +346,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 +364,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 +406,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 +436,40 @@ 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) |> 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 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 +479,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; diff -r 3d6aab74a184 -r 7b25295489b6 src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Wed Feb 25 10:24:58 2009 +0100 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Wed Feb 25 11:49:05 2009 +0100 @@ -1,5 +1,4 @@ -(* ID: "$Id$" - Authors: Julien Narboux and Christian Urban +(* Authors: Julien Narboux and Christian Urban This file introduces the infrastructure for the lemma declaration "eqvts" "bijs" and "freshs". @@ -63,10 +62,11 @@ then tac THEN print_tac ("after "^msg) else tac -fun tactic_eqvt ctx orig_thm pi typi = +fun tactic_eqvt ctx orig_thm pi pi' = let - val mypi = Thm.cterm_of ctx (Var (pi,typi)) - val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi)) + val mypi = Thm.cterm_of ctx pi + val T = fastype_of pi' + val mypifree = Thm.cterm_of ctx (Const ("List.rev", T --> T) $ pi') val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp" in EVERY [tactic ("iffI applied",rtac iffI 1), @@ -80,14 +80,19 @@ full_simp_tac (HOL_basic_ss addsimps perm_pi_simp) 1)] end; -fun get_derived_thm thy hyp concl orig_thm pi typi = - let - val lhs = (Const("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ Var(pi,typi) $ hyp) - val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl))) - val _ = Display.print_cterm (cterm_of thy goal_term) - in - Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi)) - end +fun get_derived_thm ctxt hyp concl orig_thm pi typi = + let + val thy = ProofContext.theory_of ctxt; + val pi' = Var (pi, typi); + val lhs = Const ("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp; + val ([goal_term, pi''], ctxt') = Variable.import_terms false + [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt + val _ = Display.print_cterm (cterm_of thy goal_term) + in + Goal.prove ctxt' [] [] goal_term + (fn _ => tactic_eqvt thy orig_thm pi' pi'') |> + singleton (ProofContext.export ctxt' ctxt) + end (* replaces every variable x in t with pi o x *) fun apply_pi trm (pi,typi) = @@ -145,7 +150,8 @@ if (apply_pi hyp (pi,typi) = concl) then (warning ("equivariance lemma of the relational form"); - [orig_thm, get_derived_thm thy hyp concl orig_thm pi typi]) + [orig_thm, + get_derived_thm (Context.proof_of context) hyp concl orig_thm pi typi]) else raise EQVT_FORM "Type Implication" end (* case: eqvt-lemma is of the equational form *) diff -r 3d6aab74a184 -r 7b25295489b6 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Wed Feb 25 10:24:58 2009 +0100 +++ b/src/HOL/Tools/inductive_package.ML Wed Feb 25 11:49:05 2009 +0100 @@ -738,7 +738,7 @@ val _ = message (quiet_mode andalso not verbose) ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names); - val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn; (* FIXME *) + val cnames = map (LocalTheory.full_name ctxt o #1) cnames_syn; (* FIXME *) val ((intr_names, intr_atts), intr_ts) = apfst split_list (split_list (map (check_rule ctxt cs params) intros)); diff -r 3d6aab74a184 -r 7b25295489b6 src/HOL/Tools/inductive_set_package.ML --- a/src/HOL/Tools/inductive_set_package.ML Wed Feb 25 10:24:58 2009 +0100 +++ b/src/HOL/Tools/inductive_set_package.ML Wed Feb 25 11:49:05 2009 +0100 @@ -503,7 +503,7 @@ if Binding.is_empty alt_name then Binding.name (space_implode "_" (map (Binding.base_name o fst) cnames_syn)) else alt_name; - val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o #1) cnames_syn; (* FIXME *) + val cnames = map (LocalTheory.full_name ctxt3 o #1) cnames_syn; (* FIXME *) val (intr_names, intr_atts) = split_list (map fst intros); val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct; val (intrs', elims', induct, ctxt4) =