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