src/HOL/Tools/datatype_rep_proofs.ML
changeset 20046 9c8909fc5865
parent 19540 d036bff01c23
child 20071 8f3e1ddb50e6
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Sat Jul 08 12:54:32 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sat Jul 08 12:54:33 2006 +0200
     1.3 @@ -278,20 +278,20 @@
     1.4          val Abs_name = Sign.intern_const sg ("Abs_" ^ s);
     1.5  
     1.6          val inj_Abs_thm = 
     1.7 -	    standard (Goal.prove sg [] []
     1.8 -	      (HOLogic.mk_Trueprop 
     1.9 -		(Const ("Fun.inj_on", [AbsT, UnivT] ---> HOLogic.boolT) $
    1.10 -		 Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT)))
    1.11 -              (fn _ => EVERY [rtac inj_on_inverseI 1, etac thm1 1]));
    1.12 +            Goal.prove_global sg [] []
    1.13 +              (HOLogic.mk_Trueprop 
    1.14 +                (Const ("Fun.inj_on", [AbsT, UnivT] ---> HOLogic.boolT) $
    1.15 +                 Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT)))
    1.16 +              (fn _ => EVERY [rtac inj_on_inverseI 1, etac thm1 1]);
    1.17  
    1.18          val setT = HOLogic.mk_setT T
    1.19  
    1.20          val inj_Rep_thm =
    1.21 -	    standard (Goal.prove sg [] []
    1.22 -	      (HOLogic.mk_Trueprop
    1.23 -		(Const ("Fun.inj_on", [RepT, setT] ---> HOLogic.boolT) $
    1.24 -		 Const (Rep_name, RepT) $ Const ("UNIV", setT)))
    1.25 -              (fn _ => EVERY [rtac inj_inverseI 1, rtac thm2 1]));
    1.26 +            Goal.prove_global sg [] []
    1.27 +              (HOLogic.mk_Trueprop
    1.28 +                (Const ("Fun.inj_on", [RepT, setT] ---> HOLogic.boolT) $
    1.29 +                 Const (Rep_name, RepT) $ Const ("UNIV", setT)))
    1.30 +              (fn _ => EVERY [rtac inj_inverseI 1, rtac thm2 1]);
    1.31  
    1.32        in (inj_Abs_thm, inj_Rep_thm) end;
    1.33  
    1.34 @@ -372,8 +372,8 @@
    1.35          (* prove characteristic equations *)
    1.36  
    1.37          val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
    1.38 -        val char_thms' = map (fn eqn => standard (Goal.prove thy' [] [] eqn
    1.39 -          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))) eqns;
    1.40 +        val char_thms' = map (fn eqn => Goal.prove_global thy' [] [] eqn
    1.41 +          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
    1.42  
    1.43        in (thy', char_thms' @ char_thms) end;
    1.44  
    1.45 @@ -394,12 +394,12 @@
    1.46              val Ts = map (TFree o rpair HOLogic.typeS)
    1.47                (variantlist (replicate i "'t", used));
    1.48              val f = Free ("f", Ts ---> U)
    1.49 -          in standard (Goal.prove sign [] [] (Logic.mk_implies
    1.50 +          in Goal.prove_global sign [] [] (Logic.mk_implies
    1.51              (HOLogic.mk_Trueprop (HOLogic.list_all
    1.52                 (map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))),
    1.53               HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
    1.54                 r $ (a $ app_bnds f i)), f))))
    1.55 -            (fn _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1]))
    1.56 +            (fn _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1])
    1.57            end
    1.58        in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
    1.59  
    1.60 @@ -427,7 +427,7 @@
    1.61          val inj_thms' = map (fn r => r RS injD)
    1.62            (map snd newT_iso_inj_thms @ inj_thms);
    1.63  
    1.64 -        val inj_thm = standard (Goal.prove thy5 [] []
    1.65 +        val inj_thm = Goal.prove_global thy5 [] []
    1.66            (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
    1.67              [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
    1.68               REPEAT (EVERY
    1.69 @@ -447,18 +447,18 @@
    1.70                           REPEAT (eresolve_tac (mp :: allE ::
    1.71                             map make_elim (Suml_inject :: Sumr_inject ::
    1.72                               Lim_inject :: fun_cong :: inj_thms')) 1),
    1.73 -                         atac 1]))])])])]));
    1.74 +                         atac 1]))])])])]);
    1.75  
    1.76          val inj_thms'' = map (fn r => r RS datatype_injI)
    1.77                               (split_conj_thm inj_thm);
    1.78  
    1.79          val elem_thm = 
    1.80 -	    standard (Goal.prove thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
    1.81 -	      (fn _ =>
    1.82 -	       EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
    1.83 -		rewrite_goals_tac rewrites,
    1.84 -		REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
    1.85 -                  ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]));
    1.86 +            Goal.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
    1.87 +              (fn _ =>
    1.88 +               EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
    1.89 +                rewrite_goals_tac rewrites,
    1.90 +                REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
    1.91 +                  ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
    1.92  
    1.93        in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
    1.94        end;
    1.95 @@ -489,7 +489,7 @@
    1.96  
    1.97      val iso_thms = if length descr = 1 then [] else
    1.98        Library.drop (length newTs, split_conj_thm
    1.99 -        (standard (Goal.prove thy5 [] [] iso_t (fn _ => EVERY
   1.100 +        (Goal.prove_global thy5 [] [] iso_t (fn _ => EVERY
   1.101             [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   1.102              REPEAT (rtac TrueI 1),
   1.103              rewrite_goals_tac (mk_meta_eq choice_eq ::
   1.104 @@ -500,7 +500,7 @@
   1.105                   List.concat (map (mk_funs_inv o #1) newT_iso_axms)) 1),
   1.106                 TRY (hyp_subst_tac 1),
   1.107                 rtac (sym RS range_eqI) 1,
   1.108 -               resolve_tac iso_char_thms 1])]))));
   1.109 +               resolve_tac iso_char_thms 1])])));
   1.110  
   1.111      val Abs_inverse_thms' =
   1.112        map #1 newT_iso_axms @
   1.113 @@ -519,12 +519,12 @@
   1.114        let
   1.115          val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
   1.116          val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
   1.117 -      in standard (Goal.prove thy5 [] [] eqn (fn _ => EVERY
   1.118 +      in Goal.prove_global thy5 [] [] eqn (fn _ => EVERY
   1.119          [resolve_tac inj_thms 1,
   1.120           rewrite_goals_tac rewrites,
   1.121           rtac refl 1,
   1.122           resolve_tac rep_intrs 2,
   1.123 -         REPEAT (resolve_tac iso_elem_thms 1)]))
   1.124 +         REPEAT (resolve_tac iso_elem_thms 1)])
   1.125        end;
   1.126  
   1.127      (*--------------------------------------------------------------*)
   1.128 @@ -541,8 +541,8 @@
   1.129      fun prove_distinct_thms (_, []) = []
   1.130        | prove_distinct_thms (dist_rewrites', t::_::ts) =
   1.131            let
   1.132 -            val dist_thm = standard (Goal.prove thy5 [] [] t (fn _ =>
   1.133 -              EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1]))
   1.134 +            val dist_thm = Goal.prove_global thy5 [] [] t (fn _ =>
   1.135 +              EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
   1.136            in dist_thm::(standard (dist_thm RS not_sym))::
   1.137              (prove_distinct_thms (dist_rewrites', ts))
   1.138            end;
   1.139 @@ -562,7 +562,7 @@
   1.140          ((map (fn r => r RS injD) iso_inj_thms) @
   1.141            [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
   1.142             Lim_inject, Suml_inject, Sumr_inject]))
   1.143 -      in standard (Goal.prove thy5 [] [] t (fn _ => EVERY
   1.144 +      in Goal.prove_global thy5 [] [] t (fn _ => EVERY
   1.145          [rtac iffI 1,
   1.146           REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
   1.147           dresolve_tac rep_congs 1, dtac box_equals 1,
   1.148 @@ -570,7 +570,7 @@
   1.149           REPEAT (eresolve_tac inj_thms 1),
   1.150           REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac ext 1),
   1.151             REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1),
   1.152 -           atac 1]))]))
   1.153 +           atac 1]))])
   1.154        end;
   1.155  
   1.156      val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
   1.157 @@ -612,14 +612,14 @@
   1.158  
   1.159      val cert = cterm_of (Theory.sign_of thy6);
   1.160  
   1.161 -    val indrule_lemma = standard (Goal.prove thy6 [] []
   1.162 +    val indrule_lemma = Goal.prove_global thy6 [] []
   1.163        (Logic.mk_implies
   1.164          (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
   1.165           HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
   1.166             [REPEAT (etac conjE 1),
   1.167              REPEAT (EVERY
   1.168                [TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1,
   1.169 -               etac mp 1, resolve_tac iso_elem_thms 1])]));
   1.170 +               etac mp 1, resolve_tac iso_elem_thms 1])]);
   1.171  
   1.172      val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
   1.173      val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
   1.174 @@ -627,7 +627,7 @@
   1.175      val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
   1.176  
   1.177      val dt_induct_prop = DatatypeProp.make_ind descr sorts;
   1.178 -    val dt_induct = standard (Goal.prove thy6 []
   1.179 +    val dt_induct = Goal.prove_global thy6 []
   1.180        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
   1.181        (fn prems => EVERY
   1.182          [rtac indrule_lemma' 1,
   1.183 @@ -636,7 +636,7 @@
   1.184             [REPEAT (eresolve_tac Abs_inverse_thms 1),
   1.185              simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
   1.186              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
   1.187 -                (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]));
   1.188 +                (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
   1.189  
   1.190      val ([dt_induct'], thy7) =
   1.191        thy6