src/Tools/coherent.ML
author blanchet
Mon, 15 Sep 2014 10:49:07 +0200
changeset 58335 a5a3b576fcfb
parent 55636 9d120886c50b
child 58839 ccda99401bc8
permissions -rw-r--r--
generate 'code' attribute only if 'code' plugin is enabled
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30160
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 29273
diff changeset
     1
(*  Title:      Tools/coherent.ML
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
     2
    Author:     Stefan Berghofer, TU Muenchen
31241
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30552
diff changeset
     3
    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
     4
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
     5
Prover for coherent logic, see e.g.
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
     6
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
     7
  Marc Bezem and Thierry Coquand, Automating Coherent Logic, LPAR 2005
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
     8
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
     9
for a description of the algorithm.
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    10
*)
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    11
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    12
signature COHERENT_DATA =
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    13
sig
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    14
  val atomize_elimL: thm
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    15
  val atomize_exL: thm
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    16
  val atomize_conjL: thm
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    17
  val atomize_disjL: thm
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    18
  val operator_names: string list
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    19
end;
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    20
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    21
signature COHERENT =
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    22
sig
55632
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
    23
  val trace: bool Config.T
31241
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30552
diff changeset
    24
  val coherent_tac: Proof.context -> thm list -> int -> tactic
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    25
end;
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    26
32734
06c13b2e562e misc tuning and modernization;
wenzelm
parents: 32199
diff changeset
    27
functor Coherent(Data: COHERENT_DATA) : COHERENT =
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    28
struct
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    29
31241
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30552
diff changeset
    30
(** misc tools **)
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30552
diff changeset
    31
55632
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
    32
val (trace, trace_setup) = Attrib.config_bool @{binding coherent_trace} (K false);
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
    33
fun cond_trace ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ();
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    34
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    35
datatype cl_prf =
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    36
  ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list *
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    37
  int list * (term list * cl_prf) list;
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    38
29273
285c00993bc2 use exists_Const directly;
wenzelm
parents: 28339
diff changeset
    39
val is_atomic = not o exists_Const (member (op =) Data.operator_names o #1);
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    40
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 46186
diff changeset
    41
fun rulify_elim_conv ctxt ct =
36946
4eba866311df avoid open Conv;
wenzelm
parents: 36945
diff changeset
    42
  if is_atomic (Logic.strip_imp_concl (term_of ct)) then Conv.all_conv ct
4eba866311df avoid open Conv;
wenzelm
parents: 36945
diff changeset
    43
  else Conv.concl_conv (length (Logic.strip_imp_prems (term_of ct)))
4eba866311df avoid open Conv;
wenzelm
parents: 36945
diff changeset
    44
    (Conv.rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 46186
diff changeset
    45
     Raw_Simplifier.rewrite ctxt true (map Thm.symmetric
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    46
       [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    47
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
    48
fun rulify_elim ctxt th = Simplifier.norm_hhf ctxt (Conv.fconv_rule (rulify_elim_conv ctxt) th);
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    49
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    50
(* Decompose elimination rule of the form
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    51
   A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    52
*)
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    53
fun dest_elim prop =
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    54
  let
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    55
    val prems = Logic.strip_imp_prems prop;
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    56
    val concl = Logic.strip_imp_concl prop;
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    57
    val (prems1, prems2) =
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    58
      take_suffix (fn t => Logic.strip_assums_concl t = concl) prems;
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    59
  in
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    60
    (prems1,
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    61
     if null prems2 then [([], [concl])]
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    62
     else map (fn t =>
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    63
       (map snd (Logic.strip_params t), Logic.strip_assums_hyp t)) prems2)
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    64
  end;
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    65
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 46186
diff changeset
    66
fun mk_rule ctxt th =
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    67
  let
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 46186
diff changeset
    68
    val th' = rulify_elim ctxt th;
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    69
    val (prems, cases) = dest_elim (prop_of th')
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    70
  in (th', prems, cases) end;
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    71
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    72
fun mk_dom ts = fold (fn t =>
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    73
  Typtab.map_default (fastype_of t, []) (fn us => us @ [t])) ts Typtab.empty;
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    74
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    75
val empty_env = (Vartab.empty, Vartab.empty);
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    76
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    77
(* Find matcher that makes conjunction valid in given state *)
55631
7f428e08111b removed dead code;
wenzelm
parents: 55628
diff changeset
    78
fun valid_conj _ _ env [] = Seq.single (env, [])
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    79
  | valid_conj ctxt facts env (t :: ts) =
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    80
      Seq.maps (fn (u, x) => Seq.map (apsnd (cons x))
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    81
        (valid_conj ctxt facts
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41228
diff changeset
    82
           (Pattern.match (Proof_Context.theory_of ctxt) (t, u) env) ts
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    83
         handle Pattern.MATCH => Seq.empty))
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    84
          (Seq.of_list (sort (int_ord o pairself snd) (Net.unify_term facts t)));
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    85
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    86
(* Instantiate variables that only occur free in conlusion *)
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    87
fun inst_extra_vars ctxt dom cs =
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    88
  let
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    89
    val vs = fold Term.add_vars (maps snd cs) [];
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
    90
    fun insts [] inst = Seq.single inst
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
    91
      | insts ((ixn, T) :: vs') inst =
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
    92
          Seq.maps (fn t => insts vs' (((ixn, T), t) :: inst))
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
    93
            (Seq.of_list
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
    94
              (case Typtab.lookup dom T of
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
    95
                NONE =>
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
    96
                  error ("Unknown domain: " ^
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
    97
                    Syntax.string_of_typ ctxt T ^ "\nfor term(s) " ^
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
    98
                    commas (maps (map (Syntax.string_of_term ctxt) o snd) cs))
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
    99
              | SOME ts => ts))
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   100
  in
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   101
    Seq.map (fn inst =>
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   102
      (inst, map (apsnd (map (subst_Vars (map (apfst fst) inst)))) cs))
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   103
        (insts vs [])
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   104
  end;
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   105
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   106
(* Check whether disjunction is valid in given state *)
55631
7f428e08111b removed dead code;
wenzelm
parents: 55628
diff changeset
   107
fun is_valid_disj _ _ [] = false
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   108
  | is_valid_disj ctxt facts ((Ts, ts) :: ds) =
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   109
      let val vs = map_index (fn (i, T) => Var (("x", i), T)) Ts in
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   110
        (case Seq.pull (valid_conj ctxt facts empty_env
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   111
            (map (fn t => subst_bounds (rev vs, t)) ts)) of
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   112
          SOME _ => true
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   113
        | NONE => is_valid_disj ctxt facts ds)
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   114
      end;
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   115
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   116
fun string_of_facts ctxt s facts =
55634
306ff289da3a tuned messages;
wenzelm
parents: 55632
diff changeset
   117
  Pretty.string_of (Pretty.big_list s
306ff289da3a tuned messages;
wenzelm
parents: 55632
diff changeset
   118
    (map (Syntax.pretty_term ctxt) (map fst (sort (int_ord o pairself snd) (Net.content facts)))));
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   119
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   120
fun valid ctxt rules goal dom facts nfacts nparams =
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   121
  let
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   122
    val seq =
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   123
      Seq.of_list rules |> Seq.maps (fn (th, ps, cs) =>
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   124
        valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) =>
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   125
          let val cs' = map (fn (Ts, ts) =>
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   126
            (map (Envir.subst_type tye) Ts, map (Envir.subst_term env) ts)) cs
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   127
          in
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   128
            inst_extra_vars ctxt dom cs' |>
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   129
              Seq.map_filter (fn (inst, cs'') =>
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   130
                if is_valid_disj ctxt facts cs'' then NONE
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   131
                else SOME (th, env, inst, is, cs''))
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   132
          end));
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   133
  in
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   134
    (case Seq.pull seq of
55634
306ff289da3a tuned messages;
wenzelm
parents: 55632
diff changeset
   135
      NONE =>
306ff289da3a tuned messages;
wenzelm
parents: 55632
diff changeset
   136
        (if Context_Position.is_visible ctxt then
306ff289da3a tuned messages;
wenzelm
parents: 55632
diff changeset
   137
          warning (string_of_facts ctxt "Countermodel found:" facts)
306ff289da3a tuned messages;
wenzelm
parents: 55632
diff changeset
   138
         else (); NONE)
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   139
    | SOME ((th, env, inst, is, cs), _) =>
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   140
        if cs = [([], [goal])] then SOME (ClPrf (th, env, inst, is, []))
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   141
        else
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   142
          (case valid_cases ctxt rules goal dom facts nfacts nparams cs of
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   143
            NONE => NONE
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   144
          | SOME prfs => SOME (ClPrf (th, env, inst, is, prfs))))
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   145
  end
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   146
55631
7f428e08111b removed dead code;
wenzelm
parents: 55628
diff changeset
   147
and valid_cases _ _ _ _ _ _ _ [] = SOME []
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   148
  | valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) =
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   149
      let
55634
306ff289da3a tuned messages;
wenzelm
parents: 55632
diff changeset
   150
        val _ =
306ff289da3a tuned messages;
wenzelm
parents: 55632
diff changeset
   151
          cond_trace ctxt (fn () =>
306ff289da3a tuned messages;
wenzelm
parents: 55632
diff changeset
   152
            Pretty.string_of (Pretty.block
306ff289da3a tuned messages;
wenzelm
parents: 55632
diff changeset
   153
              (Pretty.str "case" :: Pretty.brk 1 ::
306ff289da3a tuned messages;
wenzelm
parents: 55632
diff changeset
   154
                Pretty.commas (map (Syntax.pretty_term ctxt) ts))));
55636
9d120886c50b more official params in context;
wenzelm
parents: 55634
diff changeset
   155
9d120886c50b more official params in context;
wenzelm
parents: 55634
diff changeset
   156
        val ps = map_index (fn (i, T) => ("par" ^ string_of_int (nparams + i), T)) Ts;
9d120886c50b more official params in context;
wenzelm
parents: 55634
diff changeset
   157
        val (params, ctxt') = fold_map Variable.next_bound ps ctxt;
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   158
        val ts' = map_index (fn (i, t) => (subst_bounds (rev params, t), nfacts + i)) ts;
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   159
        val dom' =
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   160
          fold (fn (T, p) => Typtab.map_default (T, []) (fn ps => ps @ [p])) (Ts ~~ params) dom;
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   161
        val facts' = fold (fn (t, i) => Net.insert_term op = (t, (t, i))) ts' facts;
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   162
      in
55636
9d120886c50b more official params in context;
wenzelm
parents: 55634
diff changeset
   163
        (case valid ctxt' rules goal dom' facts' (nfacts + length ts) (nparams + length Ts) of
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   164
          NONE => NONE
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   165
        | SOME prf =>
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   166
            (case valid_cases ctxt rules goal dom facts nfacts nparams ds of
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   167
              NONE => NONE
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   168
            | SOME prfs => SOME ((params, prf) :: prfs)))
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   169
      end;
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   170
31241
b3c7044d47b6 modernized method setup;
wenzelm
parents: 30552
diff changeset
   171
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   172
(** proof replaying **)
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   173
55632
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   174
fun thm_of_cl_prf ctxt goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   175
  let
55632
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   176
    val thy = Proof_Context.theory_of ctxt;
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   177
    val cert = Thm.cterm_of thy;
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   178
    val certT = Thm.ctyp_of thy;
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   179
    val _ =
55632
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   180
      cond_trace ctxt (fn () =>
55634
306ff289da3a tuned messages;
wenzelm
parents: 55632
diff changeset
   181
        Pretty.string_of (Pretty.big_list "asms:" (map (Display.pretty_thm ctxt) asms)));
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   182
    val th' =
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   183
      Drule.implies_elim_list
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   184
        (Thm.instantiate
55632
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   185
           (map (fn (ixn, (S, T)) => (certT (TVar ((ixn, S))), certT T)) (Vartab.dest tye),
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   186
            map (fn (ixn, (T, t)) =>
55632
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   187
              (cert (Var (ixn, Envir.subst_type tye T)), cert t)) (Vartab.dest env) @
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   188
            map (fn (ixnT, t) => (cert (Var ixnT), cert t)) insts) th)
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   189
        (map (nth asms) is);
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   190
    val (_, cases) = dest_elim (prop_of th');
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   191
  in
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   192
    (case (cases, prfs) of
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   193
      ([([], [_])], []) => th'
55632
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   194
    | ([([], [_])], [([], prf)]) => thm_of_cl_prf ctxt goal (asms @ [th']) prf
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   195
    | _ =>
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   196
        Drule.implies_elim_list
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   197
          (Thm.instantiate (Thm.match
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   198
             (Drule.strip_imp_concl (cprop_of th'), goal)) th')
55632
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   199
          (map (thm_of_case_prf ctxt goal asms) (prfs ~~ cases)))
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   200
  end
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   201
55632
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   202
and thm_of_case_prf ctxt goal asms ((params, prf), (_, asms')) =
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   203
  let
55632
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   204
    val thy = Proof_Context.theory_of ctxt;
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   205
    val cert = Thm.cterm_of thy;
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   206
    val cparams = map cert params;
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   207
    val asms'' = map (cert o curry subst_bounds (rev params)) asms';
55634
306ff289da3a tuned messages;
wenzelm
parents: 55632
diff changeset
   208
    val (prems'', ctxt') = fold_map Thm.assume_hyps asms'' ctxt;
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   209
  in
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   210
    Drule.forall_intr_list cparams
55634
306ff289da3a tuned messages;
wenzelm
parents: 55632
diff changeset
   211
      (Drule.implies_intr_list asms'' (thm_of_cl_prf ctxt' goal (asms @ prems'') prf))
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   212
  end;
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   213
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   214
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   215
(** external interface **)
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   216
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 46186
diff changeset
   217
fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context = ctxt', ...} =>
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 46186
diff changeset
   218
  rtac (rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2) 1 THEN
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 46186
diff changeset
   219
  SUBPROOF (fn {prems = prems', concl, context = ctxt'', ...} =>
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   220
    let
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   221
      val xs =
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   222
        map (term_of o #2) params @
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   223
        map (fn (_, s) => Free (s, the (Variable.default_type ctxt'' s)))
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   224
          (rev (Variable.dest_fixes ctxt''))  (* FIXME !? *)
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   225
    in
55632
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   226
      (case
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   227
        valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   228
          (mk_dom xs) Net.empty 0 0 of
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54883
diff changeset
   229
        NONE => no_tac
55632
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   230
      | SOME prf => rtac (thm_of_cl_prf ctxt'' concl [] prf) 1)
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 46186
diff changeset
   231
    end) ctxt' 1) ctxt;
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   232
55632
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   233
val _ = Theory.setup
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   234
  (trace_setup #>
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   235
   Method.setup @{binding coherent}
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   236
    (Attrib.thms >> (fn rules => fn ctxt =>
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   237
        METHOD (fn facts => HEADGOAL (coherent_tac ctxt (facts @ rules)))))
0f9d03649a9c modernized tool setup;
wenzelm
parents: 55631
diff changeset
   238
      "prove coherent formula");
28326
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   239
ddd53738dae8 New prover for coherent logic.
berghofe
parents:
diff changeset
   240
end;