src/Pure/assumption.ML
changeset 20222 e2b876cd9e29
child 20296 753fad9f6e03
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/assumption.ML	Thu Jul 27 13:42:59 2006 +0200
     1.3 @@ -0,0 +1,110 @@
     1.4 +(*  Title:      Pure/assumption.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Local assumptions, parameterized by export rules.
     1.9 +*)
    1.10 +
    1.11 +signature ASSUMPTION =
    1.12 +sig
    1.13 +  type export
    1.14 +  val assume_export: export
    1.15 +  val presume_export: export
    1.16 +  val assume: cterm -> thm
    1.17 +  val assms_of: Context.proof -> term list
    1.18 +  val prems_of: Context.proof -> thm list
    1.19 +  val extra_hyps: Context.proof -> thm -> term list
    1.20 +  val add_assms: export -> cterm list -> Context.proof -> thm list * Context.proof
    1.21 +  val add_assumes: cterm list -> Context.proof -> thm list * Context.proof
    1.22 +  val add_view: Context.proof -> cterm list -> Context.proof -> Context.proof
    1.23 +  val exports: bool -> Context.proof -> Context.proof -> thm list -> thm list Seq.seq
    1.24 +end;
    1.25 +
    1.26 +structure Assumption: ASSUMPTION =
    1.27 +struct
    1.28 +
    1.29 +(** basic rules **)
    1.30 +
    1.31 +type export = bool -> cterm list -> thm -> thm Seq.seq;
    1.32 +
    1.33 +(*
    1.34 +    [A]
    1.35 +     :
    1.36 +     B
    1.37 +  --------
    1.38 +  #A ==> B
    1.39 +*)
    1.40 +fun assume_export true = Seq.single oo Drule.implies_intr_protected
    1.41 +  | assume_export false = Seq.single oo Drule.implies_intr_list;
    1.42 +
    1.43 +(*
    1.44 +    [A]
    1.45 +     :
    1.46 +     B
    1.47 +  -------
    1.48 +  A ==> B
    1.49 +*)
    1.50 +fun presume_export _ = assume_export false;
    1.51 +
    1.52 +val assume = norm_hhf o Thm.assume;
    1.53 +
    1.54 +
    1.55 +
    1.56 +(** local context data **)
    1.57 +
    1.58 +datatype data = Data of
    1.59 + {assms: (export * cterm list) list,    (*assumes and views: A ==> _*)
    1.60 +  prems: thm list};                     (*prems: A |- A*)
    1.61 +
    1.62 +fun make_data (assms, prems) = Data {assms = assms, prems = prems};
    1.63 +
    1.64 +structure Data = ProofDataFun
    1.65 +(
    1.66 +  val name = "Pure/assumption";
    1.67 +  type T = data;
    1.68 +  fun init _ = make_data ([], []);
    1.69 +  fun print _ _ = ();
    1.70 +);
    1.71 +
    1.72 +val _ = Context.add_setup Data.init;
    1.73 +
    1.74 +fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
    1.75 +fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
    1.76 +
    1.77 +val assumptions_of = #assms o rep_data;
    1.78 +val assms_of = map Thm.term_of o maps #2 o assumptions_of;
    1.79 +val prems_of = #prems o rep_data;
    1.80 +
    1.81 +fun extra_hyps ctxt th = subtract (op aconv) (assms_of ctxt) (Thm.hyps_of th);
    1.82 +
    1.83 +
    1.84 +(* add assumptions *)
    1.85 +
    1.86 +fun add_assms export new_asms =
    1.87 +  let val new_prems = map assume new_asms in
    1.88 +    map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems)) #>
    1.89 +    pair new_prems
    1.90 +  end;
    1.91 +
    1.92 +val add_assumes = add_assms assume_export;
    1.93 +
    1.94 +fun add_view outer view = map_data (fn (asms, prems) =>
    1.95 +  let
    1.96 +    val (asms1, asms2) = chop (length (assumptions_of outer)) asms;
    1.97 +    val asms' = asms1 @ [(assume_export, view)] @ asms2;
    1.98 +  in (asms', prems) end);
    1.99 +
   1.100 +
   1.101 +(* exports *)
   1.102 +
   1.103 +fun exports is_goal inner outer =
   1.104 +  let
   1.105 +    val asms = rev (Library.drop (length (assumptions_of outer), assumptions_of inner));
   1.106 +    val exp_asms = map (fn (exp, As) => exp is_goal As) asms;
   1.107 +  in
   1.108 +    map norm_hhf_protect
   1.109 +    #> Seq.map_list (Seq.EVERY exp_asms)
   1.110 +    #> Seq.map (map norm_hhf_protect)
   1.111 +  end;
   1.112 +
   1.113 +end;