moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
authorwenzelm
Thu Jul 27 13:43:06 2006 +0200 (2006-07-27)
changeset 20228e0f9e8a6556b
parent 20227 435601e8e53d
child 20229 da4ec4b48be1
moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
src/Pure/goal.ML
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/goal.ML	Thu Jul 27 13:43:05 2006 +0200
     1.2 +++ b/src/Pure/goal.ML	Thu Jul 27 13:43:06 2006 +0200
     1.3 @@ -17,8 +17,6 @@
     1.4    val protect: thm -> thm
     1.5    val conclude: thm -> thm
     1.6    val finish: thm -> thm
     1.7 -  val norm_hhf: thm -> thm
     1.8 -  val norm_hhf_protect: thm -> thm
     1.9    val compose_hhf: thm -> int -> thm -> thm Seq.seq
    1.10    val compose_hhf_tac: thm -> int -> tactic
    1.11    val comp_hhf: thm -> thm -> thm
    1.12 @@ -76,28 +74,6 @@
    1.13  
    1.14  (** results **)
    1.15  
    1.16 -(* HHF normal form: !! before ==>, outermost !! generalized *)
    1.17 -
    1.18 -local
    1.19 -
    1.20 -fun gen_norm_hhf ss =
    1.21 -  (not o Drule.is_norm_hhf o Thm.prop_of) ?
    1.22 -    Drule.fconv_rule (MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) ss)
    1.23 -  #> Thm.adjust_maxidx_thm
    1.24 -  #> Drule.gen_all;
    1.25 -
    1.26 -val ss =
    1.27 -  MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss
    1.28 -    addsimps [Drule.norm_hhf_eq];
    1.29 -
    1.30 -in
    1.31 -
    1.32 -val norm_hhf = gen_norm_hhf ss;
    1.33 -val norm_hhf_protect = gen_norm_hhf (ss addeqcongs [Drule.protect_cong]);
    1.34 -
    1.35 -end;
    1.36 -
    1.37 -
    1.38  (* composition of normal results *)
    1.39  
    1.40  fun compose_hhf tha i thb =
     2.1 --- a/src/Pure/meta_simplifier.ML	Thu Jul 27 13:43:05 2006 +0200
     2.2 +++ b/src/Pure/meta_simplifier.ML	Thu Jul 27 13:43:06 2006 +0200
     2.3 @@ -72,6 +72,8 @@
     2.4    val addSSolver: simpset * solver -> simpset
     2.5    val setSolver: simpset * solver -> simpset
     2.6    val addSolver: simpset * solver -> simpset
     2.7 +  val norm_hhf: thm -> thm
     2.8 +  val norm_hhf_protect: thm -> thm
     2.9  end;
    2.10  
    2.11  signature META_SIMPLIFIER =
    2.12 @@ -1200,6 +1202,26 @@
    2.13    then Drule.fconv_rule (Drule.goals_conv (fn j => j=i) (rewrite_cterm mode prover ss)) thm
    2.14    else raise THM("rewrite_goal_rule",i,[thm]);
    2.15  
    2.16 +
    2.17 +(* HHF normal form: !! before ==>, outermost !! generalized *)
    2.18 +
    2.19 +local
    2.20 +
    2.21 +fun gen_norm_hhf ss =
    2.22 +  (not o Drule.is_norm_hhf o Thm.prop_of) ?
    2.23 +    Drule.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) ss)
    2.24 +  #> Thm.adjust_maxidx_thm
    2.25 +  #> Drule.gen_all;
    2.26 +
    2.27 +val ss = theory_context ProtoPure.thy empty_ss addsimps [Drule.norm_hhf_eq];
    2.28 +
    2.29 +in
    2.30 +
    2.31 +val norm_hhf = gen_norm_hhf ss;
    2.32 +val norm_hhf_protect = gen_norm_hhf (ss addeqcongs [Drule.protect_cong]);
    2.33 +
    2.34 +end;
    2.35 +
    2.36  end;
    2.37  
    2.38  structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;