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