--- a/src/HOL/List.thy Sun May 07 00:21:13 2006 +0200
+++ b/src/HOL/List.thy Sun May 07 00:22:05 2006 +0200
@@ -818,7 +818,7 @@
lemma Cons_eq_filterD:
"x#xs = filter P ys \<Longrightarrow>
\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
- (concl is "\<exists>us vs. ?P ys us vs")
+ (is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs")
proof(induct ys)
case Nil thus ?case by simp
next
--- a/src/HOL/Tools/function_package/fundef_package.ML Sun May 07 00:21:13 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Sun May 07 00:22:05 2006 +0200
@@ -68,7 +68,7 @@
in
thy |> ProofContext.init
|> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs curry_info name data natts) NONE ("", [])
- (map (fn t => (("", []), [(t, ([], []))])) props)
+ (map (fn t => (("", []), [(t, [])])) props)
end
@@ -138,7 +138,7 @@
|> ProofContext.note_thmss_i [(("termination_intro",
[ContextRules.intro_query NONE]), [([total_intro], [])])] |> snd
|> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name) NONE ("", [])
- [(("", []), [(goal, ([], []))])]
+ [(("", []), [(goal, [])])]
end
| fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
let
@@ -148,7 +148,7 @@
in
thy |> ProofContext.init
|> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
- [(("", []), [(subs, ([], [])), (dcl, ([], []))])]
+ [(("", []), [(subs, []), (dcl, [])])]
end
@@ -192,4 +192,4 @@
end;
-end
\ No newline at end of file
+end
--- a/src/HOL/Tools/recdef_package.ML Sun May 07 00:21:13 2006 +0200
+++ b/src/HOL/Tools/recdef_package.ML Sun May 07 00:22:05 2006 +0200
@@ -284,7 +284,7 @@
val tc = List.nth (tcs, i - 1) handle Subscript =>
error ("No termination condition #" ^ string_of_int i ^
" in recdef definition of " ^ quote name);
- in IsarThy.theorem_i PureThy.internalK (bname, atts) (HOLogic.mk_Trueprop tc, ([], [])) thy end;
+ in IsarThy.theorem_i PureThy.internalK (bname, atts) (HOLogic.mk_Trueprop tc, []) thy end;
val recdef_tc = gen_recdef_tc Attrib.attribute Sign.intern_const;
val recdef_tc_i = gen_recdef_tc (K I) (K I);
--- a/src/HOL/Tools/specification_package.ML Sun May 07 00:21:13 2006 +0200
+++ b/src/HOL/Tools/specification_package.ML Sun May 07 00:22:05 2006 +0200
@@ -231,7 +231,7 @@
in
IsarThy.theorem_i PureThy.internalK
("", [add_spec axiomatic (zip3 names cnames overloaded), post_proc])
- (HOLogic.mk_Trueprop ex_prop, ([], [])) thy
+ (HOLogic.mk_Trueprop ex_prop, []) thy
end
--- a/src/HOL/Tools/typedef_package.ML Sun May 07 00:21:13 2006 +0200
+++ b/src/HOL/Tools/typedef_package.ML Sun May 07 00:22:05 2006 +0200
@@ -271,7 +271,7 @@
fun att (thy, th) =
let val ((th', _), thy') = att_result th thy
in (thy', th') end;
- in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, ([goal_pat], [])) thy end;
+ in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, [goal_pat]) thy end;
in
--- a/src/HOLCF/pcpodef_package.ML Sun May 07 00:21:13 2006 +0200
+++ b/src/HOLCF/pcpodef_package.ML Sun May 07 00:22:05 2006 +0200
@@ -177,7 +177,7 @@
let
val (goal, att) =
gen_prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
- in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, ([], [])) thy end;
+ in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, []) thy end;
fun pcpodef_proof x = gen_pcpodef_proof read_term true x;
fun pcpodef_proof_i x = gen_pcpodef_proof cert_term true x;
--- a/src/Pure/Isar/element.ML Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/element.ML Sun May 07 00:22:05 2006 +0200
@@ -8,14 +8,14 @@
signature ELEMENT =
sig
datatype ('typ, 'term) stmt =
- Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
+ Shows of ((string * Attrib.src list) * ('term * 'term list) list) list |
Obtains of (string * ((string * 'typ option) list * 'term list)) list
type statement (*= (string, string) stmt*)
type statement_i (*= (typ, term) stmt*)
datatype ('typ, 'term, 'fact) ctxt =
Fixes of (string * 'typ option * mixfix) list |
Constrains of (string * 'typ) list |
- Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
+ Assumes of ((string * Attrib.src list) * ('term * 'term list) list) list |
Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list
type context (*= (string, string, thmref) ctxt*)
@@ -49,7 +49,7 @@
(** conclusions **)
datatype ('typ, 'term) stmt =
- Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
+ Shows of ((string * Attrib.src list) * ('term * 'term list) list) list |
Obtains of (string * ((string * 'typ option) list * 'term list)) list;
type statement = (string, string) stmt;
@@ -64,7 +64,7 @@
datatype ('typ, 'term, 'fact) ctxt =
Fixes of (string * 'typ option * mixfix) list |
Constrains of (string * 'typ) list |
- Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
+ Assumes of ((string * Attrib.src list) * ('term * 'term list) list) list |
Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list;
@@ -76,8 +76,7 @@
let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
| Constrains xs => Constrains (xs |> map (fn (x, T) => (#1 (var (x, NoSyn)), typ T)))
| Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
- ((name a, map attrib atts), propps |> map (fn (t, (ps, qs)) =>
- (term t, (map term ps, map term qs))))))
+ ((name a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps)))))
| Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
((name a, map attrib atts), (term t, map term ps))))
| Notes facts => Notes (facts |> map (fn ((a, atts), bs) =>
@@ -255,10 +254,11 @@
fun prt_var (x, SOME T) = Pretty.block [Pretty.str (x ^ " ::"), Pretty.brk 1, prt_typ T]
| prt_var (x, NONE) = Pretty.str x;
+ val prt_vars = separate (Pretty.keyword "and") o map prt_var;
fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
| prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks
- (map prt_var xs @ [Pretty.keyword "where"] @ prt_terms ts));
+ (prt_vars xs @ [Pretty.keyword "where"] @ prt_terms ts));
in
fn Shows shows => pretty_items "shows" "and" (map prt_show shows)
| Obtains obtains => pretty_items "obtains" "|" (map prt_obtain obtains)
@@ -349,9 +349,9 @@
val (asms, cases) = take_suffix (fn prem => thesis aconv Logic.strip_assums_concl prem) prems;
in
pretty_ctxt ctxt (Fixes (map (fn (x, T) => (x, SOME T, NoSyn)) fixes)) @
- pretty_ctxt ctxt (Assumes (map (fn t => (("", []), [(t, ([], []))])) asms)) @
+ pretty_ctxt ctxt (Assumes (map (fn t => (("", []), [(t, [])])) asms)) @
pretty_stmt ctxt
- (if null cases then Shows [(("", []), [(concl, ([], []))])]
+ (if null cases then Shows [(("", []), [(concl, [])])]
else Obtains (#1 (fold_map obtain cases (ctxt |> ProofContext.declare_term prop))))
end |> thm_name kind raw_th;
--- a/src/Pure/Isar/isar_thy.ML Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/isar_thy.ML Sun May 07 00:22:05 2006 +0200
@@ -24,18 +24,16 @@
theory -> Proof.context * theory
val declare_theorems: xstring option ->
(thmref * Attrib.src list) list -> theory -> Proof.context * theory
- val have: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
+ val have: ((string * Attrib.src list) * (string * string list) list) list ->
bool -> Proof.state -> Proof.state
- val hence: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
- bool -> Proof.state -> Proof.state
- val show: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
+ val hence: ((string * Attrib.src list) * (string * string list) list) list ->
bool -> Proof.state -> Proof.state
- val thus: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
+ val show: ((string * Attrib.src list) * (string * string list) list) list ->
bool -> Proof.state -> Proof.state
- val theorem: string -> string * Attrib.src list -> string * (string list * string list) ->
- theory -> Proof.state
- val theorem_i: string -> string * attribute list -> term * (term list * term list) ->
- theory -> Proof.state
+ val thus: ((string * Attrib.src list) * (string * string list) list) list ->
+ bool -> Proof.state -> Proof.state
+ val theorem: string -> string * Attrib.src list -> string * string list -> theory -> Proof.state
+ val theorem_i: string -> string * attribute list -> term * term list -> theory -> Proof.state
val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
val terminal_proof: Method.text * Method.text option ->
Toplevel.transition -> Toplevel.transition
--- a/src/Pure/Isar/local_defs.ML Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/local_defs.ML Sun May 07 00:22:05 2006 +0200
@@ -84,7 +84,7 @@
in
ctxt
|> ProofContext.add_fixes_i [(x, NONE, NoSyn)] |> snd
- |> ProofContext.add_assms_i def_export [(("", []), [(eq, ([], []))])]
+ |> ProofContext.add_assms_i def_export [(("", []), [(eq, [])])]
|>> (fn [(_, [th])] => (x', th))
end;
--- a/src/Pure/Isar/locale.ML Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/locale.ML Sun May 07 00:22:05 2006 +0200
@@ -56,13 +56,13 @@
(* Processing of locale statements *)
val read_context_statement: xstring option -> Element.context element list ->
- (string * (string list * string list)) list list -> Proof.context ->
+ (string * string list) list list -> Proof.context ->
string option * (cterm list * Proof.context) * (cterm list * Proof.context) *
- (term * (term list * term list)) list list
+ (term * term list) list list
val cert_context_statement: string option -> Element.context_i element list ->
- (term * (term list * term list)) list list -> Proof.context ->
+ (term * term list) list list -> Proof.context ->
string option * (cterm list * Proof.context) * (cterm list * Proof.context) *
- (term * (term list * term list)) list list
+ (term * term list) list list
(* Diagnostic functions *)
val print_locales: theory -> unit
@@ -864,7 +864,7 @@
ctxt |> ProofContext.add_assms_i LocalDefs.def_export
(defs' |> map (fn ((name, atts), (t, ps)) =>
let val ((c, _), t') = LocalDefs.cert_def ctxt t
- in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end))
+ in ((if name = "" then Thm.def_name c else name, atts), [(t', ps)]) end))
in ((ctxt', Assumed axs), []) end
| activate_elem _ ((ctxt, Derived ths), Defines defs) =
((ctxt, Derived ths), [])
@@ -947,7 +947,7 @@
let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
in (ctxt', []) end
| declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
- | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
+ | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs)
| declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
@@ -1024,7 +1024,7 @@
let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
in (ctxt', []) end
| declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
- | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
+ | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs)
| declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
@@ -1136,7 +1136,7 @@
in
(case elem of
Assumes asms => Assumes (asms |> map (fn (a, propps) =>
- (a, map (fn (t, (ps, qs)) => (close_frees t, (no_binds ps, no_binds qs))) propps)))
+ (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
| Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
(a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
| e => e)
@@ -1149,7 +1149,7 @@
| finish_ext_elem _ close (Assumes asms, propp) =
close (Assumes (map #1 asms ~~ propp))
| finish_ext_elem _ close (Defines defs, propp) =
- close (Defines (map #1 defs ~~ map (fn [(t, (ps, []))] => (t, ps)) propp))
+ close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
| finish_ext_elem _ _ (Notes facts, _) = Notes facts;
@@ -1667,7 +1667,7 @@
thy |> def_pred aname parms defs exts exts';
val elemss' =
change_elemss axioms elemss
- @ [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])];
+ @ [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
in
def_thy
|> PureThy.note_thmss_qualified "" aname [((introN, []), [([intro], [])])]
@@ -2145,7 +2145,7 @@
in (propss, activate) end;
fun prep_propp propss = propss |> map (fn ((name, _), props) =>
- (("", []), map (rpair ([], []) o Logic.protect) props));
+ (("", []), map (rpair [] o Logic.protect) props));
fun prep_result propps thmss =
ListPair.map (fn ((_, props), thms) => (props ~~ thms)) (propps, thmss);
--- a/src/Pure/Isar/obtain.ML Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/obtain.ML Sun May 07 00:22:05 2006 +0200
@@ -40,19 +40,18 @@
signature OBTAIN =
sig
val obtain: string -> (string * string option) list ->
- ((string * Attrib.src list) * (string * (string list * string list)) list) list
+ ((string * Attrib.src list) * (string * string list) list) list
-> bool -> Proof.state -> Proof.state
val obtain_i: string -> (string * typ option) list ->
- ((string * attribute list) * (term * (term list * term list)) list) list
+ ((string * attribute list) * (term * term list) list) list
-> bool -> Proof.state -> Proof.state
val guess: (string * string option) list -> bool -> Proof.state -> Proof.state
val guess_i: (string * typ option) list -> bool -> Proof.state -> Proof.state
val statement: (string * ((string * 'typ option) list * 'term list)) list ->
(('typ, 'term, 'fact) Element.ctxt list *
- ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list) *
- (((string * Attrib.src list) * (term * (term list * term list)) list) list -> Proof.context ->
- (((string * Attrib.src list) * (term * (term list * term list)) list) list * thm list) *
- Proof.context)
+ ((string * Attrib.src list) * ('term * 'term list) list) list) *
+ (((string * Attrib.src list) * (term * term list) list) list -> Proof.context ->
+ (((string * Attrib.src list) * (term * term list) list) list * thm list) * Proof.context)
end;
structure Obtain: OBTAIN =
@@ -151,13 +150,13 @@
in
state
|> Proof.enter_forward
- |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, ([], []))])] int
+ |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, [])])] int
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd
|> Proof.fix_i [(thesisN, NONE)]
- |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, ([], []))])]
+ |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
|> `Proof.the_facts
||> Proof.chain_facts chain_facts
- ||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false
+ ||> Proof.show_i NONE after_qed [(("", []), [(thesis, [])])] false
|-> Proof.refine_insert
end;
@@ -246,7 +245,7 @@
val ps = map dest_Free ts;
val asms =
Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
- |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), ([], [])));
+ |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), []));
val _ = conditional (null asms) (fn () => error "Trivial result -- nothing guessed");
in
Proof.fix_i (map (apsnd SOME) parms)
@@ -285,7 +284,7 @@
cases |> map_index (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name);
val elems = cases |> map (fn (_, (vars, _)) =>
Element.Constrains (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE)));
- val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair ([], [])) props));
+ val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair []) props));
fun mk_stmt stmt ctxt =
let
@@ -306,14 +305,14 @@
in
ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
ctxt' |> ProofContext.add_assms_i ProofContext.assume_export
- [((name, [ContextRules.intro_query NONE]), [(asm, ([], []))])]
+ [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
|>> (fn [(_, [th])] => th)
end;
val (ths, ctxt') = ctxt
|> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)])
|> fold_map assume_case (cases ~~ stmt)
|-> (fn ths => ProofContext.note_thmss_i [((thatN, []), [(ths, [])])] #> #2 #> pair ths);
- in (([(("", atts), [(thesis, ([], []))])], ths), ctxt') end;
+ in (([(("", atts), [(thesis, [])])], ths), ctxt') end;
in ((elems, concl), mk_stmt) end;
end;
--- a/src/Pure/Isar/outer_parse.ML Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/outer_parse.ML Sun May 07 00:22:05 2006 +0200
@@ -65,7 +65,7 @@
val simple_fixes: token list -> (string * string option) list * token list
val term: token list -> string * token list
val prop: token list -> string * token list
- val propp: token list -> (string * (string list * string list)) * token list
+ val propp: token list -> (string * string list) * token list
val termp: token list -> (string * string list) * token list
val arguments: token list -> Args.T list * token list
val attribs: token list -> Attrib.src list * token list
@@ -91,7 +91,7 @@
val locale_element: token list -> Element.context Locale.element * token list
val context_element: token list -> Element.context * token list
val statement: token list ->
- ((bstring * Attrib.src list) * (string * (string list * string list)) list) list * token list
+ ((bstring * Attrib.src list) * (string * string list) list) list * token list
val general_statement: token list ->
(Element.context Locale.element list * Element.statement) * OuterLex.token list
val statement_keyword: token list -> string * token list
@@ -281,11 +281,8 @@
val is_terms = Scan.repeat1 ($$$ "is" |-- term);
val is_props = Scan.repeat1 ($$$ "is" |-- prop);
-val concl_props = $$$ "concl" |-- !!! is_props;
-val any_props = concl_props >> pair [] || is_props -- Scan.optional concl_props [];
-val propp = prop -- Scan.optional ($$$ "(" |-- !!! (any_props --| $$$ ")")) ([], []);
-val propp' = prop -- Scan.optional ($$$ "(" |-- !!! (is_props --| $$$ ")")) [];
+val propp = prop -- Scan.optional ($$$ "(" |-- !!! (is_props --| $$$ ")")) [];
val termp = term -- Scan.optional ($$$ "(" |-- !!! (is_terms --| $$$ ")")) [];
@@ -363,7 +360,7 @@
>> Element.Constrains ||
$$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp))
>> Element.Assumes ||
- $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp'))
+ $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp))
>> Element.Defines ||
$$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1))
>> Element.Notes;
--- a/src/Pure/Isar/proof.ML Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/proof.ML Sun May 07 00:22:05 2006 +0200
@@ -47,23 +47,15 @@
val fix: (string * string option) list -> state -> state
val fix_i: (string * typ option) list -> state -> state
val assm: ProofContext.export ->
- ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
- state -> state
+ ((string * Attrib.src list) * (string * string list) list) list -> state -> state
val assm_i: ProofContext.export ->
- ((string * attribute list) * (term * (term list * term list)) list) list
- -> state -> state
- val assume: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
- state -> state
- val assume_i: ((string * attribute list) * (term * (term list * term list)) list) list
- -> state -> state
- val presume: ((string * Attrib.src list) * (string * (string list * string list)) list) list
- -> state -> state
- val presume_i: ((string * attribute list) * (term * (term list * term list)) list) list
- -> state -> state
- val def: ((string * Attrib.src list) * (string * (string * string list))) list ->
- state -> state
- val def_i: ((string * attribute list) * (string * (term * term list))) list ->
- state -> state
+ ((string * attribute list) * (term * term list) list) list -> state -> state
+ val assume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
+ val assume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
+ val presume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
+ val presume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
+ val def: ((string * Attrib.src list) * (string * (string * string list))) list -> state -> state
+ val def_i: ((string * attribute list) * (string * (term * term list))) list -> state -> state
val chain: state -> state
val chain_facts: thm list -> state -> state
val get_thmss: state -> (thmref * Attrib.src list) list -> thm list
@@ -114,25 +106,19 @@
val global_done_proof: state -> context * theory
val global_skip_proof: bool -> state -> context * theory
val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
- ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
- bool -> state -> state
+ ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
- ((string * attribute list) * (term * (term list * term list)) list) list ->
- bool -> state -> state
+ ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
- ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
- bool -> state -> state
+ ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
- ((string * attribute list) * (term * (term list * term list)) list) list ->
- bool -> state -> state
+ ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
string option -> string * Attrib.src list ->
- ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
- context -> state
+ ((string * Attrib.src list) * (string * string list) list) list -> context -> state
val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) ->
string option -> string * attribute list ->
- ((string * attribute list) * (term * (term list * term list)) list) list ->
- context -> state
+ ((string * attribute list) * (term * term list) list) list -> context -> state
end;
structure Proof: PROOF =
@@ -580,7 +566,7 @@
in
state'
|> fix (map (rpair NONE) xs)
- |> assm_i LocalDefs.def_export ((names ~~ atts) ~~ map (fn eq => [(eq, ([], []))]) eqs)
+ |> assm_i LocalDefs.def_export ((names ~~ atts) ~~ map (fn eq => [(eq, [])]) eqs)
end;
in
@@ -681,7 +667,7 @@
val atts = map (prep_att (theory_of state)) raw_atts;
val (asms, state') = state |> map_context_result (fn ctxt =>
ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs));
- val assumptions = asms |> map (fn (a, ts) => ((a, atts), map (rpair ([], [])) ts));
+ val assumptions = asms |> map (fn (a, ts) => ((a, atts), map (rpair []) ts));
in
state'
|> map_context (ProofContext.qualified_names #> ProofContext.no_base_names)
--- a/src/Pure/Isar/proof_context.ML Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/proof_context.ML Sun May 07 00:22:05 2006 +0200
@@ -88,21 +88,21 @@
val auto_bind_facts: term list -> context -> context
val match_bind: bool -> (string list * string) list -> context -> term list * context
val match_bind_i: bool -> (term list * term) list -> context -> term list * context
- val read_propp: context * (string * (string list * string list)) list list
- -> context * (term * (term list * term list)) list list
- val cert_propp: context * (term * (term list * term list)) list list
- -> context * (term * (term list * term list)) list list
- val read_propp_schematic: context * (string * (string list * string list)) list list
- -> context * (term * (term list * term list)) list list
- val cert_propp_schematic: context * (term * (term list * term list)) list list
- -> context * (term * (term list * term list)) list list
- val bind_propp: context * (string * (string list * string list)) list list
+ val read_propp: context * (string * string list) list list
+ -> context * (term * term list) list list
+ val cert_propp: context * (term * term list) list list
+ -> context * (term * term list) list list
+ val read_propp_schematic: context * (string * string list) list list
+ -> context * (term * term list) list list
+ val cert_propp_schematic: context * (term * term list) list list
+ -> context * (term * term list) list list
+ val bind_propp: context * (string * string list) list list
-> context * (term list list * (context -> context))
- val bind_propp_i: context * (term * (term list * term list)) list list
+ val bind_propp_i: context * (term * term list) list list
-> context * (term list list * (context -> context))
- val bind_propp_schematic: context * (string * (string list * string list)) list list
+ val bind_propp_schematic: context * (string * string list) list list
-> context * (term list list * (context -> context))
- val bind_propp_schematic_i: context * (term * (term list * term list)) list list
+ val bind_propp_schematic_i: context * (term * term list) list list
-> context * (term list list * (context -> context))
val fact_tac: thm list -> int -> tactic
val some_fact_tac: context -> int -> tactic
@@ -142,10 +142,10 @@
val auto_fixes: context * (term list list * 'a) -> context * (term list list * 'a)
val bind_fixes: string list -> context -> (term -> term) * context
val add_assms: export ->
- ((string * attribute list) * (string * (string list * string list)) list) list ->
+ ((string * attribute list) * (string * string list) list) list ->
context -> (bstring * thm list) list * context
val add_assms_i: export ->
- ((string * attribute list) * (term * (term list * term list)) list) list ->
+ ((string * attribute list) * (term * term list) list) list ->
context -> (bstring * thm list) list * context
val assume_export: export
val presume_export: export
@@ -833,11 +833,12 @@
(* simult_matches *)
-fun simult_matches ctxt [] = []
- | simult_matches ctxt pairs =
+fun simult_matches _ (_, []) = []
+ | simult_matches ctxt (t, pats) =
let
fun fail () = error "Pattern match failed!";
+ val pairs = map (rpair t) pats;
val maxidx = fold (fn (t1, t2) => fn i =>
Int.max (Int.max (Term.maxidx_of_term t1, Term.maxidx_of_term t2), i)) pairs ~1;
val envs = Unify.smash_unifiers (theory_of ctxt, Envir.empty maxidx,
@@ -885,8 +886,8 @@
fun prep_bind prep_pats (raw_pats, t) ctxt =
let
val ctxt' = declare_term t ctxt;
- val pats = prep_pats (fastype_of t) ctxt' raw_pats;
- val binds = simult_matches ctxt' (map (rpair t) pats);
+ val pats = prep_pats (Term.fastype_of t) ctxt' raw_pats;
+ val binds = simult_matches ctxt' (t, pats);
in (binds, ctxt') end;
fun gen_binds prep_terms prep_pats gen raw_binds ctxt =
@@ -919,23 +920,18 @@
fun prep_propp schematic prep_props prep_pats (context, args) =
let
- fun prep (_, (raw_pats1, raw_pats2)) (ctxt, prop :: props) =
- let
- val ctxt' = declare_term prop ctxt;
- val pats = prep_pats ctxt' (raw_pats1 @ raw_pats2); (*simultaneous type inference!*)
- in ((prop, chop (length raw_pats1) pats), (ctxt', props)) end
+ fun prep (_, raw_pats) (ctxt, prop :: props) =
+ let val ctxt' = declare_term prop ctxt
+ in ((prop, prep_pats ctxt' raw_pats), (ctxt', props)) end
| prep _ _ = sys_error "prep_propp";
val (propp, (context', _)) = (fold_map o fold_map) prep args
(context, prep_props schematic context (maps (map fst) args));
in (context', propp) end;
-fun matches ctxt (prop, (pats1, pats2)) =
- simult_matches ctxt (map (rpair prop) pats1 @ map (rpair (Logic.strip_imp_concl prop)) pats2);
-
fun gen_bind_propp prepp (ctxt, raw_args) =
let
val (ctxt', args) = prepp (ctxt, raw_args);
- val binds = flat (flat (map (map (matches ctxt')) args));
+ val binds = flat (flat (map (map (simult_matches ctxt')) args));
val propss = map (map #1) args;
(*generalize result: context evaluated now, binds added later*)
--- a/src/Pure/Isar/specification.ML Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/specification.ML Sun May 07 00:22:05 2006 +0200
@@ -46,7 +46,7 @@
val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
val ((specs, vs), specs_ctxt) =
- prep_propp (params_ctxt, map (map (rpair ([], [])) o snd) raw_specs)
+ prep_propp (params_ctxt, map (map (rpair []) o snd) raw_specs)
|> swap |>> map (map fst)
||>> fold_map ProofContext.inferred_param xs;
--- a/src/Pure/Tools/class_package.ML Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Tools/class_package.ML Sun May 07 00:22:05 2006 +0200
@@ -301,7 +301,7 @@
thy
|> ProofContext.init
|> Proof.theorem_i PureThy.internalK NONE (after_qed oo (fold o fold) add_thm) NONE ("", [])
- (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst));
+ (map (fn t => (("", []), [(t, [])])) (mk_prop thy inst));
in
--- a/src/Pure/axclass.ML Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/axclass.ML Sun May 07 00:22:05 2006 +0200
@@ -283,7 +283,7 @@
|> map_term_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
|> Logic.close_form;
- val axiomss = prep_propp (ctxt, map (map (rpair ([], [])) o snd) raw_specs)
+ val axiomss = prep_propp (ctxt, map (map (rpair []) o snd) raw_specs)
|> snd |> map (map (prep_axiom o fst));
val name_atts = Attrib.map_specs (prep_att thy) raw_specs |> map fst;