# HG changeset patch # User wenzelm # Date 1519387785 -3600 # Node ID 454dfdaf021deea7f69b89dba9538dd5992a86aa # Parent 0455834f7817f32979f8d15e744553190772bbf7 more robust normalization of witness, e.g. relevant for proofs of transfer_existence_ivl0, transfer_flow0 in AFP/thys/Ordinary_Differential_Equations/Numerics/Transfer_Euclidean_Space_Vector.thy; diff -r 0455834f7817 -r 454dfdaf021d src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Thu Feb 22 14:28:05 2018 +0100 +++ b/src/Pure/Isar/element.ML Fri Feb 23 13:09:45 2018 +0100 @@ -321,18 +321,6 @@ end; - -fun compose_witness (Witness (_, th)) r = - let - val th' = Goal.conclude th; - val A = Thm.cprem_of r 1; - in - Thm.implies_elim - (Conv.gconv_rule Drule.beta_eta_conversion 1 r) - (Conv.fconv_rule Drule.beta_eta_conversion - (Thm.instantiate (Thm.match (Thm.cprop_of th', A)) th')) - end; - fun conclude_witness ctxt (Witness (_, th)) = Thm.close_derivation (Raw_Simplifier.norm_hhf_protect ctxt (Goal.conclude th)); @@ -354,14 +342,42 @@ (* satisfy hypotheses *) +local + +val norm_term = Envir.beta_eta_contract; +val norm_conv = Drule.beta_eta_conversion; +val norm_cterm = Thm.rhs_of o norm_conv; + +fun find_witness witns hyp = + (case find_first (fn Witness (t, _) => hyp aconv t) witns of + NONE => + let val hyp' = norm_term hyp + in find_first (fn Witness (t, _) => hyp' aconv norm_term t) witns end + | some => some); + +fun compose_witness (Witness (_, th)) r = + let + val th' = Goal.conclude th; + val A = Thm.cprem_of r 1; + in + Thm.implies_elim + (Conv.gconv_rule norm_conv 1 r) + (Conv.fconv_rule norm_conv + (Thm.instantiate (Thm.match (apply2 norm_cterm (Thm.cprop_of th', A))) th')) + end; + +in + fun satisfy_thm witns thm = - thm |> fold (fn hyp => - (case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of + (Thm.chyps_of thm, thm) |-> fold (fn hyp => + (case find_witness witns (Thm.term_of hyp) of NONE => I - | SOME w => Thm.implies_intr hyp #> compose_witness w)) (Thm.chyps_of thm); + | SOME w => Thm.implies_intr hyp #> compose_witness w)); val satisfy_morphism = Morphism.thm_morphism "Element.satisfy" o satisfy_thm; +end; + (* rewriting with equalities *)