author  wenzelm 
Mon, 09 Oct 2006 02:20:02 +0200  
changeset 20909  7132ab2b4621 
parent 20887  ec9a1bb086da 
child 20980  e4fd72aecd03 
permissions  rwrr 
18830  1 
(* Title: Pure/Isar/local_defs.ML 
2 
ID: $Id$ 

3 
Author: Makarius 

4 

18840  5 
Local definitions. 
18830  6 
*) 
7 

8 
signature LOCAL_DEFS = 

9 
sig 

20306  10 
val cert_def: Proof.context > term > (string * typ) * term 
18830  11 
val abs_def: term > (string * typ) * term 
20306  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 
20887  14 
val find_def: Proof.context > string > thm option 
15 
val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list > Proof.context > 

16 
(term * (bstring * thm)) list * Proof.context 

18840  17 
val print_rules: Context.generic > unit 
18 
val defn_add: attribute 

19 
val defn_del: attribute 

18859  20 
val meta_rewrite_rule: Context.generic > thm > thm 
20306  21 
val unfold: Proof.context > thm list > thm > thm 
22 
val unfold_goals: Proof.context > thm list > thm > thm 

23 
val unfold_tac: Proof.context > thm list > tactic 

24 
val fold: Proof.context > thm list > thm > thm 

25 
val fold_tac: Proof.context > thm list > tactic 

26 
val derived_def: Proof.context > bool > term > 

20909  27 
((string * typ) * term) * (Proof.context > thm > thm) 
18830  28 
end; 
29 

30 
structure LocalDefs: LOCAL_DEFS = 

31 
struct 

32 

18840  33 
(** primitive definitions **) 
34 

18830  35 
(* prepare defs *) 
36 

37 
fun cert_def ctxt eq = 

38 
let 

18950  39 
val pp = ProofContext.pp ctxt; 
40 
val display_term = quote o Pretty.string_of_term pp; 

41 
fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^ display_term eq); 

42 
val ((lhs, _), eq') = eq 

43 
> Sign.no_vars pp 

19897
fe661eb3b0e7
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19585
diff
changeset

44 
> Logic.dest_def pp Term.is_Free (Variable.is_fixed ctxt) (K true) 
18950  45 
handle TERM (msg, _) => err msg  ERROR msg => err msg; 
46 
in (Term.dest_Free (Term.head_of lhs), eq') end; 

18830  47 

18950  48 
val abs_def = Logic.abs_def #> apfst Term.dest_Free; 
18830  49 

18875  50 
fun mk_def ctxt args = 
51 
let 

52 
val (xs, rhss) = split_list args; 

53 
val (bind, _) = ProofContext.bind_fixes xs ctxt; 

54 
val lhss = map (fn (x, rhs) => bind (Free (x, Term.fastype_of rhs))) args; 

55 
in map Logic.mk_equals (lhss ~~ rhss) end; 

56 

18830  57 

58 
(* export defs *) 

59 

20021  60 
val head_of_def = 
20887  61 
#1 o Term.dest_Free o Term.head_of o #1 o Logic.dest_equals o Term.strip_all_body; 
20021  62 

18830  63 

18875  64 
(* 
20887  65 
[x, x == a] 
18896  66 
: 
67 
B x 

68 
 

20887  69 
B a 
18875  70 
*) 
20306  71 
fun def_export _ defs thm = 
18830  72 
thm 
20306  73 
> Drule.implies_intr_list defs 
20887  74 
> Drule.generalize ([], map (head_of_def o Thm.term_of) defs) 
20306  75 
> funpow (length defs) (fn th => Drule.reflexive_thm RS th); 
18830  76 

77 

20887  78 
(* find def *) 
79 

80 
fun find_def ctxt x = 

81 
Assumption.prems_of ctxt > find_first (fn th => 

82 
(case try (head_of_def o Thm.prop_of) th of 

83 
SOME y => x = y 

84 
 NONE => false)); 

85 

86 

18830  87 
(* add defs *) 
88 

20887  89 
fun add_defs defs ctxt = 
18830  90 
let 
20887  91 
val ((xs, mxs), specs) = defs > split_list >> split_list; 
92 
val ((names, atts), rhss) = specs > split_list >> split_list; 

93 
val names' = map2 Thm.def_name_optional xs names; 

94 
val eqs = mk_def ctxt (xs ~~ rhss); 

95 
val lhss = map (fst o Logic.dest_equals) eqs; 

18830  96 
in 
97 
ctxt 

20887  98 
> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) > #2 
99 
> ProofContext.add_assms_i def_export 

100 
(map2 (fn a => fn eq => (a, [(eq, [])])) (names' ~~ atts) eqs) 

101 
>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss 

18830  102 
end; 
103 

18840  104 

105 

106 
(** defived definitions **) 

107 

108 
(* transformation rules *) 

109 

18859  110 
structure Rules = GenericDataFun 
18840  111 
( 
112 
val name = "Pure/derived_defs"; 

113 
type T = thm list; 

114 
val empty = [] 

115 
val extend = I; 

116 
fun merge _ = Drule.merge_rules; 

117 
fun print context rules = 

118 
Pretty.writeln (Pretty.big_list "definitional transformations:" 

119 
(map (ProofContext.pretty_thm (Context.proof_of context)) rules)); 

120 
); 

121 

18859  122 
val _ = Context.add_setup Rules.init; 
18840  123 

18859  124 
val print_rules = Rules.print; 
18840  125 

18859  126 
val defn_add = Thm.declaration_attribute (Rules.map o Drule.add_rule); 
127 
val defn_del = Thm.declaration_attribute (Rules.map o Drule.del_rule); 

18840  128 

129 

18875  130 
(* meta rewrite rules *) 
18840  131 

132 
val equals_ss = 

133 
MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss 

134 
addeqcongs [Drule.equals_cong]; (*protect metalevel equality*) 

135 

18859  136 
fun meta_rewrite context = 
18840  137 
MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE)) 
18859  138 
(equals_ss addsimps (Rules.get context)); 
18840  139 

18859  140 
val meta_rewrite_rule = Drule.fconv_rule o meta_rewrite; 
18840  141 

142 
fun meta_rewrite_tac ctxt i = 

18859  143 
PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (meta_rewrite (Context.Proof ctxt)))); 
18840  144 

18875  145 

146 
(* rewriting with objectlevel rules *) 

147 

148 
fun meta f ctxt = f o map (meta_rewrite_rule (Context.Proof ctxt)); 

18840  149 

18875  150 
val unfold = meta Tactic.rewrite_rule; 
151 
val unfold_goals = meta Tactic.rewrite_goals_rule; 

152 
val unfold_tac = meta Tactic.rewrite_goals_tac; 

153 
val fold = meta Tactic.fold_rule; 

154 
val fold_tac = meta Tactic.fold_goals_tac; 

18840  155 

156 

157 
(* derived defs  potentially within the objectlogic *) 

158 

18950  159 
fun derived_def ctxt conditional prop = 
18840  160 
let 
161 
val ((c, T), rhs) = prop 

20049  162 
> Thm.cterm_of (ProofContext.theory_of ctxt) 
18859  163 
> meta_rewrite (Context.Proof ctxt) 
18840  164 
> (snd o Logic.dest_equals o Thm.prop_of) 
18950  165 
> K conditional ? Logic.strip_imp_concl 
166 
> (abs_def o #2 o cert_def ctxt); 

20909  167 
fun prove ctxt' def = 
18840  168 
let 
169 
val frees = Term.fold_aterms (fn Free (x, _) => 

20909  170 
if Variable.is_fixed ctxt' x then I else insert (op =) x  _ => I) prop []; 
18840  171 
in 
20909  172 
Goal.prove ctxt' frees [] prop (K (ALLGOALS 
18840  173 
(meta_rewrite_tac ctxt' THEN' 
174 
Tactic.rewrite_goal_tac [def] THEN' 

175 
Tactic.resolve_tac [Drule.reflexive_thm]))) 

176 
handle ERROR msg => cat_error msg "Failed to prove definitional specification." 

177 
end; 

178 
in (((c, T), rhs), prove) end; 

179 

18830  180 
end; 