src/Pure/Syntax/syntax_trans.ML
changeset 52177 15fcad6eb956
parent 52163 72e83c82c1d4
child 55948 bb21b380f65d
equal deleted inserted replaced
52176:d3ee6315ca22 52177:15fcad6eb956
    37   val atomic_abs_tr': string * typ * term -> term * term
    37   val atomic_abs_tr': string * typ * term -> term * term
    38   val const_abs_tr': term -> term
    38   val const_abs_tr': term -> term
    39   val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term)
    39   val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term)
    40   val preserve_binder_abs_tr': string -> string -> string * (Proof.context -> term list -> term)
    40   val preserve_binder_abs_tr': string -> string -> string * (Proof.context -> term list -> term)
    41   val preserve_binder_abs2_tr': string -> string -> string * (Proof.context -> term list -> term)
    41   val preserve_binder_abs2_tr': string -> string -> string * (Proof.context -> term list -> term)
    42   val prop_tr': term -> term
       
    43   val variant_abs: string * typ * term -> string * term
    42   val variant_abs: string * typ * term -> string * term
    44   val variant_abs': string * typ * term -> string * term
    43   val variant_abs': string * typ * term -> string * term
    45   val dependent_tr': string * string -> term list -> term
    44   val dependent_tr': string * string -> term list -> term
    46   val antiquote_tr': string -> term -> term
    45   val antiquote_tr': string -> term -> term
    47   val quote_tr': string -> term -> term
    46   val quote_tr': string -> term -> term
   376 fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] =
   375 fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] =
   377       Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
   376       Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
   378   | idtyp_ast_tr' _ _ = raise Match;
   377   | idtyp_ast_tr' _ _ = raise Match;
   379 
   378 
   380 
   379 
   381 (* meta propositions *)
       
   382 
       
   383 fun prop_tr' tm =
       
   384   let
       
   385     fun aprop t = Syntax.const "_aprop" $ t;
       
   386 
       
   387     fun is_prop Ts t =
       
   388       fastype_of1 (Ts, t) = propT handle TERM _ => false;
       
   389 
       
   390     fun is_term (Const ("Pure.term", _) $ _) = true
       
   391       | is_term _ = false;
       
   392 
       
   393     fun tr' _ (t as Const _) = t
       
   394       | tr' Ts (t as Const ("_bound", _) $ u) =
       
   395           if is_prop Ts u then aprop t else t
       
   396       | tr' _ (t as Free (x, T)) =
       
   397           if T = propT then aprop (Syntax.free x) else t
       
   398       | tr' _ (t as Var (xi, T)) =
       
   399           if T = propT then aprop (Syntax.var xi) else t
       
   400       | tr' Ts (t as Bound _) =
       
   401           if is_prop Ts t then aprop t else t
       
   402       | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
       
   403       | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
       
   404           if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
       
   405           else tr' Ts t1 $ tr' Ts t2
       
   406       | tr' Ts (t as t1 $ t2) =
       
   407           (if is_Const (Term.head_of t) orelse not (is_prop Ts t)
       
   408             then I else aprop) (tr' Ts t1 $ tr' Ts t2);
       
   409   in tr' [] tm end;
       
   410 
       
   411 
       
   412 (* meta implication *)
   380 (* meta implication *)
   413 
   381 
   414 fun impl_ast_tr' asts =
   382 fun impl_ast_tr' asts =
   415   if no_brackets () then raise Match
   383   if no_brackets () then raise Match
   416   else
   384   else