1(*  Title:      Pure/assumption.ML
2    Author:     Makarius
3
4Context assumptions, parameterized by export rules.
5*)
6
7signature ASSUMPTION =
8sig
9  type export = bool -> cterm list -> (thm -> thm) * (term -> term)
10  val assume_export: export
11  val presume_export: export
12  val assume: Proof.context -> cterm -> thm
13  val assume_hyps: cterm -> Proof.context -> thm * Proof.context
14  val all_assms_of: Proof.context -> cterm list
15  val all_prems_of: Proof.context -> thm list
16  val local_assms_of: Proof.context -> Proof.context -> cterm list
17  val local_prems_of: Proof.context -> Proof.context -> thm list
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
21  val export_term: Proof.context -> Proof.context -> term -> term
22  val export_morphism: Proof.context -> Proof.context -> morphism
23end;
24
25structure Assumption: ASSUMPTION =
26struct
27
28(** basic rules **)
29
30type export = bool -> cterm list -> (thm -> thm) * (term -> term);
31
32(*
33    [A]
34     :
35     B
36  --------
37  #A \<Longrightarrow> B
38*)
39fun assume_export is_goal asms =
40  (if is_goal then Drule.implies_intr_protected asms else Drule.implies_intr_list asms, fn t => t);
41
42(*
43    [A]
44     :
45     B
46  -------
47  A \<Longrightarrow> B
48*)
49fun presume_export _ = assume_export false;
50
51
52fun assume ctxt = Raw_Simplifier.norm_hhf ctxt o Thm.assume;
53
54fun assume_hyps ct ctxt =
55  let val (th, ctxt') = Thm.assume_hyps ct ctxt
56  in (Raw_Simplifier.norm_hhf ctxt' th, ctxt') end;
57
58
59
60(** local context data **)
61
62datatype data = Data of
63 {assms: (export * cterm list) list,    (*assumes: A \<Longrightarrow> _*)
64  prems: thm list};                     (*prems: A |- norm_hhf A*)
65
66fun make_data (assms, prems) = Data {assms = assms, prems = prems};
67val empty_data = make_data ([], []);
68
69structure Data = Proof_Data
70(
71  type T = data;
72  fun init _ = empty_data;
73);
74
75fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
76fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
77
78
79(* all assumptions *)
80
81val all_assumptions_of = #assms o rep_data;
82val all_assms_of = maps #2 o all_assumptions_of;
83val all_prems_of = #prems o rep_data;
84
85
86(* local assumptions *)
87
88local
89
90fun 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
94fun 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
101in
102
103fun local_assumptions_of inner outer =
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;
107
108val local_assms_of = maps #2 oo local_assumptions_of;
109
110fun local_prems_of inner outer =
111  drop_prefix Thm.eq_thm_prop (apply2 all_prems_of (outer, inner))
112  |> check_result outer "premise" Thm.prop_of;
113
114end;
115
116
117(* add assumptions *)
118
119fun add_assms export new_asms ctxt =
120  let val (new_prems, ctxt') = fold_map assume_hyps new_asms ctxt in
121    ctxt'
122    |> map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems))
123    |> pair new_prems
124  end;
125
126val add_assumes = add_assms assume_export;
127
128
129(* export *)
130
131fun export is_goal inner outer =
132  Raw_Simplifier.norm_hhf_protect inner #>
133  fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
134  Raw_Simplifier.norm_hhf_protect outer;
135
136fun export_term inner outer =
137  fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
138
139fun export_morphism inner outer =
140  let
141    val thm = export false inner outer;
142    val term = export_term inner outer;
143    val typ = Logic.type_map term;
144  in
145    Morphism.transfer_morphism' inner $>
146    Morphism.transfer_morphism' outer $>
147    Morphism.morphism "Assumption.export"
148      {binding = [], typ = [typ], term = [term], fact = [map thm]}
149  end;
150
151end;
152