author  wenzelm 
Tue, 31 Dec 2013 14:29:16 +0100  
changeset 54883  dd04a8b654fc 
parent 54740  91f54d386680 
child 54984  da70ab8531f4 
permissions  rwrr 
20222  1 
(* Title: Pure/assumption.ML 
2 
Author: Makarius 

3 

30471
178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

4 
Context assumptions, parameterized by export rules. 
20222  5 
*) 
6 

7 
signature ASSUMPTION = 

8 
sig 

35716  9 
type export = bool > cterm list > (thm > thm) * (term > term) 
20222  10 
val assume_export: export 
11 
val presume_export: export 

54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54740
diff
changeset

12 
val assume: Proof.context > cterm > thm 
30471
178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

13 
val all_assms_of: Proof.context > cterm list 
178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

14 
val all_prems_of: Proof.context > thm list 
54567
cfe53047dc16
more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal  NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
wenzelm
parents:
47236
diff
changeset

15 
val check_hyps: Proof.context > thm > thm 
30471
178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

16 
val local_assms_of: Proof.context > Proof.context > cterm list 
178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

17 
val local_prems_of: Proof.context > Proof.context > thm list 
20296  18 
val add_assms: export > cterm list > Proof.context > thm list * Proof.context 
19 
val add_assumes: cterm list > Proof.context > thm list * Proof.context 

20 
val export: bool > Proof.context > Proof.context > thm > thm 

21679  21 
val export_term: Proof.context > Proof.context > term > term 
21517  22 
val export_morphism: Proof.context > Proof.context > morphism 
20222  23 
end; 
24 

25 
structure Assumption: ASSUMPTION = 

26 
struct 

27 

28 
(** basic rules **) 

29 

21679  30 
type export = bool > cterm list > (thm > thm) * (term > term); 
20222  31 

32 
(* 

33 
[A] 

34 
: 

35 
B 

36 
 

37 
#A ==> B 

38 
*) 

21679  39 
fun assume_export is_goal asms = 
40 
(if is_goal then Drule.implies_intr_protected asms else Drule.implies_intr_list asms, fn t => t); 

20222  41 

42 
(* 

43 
[A] 

44 
: 

45 
B 

46 
 

47 
A ==> B 

48 
*) 

49 
fun presume_export _ = assume_export false; 

50 

54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54740
diff
changeset

51 
fun assume ctxt = Raw_Simplifier.norm_hhf ctxt o Thm.assume; 
20222  52 

53 

54 

55 
(** local context data **) 

56 

57 
datatype data = Data of 

30479  58 
{assms: (export * cterm list) list, (*assumes: A ==> _*) 
47236  59 
prems: thm list}; (*prems: A  norm_hhf A*) 
20222  60 

61 
fun make_data (assms, prems) = Data {assms = assms, prems = prems}; 

62 

33519  63 
structure Data = Proof_Data 
20222  64 
( 
65 
type T = data; 

66 
fun init _ = make_data ([], []); 

67 
); 

68 

69 
fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems))); 

45650  70 
fun rep_data ctxt = Data.get ctxt > (fn Data rep => rep); 
20222  71 

30471
178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

72 

178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

73 
(* all assumptions *) 
178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

74 

178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

75 
val all_assumptions_of = #assms o rep_data; 
178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

76 
val all_assms_of = maps #2 o all_assumptions_of; 
178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

77 
val all_prems_of = #prems o rep_data; 
20222  78 

54567
cfe53047dc16
more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal  NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
wenzelm
parents:
47236
diff
changeset

79 
fun check_hyps ctxt th = 
cfe53047dc16
more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal  NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
wenzelm
parents:
47236
diff
changeset

80 
let 
cfe53047dc16
more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal  NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
wenzelm
parents:
47236
diff
changeset

81 
val extra_hyps = subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th); 
cfe53047dc16
more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal  NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
wenzelm
parents:
47236
diff
changeset

82 
val _ = null extra_hyps orelse 
cfe53047dc16
more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal  NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
wenzelm
parents:
47236
diff
changeset

83 
error ("Additional hypotheses:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) extra_hyps)); 
cfe53047dc16
more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal  NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
wenzelm
parents:
47236
diff
changeset

84 
in th end; 
30471
178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

85 

20222  86 

30471
178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

87 
(* local assumptions *) 
178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

88 

178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

89 
fun local_assumptions_of inner outer = 
33957  90 
drop (length (all_assumptions_of outer)) (all_assumptions_of inner); 
26392  91 

30471
178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

92 
val local_assms_of = maps #2 oo local_assumptions_of; 
178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

93 

178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

94 
fun local_prems_of inner outer = 
33957  95 
drop (length (all_prems_of outer)) (all_prems_of inner); 
26392  96 

97 

20222  98 
(* add assumptions *) 
99 

54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54740
diff
changeset

100 
fun add_assms export new_asms ctxt = 
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54740
diff
changeset

101 
let val new_prems = map (assume ctxt) new_asms in 
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54740
diff
changeset

102 
ctxt 
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54740
diff
changeset

103 
> map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems)) 
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54740
diff
changeset

104 
> pair new_prems 
20222  105 
end; 
106 

107 
val add_assumes = add_assms assume_export; 

108 

109 

20296  110 
(* export *) 
20222  111 

20296  112 
fun export is_goal inner outer = 
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54740
diff
changeset

113 
Raw_Simplifier.norm_hhf_protect inner #> 
30479  114 
fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #> 
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54740
diff
changeset

115 
Raw_Simplifier.norm_hhf_protect outer; 
20222  116 

21679  117 
fun export_term inner outer = 
30471
178de3995e91
renamed assms_of to all_assms_of, and prems_of to all_prems_of;
wenzelm
parents:
29605
diff
changeset

118 
fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer); 
21679  119 

21517  120 
fun export_morphism inner outer = 
121 
let 

122 
val thm = export false inner outer; 

21679  123 
val term = export_term inner outer; 
21517  124 
val typ = Logic.type_map term; 
54740  125 
in 
126 
Morphism.morphism "Assumption.export" 

127 
{binding = [], typ = [typ], term = [term], fact = [map thm]} 

128 
end; 

21517  129 

20222  130 
end; 