proper context;
authorwenzelm
Tue Jun 04 15:14:19 2019 +0200 (6 weeks ago)
changeset 7031934bc296374ee
parent 70318 9eff9e2dc177
child 70320 59258a3192bf
proper context;
src/HOL/Tools/Function/partial_function.ML
     1.1 --- a/src/HOL/Tools/Function/partial_function.ML	Tue Jun 04 15:11:29 2019 +0200
     1.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Tue Jun 04 15:14:19 2019 +0200
     1.3 @@ -169,17 +169,16 @@
     1.4      val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
     1.5      val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0))
     1.6    in
     1.7 -    (* FIXME ctxt vs. ctxt' (!?) *)
     1.8      rule
     1.9 -    |> infer_instantiate' ctxt
    1.10 -      ((map o Option.map) (Thm.cterm_of ctxt) [SOME uncurry, NONE, SOME curry, NONE, SOME P_inst])
    1.11 -    |> Tactic.rule_by_tactic ctxt
    1.12 -      (Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 (* discharge U (C f) = f *)
    1.13 -       THEN Simplifier.simp_tac (put_simpset curry_K_ss ctxt) 4 (* simplify bot case *)
    1.14 -       THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 5) (* simplify induction step *)
    1.15 +    |> infer_instantiate' ctxt'
    1.16 +      ((map o Option.map) (Thm.cterm_of ctxt') [SOME uncurry, NONE, SOME curry, NONE, SOME P_inst])
    1.17 +    |> Tactic.rule_by_tactic ctxt'
    1.18 +      (Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt') 3 (* discharge U (C f) = f *)
    1.19 +       THEN Simplifier.simp_tac (put_simpset curry_K_ss ctxt') 4 (* simplify bot case *)
    1.20 +       THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt') 5) (* simplify induction step *)
    1.21      |> (fn thm => thm OF [mono_thm, f_def])
    1.22      |> Conv.fconv_rule (Conv.concl_conv ~1    (* simplify conclusion *)
    1.23 -         (Raw_Simplifier.rewrite ctxt false [mk_meta_eq @{thm Product_Type.curry_case_prod}]))
    1.24 +         (Raw_Simplifier.rewrite ctxt' false [mk_meta_eq @{thm Product_Type.curry_case_prod}]))
    1.25      |> singleton (Variable.export ctxt' ctxt)
    1.26    end
    1.27  
    1.28 @@ -192,8 +191,7 @@
    1.29        Conv.every_conv (replicate (length args - 1) (Conv.rewr_conv @{thm split_paired_all}))
    1.30  
    1.31      val split_params_conv =
    1.32 -      Conv.params_conv ~1 (fn ctxt' =>
    1.33 -        Conv.implies_conv split_paired_all_conv Conv.all_conv)
    1.34 +      Conv.params_conv ~1 (fn _ => Conv.implies_conv split_paired_all_conv Conv.all_conv)
    1.35  
    1.36      val (P_var, x_var) =
    1.37         Thm.prop_of inst_rule |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop
    1.38 @@ -205,13 +203,13 @@
    1.39      val P_inst = cert (uncurry_n (length args) (Free (P, PT)))
    1.40  
    1.41      val inst_rule' = inst_rule
    1.42 -      |> Tactic.rule_by_tactic ctxt
    1.43 -        (Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 4
    1.44 -         THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3
    1.45 -         THEN CONVERSION (split_params_conv ctxt
    1.46 -           then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt)) 3)
    1.47 +      |> Tactic.rule_by_tactic ctxt'
    1.48 +        (Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt') 4
    1.49 +         THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt') 3
    1.50 +         THEN CONVERSION (split_params_conv ctxt'
    1.51 +           then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt')) 3)
    1.52        |> Thm.instantiate ([], [(P_var, P_inst), (x_var, x_inst)])
    1.53 -      |> Simplifier.full_simplify (put_simpset split_conv_ss ctxt)
    1.54 +      |> Simplifier.full_simplify (put_simpset split_conv_ss ctxt')
    1.55        |> singleton (Variable.export ctxt' ctxt)
    1.56    in
    1.57      inst_rule'