src/HOL/HOLCF/Tools/Domain/domain_induction.ML
changeset 42793 88bee9f6eec7
parent 42375 774df7c59508
child 44080 53d95b52954c
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Fri May 13 16:03:03 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Fri May 13 22:55:00 2011 +0200
     1.3 @@ -150,7 +150,7 @@
     1.4                (Ps ~~ take_consts ~~ xs)
     1.5        val goal = mk_trp (foldr1 mk_conj concls)
     1.6  
     1.7 -      fun tacf {prems, context} =
     1.8 +      fun tacf {prems, context = ctxt} =
     1.9          let
    1.10            (* Prove stronger prems, without definedness side conditions *)
    1.11            fun con_thm p (con, args) =
    1.12 @@ -165,23 +165,23 @@
    1.13                    map arg_tac args @
    1.14                    [REPEAT (rtac impI 1), ALLGOALS simplify]
    1.15              in
    1.16 -              Goal.prove context [] [] subgoal (K (EVERY tacs))
    1.17 +              Goal.prove ctxt [] [] subgoal (K (EVERY tacs))
    1.18              end
    1.19            fun eq_thms (p, cons) = map (con_thm p) cons
    1.20            val conss = map #con_specs constr_infos
    1.21            val prems' = maps eq_thms (Ps ~~ conss)
    1.22  
    1.23            val tacs1 = [
    1.24 -            quant_tac context 1,
    1.25 +            quant_tac ctxt 1,
    1.26              simp_tac HOL_ss 1,
    1.27 -            InductTacs.induct_tac context [[SOME "n"]] 1,
    1.28 +            InductTacs.induct_tac ctxt [[SOME "n"]] 1,
    1.29              simp_tac (take_ss addsimps prems) 1,
    1.30 -            TRY (safe_tac HOL_cs)]
    1.31 +            TRY (safe_tac (put_claset HOL_cs ctxt))]
    1.32            fun con_tac _ = 
    1.33              asm_simp_tac take_ss 1 THEN
    1.34              (resolve_tac prems' THEN_ALL_NEW etac spec) 1
    1.35            fun cases_tacs (cons, exhaust) =
    1.36 -            res_inst_tac context [(("y", 0), "x")] exhaust 1 ::
    1.37 +            res_inst_tac ctxt [(("y", 0), "x")] exhaust 1 ::
    1.38              asm_simp_tac (take_ss addsimps prems) 1 ::
    1.39              map con_tac cons
    1.40            val tacs = tacs1 @ maps cases_tacs (conss ~~ exhausts)
    1.41 @@ -196,15 +196,15 @@
    1.42        val concls = map (op $) (Ps ~~ xs)
    1.43        val goal = mk_trp (foldr1 mk_conj concls)
    1.44        val adms = if is_finite then [] else map (mk_trp o mk_adm) Ps
    1.45 -      fun tacf {prems, context} =
    1.46 +      fun tacf {prems, context = ctxt} =
    1.47          let
    1.48            fun finite_tac (take_induct, fin_ind) =
    1.49                rtac take_induct 1 THEN
    1.50                (if is_finite then all_tac else resolve_tac prems 1) THEN
    1.51                (rtac fin_ind THEN_ALL_NEW solve_tac prems) 1
    1.52 -          val fin_inds = Project_Rule.projections context finite_ind
    1.53 +          val fin_inds = Project_Rule.projections ctxt finite_ind
    1.54          in
    1.55 -          TRY (safe_tac HOL_cs) THEN
    1.56 +          TRY (safe_tac (put_claset HOL_cs ctxt)) THEN
    1.57            EVERY (map finite_tac (take_induct_thms ~~ fin_inds))
    1.58          end
    1.59      in Goal.prove_global thy [] (adms @ assms) goal tacf end
    1.60 @@ -318,18 +318,18 @@
    1.61        val goal =
    1.62            mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts)))
    1.63        val rules = @{thm Rep_cfun_strict1} :: take_0_thms
    1.64 -      fun tacf {prems, context} =
    1.65 +      fun tacf {prems, context = ctxt} =
    1.66          let
    1.67            val prem' = rewrite_rule [bisim_def_thm] (hd prems)
    1.68 -          val prems' = Project_Rule.projections context prem'
    1.69 +          val prems' = Project_Rule.projections ctxt prem'
    1.70            val dests = map (fn th => th RS spec RS spec RS mp) prems'
    1.71            fun one_tac (dest, rews) =
    1.72 -              dtac dest 1 THEN safe_tac HOL_cs THEN
    1.73 +              dtac dest 1 THEN safe_tac (put_claset HOL_cs ctxt) THEN
    1.74                ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps rews))
    1.75          in
    1.76            rtac @{thm nat.induct} 1 THEN
    1.77            simp_tac (HOL_ss addsimps rules) 1 THEN
    1.78 -          safe_tac HOL_cs THEN
    1.79 +          safe_tac (put_claset HOL_cs ctxt) THEN
    1.80            EVERY (map one_tac (dests ~~ take_rews))
    1.81          end
    1.82      in