src/Pure/conv.ML
changeset 36936 c52d1c130898
parent 32843 c8f5a7c8353f
child 38668 e8236c4aff16
     1.1 --- a/src/Pure/conv.ML	Sat May 15 15:31:33 2010 +0200
     1.2 +++ b/src/Pure/conv.ML	Sat May 15 17:59:06 2010 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4  (*  Title:      Pure/conv.ML
     1.5      Author:     Amine Chaieb, TU Muenchen
     1.6 +    Author:     Sascha Boehme, TU Muenchen
     1.7      Author:     Makarius
     1.8  
     1.9  Conversions: primitive equality reasoning.
    1.10 @@ -32,10 +33,16 @@
    1.11    val arg1_conv: conv -> conv
    1.12    val fun2_conv: conv -> conv
    1.13    val binop_conv: conv -> conv
    1.14 +  val binder_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
    1.15    val forall_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
    1.16    val implies_conv: conv -> conv -> conv
    1.17    val implies_concl_conv: conv -> conv
    1.18    val rewr_conv: thm -> conv
    1.19 +  val rewrs_conv: thm list -> conv
    1.20 +  val sub_conv: (Proof.context -> conv) -> Proof.context -> conv
    1.21 +  val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv
    1.22 +  val top_conv: (Proof.context -> conv) -> Proof.context -> conv
    1.23 +  val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv
    1.24    val params_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
    1.25    val prems_conv: int -> conv -> conv
    1.26    val concl_conv: int -> conv -> conv
    1.27 @@ -105,6 +112,29 @@
    1.28  
    1.29  fun binop_conv cv = combination_conv (arg_conv cv) cv;
    1.30  
    1.31 +fun binder_conv cv ctxt = arg_conv (abs_conv cv ctxt);
    1.32 +
    1.33 +
    1.34 +(* subterm structure *)
    1.35 +
    1.36 +(*cf. SUB_CONV in HOL*)
    1.37 +fun sub_conv conv ctxt =
    1.38 +  comb_conv (conv ctxt) else_conv
    1.39 +  abs_conv (conv o snd) ctxt else_conv
    1.40 +  all_conv;
    1.41 +
    1.42 +(*cf. BOTTOM_CONV in HOL*)
    1.43 +fun bottom_conv conv ctxt ct =
    1.44 +  (sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct;
    1.45 +
    1.46 +(*cf. TOP_CONV in HOL*)
    1.47 +fun top_conv conv ctxt ct =
    1.48 +  (conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct;
    1.49 +
    1.50 +(*cf. TOP_SWEEP_CONV in HOL*)
    1.51 +fun top_sweep_conv conv ctxt ct =
    1.52 +  (conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct;
    1.53 +
    1.54  
    1.55  (* primitive logic *)
    1.56  
    1.57 @@ -136,6 +166,8 @@
    1.58        handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
    1.59    end;
    1.60  
    1.61 +fun rewrs_conv rules = first_conv (map rewr_conv rules);
    1.62 +
    1.63  
    1.64  (* conversions on HHF rules *)
    1.65