author  wenzelm 
Thu, 11 Oct 2007 19:10:23 +0200  
changeset 24981  4ec3f95190bf 
parent 24259  c9e05c49d02c 
child 29580  117b88da143c 
permissions  rwrr 
24259  1 
(* Title: Pure/primitive_defs.ML 
2 
ID: $Id$ 

3 
Author: Makarius 

4 

5 
Primitive definition forms. 

6 
*) 

7 

8 
signature PRIMITIVE_DEFS = 

9 
sig 

24981
4ec3f95190bf
dest/cert_def: replaced Pretty.pp by explicit Proof.context;
wenzelm
parents:
24259
diff
changeset

10 
val dest_def: Proof.context > (term > bool) > (string > bool) > (string > bool) > 
24259  11 
term > (term * term) * term 
12 
val abs_def: term > term * term 

13 
val mk_defpair: term * term > string * term 

14 
end; 

15 

16 
structure PrimitiveDefs: PRIMITIVE_DEFS = 

17 
struct 

18 

19 
fun term_kind (Const _) = "existing constant " 

20 
 term_kind (Free _) = "free variable " 

21 
 term_kind (Bound _) = "bound variable " 

22 
 term_kind _ = ""; 

23 

24 
(*c x == t[x] to !!x. c x == t[x]*) 

24981
4ec3f95190bf
dest/cert_def: replaced Pretty.pp by explicit Proof.context;
wenzelm
parents:
24259
diff
changeset

25 
fun dest_def ctxt check_head is_fixed is_fixedT eq = 
24259  26 
let 
27 
fun err msg = raise TERM (msg, [eq]); 

28 
val eq_vars = Term.strip_all_vars eq; 

29 
val eq_body = Term.strip_all_body eq; 

30 

31 
val display_terms = 

24981
4ec3f95190bf
dest/cert_def: replaced Pretty.pp by explicit Proof.context;
wenzelm
parents:
24259
diff
changeset

32 
commas_quote o map (Syntax.string_of_term ctxt o Syntax.bound_vars eq_vars); 
4ec3f95190bf
dest/cert_def: replaced Pretty.pp by explicit Proof.context;
wenzelm
parents:
24259
diff
changeset

33 
val display_types = commas_quote o map (Syntax.string_of_typ ctxt); 
24259  34 

35 
val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a metaequality (==)"; 

36 
val lhs = Envir.beta_eta_contract raw_lhs; 

37 
val (head, args) = Term.strip_comb lhs; 

38 
val head_tfrees = Term.add_tfrees head []; 

39 

40 
fun check_arg (Bound _) = true 

41 
 check_arg (Free (x, _)) = not (is_fixed x) 

42 
 check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true 

43 
 check_arg _ = false; 

44 
fun close_arg (Bound _) t = t 

45 
 close_arg x t = Term.all (Term.fastype_of x) $ lambda x t; 

46 

47 
val lhs_bads = filter_out check_arg args; 

48 
val lhs_dups = duplicates (op aconv) args; 

49 
val rhs_extras = Term.fold_aterms (fn v as Free (x, _) => 

50 
if is_fixed x orelse member (op aconv) args v then I 

51 
else insert (op aconv) v  _ => I) rhs []; 

52 
val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) => 

53 
if is_fixedT a orelse member (op =) head_tfrees (a, S) then I 

54 
else insert (op =) v  _ => I)) rhs []; 

55 
in 

56 
if not (check_head head) then 

57 
err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head]) 

58 
else if not (null lhs_bads) then 

59 
err ("Bad arguments on lhs: " ^ display_terms lhs_bads) 

60 
else if not (null lhs_dups) then 

61 
err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups) 

62 
else if not (null rhs_extras) then 

63 
err ("Extra variables on rhs: " ^ display_terms rhs_extras) 

64 
else if not (null rhs_extrasT) then 

65 
err ("Extra type variables on rhs: " ^ display_types rhs_extrasT) 

66 
else if exists_subterm (fn t => t aconv head) rhs then 

67 
err "Entity to be defined occurs on rhs" 

68 
else 

69 
((lhs, rhs), fold_rev close_arg args (Term.list_all (eq_vars, (Logic.mk_equals (lhs, rhs))))) 

70 
end; 

71 

72 
(*!!x. c x == t[x] to c == %x. t[x]*) 

73 
fun abs_def eq = 

74 
let 

75 
val body = Term.strip_all_body eq; 

76 
val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq)); 

77 
val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body)); 

78 
val (lhs', args) = Term.strip_comb lhs; 

79 
val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs); 

80 
in (lhs', rhs') end; 

81 

82 
fun mk_defpair (lhs, rhs) = 

83 
(case Term.head_of lhs of 

84 
Const (name, _) => 

85 
(NameSpace.base name ^ "_def", Logic.mk_equals (lhs, rhs)) 

86 
 _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs])); 

87 

88 
end; 