src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
changeset 58957 c9e744ea8a38
parent 58059 4e477dcd050a
child 59058 a78612c67ec0
     1.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -412,17 +412,17 @@
     1.4      @{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp},
     1.5      @{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}])
     1.6  
     1.7 -  fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = (
     1.8 +  fun nnf_quant_tac ctxt thm (qs as (qs1, qs2)) i st = (
     1.9      rtac thm ORELSE'
    1.10 -    (match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
    1.11 -    (match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
    1.12 +    (match_tac ctxt qs1 THEN' nnf_quant_tac ctxt thm qs) ORELSE'
    1.13 +    (match_tac ctxt qs2 THEN' nnf_quant_tac ctxt thm qs)) i st
    1.14  
    1.15 -  fun nnf_quant_tac_varified vars eq =
    1.16 -    nnf_quant_tac (Old_Z3_Proof_Tools.varify vars eq)
    1.17 +  fun nnf_quant_tac_varified ctxt vars eq =
    1.18 +    nnf_quant_tac ctxt (Old_Z3_Proof_Tools.varify vars eq)
    1.19  
    1.20    fun nnf_quant ctxt vars qs p ct =
    1.21      Old_Z3_Proof_Tools.as_meta_eq ct
    1.22 -    |> Old_Z3_Proof_Tools.by_tac ctxt (nnf_quant_tac_varified vars (meta_eq_of p) qs)
    1.23 +    |> Old_Z3_Proof_Tools.by_tac ctxt (nnf_quant_tac_varified ctxt vars (meta_eq_of p) qs)
    1.24  
    1.25    fun prove_nnf ctxt = try_apply ctxt [] [
    1.26      named ctxt "conj/disj" Old_Z3_Proof_Literals.prove_conj_disj_eq,
    1.27 @@ -555,7 +555,7 @@
    1.28      val thm = meta_eq_of p
    1.29      val rules' = Old_Z3_Proof_Tools.varify vars thm :: rules
    1.30      val cu = Old_Z3_Proof_Tools.as_meta_eq ct
    1.31 -    val tac = REPEAT_ALL_NEW (match_tac rules')
    1.32 +    val tac = REPEAT_ALL_NEW (match_tac ctxt rules')
    1.33    in MetaEq (Old_Z3_Proof_Tools.by_tac ctxt tac cu) end
    1.34  end
    1.35  
    1.36 @@ -577,15 +577,15 @@
    1.37    val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
    1.38    val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
    1.39  
    1.40 -  fun elim_unused_tac i st = (
    1.41 -    match_tac [@{thm refl}]
    1.42 -    ORELSE' (match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
    1.43 +  fun elim_unused_tac ctxt i st = (
    1.44 +    match_tac ctxt [@{thm refl}]
    1.45 +    ORELSE' (match_tac ctxt [elim_all, elim_ex] THEN' elim_unused_tac ctxt)
    1.46      ORELSE' (
    1.47 -      match_tac [@{thm iff_allI}, @{thm iff_exI}]
    1.48 -      THEN' elim_unused_tac)) i st
    1.49 +      match_tac ctxt [@{thm iff_allI}, @{thm iff_exI}]
    1.50 +      THEN' elim_unused_tac ctxt)) i st
    1.51  in
    1.52  
    1.53 -fun elim_unused_vars ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt elim_unused_tac
    1.54 +fun elim_unused_vars ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt (elim_unused_tac ctxt)
    1.55  
    1.56  end
    1.57  
    1.58 @@ -601,7 +601,7 @@
    1.59    val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
    1.60  in
    1.61  fun quant_inst ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt (
    1.62 -  REPEAT_ALL_NEW (match_tac [rule])
    1.63 +  REPEAT_ALL_NEW (match_tac ctxt [rule])
    1.64    THEN' rtac @{thm excluded_middle})
    1.65  end
    1.66