src/HOL/Library/cconv.ML
author wenzelm
Mon Dec 28 01:28:28 2015 +0100 (2015-12-28)
changeset 61945 1135b8de26c3
parent 60642 48dd1cefb4ae
child 69593 3dda49e08b9d
permissions -rw-r--r--
more symbols;
     1 (*  Title:      HOL/Library/cconv.ML
     2     Author:     Christoph Traut, Lars Noschinski, TU Muenchen
     3 
     4 FIXME!?
     5 *)
     6 
     7 infix 1 then_cconv
     8 infix 0 else_cconv
     9 
    10 type cconv = conv
    11 
    12 signature BASIC_CCONV =
    13 sig
    14   val then_cconv: cconv * cconv -> cconv
    15   val else_cconv: cconv * cconv -> cconv
    16   val CCONVERSION: cconv -> int -> tactic
    17 end
    18 
    19 signature CCONV =
    20 sig
    21   include BASIC_CCONV
    22   val no_cconv: cconv
    23   val all_cconv: cconv
    24   val first_cconv: cconv list -> cconv
    25   val abs_cconv: (cterm * Proof.context -> cconv) -> Proof.context -> cconv
    26   val combination_cconv: cconv -> cconv -> cconv
    27   val comb_cconv: cconv -> cconv
    28   val arg_cconv: cconv -> cconv
    29   val fun_cconv: cconv -> cconv
    30   val arg1_cconv: cconv -> cconv
    31   val fun2_cconv: cconv -> cconv
    32   val rewr_cconv: thm -> cconv
    33   val rewrs_cconv: thm list -> cconv
    34   val params_cconv: int -> (Proof.context -> cconv) -> Proof.context -> cconv
    35   val prems_cconv: int -> cconv -> cconv
    36   val with_prems_cconv: int -> cconv -> cconv
    37   val concl_cconv: int -> cconv -> cconv
    38   val fconv_rule: cconv -> thm -> thm
    39   val gconv_rule: cconv -> int -> thm -> thm
    40 end
    41 
    42 structure CConv : CCONV =
    43 struct
    44 
    45 val concl_lhs_of = Thm.cprop_of #> Drule.strip_imp_concl #> Thm.dest_equals_lhs
    46 val concl_rhs_of = Thm.cprop_of #> Drule.strip_imp_concl #> Thm.dest_equals_rhs
    47 
    48 fun transitive th1 th2 = Drule.transitive_thm OF [th1, th2]
    49 
    50 val combination_thm =
    51   let
    52     val fg = @{cprop "f :: 'a :: {} \<Rightarrow> 'b :: {} \<equiv> g"}
    53     val st = @{cprop "s :: 'a :: {} \<equiv> t"}
    54     val thm = Thm.combination (Thm.assume fg) (Thm.assume st)
    55       |> Thm.implies_intr st
    56       |> Thm.implies_intr fg
    57   in Drule.export_without_context thm end
    58 
    59 fun abstract_rule_thm n =
    60   let
    61     val eq = @{cprop "\<And>x :: 'a :: {}. (s :: 'a \<Rightarrow> 'b :: {}) x \<equiv> t x"}
    62     val x = @{cterm "x :: 'a :: {}"}
    63     val thm = eq
    64       |> Thm.assume
    65       |> Thm.forall_elim x
    66       |> Thm.abstract_rule n x
    67       |> Thm.implies_intr eq
    68   in Drule.export_without_context thm end
    69 
    70 val no_cconv = Conv.no_conv
    71 val all_cconv = Conv.all_conv
    72 
    73 fun (cv1 else_cconv cv2) ct =
    74   (cv1 ct
    75     handle THM _ => cv2 ct
    76       | CTERM _ => cv2 ct
    77       | TERM _ => cv2 ct
    78       | TYPE _ => cv2 ct)
    79 
    80 fun (cv1 then_cconv cv2) ct =
    81   let
    82     val eq1 = cv1 ct
    83     val eq2 = cv2 (concl_rhs_of eq1)
    84   in
    85     if Thm.is_reflexive eq1 then eq2
    86     else if Thm.is_reflexive eq2 then eq1
    87     else transitive eq1 eq2
    88   end
    89 
    90 fun first_cconv cvs = fold_rev (curry op else_cconv) cvs no_cconv
    91 
    92 fun rewr_cconv rule ct =
    93   let
    94     val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule
    95     val lhs = concl_lhs_of rule1
    96     val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1
    97     val rule3 = Thm.instantiate (Thm.match (lhs, ct)) rule2
    98                 handle Pattern.MATCH => raise CTERM ("rewr_cconv", [lhs, ct])
    99     val concl = rule3 |> Thm.cprop_of |> Drule.strip_imp_concl
   100     val rule4 =
   101       if Thm.dest_equals_lhs concl aconvc ct then rule3
   102       else let val ceq = Thm.dest_fun2 concl
   103            in rule3 RS Thm.trivial (Thm.mk_binop ceq ct (Thm.dest_equals_rhs concl)) end
   104   in
   105     transitive rule4 (Thm.beta_conversion true (concl_rhs_of rule4))
   106   end
   107 
   108 fun rewrs_cconv rules = first_cconv (map rewr_cconv rules)
   109 
   110 fun combination_cconv cv1 cv2 cterm =
   111   let val (l, r) = Thm.dest_comb cterm
   112   in combination_thm OF [cv1 l, cv2 r] end
   113 
   114 fun comb_cconv cv = combination_cconv cv cv
   115 
   116 fun fun_cconv conversion =
   117   combination_cconv conversion all_cconv
   118 
   119 fun arg_cconv conversion =
   120   combination_cconv all_cconv conversion
   121 
   122 fun abs_cconv cv ctxt ct =
   123   (case Thm.term_of ct of
   124      Abs (x, _, _) =>
   125        let
   126          (* Instantiate the rule properly and apply it to the eq theorem. *)
   127          fun abstract_rule u v eq =
   128            let
   129              (* Take a variable v and an equality theorem of form:
   130                   P1 \<Longrightarrow> ... \<Longrightarrow> Pn \<Longrightarrow> L v \<equiv> R v
   131                 And build a term of form:
   132                   \<And>v. (\<lambda>x. L x) v \<equiv> (\<lambda>x. R x) v *)
   133              fun mk_concl var eq =
   134                let
   135                  val certify = Thm.cterm_of ctxt
   136                  fun abs term = (Term.lambda var term) $ var
   137                  fun equals_cong f t =
   138                    Logic.dest_equals t
   139                    |> (fn (a, b) => (f a, f b))
   140                    |> Logic.mk_equals
   141                in
   142                  Thm.concl_of eq
   143                  |> equals_cong abs
   144                  |> Logic.all var |> certify
   145                end
   146              val rule = abstract_rule_thm x
   147              val inst = Thm.match (Drule.cprems_of rule |> hd, mk_concl (Thm.term_of v) eq)
   148            in
   149              (Drule.instantiate_normalize inst rule OF [Drule.generalize ([], [u]) eq])
   150              |> Drule.zero_var_indexes
   151            end
   152 
   153          (* Destruct the abstraction and apply the conversion. *)
   154          val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt
   155          val (v, ct') = Thm.dest_abs (SOME u) ct
   156          val eq = cv (v, ctxt') ct'
   157        in
   158          if Thm.is_reflexive eq
   159          then all_cconv ct
   160          else abstract_rule u v eq
   161        end
   162    | _ => raise CTERM ("abs_cconv", [ct]))
   163 
   164 val arg1_cconv = fun_cconv o arg_cconv
   165 val fun2_cconv = fun_cconv o fun_cconv
   166 
   167 (* conversions on HHF rules *)
   168 
   169 (*rewrite B in \<And>x1 ... xn. B*)
   170 fun params_cconv n cv ctxt ct =
   171   if n <> 0 andalso Logic.is_all (Thm.term_of ct)
   172   then arg_cconv (abs_cconv (params_cconv (n - 1) cv o #2) ctxt) ct
   173   else cv ctxt ct
   174 
   175 (* TODO: This code behaves not exactly like Conv.prems_cconv does.
   176          Fix this! *)
   177 (*rewrite the A's in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
   178 fun prems_cconv 0 cv ct = cv ct
   179   | prems_cconv n cv ct =
   180       (case ct |> Thm.term_of of
   181         (Const (@{const_name "Pure.imp"}, _) $ _) $ _ =>
   182           ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
   183       | _ =>  cv ct)
   184 
   185 fun inst_imp_cong ct = Thm.instantiate ([], [((("A", 0), propT), ct)]) Drule.imp_cong
   186 
   187 (*rewrite B in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
   188 fun concl_cconv 0 cv ct = cv ct
   189   | concl_cconv n cv ct =
   190       (case try Thm.dest_implies ct of
   191         NONE => cv ct
   192       | SOME (A,B) => (concl_cconv (n-1) cv B) RS inst_imp_cong A)
   193 
   194 (* Rewrites A in A \<Longrightarrow> A1 \<Longrightarrow> An \<Longrightarrow> B.
   195    The premises of the resulting theorem assume A1, ..., An
   196    *)
   197 fun with_prems_cconv n cv ct =
   198   let
   199     fun strip_prems 0 As B = (As, B)
   200       | strip_prems i As B =
   201           case try Thm.dest_implies B of
   202             NONE => (As, B)
   203           | SOME (A,B) => strip_prems (i - 1) (A::As) B
   204     val (prem, (prems, concl)) = ct |> Thm.dest_implies ||> strip_prems n [] 
   205     val rewr_imp_concl = Thm.instantiate ([], [((("C", 0), propT), concl)]) @{thm rewr_imp}
   206     val th1 = cv prem RS rewr_imp_concl
   207     val nprems = Thm.nprems_of th1
   208     fun inst_cut_rl ct = Thm.instantiate ([], [((("psi", 0), propT), ct)]) cut_rl
   209     fun f p th = (th RS inst_cut_rl p)
   210       |> Conv.fconv_rule (Conv.concl_conv nprems (Conv.rewr_conv @{thm imp_cong_eq}))
   211   in fold f prems th1 end
   212 
   213 (*forward conversion, cf. FCONV_RULE in LCF*)
   214 fun fconv_rule cv th =
   215   let
   216     val eq = cv (Thm.cprop_of th)
   217   in
   218     if Thm.is_reflexive eq then th
   219     else th COMP (Thm.permute_prems 0 (Thm.nprems_of eq) (eq RS Drule.equal_elim_rule1))
   220   end
   221 
   222 (*goal conversion*)
   223 fun gconv_rule cv i th =
   224   (case try (Thm.cprem_of th) i of
   225     SOME ct =>
   226       let
   227         val eq = cv ct
   228 
   229         (* Drule.with_subgoal assumes that there are no new premises generated
   230            and thus rotates the premises wrongly. *)
   231         fun with_subgoal i f thm =
   232           let
   233             val num_prems = Thm.nprems_of thm
   234             val rotate_to_front = rotate_prems (i - 1)
   235             fun rotate_back thm = rotate_prems (1 - i + num_prems - Thm.nprems_of thm) thm
   236           in
   237             thm |> rotate_to_front |> f |> rotate_back
   238           end
   239       in
   240         if Thm.is_reflexive eq then th
   241         else with_subgoal i (fconv_rule (arg1_cconv (K eq))) th
   242       end
   243   | NONE => raise THM ("gconv_rule", i, [th]))
   244 
   245 (* Conditional conversions as tactics. *)
   246 fun CCONVERSION cv i st = Seq.single (gconv_rule cv i st)
   247   handle THM _ => Seq.empty
   248        | CTERM _ => Seq.empty
   249        | TERM _ => Seq.empty
   250        | TYPE _ => Seq.empty
   251 
   252 end
   253 
   254 structure Basic_CConv: BASIC_CCONV = CConv
   255 open Basic_CConv