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";