simplified exporter interface;
authorwenzelm
Tue Oct 16 23:02:14 2001 +0200 (2001-10-16)
changeset 11816545aab7410ac
parent 11815 ef7619398680
child 11817 875ee0c20da2
simplified exporter interface;
src/Pure/Isar/local_defs.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/local_defs.ML	Tue Oct 16 23:00:21 2001 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Tue Oct 16 23:02:14 2001 +0200
     1.3 @@ -18,30 +18,20 @@
     1.4  struct
     1.5  
     1.6  
     1.7 -(* export_defs *)
     1.8 -
     1.9 -local
    1.10 -
    1.11 -val refl_tac = Tactic.rtac (Drule.reflexive_thm RS Drule.triv_goal);
    1.12 +(* export_def *)
    1.13  
    1.14  fun dest_lhs cprop =
    1.15 -  let val x = #1 (Logic.dest_equals (Logic.dest_goal (Thm.term_of cprop)))
    1.16 +  let val x = #1 (Logic.dest_equals (Thm.term_of cprop))
    1.17    in Term.dest_Free x; Thm.cterm_of (Thm.sign_of_cterm cprop) x end
    1.18    handle TERM _ => raise TERM ("Malformed definitional assumption encountered:\n" ^
    1.19        quote (Display.string_of_cterm cprop), []);
    1.20  
    1.21 -fun disch_defs cprops thm =
    1.22 +fun export_def _ cprops thm =
    1.23    thm
    1.24    |> Drule.implies_intr_list cprops
    1.25    |> Drule.forall_intr_list (map dest_lhs cprops)
    1.26    |> Drule.forall_elim_vars 0
    1.27 -  |> RANGE (replicate (length cprops) refl_tac) 1;
    1.28 -
    1.29 -in
    1.30 -
    1.31 -val export_defs = (disch_defs, fn _ => fn _ => []);
    1.32 -
    1.33 -end;
    1.34 +  |> RANGE (replicate (length cprops) (Tactic.rtac Drule.reflexive_thm)) 1;
    1.35  
    1.36  
    1.37  (* def(_i) *)
    1.38 @@ -63,7 +53,7 @@
    1.39      state
    1.40      |> fix [([x], None)]
    1.41      |> Proof.match_bind_i [(pats, rhs)]
    1.42 -    |> Proof.assm_i export_defs [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])]
    1.43 +    |> Proof.assm_i export_def [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])]
    1.44    end;
    1.45  
    1.46  val def = gen_def Proof.fix ProofContext.read_term ProofContext.read_term_pats;
     2.1 --- a/src/Pure/Isar/obtain.ML	Tue Oct 16 23:00:21 2001 +0200
     2.2 +++ b/src/Pure/Isar/obtain.ML	Tue Oct 16 23:02:14 2001 +0200
     2.3 @@ -32,18 +32,18 @@
     2.4  struct
     2.5  
     2.6  
     2.7 -(** disch_obtained **)
     2.8 +(** export_obtain **)
     2.9  
    2.10 -fun disch_obtained state parms rule cprops thm =
    2.11 +fun export_obtain state parms rule _ cprops thm =
    2.12    let
    2.13      val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
    2.14      val cparms = map (Thm.cterm_of sign) parms;
    2.15  
    2.16      val thm' = thm
    2.17 -      |> Drule.implies_intr_list cprops
    2.18 +      |> Drule.implies_intr_goals cprops
    2.19        |> Drule.forall_intr_list cparms
    2.20        |> Drule.forall_elim_vars (maxidx + 1);
    2.21 -    val elim_tacs = replicate (length cprops) Proof.hard_asm_tac;
    2.22 +    val elim_tacs = replicate (length cprops) (Tactic.etac Drule.triv_goal);
    2.23  
    2.24      val concl = Logic.strip_assums_concl prop;
    2.25      val bads = parms inter (Term.term_frees concl);
    2.26 @@ -100,14 +100,11 @@
    2.27        Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, bound_thesis))
    2.28        |> Library.curry Logic.list_rename_params (map #2 parm_names);
    2.29  
    2.30 -    fun export_obtained rule =
    2.31 -      (disch_obtained state parms rule, fn _ => fn _ => []);
    2.32 -
    2.33      fun after_qed st = st
    2.34        |> Proof.end_block
    2.35        |> Seq.map (fn st' => st'
    2.36          |> Proof.fix_i vars
    2.37 -        |> Proof.assm_i (export_obtained (Proof.the_fact st')) asms);
    2.38 +        |> Proof.assm_i (export_obtain state parms (Proof.the_fact st')) asms);
    2.39    in
    2.40      state
    2.41      |> Proof.enter_forward
     3.1 --- a/src/Pure/Isar/proof.ML	Tue Oct 16 23:00:21 2001 +0200
     3.2 +++ b/src/Pure/Isar/proof.ML	Tue Oct 16 23:02:14 2001 +0200
     3.3 @@ -62,8 +62,6 @@
     3.4      (thm list * context attribute list) list) list -> state -> state
     3.5    val fix: (string list * string option) list -> state -> state
     3.6    val fix_i: (string list * typ option) list -> state -> state
     3.7 -  val hard_asm_tac: int -> tactic
     3.8 -  val soft_asm_tac: int -> tactic
     3.9    val assm: ProofContext.exporter
    3.10      -> ((string * context attribute list) * (string * (string list * string list)) list) list
    3.11      -> state -> state
    3.12 @@ -413,20 +411,26 @@
    3.13  
    3.14  (* export results *)
    3.15  
    3.16 +fun refine_tac rule =
    3.17 +  Tactic.rtac rule THEN_ALL_NEW (SUBGOAL (fn (goal, i) =>
    3.18 +    if can Logic.dest_goal (Logic.strip_assums_concl goal) then
    3.19 +      Tactic.etac Drule.triv_goal i
    3.20 +    else all_tac));
    3.21 +
    3.22  fun export_goal print_rule raw_rule inner state =
    3.23    let
    3.24      val (outer, (_, ((result, (facts, thm)), f))) = find_goal state;
    3.25 -    val (exp_tac, tacs) = ProofContext.export_wrt true inner (Some outer);
    3.26 +    val exp_tac = ProofContext.export_wrt true inner (Some outer);
    3.27      fun exp_rule rule =
    3.28        let
    3.29          val _ = print_rule rule;
    3.30 -        val thmq = FINDGOAL (Tactic.rtac rule THEN' RANGE tacs) thm;
    3.31 +        val thmq = FINDGOAL (refine_tac rule) thm;
    3.32        in Seq.map (fn th => map_goal I (K ((result, (facts, th)), f)) state) thmq end;
    3.33    in raw_rule |> exp_tac |> (Seq.flat o Seq.map exp_rule) end;
    3.34  
    3.35  fun export_thm inner thm =
    3.36 -  let val (exp_tac, tacs) = ProofContext.export_wrt false inner None in
    3.37 -    (case Seq.chop (2, (exp_tac THEN RANGE tacs 1) thm) of
    3.38 +  let val exp_tac = ProofContext.export_wrt false inner None in
    3.39 +    (case Seq.chop (2, exp_tac thm) of
    3.40        ([thm'], _) => thm'
    3.41      | ([], _) => raise THM ("export: failed", 0, [thm])
    3.42      | _ => raise THM ("export: more than one result", 0, [thm]))
    3.43 @@ -437,9 +441,9 @@
    3.44      None => Seq.single (reset_facts state)
    3.45    | Some thms =>
    3.46        let
    3.47 -        val (exp_tac, tacs) =
    3.48 +        val exp_tac =
    3.49            ProofContext.export_wrt false (context_of inner_state) (Some (context_of state));
    3.50 -        val thmqs = map (exp_tac THEN RANGE tacs 1) thms;
    3.51 +        val thmqs = map exp_tac thms;
    3.52        in Seq.map (fn ths => put_facts (Some ths) state) (Seq.commute thmqs) end);
    3.53  
    3.54  
    3.55 @@ -460,7 +464,7 @@
    3.56      val tsig = Sign.tsig_of sign;
    3.57  
    3.58      val casms = flat (map #1 (assumptions state));
    3.59 -    val bad_hyps = Library.gen_rems Term.aconv (hyps, map (Thm.term_of o Drule.mk_cgoal) casms);
    3.60 +    val bad_hyps = Library.gen_rems Term.aconv (hyps, map Thm.term_of casms);
    3.61    in
    3.62      if not (null bad_hyps) then
    3.63        err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) bad_hyps))
    3.64 @@ -518,9 +522,6 @@
    3.65  
    3.66  (* assume *)
    3.67  
    3.68 -val hard_asm_tac = Tactic.etac Drule.triv_goal;
    3.69 -val soft_asm_tac = Tactic.rtac Drule.triv_goal THEN' Tactic.norm_hhf_tac;
    3.70 -
    3.71  local
    3.72  
    3.73  fun gen_assume f exp args state =
    3.74 @@ -531,18 +532,19 @@
    3.75      these_factss (st, factss)
    3.76      |> put_thms ("prems", prems));
    3.77  
    3.78 -fun simple_exporter tac1 tac2 =
    3.79 -  (Seq.single oo Drule.implies_intr_list, fn is_goal => fn n =>
    3.80 -    replicate n (Tactic.norm_hhf_tac THEN' (if is_goal then tac1 else tac2)));
    3.81 +fun export_assume true = Seq.single oo Drule.implies_intr_goals
    3.82 +  | export_assume false = Seq.single oo Drule.implies_intr_list;
    3.83 +
    3.84 +fun export_presume _ = export_assume false;
    3.85  
    3.86  in
    3.87  
    3.88  val assm = gen_assume ProofContext.assume;
    3.89  val assm_i = gen_assume ProofContext.assume_i;
    3.90 -val assume = assm (simple_exporter hard_asm_tac soft_asm_tac);
    3.91 -val assume_i = assm_i (simple_exporter hard_asm_tac soft_asm_tac);
    3.92 -val presume = assm (simple_exporter soft_asm_tac soft_asm_tac);
    3.93 -val presume_i = assm_i (simple_exporter soft_asm_tac soft_asm_tac);
    3.94 +val assume = assm export_assume;
    3.95 +val assume_i = assm_i export_assume;
    3.96 +val presume = assm export_presume;
    3.97 +val presume_i = assm_i export_presume;
    3.98  
    3.99  end;
   3.100  
   3.101 @@ -676,7 +678,7 @@
   3.102      val outer_ctxt = context_of outer_state;
   3.103  
   3.104      val result = prep_result state t raw_thm;
   3.105 -    val resultq = #1 (ProofContext.export_wrt false goal_ctxt (Some outer_ctxt)) result;
   3.106 +    val resultq = ProofContext.export_wrt false goal_ctxt (Some outer_ctxt) result;
   3.107  
   3.108      val (atts, opt_solve) =
   3.109        (case kind of
     4.1 --- a/src/Pure/Isar/proof_context.ML	Tue Oct 16 23:00:21 2001 +0200
     4.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Oct 16 23:02:14 2001 +0200
     4.3 @@ -42,7 +42,7 @@
     4.4    val generalizeT: context -> context -> typ -> typ
     4.5    val generalize: context -> context -> term -> term
     4.6    val find_free: term -> string -> term option
     4.7 -  val export_wrt: bool -> context -> context option -> (thm -> thm Seq.seq) * (int -> tactic) list
     4.8 +  val export_wrt: bool -> context -> context option -> thm -> thm Seq.seq
     4.9    val drop_schematic: indexname * term option -> indexname * term option
    4.10    val add_binds: (indexname * string option) list -> context -> context
    4.11    val add_binds_i: (indexname * term option) list -> context -> context
    4.12 @@ -120,8 +120,7 @@
    4.13  
    4.14  (** datatype context **)
    4.15  
    4.16 -type exporter =
    4.17 -  (cterm list -> thm -> thm Seq.seq) * (bool -> int -> (int -> tactic) list);
    4.18 +type exporter = bool -> cterm list -> thm -> thm Seq.seq;
    4.19  
    4.20  datatype context =
    4.21    Context of
    4.22 @@ -578,40 +577,31 @@
    4.23  
    4.24  fun find_free t x = foldl_aterms (get_free x) (None, t);
    4.25  
    4.26 -
    4.27 -local
    4.28 -
    4.29 -fun export tfrees fixes goal_asms thm =
    4.30 -  thm
    4.31 -  |> Tactic.norm_hhf
    4.32 -  |> Seq.EVERY (rev (map op |> goal_asms))
    4.33 -  |> Seq.map (fn rule =>
    4.34 -    let
    4.35 -      val {sign, prop, maxidx, ...} = Thm.rep_thm rule;
    4.36 -      val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) fixes);
    4.37 -    in
    4.38 -      rule
    4.39 -      |> Drule.forall_intr_list frees
    4.40 -      |> Tactic.norm_hhf
    4.41 -      |> Drule.tvars_intr_list tfrees
    4.42 -    end);
    4.43 -
    4.44  fun diff_context inner None = (gen_tfrees inner None, fixed_names inner, assumptions inner)
    4.45    | diff_context inner (Some outer) =
    4.46        (gen_tfrees inner (Some outer),
    4.47          fixed_names inner \\ fixed_names outer,
    4.48          Library.drop (length (assumptions outer), assumptions inner));
    4.49  
    4.50 -in
    4.51 -
    4.52  fun export_wrt is_goal inner opt_outer =
    4.53    let
    4.54      val (tfrees, fixes, asms) = diff_context inner opt_outer;
    4.55 -    val goal_asms = map (fn (cprops, (exp, _)) => (map Drule.mk_cgoal cprops, exp)) asms;
    4.56 -    val tacs = flat (map (fn (cprops, (_, f)) => f is_goal (length cprops)) asms);
    4.57 -  in (export tfrees fixes goal_asms, tacs) end;
    4.58 -
    4.59 -end;
    4.60 +    val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms;
    4.61 +  in fn thm =>
    4.62 +    thm
    4.63 +    |> Tactic.norm_hhf
    4.64 +    |> Seq.EVERY (rev exp_asms)
    4.65 +    |> Seq.map (fn rule =>
    4.66 +      let
    4.67 +        val {sign, prop, ...} = Thm.rep_thm rule;
    4.68 +        val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) fixes);
    4.69 +      in
    4.70 +        rule
    4.71 +        |> Drule.forall_intr_list frees
    4.72 +        |> Tactic.norm_hhf
    4.73 +        |> Drule.tvars_intr_list tfrees
    4.74 +      end)
    4.75 +  end;
    4.76  
    4.77  
    4.78  
    4.79 @@ -849,7 +839,7 @@
    4.80  fun add_assm (ctxt, ((name, attrs), props)) =
    4.81    let
    4.82      val cprops = map (Thm.cterm_of (sign_of ctxt)) props;
    4.83 -    val asms = map (Tactic.norm_hhf o Drule.assume_goal) cprops;
    4.84 +    val asms = map (Tactic.norm_hhf o Thm.assume) cprops;
    4.85  
    4.86      val ths = map (fn th => ([th], [])) asms;
    4.87      val (ctxt', [(_, thms)]) =