src/Pure/Proof/proof_syntax.ML
changeset 11522 42fbb6abed5a
child 11539 0f17da240450
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri Aug 31 16:17:05 2001 +0200
     1.3 @@ -0,0 +1,267 @@
     1.4 +(*  Title:      Pure/Proof/proof_syntax.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Stefan Berghofer
     1.7 +    Copyright   2000  TU Muenchen
     1.8 +
     1.9 +Function for parsing and printing proof terms.
    1.10 +*)
    1.11 +
    1.12 +signature PROOF_SYNTAX =
    1.13 +sig
    1.14 +  val proofT : typ
    1.15 +  val add_proof_syntax : Sign.sg -> Sign.sg
    1.16 +  val disambiguate_names : theory -> Proofterm.proof ->
    1.17 +    Proofterm.proof * Proofterm.proof Symtab.table
    1.18 +  val proof_of_term : theory -> Proofterm.proof Symtab.table ->
    1.19 +    bool -> term -> Proofterm.proof
    1.20 +  val term_of_proof : Proofterm.proof -> term
    1.21 +  val cterm_of_proof : theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)
    1.22 +  val read_term : theory -> typ -> string -> term
    1.23 +  val read_proof : theory -> bool -> string -> Proofterm.proof
    1.24 +  val pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T
    1.25 +  val pretty_proof_of : bool -> thm -> Pretty.T
    1.26 +  val print_proof_of : bool -> thm -> unit
    1.27 +end;
    1.28 +
    1.29 +structure ProofSyntax : PROOF_SYNTAX =
    1.30 +struct
    1.31 +
    1.32 +open Proofterm;
    1.33 +
    1.34 +(**** add special syntax for embedding proof terms ****)
    1.35 +
    1.36 +val proofT = Type ("proof", []);
    1.37 +val lamT = Type ("lam_syn", []);
    1.38 +val idtT = Type ("idt", []);
    1.39 +val aT = TFree ("'a", ["logic"]);
    1.40 +
    1.41 +(** constants for theorems and axioms **)
    1.42 +
    1.43 +fun add_prefix a b = NameSpace.pack (a :: NameSpace.unpack b);
    1.44 +
    1.45 +fun add_proof_atom_consts names sg = Sign.add_consts_i
    1.46 +  (map (fn name => (name, proofT, NoSyn)) names) (Sign.add_path "//" sg);
    1.47 +
    1.48 +(** constants for application and abstraction **)
    1.49 +  
    1.50 +fun add_proof_syntax sg =
    1.51 +  sg
    1.52 +  |> Sign.copy
    1.53 +  |> Sign.add_path "/"
    1.54 +  |> Sign.add_defsort_i ["logic"]
    1.55 +  |> Sign.add_types [("proof", 0, NoSyn)]
    1.56 +  |> Sign.add_arities [("proof", [], "logic")]
    1.57 +  |> Sign.add_consts_i
    1.58 +      [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
    1.59 +       ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
    1.60 +       ("Abst", (aT --> proofT) --> proofT, NoSyn),
    1.61 +       ("AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn)]
    1.62 +  |> Sign.add_nonterminals ["lam_syn"]
    1.63 +  |> Sign.add_syntax_i
    1.64 +      [("_Lam", [lamT, proofT] ---> proofT, Mixfix ("(3Lam _./ _)", [0,0], 1)),
    1.65 +       ("_Lam0", [lamT, lamT] ---> lamT, Mixfix ("_,/ _", [1, 0], 0)),
    1.66 +       ("_Lam1", [idtT, propT] ---> lamT, Mixfix ("_ : _", [0, 0], 1)),
    1.67 +       ("_Lam2", idtT --> lamT, Mixfix ("_", [0], 1))]
    1.68 +  |> Sign.add_modesyntax_i (("xsymbols", true),
    1.69 +      [("_Lam", [lamT, proofT] ---> proofT, Mixfix ("(3\\<Lambda>_./ _)", [0,0], 1)),
    1.70 +       ("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
    1.71 +       ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))])
    1.72 +  |> Sign.add_trrules_i (map Syntax.ParsePrintRule
    1.73 +      [(Syntax.mk_appl (Constant "_Lam")
    1.74 +          [Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"],
    1.75 +        Syntax.mk_appl (Constant "AbsP") [Variable "A",
    1.76 +          (Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]),
    1.77 +       (Syntax.mk_appl (Constant "_Lam")
    1.78 +          [Syntax.mk_appl (Constant "_Lam2") [Variable "x"], Variable "A"],
    1.79 +        Syntax.mk_appl (Constant "Abst")
    1.80 +          [(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])]),
    1.81 +       (Syntax.mk_appl (Constant "_Lam")
    1.82 +          [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],
    1.83 +        Syntax.mk_appl (Constant "_Lam")
    1.84 +          [Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]])]);
    1.85 +
    1.86 +
    1.87 +(**** create unambiguous theorem names ****)
    1.88 +
    1.89 +fun disambiguate_names thy prf =
    1.90 +  let
    1.91 +    val thms = thms_of_proof Symtab.empty prf;
    1.92 +    val thms' = map (apsnd (#prop o rep_thm)) (flat
    1.93 +      (map PureThy.thms_of (thy :: Theory.ancestors_of thy)));
    1.94 +
    1.95 +    val tab = Symtab.foldl (fn (tab, (key, ps)) =>
    1.96 +      let val prop = if_none (assoc (thms', key)) (Bound 0)
    1.97 +      in fst (foldr (fn ((prop', prf), x as (tab, i)) =>
    1.98 +        if prop <> prop' then
    1.99 +          (Symtab.update ((key ^ "_" ^ string_of_int i, prf), tab), i+1)
   1.100 +        else x) (ps, (tab, 1)))
   1.101 +      end) (Symtab.empty, thms);
   1.102 +
   1.103 +    fun rename (Abst (s, T, prf)) = Abst (s, T, rename prf)
   1.104 +      | rename (AbsP (s, t, prf)) = AbsP (s, t, rename prf)
   1.105 +      | rename (prf1 % prf2) = rename prf1 % rename prf2
   1.106 +      | rename (prf %% t) = rename prf %% t
   1.107 +      | rename (prf' as PThm ((s, tags), prf, prop, Ts)) =
   1.108 +          let
   1.109 +            val prop' = if_none (assoc (thms', s)) (Bound 0);
   1.110 +            val ps = map fst (the (Symtab.lookup (thms, s))) \ prop'
   1.111 +          in if prop = prop' then prf' else
   1.112 +            PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags),
   1.113 +              prf, prop, Ts)
   1.114 +          end
   1.115 +      | rename prf = prf
   1.116 +
   1.117 +  in (rename prf, tab) end;
   1.118 +
   1.119 +
   1.120 +(**** translation between proof terms and pure terms ****)
   1.121 +
   1.122 +fun change_type T (PThm (name, prf, prop, _)) = PThm (name, prf, prop, T)
   1.123 +  | change_type T (PAxm (name, prop, _)) = PAxm (name, prop, T)
   1.124 +  | change_type _ _ = error "Not a proper theorem";
   1.125 +
   1.126 +fun proof_of_term thy tab ty =
   1.127 +  let
   1.128 +    val thys = thy :: Theory.ancestors_of thy;
   1.129 +    val thms = flat (map thms_of thys);
   1.130 +    val axms = flat (map (Symtab.dest o #axioms o rep_theory) thys);
   1.131 +
   1.132 +    fun prf_of [] (Bound i) = PBound i
   1.133 +      | prf_of Ts (Const (s, Type ("proof", _))) =
   1.134 +          change_type (if ty then Some Ts else None)
   1.135 +            (case NameSpace.unpack s of
   1.136 +               "Axm" :: xs =>
   1.137 +                 let
   1.138 +                   val name = NameSpace.pack xs;
   1.139 +                   val prop = (case assoc (axms, name) of
   1.140 +                       Some prop => prop
   1.141 +                     | None => error ("Unknown axiom " ^ quote name))
   1.142 +                 in PAxm (name, prop, None) end
   1.143 +             | "Thm" :: xs =>
   1.144 +                 let val name = NameSpace.pack xs;
   1.145 +                 in (case assoc (thms, name) of
   1.146 +                     Some thm => fst (strip_combt (#2 (#der (rep_thm thm))))
   1.147 +                   | None => (case Symtab.lookup (tab, name) of
   1.148 +                         Some prf => prf
   1.149 +                       | None => error ("Unknown theorem " ^ quote name)))
   1.150 +                 end
   1.151 +             | _ => error ("Illegal proof constant name: " ^ quote s))
   1.152 +      | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v
   1.153 +      | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) =
   1.154 +          Abst (s, if ty then Some T else None,
   1.155 +            incr_pboundvars (~1) 0 (prf_of [] prf))
   1.156 +      | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) =
   1.157 +          AbsP (s, case t of Const ("dummy_pattern", _) => None | _ => Some t,
   1.158 +            incr_pboundvars 0 (~1) (prf_of [] prf))
   1.159 +      | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =
   1.160 +          prf_of [] prf1 % prf_of [] prf2
   1.161 +      | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) =
   1.162 +          prf_of (T::Ts) prf
   1.163 +      | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %%
   1.164 +          (case t of Const ("dummy_pattern", _) => None | _ => Some t)
   1.165 +      | prf_of _ t = error ("Not a proof term:\n" ^
   1.166 +          Sign.string_of_term (sign_of thy) t)
   1.167 +
   1.168 +  in prf_of [] end;
   1.169 +
   1.170 +
   1.171 +val AbsPt = Const ("AbsP", [propT, proofT --> proofT] ---> proofT);
   1.172 +val AppPt = Const ("AppP", [proofT, proofT] ---> proofT);
   1.173 +val Hypt = Free ("Hyp", propT --> proofT);
   1.174 +val Oraclet = Free ("Oracle", propT --> proofT);
   1.175 +val MinProoft = Free ("?", proofT);
   1.176 +
   1.177 +val mk_tyapp = foldl (fn (prf, T) => Const ("Appt",
   1.178 +  [proofT, itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
   1.179 +
   1.180 +fun term_of _ (PThm ((name, _), _, _, None)) =
   1.181 +      Const (add_prefix "Thm" name, proofT)
   1.182 +  | term_of _ (PThm ((name, _), _, _, Some Ts)) =
   1.183 +      mk_tyapp (Const (add_prefix "Thm" name, proofT), Ts)
   1.184 +  | term_of _ (PAxm (name, _, None)) = Const (add_prefix "Axm" name, proofT)
   1.185 +  | term_of _ (PAxm (name, _, Some Ts)) =
   1.186 +      mk_tyapp (Const (add_prefix "Axm" name, proofT), Ts)
   1.187 +  | term_of _ (PBound i) = Bound i
   1.188 +  | term_of Ts (Abst (s, opT, prf)) = 
   1.189 +      let val T = if_none opT dummyT
   1.190 +      in Const ("Abst", (T --> proofT) --> proofT) $
   1.191 +        Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf))
   1.192 +      end
   1.193 +  | term_of Ts (AbsP (s, t, prf)) =
   1.194 +      AbsPt $ if_none t (Const ("dummy_pattern", propT)) $
   1.195 +        Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf))
   1.196 +  | term_of Ts (prf1 % prf2) =
   1.197 +      AppPt $ term_of Ts prf1 $ term_of Ts prf2
   1.198 +  | term_of Ts (prf %% opt) = 
   1.199 +      let val t = if_none opt (Const ("dummy_pattern", dummyT))
   1.200 +      in Const ("Appt",
   1.201 +        [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $
   1.202 +          term_of Ts prf $ t
   1.203 +      end
   1.204 +  | term_of Ts (Hyp t) = Hypt $ t
   1.205 +  | term_of Ts (Oracle (_, t, _)) = Oraclet $ t
   1.206 +  | term_of Ts (MinProof _) = MinProoft;
   1.207 +
   1.208 +val term_of_proof = term_of [];
   1.209 +
   1.210 +fun cterm_of_proof thy prf =
   1.211 +  let
   1.212 +    val (prf', tab) = disambiguate_names thy prf;
   1.213 +    val thys = thy :: Theory.ancestors_of thy;
   1.214 +    val thm_names = filter_out (equal "") (map fst (flat (map thms_of thys))) @
   1.215 +      map fst (Symtab.dest tab);
   1.216 +    val axm_names = map fst (flat (map (Symtab.dest o #axioms o rep_theory) thys));
   1.217 +    val sg = sign_of thy |>
   1.218 +      add_proof_syntax |>
   1.219 +      add_proof_atom_consts
   1.220 +        (map (add_prefix "Thm") thm_names @ map (add_prefix "Axm") axm_names)
   1.221 +  in
   1.222 +    (cterm_of sg (term_of_proof prf'),
   1.223 +     proof_of_term thy tab true o Thm.term_of)
   1.224 +  end;
   1.225 +
   1.226 +fun read_term thy =
   1.227 +  let
   1.228 +    val thys = thy :: Theory.ancestors_of thy;
   1.229 +    val thm_names = filter_out (equal "") (map fst (flat (map thms_of thys)));
   1.230 +    val axm_names = map fst (flat (map (Symtab.dest o #axioms o rep_theory) thys));
   1.231 +    val sg = sign_of thy |>
   1.232 +      add_proof_syntax |>
   1.233 +      add_proof_atom_consts
   1.234 +        (map (add_prefix "Thm") thm_names @ map (add_prefix "Axm") axm_names)
   1.235 +  in
   1.236 +    (fn T => fn s => Thm.term_of (read_cterm sg (s, T)))
   1.237 +  end;
   1.238 +
   1.239 +fun read_proof thy =
   1.240 +  let val rd = read_term thy proofT
   1.241 +  in
   1.242 +    (fn ty => fn s => proof_of_term thy Symtab.empty ty (Logic.varify (rd s)))
   1.243 +  end;
   1.244 +
   1.245 +fun pretty_proof sg prf =
   1.246 +  let
   1.247 +    val thm_names = map fst (Symtab.dest (thms_of_proof Symtab.empty prf)) \ "";
   1.248 +    val axm_names = map fst (Symtab.dest (axms_of_proof Symtab.empty prf));
   1.249 +    val sg' = sg |>
   1.250 +      add_proof_syntax |>
   1.251 +      add_proof_atom_consts
   1.252 +        (map (add_prefix "Thm") thm_names @ map (add_prefix "Axm") axm_names)
   1.253 +  in
   1.254 +    Sign.pretty_term sg' (term_of_proof prf)
   1.255 +  end;
   1.256 +
   1.257 +fun pretty_proof_of full thm =
   1.258 +  let
   1.259 +    val {sign, der = (_, prf), prop, ...} = rep_thm thm;
   1.260 +    val prf' = (case strip_combt (fst (strip_combP prf)) of
   1.261 +        (PThm (_, prf', prop', _), _) => if prop=prop' then prf' else prf
   1.262 +      | _ => prf)
   1.263 +  in
   1.264 +    pretty_proof sign
   1.265 +      (if full then Reconstruct.reconstruct_prf sign prop prf' else prf')
   1.266 +  end;
   1.267 +
   1.268 +val print_proof_of = Pretty.writeln oo pretty_proof_of;
   1.269 +
   1.270 +end;