src/Pure/Isar/local_defs.ML
changeset 18950 053e830c25ad
parent 18896 efd9d44a0bdb
child 19585 70a1ce3b23ae
     1.1 --- a/src/Pure/Isar/local_defs.ML	Mon Feb 06 20:59:49 2006 +0100
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Mon Feb 06 20:59:50 2006 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature LOCAL_DEFS =
     1.6  sig
     1.7 -  val cert_def: ProofContext.context -> term -> string * term
     1.8 +  val cert_def: ProofContext.context -> term -> (string * typ) * term
     1.9    val abs_def: term -> (string * typ) * term
    1.10    val mk_def: ProofContext.context -> (string * term) list -> term list
    1.11    val def_export: ProofContext.export
    1.12 @@ -22,7 +22,7 @@
    1.13    val unfold_tac: ProofContext.context -> thm list -> tactic
    1.14    val fold: ProofContext.context -> thm list -> thm -> thm
    1.15    val fold_tac: ProofContext.context -> thm list -> tactic
    1.16 -  val derived_def: ProofContext.context -> term ->
    1.17 +  val derived_def: ProofContext.context -> bool -> term ->
    1.18      ((string * typ) * term) * (ProofContext.context -> term -> thm -> thm)
    1.19  end;
    1.20  
    1.21 @@ -33,48 +33,19 @@
    1.22  
    1.23  (* prepare defs *)
    1.24  
    1.25 -(*c x == t[x] to !!x. c x == t[x]*)
    1.26  fun cert_def ctxt eq =
    1.27    let
    1.28 -    fun err msg = cat_error msg
    1.29 -      ("The error(s) above occurred in definition: " ^ ProofContext.string_of_term ctxt eq);
    1.30 -
    1.31 -    val (lhs, rhs) = Logic.dest_equals (Term.strip_all_body eq)
    1.32 -      handle TERM _ => err "Not a meta-equality (==)";
    1.33 -    val (f, xs) = Term.strip_comb (Pattern.beta_eta_contract lhs);
    1.34 -    val (c, _) = Term.dest_Free f handle TERM _ =>
    1.35 -      err "Head of lhs must be a free/fixed variable";
    1.36 -
    1.37 -    fun check_arg (Bound _) = true
    1.38 -      | check_arg (Free (x, _)) = not (ProofContext.is_fixed ctxt x)
    1.39 -      | check_arg t = (case try Logic.dest_type t of SOME (TFree _) => true | _ => false);
    1.40 -    fun close_arg (Bound _) t = t
    1.41 -      | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t;
    1.42 +    val pp = ProofContext.pp ctxt;
    1.43 +    val display_term = quote o Pretty.string_of_term pp;
    1.44 +    fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^ display_term eq);
    1.45 +    val ((lhs, _), eq') = eq
    1.46 +      |> Sign.no_vars pp
    1.47 +      |> Logic.dest_def pp Term.is_Free (ProofContext.is_fixed ctxt) (K true)
    1.48 +      handle TERM (msg, _) => err msg | ERROR msg => err msg;
    1.49 +  in (Term.dest_Free (Term.head_of lhs), eq') end;
    1.50  
    1.51 -    val extra_frees = Term.fold_aterms (fn v as Free (x, _) =>
    1.52 -      if ProofContext.is_fixed ctxt x orelse member (op aconv) xs v then I
    1.53 -      else insert (op =) x | _ => I) rhs [];
    1.54 -  in
    1.55 -    if not (forall check_arg xs) orelse has_duplicates (op aconv) xs then
    1.56 -      err "Arguments of lhs must be distinct free/bound variables"
    1.57 -    else if not (null extra_frees) then
    1.58 -      err ("Extra free variables on rhs: " ^ commas_quote extra_frees)
    1.59 -    else if Term.exists_subterm (fn t => t = f) rhs then
    1.60 -      err "Element to be defined occurs on rhs"
    1.61 -    else (c, fold_rev close_arg xs eq)
    1.62 -  end;
    1.63 +val abs_def = Logic.abs_def #> apfst Term.dest_Free;
    1.64  
    1.65 -(*!!x. c x == t[x] to c == %x. t[x]*)
    1.66 -fun abs_def eq =
    1.67 -  let
    1.68 -    val body = Term.strip_all_body eq;
    1.69 -    val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
    1.70 -    val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body));
    1.71 -    val (f, xs) = Term.strip_comb (Pattern.beta_eta_contract lhs);
    1.72 -    val eq' = Term.list_abs_free (map Term.dest_Free xs, rhs);
    1.73 -  in (Term.dest_Free f, eq') end;
    1.74 -
    1.75 -(*c == t*)
    1.76  fun mk_def ctxt args =
    1.77    let
    1.78      val (xs, rhss) = split_list args;
    1.79 @@ -86,7 +57,7 @@
    1.80  (* export defs *)
    1.81  
    1.82  fun head_of_def cprop =
    1.83 -  #1 (Term.strip_comb (#1 (Logic.dest_equals (Term.strip_all_body (Thm.term_of cprop)))))
    1.84 +  Term.head_of (#1 (Logic.dest_equals (Term.strip_all_body (Thm.term_of cprop))))
    1.85    |> Thm.cterm_of (Thm.theory_of_cterm cprop);
    1.86  
    1.87  (*
    1.88 @@ -172,16 +143,15 @@
    1.89  
    1.90  (* derived defs -- potentially within the object-logic *)
    1.91  
    1.92 -fun derived_def ctxt prop =
    1.93 +fun derived_def ctxt conditional prop =
    1.94    let
    1.95      val thy = ProofContext.theory_of ctxt;
    1.96      val ((c, T), rhs) = prop
    1.97        |> Thm.cterm_of thy
    1.98        |> meta_rewrite (Context.Proof ctxt)
    1.99        |> (snd o Logic.dest_equals o Thm.prop_of)
   1.100 -      |> Logic.strip_imp_concl
   1.101 -      |> (snd o cert_def ctxt)
   1.102 -      |> abs_def;
   1.103 +      |> K conditional ? Logic.strip_imp_concl
   1.104 +      |> (abs_def o #2 o cert_def ctxt);
   1.105      fun prove ctxt' t def =
   1.106        let
   1.107          val thy' = ProofContext.theory_of ctxt';
   1.108 @@ -197,5 +167,4 @@
   1.109        end;
   1.110    in (((c, T), rhs), prove) end;
   1.111  
   1.112 -
   1.113  end;