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 |