src/Pure/Isar/obtain.ML
author wenzelm
Thu Dec 06 00:43:03 2001 +0100 (2001-12-06)
changeset 12404 968213967c07
parent 12350 5fad0e7129c3
child 12970 c9b1838a2cc0
permissions -rw-r--r--
Syntax.internal thesis;
     1 (*  Title:      Pure/Isar/obtain.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 The 'obtain' language element -- generalized existence at the level of
     7 proof texts.
     8 
     9   <chain_facts>
    10   obtain x where "P x" <proof> ==
    11 
    12   {
    13     fix thesis
    14     assume that [intro]: "!!x. P x ==> thesis"
    15     <chain_facts> have thesis <proof (insert that)>
    16   }
    17   fix x assm (obtained) "P x"
    18 
    19 *)
    20 
    21 signature OBTAIN =
    22 sig
    23   val obtain: (string list * string option) list ->
    24     ((string * Proof.context attribute list) * (string * (string list * string list)) list) list
    25     -> Proof.state -> Proof.state Seq.seq
    26   val obtain_i: (string list * typ option) list ->
    27     ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
    28     -> Proof.state -> Proof.state Seq.seq
    29 end;
    30 
    31 structure Obtain: OBTAIN =
    32 struct
    33 
    34 
    35 (** export_obtain **)
    36 
    37 fun export_obtain state parms rule _ cprops thm =
    38   let
    39     val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
    40     val cparms = map (Thm.cterm_of sign) parms;
    41 
    42     val thm' = thm
    43       |> Drule.implies_intr_goals cprops
    44       |> Drule.forall_intr_list cparms
    45       |> Drule.forall_elim_vars (maxidx + 1);
    46     val elim_tacs = replicate (length cprops) (Tactic.etac Drule.triv_goal);
    47 
    48     val concl = Logic.strip_assums_concl prop;
    49     val bads = parms inter (Term.term_frees concl);
    50   in
    51     if not (null bads) then
    52       raise Proof.STATE ("Conclusion contains obtained parameters: " ^
    53         space_implode " " (map (ProofContext.string_of_term (Proof.context_of state)) bads), state)
    54     else if not (ObjectLogic.is_judgment sign (Logic.strip_assums_concl prop)) then
    55       raise Proof.STATE ("Conclusions of 'obtain' context must be object-logic judgments", state)
    56     else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
    57   end;
    58 
    59 
    60 
    61 (** obtain(_i) **)
    62 
    63 val thatN = "that";
    64 
    65 fun gen_obtain prep_vars prep_propp raw_vars raw_asms state =
    66   let
    67     val _ = Proof.assert_forward_or_chain state;
    68     val chain_facts = if Proof.is_chain state then Proof.the_facts state else [];
    69     val thy = Proof.theory_of state;
    70     val sign = Theory.sign_of thy;
    71 
    72     (*obtain vars*)
    73     val (vars_ctxt, vars) = foldl_map prep_vars (Proof.context_of state, raw_vars);
    74     val xs = flat (map fst vars);
    75     val fix_ctxt = vars_ctxt |> ProofContext.fix_i vars;
    76 
    77     (*obtain asms*)
    78     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
    79     val asm_props = flat (map (map fst) proppss);
    80     val asms = map fst raw_asms ~~ proppss;
    81 
    82     val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
    83 
    84     (*that_prop*)
    85     val thesisN = Term.variant xs (Syntax.internal AutoBind.thesisN);
    86     val bound_thesis =
    87       ProofContext.bind_skolem fix_ctxt [thesisN] (ObjectLogic.fixed_judgment sign thesisN);
    88 
    89     fun occs_var x = Library.get_first (fn t =>
    90       ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
    91     val raw_parms = map occs_var xs;
    92     val parms = mapfilter I raw_parms;
    93     val parm_names =
    94       mapfilter (fn (Some (Free a), x) => Some (a, x) | _ => None) (raw_parms ~~ xs);
    95 
    96     val that_prop =
    97       Term.list_all_free (map #1 parm_names, Logic.list_implies (asm_props, bound_thesis))
    98       |> Library.curry Logic.list_rename_params (map #2 parm_names);
    99 
   100     fun after_qed st = st
   101       |> Proof.end_block
   102       |> Seq.map (fn st' => st'
   103         |> Proof.fix_i vars
   104         |> Proof.assm_i (export_obtain state parms (Proof.the_fact st')) asms);
   105   in
   106     state
   107     |> Proof.enter_forward
   108     |> Proof.begin_block
   109     |> Proof.fix_i [([thesisN], None)]
   110     |> Proof.assume_i [((thatN, [ContextRules.intro_query_local None]), [(that_prop, ([], []))])]
   111     |> (fn state' =>
   112       state'
   113       |> Proof.from_facts chain_facts
   114       |> Proof.have_i after_qed [(("", []), [(bound_thesis, ([], []))])]
   115       |> Method.refine (Method.Basic (K (Method.insert (Proof.the_facts state')))))
   116   end;
   117 
   118 val obtain = gen_obtain ProofContext.read_vars ProofContext.read_propp;
   119 val obtain_i = gen_obtain ProofContext.cert_vars ProofContext.cert_propp;
   120 
   121 
   122 end;