src/Tools/coherent.ML
author wenzelm
Tue Jul 21 01:03:18 2009 +0200 (2009-07-21)
changeset 32091 30e2ffbba718
parent 32035 8e77b6a250d5
child 32199 82c4c570310a
permissions -rw-r--r--
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm@30160
     1
(*  Title:      Tools/coherent.ML
berghofe@28326
     2
    Author:     Stefan Berghofer, TU Muenchen
wenzelm@31241
     3
    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen
berghofe@28326
     4
berghofe@28326
     5
Prover for coherent logic, see e.g.
berghofe@28326
     6
berghofe@28326
     7
  Marc Bezem and Thierry Coquand, Automating Coherent Logic, LPAR 2005
berghofe@28326
     8
berghofe@28326
     9
for a description of the algorithm.
berghofe@28326
    10
*)
berghofe@28326
    11
berghofe@28326
    12
signature COHERENT_DATA =
berghofe@28326
    13
sig
berghofe@28326
    14
  val atomize_elimL: thm
berghofe@28326
    15
  val atomize_exL: thm
berghofe@28326
    16
  val atomize_conjL: thm
berghofe@28326
    17
  val atomize_disjL: thm
berghofe@28326
    18
  val operator_names: string list
berghofe@28326
    19
end;
berghofe@28326
    20
berghofe@28326
    21
signature COHERENT =
berghofe@28326
    22
sig
berghofe@28326
    23
  val verbose: bool ref
berghofe@28326
    24
  val show_facts: bool ref
wenzelm@31241
    25
  val coherent_tac: Proof.context -> thm list -> int -> tactic
berghofe@28326
    26
  val setup: theory -> theory
berghofe@28326
    27
end;
berghofe@28326
    28
berghofe@28326
    29
functor CoherentFun(Data: COHERENT_DATA) : COHERENT =
berghofe@28326
    30
struct
berghofe@28326
    31
wenzelm@31241
    32
(** misc tools **)
wenzelm@31241
    33
berghofe@28326
    34
val verbose = ref false;
berghofe@28326
    35
berghofe@28326
    36
fun message f = if !verbose then tracing (f ()) else ();
berghofe@28326
    37
berghofe@28326
    38
datatype cl_prf =
berghofe@28326
    39
  ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list *
berghofe@28326
    40
  int list * (term list * cl_prf) list;
berghofe@28326
    41
wenzelm@29273
    42
val is_atomic = not o exists_Const (member (op =) Data.operator_names o #1);
berghofe@28326
    43
berghofe@28326
    44
local open Conv in
berghofe@28326
    45
berghofe@28326
    46
fun rulify_elim_conv ct =
berghofe@28326
    47
  if is_atomic (Logic.strip_imp_concl (term_of ct)) then all_conv ct
berghofe@28326
    48
  else concl_conv (length (Logic.strip_imp_prems (term_of ct)))
berghofe@28326
    49
    (rewr_conv (symmetric Data.atomize_elimL) then_conv
berghofe@28326
    50
     MetaSimplifier.rewrite true (map symmetric
berghofe@28326
    51
       [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
berghofe@28326
    52
berghofe@28326
    53
end;
berghofe@28326
    54
wenzelm@30552
    55
fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);
berghofe@28326
    56
berghofe@28326
    57
(* Decompose elimination rule of the form
berghofe@28326
    58
   A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P
berghofe@28326
    59
*)
berghofe@28326
    60
fun dest_elim prop =
berghofe@28326
    61
  let
berghofe@28326
    62
    val prems = Logic.strip_imp_prems prop;
berghofe@28326
    63
    val concl = Logic.strip_imp_concl prop;
berghofe@28326
    64
    val (prems1, prems2) =
berghofe@28326
    65
      take_suffix (fn t => Logic.strip_assums_concl t = concl) prems;
berghofe@28326
    66
  in
berghofe@28326
    67
    (prems1,
berghofe@28326
    68
     if null prems2 then [([], [concl])]
berghofe@28326
    69
     else map (fn t =>
berghofe@28326
    70
       (map snd (Logic.strip_params t), Logic.strip_assums_hyp t)) prems2)
berghofe@28326
    71
  end;
berghofe@28326
    72
berghofe@28326
    73
fun mk_rule th =
berghofe@28326
    74
  let
berghofe@28326
    75
    val th' = rulify_elim th;
berghofe@28326
    76
    val (prems, cases) = dest_elim (prop_of th')
berghofe@28326
    77
  in (th', prems, cases) end;
berghofe@28326
    78
berghofe@28326
    79
fun mk_dom ts = fold (fn t =>
berghofe@28326
    80
  Typtab.map_default (fastype_of t, []) (fn us => us @ [t])) ts Typtab.empty;
berghofe@28326
    81
berghofe@28326
    82
val empty_env = (Vartab.empty, Vartab.empty);
berghofe@28326
    83
berghofe@28326
    84
(* Find matcher that makes conjunction valid in given state *)
berghofe@28326
    85
fun valid_conj ctxt facts env [] = Seq.single (env, [])
berghofe@28326
    86
  | valid_conj ctxt facts env (t :: ts) =
berghofe@28326
    87
      Seq.maps (fn (u, x) => Seq.map (apsnd (cons x))
berghofe@28326
    88
        (valid_conj ctxt facts
berghofe@28326
    89
           (Pattern.match (ProofContext.theory_of ctxt) (t, u) env) ts
berghofe@28326
    90
         handle Pattern.MATCH => Seq.empty))
berghofe@28326
    91
          (Seq.of_list (sort (int_ord o pairself snd) (Net.unify_term facts t)));
berghofe@28326
    92
berghofe@28326
    93
(* Instantiate variables that only occur free in conlusion *)
berghofe@28326
    94
fun inst_extra_vars ctxt dom cs =
berghofe@28326
    95
  let
berghofe@28326
    96
    val vs = fold Term.add_vars (maps snd cs) [];
berghofe@28326
    97
    fun insts [] inst = Seq.single inst
berghofe@28326
    98
      | insts ((ixn, T) :: vs') inst = Seq.maps
berghofe@28326
    99
          (fn t => insts vs' (((ixn, T), t) :: inst))
berghofe@28326
   100
          (Seq.of_list (case Typtab.lookup dom T of
berghofe@28326
   101
             NONE => error ("Unknown domain: " ^
berghofe@28326
   102
               Syntax.string_of_typ ctxt T ^ "\nfor term(s) " ^
berghofe@28326
   103
               commas (maps (map (Syntax.string_of_term ctxt) o snd) cs))
berghofe@28326
   104
           | SOME ts => ts))
berghofe@28326
   105
  in Seq.map (fn inst =>
berghofe@28326
   106
    (inst, map (apsnd (map (subst_Vars (map (apfst fst) inst)))) cs))
berghofe@28326
   107
      (insts vs [])
berghofe@28326
   108
  end;
berghofe@28326
   109
berghofe@28326
   110
(* Check whether disjunction is valid in given state *)
berghofe@28326
   111
fun is_valid_disj ctxt facts [] = false
berghofe@28326
   112
  | is_valid_disj ctxt facts ((Ts, ts) :: ds) =
berghofe@31855
   113
      let val vs = map_index (fn (i, T) => Var (("x", i), T)) Ts
berghofe@28326
   114
      in case Seq.pull (valid_conj ctxt facts empty_env
berghofe@31855
   115
        (map (fn t => subst_bounds (rev vs, t)) ts)) of
berghofe@28326
   116
          SOME _ => true
berghofe@28326
   117
        | NONE => is_valid_disj ctxt facts ds
berghofe@28326
   118
      end;
berghofe@28326
   119
berghofe@28326
   120
val show_facts = ref false;
berghofe@28326
   121
berghofe@28326
   122
fun string_of_facts ctxt s facts = space_implode "\n"
berghofe@28326
   123
  (s :: map (Syntax.string_of_term ctxt)
berghofe@28326
   124
     (map fst (sort (int_ord o pairself snd) (Net.content facts)))) ^ "\n\n";
berghofe@28326
   125
berghofe@28326
   126
fun print_facts ctxt facts =
berghofe@28326
   127
  if !show_facts then message (fn () => string_of_facts ctxt "Facts:" facts)
berghofe@28326
   128
  else ();
berghofe@28326
   129
berghofe@28326
   130
fun valid ctxt rules goal dom facts nfacts nparams =
berghofe@28326
   131
  let val seq = Seq.of_list rules |> Seq.maps (fn (th, ps, cs) =>
berghofe@28326
   132
    valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) =>
berghofe@28326
   133
      let val cs' = map (fn (Ts, ts) =>
wenzelm@32035
   134
        (map (Envir.subst_type tye) Ts, map (Envir.subst_term env) ts)) cs
berghofe@28326
   135
      in
berghofe@28326
   136
        inst_extra_vars ctxt dom cs' |>
berghofe@28326
   137
          Seq.map_filter (fn (inst, cs'') =>
berghofe@28326
   138
            if is_valid_disj ctxt facts cs'' then NONE
berghofe@28326
   139
            else SOME (th, env, inst, is, cs''))
berghofe@28326
   140
      end))
berghofe@28326
   141
  in
berghofe@28326
   142
    case Seq.pull seq of
berghofe@28326
   143
      NONE => (tracing (string_of_facts ctxt "Countermodel found:" facts); NONE)
berghofe@28326
   144
    | SOME ((th, env, inst, is, cs), _) =>
berghofe@28326
   145
        if cs = [([], [goal])] then SOME (ClPrf (th, env, inst, is, []))
berghofe@28326
   146
        else
berghofe@28326
   147
          (case valid_cases ctxt rules goal dom facts nfacts nparams cs of
berghofe@28326
   148
             NONE => NONE
berghofe@28326
   149
           | SOME prfs => SOME (ClPrf (th, env, inst, is, prfs)))
berghofe@28326
   150
  end
berghofe@28326
   151
berghofe@28326
   152
and valid_cases ctxt rules goal dom facts nfacts nparams [] = SOME []
berghofe@28326
   153
  | valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) =
berghofe@28326
   154
      let
berghofe@28326
   155
        val _ = message (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts));
berghofe@31855
   156
        val params = map_index (fn (i, T) =>
berghofe@31855
   157
          Free ("par" ^ string_of_int (nparams + i), T)) Ts;
berghofe@28326
   158
        val ts' = map_index (fn (i, t) =>
berghofe@31855
   159
          (subst_bounds (rev params, t), nfacts + i)) ts;
berghofe@28326
   160
        val dom' = fold (fn (T, p) =>
berghofe@28326
   161
          Typtab.map_default (T, []) (fn ps => ps @ [p]))
berghofe@28326
   162
            (Ts ~~ params) dom;
berghofe@28326
   163
        val facts' = fold (fn (t, i) => Net.insert_term op =
berghofe@28326
   164
          (t, (t, i))) ts' facts
berghofe@28326
   165
      in
berghofe@28326
   166
        case valid ctxt rules goal dom' facts'
berghofe@28326
   167
          (nfacts + length ts) (nparams + length Ts) of
berghofe@28326
   168
          NONE => NONE
berghofe@28326
   169
        | SOME prf => (case valid_cases ctxt rules goal dom facts nfacts nparams ds of
berghofe@28326
   170
            NONE => NONE
berghofe@28326
   171
          | SOME prfs => SOME ((params, prf) :: prfs))
berghofe@28326
   172
      end;
berghofe@28326
   173
wenzelm@31241
   174
berghofe@28326
   175
(** proof replaying **)
berghofe@28326
   176
berghofe@28326
   177
fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
berghofe@28326
   178
  let
berghofe@28326
   179
    val _ = message (fn () => space_implode "\n"
wenzelm@32091
   180
      ("asms:" :: map (Display.string_of_thm_global thy) asms) ^ "\n\n");
berghofe@28326
   181
    val th' = Drule.implies_elim_list
berghofe@28326
   182
      (Thm.instantiate
berghofe@28326
   183
         (map (fn (ixn, (S, T)) =>
berghofe@28326
   184
            (Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T))
berghofe@28326
   185
               (Vartab.dest tye),
berghofe@28326
   186
          map (fn (ixn, (T, t)) =>
wenzelm@32035
   187
            (Thm.cterm_of thy (Var (ixn, Envir.subst_type tye T)),
berghofe@28326
   188
             Thm.cterm_of thy t)) (Vartab.dest env) @
berghofe@28326
   189
          map (fn (ixnT, t) =>
berghofe@28326
   190
            (Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th)
berghofe@28326
   191
      (map (nth asms) is);
berghofe@28326
   192
    val (_, cases) = dest_elim (prop_of th')
berghofe@28326
   193
  in
berghofe@28326
   194
    case (cases, prfs) of
berghofe@28326
   195
      ([([], [_])], []) => th'
berghofe@28326
   196
    | ([([], [_])], [([], prf)]) => thm_of_cl_prf thy goal (asms @ [th']) prf
berghofe@28326
   197
    | _ => Drule.implies_elim_list
berghofe@28326
   198
        (Thm.instantiate (Thm.match
berghofe@28326
   199
           (Drule.strip_imp_concl (cprop_of th'), goal)) th')
berghofe@28326
   200
        (map (thm_of_case_prf thy goal asms) (prfs ~~ cases))
berghofe@28326
   201
  end
berghofe@28326
   202
berghofe@28326
   203
and thm_of_case_prf thy goal asms ((params, prf), (_, asms')) =
berghofe@28326
   204
  let
berghofe@28326
   205
    val cparams = map (cterm_of thy) params;
berghofe@28326
   206
    val asms'' = map (cterm_of thy o curry subst_bounds (rev params)) asms'
berghofe@28326
   207
  in
berghofe@28326
   208
    Drule.forall_intr_list cparams (Drule.implies_intr_list asms''
berghofe@28326
   209
      (thm_of_cl_prf thy goal (asms @ map Thm.assume asms'') prf))
berghofe@28326
   210
  end;
berghofe@28326
   211
berghofe@28326
   212
berghofe@28326
   213
(** external interface **)
berghofe@28326
   214
wenzelm@31241
   215
fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context, ...} =>
berghofe@28326
   216
  rtac (rulify_elim_conv concl RS equal_elim_rule2) 1 THEN
berghofe@28326
   217
  SUBPROOF (fn {prems = prems', concl, context, ...} =>
berghofe@28326
   218
    let val xs = map term_of params @
berghofe@28326
   219
      map (fn (_, s) => Free (s, the (Variable.default_type context s)))
berghofe@28326
   220
        (Variable.fixes_of context)
berghofe@28326
   221
    in
berghofe@28326
   222
      case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl)
berghofe@28326
   223
           (mk_dom xs) Net.empty 0 0 of
berghofe@28326
   224
         NONE => no_tac
berghofe@28326
   225
       | SOME prf =>
berghofe@28326
   226
           rtac (thm_of_cl_prf (ProofContext.theory_of context) concl [] prf) 1
berghofe@28339
   227
    end) context 1) ctxt;
berghofe@28326
   228
wenzelm@31241
   229
val setup = Method.setup @{binding coherent}
wenzelm@31241
   230
  (Attrib.thms >> (fn rules => fn ctxt =>
wenzelm@31241
   231
      METHOD (fn facts => HEADGOAL (coherent_tac ctxt (facts @ rules)))))
wenzelm@31241
   232
    "prove coherent formula";
berghofe@28326
   233
berghofe@28326
   234
end;