src/Pure/assumption.ML
author wenzelm
Thu Aug 15 16:02:47 2019 +0200 (9 months ago)
changeset 70533 031620901fcd
parent 70313 9c19e15c8548
child 70735 561b11865cb5
permissions -rw-r--r--
support for (fully reconstructed) proof terms in Scala;
proper cache_typs;
     1 (*  Title:      Pure/assumption.ML
     2     Author:     Makarius
     3 
     4 Context assumptions, parameterized by export rules.
     5 *)
     6 
     7 signature ASSUMPTION =
     8 sig
     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
    23 end;
    24 
    25 structure Assumption: ASSUMPTION =
    26 struct
    27 
    28 (** basic rules **)
    29 
    30 type export = bool -> cterm list -> (thm -> thm) * (term -> term);
    31 
    32 (*
    33     [A]
    34      :
    35      B
    36   --------
    37   #A \<Longrightarrow> B
    38 *)
    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);
    41 
    42 (*
    43     [A]
    44      :
    45      B
    46   -------
    47   A \<Longrightarrow> B
    48 *)
    49 fun presume_export _ = assume_export false;
    50 
    51 
    52 fun assume ctxt = Raw_Simplifier.norm_hhf ctxt o Thm.assume;
    53 
    54 fun 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 
    62 datatype data = Data of
    63  {assms: (export * cterm list) list,    (*assumes: A \<Longrightarrow> _*)
    64   prems: thm list};                     (*prems: A |- norm_hhf A*)
    65 
    66 fun make_data (assms, prems) = Data {assms = assms, prems = prems};
    67 val empty_data = make_data ([], []);
    68 
    69 structure Data = Proof_Data
    70 (
    71   type T = data;
    72   fun init _ = empty_data;
    73 );
    74 
    75 fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
    76 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
    77 
    78 
    79 (* all assumptions *)
    80 
    81 val all_assumptions_of = #assms o rep_data;
    82 val all_assms_of = maps #2 o all_assumptions_of;
    83 val all_prems_of = #prems o rep_data;
    84 
    85 
    86 (* local assumptions *)
    87 
    88 fun local_assumptions_of inner outer =
    89   drop (length (all_assumptions_of outer)) (all_assumptions_of inner);
    90 
    91 val local_assms_of = maps #2 oo local_assumptions_of;
    92 
    93 fun local_prems_of inner outer =
    94   drop (length (all_prems_of outer)) (all_prems_of inner);
    95 
    96 
    97 (* add assumptions *)
    98 
    99 fun add_assms export new_asms ctxt =
   100   let val (new_prems, ctxt') = fold_map assume_hyps new_asms ctxt in
   101     ctxt'
   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 
   109 (* export *)
   110 
   111 fun normalize ctxt0 th0 =
   112   let val (ctxt, th) = Thm.join_transfer_context (ctxt0, th0)
   113   in Raw_Simplifier.norm_hhf_protect ctxt th end;
   114 
   115 fun export is_goal inner outer =
   116   normalize inner #>
   117   fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
   118   normalize outer;
   119 
   120 fun export_term inner outer =
   121   fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
   122 
   123 fun export_morphism inner outer =
   124   let
   125     val thm = export false inner outer;
   126     val term = export_term inner outer;
   127     val typ = Logic.type_map term;
   128   in
   129     Morphism.transfer_morphism' inner $>
   130     Morphism.transfer_morphism' outer $>
   131     Morphism.morphism "Assumption.export"
   132       {binding = [], typ = [typ], term = [term], fact = [map thm]}
   133   end;
   134 
   135 end;