src/Pure/Isar/local_defs.ML
changeset 18875 853fa34047a4
parent 18859 75248f8badc9
child 18896 efd9d44a0bdb
     1.1 --- a/src/Pure/Isar/local_defs.ML	Tue Jan 31 18:19:29 2006 +0100
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Tue Jan 31 18:19:30 2006 +0100
     1.3 @@ -7,9 +7,9 @@
     1.4  
     1.5  signature LOCAL_DEFS =
     1.6  sig
     1.7 -  val mk_def: ProofContext.context -> (string * term) list -> term list
     1.8    val cert_def: ProofContext.context -> term -> string * 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    val add_def: string * term -> ProofContext.context ->
    1.13      ((string * typ) * thm) * ProofContext.context
    1.14 @@ -17,11 +17,11 @@
    1.15    val defn_add: attribute
    1.16    val defn_del: attribute
    1.17    val meta_rewrite_rule: Context.generic -> thm -> thm
    1.18 -  val unfold: ProofContext.context -> bool -> thm list -> thm -> thm
    1.19 -  val unfold_goals: ProofContext.context -> bool -> thm list -> thm -> thm
    1.20 -  val unfold_tac: ProofContext.context -> bool -> thm list -> tactic
    1.21 -  val fold: ProofContext.context -> bool -> thm list -> thm -> thm
    1.22 -  val fold_tac: ProofContext.context -> bool -> thm list -> tactic
    1.23 +  val unfold: ProofContext.context -> thm list -> thm -> thm
    1.24 +  val unfold_goals: ProofContext.context -> thm list -> thm -> thm
    1.25 +  val unfold_tac: ProofContext.context -> thm list -> tactic
    1.26 +  val fold: ProofContext.context -> thm list -> thm -> thm
    1.27 +  val fold_tac: ProofContext.context -> thm list -> tactic
    1.28    val derived_def: ProofContext.context -> term ->
    1.29      ((string * typ) * term) * (ProofContext.context -> term -> thm -> thm)
    1.30  end;
    1.31 @@ -33,13 +33,7 @@
    1.32  
    1.33  (* prepare defs *)
    1.34  
    1.35 -fun mk_def ctxt args =
    1.36 -  let
    1.37 -    val (xs, rhss) = split_list args;
    1.38 -    val (bind, _) = ProofContext.bind_fixes xs ctxt;
    1.39 -    val lhss = map (fn (x, rhs) => bind (Free (x, Term.fastype_of rhs))) args;
    1.40 -  in map Logic.mk_equals (lhss ~~ rhss) end;
    1.41 -
    1.42 +(*c x == t[x] to !!x. c x == t[x]*)
    1.43  fun cert_def ctxt eq =
    1.44    let
    1.45      fun err msg = cat_error msg
    1.46 @@ -54,15 +48,14 @@
    1.47      fun check_arg (Bound _) = true
    1.48        | check_arg (Free (x, _)) = not (ProofContext.is_fixed ctxt x)
    1.49        | check_arg t = (case try Logic.dest_type t of SOME (TFree _) => true | _ => false);
    1.50 -    fun close_arg (Free (x, T)) t = Term.all T $ Term.absfree (x, T, t)
    1.51 -      | close_arg (Const ("TYPE", T)) t = Term.all T $ Term.absdummy (T, t)
    1.52 -      | close_arg _ t = t;
    1.53 +    fun close_arg (Bound _) t = t
    1.54 +      | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t;
    1.55  
    1.56      val extra_frees = Term.fold_aterms (fn v as Free (x, _) =>
    1.57        if ProofContext.is_fixed ctxt x orelse member (op aconv) xs v then I
    1.58        else insert (op =) x | _ => I) rhs [];
    1.59    in
    1.60 -    if not (forall check_arg xs) orelse has_duplicates (op =) xs then
    1.61 +    if not (forall check_arg xs) orelse has_duplicates (op aconv) xs then
    1.62        err "Arguments of lhs must be distinct free/bound variables"
    1.63      else if not (null extra_frees) then
    1.64        err ("Extra free variables on rhs: " ^ commas_quote extra_frees)
    1.65 @@ -71,6 +64,7 @@
    1.66      else (c, fold_rev close_arg xs eq)
    1.67    end;
    1.68  
    1.69 +(*!!x. c x == t[x] to c == %x. t[x]*)
    1.70  fun abs_def eq =
    1.71    let
    1.72      val body = Term.strip_all_body eq;
    1.73 @@ -80,6 +74,14 @@
    1.74      val eq' = Term.list_abs_free (map Term.dest_Free xs, rhs);
    1.75    in (Term.dest_Free f, eq') end;
    1.76  
    1.77 +(*c == t*)
    1.78 +fun mk_def ctxt args =
    1.79 +  let
    1.80 +    val (xs, rhss) = split_list args;
    1.81 +    val (bind, _) = ProofContext.bind_fixes xs ctxt;
    1.82 +    val lhss = map (fn (x, rhs) => bind (Free (x, Term.fastype_of rhs))) args;
    1.83 +  in map Logic.mk_equals (lhss ~~ rhss) end;
    1.84 +
    1.85  
    1.86  (* export defs *)
    1.87  
    1.88 @@ -87,6 +89,14 @@
    1.89    #1 (Term.strip_comb (#1 (Logic.dest_equals (Term.strip_all_body (Thm.term_of cprop)))))
    1.90    |> Thm.cterm_of (Thm.theory_of_cterm cprop);
    1.91  
    1.92 +(*
    1.93 +  [x]
    1.94 +  [x == t]
    1.95 +     :
    1.96 +    B x
    1.97 +  --------
    1.98 +    B t
    1.99 +*)
   1.100  fun def_export _ cprops thm =
   1.101    thm
   1.102    |> Drule.implies_intr_list cprops
   1.103 @@ -134,7 +144,7 @@
   1.104  val defn_del = Thm.declaration_attribute (Rules.map o Drule.del_rule);
   1.105  
   1.106  
   1.107 -(* transform rewrite rules *)
   1.108 +(* meta rewrite rules *)
   1.109  
   1.110  val equals_ss =
   1.111    MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss
   1.112 @@ -149,14 +159,16 @@
   1.113  fun meta_rewrite_tac ctxt i =
   1.114    PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (meta_rewrite (Context.Proof ctxt))));
   1.115  
   1.116 -fun transformed f _ false = f
   1.117 -  | transformed f ctxt true = f o map (meta_rewrite_rule (Context.Proof ctxt));
   1.118 +
   1.119 +(* rewriting with object-level rules *)
   1.120 +
   1.121 +fun meta f ctxt = f o map (meta_rewrite_rule (Context.Proof ctxt));
   1.122  
   1.123 -val unfold       = transformed Tactic.rewrite_rule;
   1.124 -val unfold_goals = transformed Tactic.rewrite_goals_rule;
   1.125 -val unfold_tac   = transformed Tactic.rewrite_goals_tac;
   1.126 -val fold         = transformed Tactic.fold_rule;
   1.127 -val fold_tac     = transformed Tactic.fold_goals_tac;
   1.128 +val unfold       = meta Tactic.rewrite_rule;
   1.129 +val unfold_goals = meta Tactic.rewrite_goals_rule;
   1.130 +val unfold_tac   = meta Tactic.rewrite_goals_tac;
   1.131 +val fold         = meta Tactic.fold_rule;
   1.132 +val fold_tac     = meta Tactic.fold_goals_tac;
   1.133  
   1.134  
   1.135  (* derived defs -- potentially within the object-logic *)