moved basic assumption operations from structure ProofContext to Assumption;
authorwenzelm
Thu Jul 27 13:43:01 2006 +0200 (2006-07-27)
changeset 202249c40a144ee0e
parent 20223 89d2758ecddf
child 20225 4b8e42490e58
moved basic assumption operations from structure ProofContext to Assumption;
src/HOL/Import/shuffler.ML
src/HOL/Tools/res_atp.ML
src/Pure/Isar/args.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
     1.1 --- a/src/HOL/Import/shuffler.ML	Thu Jul 27 13:43:00 2006 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Thu Jul 27 13:43:01 2006 +0200
     1.3 @@ -665,7 +665,7 @@
     1.4  fun search_meth ctxt =
     1.5      let
     1.6  	val thy = ProofContext.theory_of ctxt
     1.7 -	val prems = ProofContext.prems_of ctxt
     1.8 +	val prems = Assumption.prems_of ctxt
     1.9      in
    1.10  	Method.SIMPLE_METHOD' HEADGOAL (gen_shuffle_tac thy true (map (pair "premise") prems))
    1.11      end
     2.1 --- a/src/HOL/Tools/res_atp.ML	Thu Jul 27 13:43:00 2006 +0200
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Jul 27 13:43:01 2006 +0200
     2.3 @@ -576,7 +576,7 @@
     2.4  
     2.5  
     2.6  fun cnf_hyps_thms ctxt = 
     2.7 -    let val ths = ProofContext.prems_of ctxt
     2.8 +    let val ths = Assumption.prems_of ctxt
     2.9      in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
    2.10  
    2.11  
     3.1 --- a/src/Pure/Isar/args.ML	Thu Jul 27 13:43:00 2006 +0200
     3.2 +++ b/src/Pure/Isar/args.ML	Thu Jul 27 13:43:01 2006 +0200
     3.3 @@ -320,7 +320,7 @@
     3.4    nat >> PureThy.Single));
     3.5  
     3.6  val bang_facts = Scan.peek (fn context =>
     3.7 -  $$$ "!" >> K (ProofContext.prems_of (Context.proof_of context)) || Scan.succeed []);
     3.8 +  $$$ "!" >> K (Assumption.prems_of (Context.proof_of context)) || Scan.succeed []);
     3.9  
    3.10  
    3.11  (* goal specification *)
     4.1 --- a/src/Pure/Isar/local_defs.ML	Thu Jul 27 13:43:00 2006 +0200
     4.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Jul 27 13:43:01 2006 +0200
     4.3 @@ -10,7 +10,7 @@
     4.4    val cert_def: ProofContext.context -> term -> (string * typ) * term
     4.5    val abs_def: term -> (string * typ) * term
     4.6    val mk_def: ProofContext.context -> (string * term) list -> term list
     4.7 -  val def_export: ProofContext.export
     4.8 +  val def_export: Assumption.export
     4.9    val add_def: string * term -> ProofContext.context ->
    4.10      ((string * typ) * thm) * ProofContext.context
    4.11    val print_rules: Context.generic -> unit
     5.1 --- a/src/Pure/Isar/locale.ML	Thu Jul 27 13:43:00 2006 +0200
     5.2 +++ b/src/Pure/Isar/locale.ML	Thu Jul 27 13:43:01 2006 +0200
     5.3 @@ -1816,7 +1816,8 @@
     5.4      val pred_ctxt = ProofContext.init pred_thy;
     5.5      val (ctxt, (_, facts)) = activate_facts true (K I)
     5.6        (pred_ctxt, axiomify predicate_axioms elemss');
     5.7 -    val export = ProofContext.export_view predicate_statement ctxt thy_ctxt;
     5.8 +    val export = singleton (ProofContext.export_standard
     5.9 +        (Assumption.add_view thy_ctxt predicate_statement ctxt) thy_ctxt);
    5.10      val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
    5.11      val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
    5.12      val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
     6.1 --- a/src/Pure/Isar/method.ML	Thu Jul 27 13:43:00 2006 +0200
     6.2 +++ b/src/Pure/Isar/method.ML	Thu Jul 27 13:43:01 2006 +0200
     6.3 @@ -227,7 +227,7 @@
     6.4  
     6.5  fun assm_tac ctxt =
     6.6    assume_tac APPEND'
     6.7 -  asm_tac (ProofContext.prems_of ctxt) APPEND'
     6.8 +  asm_tac (Assumption.prems_of ctxt) APPEND'
     6.9    cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
    6.10    cond_rtac (can Logic.dest_term) Drule.termI;
    6.11  
     7.1 --- a/src/Pure/Isar/obtain.ML	Thu Jul 27 13:43:00 2006 +0200
     7.2 +++ b/src/Pure/Isar/obtain.ML	Thu Jul 27 13:43:01 2006 +0200
     7.3 @@ -319,7 +319,7 @@
     7.4              val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
     7.5            in
     7.6              ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
     7.7 -            ctxt' |> ProofContext.add_assms_i ProofContext.assume_export
     7.8 +            ctxt' |> ProofContext.add_assms_i Assumption.assume_export
     7.9                [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
    7.10              |>> (fn [(_, [th])] => th)
    7.11            end;
     8.1 --- a/src/Pure/Isar/proof.ML	Thu Jul 27 13:43:00 2006 +0200
     8.2 +++ b/src/Pure/Isar/proof.ML	Thu Jul 27 13:43:01 2006 +0200
     8.3 @@ -47,9 +47,9 @@
     8.4    val let_bind_i: (term list * term) list -> state -> state
     8.5    val fix: (string * string option * mixfix) list -> state -> state
     8.6    val fix_i: (string * typ option * mixfix) list -> state -> state
     8.7 -  val assm: ProofContext.export ->
     8.8 +  val assm: Assumption.export ->
     8.9      ((string * Attrib.src list) * (string * string list) list) list -> state -> state
    8.10 -  val assm_i: ProofContext.export ->
    8.11 +  val assm_i: Assumption.export ->
    8.12      ((string * attribute list) * (term * term list) list) list -> state -> state
    8.13    val assume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
    8.14    val assume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
    8.15 @@ -476,10 +476,10 @@
    8.16      val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
    8.17          (pretty_goals_local ctxt "" (true, ! show_main_goal) (! Display.goals_limit) goal @
    8.18            [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])));
    8.19 -    val _ =
    8.20 -      (case subtract (op aconv) (ProofContext.assms_of ctxt) (#hyps (Thm.rep_thm goal)) of
    8.21 -        [] => ()
    8.22 -      | hyps => error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term hyps)));
    8.23 +
    8.24 +    val extra_hyps = Assumption.extra_hyps ctxt goal;
    8.25 +    val _ = null extra_hyps orelse
    8.26 +      error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term extra_hyps));
    8.27  
    8.28      val (results, th) = `(Conjunction.elim_precise (map length propss)) (Goal.conclude goal)
    8.29        handle THM _ => error ("Lost goal structure:\n" ^ string_of_thm goal);
    8.30 @@ -544,10 +544,10 @@
    8.31  
    8.32  val assm      = gen_assume ProofContext.add_assms Attrib.attribute;
    8.33  val assm_i    = gen_assume ProofContext.add_assms_i (K I);
    8.34 -val assume    = assm ProofContext.assume_export;
    8.35 -val assume_i  = assm_i ProofContext.assume_export;
    8.36 -val presume   = assm ProofContext.presume_export;
    8.37 -val presume_i = assm_i ProofContext.presume_export;
    8.38 +val assume    = assm Assumption.assume_export;
    8.39 +val assume_i  = assm_i Assumption.assume_export;
    8.40 +val presume   = assm Assumption.presume_export;
    8.41 +val presume_i = assm_i Assumption.presume_export;
    8.42  
    8.43  end;
    8.44