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