prove_global: pass context;
authorwenzelm
Thu Apr 17 22:22:21 2008 +0200 (2008-04-17 ago)
changeset 267113a478bfa1650
parent 26710 f79aa228c582
child 26712 e2dcda7b0401
prove_global: pass context;
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/simpdata.ML
src/HOLCF/Tools/domain/domain_theorems.ML
src/Provers/splitter.ML
src/Pure/Isar/skip_proof.ML
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Apr 17 22:22:19 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Apr 17 22:22:21 2008 +0200
     1.3 @@ -311,8 +311,7 @@
     1.4        in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
     1.5  
     1.6      fun mk_ind_proof thy thss =
     1.7 -      let val ctxt = ProofContext.init thy
     1.8 -      in Goal.prove_global thy [] prems' concl' (fn ihyps =>
     1.9 +      Goal.prove_global thy [] prems' concl' (fn {prems = ihyps, context = ctxt} =>
    1.10          let val th = Goal.prove ctxt [] [] concl (fn {context, ...} =>
    1.11            rtac raw_induct 1 THEN
    1.12            EVERY (maps (fn ((((_, bvars, oprems, _), vc_compat_ths), ihyp), (vs, ihypt)) =>
    1.13 @@ -404,8 +403,7 @@
    1.14            REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
    1.15              etac impE 1 THEN atac 1 THEN REPEAT (etac allE_Nil 1) THEN
    1.16              asm_full_simp_tac (simpset_of thy) 1)
    1.17 -        end)
    1.18 -      end;
    1.19 +        end);
    1.20  
    1.21      (** strong case analysis rule **)
    1.22  
    1.23 @@ -460,8 +458,8 @@
    1.24  
    1.25      fun mk_cases_proof thy ((((name, thss), elim), (prem, args, concl, prems)),
    1.26          prems') =
    1.27 -      let val ctxt1 = ProofContext.init thy
    1.28 -      in (name, Goal.prove_global thy [] (prem :: prems') concl (fn hyp :: hyps =>
    1.29 +      (name, Goal.prove_global thy [] (prem :: prems') concl
    1.30 +        (fn {prems = hyp :: hyps, context = ctxt1} =>
    1.31          EVERY (rtac (hyp RS elim) 1 ::
    1.32            map (fn (((_, vc_compat_ths), case_hyp), (_, qs, is, _)) =>
    1.33              SUBPROOF (fn {prems = case_hyps, params, context = ctxt2, concl, ...} =>
    1.34 @@ -534,7 +532,6 @@
    1.35                    val final = ProofContext.export ctxt3 ctxt2 [th]
    1.36                  in resolve_tac final 1 end) ctxt1 1)
    1.37                    (thss ~~ hyps ~~ prems))))
    1.38 -      end
    1.39  
    1.40    in
    1.41      thy |>
     2.1 --- a/src/HOL/Nominal/nominal_package.ML	Thu Apr 17 22:22:19 2008 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_package.ML	Thu Apr 17 22:22:21 2008 +0200
     2.3 @@ -1049,7 +1049,7 @@
     2.4      val dt_induct_prop = DatatypeProp.make_ind descr' sorts';
     2.5      val dt_induct = Goal.prove_global thy8 []
     2.6        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
     2.7 -      (fn prems => EVERY
     2.8 +      (fn {prems, ...} => EVERY
     2.9          [rtac indrule_lemma' 1,
    2.10           (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    2.11           EVERY (map (fn (prem, r) => (EVERY
    2.12 @@ -1270,7 +1270,7 @@
    2.13  
    2.14      val _ = warning "proving strong induction theorem ...";
    2.15  
    2.16 -    val induct_aux = Goal.prove_global thy9 [] ind_prems' ind_concl' (fn prems =>
    2.17 +    val induct_aux = Goal.prove_global thy9 [] ind_prems' ind_concl' (fn {prems, context} =>
    2.18        let
    2.19          val (prems1, prems2) = chop (length dt_atomTs) prems;
    2.20          val ind_ss2 = HOL_ss addsimps
    2.21 @@ -1283,7 +1283,7 @@
    2.22            fin_set_fresh @ calc_atm;
    2.23          val ind_ss5 = HOL_basic_ss addsimps pt1_atoms;
    2.24          val ind_ss6 = HOL_basic_ss addsimps flat perm_simps';
    2.25 -        val th = Goal.prove (ProofContext.init thy9) [] [] aux_ind_concl
    2.26 +        val th = Goal.prove context [] [] aux_ind_concl
    2.27            (fn {context = context1, ...} =>
    2.28               EVERY (indtac dt_induct tnames 1 ::
    2.29                 maps (fn ((_, (_, _, constrs)), (_, constrs')) =>
    2.30 @@ -1369,7 +1369,7 @@
    2.31          end) fresh_fs) induct_aux;
    2.32  
    2.33      val induct = Goal.prove_global thy9 [] ind_prems ind_concl
    2.34 -      (fn prems => EVERY
    2.35 +      (fn {prems, ...} => EVERY
    2.36           [rtac induct_aux' 1,
    2.37            REPEAT (resolve_tac fs_atoms 1),
    2.38            REPEAT ((resolve_tac prems THEN_ALL_NEW
    2.39 @@ -1552,7 +1552,8 @@
    2.40                     HOLogic.mk_imp (R $ x $ y,
    2.41                       finite $ (Const ("Nominal.supp", U --> aset) $ y))
    2.42                   end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ (1 upto length recTs)))))
    2.43 -            (fn fins => (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT
    2.44 +            (fn {prems = fins, ...} =>
    2.45 +              (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT
    2.46                 (NominalPermeq.finite_guess_tac (HOL_ss addsimps [fs_name]) 1))))
    2.47        end) dt_atomTs;
    2.48  
    2.49 @@ -1992,7 +1993,7 @@
    2.50            (resolve_tac prems THEN_ALL_NEW atac)
    2.51        in
    2.52          Goal.prove_global thy12 [] prems' concl'
    2.53 -          (fn prems => EVERY
    2.54 +          (fn {prems, ...} => EVERY
    2.55              [rewrite_goals_tac reccomb_defs,
    2.56               rtac the1_equality 1,
    2.57               solve rec_unique_thms prems 1,
     3.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Apr 17 22:22:19 2008 +0200
     3.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Apr 17 22:22:21 2008 +0200
     3.3 @@ -71,7 +71,7 @@
     3.4  
     3.5        in
     3.6          SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
     3.7 -          (fn prems => EVERY
     3.8 +          (fn {prems, ...} => EVERY
     3.9              [rtac induct' 1,
    3.10               REPEAT (rtac TrueI 1),
    3.11               REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
    3.12 @@ -383,7 +383,7 @@
    3.13    let
    3.14      fun prove_weak_case_cong t =
    3.15         SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    3.16 -         (fn prems => EVERY [rtac ((hd prems) RS arg_cong) 1])
    3.17 +         (fn {prems, ...} => EVERY [rtac ((hd prems) RS arg_cong) 1])
    3.18  
    3.19      val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs
    3.20        new_type_names descr sorts thy)
    3.21 @@ -426,7 +426,7 @@
    3.22            [(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy'
    3.23        in
    3.24          SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    3.25 -          (fn prems => 
    3.26 +          (fn {prems, ...} => 
    3.27              let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites))
    3.28              in EVERY [simp_tac (HOL_ss addsimps [hd prems]) 1,
    3.29                  cut_facts_tac [nchotomy''] 1,
     4.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Apr 17 22:22:19 2008 +0200
     4.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Apr 17 22:22:21 2008 +0200
     4.3 @@ -607,7 +607,7 @@
     4.4      val dt_induct_prop = DatatypeProp.make_ind descr sorts;
     4.5      val dt_induct = SkipProof.prove_global thy6 []
     4.6        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
     4.7 -      (fn prems => EVERY
     4.8 +      (fn {prems, ...} => EVERY
     4.9          [rtac indrule_lemma' 1,
    4.10           (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    4.11           EVERY (map (fn (prem, r) => (EVERY
     5.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Apr 17 22:22:19 2008 +0200
     5.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Apr 17 22:22:21 2008 +0200
     5.3 @@ -391,7 +391,7 @@
     5.4            (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
     5.5          val rews = map mk_meta_eq
     5.6            (fst_conv :: snd_conv :: get #rec_thms dt_info);
     5.7 -        val thm = Goal.prove_global thy [] prems concl (fn prems => EVERY
     5.8 +        val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
     5.9            [rtac (#raw_induct ind_info) 1,
    5.10             rewrite_goals_tac rews,
    5.11             REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
    5.12 @@ -450,7 +450,7 @@
    5.13          val rlz' = strip_all (Logic.unvarify rlz);
    5.14          val rews = map mk_meta_eq case_thms;
    5.15          val thm = Goal.prove_global thy []
    5.16 -          (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn prems => EVERY
    5.17 +          (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY
    5.18            [cut_facts_tac [hd prems] 1,
    5.19             etac elimR 1,
    5.20             ALLGOALS (asm_simp_tac HOL_basic_ss),
     6.1 --- a/src/HOL/simpdata.ML	Thu Apr 17 22:22:19 2008 +0200
     6.2 +++ b/src/HOL/simpdata.ML	Thu Apr 17 22:22:21 2008 +0200
     6.3 @@ -73,7 +73,7 @@
     6.4        in Goal.prove_global (Thm.theory_of_thm st) []
     6.5          [mk_simp_implies (Logic.mk_equals (x, y))]
     6.6          (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
     6.7 -        (fn prems => EVERY
     6.8 +        (fn {prems, ...} => EVERY
     6.9           [rewrite_goals_tac @{thms simp_implies_def},
    6.10            REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
    6.11              map (rewrite_rule @{thms simp_implies_def}) prems) 1)])
     7.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Thu Apr 17 22:22:19 2008 +0200
     7.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Thu Apr 17 22:22:21 2008 +0200
     7.3 @@ -84,7 +84,7 @@
     7.4      val t' = legacy_infer_term thy t;
     7.5      val asms = Logic.strip_imp_prems t';
     7.6      val prop = Logic.strip_imp_concl t';
     7.7 -    fun tac prems =
     7.8 +    fun tac {prems, context} =
     7.9        rewrite_goals_tac defs THEN
    7.10        EVERY (tacs (map (rewrite_rule defs) prems));
    7.11    in Goal.prove_global thy [] asms prop tac end;
     8.1 --- a/src/Provers/splitter.ML	Thu Apr 17 22:22:19 2008 +0200
     8.2 +++ b/src/Provers/splitter.ML	Thu Apr 17 22:22:21 2008 +0200
     8.3 @@ -105,7 +105,7 @@
     8.4  val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
     8.5    [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
     8.6    (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
     8.7 -  (fn [prem] => rewtac prem THEN rtac reflexive_thm 1)
     8.8 +  (fn {prems = [prem], ...} => rewtac prem THEN rtac reflexive_thm 1)
     8.9  
    8.10  val trlift = lift RS transitive_thm;
    8.11  val _ $ (P $ _) $ _ = concl_of trlift;
     9.1 --- a/src/Pure/Isar/skip_proof.ML	Thu Apr 17 22:22:19 2008 +0200
     9.2 +++ b/src/Pure/Isar/skip_proof.ML	Thu Apr 17 22:22:21 2008 +0200
     9.3 @@ -12,7 +12,7 @@
     9.4    val prove: Proof.context -> string list -> term list -> term ->
     9.5      ({prems: thm list, context: Proof.context} -> tactic) -> thm
     9.6    val prove_global: theory -> string list -> term list -> term ->
     9.7 -    (thm list -> tactic) -> thm
     9.8 +    ({prems: thm list, context: Proof.context} -> tactic) -> thm
     9.9  end;
    9.10  
    9.11  structure SkipProof: SKIP_PROOF =
    9.12 @@ -45,6 +45,6 @@
    9.13      else tac args st);
    9.14  
    9.15  fun prove_global thy xs asms prop tac =
    9.16 -  Drule.standard (prove (ProofContext.init thy) xs asms prop (fn {prems, ...} => tac prems));
    9.17 +  Drule.standard (prove (ProofContext.init thy) xs asms prop tac);
    9.18  
    9.19  end;