src/Pure/Proof/proof_syntax.ML
changeset 11614 3131fa12d425
parent 11539 0f17da240450
child 11640 be1bc3b88480
     1.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Sep 28 11:05:37 2001 +0200
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri Sep 28 11:07:40 2001 +0200
     1.3 @@ -31,7 +31,8 @@
     1.4  (**** add special syntax for embedding proof terms ****)
     1.5  
     1.6  val proofT = Type ("proof", []);
     1.7 -val lamT = Type ("lam_syn", []);
     1.8 +val paramT = Type ("param", []);
     1.9 +val paramsT = Type ("params", []);
    1.10  val idtT = Type ("idt", []);
    1.11  val aT = TFree ("'a", ["logic"]);
    1.12  
    1.13 @@ -43,7 +44,7 @@
    1.14    (map (fn name => (name, proofT, NoSyn)) names) (Sign.add_path "//" sg);
    1.15  
    1.16  (** constants for application and abstraction **)
    1.17 -  
    1.18 +
    1.19  fun add_proof_syntax sg =
    1.20    sg
    1.21    |> Sign.copy
    1.22 @@ -52,33 +53,35 @@
    1.23    |> Sign.add_types [("proof", 0, NoSyn)]
    1.24    |> Sign.add_arities [("proof", [], "logic")]
    1.25    |> Sign.add_consts_i
    1.26 -      [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
    1.27 -       ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
    1.28 +      [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
    1.29 +       ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
    1.30         ("Abst", (aT --> proofT) --> proofT, NoSyn),
    1.31         ("AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn)]
    1.32 -  |> Sign.add_nonterminals ["lam_syn"]
    1.33 +  |> Sign.add_nonterminals ["param", "params"]
    1.34    |> Sign.add_syntax_i
    1.35 -      [("_Lam", [lamT, proofT] ---> proofT, Mixfix ("(3Lam _./ _)", [0,0], 1)),
    1.36 -       ("_Lam0", [lamT, lamT] ---> lamT, Mixfix ("_,/ _", [1, 0], 0)),
    1.37 -       ("_Lam1", [idtT, propT] ---> lamT, Mixfix ("_ : _", [0, 0], 1)),
    1.38 -       ("_Lam2", idtT --> lamT, Mixfix ("_", [0], 1))]
    1.39 +      [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(3Lam _./ _)", [0, 3], 3)),
    1.40 +       ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
    1.41 +       ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
    1.42 +       ("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)),
    1.43 +       ("", paramT --> paramT, Delimfix "'(_')"),
    1.44 +       ("", idtT --> paramsT, Delimfix "_"),
    1.45 +       ("", paramT --> paramsT, Delimfix "_")]
    1.46    |> Sign.add_modesyntax_i (("xsymbols", true),
    1.47 -      [("_Lam", [lamT, proofT] ---> proofT, Mixfix ("(3\\<Lambda>_./ _)", [0,0], 1)),
    1.48 +      [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(3\\<Lambda>_./ _)", [0, 3], 3)),
    1.49         ("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
    1.50         ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))])
    1.51    |> Sign.add_trrules_i (map Syntax.ParsePrintRule
    1.52        [(Syntax.mk_appl (Constant "_Lam")
    1.53 +          [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],
    1.54 +        Syntax.mk_appl (Constant "_Lam")
    1.55 +          [Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]),
    1.56 +       (Syntax.mk_appl (Constant "_Lam")
    1.57            [Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"],
    1.58          Syntax.mk_appl (Constant "AbsP") [Variable "A",
    1.59            (Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]),
    1.60 -       (Syntax.mk_appl (Constant "_Lam")
    1.61 -          [Syntax.mk_appl (Constant "_Lam2") [Variable "x"], Variable "A"],
    1.62 +       (Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"],
    1.63          Syntax.mk_appl (Constant "Abst")
    1.64 -          [(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])]),
    1.65 -       (Syntax.mk_appl (Constant "_Lam")
    1.66 -          [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],
    1.67 -        Syntax.mk_appl (Constant "_Lam")
    1.68 -          [Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]])]);
    1.69 +          [(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]);
    1.70  
    1.71  
    1.72  (**** create unambiguous theorem names ****)
    1.73 @@ -99,8 +102,8 @@
    1.74  
    1.75      fun rename (Abst (s, T, prf)) = Abst (s, T, rename prf)
    1.76        | rename (AbsP (s, t, prf)) = AbsP (s, t, rename prf)
    1.77 -      | rename (prf1 % prf2) = rename prf1 % rename prf2
    1.78 -      | rename (prf %% t) = rename prf %% t
    1.79 +      | rename (prf1 %% prf2) = rename prf1 %% rename prf2
    1.80 +      | rename (prf % t) = rename prf % t
    1.81        | rename (prf' as PThm ((s, tags), prf, prop, Ts)) =
    1.82            let
    1.83              val prop' = if_none (assoc (thms', s)) (Bound 0);
    1.84 @@ -126,18 +129,21 @@
    1.85      val thms = flat (map thms_of thys);
    1.86      val axms = flat (map (Symtab.dest o #axioms o rep_theory) thys);
    1.87  
    1.88 +    fun mk_term t = (if ty then I else map_term_types (K dummyT))
    1.89 +      (Term.no_dummy_patterns t);
    1.90 +
    1.91      fun prf_of [] (Bound i) = PBound i
    1.92        | prf_of Ts (Const (s, Type ("proof", _))) =
    1.93            change_type (if ty then Some Ts else None)
    1.94              (case NameSpace.unpack s of
    1.95 -               "Axm" :: xs =>
    1.96 +               "axm" :: xs =>
    1.97                   let
    1.98                     val name = NameSpace.pack xs;
    1.99                     val prop = (case assoc (axms, name) of
   1.100                         Some prop => prop
   1.101                       | None => error ("Unknown axiom " ^ quote name))
   1.102                   in PAxm (name, prop, None) end
   1.103 -             | "Thm" :: xs =>
   1.104 +             | "thm" :: xs =>
   1.105                   let val name = NameSpace.pack xs;
   1.106                   in (case assoc (thms, name) of
   1.107                       Some thm => fst (strip_combt (#2 (#der (rep_thm thm))))
   1.108 @@ -151,14 +157,17 @@
   1.109            Abst (s, if ty then Some T else None,
   1.110              incr_pboundvars (~1) 0 (prf_of [] prf))
   1.111        | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) =
   1.112 -          AbsP (s, case t of Const ("dummy_pattern", _) => None | _ => Some t,
   1.113 +          AbsP (s, case t of
   1.114 +                Const ("dummy_pattern", _) => None
   1.115 +              | _ $ Const ("dummy_pattern", _) => None
   1.116 +              | _ => Some (mk_term t),
   1.117              incr_pboundvars 0 (~1) (prf_of [] prf))
   1.118        | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =
   1.119 -          prf_of [] prf1 % prf_of [] prf2
   1.120 +          prf_of [] prf1 %% prf_of [] prf2
   1.121        | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) =
   1.122            prf_of (T::Ts) prf
   1.123 -      | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %%
   1.124 -          (case t of Const ("dummy_pattern", _) => None | _ => Some t)
   1.125 +      | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %
   1.126 +          (case t of Const ("dummy_pattern", _) => None | _ => Some (mk_term t))
   1.127        | prf_of _ t = error ("Not a proof term:\n" ^
   1.128            Sign.string_of_term (sign_of thy) t)
   1.129  
   1.130 @@ -175,12 +184,12 @@
   1.131    [proofT, itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
   1.132  
   1.133  fun term_of _ (PThm ((name, _), _, _, None)) =
   1.134 -      Const (add_prefix "Thm" name, proofT)
   1.135 +      Const (add_prefix "thm" name, proofT)
   1.136    | term_of _ (PThm ((name, _), _, _, Some Ts)) =
   1.137 -      mk_tyapp (Const (add_prefix "Thm" name, proofT), Ts)
   1.138 -  | term_of _ (PAxm (name, _, None)) = Const (add_prefix "Axm" name, proofT)
   1.139 +      mk_tyapp (Const (add_prefix "thm" name, proofT), Ts)
   1.140 +  | term_of _ (PAxm (name, _, None)) = Const (add_prefix "axm" name, proofT)
   1.141    | term_of _ (PAxm (name, _, Some Ts)) =
   1.142 -      mk_tyapp (Const (add_prefix "Axm" name, proofT), Ts)
   1.143 +      mk_tyapp (Const (add_prefix "axm" name, proofT), Ts)
   1.144    | term_of _ (PBound i) = Bound i
   1.145    | term_of Ts (Abst (s, opT, prf)) = 
   1.146        let val T = if_none opT dummyT
   1.147 @@ -190,9 +199,9 @@
   1.148    | term_of Ts (AbsP (s, t, prf)) =
   1.149        AbsPt $ if_none t (Const ("dummy_pattern", propT)) $
   1.150          Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf))
   1.151 -  | term_of Ts (prf1 % prf2) =
   1.152 +  | term_of Ts (prf1 %% prf2) =
   1.153        AppPt $ term_of Ts prf1 $ term_of Ts prf2
   1.154 -  | term_of Ts (prf %% opt) = 
   1.155 +  | term_of Ts (prf % opt) = 
   1.156        let val t = if_none opt (Const ("dummy_pattern", dummyT))
   1.157        in Const ("Appt",
   1.158          [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $
   1.159 @@ -214,7 +223,7 @@
   1.160      val sg = sign_of thy |>
   1.161        add_proof_syntax |>
   1.162        add_proof_atom_consts
   1.163 -        (map (add_prefix "Thm") thm_names @ map (add_prefix "Axm") axm_names)
   1.164 +        (map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
   1.165    in
   1.166      (cterm_of sg (term_of_proof prf'),
   1.167       proof_of_term thy tab true o Thm.term_of)
   1.168 @@ -228,7 +237,7 @@
   1.169      val sg = sign_of thy |>
   1.170        add_proof_syntax |>
   1.171        add_proof_atom_consts
   1.172 -        (map (add_prefix "Thm") thm_names @ map (add_prefix "Axm") axm_names)
   1.173 +        (map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
   1.174    in
   1.175      (fn T => fn s => Thm.term_of (read_cterm sg (s, T)))
   1.176    end;
   1.177 @@ -246,7 +255,7 @@
   1.178      val sg' = sg |>
   1.179        add_proof_syntax |>
   1.180        add_proof_atom_consts
   1.181 -        (map (add_prefix "Thm") thm_names @ map (add_prefix "Axm") axm_names)
   1.182 +        (map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
   1.183    in
   1.184      Sign.pretty_term sg' (term_of_proof prf)
   1.185    end;
   1.186 @@ -259,7 +268,7 @@
   1.187        | _ => prf)
   1.188    in
   1.189      pretty_proof sign
   1.190 -      (if full then Reconstruct.reconstruct_prf sign prop prf' else prf')
   1.191 +      (if full then Reconstruct.reconstruct_proof sign prop prf' else prf')
   1.192    end;
   1.193  
   1.194  val print_proof_of = Pretty.writeln oo pretty_proof_of;