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