src/HOL/Tools/inductive_package.ML
changeset 17985 d5d576b72371
parent 17959 8db36a108213
child 18222 a8ccacce3b52
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Oct 22 01:22:10 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Oct 25 18:18:49 2005 +0200
     1.3 @@ -248,7 +248,7 @@
     1.4    | ap_split _ _ _ _ u =  u;
     1.5  
     1.6  fun mk_tuple p ps (Type ("*", [T1, T2])) (tms as t::_) =
     1.7 -      if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms, 
     1.8 +      if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms,
     1.9          mk_tuple (2::p) ps T2 (Library.drop (length (prodT_factors (1::p) ps T1), tms)))
    1.10        else t
    1.11    | mk_tuple _ _ _ (t::_) = t;
    1.12 @@ -286,7 +286,7 @@
    1.13  
    1.14  val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\"";
    1.15  
    1.16 -val all_not_allowed = 
    1.17 +val all_not_allowed =
    1.18      "Introduction rule must not have a leading \"!!\" quantifier";
    1.19  
    1.20  fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize [];
    1.21 @@ -472,10 +472,11 @@
    1.22  
    1.23  fun prove_mono setT fp_fun monos thy =
    1.24   (message "  Proving monotonicity ...";
    1.25 -  OldGoals.prove_goalw_cterm []      (*NO quick_and_dirty_prove_goalw_cterm here!*)
    1.26 -    (Thm.cterm_of thy (HOLogic.mk_Trueprop
    1.27 -      (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
    1.28 -    (fn _ => [rtac monoI 1, REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)]));
    1.29 +  standard (Goal.prove thy [] []   (*NO quick_and_dirty here!*)
    1.30 +    (HOLogic.mk_Trueprop
    1.31 +      (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun))
    1.32 +    (fn _ => EVERY [rtac monoI 1,
    1.33 +      REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)])));
    1.34  
    1.35  
    1.36  (* prove introduction rules *)
    1.37 @@ -491,20 +492,18 @@
    1.38        | select_disj _ 1 = [rtac disjI1]
    1.39        | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
    1.40  
    1.41 -    val intrs = map (fn (i, intr) => OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
    1.42 -      (Thm.cterm_of thy intr) (fn prems =>
    1.43 -       [(*insert prems and underlying sets*)
    1.44 -       cut_facts_tac prems 1,
    1.45 -       stac unfold 1,
    1.46 -       REPEAT (resolve_tac [vimageI2, CollectI] 1),
    1.47 -       (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
    1.48 -       EVERY1 (select_disj (length intr_ts) i),
    1.49 -       (*Not ares_tac, since refl must be tried before any equality assumptions;
    1.50 -         backtracking may occur if the premises have extra variables!*)
    1.51 -       DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1),
    1.52 -       (*Now solve the equations like Inl 0 = Inl ?b2*)
    1.53 -       REPEAT (rtac refl 1)])
    1.54 -      |> rulify) (1 upto (length intr_ts) ~~ intr_ts)
    1.55 +    val intrs = (1 upto (length intr_ts) ~~ intr_ts) |> map (fn (i, intr) =>
    1.56 +      rulify (standard (SkipProof.prove thy [] [] intr (fn _ => EVERY
    1.57 +       [rewrite_goals_tac rec_sets_defs,
    1.58 +        stac unfold 1,
    1.59 +        REPEAT (resolve_tac [vimageI2, CollectI] 1),
    1.60 +        (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
    1.61 +        EVERY1 (select_disj (length intr_ts) i),
    1.62 +        (*Not ares_tac, since refl must be tried before any equality assumptions;
    1.63 +          backtracking may occur if the premises have extra variables!*)
    1.64 +        DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1),
    1.65 +        (*Now solve the equations like Inl 0 = Inl ?b2*)
    1.66 +        REPEAT (rtac refl 1)]))))
    1.67  
    1.68    in (intrs, unfold) end;
    1.69  
    1.70 @@ -519,13 +518,16 @@
    1.71      val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
    1.72    in
    1.73      mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
    1.74 -      OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
    1.75 -        (Thm.cterm_of thy t) (fn prems =>
    1.76 +      SkipProof.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    1.77 +        (fn prems => EVERY
    1.78            [cut_facts_tac [hd prems] 1,
    1.79 +           rewrite_goals_tac rec_sets_defs,
    1.80             dtac (unfold RS subst) 1,
    1.81             REPEAT (FIRSTGOAL (eresolve_tac rules1)),
    1.82             REPEAT (FIRSTGOAL (eresolve_tac rules2)),
    1.83 -           EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
    1.84 +           EVERY (map (fn prem =>
    1.85 +             DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_sets_defs prem, conjI] 1)) (tl prems))])
    1.86 +        |> standard
    1.87          |> rulify
    1.88          |> RuleCases.name cases)
    1.89    end;
    1.90 @@ -624,9 +626,9 @@
    1.91        mk_indrule cs cTs params intr_ts;
    1.92  
    1.93      val dummy = if !trace then
    1.94 -		(writeln "ind_prems = ";
    1.95 -		 List.app (writeln o Sign.string_of_term thy) ind_prems)
    1.96 -	    else ();
    1.97 +                (writeln "ind_prems = ";
    1.98 +                 List.app (writeln o Sign.string_of_term thy) ind_prems)
    1.99 +            else ();
   1.100  
   1.101      (* make predicate for instantiation of abstract induction rule *)
   1.102  
   1.103 @@ -648,22 +650,24 @@
   1.104      (* simplification rules for vimage and Collect *)
   1.105  
   1.106      val vimage_simps = if length cs < 2 then [] else
   1.107 -      map (fn c => OldGoals.quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of thy
   1.108 +      map (fn c => standard (SkipProof.prove thy [] []
   1.109          (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.110            (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
   1.111             HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
   1.112 -             List.nth (preds, find_index_eq c cs)))))
   1.113 -        (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
   1.114 +             List.nth (preds, find_index_eq c cs))))
   1.115 +        (fn _ => EVERY
   1.116 +          [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1]))) cs;
   1.117  
   1.118      val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
   1.119  
   1.120      val dummy = if !trace then
   1.121 -		(writeln "raw_fp_induct = "; print_thm raw_fp_induct)
   1.122 -	    else ();
   1.123 +                (writeln "raw_fp_induct = "; print_thm raw_fp_induct)
   1.124 +            else ();
   1.125  
   1.126 -    val induct = OldGoals.quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of thy
   1.127 -      (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
   1.128 -        [rtac (impI RS allI) 1,
   1.129 +    val induct = standard (SkipProof.prove thy [] ind_prems ind_concl
   1.130 +      (fn prems => EVERY
   1.131 +        [rewrite_goals_tac [inductive_conj_def],
   1.132 +         rtac (impI RS allI) 1,
   1.133           DETERM (etac raw_fp_induct 1),
   1.134           rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
   1.135           fold_goals_tac rec_sets_defs,
   1.136 @@ -674,16 +678,16 @@
   1.137           REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
   1.138           ALLGOALS (simp_tac (HOL_basic_ss addsimps sum_case_rewrites)),
   1.139           EVERY (map (fn prem =>
   1.140 -   	             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
   1.141 +           DEPTH_SOLVE_1 (ares_tac [rewrite_rule [inductive_conj_def] prem, conjI, refl] 1)) prems)]));
   1.142  
   1.143 -    val lemma = OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of thy
   1.144 -      (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
   1.145 -        [cut_facts_tac prems 1,
   1.146 +    val lemma = standard (SkipProof.prove thy [] []
   1.147 +      (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY
   1.148 +        [rewrite_goals_tac rec_sets_defs,
   1.149           REPEAT (EVERY
   1.150             [REPEAT (resolve_tac [conjI, impI] 1),
   1.151              TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
   1.152              rewrite_goals_tac sum_case_rewrites,
   1.153 -            atac 1])])
   1.154 +            atac 1])]))
   1.155  
   1.156    in standard (split_rule factors (induct RS lemma)) end;
   1.157