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