src/HOL/Nominal/nominal_inductive.ML
changeset 51717 9e7d1c139569
parent 50771 2852f997bfb5
child 54895 515630483010
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -20,12 +20,12 @@
     1.4  
     1.5  fun rulify_term thy = Raw_Simplifier.rewrite_term thy inductive_rulify [];
     1.6  
     1.7 -val atomize_conv =
     1.8 +fun atomize_conv ctxt =
     1.9    Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
    1.10 -    (HOL_basic_ss addsimps inductive_atomize);
    1.11 -val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
    1.12 +    (put_simpset HOL_basic_ss ctxt addsimps inductive_atomize);
    1.13 +fun atomize_intr ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (atomize_conv ctxt));
    1.14  fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
    1.15 -  (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
    1.16 +  (Conv.params_conv ~1 (K (Conv.prems_conv ~1 (atomize_conv ctxt))) ctxt));
    1.17  
    1.18  fun preds_of ps t = inter (op = o apsnd dest_Free) ps (Term.add_frees t []);
    1.19  
    1.20 @@ -40,7 +40,7 @@
    1.21    [(perm_boolI_pi, pi)] perm_boolI;
    1.22  
    1.23  fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
    1.24 -  (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss =>
    1.25 +  (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
    1.26      fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
    1.27           if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
    1.28           then SOME perm_bool else NONE
    1.29 @@ -103,10 +103,10 @@
    1.30        else NONE
    1.31    | inst_conj_all _ _ _ _ _ = NONE;
    1.32  
    1.33 -fun inst_conj_all_tac k = EVERY
    1.34 +fun inst_conj_all_tac ctxt k = EVERY
    1.35    [TRY (EVERY [etac conjE 1, rtac conjI 1, atac 1]),
    1.36     REPEAT_DETERM_N k (etac allE 1),
    1.37 -   simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1];
    1.38 +   simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm id_apply}]) 1];
    1.39  
    1.40  fun map_term f t u = (case f t u of
    1.41        NONE => map_term' f t u | x => x)
    1.42 @@ -271,10 +271,10 @@
    1.43      val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
    1.44      val pt2_atoms = map (fn aT => Global_Theory.get_thm thy
    1.45        ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
    1.46 -    val eqvt_ss = Simplifier.global_context thy HOL_basic_ss
    1.47 +    val eqvt_ss = simpset_of (Simplifier.global_context thy HOL_basic_ss
    1.48        addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
    1.49        addsimprocs [mk_perm_bool_simproc [@{const_name Fun.id}],
    1.50 -        NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
    1.51 +        NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]);
    1.52      val fresh_bij = Global_Theory.get_thms thy "fresh_bij";
    1.53      val perm_bij = Global_Theory.get_thms thy "perm_bij";
    1.54      val fs_atoms = map (fn aT => Global_Theory.get_thm thy
    1.55 @@ -299,10 +299,10 @@
    1.56              [resolve_tac exists_fresh' 1,
    1.57               resolve_tac fs_atoms 1]);
    1.58          val (([(_, cx)], ths), ctxt') = Obtain.result
    1.59 -          (fn _ => EVERY
    1.60 +          (fn ctxt' => EVERY
    1.61              [etac exE 1,
    1.62 -             full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
    1.63 -             full_simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1,
    1.64 +             full_simp_tac (put_simpset HOL_ss ctxt' addsimps (fresh_prod :: fresh_atm)) 1,
    1.65 +             full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]) 1,
    1.66               REPEAT (etac conjE 1)])
    1.67            [ex] ctxt
    1.68        in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
    1.69 @@ -312,7 +312,7 @@
    1.70          let val th = Goal.prove ctxt [] [] concl (fn {context, ...} =>
    1.71            rtac raw_induct 1 THEN
    1.72            EVERY (maps (fn ((((_, bvars, oprems, _), vc_compat_ths), ihyp), (vs, ihypt)) =>
    1.73 -            [REPEAT (rtac allI 1), simp_tac eqvt_ss 1,
    1.74 +            [REPEAT (rtac allI 1), simp_tac (put_simpset eqvt_ss context) 1,
    1.75               SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} =>
    1.76                 let
    1.77                   val (params', (pis, z)) =
    1.78 @@ -343,9 +343,9 @@
    1.79                      map (fold_rev (NominalDatatype.mk_perm [])
    1.80                        (rev pis' @ pis)) params' @ [z])) ihyp;
    1.81                   fun mk_pi th =
    1.82 -                   Simplifier.simplify (HOL_basic_ss addsimps [@{thm id_apply}]
    1.83 +                   Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm id_apply}]
    1.84                         addsimprocs [NominalDatatype.perm_simproc])
    1.85 -                     (Simplifier.simplify eqvt_ss
    1.86 +                     (Simplifier.simplify (put_simpset eqvt_ss ctxt)
    1.87                         (fold_rev (mk_perm_bool o cterm_of thy)
    1.88                           (rev pis' @ pis) th));
    1.89                   val (gprems1, gprems2) = split_list
    1.90 @@ -355,7 +355,7 @@
    1.91                          (map_thm ctxt (split_conj (K o I) names)
    1.92                             (etac conjunct1 1) monos NONE th,
    1.93                           mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis''))
    1.94 -                           (inst_conj_all_tac (length pis'')) monos (SOME t) th))))
    1.95 +                           (inst_conj_all_tac ctxt (length pis'')) monos (SOME t) th))))
    1.96                        (gprems ~~ oprems)) |>> map_filter I;
    1.97                   val vc_compat_ths' = map (fn th =>
    1.98                     let
    1.99 @@ -368,29 +368,29 @@
   1.100                       val th'' = Goal.prove ctxt'' [] [] (HOLogic.mk_Trueprop
   1.101                           (bop (fold_rev (NominalDatatype.mk_perm []) pis lhs)
   1.102                              (fold_rev (NominalDatatype.mk_perm []) pis rhs)))
   1.103 -                       (fn _ => simp_tac (HOL_basic_ss addsimps
   1.104 +                       (fn _ => simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps
   1.105                            (fresh_bij @ perm_bij)) 1 THEN rtac th' 1)
   1.106 -                   in Simplifier.simplify (eqvt_ss addsimps fresh_atm) th'' end)
   1.107 +                   in Simplifier.simplify (put_simpset eqvt_ss ctxt'' addsimps fresh_atm) th'' end)
   1.108                       vc_compat_ths;
   1.109                   val vc_compat_ths'' = NominalDatatype.mk_not_sym vc_compat_ths';
   1.110                   (** Since swap_simps simplifies (pi :: 'a prm) o (x :: 'b) to x **)
   1.111                   (** we have to pre-simplify the rewrite rules                   **)
   1.112 -                 val swap_simps_ss = HOL_ss addsimps swap_simps @
   1.113 -                    map (Simplifier.simplify (HOL_ss addsimps swap_simps))
   1.114 +                 val swap_simps_simpset = put_simpset HOL_ss ctxt'' addsimps swap_simps @
   1.115 +                    map (Simplifier.simplify (put_simpset HOL_ss ctxt'' addsimps swap_simps))
   1.116                        (vc_compat_ths'' @ freshs2');
   1.117                   val th = Goal.prove ctxt'' [] []
   1.118                     (HOLogic.mk_Trueprop (list_comb (P $ hd ts,
   1.119                       map (fold (NominalDatatype.mk_perm []) pis') (tl ts))))
   1.120 -                   (fn _ => EVERY ([simp_tac eqvt_ss 1, rtac ihyp' 1,
   1.121 +                   (fn _ => EVERY ([simp_tac (put_simpset eqvt_ss ctxt'') 1, rtac ihyp' 1,
   1.122                       REPEAT_DETERM_N (nprems_of ihyp - length gprems)
   1.123 -                       (simp_tac swap_simps_ss 1),
   1.124 +                       (simp_tac swap_simps_simpset 1),
   1.125                       REPEAT_DETERM_N (length gprems)
   1.126 -                       (simp_tac (HOL_basic_ss
   1.127 +                       (simp_tac (put_simpset HOL_basic_ss ctxt''
   1.128                            addsimps [inductive_forall_def']
   1.129                            addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
   1.130                          resolve_tac gprems2 1)]));
   1.131                   val final = Goal.prove ctxt'' [] [] (term_of concl)
   1.132 -                   (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (HOL_ss
   1.133 +                   (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (put_simpset HOL_ss ctxt''
   1.134                       addsimps vc_compat_ths'' @ freshs2' @
   1.135                         perm_fresh_fresh @ fresh_atm) 1);
   1.136                   val final' = Proof_Context.export ctxt'' ctxt' [final];
   1.137 @@ -400,7 +400,7 @@
   1.138            cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN
   1.139            REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
   1.140              etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN
   1.141 -            asm_full_simp_tac (simpset_of ctxt) 1)
   1.142 +            asm_full_simp_tac ctxt 1)
   1.143          end) |> singleton (Proof_Context.export ctxt' ctxt);
   1.144  
   1.145      (** strong case analysis rule **)
   1.146 @@ -452,13 +452,13 @@
   1.147                     concl))
   1.148            in map mk_prem prems end) cases_prems;
   1.149  
   1.150 -    val cases_eqvt_ss = Simplifier.global_context thy HOL_ss
   1.151 +    val cases_eqvt_simpset = Simplifier.global_context thy HOL_ss
   1.152        addsimps eqvt_thms @ swap_simps @ perm_pi_simp
   1.153        addsimprocs [NominalPermeq.perm_simproc_app,
   1.154          NominalPermeq.perm_simproc_fun];
   1.155  
   1.156      val simp_fresh_atm = map
   1.157 -      (Simplifier.simplify (HOL_basic_ss addsimps fresh_atm));
   1.158 +      (Simplifier.simplify (Simplifier.global_context thy HOL_basic_ss addsimps fresh_atm));
   1.159  
   1.160      fun mk_cases_proof ((((name, thss), elim), (prem, args, concl, (prems, ctxt'))),
   1.161          prems') =
   1.162 @@ -520,16 +520,16 @@
   1.163                         SUBPROOF (fn {prems = fresh_hyps, ...} =>
   1.164                           let
   1.165                             val fresh_hyps' = NominalDatatype.mk_not_sym fresh_hyps;
   1.166 -                           val case_ss = cases_eqvt_ss addsimps freshs2' @
   1.167 +                           val case_simpset = cases_eqvt_simpset addsimps freshs2' @
   1.168                               simp_fresh_atm (vc_compat_ths' @ fresh_hyps');
   1.169 -                           val fresh_fresh_ss = case_ss addsimps perm_fresh_fresh;
   1.170 +                           val fresh_fresh_simpset = case_simpset addsimps perm_fresh_fresh;
   1.171                             val hyps1' = map
   1.172 -                             (mk_pis #> Simplifier.simplify fresh_fresh_ss) hyps1;
   1.173 +                             (mk_pis #> Simplifier.simplify fresh_fresh_simpset) hyps1;
   1.174                             val hyps2' = map
   1.175 -                             (mk_pis #> Simplifier.simplify case_ss) hyps2;
   1.176 +                             (mk_pis #> Simplifier.simplify case_simpset) hyps2;
   1.177                             val case_hyps' = hyps1' @ hyps2'
   1.178                           in
   1.179 -                           simp_tac case_ss 1 THEN
   1.180 +                           simp_tac case_simpset 1 THEN
   1.181                             REPEAT_DETERM (TRY (rtac conjI 1) THEN
   1.182                               resolve_tac case_hyps' 1)
   1.183                           end) ctxt4 1)
   1.184 @@ -547,11 +547,11 @@
   1.185          val ind_case_names = Rule_Cases.case_names induct_cases;
   1.186          val induct_cases' = Inductive.partition_rules' raw_induct
   1.187            (intrs ~~ induct_cases); 
   1.188 -        val thss' = map (map atomize_intr) thss;
   1.189 +        val thss' = map (map (atomize_intr ctxt)) thss;
   1.190          val thsss = Inductive.partition_rules' raw_induct (intrs ~~ thss');
   1.191          val strong_raw_induct =
   1.192 -          mk_ind_proof ctxt thss' |> Inductive.rulify;
   1.193 -        val strong_cases = map (mk_cases_proof ##> Inductive.rulify)
   1.194 +          mk_ind_proof ctxt thss' |> Inductive.rulify ctxt;
   1.195 +        val strong_cases = map (mk_cases_proof ##> Inductive.rulify ctxt)
   1.196            (thsss ~~ elims ~~ cases_prems ~~ cases_prems');
   1.197          val strong_induct_atts =
   1.198            map (Attrib.internal o K)
   1.199 @@ -586,7 +586,7 @@
   1.200        Inductive.the_inductive ctxt (Sign.intern_const thy s);
   1.201      val raw_induct = atomize_induct ctxt raw_induct;
   1.202      val elims = map (atomize_induct ctxt) elims;
   1.203 -    val intrs = map atomize_intr intrs;
   1.204 +    val intrs = map (atomize_intr ctxt) intrs;
   1.205      val monos = Inductive.get_monos ctxt;
   1.206      val intrs' = Inductive.unpartition_rules intrs
   1.207        (map (fn (((s, ths), (_, k)), th) =>
   1.208 @@ -608,7 +608,7 @@
   1.209           atoms)
   1.210        end;
   1.211      val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
   1.212 -    val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps
   1.213 +    val eqvt_simpset = Simplifier.global_context thy HOL_basic_ss addsimps
   1.214        (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
   1.215        [mk_perm_bool_simproc names,
   1.216         NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
   1.217 @@ -628,7 +628,7 @@
   1.218            let
   1.219              val prems' = map (fn th => the_default th (map_thm ctxt'
   1.220                (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems;
   1.221 -            val prems'' = map (fn th => Simplifier.simplify eqvt_ss
   1.222 +            val prems'' = map (fn th => Simplifier.simplify eqvt_simpset
   1.223                (mk_perm_bool (cterm_of thy pi) th)) prems';
   1.224              val intr' = Drule.cterm_instantiate (map (cterm_of thy) vs ~~
   1.225                 map (cterm_of thy o NominalDatatype.mk_perm [] pi o term_of o #2) params)
   1.226 @@ -654,7 +654,7 @@
   1.227                  map (NominalDatatype.mk_perm [] pi') ts2))
   1.228              end) ps)))
   1.229            (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>
   1.230 -              full_simp_tac eqvt_ss 1 THEN
   1.231 +              full_simp_tac eqvt_simpset 1 THEN
   1.232                eqvt_tac context pi' intr_vs) intrs')) |>
   1.233            singleton (Proof_Context.export ctxt' ctxt)))
   1.234        end) atoms