added attributes defn_add/del;
authorwenzelm
Sun Jan 29 19:23:47 2006 +0100 (2006-01-29 ago)
changeset 18840ce16e2bad548
parent 18839 86a59812b03b
child 18841 edecd40194c1
added attributes defn_add/del;
added (un)fold operations (from object_logic.ML);
tuned;
src/Pure/Isar/local_defs.ML
     1.1 --- a/src/Pure/Isar/local_defs.ML	Sun Jan 29 19:23:46 2006 +0100
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Sun Jan 29 19:23:47 2006 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius
     1.6  
     1.7 -Basic operations on local definitions.
     1.8 +Local definitions.
     1.9  *)
    1.10  
    1.11  signature LOCAL_DEFS =
    1.12 @@ -10,16 +10,26 @@
    1.13    val mk_def: ProofContext.context -> (string * term) list -> term list
    1.14    val cert_def: ProofContext.context -> term -> string * term
    1.15    val abs_def: term -> (string * typ) * term
    1.16 -  val derived_def: ProofContext.context -> term ->
    1.17 -    ((string * typ) * term) * (ProofContext.context -> term -> thm -> thm)
    1.18    val def_export: ProofContext.export
    1.19    val add_def: string * term -> ProofContext.context ->
    1.20      ((string * typ) * thm) * ProofContext.context
    1.21 +  val print_rules: Context.generic -> unit
    1.22 +  val defn_add: attribute
    1.23 +  val defn_del: attribute
    1.24 +  val unfold: ProofContext.context -> bool -> thm list -> thm -> thm
    1.25 +  val unfold_goals: ProofContext.context -> bool -> thm list -> thm -> thm
    1.26 +  val unfold_tac: ProofContext.context -> bool -> thm list -> tactic
    1.27 +  val fold: ProofContext.context -> bool -> thm list -> thm -> thm
    1.28 +  val fold_tac: ProofContext.context -> bool -> thm list -> tactic
    1.29 +  val derived_def: ProofContext.context -> term ->
    1.30 +    ((string * typ) * term) * (ProofContext.context -> term -> thm -> thm)
    1.31  end;
    1.32  
    1.33  structure LocalDefs: LOCAL_DEFS =
    1.34  struct
    1.35  
    1.36 +(** primitive definitions **)
    1.37 +
    1.38  (* prepare defs *)
    1.39  
    1.40  fun mk_def ctxt args =
    1.41 @@ -70,34 +80,6 @@
    1.42    in (Term.dest_Free f, eq') end;
    1.43  
    1.44  
    1.45 -(* derived defs -- potentially within the object-logic *)
    1.46 -
    1.47 -fun derived_def ctxt prop =
    1.48 -  let
    1.49 -    val thy = ProofContext.theory_of ctxt;
    1.50 -    val ((c, T), rhs) = prop
    1.51 -      |> Thm.cterm_of thy
    1.52 -      |> ObjectLogic.meta_rewrite_cterm
    1.53 -      |> (snd o Logic.dest_equals o Thm.prop_of)
    1.54 -      |> Logic.strip_imp_concl
    1.55 -      |> (snd o cert_def ctxt)
    1.56 -      |> abs_def;
    1.57 -    fun prove ctxt' t def =
    1.58 -      let
    1.59 -        val thy' = ProofContext.theory_of ctxt';
    1.60 -        val prop' = Term.subst_atomic [(Free (c, T), t)] prop;
    1.61 -        val frees = Term.fold_aterms (fn Free (x, _) =>
    1.62 -          if ProofContext.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop' [];
    1.63 -      in
    1.64 -        Goal.prove thy' frees [] prop' (K (ALLGOALS
    1.65 -          (ObjectLogic.meta_rewrite_tac THEN'
    1.66 -            Tactic.rewrite_goal_tac [def] THEN'
    1.67 -            Tactic.resolve_tac [Drule.reflexive_thm])))
    1.68 -        handle ERROR msg => cat_error msg "Failed to prove definitional specification."
    1.69 -      end;
    1.70 -  in (((c, T), rhs), prove) end;
    1.71 -
    1.72 -
    1.73  (* export defs *)
    1.74  
    1.75  fun head_of_def cprop =
    1.76 @@ -125,4 +107,84 @@
    1.77      |>> (fn [(_, [th])] => (x', th))
    1.78    end;
    1.79  
    1.80 +
    1.81 +
    1.82 +(** defived definitions **)
    1.83 +
    1.84 +(* transformation rules *)
    1.85 +
    1.86 +structure Data = GenericDataFun
    1.87 +(
    1.88 +  val name = "Pure/derived_defs";
    1.89 +  type T = thm list;
    1.90 +  val empty = []
    1.91 +  val extend = I;
    1.92 +  fun merge _ = Drule.merge_rules;
    1.93 +  fun print context rules =
    1.94 +    Pretty.writeln (Pretty.big_list "definitional transformations:"
    1.95 +      (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
    1.96 +);
    1.97 +
    1.98 +val _ = Context.add_setup Data.init;
    1.99 +
   1.100 +val print_rules = Data.print;
   1.101 +val get_rules = Data.get o Context.Proof;
   1.102 +
   1.103 +val defn_add = Thm.declaration_attribute (Data.map o Drule.add_rule);
   1.104 +val defn_del = Thm.declaration_attribute (Data.map o Drule.del_rule);
   1.105 +
   1.106 +
   1.107 +(* transform rewrite rules *)
   1.108 +
   1.109 +val equals_ss =
   1.110 +  MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss
   1.111 +    addeqcongs [Drule.equals_cong];    (*protect meta-level equality*)
   1.112 +
   1.113 +fun meta_rewrite ctxt =
   1.114 +  MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE))
   1.115 +    (equals_ss addsimps (get_rules ctxt));
   1.116 +
   1.117 +val meta_rewrite_thm = Drule.fconv_rule o meta_rewrite;
   1.118 +
   1.119 +fun meta_rewrite_tac ctxt i =
   1.120 +  PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (meta_rewrite ctxt)));
   1.121 +
   1.122 +fun transformed f _ false = f
   1.123 +  | transformed f ctxt true = f o map (meta_rewrite_thm ctxt);
   1.124 +
   1.125 +val unfold       = transformed Tactic.rewrite_rule;
   1.126 +val unfold_goals = transformed Tactic.rewrite_goals_rule;
   1.127 +val unfold_tac   = transformed Tactic.rewrite_goals_tac;
   1.128 +val fold         = transformed Tactic.fold_rule;
   1.129 +val fold_tac     = transformed Tactic.fold_goals_tac;
   1.130 +
   1.131 +
   1.132 +(* derived defs -- potentially within the object-logic *)
   1.133 +
   1.134 +fun derived_def ctxt prop =
   1.135 +  let
   1.136 +    val thy = ProofContext.theory_of ctxt;
   1.137 +    val ((c, T), rhs) = prop
   1.138 +      |> Thm.cterm_of thy
   1.139 +      |> meta_rewrite ctxt
   1.140 +      |> (snd o Logic.dest_equals o Thm.prop_of)
   1.141 +      |> Logic.strip_imp_concl
   1.142 +      |> (snd o cert_def ctxt)
   1.143 +      |> abs_def;
   1.144 +    fun prove ctxt' t def =
   1.145 +      let
   1.146 +        val thy' = ProofContext.theory_of ctxt';
   1.147 +        val prop' = Term.subst_atomic [(Free (c, T), t)] prop;
   1.148 +        val frees = Term.fold_aterms (fn Free (x, _) =>
   1.149 +          if ProofContext.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop' [];
   1.150 +      in
   1.151 +        Goal.prove thy' frees [] prop' (K (ALLGOALS
   1.152 +          (meta_rewrite_tac ctxt' THEN'
   1.153 +            Tactic.rewrite_goal_tac [def] THEN'
   1.154 +            Tactic.resolve_tac [Drule.reflexive_thm])))
   1.155 +        handle ERROR msg => cat_error msg "Failed to prove definitional specification."
   1.156 +      end;
   1.157 +  in (((c, T), rhs), prove) end;
   1.158 +
   1.159 +
   1.160  end;