1.1 --- a/src/Pure/Isar/isar_syn.ML Sun Jun 11 21:59:23 2006 +0200
1.2 +++ b/src/Pure/Isar/isar_syn.ML Sun Jun 11 21:59:24 2006 +0200
1.3 @@ -449,7 +449,7 @@
1.4 val fixP =
1.5 OuterSyntax.command "fix" "fix local variables (Skolem constants)"
1.6 (K.tag_proof K.prf_asm)
1.7 - (P.simple_fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
1.8 + (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
1.9
1.10 val assumeP =
1.11 OuterSyntax.command "assume" "assume propositions"
1.12 @@ -465,19 +465,20 @@
1.13 OuterSyntax.command "def" "local definition"
1.14 (K.tag_proof K.prf_asm)
1.15 (P.and_list1
1.16 - (P.opt_thm_name ":" -- (P.name -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
1.17 + (P.opt_thm_name ":" --
1.18 + ((P.name -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
1.19 >> (Toplevel.print oo (Toplevel.proof o Proof.def)));
1.20
1.21 val obtainP =
1.22 OuterSyntax.command "obtain" "generalized existence"
1.23 (K.tag_proof K.prf_asm_goal)
1.24 - (P.parname -- Scan.optional (P.simple_fixes --| P.$$$ "where") [] -- P.statement
1.25 + (P.parname -- Scan.optional (P.fixes --| P.$$$ "where") [] -- P.statement
1.26 >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z)));
1.27
1.28 val guessP =
1.29 OuterSyntax.command "guess" "wild guessing (unstructured)"
1.30 (K.tag_proof K.prf_asm_goal)
1.31 - (Scan.optional P.simple_fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
1.32 + (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
1.33
1.34 val letP =
1.35 OuterSyntax.command "let" "bind text variables"
2.1 --- a/src/Pure/Isar/obtain.ML Sun Jun 11 21:59:23 2006 +0200
2.2 +++ b/src/Pure/Isar/obtain.ML Sun Jun 11 21:59:24 2006 +0200
2.3 @@ -39,14 +39,14 @@
2.4
2.5 signature OBTAIN =
2.6 sig
2.7 - val obtain: string -> (string * string option) list ->
2.8 + val obtain: string -> (string * string option * mixfix) list ->
2.9 ((string * Attrib.src list) * (string * string list) list) list
2.10 -> bool -> Proof.state -> Proof.state
2.11 - val obtain_i: string -> (string * typ option) list ->
2.12 + val obtain_i: string -> (string * typ option * mixfix) list ->
2.13 ((string * attribute list) * (term * term list) list) list
2.14 -> bool -> Proof.state -> Proof.state
2.15 - val guess: (string * string option) list -> bool -> Proof.state -> Proof.state
2.16 - val guess_i: (string * typ option) list -> bool -> Proof.state -> Proof.state
2.17 + val guess: (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state
2.18 + val guess_i: (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
2.19 val statement: (string * ((string * 'typ option) list * 'term list)) list ->
2.20 (('typ, 'term, 'fact) Element.ctxt list *
2.21 ((string * Attrib.src list) * ('term * 'term list) list) list) *
2.22 @@ -112,7 +112,7 @@
2.23 val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
2.24
2.25 (*obtain vars*)
2.26 - val (vars, vars_ctxt) = prep_vars (map Syntax.no_syn raw_vars) ctxt;
2.27 + val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
2.28 val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
2.29 val xs = map #1 vars;
2.30
2.31 @@ -145,14 +145,14 @@
2.32 fun after_qed _ =
2.33 Proof.local_qed (NONE, false)
2.34 #> Seq.map (`Proof.the_fact #-> (fn rule =>
2.35 - Proof.fix_i (xs ~~ map #2 vars)
2.36 + Proof.fix_i (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
2.37 #> Proof.assm_i (K (obtain_export ctxt parms rule)) asms));
2.38 in
2.39 state
2.40 |> Proof.enter_forward
2.41 |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, [])])] int
2.42 |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
2.43 - |> Proof.fix_i [(thesisN, NONE)]
2.44 + |> Proof.fix_i [(thesisN, NONE, NoSyn)]
2.45 |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
2.46 |> `Proof.the_facts
2.47 ||> Proof.chain_facts chain_facts
2.48 @@ -231,8 +231,7 @@
2.49 val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
2.50
2.51 val (thesis_var, thesis) = bind_judgment ctxt AutoBind.thesisN;
2.52 - val vars = ctxt |> prep_vars (map Syntax.no_syn raw_vars)
2.53 - |-> fold_map inferred_type |> polymorphic;
2.54 + val vars = ctxt |> prep_vars raw_vars |-> fold_map inferred_type |> polymorphic;
2.55
2.56 fun check_result th =
2.57 (case Thm.prems_of th of
2.58 @@ -254,7 +253,7 @@
2.59 |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), []));
2.60 val _ = not (null asms) orelse error "Trivial result -- nothing guessed";
2.61 in
2.62 - Proof.fix_i (map (apsnd SOME) parms)
2.63 + Proof.fix_i (map2 (fn (x, T) => fn (_, mx) => (x, SOME T, mx)) parms vars)
2.64 #> Proof.assm_i (K (obtain_export ctxt ts rule)) [(("", []), asms)]
2.65 #> Proof.add_binds_i AutoBind.no_facts
2.66 end;
2.67 @@ -270,7 +269,7 @@
2.68 state
2.69 |> Proof.enter_forward
2.70 |> Proof.begin_block
2.71 - |> Proof.fix_i [(AutoBind.thesisN, NONE)]
2.72 + |> Proof.fix_i [(AutoBind.thesisN, NONE, NoSyn)]
2.73 |> Proof.chain_facts chain_facts
2.74 |> Proof.local_goal print_result (K I) (apsnd (rpair I))
2.75 "guess" before_qed after_qed [(("", []), [Logic.mk_term goal, goal])]