src/Pure/Isar/local_defs.ML
author wenzelm
Wed, 02 Aug 2006 22:27:00 +0200
changeset 20306 614b7e6c6276
parent 20224 9c40a144ee0e
child 20887 ec9a1bb086da
permissions -rw-r--r--
normalized Proof.context/method type aliases; simplified Assumption/ProofContext.export;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18830
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/local_defs.ML
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
     4
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
     5
Local definitions.
18830
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
     6
*)
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
     7
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
     8
signature LOCAL_DEFS =
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
     9
sig
20306
614b7e6c6276 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    10
  val cert_def: Proof.context -> term -> (string * typ) * term
18830
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    11
  val abs_def: term -> (string * typ) * term
20306
614b7e6c6276 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    12
  val mk_def: Proof.context -> (string * term) list -> term list
20224
9c40a144ee0e moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents: 20049
diff changeset
    13
  val def_export: Assumption.export
20306
614b7e6c6276 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    14
  val add_def: string * term -> Proof.context -> ((string * typ) * thm) * Proof.context
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
    15
  val print_rules: Context.generic -> unit
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
    16
  val defn_add: attribute
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
    17
  val defn_del: attribute
18859
75248f8badc9 export meta_rewrite_rule;
wenzelm
parents: 18840
diff changeset
    18
  val meta_rewrite_rule: Context.generic -> thm -> thm
20306
614b7e6c6276 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    19
  val unfold: Proof.context -> thm list -> thm -> thm
614b7e6c6276 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    20
  val unfold_goals: Proof.context -> thm list -> thm -> thm
614b7e6c6276 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    21
  val unfold_tac: Proof.context -> thm list -> tactic
614b7e6c6276 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    22
  val fold: Proof.context -> thm list -> thm -> thm
614b7e6c6276 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    23
  val fold_tac: Proof.context -> thm list -> tactic
614b7e6c6276 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    24
  val derived_def: Proof.context -> bool -> term ->
614b7e6c6276 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    25
    ((string * typ) * term) * (Proof.context -> term -> thm -> thm)
18830
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    26
end;
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    27
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    28
structure LocalDefs: LOCAL_DEFS =
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    29
struct
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    30
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
    31
(** primitive definitions **)
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
    32
18830
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    33
(* prepare defs *)
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    34
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    35
fun cert_def ctxt eq =
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    36
  let
18950
053e830c25ad cert_def: use Logic.dest_def;
wenzelm
parents: 18896
diff changeset
    37
    val pp = ProofContext.pp ctxt;
053e830c25ad cert_def: use Logic.dest_def;
wenzelm
parents: 18896
diff changeset
    38
    val display_term = quote o Pretty.string_of_term pp;
053e830c25ad cert_def: use Logic.dest_def;
wenzelm
parents: 18896
diff changeset
    39
    fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^ display_term eq);
053e830c25ad cert_def: use Logic.dest_def;
wenzelm
parents: 18896
diff changeset
    40
    val ((lhs, _), eq') = eq
053e830c25ad cert_def: use Logic.dest_def;
wenzelm
parents: 18896
diff changeset
    41
      |> Sign.no_vars pp
19897
fe661eb3b0e7 ProofContext: moved variable operations to struct Variable;
wenzelm
parents: 19585
diff changeset
    42
      |> Logic.dest_def pp Term.is_Free (Variable.is_fixed ctxt) (K true)
18950
053e830c25ad cert_def: use Logic.dest_def;
wenzelm
parents: 18896
diff changeset
    43
      handle TERM (msg, _) => err msg | ERROR msg => err msg;
053e830c25ad cert_def: use Logic.dest_def;
wenzelm
parents: 18896
diff changeset
    44
  in (Term.dest_Free (Term.head_of lhs), eq') end;
18830
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    45
18950
053e830c25ad cert_def: use Logic.dest_def;
wenzelm
parents: 18896
diff changeset
    46
val abs_def = Logic.abs_def #> apfst Term.dest_Free;
18830
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    47
18875
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
    48
fun mk_def ctxt args =
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
    49
  let
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
    50
    val (xs, rhss) = split_list args;
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
    51
    val (bind, _) = ProofContext.bind_fixes xs ctxt;
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
    52
    val lhss = map (fn (x, rhs) => bind (Free (x, Term.fastype_of rhs))) args;
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
    53
  in map Logic.mk_equals (lhss ~~ rhss) end;
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
    54
18830
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    55
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    56
(* export defs *)
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    57
20021
815393c02db9 def_export: Drule.generalize;
wenzelm
parents: 19897
diff changeset
    58
val head_of_def =
815393c02db9 def_export: Drule.generalize;
wenzelm
parents: 19897
diff changeset
    59
  #1 o Term.dest_Free o Term.head_of o #1 o Logic.dest_equals o Term.strip_all_body o Thm.term_of;
815393c02db9 def_export: Drule.generalize;
wenzelm
parents: 19897
diff changeset
    60
18830
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    61
18875
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
    62
(*
18896
efd9d44a0bdb tuned comments;
wenzelm
parents: 18875
diff changeset
    63
  [x, x == t]
efd9d44a0bdb tuned comments;
wenzelm
parents: 18875
diff changeset
    64
       :
efd9d44a0bdb tuned comments;
wenzelm
parents: 18875
diff changeset
    65
      B x
efd9d44a0bdb tuned comments;
wenzelm
parents: 18875
diff changeset
    66
  -----------
efd9d44a0bdb tuned comments;
wenzelm
parents: 18875
diff changeset
    67
      B t
18875
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
    68
*)
20306
614b7e6c6276 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    69
fun def_export _ defs thm =
18830
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    70
  thm
20306
614b7e6c6276 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    71
  |> Drule.implies_intr_list defs
614b7e6c6276 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    72
  |> Drule.generalize ([], map head_of_def defs)
614b7e6c6276 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    73
  |> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
18830
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    74
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    75
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    76
(* add defs *)
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    77
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    78
fun add_def (x, t) ctxt =
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    79
  let
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    80
    val [eq] = mk_def ctxt [(x, t)];
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    81
    val x' = Term.dest_Free (fst (Logic.dest_equals eq));
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    82
  in
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    83
    ctxt
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    84
    |> ProofContext.add_fixes_i [(x, NONE, NoSyn)] |> snd
19585
70a1ce3b23ae removed 'concl is' patterns;
wenzelm
parents: 18950
diff changeset
    85
    |> ProofContext.add_assms_i def_export [(("", []), [(eq, [])])]
18830
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    86
    |>> (fn [(_, [th])] => (x', th))
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    87
  end;
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
    88
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
    89
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
    90
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
    91
(** defived definitions **)
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
    92
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
    93
(* transformation rules *)
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
    94
18859
75248f8badc9 export meta_rewrite_rule;
wenzelm
parents: 18840
diff changeset
    95
structure Rules = GenericDataFun
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
    96
(
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
    97
  val name = "Pure/derived_defs";
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
    98
  type T = thm list;
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
    99
  val empty = []
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   100
  val extend = I;
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   101
  fun merge _ = Drule.merge_rules;
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   102
  fun print context rules =
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   103
    Pretty.writeln (Pretty.big_list "definitional transformations:"
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   104
      (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   105
);
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   106
18859
75248f8badc9 export meta_rewrite_rule;
wenzelm
parents: 18840
diff changeset
   107
val _ = Context.add_setup Rules.init;
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   108
18859
75248f8badc9 export meta_rewrite_rule;
wenzelm
parents: 18840
diff changeset
   109
val print_rules = Rules.print;
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   110
18859
75248f8badc9 export meta_rewrite_rule;
wenzelm
parents: 18840
diff changeset
   111
val defn_add = Thm.declaration_attribute (Rules.map o Drule.add_rule);
75248f8badc9 export meta_rewrite_rule;
wenzelm
parents: 18840
diff changeset
   112
val defn_del = Thm.declaration_attribute (Rules.map o Drule.del_rule);
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   113
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   114
18875
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
   115
(* meta rewrite rules *)
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   116
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   117
val equals_ss =
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   118
  MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   119
    addeqcongs [Drule.equals_cong];    (*protect meta-level equality*)
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   120
18859
75248f8badc9 export meta_rewrite_rule;
wenzelm
parents: 18840
diff changeset
   121
fun meta_rewrite context =
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   122
  MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE))
18859
75248f8badc9 export meta_rewrite_rule;
wenzelm
parents: 18840
diff changeset
   123
    (equals_ss addsimps (Rules.get context));
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   124
18859
75248f8badc9 export meta_rewrite_rule;
wenzelm
parents: 18840
diff changeset
   125
val meta_rewrite_rule = Drule.fconv_rule o meta_rewrite;
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   126
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   127
fun meta_rewrite_tac ctxt i =
18859
75248f8badc9 export meta_rewrite_rule;
wenzelm
parents: 18840
diff changeset
   128
  PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (meta_rewrite (Context.Proof ctxt))));
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   129
18875
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
   130
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
   131
(* rewriting with object-level rules *)
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
   132
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
   133
fun meta f ctxt = f o map (meta_rewrite_rule (Context.Proof ctxt));
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   134
18875
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
   135
val unfold       = meta Tactic.rewrite_rule;
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
   136
val unfold_goals = meta Tactic.rewrite_goals_rule;
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
   137
val unfold_tac   = meta Tactic.rewrite_goals_tac;
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
   138
val fold         = meta Tactic.fold_rule;
853fa34047a4 (un)fold: no raw flag;
wenzelm
parents: 18859
diff changeset
   139
val fold_tac     = meta Tactic.fold_goals_tac;
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   140
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   141
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   142
(* derived defs -- potentially within the object-logic *)
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   143
18950
053e830c25ad cert_def: use Logic.dest_def;
wenzelm
parents: 18896
diff changeset
   144
fun derived_def ctxt conditional prop =
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   145
  let
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   146
    val ((c, T), rhs) = prop
20049
f48c4a3a34bc Goal.prove: context;
wenzelm
parents: 20021
diff changeset
   147
      |> Thm.cterm_of (ProofContext.theory_of ctxt)
18859
75248f8badc9 export meta_rewrite_rule;
wenzelm
parents: 18840
diff changeset
   148
      |> meta_rewrite (Context.Proof ctxt)
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   149
      |> (snd o Logic.dest_equals o Thm.prop_of)
18950
053e830c25ad cert_def: use Logic.dest_def;
wenzelm
parents: 18896
diff changeset
   150
      |> K conditional ? Logic.strip_imp_concl
053e830c25ad cert_def: use Logic.dest_def;
wenzelm
parents: 18896
diff changeset
   151
      |> (abs_def o #2 o cert_def ctxt);
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   152
    fun prove ctxt' t def =
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   153
      let
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   154
        val prop' = Term.subst_atomic [(Free (c, T), t)] prop;
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   155
        val frees = Term.fold_aterms (fn Free (x, _) =>
19897
fe661eb3b0e7 ProofContext: moved variable operations to struct Variable;
wenzelm
parents: 19585
diff changeset
   156
          if Variable.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop' [];
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   157
      in
20049
f48c4a3a34bc Goal.prove: context;
wenzelm
parents: 20021
diff changeset
   158
        Goal.prove ctxt' frees [] prop' (K (ALLGOALS
18840
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   159
          (meta_rewrite_tac ctxt' THEN'
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   160
            Tactic.rewrite_goal_tac [def] THEN'
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   161
            Tactic.resolve_tac [Drule.reflexive_thm])))
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   162
        handle ERROR msg => cat_error msg "Failed to prove definitional specification."
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   163
      end;
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   164
  in (((c, T), rhs), prove) end;
ce16e2bad548 added attributes defn_add/del;
wenzelm
parents: 18830
diff changeset
   165
18830
34b51dcdc570 Basic operations on local definitions.
wenzelm
parents:
diff changeset
   166
end;