src/HOL/Nominal/nominal_inductive.ML
changeset 30240 5b25fee0362c
parent 29585 c23295521af5
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -7,8 +7,8 @@
     1.4  
     1.5  signature NOMINAL_INDUCTIVE =
     1.6  sig
     1.7 -  val prove_strong_ind: string -> (string * string list) list -> theory -> Proof.state
     1.8 -  val prove_eqvt: string -> string list -> theory -> theory
     1.9 +  val prove_strong_ind: string -> (string * string list) list -> local_theory -> Proof.state
    1.10 +  val prove_eqvt: string -> string list -> local_theory -> local_theory
    1.11  end
    1.12  
    1.13  structure NominalInductive : NOMINAL_INDUCTIVE =
    1.14 @@ -28,6 +28,8 @@
    1.15  fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
    1.16    (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
    1.17  
    1.18 +fun preds_of ps t = gen_inter (op = o apfst dest_Free) (ps, Term.add_frees t []);
    1.19 +
    1.20  val fresh_prod = thm "fresh_prod";
    1.21  
    1.22  val perm_bool = mk_meta_eq (thm "perm_bool");
    1.23 @@ -142,9 +144,9 @@
    1.24  fun first_order_mrs ths th = ths MRS
    1.25    Thm.instantiate (first_order_matchs (cprems_of th) (map cprop_of ths)) th;
    1.26  
    1.27 -fun prove_strong_ind s avoids thy =
    1.28 +fun prove_strong_ind s avoids ctxt =
    1.29    let
    1.30 -    val ctxt = ProofContext.init thy;
    1.31 +    val thy = ProofContext.theory_of ctxt;
    1.32      val ({names, ...}, {raw_induct, intrs, elims, ...}) =
    1.33        InductivePackage.the_inductive ctxt (Sign.intern_const thy s);
    1.34      val ind_params = InductivePackage.params_of raw_induct;
    1.35 @@ -158,8 +160,7 @@
    1.36            commas_quote xs));
    1.37      val induct_cases = map fst (fst (RuleCases.get (the
    1.38        (Induct.lookup_inductP ctxt (hd names)))));
    1.39 -    val raw_induct' = Logic.unvarify (prop_of raw_induct);
    1.40 -    val elims' = map (Logic.unvarify o prop_of) elims;
    1.41 +    val ([raw_induct'], ctxt') = Variable.import_terms false [prop_of raw_induct] ctxt;
    1.42      val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
    1.43        HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);
    1.44      val ps = map (fst o snd) concls;
    1.45 @@ -199,8 +200,8 @@
    1.46      val ind_sort = if null atomTs then HOLogic.typeS
    1.47        else Sign.certify_sort thy (map (fn T => Sign.intern_class thy
    1.48          ("fs_" ^ Sign.base_name (fst (dest_Type T)))) atomTs);
    1.49 -    val fs_ctxt_tyname = Name.variant (map fst (OldTerm.term_tfrees raw_induct')) "'n";
    1.50 -    val fs_ctxt_name = Name.variant (OldTerm.add_term_names (raw_induct', [])) "z";
    1.51 +    val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
    1.52 +    val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
    1.53      val fsT = TFree (fs_ctxt_tyname, ind_sort);
    1.54  
    1.55      val inductive_forall_def' = Drule.instantiate'
    1.56 @@ -237,7 +238,7 @@
    1.57          val prem = Logic.list_implies
    1.58            (map mk_fresh bvars @ mk_distinct bvars @
    1.59             map (fn prem =>
    1.60 -             if null (OldTerm.term_frees prem inter ps) then prem
    1.61 +             if null (preds_of ps prem) then prem
    1.62               else lift_prem prem) prems,
    1.63             HOLogic.mk_Trueprop (lift_pred p ts));
    1.64          val vs = map (Var o apfst (rpair 0)) (Term.rename_wrt_term prem params')
    1.65 @@ -263,7 +264,7 @@
    1.66      val vc_compat = map (fn (params, bvars, prems, (p, ts)) =>
    1.67        map (fn q => list_all (params, incr_boundvars ~1 (Logic.list_implies
    1.68            (List.mapPartial (fn prem =>
    1.69 -             if null (ps inter OldTerm.term_frees prem) then SOME prem
    1.70 +             if null (preds_of ps prem) then SOME prem
    1.71               else map_term (split_conj (K o I) names) prem prem) prems, q))))
    1.72          (mk_distinct bvars @
    1.73           maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop
    1.74 @@ -309,8 +310,8 @@
    1.75            [ex] ctxt
    1.76        in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
    1.77  
    1.78 -    fun mk_ind_proof thy thss =
    1.79 -      Goal.prove_global thy [] prems' concl' (fn {prems = ihyps, context = ctxt} =>
    1.80 +    fun mk_ind_proof ctxt' thss =
    1.81 +      Goal.prove ctxt' [] prems' concl' (fn {prems = ihyps, context = ctxt} =>
    1.82          let val th = Goal.prove ctxt [] [] concl (fn {context, ...} =>
    1.83            rtac raw_induct 1 THEN
    1.84            EVERY (maps (fn ((((_, bvars, oprems, _), vc_compat_ths), ihyp), (vs, ihypt)) =>
    1.85 @@ -352,7 +353,7 @@
    1.86                           (rev pis' @ pis) th));
    1.87                   val (gprems1, gprems2) = split_list
    1.88                     (map (fn (th, t) =>
    1.89 -                      if null (OldTerm.term_frees t inter ps) then (SOME th, mk_pi th)
    1.90 +                      if null (preds_of ps t) then (SOME th, mk_pi th)
    1.91                        else
    1.92                          (map_thm ctxt (split_conj (K o I) names)
    1.93                             (etac conjunct1 1) monos NONE th,
    1.94 @@ -403,42 +404,42 @@
    1.95            REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
    1.96              etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN
    1.97              asm_full_simp_tac (simpset_of thy) 1)
    1.98 -        end);
    1.99 +        end) |> singleton (ProofContext.export ctxt' ctxt);
   1.100  
   1.101      (** strong case analysis rule **)
   1.102  
   1.103      val cases_prems = map (fn ((name, avoids), rule) =>
   1.104        let
   1.105 -        val prem :: prems = Logic.strip_imp_prems rule;
   1.106 -        val concl = Logic.strip_imp_concl rule;
   1.107 -        val used = Term.add_free_names rule [];
   1.108 +        val ([rule'], ctxt') = Variable.import_terms false [prop_of rule] ctxt;
   1.109 +        val prem :: prems = Logic.strip_imp_prems rule';
   1.110 +        val concl = Logic.strip_imp_concl rule'
   1.111        in
   1.112          (prem,
   1.113           List.drop (snd (strip_comb (HOLogic.dest_Trueprop prem)), length ind_params),
   1.114           concl,
   1.115 -         fst (fold_map (fn (prem, (_, avoid)) => fn used =>
   1.116 +         fold_map (fn (prem, (_, avoid)) => fn ctxt =>
   1.117             let
   1.118               val prems = Logic.strip_assums_hyp prem;
   1.119               val params = Logic.strip_params prem;
   1.120               val bnds = fold (add_binders thy 0) prems [] @ mk_avoids params avoid;
   1.121 -             fun mk_subst (p as (s, T)) (i, j, used, ps, qs, is, ts) =
   1.122 +             fun mk_subst (p as (s, T)) (i, j, ctxt, ps, qs, is, ts) =
   1.123                 if member (op = o apsnd fst) bnds (Bound i) then
   1.124                   let
   1.125 -                   val s' = Name.variant used s;
   1.126 +                   val ([s'], ctxt') = Variable.variant_fixes [s] ctxt;
   1.127                     val t = Free (s', T)
   1.128 -                 in (i + 1, j, s' :: used, ps, (t, T) :: qs, i :: is, t :: ts) end
   1.129 -               else (i + 1, j + 1, used, p :: ps, qs, is, Bound j :: ts);
   1.130 -             val (_, _, used', ps, qs, is, ts) = fold_rev mk_subst params
   1.131 -               (0, 0, used, [], [], [], [])
   1.132 +                 in (i + 1, j, ctxt', ps, (t, T) :: qs, i :: is, t :: ts) end
   1.133 +               else (i + 1, j + 1, ctxt, p :: ps, qs, is, Bound j :: ts);
   1.134 +             val (_, _, ctxt', ps, qs, is, ts) = fold_rev mk_subst params
   1.135 +               (0, 0, ctxt, [], [], [], [])
   1.136             in
   1.137 -             ((ps, qs, is, map (curry subst_bounds (rev ts)) prems), used')
   1.138 -           end) (prems ~~ avoids) used))
   1.139 +             ((ps, qs, is, map (curry subst_bounds (rev ts)) prems), ctxt')
   1.140 +           end) (prems ~~ avoids) ctxt')
   1.141        end)
   1.142          (InductivePackage.partition_rules' raw_induct (intrs ~~ avoids') ~~
   1.143 -         elims');
   1.144 +         elims);
   1.145  
   1.146      val cases_prems' =
   1.147 -      map (fn (prem, args, concl, prems) =>
   1.148 +      map (fn (prem, args, concl, (prems, _)) =>
   1.149          let
   1.150            fun mk_prem (ps, [], _, prems) =
   1.151                  list_all (ps, Logic.list_implies (prems, concl))
   1.152 @@ -462,9 +463,9 @@
   1.153      val simp_fresh_atm = map
   1.154        (Simplifier.simplify (HOL_basic_ss addsimps fresh_atm));
   1.155  
   1.156 -    fun mk_cases_proof thy ((((name, thss), elim), (prem, args, concl, prems)),
   1.157 +    fun mk_cases_proof ((((name, thss), elim), (prem, args, concl, (prems, ctxt'))),
   1.158          prems') =
   1.159 -      (name, Goal.prove_global thy [] (prem :: prems') concl
   1.160 +      (name, Goal.prove ctxt' [] (prem :: prems') concl
   1.161          (fn {prems = hyp :: hyps, context = ctxt1} =>
   1.162          EVERY (rtac (hyp RS elim) 1 ::
   1.163            map (fn (((_, vc_compat_ths), case_hyp), (_, qs, is, _)) =>
   1.164 @@ -537,52 +538,54 @@
   1.165                           end) ctxt4 1)
   1.166                    val final = ProofContext.export ctxt3 ctxt2 [th]
   1.167                  in resolve_tac final 1 end) ctxt1 1)
   1.168 -                  (thss ~~ hyps ~~ prems))))
   1.169 +                  (thss ~~ hyps ~~ prems))) |>
   1.170 +                  singleton (ProofContext.export ctxt' ctxt))
   1.171  
   1.172    in
   1.173 -    thy |>
   1.174 -    ProofContext.init |>
   1.175 -    Proof.theorem_i NONE (fn thss => ProofContext.theory (fn thy =>
   1.176 +    ctxt'' |>
   1.177 +    Proof.theorem_i NONE (fn thss => fn ctxt =>
   1.178        let
   1.179 -        val ctxt = ProofContext.init thy;
   1.180          val rec_name = space_implode "_" (map Sign.base_name names);
   1.181 +        val rec_qualified = Binding.qualify false rec_name;
   1.182          val ind_case_names = RuleCases.case_names induct_cases;
   1.183          val induct_cases' = InductivePackage.partition_rules' raw_induct
   1.184            (intrs ~~ induct_cases); 
   1.185          val thss' = map (map atomize_intr) thss;
   1.186          val thsss = InductivePackage.partition_rules' raw_induct (intrs ~~ thss');
   1.187          val strong_raw_induct =
   1.188 -          mk_ind_proof thy thss' |> InductivePackage.rulify;
   1.189 -        val strong_cases = map (mk_cases_proof thy ##> InductivePackage.rulify)
   1.190 +          mk_ind_proof ctxt thss' |> InductivePackage.rulify;
   1.191 +        val strong_cases = map (mk_cases_proof ##> InductivePackage.rulify)
   1.192            (thsss ~~ elims ~~ cases_prems ~~ cases_prems');
   1.193          val strong_induct =
   1.194            if length names > 1 then
   1.195              (strong_raw_induct, [ind_case_names, RuleCases.consumes 0])
   1.196            else (strong_raw_induct RSN (2, rev_mp),
   1.197              [ind_case_names, RuleCases.consumes 1]);
   1.198 -        val ([strong_induct'], thy') = thy |>
   1.199 -          Sign.add_path rec_name |>
   1.200 -          PureThy.add_thms [((Binding.name "strong_induct", #1 strong_induct), #2 strong_induct)];
   1.201 +        val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.theoremK
   1.202 +          ((rec_qualified (Binding.name "strong_induct"),
   1.203 +            map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
   1.204 +          ctxt;
   1.205          val strong_inducts =
   1.206            ProjectRule.projects ctxt (1 upto length names) strong_induct'
   1.207        in
   1.208 -        thy' |>
   1.209 -        PureThy.add_thmss [((Binding.name "strong_inducts", strong_inducts),
   1.210 -          [ind_case_names, RuleCases.consumes 1])] |> snd |>
   1.211 -        Sign.parent_path |>
   1.212 -        fold (fn ((name, elim), (_, cases)) =>
   1.213 -          Sign.add_path (Sign.base_name name) #>
   1.214 -          PureThy.add_thms [((Binding.name "strong_cases", elim),
   1.215 -            [RuleCases.case_names (map snd cases),
   1.216 -             RuleCases.consumes 1])] #> snd #>
   1.217 -          Sign.parent_path) (strong_cases ~~ induct_cases')
   1.218 -      end))
   1.219 +        ctxt' |>
   1.220 +        LocalTheory.note Thm.theoremK
   1.221 +          ((rec_qualified (Binding.name "strong_inducts"),
   1.222 +            [Attrib.internal (K ind_case_names),
   1.223 +             Attrib.internal (K (RuleCases.consumes 1))]),
   1.224 +           strong_inducts) |> snd |>
   1.225 +        LocalTheory.notes Thm.theoremK (map (fn ((name, elim), (_, cases)) =>
   1.226 +            ((Binding.name (NameSpace.qualified (Sign.base_name name) "strong_cases"),
   1.227 +              [Attrib.internal (K (RuleCases.case_names (map snd cases))),
   1.228 +               Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])]))
   1.229 +          (strong_cases ~~ induct_cases')) |> snd
   1.230 +      end)
   1.231        (map (map (rulify_term thy #> rpair [])) vc_compat)
   1.232    end;
   1.233  
   1.234 -fun prove_eqvt s xatoms thy =
   1.235 +fun prove_eqvt s xatoms ctxt =
   1.236    let
   1.237 -    val ctxt = ProofContext.init thy;
   1.238 +    val thy = ProofContext.theory_of ctxt;
   1.239      val ({names, ...}, {raw_induct, intrs, elims, ...}) =
   1.240        InductivePackage.the_inductive ctxt (Sign.intern_const thy s);
   1.241      val raw_induct = atomize_induct ctxt raw_induct;
   1.242 @@ -594,6 +597,7 @@
   1.243             (s, ths ~~ InductivePackage.infer_intro_vars th k ths))
   1.244           (InductivePackage.partition_rules raw_induct intrs ~~
   1.245            InductivePackage.arities_of raw_induct ~~ elims));
   1.246 +    val k = length (InductivePackage.params_of raw_induct);
   1.247      val atoms' = NominalAtoms.atoms_of thy;
   1.248      val atoms =
   1.249        if null xatoms then atoms' else
   1.250 @@ -612,19 +616,21 @@
   1.251        (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
   1.252        [mk_perm_bool_simproc names,
   1.253         NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
   1.254 -    val t = Logic.unvarify (concl_of raw_induct);
   1.255 -    val pi = Name.variant (OldTerm.add_term_names (t, [])) "pi";
   1.256 +    val (([t], [pi]), ctxt') = ctxt |>
   1.257 +      Variable.import_terms false [concl_of raw_induct] ||>>
   1.258 +      Variable.variant_fixes ["pi"];
   1.259      val ps = map (fst o HOLogic.dest_imp)
   1.260        (HOLogic.dest_conj (HOLogic.dest_Trueprop t));
   1.261 -    fun eqvt_tac pi (intr, vs) st =
   1.262 +    fun eqvt_tac ctxt'' pi (intr, vs) st =
   1.263        let
   1.264 -        fun eqvt_err s = error
   1.265 -          ("Could not prove equivariance for introduction rule\n" ^
   1.266 -           Syntax.string_of_term_global (theory_of_thm intr)
   1.267 -             (Logic.unvarify (prop_of intr)) ^ "\n" ^ s);
   1.268 +        fun eqvt_err s =
   1.269 +          let val ([t], ctxt''') = Variable.import_terms true [prop_of intr] ctxt
   1.270 +          in error ("Could not prove equivariance for introduction rule\n" ^
   1.271 +            Syntax.string_of_term ctxt''' t ^ "\n" ^ s)
   1.272 +          end;
   1.273          val res = SUBPROOF (fn {prems, params, ...} =>
   1.274            let
   1.275 -            val prems' = map (fn th => the_default th (map_thm ctxt
   1.276 +            val prems' = map (fn th => the_default th (map_thm ctxt'
   1.277                (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems;
   1.278              val prems'' = map (fn th => Simplifier.simplify eqvt_ss
   1.279                (mk_perm_bool (cterm_of thy pi) th)) prems';
   1.280 @@ -632,29 +638,36 @@
   1.281                 map (cterm_of thy o NominalPackage.mk_perm [] pi o term_of) params)
   1.282                 intr
   1.283            in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1
   1.284 -          end) ctxt 1 st
   1.285 +          end) ctxt' 1 st
   1.286        in
   1.287          case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of
   1.288            NONE => eqvt_err ("Rule does not match goal\n" ^
   1.289 -            Syntax.string_of_term_global (theory_of_thm st) (hd (prems_of st)))
   1.290 +            Syntax.string_of_term ctxt'' (hd (prems_of st)))
   1.291          | SOME (th, _) => Seq.single th
   1.292        end;
   1.293      val thss = map (fn atom =>
   1.294        let val pi' = Free (pi, NominalAtoms.mk_permT (Type (atom, [])))
   1.295        in map (fn th => zero_var_indexes (th RS mp))
   1.296 -        (DatatypeAux.split_conj_thm (Goal.prove_global thy [] []
   1.297 +        (DatatypeAux.split_conj_thm (Goal.prove ctxt' [] []
   1.298            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p =>
   1.299 -            HOLogic.mk_imp (p, list_comb
   1.300 -             (apsnd (map (NominalPackage.mk_perm [] pi')) (strip_comb p)))) ps)))
   1.301 -          (fn _ => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>
   1.302 +            let
   1.303 +              val (h, ts) = strip_comb p;
   1.304 +              val (ts1, ts2) = chop k ts
   1.305 +            in
   1.306 +              HOLogic.mk_imp (p, list_comb (h, ts1 @
   1.307 +                map (NominalPackage.mk_perm [] pi') ts2))
   1.308 +            end) ps)))
   1.309 +          (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>
   1.310                full_simp_tac eqvt_ss 1 THEN
   1.311 -              eqvt_tac pi' intr_vs) intrs'))))
   1.312 +              eqvt_tac context pi' intr_vs) intrs')) |>
   1.313 +          singleton (ProofContext.export ctxt' ctxt)))
   1.314        end) atoms
   1.315    in
   1.316 -    fold (fn (name, ths) =>
   1.317 -      Sign.add_path (Sign.base_name name) #>
   1.318 -      PureThy.add_thmss [((Binding.name "eqvt", ths), [NominalThmDecls.eqvt_add])] #> snd #>
   1.319 -      Sign.parent_path) (names ~~ transp thss) thy
   1.320 +    ctxt |>
   1.321 +    LocalTheory.notes Thm.theoremK (map (fn (name, ths) =>
   1.322 +        ((Binding.name (NameSpace.qualified (Sign.base_name name) "eqvt"),
   1.323 +          [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
   1.324 +      (names ~~ transp thss)) |> snd
   1.325    end;
   1.326  
   1.327  
   1.328 @@ -665,17 +678,17 @@
   1.329  val _ = OuterKeyword.keyword "avoids";
   1.330  
   1.331  val _ =
   1.332 -  OuterSyntax.command "nominal_inductive"
   1.333 +  OuterSyntax.local_theory_to_proof "nominal_inductive"
   1.334      "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
   1.335 -    (P.name -- Scan.optional (P.$$$ "avoids" |-- P.and_list1 (P.name --
   1.336 +    (P.xname -- Scan.optional (P.$$$ "avoids" |-- P.and_list1 (P.name --
   1.337        (P.$$$ ":" |-- Scan.repeat1 P.name))) [] >> (fn (name, avoids) =>
   1.338 -        Toplevel.print o Toplevel.theory_to_proof (prove_strong_ind name avoids)));
   1.339 +        prove_strong_ind name avoids));
   1.340  
   1.341  val _ =
   1.342 -  OuterSyntax.command "equivariance"
   1.343 +  OuterSyntax.local_theory "equivariance"
   1.344      "prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl
   1.345 -    (P.name -- Scan.optional (P.$$$ "[" |-- P.list1 P.name --| P.$$$ "]") [] >>
   1.346 -      (fn (name, atoms) => Toplevel.theory (prove_eqvt name atoms)));
   1.347 +    (P.xname -- Scan.optional (P.$$$ "[" |-- P.list1 P.name --| P.$$$ "]") [] >>
   1.348 +      (fn (name, atoms) => prove_eqvt name atoms));
   1.349  
   1.350  end;
   1.351