src/Pure/Isar/obtain.ML
changeset 9468 9adbcf6375c1
parent 9293 3da2533e0a61
child 9481 b16624f1ea38
     1.1 --- a/src/Pure/Isar/obtain.ML	Sun Jul 30 12:53:22 2000 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Sun Jul 30 12:54:07 2000 +0200
     1.3 @@ -6,43 +6,21 @@
     1.4  The 'obtain' language element -- generalized existence at the level of
     1.5  proof texts.
     1.6  
     1.7 -The common case:
     1.8 -
     1.9 -    <goal_facts>
    1.10 -    have/show C
    1.11 -      obtain a in P[a] <proof>          ==
    1.12 -
    1.13 -    <goal_facts>
    1.14 -    have/show C
    1.15 -    proof succeed
    1.16 -      def thesis == C
    1.17 -      presume that: !!a. P a ==> thesis
    1.18 -      from goal_facts show thesis <proof>
    1.19 -    next
    1.20 -      fix a
    1.21 -      assume P a
    1.22 +  <chain_facts>
    1.23 +  obtain x where "P x" <proof> ==
    1.24  
    1.25 -The general case:
    1.26 -
    1.27 -    <goal_facts>
    1.28 -    have/show !!x. G x ==> C x
    1.29 -      obtain a in P[a] <proof>          ==
    1.30 +  {
    1.31 +    fix thesis
    1.32 +    assume that: "!!x. P x ==> thesis"
    1.33 +    <chain_facts> have thesis <proof>
    1.34 +  }
    1.35 +  fix x assm(obtained) "P x"
    1.36  
    1.37 -    <goal_facts>
    1.38 -    have/show !!x. G x ==> C x
    1.39 -    proof succeed
    1.40 -      fix x
    1.41 -      assume hyps: G x
    1.42 -      def thesis == C x
    1.43 -      presume that: !!a. P a ==> thesis
    1.44 -      from goal_facts show thesis <proof>
    1.45 -    next
    1.46 -      fix a
    1.47 -      assume P a
    1.48  *)
    1.49  
    1.50  signature OBTAIN_DATA =
    1.51  sig
    1.52 +  val atomic_thesis: string -> term
    1.53    val that_atts: Proof.context attribute list
    1.54  end;
    1.55  
    1.56 @@ -60,22 +38,51 @@
    1.57  struct
    1.58  
    1.59  
    1.60 +(** export_obtained **)
    1.61 +
    1.62 +fun disch_obtained state parms rule cprops thm =
    1.63 +  let
    1.64 +    val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
    1.65 +    val cparms = map (Thm.cterm_of sign) parms;
    1.66 +
    1.67 +    val thm' = thm
    1.68 +      |> Drule.implies_intr_list cprops
    1.69 +      |> Drule.forall_intr_list cparms
    1.70 +      |> Drule.forall_elim_vars (maxidx + 1);
    1.71 +    val elim_tacs = replicate (length cprops) Proof.hard_asm_tac;
    1.72 +
    1.73 +    val concl = Logic.strip_assums_concl prop;
    1.74 +    val bads = parms inter (Term.term_frees concl);
    1.75 +  in
    1.76 +    if not (null bads) then
    1.77 +      raise Proof.STATE ("Result contains illegal parameters: " ^
    1.78 +        space_implode " " (map (Sign.string_of_term sign) bads), state)
    1.79 +    else if not (AutoBind.is_judgment (Logic.strip_assums_concl prop)) then
    1.80 +      raise Proof.STATE ("Conclusion of result is not an object-logic judgment", state)
    1.81 +    else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
    1.82 +  end;
    1.83 +
    1.84 +fun export_obtained state parms rule =
    1.85 +  (disch_obtained state parms rule, fn _ => fn _ => []);
    1.86 +
    1.87 +
    1.88 +
    1.89  (** obtain(_i) **)
    1.90  
    1.91  val thatN = "that";
    1.92 -val hypsN = "hyps";
    1.93  
    1.94  fun gen_obtain prep_vars prep_propp prep_att (raw_vars, raw_asms) state =
    1.95    let
    1.96 -    val _ = Proof.assert_backward state;
    1.97 +    val _ = Proof.assert_forward_or_chain state;
    1.98 +    val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
    1.99  
   1.100      (*obtain vars*)
   1.101      val (vars_ctxt, vars) =
   1.102        foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars);
   1.103      val xs = flat (map fst vars);
   1.104 -    val xs_thesis = xs @ [AutoBind.thesisN];
   1.105 +    val thesisN = Term.variant xs AutoBind.thesisN;
   1.106  
   1.107 -    val bind_skolem = ProofContext.bind_skolem vars_ctxt xs_thesis;
   1.108 +    val bind_skolem = ProofContext.bind_skolem vars_ctxt (xs @ [thesisN]);
   1.109      fun bind_propp (prop, (pats1, pats2)) =
   1.110        (bind_skolem prop, (map bind_skolem pats1, map bind_skolem pats2));
   1.111  
   1.112 @@ -91,52 +98,36 @@
   1.113      val asm_props = flat asm_propss;
   1.114      val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt;
   1.115  
   1.116 -    (*thesis*)
   1.117 -    val (prop, (goal_facts, _)) = Proof.get_goal state;
   1.118 -
   1.119 -    val parms = Logic.strip_params prop;
   1.120 -    val parm_names = Term.variantlist (map #1 parms, Term.add_term_names (prop, xs_thesis));
   1.121 -    val parm_types = map #2 parms;
   1.122 -    val parm_vars = map Library.single parm_names ~~ map Some parm_types;
   1.123 -
   1.124 -    val frees = map2 Free (parm_names, parm_types);
   1.125 -    val rev_frees = rev frees;
   1.126 -
   1.127 -    val hyps = map (fn t => Term.subst_bounds (rev_frees, t)) (Logic.strip_assums_hyp prop);
   1.128 -    val concl = Term.subst_bounds (rev_frees, Logic.strip_assums_concl prop);
   1.129 -    val (thesis_term, atomic_thesis) = AutoBind.atomic_thesis concl;
   1.130 -    val bound_thesis = bind_skolem atomic_thesis;
   1.131 -
   1.132      (*that_prop*)
   1.133      fun find_free x t =
   1.134        (case ProofContext.find_free t x of Some (Free a) => Some a | _ => None);
   1.135      fun occs_var x = Library.get_first (find_free x) asm_props;
   1.136 -    val that_prop =
   1.137 -      Term.list_all_free (mapfilter occs_var xs, Logic.list_implies (asm_props, bound_thesis));
   1.138 +    val xs' = mapfilter occs_var xs;
   1.139 +    val parms = map (bind_skolem o Free) xs';
   1.140 +
   1.141 +    val bound_thesis = bind_skolem (Data.atomic_thesis thesisN);
   1.142 +    val that_prop = Term.list_all_free (xs', Logic.list_implies (asm_props, bound_thesis));
   1.143  
   1.144 -    fun after_qed st =
   1.145 -      st
   1.146 -      |> Proof.next_block
   1.147 -      |> Proof.fix_i vars
   1.148 -      |> Proof.assume_i asms
   1.149 -      |> Seq.single;
   1.150 +    fun after_qed st = st
   1.151 +      |> Proof.end_block
   1.152 +      |> Seq.map (fn st' => st'
   1.153 +        |> Proof.fix_i vars
   1.154 +        |> Proof.assm_i (export_obtained state parms (Proof.the_fact st')) asms);
   1.155    in
   1.156      state
   1.157 -    |> Method.proof (Some (Method.Basic (K Method.succeed)))
   1.158 -    |> Seq.map (fn st => st
   1.159 -      |> Proof.fix_i parm_vars
   1.160 -      |> Proof.assume_i [(hypsN, [], map (rpair ([], [])) hyps)]
   1.161 -      |> LocalDefs.def_i "" [] ((AutoBind.thesisN, None), (thesis_term, []))
   1.162 -      |> Proof.presume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])]
   1.163 -      |> Proof.from_facts goal_facts
   1.164 -      |> Proof.show_i after_qed "" [] (bound_thesis, ([], [])))
   1.165 +    |> Proof.enter_forward
   1.166 +    |> Proof.begin_block
   1.167 +    |> Proof.fix_i [([thesisN], None)]
   1.168 +    |> Proof.assume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])]
   1.169 +    |> Proof.from_facts chain_facts
   1.170 +    |> Proof.have_i after_qed "" [] (bound_thesis, ([], []))
   1.171    end;
   1.172  
   1.173  
   1.174 -val obtain = ProofHistory.applys o
   1.175 +val obtain = ProofHistory.apply o
   1.176    (gen_obtain ProofContext.read_vars ProofContext.read_propp Attrib.local_attribute);
   1.177  
   1.178 -val obtain_i = ProofHistory.applys o
   1.179 +val obtain_i = ProofHistory.apply o
   1.180    (gen_obtain ProofContext.cert_vars ProofContext.cert_propp (K I));
   1.181  
   1.182  
   1.183 @@ -159,5 +150,4 @@
   1.184  
   1.185  end;
   1.186  
   1.187 -
   1.188  end;