src/Pure/Proof/proofchecker.ML
author wenzelm
Mon, 08 Aug 2011 17:23:15 +0200
changeset 44058 ae85c5d64913
parent 44057 fda143b5c2f5
child 44061 9f17ede679e9
permissions -rw-r--r--
misc tuning -- eliminated old-fashioned rep_thm;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     1
(*  Title:      Pure/Proof/proofchecker.ML
11539
0f17da240450 tuned headers;
wenzelm
parents: 11522
diff changeset
     2
    Author:     Stefan Berghofer, TU Muenchen
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     3
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     4
Simple proof checker based only on the core inference rules
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     5
of Isabelle/Pure.
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     6
*)
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     7
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     8
signature PROOF_CHECKER =
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
     9
sig
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    10
  val thm_of_proof : theory -> Proofterm.proof -> thm
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    11
end;
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    12
44057
fda143b5c2f5 modernized strcture Proof_Checker;
wenzelm
parents: 43326
diff changeset
    13
structure Proof_Checker : PROOF_CHECKER =
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    14
struct
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    15
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    16
(***** construct a theorem out of a proof term *****)
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    17
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    18
fun lookup_thm thy =
44057
fda143b5c2f5 modernized strcture Proof_Checker;
wenzelm
parents: 43326
diff changeset
    19
  let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty in
fda143b5c2f5 modernized strcture Proof_Checker;
wenzelm
parents: 43326
diff changeset
    20
    fn s =>
fda143b5c2f5 modernized strcture Proof_Checker;
wenzelm
parents: 43326
diff changeset
    21
      (case Symtab.lookup tab s of
fda143b5c2f5 modernized strcture Proof_Checker;
wenzelm
parents: 43326
diff changeset
    22
        NONE => error ("Unknown theorem " ^ quote s)
fda143b5c2f5 modernized strcture Proof_Checker;
wenzelm
parents: 43326
diff changeset
    23
      | SOME thm => thm)
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    24
  end;
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    25
13733
8ea7388f66d4 - tuned beta_eta_convert
berghofe
parents: 13670
diff changeset
    26
val beta_eta_convert =
22910
54d231cbc19a moved conversions to structure Conv;
wenzelm
parents: 21646
diff changeset
    27
  Conv.fconv_rule Drule.beta_eta_conversion;
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    28
37229
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    29
(* equality modulo renaming of type variables *)
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    30
fun is_equal t t' =
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    31
  let
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    32
    val atoms = fold_types (fold_atyps (insert (op =))) t [];
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    33
    val atoms' = fold_types (fold_atyps (insert (op =))) t' []
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    34
  in
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    35
    length atoms = length atoms' andalso
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    36
    map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t'
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    37
  end;
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    38
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    39
fun pretty_prf thy vs Hs prf =
37310
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37229
diff changeset
    40
  let val prf' = prf |> Proofterm.prf_subst_bounds (map Free vs) |>
96e2b9a6f074 do not open Proofterm, which is very ould style;
wenzelm
parents: 37229
diff changeset
    41
    Proofterm.prf_subst_pbounds (map (Hyp o prop_of) Hs)
37229
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    42
  in
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    43
    (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    44
     Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    45
  end;
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    46
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    47
fun pretty_term thy vs _ t =
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    48
  let val t' = subst_bounds (map Free vs, t)
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    49
  in
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    50
    (Syntax.pretty_term_global thy t',
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    51
     Syntax.pretty_typ_global thy (fastype_of t'))
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    52
  end;
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    53
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    54
fun appl_error thy prt vs Hs s f a =
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    55
  let
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    56
    val (pp_f, pp_fT) = pretty_prf thy vs Hs f;
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    57
    val (pp_a, pp_aT) = prt thy vs Hs a
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    58
  in
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    59
    error (cat_lines
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    60
      [s,
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    61
       "",
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    62
       Pretty.string_of (Pretty.block
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    63
         [Pretty.str "Operator:", Pretty.brk 2, pp_f,
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    64
           Pretty.str " ::", Pretty.brk 1, pp_fT]),
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    65
       Pretty.string_of (Pretty.block
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    66
         [Pretty.str "Operand:", Pretty.brk 3, pp_a,
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    67
           Pretty.str " ::", Pretty.brk 1, pp_aT]),
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    68
       ""])
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    69
  end;
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    70
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    71
fun thm_of_proof thy prf =
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    72
  let
29277
29dd1c516337 Term.declare_term_frees;
wenzelm
parents: 29270
diff changeset
    73
    val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    74
    val lookup = lookup_thm thy;
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    75
13670
c71b905a852a Fixed problem with theorems containing TFrees.
berghofe
parents: 12238
diff changeset
    76
    fun thm_of_atom thm Ts =
c71b905a852a Fixed problem with theorems containing TFrees.
berghofe
parents: 12238
diff changeset
    77
      let
36042
85efdadee8ae switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
krauss
parents: 35985
diff changeset
    78
        val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 30146
diff changeset
    79
        val (fmap, thm') = Thm.varifyT_global' [] thm;
20151
b22c14181eb7 thm_of_proof: tuned Name operations;
wenzelm
parents: 20071
diff changeset
    80
        val ctye = map (pairself (Thm.ctyp_of thy))
15798
016f3be5a5ec Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents: 15574
diff changeset
    81
          (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
13670
c71b905a852a Fixed problem with theorems containing TFrees.
berghofe
parents: 12238
diff changeset
    82
      in
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35845
diff changeset
    83
        Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
13670
c71b905a852a Fixed problem with theorems containing TFrees.
berghofe
parents: 12238
diff changeset
    84
      end;
c71b905a852a Fixed problem with theorems containing TFrees.
berghofe
parents: 12238
diff changeset
    85
28808
7925199a0226 adapted PThm;
wenzelm
parents: 28674
diff changeset
    86
    fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    87
          let
37229
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
    88
            val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
44058
ae85c5d64913 misc tuning -- eliminated old-fashioned rep_thm;
wenzelm
parents: 44057
diff changeset
    89
            val prop = Thm.prop_of thm;
44057
fda143b5c2f5 modernized strcture Proof_Checker;
wenzelm
parents: 43326
diff changeset
    90
            val _ =
fda143b5c2f5 modernized strcture Proof_Checker;
wenzelm
parents: 43326
diff changeset
    91
              if is_equal prop prop' then ()
fda143b5c2f5 modernized strcture Proof_Checker;
wenzelm
parents: 43326
diff changeset
    92
              else
fda143b5c2f5 modernized strcture Proof_Checker;
wenzelm
parents: 43326
diff changeset
    93
                error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
fda143b5c2f5 modernized strcture Proof_Checker;
wenzelm
parents: 43326
diff changeset
    94
                  Syntax.string_of_term_global thy prop ^ "\n\n" ^
fda143b5c2f5 modernized strcture Proof_Checker;
wenzelm
parents: 43326
diff changeset
    95
                  Syntax.string_of_term_global thy prop');
13670
c71b905a852a Fixed problem with theorems containing TFrees.
berghofe
parents: 12238
diff changeset
    96
          in thm_of_atom thm Ts end
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
    97
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15001
diff changeset
    98
      | thm_of _ _ (PAxm (name, _, SOME Ts)) =
28674
08a77c495dc1 renamed Thm.get_axiom_i to Thm.axiom;
wenzelm
parents: 26939
diff changeset
    99
          thm_of_atom (Thm.axiom thy name) Ts
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   100
30146
a77fc0209723 eliminated NJ's List.nth;
wenzelm
parents: 29277
diff changeset
   101
      | thm_of _ Hs (PBound i) = nth Hs i
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   102
20164
928c8dc07216 thm_of_proof: improved generation of variables;
wenzelm
parents: 20151
diff changeset
   103
      | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   104
          let
43326
47cf4bc789aa simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents: 39557
diff changeset
   105
            val (x, names') = Name.variant s names;
20164
928c8dc07216 thm_of_proof: improved generation of variables;
wenzelm
parents: 20151
diff changeset
   106
            val thm = thm_of ((x, T) :: vs, names') Hs prf
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   107
          in
20151
b22c14181eb7 thm_of_proof: tuned Name operations;
wenzelm
parents: 20071
diff changeset
   108
            Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   109
          end
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   110
20164
928c8dc07216 thm_of_proof: improved generation of variables;
wenzelm
parents: 20151
diff changeset
   111
      | thm_of (vs, names) Hs (prf % SOME t) =
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   112
          let
20164
928c8dc07216 thm_of_proof: improved generation of variables;
wenzelm
parents: 20151
diff changeset
   113
            val thm = thm_of (vs, names) Hs prf;
928c8dc07216 thm_of_proof: improved generation of variables;
wenzelm
parents: 20151
diff changeset
   114
            val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
37229
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
   115
          in
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
   116
            Thm.forall_elim ct thm
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
   117
            handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
   118
          end
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   119
20164
928c8dc07216 thm_of_proof: improved generation of variables;
wenzelm
parents: 20151
diff changeset
   120
      | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   121
          let
20151
b22c14181eb7 thm_of_proof: tuned Name operations;
wenzelm
parents: 20071
diff changeset
   122
            val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
20164
928c8dc07216 thm_of_proof: improved generation of variables;
wenzelm
parents: 20151
diff changeset
   123
            val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   124
          in
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   125
            Thm.implies_intr ct thm
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   126
          end
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   127
20164
928c8dc07216 thm_of_proof: improved generation of variables;
wenzelm
parents: 20151
diff changeset
   128
      | thm_of vars Hs (prf %% prf') =
20151
b22c14181eb7 thm_of_proof: tuned Name operations;
wenzelm
parents: 20071
diff changeset
   129
          let
20164
928c8dc07216 thm_of_proof: improved generation of variables;
wenzelm
parents: 20151
diff changeset
   130
            val thm = beta_eta_convert (thm_of vars Hs prf);
928c8dc07216 thm_of_proof: improved generation of variables;
wenzelm
parents: 20151
diff changeset
   131
            val thm' = beta_eta_convert (thm_of vars Hs prf');
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   132
          in
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   133
            Thm.implies_elim thm thm'
37229
47eb565796f4 - Equality check on propositions after lookup of theorem now takes type variable
berghofe
parents: 36042
diff changeset
   134
            handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   135
          end
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   136
20151
b22c14181eb7 thm_of_proof: tuned Name operations;
wenzelm
parents: 20071
diff changeset
   137
      | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   138
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   139
      | thm_of _ _ _ = error "thm_of_proof: partial proof term";
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   140
20164
928c8dc07216 thm_of_proof: improved generation of variables;
wenzelm
parents: 20151
diff changeset
   141
  in beta_eta_convert (thm_of ([], prf_names) [] prf) end;
11522
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   142
42fbb6abed5a Initial revision of tools for proof terms.
berghofe
parents:
diff changeset
   143
end;