norm_hhf: no normalization of protected props;
authorwenzelm
Wed Nov 16 17:45:26 2005 +0100 (2005-11-16)
changeset 18180db712213504d
parent 18179 cf4b265007bf
child 18181 644d3e609db8
norm_hhf: no normalization of protected props;
src/Pure/goal.ML
     1.1 --- a/src/Pure/goal.ML	Wed Nov 16 17:45:25 2005 +0100
     1.2 +++ b/src/Pure/goal.ML	Wed Nov 16 17:45:26 2005 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4    val conclude: thm -> thm
     1.5    val finish: thm -> thm
     1.6    val norm_hhf: thm -> thm
     1.7 +  val norm_hhf': thm -> thm
     1.8    val compose_hhf: thm -> int -> thm -> thm Seq.seq
     1.9    val compose_hhf_tac: thm -> int -> tactic
    1.10    val comp_hhf: thm -> thm -> thm
    1.11 @@ -74,12 +75,22 @@
    1.12  
    1.13  (* HHF normal form *)
    1.14  
    1.15 -val norm_hhf =
    1.16 +val norm_hhf_ss =
    1.17 +  MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss
    1.18 +    addsimps [Drule.norm_hhf_eq];
    1.19 +
    1.20 +val norm_hhf_ss' = norm_hhf_ss addeqcongs [Drule.protect_cong];
    1.21 +
    1.22 +fun gen_norm_hhf protected =
    1.23    (not o Drule.is_norm_hhf o Thm.prop_of) ?
    1.24 -    MetaSimplifier.simplify_aux (K (K NONE)) true [Drule.norm_hhf_eq]
    1.25 +    Drule.fconv_rule (MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE))
    1.26 +      (if protected then norm_hhf_ss else norm_hhf_ss'))
    1.27    #> Thm.adjust_maxidx_thm
    1.28    #> Drule.gen_all;
    1.29  
    1.30 +val norm_hhf = gen_norm_hhf true;
    1.31 +val norm_hhf' = gen_norm_hhf false;
    1.32 +
    1.33  
    1.34  (* composition of normal results *)
    1.35