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;
authorwenzelm
Fri Feb 23 13:09:45 2018 +0100 (2018-02-23 ago)
changeset 67701454dfdaf021d
parent 67700 0455834f7817
child 67702 2d9918f5b33c
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;
src/Pure/Isar/element.ML
     1.1 --- a/src/Pure/Isar/element.ML	Thu Feb 22 14:28:05 2018 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Fri Feb 23 13:09:45 2018 +0100
     1.3 @@ -321,18 +321,6 @@
     1.4  
     1.5  end;
     1.6  
     1.7 -
     1.8 -fun compose_witness (Witness (_, th)) r =
     1.9 -  let
    1.10 -    val th' = Goal.conclude th;
    1.11 -    val A = Thm.cprem_of r 1;
    1.12 -  in
    1.13 -    Thm.implies_elim
    1.14 -      (Conv.gconv_rule Drule.beta_eta_conversion 1 r)
    1.15 -      (Conv.fconv_rule Drule.beta_eta_conversion
    1.16 -        (Thm.instantiate (Thm.match (Thm.cprop_of th', A)) th'))
    1.17 -  end;
    1.18 -
    1.19  fun conclude_witness ctxt (Witness (_, th)) =
    1.20    Thm.close_derivation (Raw_Simplifier.norm_hhf_protect ctxt (Goal.conclude th));
    1.21  
    1.22 @@ -354,14 +342,42 @@
    1.23  
    1.24  (* satisfy hypotheses *)
    1.25  
    1.26 +local
    1.27 +
    1.28 +val norm_term = Envir.beta_eta_contract;
    1.29 +val norm_conv = Drule.beta_eta_conversion;
    1.30 +val norm_cterm = Thm.rhs_of o norm_conv;
    1.31 +
    1.32 +fun find_witness witns hyp =
    1.33 +  (case find_first (fn Witness (t, _) => hyp aconv t) witns of
    1.34 +    NONE =>
    1.35 +      let val hyp' = norm_term hyp
    1.36 +      in find_first (fn Witness (t, _) => hyp' aconv norm_term t) witns end
    1.37 +  | some => some);
    1.38 +
    1.39 +fun compose_witness (Witness (_, th)) r =
    1.40 +  let
    1.41 +    val th' = Goal.conclude th;
    1.42 +    val A = Thm.cprem_of r 1;
    1.43 +  in
    1.44 +    Thm.implies_elim
    1.45 +      (Conv.gconv_rule norm_conv 1 r)
    1.46 +      (Conv.fconv_rule norm_conv
    1.47 +        (Thm.instantiate (Thm.match (apply2 norm_cterm (Thm.cprop_of th', A))) th'))
    1.48 +  end;
    1.49 +
    1.50 +in
    1.51 +
    1.52  fun satisfy_thm witns thm =
    1.53 -  thm |> fold (fn hyp =>
    1.54 -    (case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of
    1.55 +  (Thm.chyps_of thm, thm) |-> fold (fn hyp =>
    1.56 +    (case find_witness witns (Thm.term_of hyp) of
    1.57        NONE => I
    1.58 -    | SOME w => Thm.implies_intr hyp #> compose_witness w)) (Thm.chyps_of thm);
    1.59 +    | SOME w => Thm.implies_intr hyp #> compose_witness w));
    1.60  
    1.61  val satisfy_morphism = Morphism.thm_morphism "Element.satisfy" o satisfy_thm;
    1.62  
    1.63 +end;
    1.64 +
    1.65  
    1.66  (* rewriting with equalities *)
    1.67