src/Pure/Isar/proof.ML
changeset 8617 33e2bd53aec3
parent 8582 3051aa8aa412
child 8670 d69616c74211
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Mar 30 14:28:10 2000 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Mar 30 14:28:54 2000 +0200
     1.3 @@ -44,10 +44,11 @@
     1.4    val method_cases: (thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq) -> method
     1.5    val refine: (context -> method) -> state -> state Seq.seq
     1.6    val refine_end: (context -> method) -> state -> state Seq.seq
     1.7 -  val find_free: term -> string -> term option
     1.8    val export_thm: context -> thm -> thm
     1.9    val match_bind: (string list * string) list -> state -> state
    1.10    val match_bind_i: (term list * term) list -> state -> state
    1.11 +  val let_bind: (string list * string) list -> state -> state
    1.12 +  val let_bind_i: (term list * term) list -> state -> state
    1.13    val have_thmss: thm list -> string -> context attribute list ->
    1.14      (thm list * context attribute list) list -> state -> state
    1.15    val simple_have_thms: string -> thm list -> state -> state
    1.16 @@ -77,7 +78,6 @@
    1.17    val lemma_i: bstring -> theory attribute list -> term * (term list * term list)
    1.18      -> theory -> state
    1.19    val chain: state -> state
    1.20 -  val export_chain: state -> state Seq.seq
    1.21    val from_facts: thm list -> state -> state
    1.22    val show: (state -> state Seq.seq) -> string -> context attribute list
    1.23      -> string * (string list * string list) -> state -> state
    1.24 @@ -379,49 +379,6 @@
    1.25  end;
    1.26  
    1.27  
    1.28 -(* export *)
    1.29 -
    1.30 -fun get_free x (None, t as Free (y, _)) = if x = y then Some t else None
    1.31 -  | get_free _ (opt, _) = opt;
    1.32 -
    1.33 -fun find_free t x = foldl_aterms (get_free x) (None, t);
    1.34 -
    1.35 -
    1.36 -local
    1.37 -
    1.38 -fun varify_frees fixes thm =
    1.39 -  let
    1.40 -    val {sign, prop, ...} = Thm.rep_thm thm;
    1.41 -    val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) fixes);
    1.42 -  in
    1.43 -    thm
    1.44 -    |> Drule.forall_intr_list frees
    1.45 -    |> Drule.forall_elim_vars 0
    1.46 -  end;
    1.47 -
    1.48 -fun export fixes casms thm =
    1.49 -  thm
    1.50 -  |> Drule.implies_intr_list casms
    1.51 -  |> varify_frees fixes
    1.52 -  |> ProofContext.most_general_varify_tfrees;
    1.53 -
    1.54 -fun diff_context inner None = (ProofContext.fixed_names inner, ProofContext.assumptions inner)
    1.55 -  | diff_context inner (Some outer) =
    1.56 -      (ProofContext.fixed_names inner \\ ProofContext.fixed_names outer,
    1.57 -        Library.drop (length (ProofContext.assumptions outer), ProofContext.assumptions inner));
    1.58 -
    1.59 -in
    1.60 -
    1.61 -fun export_wrt inner opt_outer =
    1.62 -  let
    1.63 -    val (fixes, asms) = diff_context inner opt_outer;
    1.64 -    val casms = map (Drule.mk_cgoal o #1) asms;
    1.65 -    val tacs = map #2 asms;
    1.66 -  in (export fixes casms, tacs) end;
    1.67 -
    1.68 -end;
    1.69 -
    1.70 -
    1.71  (* export results *)
    1.72  
    1.73  fun RANGE [] _ = all_tac
    1.74 @@ -436,7 +393,7 @@
    1.75  fun export_goal print_rule raw_rule inner state =
    1.76    let
    1.77      val (outer, (_, ((result, (facts, thm)), f))) = find_goal 0 state;
    1.78 -    val (exp, tacs) = export_wrt inner (Some outer);
    1.79 +    val (exp, tacs) = ProofContext.export_wrt inner (Some outer);
    1.80      val rule = exp raw_rule;
    1.81      val _ = print_rule rule;
    1.82      val thmq = FINDGOAL (Tactic.rtac rule THEN' RANGE (map #1 tacs)) thm;
    1.83 @@ -444,25 +401,22 @@
    1.84  
    1.85  
    1.86  fun export_thm inner thm =
    1.87 -  let val (exp, tacs) = export_wrt inner None in
    1.88 +  let val (exp, tacs) = ProofContext.export_wrt inner None in
    1.89      (case Seq.chop (2, RANGE (map #2 tacs) 1 (exp thm)) of
    1.90        ([thm'], _) => thm'
    1.91      | ([], _) => raise THM ("export: failed", 0, [thm])
    1.92      | _ => raise THM ("export: more than one result", 0, [thm]))
    1.93    end;
    1.94  
    1.95 -
    1.96 -fun export_facts inner_state opt_outer_state state =
    1.97 -  let
    1.98 -    val thms = the_facts inner_state;
    1.99 -    val (exp, tacs) = export_wrt (context_of inner_state) (apsome context_of opt_outer_state);
   1.100 -    val thmqs = map (RANGE (map #2 tacs) 1 o exp) thms;
   1.101 -  in Seq.map (fn ths => put_facts (Some ths) state) (Seq.commute thmqs) end;
   1.102 -
   1.103  fun transfer_facts inner_state state =
   1.104    (case get_facts inner_state of
   1.105      None => Seq.single (reset_facts state)
   1.106 -  | Some ths => export_facts inner_state (Some state) state);
   1.107 +  | Some thms =>
   1.108 +      let
   1.109 +        val (exp, tacs) =
   1.110 +          ProofContext.export_wrt (context_of inner_state) (Some (context_of state));
   1.111 +        val thmqs = map (RANGE (map #2 tacs) 1 o exp) thms;
   1.112 +      in Seq.map (fn ths => put_facts (Some ths) state) (Seq.commute thmqs) end);
   1.113  
   1.114  
   1.115  (* prepare result *)
   1.116 @@ -478,7 +432,7 @@
   1.117        else (Locale.print_goals ngoals raw_thm; err (string_of_int ngoals ^ " unsolved goal(s)!"));
   1.118  
   1.119      val thm = raw_thm RS Drule.rev_triv_goal;
   1.120 -    val {hyps, prop, sign, maxidx, ...} = Thm.rep_thm thm;
   1.121 +    val {hyps, prop, sign, ...} = Thm.rep_thm thm;
   1.122      val tsig = Sign.tsig_of sign;
   1.123  
   1.124      val casms = map #1 (assumptions state);
   1.125 @@ -488,7 +442,7 @@
   1.126        err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) bad_hyps))
   1.127      else if not (t aconv prop) then
   1.128        err ("Proved a different theorem: " ^ Sign.string_of_term sign prop)
   1.129 -    else thm |> Drule.forall_elim_vars (maxidx + 1) |> ProofContext.most_general_varify_tfrees
   1.130 +    else thm
   1.131    end;
   1.132  
   1.133  
   1.134 @@ -505,8 +459,10 @@
   1.135    |> map_context (f x)
   1.136    |> reset_facts;
   1.137  
   1.138 -val match_bind = gen_bind ProofContext.match_bind;
   1.139 -val match_bind_i = gen_bind ProofContext.match_bind_i;
   1.140 +val match_bind = gen_bind (ProofContext.match_bind false);
   1.141 +val match_bind_i = gen_bind (ProofContext.match_bind_i false);
   1.142 +val let_bind = gen_bind (ProofContext.match_bind true);
   1.143 +val let_bind_i = gen_bind (ProofContext.match_bind_i true);
   1.144  
   1.145  
   1.146  (* have_thmss *)
   1.147 @@ -547,7 +503,7 @@
   1.148  
   1.149  val hard_asm_tac = Tactic.etac Drule.triv_goal;
   1.150  val soft_asm_tac = Tactic.rtac Drule.triv_goal
   1.151 -  THEN' Tactic.rtac asm_rl;	(* FIXME hack to norm goal *)
   1.152 +  THEN' Tactic.rtac asm_rl;     (* FIXME hack to norm goal *)
   1.153  
   1.154  in
   1.155  
   1.156 @@ -582,12 +538,6 @@
   1.157    |> assert_facts
   1.158    |> enter_forward_chain;
   1.159  
   1.160 -fun export_chain state =
   1.161 -  state
   1.162 -  |> assert_forward
   1.163 -  |> export_facts state None
   1.164 -  |> Seq.map chain;
   1.165 -
   1.166  fun from_facts facts state =
   1.167    state
   1.168    |> put_facts (Some facts)
   1.169 @@ -598,17 +548,17 @@
   1.170  
   1.171  fun setup_goal opt_block prepp kind after_qed name atts raw_propp state =
   1.172    let
   1.173 -    val (state', prop) =
   1.174 +    val (state', (prop, gen_binds)) =
   1.175        state
   1.176        |> assert_forward_or_chain
   1.177        |> enter_forward
   1.178 +      |> opt_block
   1.179        |> map_context_result (fn ct => prepp (ct, raw_propp));
   1.180      val cprop = Thm.cterm_of (sign_of state') prop;
   1.181      val goal = Drule.mk_triv_goal cprop;
   1.182    in
   1.183      state'
   1.184 -    |> opt_block
   1.185 -    |> put_goal (Some (((kind atts, name, prop), ([], goal)), after_qed))
   1.186 +    |> put_goal (Some (((kind atts, name, prop), ([], goal)), after_qed o map_context gen_binds))
   1.187      |> auto_bind_goal prop
   1.188      |> (if is_chain state then use_facts else reset_facts)
   1.189      |> new_block
   1.190 @@ -673,19 +623,22 @@
   1.191  
   1.192  fun finish_local (print_result, print_rule) state =
   1.193    let
   1.194 -    val (ctxt, (((kind, name, t), (_, raw_thm)), after_qed)) = current_goal state;
   1.195 +    val (goal_ctxt, (((kind, name, t), (_, raw_thm)), after_qed)) = current_goal state;
   1.196 +    val outer_state = state |> close_block;
   1.197 +    val outer_ctxt = context_of outer_state;
   1.198 +
   1.199      val result = prep_result state t raw_thm;
   1.200      val (atts, opt_solve) =
   1.201        (case kind of
   1.202 -        Goal atts => (atts, export_goal print_rule result ctxt)
   1.203 +        Goal atts => (atts, export_goal print_rule result goal_ctxt)
   1.204        | Aux atts => (atts, Seq.single)
   1.205        | _ => err_malformed "finish_local" state);
   1.206    in
   1.207      print_result {kind = kind_name kind, name = name, thm = result};
   1.208 -    state
   1.209 -    |> close_block
   1.210 -    |> auto_bind_facts name [t]
   1.211 -    |> have_thmss [] name atts [Thm.no_attributes [result]]
   1.212 +    outer_state
   1.213 +    |> auto_bind_facts name [ProofContext.generalize goal_ctxt outer_ctxt t]
   1.214 +    |> have_thmss [] name atts [Thm.no_attributes
   1.215 +        [#1 (ProofContext.export_wrt goal_ctxt (Some outer_ctxt)) result]]
   1.216      |> opt_solve
   1.217      |> (Seq.flat o Seq.map after_qed)
   1.218    end;