author  wenzelm 
Sun, 29 Nov 2020 23:23:32 +0100  
changeset 72786  21ff9c1a4644 
parent 71177  71467e35fc3c 
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 
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54883
diff
changeset

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

14 
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

15 
val all_prems_of: Proof.context > thm list 
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 
 

67721  37 
#A \<Longrightarrow> B 
20222  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 
 

67721  47 
A \<Longrightarrow> B 
20222  48 
*) 
49 
fun presume_export _ = assume_export false; 

50 

54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54883
diff
changeset

51 

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

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

54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54883
diff
changeset

54 
fun assume_hyps ct ctxt = 
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54883
diff
changeset

55 
let val (th, ctxt') = Thm.assume_hyps ct ctxt 
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54883
diff
changeset

56 
in (Raw_Simplifier.norm_hhf ctxt' th, ctxt') end; 
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54883
diff
changeset

57 

20222  58 

59 

60 
(** local context data **) 

61 

62 
datatype data = Data of 

67721  63 
{assms: (export * cterm list) list, (*assumes: A \<Longrightarrow> _*) 
47236  64 
prems: thm list}; (*prems: A  norm_hhf A*) 
20222  65 

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

59150  67 
val empty_data = make_data ([], []); 
20222  68 

33519  69 
structure Data = Proof_Data 
20222  70 
( 
71 
type T = data; 

59150  72 
fun init _ = empty_data; 
20222  73 
); 
74 

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

45650  76 
fun rep_data ctxt = Data.get ctxt > (fn Data rep => rep); 
20222  77 

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

78 

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

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

80 

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

81 
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

82 
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

83 
val all_prems_of = #prems o rep_data; 
20222  84 

85 

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

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

87 

70735  88 
local 
89 

90 
fun drop_prefix eq (args as (x :: xs, y :: ys)) = 

91 
if eq (x, y) then drop_prefix eq (xs, ys) else args 

92 
 drop_prefix _ args = args; 

93 

94 
fun check_result ctxt kind term_of res = 

95 
(case res of 

96 
([], rest) => rest 

97 
 (bad :: _, _) => 

98 
raise Fail ("Outer context disagrees on " ^ kind ^ ": " ^ 

99 
Syntax.string_of_term ctxt (term_of bad))); 

100 

101 
in 

102 

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

103 
fun local_assumptions_of inner outer = 
70735  104 
drop_prefix (eq_snd (eq_list Thm.aconvc)) (apply2 all_assumptions_of (outer, inner)) 
105 
>> maps #2 

106 
> check_result outer "assumption" Thm.term_of; 

26392  107 

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

108 
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

109 

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

110 
fun local_prems_of inner outer = 
70735  111 
drop_prefix Thm.eq_thm_prop (apply2 all_prems_of (outer, inner)) 
112 
> check_result outer "premise" Thm.prop_of; 

113 

114 
end; 

26392  115 

116 

20222  117 
(* add assumptions *) 
118 

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

119 
fun add_assms export new_asms ctxt = 
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54883
diff
changeset

120 
let val (new_prems, ctxt') = fold_map assume_hyps new_asms ctxt in 
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
54883
diff
changeset

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

122 
> 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

123 
> pair new_prems 
20222  124 
end; 
125 

126 
val add_assumes = add_assms assume_export; 

127 

128 

20296  129 
(* export *) 
20222  130 

20296  131 
fun export is_goal inner outer = 
71177  132 
Raw_Simplifier.norm_hhf_protect inner #> 
30479  133 
fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #> 
71177  134 
Raw_Simplifier.norm_hhf_protect outer; 
20222  135 

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

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

21517  139 
fun export_morphism inner outer = 
140 
let 

141 
val thm = export false inner outer; 

21679  142 
val term = export_term inner outer; 
21517  143 
val typ = Logic.type_map term; 
54740  144 
in 
70313  145 
Morphism.transfer_morphism' inner $> 
146 
Morphism.transfer_morphism' outer $> 

54740  147 
Morphism.morphism "Assumption.export" 
148 
{binding = [], typ = [typ], term = [term], fact = [map thm]} 

149 
end; 

21517  150 

20222  151 
end; 