src/Pure/conv.ML
changeset 22937 08cf9aaf3aa1
parent 22926 fb6917e426da
child 23034 b3a6815754d6
equal deleted inserted replaced
22936:284b56463da8 22937:08cf9aaf3aa1
     3     Author:     Amine Chaieb and Makarius
     3     Author:     Amine Chaieb and Makarius
     4 
     4 
     5 Conversions: primitive equality reasoning.
     5 Conversions: primitive equality reasoning.
     6 *)
     6 *)
     7 
     7 
     8 infix 1 thenc;
     8 infix 1 then_conv;
     9 infix 0 orelsec;
     9 infix 0 else_conv;
    10 
    10 
    11 signature CONV =
    11 signature CONV =
    12 sig
    12 sig
    13   type conv = cterm -> thm
    13   type conv = cterm -> thm
    14   val no_conv: conv
    14   val no_conv: conv
    15   val all_conv: conv
    15   val all_conv: conv
    16   val thenc: conv * conv -> conv
    16   val then_conv: conv * conv -> conv
    17   val orelsec: conv * conv -> conv
    17   val else_conv: conv * conv -> conv
    18   val first_conv: conv list -> conv
    18   val first_conv: conv list -> conv
    19   val every_conv: conv list -> conv
    19   val every_conv: conv list -> conv
    20   val tryc: conv -> conv
    20   val try_conv: conv -> conv
    21   val repeatc: conv -> conv
    21   val repeat_conv: conv -> conv
    22   val cache_conv: conv -> conv
    22   val cache_conv: conv -> conv
    23   val abs_conv: conv -> conv
    23   val abs_conv: conv -> conv
    24   val combination_conv: conv -> conv -> conv
    24   val combination_conv: conv -> conv -> conv
    25   val comb_conv: conv -> conv
    25   val comb_conv: conv -> conv
    26   val arg_conv: conv -> conv
    26   val arg_conv: conv -> conv
    44 fun no_conv _ = raise CTERM ("no conversion", []);
    44 fun no_conv _ = raise CTERM ("no conversion", []);
    45 val all_conv = Thm.reflexive;
    45 val all_conv = Thm.reflexive;
    46 
    46 
    47 val is_refl = op aconv o Logic.dest_equals o Thm.prop_of;
    47 val is_refl = op aconv o Logic.dest_equals o Thm.prop_of;
    48 
    48 
    49 fun (cv1 thenc cv2) ct =
    49 fun (cv1 then_conv cv2) ct =
    50   let
    50   let
    51     val eq1 = cv1 ct;
    51     val eq1 = cv1 ct;
    52     val eq2 = cv2 (Thm.rhs_of eq1);
    52     val eq2 = cv2 (Thm.rhs_of eq1);
    53   in
    53   in
    54     if is_refl eq1 then eq2
    54     if is_refl eq1 then eq2
    55     else if is_refl eq2 then eq1
    55     else if is_refl eq2 then eq1
    56     else Thm.transitive eq1 eq2
    56     else Thm.transitive eq1 eq2
    57   end;
    57   end;
    58 
    58 
    59 fun (cv1 orelsec cv2) ct =
    59 fun (cv1 else_conv cv2) ct =
    60   (case try cv1 ct of SOME eq => eq | NONE => cv2 ct);
    60   (case try cv1 ct of SOME eq => eq | NONE => cv2 ct);
    61 
    61 
    62 fun first_conv cvs = fold_rev (curry op orelsec) cvs no_conv;
    62 fun first_conv cvs = fold_rev (curry op else_conv) cvs no_conv;
    63 fun every_conv cvs = fold_rev (curry op thenc) cvs all_conv;
    63 fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv;
    64 
    64 
    65 fun tryc cv = cv orelsec all_conv;
    65 fun try_conv cv = cv else_conv all_conv;
    66 fun repeatc cv ct = tryc (cv thenc repeatc cv) ct;
    66 fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct;
    67 
    67 
    68 fun cache_conv cv =
    68 fun cache_conv cv =
    69   let
    69   let
    70     val cache = ref Termtab.empty;
    70     val cache = ref Termtab.empty;
    71     fun conv ct =
    71     fun conv ct =