src/Tools/coherent.ML
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 67522 9e712280cc37
permissions -rw-r--r--
more strict AFP properties;
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
wenzelm@55632
    23
  val trace: bool Config.T
wenzelm@31241
    24
  val coherent_tac: Proof.context -> thm list -> int -> tactic
berghofe@28326
    25
end;
berghofe@28326
    26
wenzelm@32734
    27
functor Coherent(Data: COHERENT_DATA) : COHERENT =
berghofe@28326
    28
struct
berghofe@28326
    29
wenzelm@31241
    30
(** misc tools **)
wenzelm@31241
    31
wenzelm@67149
    32
val (trace, trace_setup) = Attrib.config_bool \<^binding>\<open>coherent_trace\<close> (K false);
wenzelm@55632
    33
fun cond_trace ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ();
berghofe@28326
    34
berghofe@28326
    35
datatype cl_prf =
berghofe@28326
    36
  ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list *
berghofe@28326
    37
  int list * (term list * cl_prf) list;
berghofe@28326
    38
wenzelm@29273
    39
val is_atomic = not o exists_Const (member (op =) Data.operator_names o #1);
berghofe@28326
    40
wenzelm@54742
    41
fun rulify_elim_conv ctxt ct =
wenzelm@59582
    42
  if is_atomic (Logic.strip_imp_concl (Thm.term_of ct)) then Conv.all_conv ct
wenzelm@59582
    43
  else Conv.concl_conv (length (Logic.strip_imp_prems (Thm.term_of ct)))
wenzelm@36946
    44
    (Conv.rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv
wenzelm@54742
    45
     Raw_Simplifier.rewrite ctxt true (map Thm.symmetric
berghofe@28326
    46
       [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
berghofe@28326
    47
wenzelm@54883
    48
fun rulify_elim ctxt th = Simplifier.norm_hhf ctxt (Conv.fconv_rule (rulify_elim_conv ctxt) th);
berghofe@28326
    49
berghofe@28326
    50
(* Decompose elimination rule of the form
berghofe@28326
    51
   A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P
berghofe@28326
    52
*)
berghofe@28326
    53
fun dest_elim prop =
berghofe@28326
    54
  let
berghofe@28326
    55
    val prems = Logic.strip_imp_prems prop;
berghofe@28326
    56
    val concl = Logic.strip_imp_concl prop;
wenzelm@67522
    57
    val (prems1, prems2) = chop_suffix (fn t => Logic.strip_assums_concl t = concl) prems;
berghofe@28326
    58
  in
berghofe@28326
    59
    (prems1,
berghofe@28326
    60
     if null prems2 then [([], [concl])]
berghofe@28326
    61
     else map (fn t =>
berghofe@28326
    62
       (map snd (Logic.strip_params t), Logic.strip_assums_hyp t)) prems2)
berghofe@28326
    63
  end;
berghofe@28326
    64
wenzelm@54742
    65
fun mk_rule ctxt th =
berghofe@28326
    66
  let
wenzelm@54742
    67
    val th' = rulify_elim ctxt th;
wenzelm@59582
    68
    val (prems, cases) = dest_elim (Thm.prop_of th')
berghofe@28326
    69
  in (th', prems, cases) end;
berghofe@28326
    70
berghofe@28326
    71
fun mk_dom ts = fold (fn t =>
berghofe@28326
    72
  Typtab.map_default (fastype_of t, []) (fn us => us @ [t])) ts Typtab.empty;
berghofe@28326
    73
berghofe@28326
    74
val empty_env = (Vartab.empty, Vartab.empty);
berghofe@28326
    75
berghofe@28326
    76
(* Find matcher that makes conjunction valid in given state *)
wenzelm@55631
    77
fun valid_conj _ _ env [] = Seq.single (env, [])
berghofe@28326
    78
  | valid_conj ctxt facts env (t :: ts) =
berghofe@28326
    79
      Seq.maps (fn (u, x) => Seq.map (apsnd (cons x))
berghofe@28326
    80
        (valid_conj ctxt facts
wenzelm@42361
    81
           (Pattern.match (Proof_Context.theory_of ctxt) (t, u) env) ts
berghofe@28326
    82
         handle Pattern.MATCH => Seq.empty))
wenzelm@59058
    83
          (Seq.of_list (sort (int_ord o apply2 snd) (Net.unify_term facts t)));
berghofe@28326
    84
berghofe@28326
    85
(* Instantiate variables that only occur free in conlusion *)
berghofe@28326
    86
fun inst_extra_vars ctxt dom cs =
berghofe@28326
    87
  let
berghofe@28326
    88
    val vs = fold Term.add_vars (maps snd cs) [];
berghofe@28326
    89
    fun insts [] inst = Seq.single inst
wenzelm@55627
    90
      | insts ((ixn, T) :: vs') inst =
wenzelm@55627
    91
          Seq.maps (fn t => insts vs' (((ixn, T), t) :: inst))
wenzelm@55627
    92
            (Seq.of_list
wenzelm@55627
    93
              (case Typtab.lookup dom T of
wenzelm@55627
    94
                NONE =>
wenzelm@55627
    95
                  error ("Unknown domain: " ^
wenzelm@55627
    96
                    Syntax.string_of_typ ctxt T ^ "\nfor term(s) " ^
wenzelm@55627
    97
                    commas (maps (map (Syntax.string_of_term ctxt) o snd) cs))
wenzelm@55627
    98
              | SOME ts => ts))
wenzelm@55627
    99
  in
wenzelm@55627
   100
    Seq.map (fn inst =>
wenzelm@55627
   101
      (inst, map (apsnd (map (subst_Vars (map (apfst fst) inst)))) cs))
wenzelm@55627
   102
        (insts vs [])
berghofe@28326
   103
  end;
berghofe@28326
   104
berghofe@28326
   105
(* Check whether disjunction is valid in given state *)
wenzelm@55631
   106
fun is_valid_disj _ _ [] = false
berghofe@28326
   107
  | is_valid_disj ctxt facts ((Ts, ts) :: ds) =
wenzelm@55627
   108
      let val vs = map_index (fn (i, T) => Var (("x", i), T)) Ts in
wenzelm@55627
   109
        (case Seq.pull (valid_conj ctxt facts empty_env
wenzelm@55627
   110
            (map (fn t => subst_bounds (rev vs, t)) ts)) of
berghofe@28326
   111
          SOME _ => true
wenzelm@55627
   112
        | NONE => is_valid_disj ctxt facts ds)
berghofe@28326
   113
      end;
berghofe@28326
   114
wenzelm@55627
   115
fun string_of_facts ctxt s facts =
wenzelm@55634
   116
  Pretty.string_of (Pretty.big_list s
wenzelm@59058
   117
    (map (Syntax.pretty_term ctxt) (map fst (sort (int_ord o apply2 snd) (Net.content facts)))));
berghofe@28326
   118
berghofe@28326
   119
fun valid ctxt rules goal dom facts nfacts nparams =
wenzelm@55627
   120
  let
wenzelm@55627
   121
    val seq =
wenzelm@55627
   122
      Seq.of_list rules |> Seq.maps (fn (th, ps, cs) =>
wenzelm@55627
   123
        valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) =>
wenzelm@55627
   124
          let val cs' = map (fn (Ts, ts) =>
wenzelm@55627
   125
            (map (Envir.subst_type tye) Ts, map (Envir.subst_term env) ts)) cs
wenzelm@55627
   126
          in
wenzelm@55627
   127
            inst_extra_vars ctxt dom cs' |>
wenzelm@55627
   128
              Seq.map_filter (fn (inst, cs'') =>
wenzelm@55627
   129
                if is_valid_disj ctxt facts cs'' then NONE
wenzelm@55627
   130
                else SOME (th, env, inst, is, cs''))
wenzelm@55627
   131
          end));
berghofe@28326
   132
  in
wenzelm@55627
   133
    (case Seq.pull seq of
wenzelm@55634
   134
      NONE =>
wenzelm@55634
   135
        (if Context_Position.is_visible ctxt then
wenzelm@55634
   136
          warning (string_of_facts ctxt "Countermodel found:" facts)
wenzelm@55634
   137
         else (); NONE)
berghofe@28326
   138
    | SOME ((th, env, inst, is, cs), _) =>
berghofe@28326
   139
        if cs = [([], [goal])] then SOME (ClPrf (th, env, inst, is, []))
berghofe@28326
   140
        else
berghofe@28326
   141
          (case valid_cases ctxt rules goal dom facts nfacts nparams cs of
wenzelm@55627
   142
            NONE => NONE
wenzelm@55627
   143
          | SOME prfs => SOME (ClPrf (th, env, inst, is, prfs))))
berghofe@28326
   144
  end
berghofe@28326
   145
wenzelm@55631
   146
and valid_cases _ _ _ _ _ _ _ [] = SOME []
berghofe@28326
   147
  | valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) =
berghofe@28326
   148
      let
wenzelm@55634
   149
        val _ =
wenzelm@55634
   150
          cond_trace ctxt (fn () =>
wenzelm@55634
   151
            Pretty.string_of (Pretty.block
wenzelm@55634
   152
              (Pretty.str "case" :: Pretty.brk 1 ::
wenzelm@55634
   153
                Pretty.commas (map (Syntax.pretty_term ctxt) ts))));
wenzelm@55636
   154
wenzelm@55636
   155
        val ps = map_index (fn (i, T) => ("par" ^ string_of_int (nparams + i), T)) Ts;
wenzelm@55636
   156
        val (params, ctxt') = fold_map Variable.next_bound ps ctxt;
wenzelm@55627
   157
        val ts' = map_index (fn (i, t) => (subst_bounds (rev params, t), nfacts + i)) ts;
wenzelm@55627
   158
        val dom' =
wenzelm@55627
   159
          fold (fn (T, p) => Typtab.map_default (T, []) (fn ps => ps @ [p])) (Ts ~~ params) dom;
wenzelm@55627
   160
        val facts' = fold (fn (t, i) => Net.insert_term op = (t, (t, i))) ts' facts;
berghofe@28326
   161
      in
wenzelm@55636
   162
        (case valid ctxt' rules goal dom' facts' (nfacts + length ts) (nparams + length Ts) of
berghofe@28326
   163
          NONE => NONE
wenzelm@55627
   164
        | SOME prf =>
wenzelm@55627
   165
            (case valid_cases ctxt rules goal dom facts nfacts nparams ds of
wenzelm@55627
   166
              NONE => NONE
wenzelm@55627
   167
            | SOME prfs => SOME ((params, prf) :: prfs)))
berghofe@28326
   168
      end;
berghofe@28326
   169
wenzelm@31241
   170
berghofe@28326
   171
(** proof replaying **)
berghofe@28326
   172
wenzelm@55632
   173
fun thm_of_cl_prf ctxt goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
berghofe@28326
   174
  let
wenzelm@55627
   175
    val _ =
wenzelm@55632
   176
      cond_trace ctxt (fn () =>
wenzelm@61268
   177
        Pretty.string_of (Pretty.big_list "asms:" (map (Thm.pretty_thm ctxt) asms)));
wenzelm@55627
   178
    val th' =
wenzelm@55627
   179
      Drule.implies_elim_list
wenzelm@55627
   180
        (Thm.instantiate
wenzelm@60642
   181
           (map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T)) (Vartab.dest tye),
wenzelm@55627
   182
            map (fn (ixn, (T, t)) =>
wenzelm@60642
   183
              ((ixn, Envir.subst_type tye T), Thm.cterm_of ctxt t)) (Vartab.dest env) @
wenzelm@60642
   184
            map (fn (ixnT, t) => (ixnT, Thm.cterm_of ctxt t)) insts) th)
wenzelm@55627
   185
        (map (nth asms) is);
wenzelm@59582
   186
    val (_, cases) = dest_elim (Thm.prop_of th');
berghofe@28326
   187
  in
wenzelm@55627
   188
    (case (cases, prfs) of
berghofe@28326
   189
      ([([], [_])], []) => th'
wenzelm@55632
   190
    | ([([], [_])], [([], prf)]) => thm_of_cl_prf ctxt goal (asms @ [th']) prf
wenzelm@55627
   191
    | _ =>
wenzelm@55627
   192
        Drule.implies_elim_list
wenzelm@55627
   193
          (Thm.instantiate (Thm.match
wenzelm@59582
   194
             (Drule.strip_imp_concl (Thm.cprop_of th'), goal)) th')
wenzelm@55632
   195
          (map (thm_of_case_prf ctxt goal asms) (prfs ~~ cases)))
berghofe@28326
   196
  end
berghofe@28326
   197
wenzelm@55632
   198
and thm_of_case_prf ctxt goal asms ((params, prf), (_, asms')) =
berghofe@28326
   199
  let
wenzelm@59642
   200
    val cparams = map (Thm.cterm_of ctxt) params;
wenzelm@59642
   201
    val asms'' = map (Thm.cterm_of ctxt o curry subst_bounds (rev params)) asms';
wenzelm@55634
   202
    val (prems'', ctxt') = fold_map Thm.assume_hyps asms'' ctxt;
berghofe@28326
   203
  in
wenzelm@55627
   204
    Drule.forall_intr_list cparams
wenzelm@55634
   205
      (Drule.implies_intr_list asms'' (thm_of_cl_prf ctxt' goal (asms @ prems'') prf))
berghofe@28326
   206
  end;
berghofe@28326
   207
berghofe@28326
   208
berghofe@28326
   209
(** external interface **)
berghofe@28326
   210
wenzelm@54742
   211
fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context = ctxt', ...} =>
wenzelm@59498
   212
  resolve_tac ctxt' [rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2] 1 THEN
wenzelm@54742
   213
  SUBPROOF (fn {prems = prems', concl, context = ctxt'', ...} =>
wenzelm@55627
   214
    let
wenzelm@55627
   215
      val xs =
wenzelm@59582
   216
        map (Thm.term_of o #2) params @
wenzelm@55627
   217
        map (fn (_, s) => Free (s, the (Variable.default_type ctxt'' s)))
wenzelm@55627
   218
          (rev (Variable.dest_fixes ctxt''))  (* FIXME !? *)
berghofe@28326
   219
    in
wenzelm@55632
   220
      (case
wenzelm@59582
   221
        valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (Thm.term_of concl)
wenzelm@55632
   222
          (mk_dom xs) Net.empty 0 0 of
wenzelm@55627
   223
        NONE => no_tac
wenzelm@59498
   224
      | SOME prf => resolve_tac ctxt'' [thm_of_cl_prf ctxt'' concl [] prf] 1)
wenzelm@54742
   225
    end) ctxt' 1) ctxt;
berghofe@28326
   226
wenzelm@55632
   227
val _ = Theory.setup
wenzelm@55632
   228
  (trace_setup #>
wenzelm@67149
   229
   Method.setup \<^binding>\<open>coherent\<close>
wenzelm@55632
   230
    (Attrib.thms >> (fn rules => fn ctxt =>
wenzelm@55632
   231
        METHOD (fn facts => HEADGOAL (coherent_tac ctxt (facts @ rules)))))
wenzelm@55632
   232
      "prove coherent formula");
berghofe@28326
   233
berghofe@28326
   234
end;