1(* Title: Pure/primitive_defs.ML 2 Author: Makarius 3 4Primitive definition forms. 5*) 6 7signature PRIMITIVE_DEFS = 8sig 9 val dest_def: Proof.context -> 10 {check_head: term -> bool, 11 check_free_lhs: string -> bool, 12 check_free_rhs: string -> bool, 13 check_tfree: string -> bool} -> 14 term -> (term * term) * term list * term 15 val abs_def: term -> term * term 16end; 17 18structure Primitive_Defs: PRIMITIVE_DEFS = 19struct 20 21fun term_kind (Const _) = "existing constant " 22 | term_kind (Free _) = "free variable " 23 | term_kind (Bound _) = "bound variable " 24 | term_kind _ = ""; 25 26(*c x \<equiv> t[x] to \<And>x. c x \<equiv> t[x]*) 27fun dest_def ctxt {check_head, check_free_lhs, check_free_rhs, check_tfree} eq = 28 let 29 fun err msg = raise TERM (msg, [eq]); 30 val eq_vars = Term.strip_all_vars eq; 31 val eq_body = Term.strip_all_body eq; 32 33 val display_terms = 34 commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars eq_vars); 35 val display_types = commas_quote o map (Syntax.string_of_typ ctxt); 36 37 val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (\<equiv>)"; 38 val lhs = Envir.beta_eta_contract raw_lhs; 39 val (head, args) = Term.strip_comb lhs; 40 val head_tfrees = Term.add_tfrees head []; 41 42 fun check_arg (Bound _) = true 43 | check_arg (Free (x, _)) = check_free_lhs x 44 | check_arg (Const ("Pure.type", Type ("itself", [TFree _]))) = true 45 | check_arg _ = false; 46 fun close_arg (Bound _) t = t 47 | close_arg x t = Logic.all x t; 48 49 val lhs_bads = filter_out check_arg args; 50 val lhs_dups = duplicates (op aconv) args; 51 val rhs_extras = Term.fold_aterms (fn v as Free (x, _) => 52 if check_free_rhs x orelse member (op aconv) args v then I 53 else insert (op aconv) v | _ => I) rhs []; 54 val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) => 55 if check_tfree a orelse member (op =) head_tfrees (a, S) then I 56 else insert (op =) v | _ => I)) rhs []; 57 in 58 if not (check_head head) then 59 err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head]) 60 else if not (null lhs_bads) then 61 err ("Bad arguments on lhs: " ^ display_terms lhs_bads) 62 else if not (null lhs_dups) then 63 err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups) 64 else if not (null rhs_extras) then 65 err ("Extra variables on rhs: " ^ display_terms rhs_extras) 66 else if not (null rhs_extrasT) then 67 err ("Extra type variables on rhs: " ^ display_types rhs_extrasT) 68 else if exists_subterm (fn t => t aconv head) rhs then 69 err "Entity to be defined occurs on rhs" 70 else 71 ((lhs, rhs), args, 72 fold_rev close_arg args (Logic.list_all (eq_vars, (Logic.mk_equals (lhs, rhs))))) 73 end; 74 75(*\<And>x. c x \<equiv> t[x] to c \<equiv> \<lambda>x. t[x]*) 76fun abs_def eq = 77 let 78 val body = Term.strip_all_body eq; 79 val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq)); 80 val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body)); 81 val (lhs', args) = Term.strip_comb lhs; 82 val rhs' = fold_rev (absfree o dest_Free) args rhs; 83 in (lhs', rhs') end; 84 85end; 86