src/HOL/Tools/datatype_rep_proofs.ML
changeset 17985 d5d576b72371
parent 17959 8db36a108213
child 18314 4595eb4627fa
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Sat Oct 22 01:22:10 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Oct 25 18:18:49 2005 +0200
     1.3 @@ -279,22 +279,20 @@
     1.4          val Abs_name = Sign.intern_const sg ("Abs_" ^ s);
     1.5  
     1.6          val inj_Abs_thm = 
     1.7 -	    OldGoals.prove_goalw_cterm [] 
     1.8 -	      (cterm_of sg
     1.9 -	       (HOLogic.mk_Trueprop 
    1.10 +	    standard (Goal.prove sg [] []
    1.11 +	      (HOLogic.mk_Trueprop 
    1.12  		(Const ("Fun.inj_on", [AbsT, UnivT] ---> HOLogic.boolT) $
    1.13 -		 Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT))))
    1.14 -              (fn _ => [rtac inj_on_inverseI 1, etac thm1 1]);
    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 -	    OldGoals.prove_goalw_cterm []
    1.22 -	      (cterm_of sg
    1.23 -	       (HOLogic.mk_Trueprop
    1.24 +	    standard (Goal.prove sg [] []
    1.25 +	      (HOLogic.mk_Trueprop
    1.26  		(Const ("Fun.inj_on", [RepT, setT] ---> HOLogic.boolT) $
    1.27 -		 Const (Rep_name, RepT) $ Const ("UNIV", setT))))
    1.28 -              (fn _ => [rtac inj_inverseI 1, rtac thm2 1])
    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 @@ -375,8 +373,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 => OldGoals.prove_goalw_cterm rewrites
    1.39 -          (cterm_of (Theory.sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns;
    1.40 +        val char_thms' = map (fn eqn => standard (Goal.prove 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 @@ -397,13 +395,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 OldGoals.prove_goalw_cterm [] (cterm_of sign (Logic.mk_implies
    1.50 +          in standard (Goal.prove 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))))) (fn prems =>
    1.55 -                 [cut_facts_tac prems 1, REPEAT (rtac ext 1),
    1.56 -                  REPEAT (etac allE 1), rtac thm 1, atac 1])
    1.57 +               r $ (a $ app_bnds f i)), f))))
    1.58 +            (fn _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1]))
    1.59            end
    1.60        in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
    1.61  
    1.62 @@ -431,8 +428,8 @@
    1.63          val inj_thms' = map (fn r => r RS injD)
    1.64            (map snd newT_iso_inj_thms @ inj_thms);
    1.65  
    1.66 -        val inj_thm = OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
    1.67 -          (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
    1.68 +        val inj_thm = standard (Goal.prove thy5 [] []
    1.69 +          (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
    1.70              [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
    1.71               REPEAT (EVERY
    1.72                 [rtac allI 1, rtac impI 1,
    1.73 @@ -451,20 +448,18 @@
    1.74                           REPEAT (eresolve_tac (mp :: allE ::
    1.75                             map make_elim (Suml_inject :: Sumr_inject ::
    1.76                               Lim_inject :: fun_cong :: inj_thms')) 1),
    1.77 -                         atac 1]))])])])]);
    1.78 +                         atac 1]))])])])]));
    1.79  
    1.80          val inj_thms'' = map (fn r => r RS datatype_injI)
    1.81                               (split_conj_thm inj_thm);
    1.82  
    1.83          val elem_thm = 
    1.84 -	    OldGoals.prove_goalw_cterm []
    1.85 -	      (cterm_of (Theory.sign_of thy5)
    1.86 -	       (HOLogic.mk_Trueprop (mk_conj ind_concl2)))
    1.87 +	    standard (Goal.prove thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
    1.88  	      (fn _ =>
    1.89 -	       [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
    1.90 +	       EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
    1.91  		rewrite_goals_tac rewrites,
    1.92  		REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
    1.93 -                  ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
    1.94 +                  ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]));
    1.95  
    1.96        in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
    1.97        end;
    1.98 @@ -495,7 +490,7 @@
    1.99  
   1.100      val iso_thms = if length descr = 1 then [] else
   1.101        Library.drop (length newTs, split_conj_thm
   1.102 -        (OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ =>
   1.103 +        (standard (Goal.prove thy5 [] [] iso_t (fn _ => EVERY
   1.104             [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   1.105              REPEAT (rtac TrueI 1),
   1.106              rewrite_goals_tac (mk_meta_eq choice_eq ::
   1.107 @@ -506,7 +501,7 @@
   1.108                   List.concat (map (mk_funs_inv o #1) newT_iso_axms)) 1),
   1.109                 TRY (hyp_subst_tac 1),
   1.110                 rtac (sym RS range_eqI) 1,
   1.111 -               resolve_tac iso_char_thms 1])])));
   1.112 +               resolve_tac iso_char_thms 1])]))));
   1.113  
   1.114      val Abs_inverse_thms' =
   1.115        map #1 newT_iso_axms @
   1.116 @@ -525,12 +520,12 @@
   1.117        let
   1.118          val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
   1.119          val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
   1.120 -      in OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) eqn) (fn _ =>
   1.121 +      in standard (Goal.prove thy5 [] [] eqn (fn _ => EVERY
   1.122          [resolve_tac inj_thms 1,
   1.123           rewrite_goals_tac rewrites,
   1.124           rtac refl 1,
   1.125           resolve_tac rep_intrs 2,
   1.126 -         REPEAT (resolve_tac iso_elem_thms 1)])
   1.127 +         REPEAT (resolve_tac iso_elem_thms 1)]))
   1.128        end;
   1.129  
   1.130      (*--------------------------------------------------------------*)
   1.131 @@ -547,8 +542,8 @@
   1.132      fun prove_distinct_thms (_, []) = []
   1.133        | prove_distinct_thms (dist_rewrites', t::_::ts) =
   1.134            let
   1.135 -            val dist_thm = OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
   1.136 -              [simp_tac (HOL_ss addsimps dist_rewrites') 1])
   1.137 +            val dist_thm = standard (Goal.prove thy5 [] [] t (fn _ =>
   1.138 +              EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1]))
   1.139            in dist_thm::(standard (dist_thm RS not_sym))::
   1.140              (prove_distinct_thms (dist_rewrites', ts))
   1.141            end;
   1.142 @@ -568,7 +563,7 @@
   1.143          ((map (fn r => r RS injD) iso_inj_thms) @
   1.144            [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
   1.145             Lim_inject, Suml_inject, Sumr_inject]))
   1.146 -      in OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
   1.147 +      in standard (Goal.prove thy5 [] [] t (fn _ => EVERY
   1.148          [rtac iffI 1,
   1.149           REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
   1.150           dresolve_tac rep_congs 1, dtac box_equals 1,
   1.151 @@ -576,7 +571,7 @@
   1.152           REPEAT (eresolve_tac inj_thms 1),
   1.153           REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac ext 1),
   1.154             REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1),
   1.155 -           atac 1]))])
   1.156 +           atac 1]))]))
   1.157        end;
   1.158  
   1.159      val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
   1.160 @@ -616,29 +611,31 @@
   1.161  
   1.162      val cert = cterm_of (Theory.sign_of thy6);
   1.163  
   1.164 -    val indrule_lemma = OldGoals.prove_goalw_cterm [] (cert
   1.165 +    val indrule_lemma = standard (Goal.prove thy6 [] []
   1.166        (Logic.mk_implies
   1.167          (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
   1.168 -         HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls)))) (fn prems =>
   1.169 -           [cut_facts_tac prems 1, REPEAT (etac conjE 1),
   1.170 +         HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
   1.171 +           [REPEAT (etac conjE 1),
   1.172              REPEAT (EVERY
   1.173                [TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1,
   1.174 -               etac mp 1, resolve_tac iso_elem_thms 1])]);
   1.175 +               etac mp 1, resolve_tac iso_elem_thms 1])]));
   1.176  
   1.177      val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
   1.178      val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
   1.179        map (Free o apfst fst o dest_Var) Ps;
   1.180      val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
   1.181  
   1.182 -    val dt_induct = OldGoals.prove_goalw_cterm [] (cert
   1.183 -      (DatatypeProp.make_ind descr sorts)) (fn prems =>
   1.184 +    val dt_induct_prop = DatatypeProp.make_ind descr sorts;
   1.185 +    val dt_induct = standard (Goal.prove thy6 []
   1.186 +      (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
   1.187 +      (fn prems => EVERY
   1.188          [rtac indrule_lemma' 1,
   1.189           (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   1.190           EVERY (map (fn (prem, r) => (EVERY
   1.191             [REPEAT (eresolve_tac Abs_inverse_thms 1),
   1.192              simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
   1.193              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
   1.194 -                (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
   1.195 +                (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]));
   1.196  
   1.197      val (thy7, [dt_induct']) = thy6 |>
   1.198        Theory.add_path big_name |>