bind_skolem;
authorwenzelm
Thu Jul 13 11:39:22 2000 +0200 (2000-07-13)
changeset 92933da2533e0a61
parent 9292 c5875175751f
child 9294 9ecb78a8d471
bind_skolem;
src/Pure/Isar/obtain.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Thu Jul 13 11:39:03 2000 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Thu Jul 13 11:39:22 2000 +0200
     1.3 @@ -73,23 +73,29 @@
     1.4      val (vars_ctxt, vars) =
     1.5        foldl_map prep_vars (Proof.context_of state, map Comment.ignore raw_vars);
     1.6      val xs = flat (map fst vars);
     1.7 +    val xs_thesis = xs @ [AutoBind.thesisN];
     1.8 +
     1.9 +    val bind_skolem = ProofContext.bind_skolem vars_ctxt xs_thesis;
    1.10 +    fun bind_propp (prop, (pats1, pats2)) =
    1.11 +      (bind_skolem prop, (map bind_skolem pats1, map bind_skolem pats2));
    1.12  
    1.13      (*obtain asms*)
    1.14      fun prep_asm (ctxt, (name, src, raw_propps)) =
    1.15        let
    1.16          val atts = map (prep_att (ProofContext.theory_of ctxt)) src;
    1.17          val (ctxt', propps) = foldl_map prep_propp (ctxt, raw_propps);
    1.18 -      in (ctxt', (name, atts, propps)) end;
    1.19 +      in (ctxt', ((name, atts, map bind_propp propps), map #1 propps)) end;
    1.20  
    1.21 -    val (asms_ctxt, asms) = foldl_map prep_asm (vars_ctxt, map Comment.ignore raw_asms);
    1.22 -    val asm_props = flat (map (map fst o #3) asms);
    1.23 +    val (asms_ctxt, asms_result) = foldl_map prep_asm (vars_ctxt, map Comment.ignore raw_asms);
    1.24 +    val (asms, asm_propss) = Library.split_list asms_result;
    1.25 +    val asm_props = flat asm_propss;
    1.26      val _ = ProofContext.warn_extra_tfrees vars_ctxt asms_ctxt;
    1.27  
    1.28      (*thesis*)
    1.29 -    val (prop, (goal_facts, goal)) = Proof.get_goal state;
    1.30 +    val (prop, (goal_facts, _)) = Proof.get_goal state;
    1.31  
    1.32      val parms = Logic.strip_params prop;
    1.33 -    val parm_names = Term.variantlist (map #1 parms, Term.add_term_names (prop, xs));
    1.34 +    val parm_names = Term.variantlist (map #1 parms, Term.add_term_names (prop, xs_thesis));
    1.35      val parm_types = map #2 parms;
    1.36      val parm_vars = map Library.single parm_names ~~ map Some parm_types;
    1.37  
    1.38 @@ -98,14 +104,15 @@
    1.39  
    1.40      val hyps = map (fn t => Term.subst_bounds (rev_frees, t)) (Logic.strip_assums_hyp prop);
    1.41      val concl = Term.subst_bounds (rev_frees, Logic.strip_assums_concl prop);
    1.42 -    val ((thesis_name, thesis_term), atomic_thesis) = AutoBind.atomic_thesis concl;
    1.43 +    val (thesis_term, atomic_thesis) = AutoBind.atomic_thesis concl;
    1.44 +    val bound_thesis = bind_skolem atomic_thesis;
    1.45  
    1.46      (*that_prop*)
    1.47      fun find_free x t =
    1.48        (case ProofContext.find_free t x of Some (Free a) => Some a | _ => None);
    1.49      fun occs_var x = Library.get_first (find_free x) asm_props;
    1.50      val that_prop =
    1.51 -      Term.list_all_free (mapfilter occs_var xs, Logic.list_implies (asm_props, atomic_thesis));
    1.52 +      Term.list_all_free (mapfilter occs_var xs, Logic.list_implies (asm_props, bound_thesis));
    1.53  
    1.54      fun after_qed st =
    1.55        st
    1.56 @@ -119,10 +126,10 @@
    1.57      |> Seq.map (fn st => st
    1.58        |> Proof.fix_i parm_vars
    1.59        |> Proof.assume_i [(hypsN, [], map (rpair ([], [])) hyps)]
    1.60 -      |> LocalDefs.def_i "" [] ((thesis_name, None), (thesis_term, []))
    1.61 +      |> LocalDefs.def_i "" [] ((AutoBind.thesisN, None), (thesis_term, []))
    1.62        |> Proof.presume_i [(thatN, Data.that_atts, [(that_prop, ([], []))])]
    1.63        |> Proof.from_facts goal_facts
    1.64 -      |> Proof.show_i after_qed "" [] (atomic_thesis, ([], [])))
    1.65 +      |> Proof.show_i after_qed "" [] (bound_thesis, ([], [])))
    1.66    end;
    1.67  
    1.68