src/Pure/conv.ML
changeset 26571 114da911bc41
parent 26130 03a7cfed5e9e
child 27332 94790a9620c3
     1.1 --- a/src/Pure/conv.ML	Mon Apr 07 21:25:21 2008 +0200
     1.2 +++ b/src/Pure/conv.ML	Mon Apr 07 21:25:22 2008 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    val every_conv: conv list -> conv
     1.5    val try_conv: conv -> conv
     1.6    val repeat_conv: conv -> conv
     1.7 -  val abs_conv: (Proof.context -> conv) -> Proof.context -> conv
     1.8 +  val abs_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
     1.9    val combination_conv: conv -> conv -> conv
    1.10    val comb_conv: conv -> conv
    1.11    val arg_conv: conv -> conv
    1.12 @@ -26,9 +26,13 @@
    1.13    val arg1_conv: conv -> conv
    1.14    val fun2_conv: conv -> conv
    1.15    val binop_conv: conv -> conv
    1.16 -  val forall_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
    1.17 +  val forall_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
    1.18 +  val implies_conv: conv -> conv -> conv
    1.19 +  val implies_concl_conv: conv -> conv
    1.20 +  val rewr_conv: thm -> conv
    1.21 +  val params_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
    1.22 +  val prems_conv: int -> conv -> conv
    1.23    val concl_conv: int -> conv -> conv
    1.24 -  val prems_conv: int -> conv -> conv
    1.25    val fconv_rule: conv -> thm -> thm
    1.26    val gconv_rule: conv -> int -> thm -> thm
    1.27  end;
    1.28 @@ -76,7 +80,7 @@
    1.29        let
    1.30          val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt;
    1.31          val (v, ct') = Thm.dest_abs (SOME u) ct;
    1.32 -        val eq = cv ctxt' ct';
    1.33 +        val eq = cv (v, ctxt') ct';
    1.34        in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end
    1.35    | _ => raise CTERM ("abs_conv", [ct]));
    1.36  
    1.37 @@ -94,14 +98,52 @@
    1.38  fun binop_conv cv = combination_conv (arg_conv cv) cv;
    1.39  
    1.40  
    1.41 -(* logic *)
    1.42 +(* primitive logic *)
    1.43 +
    1.44 +fun forall_conv cv ctxt ct =
    1.45 +  (case Thm.term_of ct of
    1.46 +    Const ("all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct
    1.47 +  | _ => raise CTERM ("forall_conv", [ct]));
    1.48 +
    1.49 +fun implies_conv cv1 cv2 ct =
    1.50 +  (case Thm.term_of ct of
    1.51 +    Const ("==>", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct
    1.52 +  | _ => raise CTERM ("implies_conv", [ct]));
    1.53 +
    1.54 +fun implies_concl_conv cv ct =
    1.55 +  (case Thm.term_of ct of
    1.56 +    Const ("==>", _) $ _ $ _ => arg_conv cv ct
    1.57 +  | _ => raise CTERM ("implies_concl_conv", [ct]));
    1.58 +
    1.59 +
    1.60 +(* single rewrite step, cf. REWR_CONV in HOL *)
    1.61 +
    1.62 +fun rewr_conv rule ct =
    1.63 +  let
    1.64 +    val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
    1.65 +    val lhs = Thm.lhs_of rule1;
    1.66 +    val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
    1.67 +  in
    1.68 +    Drule.instantiate (Thm.match (lhs, ct)) rule2
    1.69 +      handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
    1.70 +  end;
    1.71 +
    1.72 +
    1.73 +(* conversions on HHF rules *)
    1.74  
    1.75  (*rewrite B in !!x1 ... xn. B*)
    1.76 -fun forall_conv n cv ctxt ct =
    1.77 +fun params_conv n cv ctxt ct =
    1.78    if n <> 0 andalso can Logic.dest_all (Thm.term_of ct)
    1.79 -  then arg_conv (abs_conv (forall_conv (n - 1) cv) ctxt) ct
    1.80 +  then arg_conv (abs_conv (params_conv (n - 1) cv o #2) ctxt) ct
    1.81    else cv ctxt ct;
    1.82  
    1.83 +(*rewrite the A's in A1 ==> ... ==> An ==> B*)
    1.84 +fun prems_conv 0 _ ct = all_conv ct
    1.85 +  | prems_conv n cv ct =
    1.86 +      (case try Thm.dest_implies ct of
    1.87 +        NONE => all_conv ct
    1.88 +      | SOME (A, B) => Drule.imp_cong_rule (cv A) (prems_conv (n - 1) cv B));
    1.89 +
    1.90  (*rewrite B in A1 ==> ... ==> An ==> B*)
    1.91  fun concl_conv 0 cv ct = cv ct
    1.92    | concl_conv n cv ct =
    1.93 @@ -109,15 +151,8 @@
    1.94          NONE => cv ct
    1.95        | SOME (A, B) => Drule.imp_cong_rule (all_conv A) (concl_conv (n - 1) cv B));
    1.96  
    1.97 -(*rewrite the A's in A1 ==> ... ==> An ==> B*)
    1.98 -fun prems_conv 0 _ ct = all_conv ct
    1.99 -  | prems_conv n cv ct =
   1.100 -      (case try Thm.dest_implies ct of
   1.101 -        NONE => all_conv ct
   1.102 -      | SOME (A, B) => Drule.imp_cong_rule (cv A) (prems_conv (n - 1) cv B));
   1.103  
   1.104 -
   1.105 -(* conversions as rules *)
   1.106 +(* conversions as inference rules *)
   1.107  
   1.108  (*forward conversion, cf. FCONV_RULE in LCF*)
   1.109  fun fconv_rule cv th =