src/Pure/Isar/local_defs.ML
author wenzelm
Thu Dec 07 00:42:04 2006 +0100 (2006-12-07 ago)
changeset 21687 f689f729afab
parent 21684 e8c135b166b3
child 21699 9395071cc5c5
permissions -rw-r--r--
reorganized structure Goal vs. Tactic;
     1 (*  Title:      Pure/Isar/local_defs.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Local definitions.
     6 *)
     7 
     8 signature LOCAL_DEFS =
     9 sig
    10   val cert_def: Proof.context -> term -> (string * typ) * term
    11   val abs_def: term -> (string * typ) * term
    12   val mk_def: Proof.context -> (string * term) list -> term list
    13   val expand: cterm list -> thm -> thm
    14   val def_export: Assumption.export
    15   val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
    16     (term * (bstring * thm)) list * Proof.context
    17   val export: Proof.context -> Proof.context -> thm -> thm list * thm
    18   val print_rules: Proof.context -> unit
    19   val defn_add: attribute
    20   val defn_del: attribute
    21   val meta_rewrite_rule: Proof.context -> thm -> thm
    22   val unfold: Proof.context -> thm list -> thm -> thm
    23   val unfold_goals: Proof.context -> thm list -> thm -> thm
    24   val unfold_tac: Proof.context -> thm list -> tactic
    25   val fold: Proof.context -> thm list -> thm -> thm
    26   val fold_tac: Proof.context -> thm list -> tactic
    27   val derived_def: Proof.context -> bool -> term ->
    28     ((string * typ) * term) * (Proof.context -> thm -> thm)
    29 end;
    30 
    31 structure LocalDefs: LOCAL_DEFS =
    32 struct
    33 
    34 (** primitive definitions **)
    35 
    36 (* prepare defs *)
    37 
    38 fun cert_def ctxt eq =
    39   let
    40     val pp = ProofContext.pp ctxt;
    41     val display_term = quote o Pretty.string_of_term pp;
    42     fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^ display_term eq);
    43     val ((lhs, _), eq') = eq
    44       |> Sign.no_vars pp
    45       |> Logic.dest_def pp Term.is_Free (Variable.is_fixed ctxt) (K true)
    46       handle TERM (msg, _) => err msg | ERROR msg => err msg;
    47   in (Term.dest_Free (Term.head_of lhs), eq') end;
    48 
    49 val abs_def = Logic.abs_def #> apfst Term.dest_Free;
    50 
    51 fun mk_def ctxt args =
    52   let
    53     val (xs, rhss) = split_list args;
    54     val (bind, _) = ProofContext.bind_fixes xs ctxt;
    55     val lhss = map (fn (x, rhs) => bind (Free (x, Term.fastype_of rhs))) args;
    56   in map Logic.mk_equals (lhss ~~ rhss) end;
    57 
    58 
    59 (* export defs *)
    60 
    61 val head_of_def =
    62   #1 o Term.dest_Free o Term.head_of o #1 o Logic.dest_equals o Term.strip_all_body;
    63 
    64 
    65 (*
    66   [x, x == a]
    67        :
    68       B x
    69   -----------
    70       B a
    71 *)
    72 fun expand defs =
    73   Drule.implies_intr_list defs
    74   #> Drule.generalize ([], map (head_of_def o Thm.term_of) defs)
    75   #> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
    76 
    77 fun expand_term [] = I
    78   | expand_term defs = Pattern.rewrite_term
    79       (Theory.merge_list (map Thm.theory_of_cterm defs))
    80       (map (Logic.dest_equals o Thm.prop_of o Assumption.assume) defs) [];
    81 
    82 fun def_export _ defs = (expand defs, expand_term defs);
    83 
    84 
    85 (* add defs *)
    86 
    87 fun add_defs defs ctxt =
    88   let
    89     val ((xs, mxs), specs) = defs |> split_list |>> split_list;
    90     val ((names, atts), rhss) = specs |> split_list |>> split_list;
    91     val names' = map2 Thm.def_name_optional xs names;
    92     val eqs = mk_def ctxt (xs ~~ rhss);
    93     val lhss = map (fst o Logic.dest_equals) eqs;
    94   in
    95     ctxt
    96     |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2
    97     |> fold Variable.declare_term eqs
    98     |> ProofContext.add_assms_i def_export
    99       (map2 (fn a => fn eq => (a, [(eq, [])])) (names' ~~ atts) eqs)
   100     |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
   101   end;
   102 
   103 
   104 (* specific export -- result based on educated guessing *)
   105 
   106 fun export inner outer th =
   107   let
   108     val th' = Assumption.export false inner outer th;
   109     val still_fixed = map #1 (Drule.fold_terms Term.add_frees th' []);
   110     val defs = Assumption.prems_of inner |> filter_out (fn prem =>
   111       (case try (head_of_def o Thm.prop_of) prem of
   112         SOME x => member (op =) still_fixed x
   113       | NONE => true));
   114   in (map Drule.abs_def defs, th') end;
   115 
   116 
   117 
   118 (** defived definitions **)
   119 
   120 (* transformation rules *)
   121 
   122 structure Rules = GenericDataFun
   123 (
   124   val name = "Pure/derived_defs";
   125   type T = thm list;
   126   val empty = []
   127   val extend = I;
   128   fun merge _ = Drule.merge_rules;
   129   fun print context rules =
   130     Pretty.writeln (Pretty.big_list "definitional transformations:"
   131       (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
   132 );
   133 
   134 val _ = Context.add_setup Rules.init;
   135 
   136 val print_rules = Rules.print o Context.Proof;
   137 
   138 val defn_add = Thm.declaration_attribute (Rules.map o Drule.add_rule);
   139 val defn_del = Thm.declaration_attribute (Rules.map o Drule.del_rule);
   140 
   141 
   142 (* meta rewrite rules *)
   143 
   144 val equals_ss =
   145   MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss
   146     addeqcongs [Drule.equals_cong];    (*protect meta-level equality*)
   147 
   148 fun meta_rewrite ctxt =
   149   MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE))
   150     (equals_ss addsimps (Rules.get (Context.Proof ctxt)));
   151 
   152 val meta_rewrite_rule = Drule.fconv_rule o meta_rewrite;
   153 
   154 fun meta_rewrite_tac ctxt i =
   155   PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (meta_rewrite ctxt)));
   156 
   157 
   158 (* rewriting with object-level rules *)
   159 
   160 fun meta f ctxt = f o map (meta_rewrite_rule ctxt);
   161 
   162 val unfold       = meta Tactic.rewrite_rule;
   163 val unfold_goals = meta Tactic.rewrite_goals_rule;
   164 val unfold_tac   = meta Tactic.rewrite_goals_tac;
   165 val fold         = meta Tactic.fold_rule;
   166 val fold_tac     = meta Tactic.fold_goals_tac;
   167 
   168 
   169 (* derived defs -- potentially within the object-logic *)
   170 
   171 fun derived_def ctxt conditional prop =
   172   let
   173     val ((c, T), rhs) = prop
   174       |> Thm.cterm_of (ProofContext.theory_of ctxt)
   175       |> meta_rewrite ctxt
   176       |> (snd o Logic.dest_equals o Thm.prop_of)
   177       |> conditional ? Logic.strip_imp_concl
   178       |> (abs_def o #2 o cert_def ctxt);
   179     fun prove ctxt' def =
   180       let
   181         val frees = Term.fold_aterms (fn Free (x, _) =>
   182           if Variable.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop [];
   183       in
   184         Goal.prove ctxt' frees [] prop (K (ALLGOALS
   185           (meta_rewrite_tac ctxt' THEN'
   186             Goal.rewrite_goal_tac [def] THEN'
   187             Tactic.resolve_tac [Drule.reflexive_thm])))
   188         handle ERROR msg => cat_error msg "Failed to prove definitional specification."
   189       end;
   190   in (((c, T), rhs), prove) end;
   191 
   192 end;