modernized file proof_checker.ML;
authorwenzelm
Mon Aug 08 21:11:10 2011 +0200 (2011-08-08)
changeset 4406255a4df7f2568
parent 44061 9f17ede679e9
child 44071 9ee98b584494
modernized file proof_checker.ML;
src/Pure/IsaMakefile
src/Pure/Proof/proof_checker.ML
src/Pure/Proof/proofchecker.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/IsaMakefile	Mon Aug 08 20:47:12 2011 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Mon Aug 08 21:11:10 2011 +0200
     1.3 @@ -158,9 +158,9 @@
     1.4    PIDE/document.ML					\
     1.5    PIDE/isar_document.ML					\
     1.6    Proof/extraction.ML					\
     1.7 +  Proof/proof_checker.ML				\
     1.8    Proof/proof_rewrite_rules.ML				\
     1.9    Proof/proof_syntax.ML					\
    1.10 -  Proof/proofchecker.ML					\
    1.11    Proof/reconstruct.ML					\
    1.12    ProofGeneral/pgip.ML					\
    1.13    ProofGeneral/pgip_input.ML				\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Proof/proof_checker.ML	Mon Aug 08 21:11:10 2011 +0200
     2.3 @@ -0,0 +1,145 @@
     2.4 +(*  Title:      Pure/Proof/proofchecker.ML
     2.5 +    Author:     Stefan Berghofer, TU Muenchen
     2.6 +
     2.7 +Simple proof checker based only on the core inference rules
     2.8 +of Isabelle/Pure.
     2.9 +*)
    2.10 +
    2.11 +signature PROOF_CHECKER =
    2.12 +sig
    2.13 +  val thm_of_proof : theory -> Proofterm.proof -> thm
    2.14 +end;
    2.15 +
    2.16 +structure Proof_Checker : PROOF_CHECKER =
    2.17 +struct
    2.18 +
    2.19 +(***** construct a theorem out of a proof term *****)
    2.20 +
    2.21 +fun lookup_thm thy =
    2.22 +  let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty in
    2.23 +    fn s =>
    2.24 +      (case Symtab.lookup tab s of
    2.25 +        NONE => error ("Unknown theorem " ^ quote s)
    2.26 +      | SOME thm => thm)
    2.27 +  end;
    2.28 +
    2.29 +val beta_eta_convert =
    2.30 +  Conv.fconv_rule Drule.beta_eta_conversion;
    2.31 +
    2.32 +(* equality modulo renaming of type variables *)
    2.33 +fun is_equal t t' =
    2.34 +  let
    2.35 +    val atoms = fold_types (fold_atyps (insert (op =))) t [];
    2.36 +    val atoms' = fold_types (fold_atyps (insert (op =))) t' []
    2.37 +  in
    2.38 +    length atoms = length atoms' andalso
    2.39 +    map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t'
    2.40 +  end;
    2.41 +
    2.42 +fun pretty_prf thy vs Hs prf =
    2.43 +  let val prf' = prf |> Proofterm.prf_subst_bounds (map Free vs) |>
    2.44 +    Proofterm.prf_subst_pbounds (map (Hyp o prop_of) Hs)
    2.45 +  in
    2.46 +    (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
    2.47 +     Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
    2.48 +  end;
    2.49 +
    2.50 +fun pretty_term thy vs _ t =
    2.51 +  let val t' = subst_bounds (map Free vs, t)
    2.52 +  in
    2.53 +    (Syntax.pretty_term_global thy t',
    2.54 +     Syntax.pretty_typ_global thy (fastype_of t'))
    2.55 +  end;
    2.56 +
    2.57 +fun appl_error thy prt vs Hs s f a =
    2.58 +  let
    2.59 +    val (pp_f, pp_fT) = pretty_prf thy vs Hs f;
    2.60 +    val (pp_a, pp_aT) = prt thy vs Hs a
    2.61 +  in
    2.62 +    error (cat_lines
    2.63 +      [s,
    2.64 +       "",
    2.65 +       Pretty.string_of (Pretty.block
    2.66 +         [Pretty.str "Operator:", Pretty.brk 2, pp_f,
    2.67 +           Pretty.str " ::", Pretty.brk 1, pp_fT]),
    2.68 +       Pretty.string_of (Pretty.block
    2.69 +         [Pretty.str "Operand:", Pretty.brk 3, pp_a,
    2.70 +           Pretty.str " ::", Pretty.brk 1, pp_aT]),
    2.71 +       ""])
    2.72 +  end;
    2.73 +
    2.74 +fun thm_of_proof thy =
    2.75 +  let val lookup = lookup_thm thy in
    2.76 +    fn prf =>
    2.77 +      let
    2.78 +        val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
    2.79 +
    2.80 +        fun thm_of_atom thm Ts =
    2.81 +          let
    2.82 +            val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
    2.83 +            val (fmap, thm') = Thm.varifyT_global' [] thm;
    2.84 +            val ctye = map (pairself (Thm.ctyp_of thy))
    2.85 +              (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
    2.86 +          in
    2.87 +            Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
    2.88 +          end;
    2.89 +
    2.90 +        fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
    2.91 +              let
    2.92 +                val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
    2.93 +                val prop = Thm.prop_of thm;
    2.94 +                val _ =
    2.95 +                  if is_equal prop prop' then ()
    2.96 +                  else
    2.97 +                    error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
    2.98 +                      Syntax.string_of_term_global thy prop ^ "\n\n" ^
    2.99 +                      Syntax.string_of_term_global thy prop');
   2.100 +              in thm_of_atom thm Ts end
   2.101 +
   2.102 +          | thm_of _ _ (PAxm (name, _, SOME Ts)) =
   2.103 +              thm_of_atom (Thm.axiom thy name) Ts
   2.104 +
   2.105 +          | thm_of _ Hs (PBound i) = nth Hs i
   2.106 +
   2.107 +          | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
   2.108 +              let
   2.109 +                val (x, names') = Name.variant s names;
   2.110 +                val thm = thm_of ((x, T) :: vs, names') Hs prf
   2.111 +              in
   2.112 +                Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
   2.113 +              end
   2.114 +
   2.115 +          | thm_of (vs, names) Hs (prf % SOME t) =
   2.116 +              let
   2.117 +                val thm = thm_of (vs, names) Hs prf;
   2.118 +                val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
   2.119 +              in
   2.120 +                Thm.forall_elim ct thm
   2.121 +                handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
   2.122 +              end
   2.123 +
   2.124 +          | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
   2.125 +              let
   2.126 +                val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
   2.127 +                val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
   2.128 +              in
   2.129 +                Thm.implies_intr ct thm
   2.130 +              end
   2.131 +
   2.132 +          | thm_of vars Hs (prf %% prf') =
   2.133 +              let
   2.134 +                val thm = beta_eta_convert (thm_of vars Hs prf);
   2.135 +                val thm' = beta_eta_convert (thm_of vars Hs prf');
   2.136 +              in
   2.137 +                Thm.implies_elim thm thm'
   2.138 +                handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
   2.139 +              end
   2.140 +
   2.141 +          | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
   2.142 +
   2.143 +          | thm_of _ _ _ = error "thm_of_proof: partial proof term";
   2.144 +
   2.145 +      in beta_eta_convert (thm_of ([], prf_names) [] prf) end
   2.146 +  end;
   2.147 +
   2.148 +end;
     3.1 --- a/src/Pure/Proof/proofchecker.ML	Mon Aug 08 20:47:12 2011 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,145 +0,0 @@
     3.4 -(*  Title:      Pure/Proof/proofchecker.ML
     3.5 -    Author:     Stefan Berghofer, TU Muenchen
     3.6 -
     3.7 -Simple proof checker based only on the core inference rules
     3.8 -of Isabelle/Pure.
     3.9 -*)
    3.10 -
    3.11 -signature PROOF_CHECKER =
    3.12 -sig
    3.13 -  val thm_of_proof : theory -> Proofterm.proof -> thm
    3.14 -end;
    3.15 -
    3.16 -structure Proof_Checker : PROOF_CHECKER =
    3.17 -struct
    3.18 -
    3.19 -(***** construct a theorem out of a proof term *****)
    3.20 -
    3.21 -fun lookup_thm thy =
    3.22 -  let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty in
    3.23 -    fn s =>
    3.24 -      (case Symtab.lookup tab s of
    3.25 -        NONE => error ("Unknown theorem " ^ quote s)
    3.26 -      | SOME thm => thm)
    3.27 -  end;
    3.28 -
    3.29 -val beta_eta_convert =
    3.30 -  Conv.fconv_rule Drule.beta_eta_conversion;
    3.31 -
    3.32 -(* equality modulo renaming of type variables *)
    3.33 -fun is_equal t t' =
    3.34 -  let
    3.35 -    val atoms = fold_types (fold_atyps (insert (op =))) t [];
    3.36 -    val atoms' = fold_types (fold_atyps (insert (op =))) t' []
    3.37 -  in
    3.38 -    length atoms = length atoms' andalso
    3.39 -    map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t'
    3.40 -  end;
    3.41 -
    3.42 -fun pretty_prf thy vs Hs prf =
    3.43 -  let val prf' = prf |> Proofterm.prf_subst_bounds (map Free vs) |>
    3.44 -    Proofterm.prf_subst_pbounds (map (Hyp o prop_of) Hs)
    3.45 -  in
    3.46 -    (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
    3.47 -     Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
    3.48 -  end;
    3.49 -
    3.50 -fun pretty_term thy vs _ t =
    3.51 -  let val t' = subst_bounds (map Free vs, t)
    3.52 -  in
    3.53 -    (Syntax.pretty_term_global thy t',
    3.54 -     Syntax.pretty_typ_global thy (fastype_of t'))
    3.55 -  end;
    3.56 -
    3.57 -fun appl_error thy prt vs Hs s f a =
    3.58 -  let
    3.59 -    val (pp_f, pp_fT) = pretty_prf thy vs Hs f;
    3.60 -    val (pp_a, pp_aT) = prt thy vs Hs a
    3.61 -  in
    3.62 -    error (cat_lines
    3.63 -      [s,
    3.64 -       "",
    3.65 -       Pretty.string_of (Pretty.block
    3.66 -         [Pretty.str "Operator:", Pretty.brk 2, pp_f,
    3.67 -           Pretty.str " ::", Pretty.brk 1, pp_fT]),
    3.68 -       Pretty.string_of (Pretty.block
    3.69 -         [Pretty.str "Operand:", Pretty.brk 3, pp_a,
    3.70 -           Pretty.str " ::", Pretty.brk 1, pp_aT]),
    3.71 -       ""])
    3.72 -  end;
    3.73 -
    3.74 -fun thm_of_proof thy =
    3.75 -  let val lookup = lookup_thm thy in
    3.76 -    fn prf =>
    3.77 -      let
    3.78 -        val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
    3.79 -
    3.80 -        fun thm_of_atom thm Ts =
    3.81 -          let
    3.82 -            val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
    3.83 -            val (fmap, thm') = Thm.varifyT_global' [] thm;
    3.84 -            val ctye = map (pairself (Thm.ctyp_of thy))
    3.85 -              (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
    3.86 -          in
    3.87 -            Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
    3.88 -          end;
    3.89 -
    3.90 -        fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
    3.91 -              let
    3.92 -                val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
    3.93 -                val prop = Thm.prop_of thm;
    3.94 -                val _ =
    3.95 -                  if is_equal prop prop' then ()
    3.96 -                  else
    3.97 -                    error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
    3.98 -                      Syntax.string_of_term_global thy prop ^ "\n\n" ^
    3.99 -                      Syntax.string_of_term_global thy prop');
   3.100 -              in thm_of_atom thm Ts end
   3.101 -
   3.102 -          | thm_of _ _ (PAxm (name, _, SOME Ts)) =
   3.103 -              thm_of_atom (Thm.axiom thy name) Ts
   3.104 -
   3.105 -          | thm_of _ Hs (PBound i) = nth Hs i
   3.106 -
   3.107 -          | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
   3.108 -              let
   3.109 -                val (x, names') = Name.variant s names;
   3.110 -                val thm = thm_of ((x, T) :: vs, names') Hs prf
   3.111 -              in
   3.112 -                Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
   3.113 -              end
   3.114 -
   3.115 -          | thm_of (vs, names) Hs (prf % SOME t) =
   3.116 -              let
   3.117 -                val thm = thm_of (vs, names) Hs prf;
   3.118 -                val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
   3.119 -              in
   3.120 -                Thm.forall_elim ct thm
   3.121 -                handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
   3.122 -              end
   3.123 -
   3.124 -          | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
   3.125 -              let
   3.126 -                val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
   3.127 -                val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
   3.128 -              in
   3.129 -                Thm.implies_intr ct thm
   3.130 -              end
   3.131 -
   3.132 -          | thm_of vars Hs (prf %% prf') =
   3.133 -              let
   3.134 -                val thm = beta_eta_convert (thm_of vars Hs prf);
   3.135 -                val thm' = beta_eta_convert (thm_of vars Hs prf');
   3.136 -              in
   3.137 -                Thm.implies_elim thm thm'
   3.138 -                handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
   3.139 -              end
   3.140 -
   3.141 -          | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
   3.142 -
   3.143 -          | thm_of _ _ _ = error "thm_of_proof: partial proof term";
   3.144 -
   3.145 -      in beta_eta_convert (thm_of ([], prf_names) [] prf) end
   3.146 -  end;
   3.147 -
   3.148 -end;
     4.1 --- a/src/Pure/ROOT.ML	Mon Aug 08 20:47:12 2011 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Mon Aug 08 21:11:10 2011 +0200
     4.3 @@ -175,7 +175,7 @@
     4.4  use "Proof/reconstruct.ML";
     4.5  use "Proof/proof_syntax.ML";
     4.6  use "Proof/proof_rewrite_rules.ML";
     4.7 -use "Proof/proofchecker.ML";
     4.8 +use "Proof/proof_checker.ML";
     4.9  
    4.10  (*outer syntax*)
    4.11  use "Isar/token.ML";