author  wenzelm 
Fri, 13 Dec 2013 20:20:15 +0100  
changeset 54740  91f54d386680 
parent 54567  cfe53047dc16 
child 54883  dd04a8b654fc 
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 

12 
val assume: 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 

41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
39557
diff
changeset

51 
val assume = Raw_Simplifier.norm_hhf 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 

100 
fun add_assms export new_asms = 

101 
let val new_prems = map assume new_asms in 

102 
map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems)) #> 

103 
pair new_prems 

104 
end; 

105 

106 
val add_assumes = add_assms assume_export; 

107 

108 

20296  109 
(* export *) 
20222  110 

20296  111 
fun export is_goal inner outer = 
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
39557
diff
changeset

112 
Raw_Simplifier.norm_hhf_protect #> 
30479  113 
fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #> 
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
39557
diff
changeset

114 
Raw_Simplifier.norm_hhf_protect; 
20222  115 

21679  116 
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

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

21517  119 
fun export_morphism inner outer = 
120 
let 

121 
val thm = export false inner outer; 

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

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

127 
end; 

21517  128 

20222  129 
end; 