src/Pure/Isar/element.ML
changeset 19808 396dd23c54ef
parent 19777 77929c3d2b74
child 19843 67cb97e856ff
     1.1 --- a/src/Pure/Isar/element.ML	Wed Jun 07 02:01:30 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Wed Jun 07 02:01:31 2006 +0200
     1.3 @@ -26,12 +26,13 @@
     1.4      typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
     1.5      attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
     1.6    val map_ctxt_values: (typ -> typ) -> (term -> term) -> (thm -> thm) -> context_i -> context_i
     1.7 -  val params_of: ('typ, 'term, 'fact) ctxt -> (string * 'typ) list
     1.8 -  val prems_of: ('typ, 'term, 'fact) ctxt -> 'term list
     1.9 +  val params_of: context_i -> (string * typ) list
    1.10 +  val prems_of: context_i -> term list
    1.11 +  val facts_of: theory -> context_i ->
    1.12 +    ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
    1.13    val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
    1.14    val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
    1.15    val pretty_statement: Proof.context -> string -> thm -> Pretty.T
    1.16 -
    1.17    type witness
    1.18    val map_witness: (term * thm -> term * thm) -> witness -> witness
    1.19    val witness_prop: witness -> term
    1.20 @@ -41,8 +42,7 @@
    1.21    val conclude_witness: witness -> thm
    1.22    val mark_witness: term -> term
    1.23    val make_witness: term -> thm -> witness
    1.24 -  val refine_witness: Proof.state -> Proof.state
    1.25 -
    1.26 +  val refine_witness: Proof.state -> Proof.state Seq.seq
    1.27    val rename: (string * (string * mixfix option)) list -> string -> string
    1.28    val rename_var: (string * (string * mixfix option)) list -> string * mixfix -> string * mixfix
    1.29    val rename_term: (string * (string * mixfix option)) list -> term -> term
    1.30 @@ -105,6 +105,9 @@
    1.31    {name = I, var = I, typ = typ, term = term, fact = map thm,
    1.32      attrib = Args.map_values I typ term thm};
    1.33  
    1.34 +
    1.35 +(* logical content *)
    1.36 +
    1.37  fun params_of (Fixes fixes) = fixes |> map
    1.38      (fn (x, SOME T, _) => (x, T)
    1.39        | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote x, []))
    1.40 @@ -114,6 +117,13 @@
    1.41    | prems_of (Defines defs) = map (fst o snd) defs
    1.42    | prems_of _ = [];
    1.43  
    1.44 +fun assume thy t = Goal.norm_hhf (Thm.assume (Thm.cterm_of thy t));
    1.45 +
    1.46 +fun facts_of thy (Assumes asms) = map (apsnd (map (fn (t, _) => ([assume thy t], [])))) asms
    1.47 +  | facts_of thy (Defines defs) = map (apsnd (fn (t, _) => [([assume thy t], [])])) defs
    1.48 +  | facts_of _ (Notes facts) = facts
    1.49 +  | facts_of _ _ = [];
    1.50 +
    1.51  
    1.52  
    1.53  (** pretty printing **)
    1.54 @@ -276,8 +286,7 @@
    1.55    Proof.refine (Method.Basic (K (Method.RAW_METHOD
    1.56      (K (ALLGOALS
    1.57        (PRECISE_CONJUNCTS ~1 (ALLGOALS
    1.58 -        (PRECISE_CONJUNCTS ~1 (TRYALL (Tactic.rtac Drule.protectI))))))))))
    1.59 -  #> Seq.hd;
    1.60 +        (PRECISE_CONJUNCTS ~1 (TRYALL (Tactic.rtac Drule.protectI))))))))));
    1.61  
    1.62  
    1.63  (* derived rules *)