src/HOL/Nominal/nominal_package.ML
changeset 20046 9c8909fc5865
parent 19985 d39c554cf750
child 20071 8f3e1ddb50e6
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Sat Jul 08 12:54:32 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Sat Jul 08 12:54:33 2006 +0200
     1.3 @@ -255,7 +255,7 @@
     1.4      val unfolded_perm_eq_thms =
     1.5        if length descr = length new_type_names then []
     1.6        else map standard (List.drop (split_conj_thm
     1.7 -        (Goal.prove thy2 [] []
     1.8 +        (Goal.prove_global thy2 [] []
     1.9            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.10              (map (fn (c as (s, T), x) =>
    1.11                 let val [T1, T2] = binder_types T
    1.12 @@ -275,7 +275,7 @@
    1.13      val perm_empty_thms = List.concat (map (fn a =>
    1.14        let val permT = mk_permT (Type (a, []))
    1.15        in map standard (List.take (split_conj_thm
    1.16 -        (Goal.prove thy2 [] []
    1.17 +        (Goal.prove_global thy2 [] []
    1.18            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.19              (map (fn ((s, T), x) => HOLogic.mk_eq
    1.20                  (Const (s, permT --> T --> T) $
    1.21 @@ -307,7 +307,7 @@
    1.22          val pt2_ax = PureThy.get_thm thy2
    1.23            (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a));
    1.24        in List.take (map standard (split_conj_thm
    1.25 -        (Goal.prove thy2 [] []
    1.26 +        (Goal.prove_global thy2 [] []
    1.27               (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.28                  (map (fn ((s, T), x) =>
    1.29                      let val perm = Const (s, permT --> T --> T)
    1.30 @@ -343,7 +343,7 @@
    1.31          val pt3_ax = PureThy.get_thm thy2
    1.32            (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a));
    1.33        in List.take (map standard (split_conj_thm
    1.34 -        (Goal.prove thy2 [] [] (Logic.mk_implies
    1.35 +        (Goal.prove_global thy2 [] [] (Logic.mk_implies
    1.36               (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
    1.37                  permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
    1.38                HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.39 @@ -393,7 +393,7 @@
    1.40                  at_inst RS (pt_inst RS pt_perm_compose) RS sym,
    1.41                  at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym]
    1.42              end))
    1.43 -        val thms = split_conj_thm (standard (Goal.prove thy [] []
    1.44 +        val thms = split_conj_thm (Goal.prove_global thy [] []
    1.45              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.46                (map (fn ((s, T), x) =>
    1.47                    let
    1.48 @@ -408,7 +408,7 @@
    1.49                    end)
    1.50                  (perm_names ~~ Ts ~~ perm_indnames))))
    1.51            (fn _ => EVERY [indtac induction perm_indnames 1,
    1.52 -             ALLGOALS (asm_full_simp_tac simps)])))
    1.53 +             ALLGOALS (asm_full_simp_tac simps)]))
    1.54        in
    1.55          foldl (fn ((s, tvs), thy) => AxClass.prove_arity
    1.56              (s, replicate (length tvs) (cp_class :: classes), [cp_class])
    1.57 @@ -517,7 +517,7 @@
    1.58        (perm_indnames ~~ descr);
    1.59  
    1.60      fun mk_perm_closed name = map (fn th => standard (th RS mp))
    1.61 -      (List.take (split_conj_thm (Goal.prove thy4 [] []
    1.62 +      (List.take (split_conj_thm (Goal.prove_global thy4 [] []
    1.63          (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
    1.64             (fn (S, x) =>
    1.65                let
    1.66 @@ -766,12 +766,12 @@
    1.67        let
    1.68          val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
    1.69          val rewrites = constr_defs @ map mk_meta_eq rep_inverse_thms
    1.70 -      in standard (Goal.prove thy8 [] [] eqn (fn _ => EVERY
    1.71 +      in Goal.prove_global thy8 [] [] eqn (fn _ => EVERY
    1.72          [resolve_tac inj_thms 1,
    1.73           rewrite_goals_tac rewrites,
    1.74           rtac refl 3,
    1.75           resolve_tac rep_intrs 2,
    1.76 -         REPEAT (resolve_tac rep_thms 1)]))
    1.77 +         REPEAT (resolve_tac rep_thms 1)])
    1.78        end;
    1.79  
    1.80      val constr_rep_thmss = map (map prove_constr_rep_thm) constr_rep_eqns;
    1.81 @@ -785,11 +785,11 @@
    1.82          val permT = mk_permT (Type (atom, []));
    1.83          val pi = Free ("pi", permT);
    1.84        in
    1.85 -        standard (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.86 +        Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.87              (Const ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
    1.88               Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x))))
    1.89            (fn _ => simp_tac (HOL_basic_ss addsimps (perm_defs @ Abs_inverse_thms @
    1.90 -            perm_closed_thms @ Rep_thms)) 1))
    1.91 +            perm_closed_thms @ Rep_thms)) 1)
    1.92        end) Rep_thms;
    1.93  
    1.94      val perm_rep_perm_thms = List.concat (map prove_perm_rep_perm
    1.95 @@ -807,8 +807,8 @@
    1.96      fun prove_distinct_thms (_, []) = []
    1.97        | prove_distinct_thms (p as (rep_thms, dist_lemma), t::ts) =
    1.98            let
    1.99 -            val dist_thm = standard (Goal.prove thy8 [] [] t (fn _ =>
   1.100 -              simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1))
   1.101 +            val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
   1.102 +              simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
   1.103            in dist_thm::(standard (dist_thm RS not_sym))::
   1.104              (prove_distinct_thms (p, ts))
   1.105            end;
   1.106 @@ -849,7 +849,7 @@
   1.107            val (_, l_args, r_args) = foldr constr_arg (1, [], []) dts;
   1.108            val c = Const (cname, map fastype_of l_args ---> T)
   1.109          in
   1.110 -          standard (Goal.prove thy8 [] []
   1.111 +          Goal.prove_global thy8 [] []
   1.112              (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.113                (perm (list_comb (c, l_args)), list_comb (c, r_args))))
   1.114              (fn _ => EVERY
   1.115 @@ -860,7 +860,7 @@
   1.116                   (symmetric perm_fun_def :: abs_perm)) 1),
   1.117                 TRY (simp_tac (HOL_basic_ss addsimps
   1.118                   (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
   1.119 -                    perm_closed_thms)) 1)]))
   1.120 +                    perm_closed_thms)) 1)])
   1.121          end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss))
   1.122        end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
   1.123  
   1.124 @@ -898,7 +898,7 @@
   1.125            val Ts = map fastype_of args1;
   1.126            val c = Const (cname, Ts ---> T)
   1.127          in
   1.128 -          standard (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.129 +          Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.130                (HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)),
   1.131                 foldr1 HOLogic.mk_conj eqs)))
   1.132              (fn _ => EVERY
   1.133 @@ -908,7 +908,7 @@
   1.134                    alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
   1.135                    perm_rep_perm_thms)) 1),
   1.136                  TRY (asm_full_simp_tac (HOL_basic_ss addsimps (perm_fun_def ::
   1.137 -                  expand_fun_eq :: rep_inject_thms @ perm_rep_perm_thms)) 1)]))
   1.138 +                  expand_fun_eq :: rep_inject_thms @ perm_rep_perm_thms)) 1)])
   1.139          end) (constrs ~~ constr_rep_thms)
   1.140        end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
   1.141  
   1.142 @@ -946,7 +946,7 @@
   1.143            fun fresh t =
   1.144              Const ("Nominal.fresh", atomT --> fastype_of t --> HOLogic.boolT) $
   1.145                Free ("a", atomT) $ t;
   1.146 -          val supp_thm = standard (Goal.prove thy8 [] []
   1.147 +          val supp_thm = Goal.prove_global thy8 [] []
   1.148                (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.149                  (supp c,
   1.150                   if null dts then Const ("{}", HOLogic.mk_setT atomT)
   1.151 @@ -955,15 +955,15 @@
   1.152                simp_tac (HOL_basic_ss addsimps (supp_def ::
   1.153                   Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
   1.154                   symmetric empty_def :: Finites.emptyI :: simp_thms @
   1.155 -                 abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1))
   1.156 +                 abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
   1.157          in
   1.158            (supp_thm,
   1.159 -           standard (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.160 +           Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.161                (fresh c,
   1.162                 if null dts then HOLogic.true_const
   1.163                 else foldr1 HOLogic.mk_conj (map fresh args2))))
   1.164               (fn _ =>
   1.165 -               simp_tac (simpset_of thy8 addsimps [fresh_def, supp_thm]) 1)))
   1.166 +               simp_tac (simpset_of thy8 addsimps [fresh_def, supp_thm]) 1))
   1.167          end) atoms) constrs)
   1.168        end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps')));
   1.169  
   1.170 @@ -985,14 +985,14 @@
   1.171      val (indrule_lemma_prems, indrule_lemma_concls) =
   1.172        Library.foldl mk_indrule_lemma (([], []), (descr'' ~~ recTs ~~ recTs'));
   1.173  
   1.174 -    val indrule_lemma = standard (Goal.prove thy8 [] []
   1.175 +    val indrule_lemma = Goal.prove_global thy8 [] []
   1.176        (Logic.mk_implies
   1.177          (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
   1.178           HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
   1.179             [REPEAT (etac conjE 1),
   1.180              REPEAT (EVERY
   1.181                [TRY (rtac conjI 1), full_simp_tac (HOL_basic_ss addsimps Rep_inverse_thms) 1,
   1.182 -               etac mp 1, resolve_tac Rep_thms 1])]));
   1.183 +               etac mp 1, resolve_tac Rep_thms 1])]);
   1.184  
   1.185      val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
   1.186      val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
   1.187 @@ -1003,7 +1003,7 @@
   1.188      val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms;
   1.189  
   1.190      val dt_induct_prop = DatatypeProp.make_ind descr' sorts';
   1.191 -    val dt_induct = standard (Goal.prove thy8 []
   1.192 +    val dt_induct = Goal.prove_global thy8 []
   1.193        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
   1.194        (fn prems => EVERY
   1.195          [rtac indrule_lemma' 1,
   1.196 @@ -1012,7 +1012,7 @@
   1.197             [REPEAT (eresolve_tac Abs_inverse_thms' 1),
   1.198              simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
   1.199              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
   1.200 -                (prems ~~ constr_defs))]));
   1.201 +                (prems ~~ constr_defs))]);
   1.202  
   1.203      val case_names_induct = mk_case_names_induct descr'';
   1.204  
   1.205 @@ -1028,7 +1028,7 @@
   1.206      val finite_supp_thms = map (fn atom =>
   1.207        let val atomT = Type (atom, [])
   1.208        in map standard (List.take
   1.209 -        (split_conj_thm (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop
   1.210 +        (split_conj_thm (Goal.prove_global thy8 [] [] (HOLogic.mk_Trueprop
   1.211             (foldr1 HOLogic.mk_conj (map (fn (s, T) => HOLogic.mk_mem
   1.212               (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T),
   1.213                Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT atomT))))
   1.214 @@ -1258,7 +1258,7 @@
   1.215  
   1.216      val _ = warning "proving strong induction theorem ...";
   1.217  
   1.218 -    val induct_aux = standard (Goal.prove thy9 [] ind_prems' ind_concl'
   1.219 +    val induct_aux = Goal.prove_global thy9 [] ind_prems' ind_concl'
   1.220        (fn prems => EVERY
   1.221          ([mk_subgoal 1 (K (K (K aux_ind_concl))),
   1.222            indtac dt_induct tnames 1] @
   1.223 @@ -1310,7 +1310,7 @@
   1.224                 (constrs ~~ constrs'))) (descr'' ~~ ndescr)) @
   1.225           [REPEAT (eresolve_tac [conjE, allE_Nil] 1),
   1.226            REPEAT (etac allE 1),
   1.227 -          REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac (simpset_of thy9) 1)])));
   1.228 +          REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac (simpset_of thy9) 1)]));
   1.229  
   1.230      val induct_aux' = Thm.instantiate ([],
   1.231        map (fn (s, T) =>
   1.232 @@ -1323,12 +1323,12 @@
   1.233            cterm_of thy9 (Const ("Nominal.supp", fastype_of f')))
   1.234          end) fresh_fs) induct_aux;
   1.235  
   1.236 -    val induct = standard (Goal.prove thy9 [] ind_prems ind_concl
   1.237 +    val induct = Goal.prove_global thy9 [] ind_prems ind_concl
   1.238        (fn prems => EVERY
   1.239           [rtac induct_aux' 1,
   1.240            REPEAT (resolve_tac induct_aux_lemmas 1),
   1.241            REPEAT ((resolve_tac prems THEN_ALL_NEW
   1.242 -            (etac meta_spec ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)]))
   1.243 +            (etac meta_spec ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)])
   1.244  
   1.245      val (_, thy10) = thy9 |>
   1.246        Theory.add_path big_name |>
   1.247 @@ -1430,19 +1430,19 @@
   1.248               HOLogic.mk_mem (HOLogic.mk_prod (mk_perm [] (pi, x), mk_perm [] (pi, y)), R'))
   1.249            end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs));
   1.250          val ths = map (fn th => standard (th RS mp)) (split_conj_thm
   1.251 -          (Goal.prove thy11 [] []
   1.252 +          (Goal.prove_global thy11 [] []
   1.253              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps)))
   1.254              (fn _ => rtac rec_induct 1 THEN REPEAT
   1.255                 (NominalPermeq.perm_simp_tac (simpset_of thy11) 1 THEN
   1.256                  (resolve_tac rec_intrs THEN_ALL_NEW
   1.257                   asm_simp_tac (HOL_ss addsimps (fresh_bij @ perm_bij))) 1))))
   1.258 -        val ths' = map (fn ((P, Q), th) => standard
   1.259 -          (Goal.prove thy11 [] []
   1.260 +        val ths' = map (fn ((P, Q), th) =>
   1.261 +          Goal.prove_global thy11 [] []
   1.262              (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P))
   1.263              (fn _ => dtac (Thm.instantiate ([],
   1.264                   [(cterm_of thy11 (Var (("pi", 0), permT)),
   1.265                     cterm_of thy11 (Const ("List.rev", permT --> permT) $ pi))]) th) 1 THEN
   1.266 -               NominalPermeq.perm_simp_tac HOL_ss 1))) (ps ~~ ths)
   1.267 +               NominalPermeq.perm_simp_tac HOL_ss 1)) (ps ~~ ths)
   1.268        in (ths, ths') end) dt_atomTs);
   1.269  
   1.270      (** finite support **)
   1.271 @@ -1458,7 +1458,7 @@
   1.272              (rec_fns ~~ rec_fn_Ts)
   1.273        in
   1.274          map (fn th => standard (th RS mp)) (split_conj_thm
   1.275 -          (Goal.prove thy11 [] fins
   1.276 +          (Goal.prove_global thy11 [] fins
   1.277              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   1.278                (map (fn (((T, U), R), i) =>
   1.279                   let