--- a/src/HOL/Boogie/Tools/boogie_commands.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Sun Apr 25 23:26:40 2010 +0200
@@ -99,7 +99,7 @@
|> (fn ctxt1 => ctxt1
|> prepare
|-> (fn us => fn ctxt2 => ctxt2
- |> Proof.theorem_i NONE (fn thmss => fn ctxt =>
+ |> Proof.theorem NONE (fn thmss => fn ctxt =>
let val export = map (finish ctxt1) o ProofContext.export ctxt ctxt2
in after_qed (map export thmss) ctxt end) [map (rpair []) us]))
end
@@ -188,7 +188,7 @@
fun prove thy meth vc =
ProofContext.init thy
- |> Proof.theorem_i NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
+ |> Proof.theorem NONE (K I) [[(Boogie_VCs.prop_of_vc vc, [])]]
|> Proof.apply meth
|> Seq.hd
|> Proof.global_done_proof
--- a/src/HOL/HOL.thy Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/HOL.thy Sun Apr 25 23:26:40 2010 +0200
@@ -1869,7 +1869,7 @@
proof
assume "PROP ?ofclass"
show "PROP ?eq"
- by (tactic {* ALLGOALS (rtac (Drule.unconstrainTs @{thm equals_eq})) *})
+ by (tactic {* ALLGOALS (rtac (Thm.unconstrain_allTs @{thm equals_eq})) *})
(fact `PROP ?ofclass`)
next
assume "PROP ?eq"
--- a/src/HOL/Nominal/nominal_inductive.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Nominal/nominal_inductive.ML Sun Apr 25 23:26:40 2010 +0200
@@ -543,7 +543,7 @@
in
ctxt'' |>
- Proof.theorem_i NONE (fn thss => fn ctxt =>
+ Proof.theorem NONE (fn thss => fn ctxt =>
let
val rec_name = space_implode "_" (map Long_Name.base_name names);
val rec_qualified = Binding.qualify false rec_name;
--- a/src/HOL/Nominal/nominal_inductive2.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Nominal/nominal_inductive2.ML Sun Apr 25 23:26:40 2010 +0200
@@ -445,7 +445,7 @@
in
ctxt'' |>
- Proof.theorem_i NONE (fn thss => fn ctxt =>
+ Proof.theorem NONE (fn thss => fn ctxt =>
let
val rec_name = space_implode "_" (map Long_Name.base_name names);
val rec_qualified = Binding.qualify false rec_name;
--- a/src/HOL/Nominal/nominal_primrec.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Nominal/nominal_primrec.ML Sun Apr 25 23:26:40 2010 +0200
@@ -363,7 +363,7 @@
in
lthy' |>
Variable.add_fixes (map fst lsrs) |> snd |>
- Proof.theorem_i NONE
+ Proof.theorem NONE
(fn thss => fn goal_ctxt =>
let
val simps = ProofContext.export goal_ctxt lthy' (flat thss);
--- a/src/HOL/Tools/Datatype/datatype_data.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Sun Apr 25 23:26:40 2010 +0200
@@ -436,7 +436,7 @@
in
thy
|> ProofContext.init
- |> Proof.theorem_i NONE after_qed' ((map o map) (rpair []) (flat rules))
+ |> Proof.theorem NONE after_qed' ((map o map) (rpair []) (flat rules))
end;
val rep_datatype = gen_rep_datatype Sign.cert_term;
--- a/src/HOL/Tools/Function/function.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Tools/Function/function.ML Sun Apr 25 23:26:40 2010 +0200
@@ -120,7 +120,7 @@
end
in
lthy
- |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
+ |> Proof.theorem NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
|> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
end
@@ -177,7 +177,7 @@
|> ProofContext.note_thmss ""
[((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
[([Goal.norm_result termination], [])])] |> snd
- |> Proof.theorem_i NONE afterqed [[(goal, [])]]
+ |> Proof.theorem NONE afterqed [[(goal, [])]]
end
val termination_proof = gen_termination_proof Syntax.check_term
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Apr 25 23:26:40 2010 +0200
@@ -3059,7 +3059,7 @@
) options [const]))
end
in
- Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
+ Proof.theorem NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
end;
val code_pred = generic_code_pred (K I);
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML Sun Apr 25 23:26:40 2010 +0200
@@ -45,7 +45,7 @@
val goals' = map (rpair []) goals
fun after_qed' thms = after_qed (the_single thms)
in
- Proof.theorem_i NONE after_qed' [goals'] ctxt
+ Proof.theorem NONE after_qed' [goals'] ctxt
end
--- a/src/HOL/Tools/choice_specification.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Tools/choice_specification.ML Sun Apr 25 23:26:40 2010 +0200
@@ -226,7 +226,7 @@
in
thy
|> ProofContext.init
- |> Proof.theorem_i NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
+ |> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
end;
--- a/src/HOL/Tools/typedef.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOL/Tools/typedef.ML Sun Apr 25 23:26:40 2010 +0200
@@ -282,7 +282,7 @@
val ((goal, goal_pat, typedef_result), lthy') =
prepare_typedef prep_term def name (b, args, mx) set opt_morphs lthy;
fun after_qed [[th]] = snd o typedef_result th;
- in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] lthy' end;
+ in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
in
--- a/src/HOLCF/Tools/pcpodef.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/HOLCF/Tools/pcpodef.ML Sun Apr 25 23:26:40 2010 +0200
@@ -328,7 +328,7 @@
prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
| after_qed _ = raise Fail "cpodef_proof";
- in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
+ in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
fun gen_pcpodef_proof prep_term prep_constraint
((def, name), (b, raw_args, mx), set, opt_morphs) thy =
@@ -339,7 +339,7 @@
prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
| after_qed _ = raise Fail "pcpodef_proof";
- in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
+ in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
in
--- a/src/Pure/Isar/calculation.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Isar/calculation.ML Sun Apr 25 23:26:40 2010 +0200
@@ -13,11 +13,11 @@
val sym_add: attribute
val sym_del: attribute
val symmetric: attribute
- val also: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
- val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
- val finally: (Facts.ref * Attrib.src list) list option -> bool ->
+ val also: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
+ val also_cmd: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
+ val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
+ val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool ->
Proof.state -> Proof.state Seq.seq
- val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
val moreover: bool -> Proof.state -> Proof.state
val ultimately: bool -> Proof.state -> Proof.state
end;
@@ -148,10 +148,10 @@
state |> maintain_calculation final calc))
end;
-val also = calculate Proof.get_thmss false;
-val also_i = calculate (K I) false;
-val finally = calculate Proof.get_thmss true;
-val finally_i = calculate (K I) true;
+val also = calculate (K I) false;
+val also_cmd = calculate Proof.get_thmss_cmd false;
+val finally = calculate (K I) true;
+val finally_cmd = calculate Proof.get_thmss_cmd true;
(* moreover and ultimately *)
--- a/src/Pure/Isar/class_target.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Isar/class_target.ML Sun Apr 25 23:26:40 2010 +0200
@@ -163,7 +163,7 @@
Symtab.empty
|> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
Symtab.map_default (class, []) (insert (op =) tyco)) arities)
- ((#arities o Sorts.rep_algebra) algebra);
+ (Sorts.arities_of algebra);
val the_arities = these o Symtab.lookup arities;
fun mk_arity class tyco =
let
@@ -370,7 +370,7 @@
in
thy
|> ProofContext.init
- |> Proof.theorem_i NONE after_qed [[(mk_prop thy classrel, [])]]
+ |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]]
end;
in
@@ -539,7 +539,7 @@
end;
val instantiation_instance = gen_instantiation_instance (fn after_qed => fn ts =>
- Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
+ Proof.theorem NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
fun prove_instantiation_instance tac = gen_instantiation_instance (fn after_qed =>
fn ts => fn lthy => after_qed (map (fn t => Goal.prove lthy [] [] t
@@ -595,7 +595,7 @@
in
thy
|> ProofContext.init
- |> Proof.theorem_i NONE after_qed (map (fn t => [(t, [])]) arities)
+ |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities)
end;
--- a/src/Pure/Isar/element.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Isar/element.ML Sun Apr 25 23:26:40 2010 +0200
@@ -283,10 +283,10 @@
in
fun witness_proof after_qed wit_propss =
- gen_witness_proof (Proof.theorem_i NONE) (fn wits => fn _ => after_qed wits)
+ gen_witness_proof (Proof.theorem NONE) (fn wits => fn _ => after_qed wits)
wit_propss [];
-val witness_proof_eqs = gen_witness_proof (Proof.theorem_i NONE);
+val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE);
fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
gen_witness_proof (fn after_qed' => fn propss =>
--- a/src/Pure/Isar/isar_cmd.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Isar/isar_cmd.ML Sun Apr 25 23:26:40 2010 +0200
@@ -219,10 +219,10 @@
fun goal opt_chain goal stmt int =
opt_chain #> goal NONE (K I) stmt int;
-val have = goal I Proof.have;
-val hence = goal Proof.chain Proof.have;
-val show = goal I Proof.show;
-val thus = goal Proof.chain Proof.show;
+val have = goal I Proof.have_cmd;
+val hence = goal Proof.chain Proof.have_cmd;
+val show = goal I Proof.show_cmd;
+val thus = goal Proof.chain Proof.show_cmd;
(* local endings *)
@@ -393,7 +393,7 @@
let
val thy = Toplevel.theory_of state;
val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy);
- val {classes, ...} = Sorts.rep_algebra algebra;
+ val classes = Sorts.classes_of algebra;
fun entry (c, (i, (_, cs))) =
(i, {name = Name_Space.extern space c, ID = c, parents = cs,
dir = "", unfold = true, path = ""});
@@ -403,7 +403,7 @@
in Present.display_graph gr end);
fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
- Thm_Deps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
+ Thm_Deps.thm_deps (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args));
(* find unused theorems *)
@@ -437,12 +437,12 @@
local
fun string_of_stmts state args =
- Proof.get_thmss state args
+ Proof.get_thmss_cmd state args
|> map (Element.pretty_statement (Proof.context_of state) Thm.theoremK)
|> Pretty.chunks2 |> Pretty.string_of;
fun string_of_thms state args =
- Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss state args));
+ Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss_cmd state args));
fun string_of_prfs full state arg =
Pretty.string_of
@@ -460,7 +460,7 @@
end
| SOME args => Pretty.chunks
(map (Proof_Syntax.pretty_proof_of (Proof.context_of state) full)
- (Proof.get_thmss state args)));
+ (Proof.get_thmss_cmd state args)));
fun string_of_prop state s =
let
--- a/src/Pure/Isar/isar_syn.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Isar/isar_syn.ML Sun Apr 25 23:26:40 2010 +0200
@@ -542,27 +542,27 @@
val _ =
OuterSyntax.command "from" "forward chaining from given facts"
(K.tag_proof K.prf_chain)
- (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss)));
+ (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
val _ =
OuterSyntax.command "with" "forward chaining from given and current facts"
(K.tag_proof K.prf_chain)
- (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss)));
+ (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
val _ =
OuterSyntax.command "note" "define facts"
(K.tag_proof K.prf_decl)
- (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss)));
+ (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
val _ =
OuterSyntax.command "using" "augment goal facts"
(K.tag_proof K.prf_decl)
- (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using)));
+ (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
val _ =
OuterSyntax.command "unfolding" "unfold definitions in goal and facts"
(K.tag_proof K.prf_decl)
- (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding)));
+ (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
(* proof context *)
@@ -570,17 +570,17 @@
val _ =
OuterSyntax.command "fix" "fix local variables (Skolem constants)"
(K.tag_proof K.prf_asm)
- (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
+ (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
val _ =
OuterSyntax.command "assume" "assume propositions"
(K.tag_proof K.prf_asm)
- (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume)));
+ (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
val _ =
OuterSyntax.command "presume" "assume propositions, to be established later"
(K.tag_proof K.prf_asm)
- (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume)));
+ (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
val _ =
OuterSyntax.command "def" "local definition"
@@ -588,24 +588,24 @@
(P.and_list1
(SpecParse.opt_thm_name ":" --
((P.binding -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
- >> (Toplevel.print oo (Toplevel.proof o Proof.def)));
+ >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
val _ =
OuterSyntax.command "obtain" "generalized existence"
(K.tag_proof K.prf_asm_goal)
(P.parname -- Scan.optional (P.fixes --| P.where_) [] -- SpecParse.statement
- >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z)));
+ >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
val _ =
OuterSyntax.command "guess" "wild guessing (unstructured)"
(K.tag_proof K.prf_asm_goal)
- (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
+ (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
val _ =
OuterSyntax.command "let" "bind text variables"
(K.tag_proof K.prf_decl)
(P.and_list1 (P.and_list1 P.term -- (P.$$$ "=" |-- P.term))
- >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind)));
+ >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
val case_spec =
(P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
@@ -614,7 +614,7 @@
val _ =
OuterSyntax.command "case" "invoke local context"
(K.tag_proof K.prf_asm)
- (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case)));
+ (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));
(* proof structure *)
@@ -711,12 +711,12 @@
val _ =
OuterSyntax.command "also" "combine calculation and current facts"
(K.tag_proof K.prf_decl)
- (calc_args >> (Toplevel.proofs' o Calculation.also));
+ (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
val _ =
OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
(K.tag_proof K.prf_chain)
- (calc_args >> (Toplevel.proofs' o Calculation.finally));
+ (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
val _ =
OuterSyntax.command "moreover" "augment calculation by current facts"
--- a/src/Pure/Isar/obtain.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Isar/obtain.ML Sun Apr 25 23:26:40 2010 +0200
@@ -39,14 +39,14 @@
signature OBTAIN =
sig
val thatN: string
- val obtain: string -> (binding * string option * mixfix) list ->
+ val obtain: string -> (binding * typ option * mixfix) list ->
+ (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
+ val obtain_cmd: string -> (binding * string option * mixfix) list ->
(Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
- val obtain_i: string -> (binding * typ option * mixfix) list ->
- (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
((string * cterm) list * thm list) * Proof.context
- val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
- val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
+ val guess: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
+ val guess_cmd: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
end;
structure Obtain: OBTAIN =
@@ -148,26 +148,26 @@
fun after_qed _ =
Proof.local_qed (NONE, false)
#> `Proof.the_fact #-> (fn rule =>
- Proof.fix_i vars
- #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
+ Proof.fix vars
+ #> Proof.assm (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
in
state
|> Proof.enter_forward
- |> Proof.have_i NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
+ |> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd
- |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
- |> Proof.assume_i
+ |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
+ |> Proof.assume
[((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
|> `Proof.the_facts
||> Proof.chain_facts chain_facts
- ||> Proof.show_i NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
+ ||> Proof.show NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
|-> Proof.refine_insert
end;
in
-val obtain = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
-val obtain_i = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
+val obtain = gen_obtain (K I) ProofContext.cert_vars ProofContext.cert_propp;
+val obtain_cmd = gen_obtain Attrib.attribute ProofContext.read_vars ProofContext.read_propp;
end;
@@ -290,8 +290,8 @@
in
state'
|> Proof.map_context (K ctxt')
- |> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
- |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
+ |> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
+ |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm
(obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
|> Proof.bind_terms Auto_Bind.no_facts
end;
@@ -307,7 +307,7 @@
state
|> Proof.enter_forward
|> Proof.begin_block
- |> Proof.fix_i [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
+ |> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
|> Proof.chain_facts chain_facts
|> Proof.local_goal print_result (K I) (apsnd (rpair I))
"guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
@@ -316,8 +316,8 @@
in
-val guess = gen_guess ProofContext.read_vars;
-val guess_i = gen_guess ProofContext.cert_vars;
+val guess = gen_guess ProofContext.cert_vars;
+val guess_cmd = gen_guess ProofContext.read_vars;
end;
--- a/src/Pure/Isar/proof.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Isar/proof.ML Sun Apr 25 23:26:40 2010 +0200
@@ -41,37 +41,35 @@
val raw_goal: state -> {context: context, facts: thm list, goal: thm}
val goal: state -> {context: context, facts: thm list, goal: thm}
val simple_goal: state -> {context: context, goal: thm}
- val match_bind: (string list * string) list -> state -> state
- val match_bind_i: (term list * term) list -> state -> state
- val let_bind: (string list * string) list -> state -> state
- val let_bind_i: (term list * term) list -> state -> state
- val fix: (binding * string option * mixfix) list -> state -> state
- val fix_i: (binding * typ option * mixfix) list -> state -> state
+ val let_bind: (term list * term) list -> state -> state
+ val let_bind_cmd: (string list * string) list -> state -> state
+ val fix: (binding * typ option * mixfix) list -> state -> state
+ val fix_cmd: (binding * string option * mixfix) list -> state -> state
val assm: Assumption.export ->
+ (Thm.binding * (term * term list) list) list -> state -> state
+ val assm_cmd: Assumption.export ->
(Attrib.binding * (string * string list) list) list -> state -> state
- val assm_i: Assumption.export ->
- (Thm.binding * (term * term list) list) list -> state -> state
- val assume: (Attrib.binding * (string * string list) list) list -> state -> state
- val assume_i: (Thm.binding * (term * term list) list) list -> state -> state
- val presume: (Attrib.binding * (string * string list) list) list -> state -> state
- val presume_i: (Thm.binding * (term * term list) list) list -> state -> state
- val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
- val def_i: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
+ val assume: (Thm.binding * (term * term list) list) list -> state -> state
+ val assume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
+ val presume: (Thm.binding * (term * term list) list) list -> state -> state
+ val presume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
+ val def: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
+ val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
val chain: state -> state
val chain_facts: thm list -> state -> state
- val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
- val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
- val note_thmss_i: (Thm.binding * (thm list * attribute list) list) list -> state -> state
- val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
- val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
- val with_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
- val with_thmss_i: ((thm list * attribute list) list) list -> state -> state
- val using: ((Facts.ref * Attrib.src list) list) list -> state -> state
- val using_i: ((thm list * attribute list) list) list -> state -> state
- val unfolding: ((Facts.ref * Attrib.src list) list) list -> state -> state
- val unfolding_i: ((thm list * attribute list) list) list -> state -> state
- val invoke_case: string * string option list * Attrib.src list -> state -> state
- val invoke_case_i: string * string option list * attribute list -> state -> state
+ val get_thmss_cmd: state -> (Facts.ref * Attrib.src list) list -> thm list
+ val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
+ val note_thmss_cmd: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
+ val from_thmss: ((thm list * attribute list) list) list -> state -> state
+ val from_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+ val with_thmss: ((thm list * attribute list) list) list -> state -> state
+ val with_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+ val using: ((thm list * attribute list) list) list -> state -> state
+ val using_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+ val unfolding: ((thm list * attribute list) list) list -> state -> state
+ val unfolding_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
+ val invoke_case: string * string option list * attribute list -> state -> state
+ val invoke_case_cmd: string * string option list * Attrib.src list -> state -> state
val begin_block: state -> state
val next_block: state -> state
val end_block: state -> state
@@ -87,9 +85,9 @@
((binding * 'a list) * 'b) list -> state -> state
val local_qed: Method.text option * bool -> state -> state
val theorem: Method.text option -> (thm list list -> context -> context) ->
+ (term * term list) list list -> context -> state
+ val theorem_cmd: Method.text option -> (thm list list -> context -> context) ->
(string * string list) list list -> context -> state
- val theorem_i: Method.text option -> (thm list list -> context -> context) ->
- (term * term list) list list -> context -> state
val global_qed: Method.text option * bool -> state -> context
val local_terminal_proof: Method.text * Method.text option -> state -> state
val local_default_proof: state -> state
@@ -102,13 +100,13 @@
val global_skip_proof: bool -> state -> context
val global_done_proof: state -> context
val have: Method.text option -> (thm list list -> state -> state) ->
+ (Thm.binding * (term * term list) list) list -> bool -> state -> state
+ val have_cmd: Method.text option -> (thm list list -> state -> state) ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
- val have_i: Method.text option -> (thm list list -> state -> state) ->
- (Thm.binding * (term * term list) list) list -> bool -> state -> state
val show: Method.text option -> (thm list list -> state -> state) ->
+ (Thm.binding * (term * term list) list) list -> bool -> state -> state
+ val show_cmd: Method.text option -> (thm list list -> state -> state) ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
- val show_i: Method.text option -> (thm list list -> state -> state) ->
- (Thm.binding * (term * term list) list) list -> bool -> state -> state
val schematic_goal: state -> bool
val is_relevant: state -> bool
val local_future_proof: (state -> ('a * state) Future.future) ->
@@ -523,22 +521,20 @@
(** context elements **)
-(* bindings *)
+(* let bindings *)
local
fun gen_bind bind args state =
state
|> assert_forward
- |> map_context (bind args #> snd)
+ |> map_context (bind true args #> snd)
|> put_facts NONE;
in
-val match_bind = gen_bind (ProofContext.match_bind false);
-val match_bind_i = gen_bind (ProofContext.match_bind_i false);
-val let_bind = gen_bind (ProofContext.match_bind true);
-val let_bind_i = gen_bind (ProofContext.match_bind_i true);
+val let_bind = gen_bind ProofContext.match_bind_i;
+val let_bind_cmd = gen_bind ProofContext.match_bind;
end;
@@ -554,8 +550,8 @@
in
-val fix = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
-val fix_i = gen_fix (K I);
+val fix = gen_fix (K I);
+val fix_cmd = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
end;
@@ -572,12 +568,12 @@
in
-val assm = gen_assume ProofContext.add_assms Attrib.attribute;
-val assm_i = gen_assume ProofContext.add_assms_i (K I);
-val assume = assm Assumption.assume_export;
-val assume_i = assm_i Assumption.assume_export;
-val presume = assm Assumption.presume_export;
-val presume_i = assm_i Assumption.presume_export;
+val assm = gen_assume ProofContext.add_assms_i (K I);
+val assm_cmd = gen_assume ProofContext.add_assms Attrib.attribute;
+val assume = assm Assumption.assume_export;
+val assume_cmd = assm_cmd Assumption.assume_export;
+val presume = assm Assumption.presume_export;
+val presume_cmd = assm_cmd Assumption.presume_export;
end;
@@ -605,8 +601,8 @@
in
-val def = gen_def Attrib.attribute ProofContext.read_vars ProofContext.match_bind;
-val def_i = gen_def (K I) ProofContext.cert_vars ProofContext.match_bind_i;
+val def = gen_def (K I) ProofContext.cert_vars ProofContext.match_bind_i;
+val def_cmd = gen_def Attrib.attribute ProofContext.read_vars ProofContext.match_bind;
end;
@@ -646,18 +642,18 @@
in
-val note_thmss = gen_thmss (K []) I #2 Attrib.attribute ProofContext.get_fact;
-val note_thmss_i = gen_thmss (K []) I #2 (K I) (K I);
+val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
+val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute ProofContext.get_fact;
-val from_thmss = gen_thmss (K []) chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
-val from_thmss_i = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
+val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
+val from_thmss_cmd = gen_thmss (K []) chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
-val with_thmss = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
-val with_thmss_i = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
+val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
+val with_thmss_cmd = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
-fun get_thmss state srcs = the_facts (note_thmss [((Binding.empty, []), srcs)] state);
+fun get_thmss_cmd state srcs = the_facts (note_thmss_cmd [((Binding.empty, []), srcs)] state);
end;
@@ -686,10 +682,10 @@
in
-val using = gen_using append_using (K (K I)) Attrib.attribute ProofContext.get_fact;
-val using_i = gen_using append_using (K (K I)) (K I) (K I);
-val unfolding = gen_using unfold_using unfold_goals Attrib.attribute ProofContext.get_fact;
-val unfolding_i = gen_using unfold_using unfold_goals (K I) (K I);
+val using = gen_using append_using (K (K I)) (K I) (K I);
+val using_cmd = gen_using append_using (K (K I)) Attrib.attribute ProofContext.get_fact;
+val unfolding = gen_using unfold_using unfold_goals (K I) (K I);
+val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute ProofContext.get_fact;
end;
@@ -709,15 +705,15 @@
val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
in
state'
- |> assume_i assumptions
+ |> assume assumptions
|> bind_terms Auto_Bind.no_facts
- |> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
+ |> `the_facts |-> (fn thms => note_thmss [((Binding.name name, []), [(thms, [])])])
end;
in
-val invoke_case = gen_invoke_case Attrib.attribute;
-val invoke_case_i = gen_invoke_case (K I);
+val invoke_case = gen_invoke_case (K I);
+val invoke_case_cmd = gen_invoke_case Attrib.attribute;
end;
@@ -790,15 +786,16 @@
local
-fun implicit_vars dest add props =
+val is_var =
+ can (dest_TVar o Logic.dest_type o Logic.dest_term) orf
+ can (dest_Var o Logic.dest_term);
+
+fun implicit_vars props =
let
- val (explicit_vars, props') = take_prefix (can dest) props |>> map dest;
- val vars = rev (subtract (op =) explicit_vars (fold add props []));
- val _ =
- if null vars then ()
- else warning ("Goal statement contains unbound schematic variable(s): " ^
- commas_quote (map (Term.string_of_vname o fst) vars));
- in (rev vars, props') end;
+ val (var_props, props') = take_prefix is_var props;
+ val explicit_vars = fold Term.add_vars var_props [];
+ val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []);
+ in map (Logic.mk_term o Var) vars end;
fun refine_terms n =
refine (Method.Basic (K (RAW_METHOD
@@ -823,11 +820,8 @@
|> map_context_result (fn ctxt => swap (prepp (ctxt, raw_propp)));
val props = flat propss;
- val (_, props') =
- implicit_vars (dest_TVar o Logic.dest_type o Logic.dest_term) Term.add_tvars props;
- val (vars, _) = implicit_vars (dest_Var o Logic.dest_term) Term.add_vars props';
-
- val propss' = map (Logic.mk_term o Var) vars :: propss;
+ val vars = implicit_vars props;
+ val propss' = vars :: propss;
val goal_propss = filter_out null propss';
val goal =
cert (Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss))
@@ -903,8 +897,8 @@
init ctxt
|> generic_goal (prepp #> ProofContext.auto_fixes) "" before_qed (K I, after_qed) propp;
-val theorem = global_goal ProofContext.bind_propp_schematic;
-val theorem_i = global_goal ProofContext.bind_propp_schematic_i;
+val theorem = global_goal ProofContext.bind_propp_schematic_i;
+val theorem_cmd = global_goal ProofContext.bind_propp_schematic;
fun global_qeds txt =
end_proof true txt
@@ -976,10 +970,10 @@
in
-val have = gen_have Attrib.attribute ProofContext.bind_propp;
-val have_i = gen_have (K I) ProofContext.bind_propp_i;
-val show = gen_show Attrib.attribute ProofContext.bind_propp;
-val show_i = gen_show (K I) ProofContext.bind_propp_i;
+val have = gen_have (K I) ProofContext.bind_propp_i;
+val have_cmd = gen_have Attrib.attribute ProofContext.bind_propp;
+val show = gen_show (K I) ProofContext.bind_propp_i;
+val show_cmd = gen_show Attrib.attribute ProofContext.bind_propp;
end;
--- a/src/Pure/Isar/specification.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Isar/specification.ML Sun Apr 25 23:26:40 2010 +0200
@@ -403,7 +403,7 @@
goal_ctxt
|> ProofContext.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
|> snd
- |> Proof.theorem_i before_qed after_qed' (map snd stmt)
+ |> Proof.theorem before_qed after_qed' (map snd stmt)
|> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
|> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
error "Illegal schematic goal statement")
--- a/src/Pure/ML/ml_thms.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/ML/ml_thms.ML Sun Apr 25 23:26:40 2010 +0200
@@ -64,7 +64,7 @@
fun after_qed res goal_ctxt =
put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt (flat res))) goal_ctxt;
val ctxt' = ctxt
- |> Proof.theorem_i NONE after_qed propss
+ |> Proof.theorem NONE after_qed propss
|> Proof.global_terminal_proof methods;
val (a, background') = background
|> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
--- a/src/Pure/Thy/thy_output.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/Thy/thy_output.ML Sun Apr 25 23:26:40 2010 +0200
@@ -574,7 +574,7 @@
val prop_src =
(case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
val _ = context
- |> Proof.theorem_i NONE (K I) [[(prop, [])]]
+ |> Proof.theorem NONE (K I) [[(prop, [])]]
|> Proof.global_terminal_proof methods;
in output (maybe_pretty_source (pretty_term context) prop_src [prop]) end);
--- a/src/Pure/axclass.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/axclass.ML Sun Apr 25 23:26:40 2010 +0200
@@ -13,8 +13,8 @@
val add_arity: thm -> theory -> theory
val prove_classrel: class * class -> tactic -> theory -> theory
val prove_arity: string * sort list * sort -> tactic -> theory -> theory
- val get_info: theory -> class ->
- {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
+ type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
+ val get_info: theory -> class -> info
val class_intros: theory -> thm list
val class_of_param: theory -> string -> class option
val cert_classrel: theory -> class * class -> class * class
@@ -37,8 +37,6 @@
val param_of_inst: theory -> string * string -> string
val inst_of_param: theory -> string -> (string * string) option
val thynames_of_arity: theory -> class * string -> string list
- val introN: string
- val axiomsN: string
end;
structure AxClass: AX_CLASS =
@@ -46,6 +44,18 @@
(** theory data **)
+(* axclass info *)
+
+type info =
+ {def: thm,
+ intro: thm,
+ axioms: thm list,
+ params: (string * typ) list};
+
+fun make_axclass (def, intro, axioms, params): info =
+ {def = def, intro = intro, axioms = axioms, params = params};
+
+
(* class parameters (canonical order) *)
type param = string * class;
@@ -57,188 +67,265 @@
" for " ^ Pretty.string_of_sort pp [c] ^
(if c = c' then "" else " and " ^ Pretty.string_of_sort pp [c'])));
-fun merge_params _ ([], qs) = qs
- | merge_params pp (ps, qs) =
- fold_rev (fn q => if member (op =) ps q then I else add_param pp q) qs ps;
+
+(* setup data *)
+
+datatype data = Data of
+ {axclasses: info Symtab.table,
+ params: param list,
+ proven_classrels: (thm * proof) Symreltab.table,
+ proven_arities: ((class * sort list) * ((thm * string) * proof)) list Symtab.table,
+ (*arity theorems with theory name*)
+ inst_params:
+ (string * thm) Symtab.table Symtab.table *
+ (*constant name ~> type constructor ~> (constant name, equation)*)
+ (string * string) Symtab.table (*constant name ~> (constant name, type constructor)*),
+ diff_merge_classrels: (class * class) list};
+
+fun make_data
+ (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =
+ Data {axclasses = axclasses, params = params, proven_classrels = proven_classrels,
+ proven_arities = proven_arities, inst_params = inst_params,
+ diff_merge_classrels = diff_merge_classrels};
+
+structure Data = Theory_Data_PP
+(
+ type T = data;
+ val empty =
+ make_data (Symtab.empty, [], Symreltab.empty, Symtab.empty, (Symtab.empty, Symtab.empty), []);
+ val extend = I;
+ fun merge pp
+ (Data {axclasses = axclasses1, params = params1, proven_classrels = proven_classrels1,
+ proven_arities = proven_arities1, inst_params = inst_params1,
+ diff_merge_classrels = diff_merge_classrels1},
+ Data {axclasses = axclasses2, params = params2, proven_classrels = proven_classrels2,
+ proven_arities = proven_arities2, inst_params = inst_params2,
+ diff_merge_classrels = diff_merge_classrels2}) =
+ let
+ val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
+ val params' =
+ if null params1 then params2
+ else fold_rev (fn q => if member (op =) params1 q then I else add_param pp q) params2 params1;
+
+ (*transitive closure of classrels and arity completion is done in Theory.at_begin hook*)
+ val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2);
+ val proven_arities' =
+ Symtab.join (K (Library.merge (eq_fst op =))) (proven_arities1, proven_arities2);
+
+ val classrels1 = Symreltab.keys proven_classrels1;
+ val classrels2 = Symreltab.keys proven_classrels2;
+ val diff_merge_classrels' =
+ subtract (op =) classrels1 classrels2 @
+ subtract (op =) classrels2 classrels1 @
+ diff_merge_classrels1 @ diff_merge_classrels2;
+
+ val inst_params' =
+ (Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2),
+ Symtab.merge (K true) (#2 inst_params1, #2 inst_params2));
+ in
+ make_data (axclasses', params', proven_classrels', proven_arities', inst_params',
+ diff_merge_classrels')
+ end;
+);
+
+fun map_data f =
+ Data.map (fn Data {axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels} =>
+ make_data (f (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels)));
+
+fun map_axclasses f =
+ map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
+ (f axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels));
+
+fun map_params f =
+ map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
+ (axclasses, f params, proven_classrels, proven_arities, inst_params, diff_merge_classrels));
+
+fun map_proven_classrels f =
+ map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
+ (axclasses, params, f proven_classrels, proven_arities, inst_params, diff_merge_classrels));
+
+fun map_proven_arities f =
+ map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
+ (axclasses, params, proven_classrels, f proven_arities, inst_params, diff_merge_classrels));
+
+fun map_inst_params f =
+ map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
+ (axclasses, params, proven_classrels, proven_arities, f inst_params, diff_merge_classrels));
+
+val clear_diff_merge_classrels =
+ map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, _) =>
+ (axclasses, params, proven_classrels, proven_arities, inst_params, []));
+
+val rep_data = Data.get #> (fn Data args => args);
+
+val axclasses_of = #axclasses o rep_data;
+val params_of = #params o rep_data;
+val proven_classrels_of = #proven_classrels o rep_data;
+val proven_arities_of = #proven_arities o rep_data;
+val inst_params_of = #inst_params o rep_data;
+val diff_merge_classrels_of = #diff_merge_classrels o rep_data;
-(* axclasses *)
-
-val introN = "intro";
-val superN = "super";
-val axiomsN = "axioms";
+(* maintain axclasses *)
-datatype axclass = AxClass of
- {def: thm,
- intro: thm,
- axioms: thm list,
- params: (string * typ) list};
+fun get_info thy c =
+ (case Symtab.lookup (axclasses_of thy) c of
+ SOME info => info
+ | NONE => error ("No such axclass: " ^ quote c));
-type axclasses = axclass Symtab.table * param list;
-
-fun make_axclass ((def, intro, axioms), params) = AxClass
- {def = def, intro = intro, axioms = axioms, params = params};
-
-fun merge_axclasses pp ((tab1, params1), (tab2, params2)) : axclasses =
- (Symtab.merge (K true) (tab1, tab2), merge_params pp (params1, params2));
+fun class_intros thy =
+ let
+ fun add_intro c = (case try (get_info thy) c of SOME {intro, ...} => cons intro | _ => I);
+ val classes = Sign.all_classes thy;
+ in map (Thm.class_triv thy) classes @ fold add_intro classes [] end;
-(* instances *)
+(* maintain params *)
+
+fun all_params_of thy S =
+ let val params = params_of thy;
+ in fold (fn (x, c) => if Sign.subsort thy (S, [c]) then cons x else I) params [] end;
+
+fun class_of_param thy = AList.lookup (op =) (params_of thy);
+
+
+(* maintain instances *)
val classrel_prefix = "classrel_";
val arity_prefix = "arity_";
-type instances =
- ((class * class) * thm) list * (*classrel theorems*)
- ((class * sort list) * (thm * string)) list Symtab.table; (*arity theorems with theory name*)
-
-fun merge_instances ((classrel1, arities1): instances, (classrel2, arities2)) =
- (merge (eq_fst op =) (classrel1, classrel2),
- Symtab.join (K (merge (eq_fst op =))) (arities1, arities2));
-
-
-(* instance parameters *)
-
-type inst_params =
- (string * thm) Symtab.table Symtab.table
- (*constant name ~> type constructor ~> (constant name, equation)*)
- * (string * string) Symtab.table; (*constant name ~> (constant name, type constructor)*)
-
-fun merge_inst_params ((const_param1, param_const1), (const_param2, param_const2)) =
- (Symtab.join (K (Symtab.merge (K true))) (const_param1, const_param2),
- Symtab.merge (K true) (param_const1, param_const2));
-
-
-(* setup data *)
-
-structure AxClassData = Theory_Data_PP
-(
- type T = axclasses * (instances * inst_params);
- val empty = ((Symtab.empty, []), (([], Symtab.empty), (Symtab.empty, Symtab.empty)));
- val extend = I;
- fun merge pp ((axclasses1, (instances1, inst_params1)), (axclasses2, (instances2, inst_params2))) =
- (merge_axclasses pp (axclasses1, axclasses2),
- (merge_instances (instances1, instances2), merge_inst_params (inst_params1, inst_params2)));
-);
-
-
-(* maintain axclasses *)
-
-val get_axclasses = #1 o AxClassData.get;
-val map_axclasses = AxClassData.map o apfst;
-
-val lookup_def = Symtab.lookup o #1 o get_axclasses;
-
-fun get_info thy c =
- (case lookup_def thy c of
- SOME (AxClass info) => info
- | NONE => error ("No such axclass: " ^ quote c));
-
-fun class_intros thy =
- let
- fun add_intro c =
- (case lookup_def thy c of SOME (AxClass {intro, ...}) => cons intro | _ => I);
- val classes = Sign.all_classes thy;
- in map (Thm.class_triv thy) classes @ fold add_intro classes [] end;
-
-
-fun get_params thy pred =
- let val params = #2 (get_axclasses thy);
- in fold (fn (x, c) => if pred c then cons x else I) params [] end;
-
-fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c]));
-
-fun class_of_param thy = AList.lookup (op =) (#2 (get_axclasses thy));
-
-
-(* maintain instances *)
-
fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a;
-val get_instances = #1 o #2 o AxClassData.get;
-val map_instances = AxClassData.map o apsnd o apfst;
-
fun the_classrel thy (c1, c2) =
- (case AList.lookup (op =) (#1 (get_instances thy)) (c1, c2) of
- SOME th => Thm.transfer thy th
+ (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
+ SOME classrel => classrel
| NONE => error ("Unproven class relation " ^
Syntax.string_of_classrel (ProofContext.init thy) [c1, c2]));
-fun put_classrel arg = map_instances (fn (classrel, arities) =>
- (insert (eq_fst op =) arg classrel, arities));
+fun the_classrel_thm thy = Thm.transfer thy o #1 o the_classrel thy;
+fun the_classrel_prf thy = #2 o the_classrel thy;
+
+fun put_trancl_classrel ((c1, c2), th) thy =
+ let
+ val cert = Thm.cterm_of thy;
+ val certT = Thm.ctyp_of thy;
+
+ val classes = Sorts.classes_of (Sign.classes_of thy);
+ val classrels = proven_classrels_of thy;
+
+ fun reflcl_classrel (c1', c2') =
+ if c1' = c2'
+ then Thm.trivial (cert (Logic.mk_of_class (TVar ((Name.aT, 0), []), c1')))
+ else the_classrel_thm thy (c1', c2');
+ fun gen_classrel (c1_pred, c2_succ) =
+ let
+ val th' = ((reflcl_classrel (c1_pred, c1) RS th) RS reflcl_classrel (c2, c2_succ))
+ |> Drule.instantiate' [SOME (certT (TVar ((Name.aT, 0), [])))] []
+ |> Thm.close_derivation;
+ val prf' = Thm.proof_of th';
+ in ((c1_pred, c2_succ), (th', prf')) end;
+
+ val new_classrels =
+ Library.map_product pair (c1 :: Graph.imm_preds classes c1) (c2 :: Graph.imm_succs classes c2)
+ |> filter_out (Symreltab.defined classrels)
+ |> map gen_classrel;
+ val needed = not (null new_classrels);
+ in
+ (needed,
+ if needed then map_proven_classrels (fold Symreltab.update new_classrels) thy
+ else thy)
+ end;
+
+fun complete_classrels thy =
+ let
+ val classrels = proven_classrels_of thy;
+ val diff_merge_classrels = diff_merge_classrels_of thy;
+ val (needed, thy') = (false, thy) |>
+ fold (fn c12 => fn (needed, thy) =>
+ put_trancl_classrel (c12, Symreltab.lookup classrels c12 |> the |> #1) thy
+ |>> (fn b => needed orelse b))
+ diff_merge_classrels;
+ in
+ if null diff_merge_classrels then NONE
+ else SOME (clear_diff_merge_classrels thy')
+ end;
fun the_arity thy a (c, Ss) =
- (case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss) of
- SOME (th, _) => Thm.transfer thy th
+ (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
+ SOME arity => arity
| NONE => error ("Unproven type arity " ^
Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
+fun the_arity_thm thy a c_Ss = the_arity thy a c_Ss |> #1 |> #1 |> Thm.transfer thy;
+fun the_arity_prf thy a c_Ss = the_arity thy a c_Ss |> #2;
+
fun thynames_of_arity thy (c, a) =
- Symtab.lookup_list (#2 (get_instances thy)) a
- |> map_filter (fn ((c', _), (_, name)) => if c = c' then SOME name else NONE)
+ Symtab.lookup_list (proven_arities_of thy) a
+ |> map_filter (fn ((c', _), ((_, name),_)) => if c = c' then SOME name else NONE)
|> rev;
-fun insert_arity_completions thy (t, ((c, Ss), (th, thy_name))) arities =
+fun insert_arity_completions thy (t, ((c, Ss), ((th, thy_name), _))) arities =
let
val algebra = Sign.classes_of thy;
val super_class_completions =
Sign.super_classes thy c
|> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2
andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t));
- val completions = map (fn c1 => (Sorts.classrel_derivation algebra
- (fn (th, c2) => fn c3 => th RS the_classrel thy (c2, c3)) (th, c) c1
- |> Thm.close_derivation, c1)) super_class_completions;
- val arities' = fold (fn (th1, c1) => Symtab.cons_list (t, ((c1, Ss), (th1, thy_name))))
+ val names_and_Ss = Name.names Name.context Name.aT (map (K []) Ss);
+ val completions = super_class_completions |> map (fn c1 =>
+ let
+ val th1 = (th RS the_classrel_thm thy (c, c1))
+ |> Drule.instantiate' (map (SOME o ctyp_of thy o TVar o apfst (rpair 0)) names_and_Ss) []
+ |> Thm.close_derivation;
+ val prf1 = Thm.proof_of th1;
+ in (((th1, thy_name), prf1), c1) end);
+ val arities' = fold (fn (th_thy_prf1, c1) => Symtab.cons_list (t, ((c1, Ss), th_thy_prf1)))
completions arities;
in (null completions, arities') end;
fun put_arity ((t, Ss, c), th) thy =
let
- val arity' = (t, ((c, Ss), (th, Context.theory_name thy)));
+ val arity' = (t, ((c, Ss), ((th, Context.theory_name thy), Thm.proof_of th)));
in
thy
- |> map_instances (fn (classrel, arities) => (classrel,
- arities
- |> Symtab.insert_list (eq_fst op =) arity'
- |> insert_arity_completions thy arity'
- |> snd))
+ |> map_proven_arities
+ (Symtab.insert_list (eq_fst op =) arity' #>
+ insert_arity_completions thy arity' #> snd)
end;
fun complete_arities thy =
let
- val arities = snd (get_instances thy);
+ val arities = proven_arities_of thy;
val (finished, arities') = arities
|> fold_map (insert_arity_completions thy) (Symtab.dest_list arities);
in
- if forall I finished then NONE
- else SOME (thy |> map_instances (fn (classrel, _) => (classrel, arities')))
+ if forall I finished
+ then NONE
+ else SOME (map_proven_arities (K arities') thy)
end;
-val _ = Context.>> (Context.map_theory (Theory.at_begin complete_arities));
+val _ = Context.>> (Context.map_theory
+ (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities));
(* maintain instance parameters *)
-val get_inst_params = #2 o #2 o AxClassData.get;
-val map_inst_params = AxClassData.map o apsnd o apsnd;
+fun get_inst_param thy (c, tyco) =
+ (case Symtab.lookup (the_default Symtab.empty (Symtab.lookup (#1 (inst_params_of thy)) c)) tyco of
+ SOME c' => c'
+ | NONE => error ("No instance parameter for constant " ^ quote c ^ " on type " ^ quote tyco));
-fun get_inst_param thy (c, tyco) =
- case Symtab.lookup ((the_default Symtab.empty o Symtab.lookup (fst (get_inst_params thy))) c) tyco
- of SOME c' => c'
- | NONE => error ("No instance parameter for constant " ^ quote c
- ^ " on type constructor " ^ quote tyco);
-
-fun add_inst_param (c, tyco) inst = (map_inst_params o apfst
- o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
+fun add_inst_param (c, tyco) inst =
+ (map_inst_params o apfst o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
#> (map_inst_params o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
-val inst_of_param = Symtab.lookup o snd o get_inst_params;
+val inst_of_param = Symtab.lookup o #2 o inst_params_of;
val param_of_inst = fst oo get_inst_param;
-fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
- (get_inst_params thy) [];
+fun inst_thms thy =
+ Symtab.fold (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of thy)) [];
fun get_inst_tyco consts = try (fst o dest_Type o the_single o Consts.typargs consts);
@@ -248,18 +335,20 @@
fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
-fun lookup_inst_param consts params (c, T) = case get_inst_tyco consts (c, T)
- of SOME tyco => AList.lookup (op =) params (c, tyco)
- | NONE => NONE;
+fun lookup_inst_param consts params (c, T) =
+ (case get_inst_tyco consts (c, T) of
+ SOME tyco => AList.lookup (op =) params (c, tyco)
+ | NONE => NONE);
fun unoverload_const thy (c_ty as (c, _)) =
- if is_some (class_of_param thy c)
- then case get_inst_tyco (Sign.consts_of thy) c_ty
- of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
- | NONE => c
+ if is_some (class_of_param thy c) then
+ (case get_inst_tyco (Sign.consts_of thy) c_ty of
+ SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
+ | NONE => c)
else c;
+
(** instances **)
(* class relations *)
@@ -331,6 +420,8 @@
(* primitive rules *)
+val shyps_topped = forall null o #shyps o Thm.rep_thm;
+
fun add_classrel raw_th thy =
let
val th = Thm.strip_shyps (Thm.transfer thy raw_th);
@@ -338,10 +429,14 @@
fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
val rel = Logic.dest_classrel prop handle TERM _ => err ();
val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
+ val th' = th
+ |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [c1])))] []
+ |> Thm.unconstrain_allTs;
+ val _ = shyps_topped th' orelse raise Fail "add_classrel: nontop shyps after unconstrain";
in
thy
|> Sign.primitive_classrel (c1, c2)
- |> put_classrel ((c1, c2), Thm.close_derivation (Drule.unconstrainTs th))
+ |> (snd oo put_trancl_classrel) ((c1, c2), th')
|> perhaps complete_arities
end;
@@ -351,17 +446,22 @@
val prop = Thm.plain_prop_of th;
fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
- val T = Type (t, map TFree (Name.names Name.context Name.aT Ss));
+ val names = Name.names Name.context Name.aT Ss;
+ val T = Type (t, map TFree names);
val missing_params = Sign.complete_sort thy [c]
|> maps (these o Option.map #params o try (get_info thy))
|> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
|> (map o apsnd o map_atyps) (K T);
val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
+ val th' = th
+ |> Drule.instantiate' (map (SOME o ctyp_of thy o TVar o apfst (rpair 0)) names) []
+ |> Thm.unconstrain_allTs;
+ val _ = shyps_topped th' orelse raise Fail "add_arity: nontop shyps after unconstrain";
in
thy
|> fold (snd oo declare_overloaded) missing_params
|> Sign.primitive_arity (t, Ss, [c])
- |> put_arity ((t, Ss, c), Thm.close_derivation (Drule.unconstrainTs th))
+ |> put_arity ((t, Ss, c), th')
end;
@@ -483,25 +583,24 @@
def_thy
|> Sign.qualified_path true bconst
|> PureThy.note_thmss ""
- [((Binding.name introN, []), [([Drule.export_without_context raw_intro], [])]),
- ((Binding.name superN, []), [(map Drule.export_without_context raw_classrel, [])]),
- ((Binding.name axiomsN, []),
+ [((Binding.name "intro", []), [([Drule.export_without_context raw_intro], [])]),
+ ((Binding.name "super", []), [(map Drule.export_without_context raw_classrel, [])]),
+ ((Binding.name "axioms", []),
[(map (fn th => Drule.export_without_context (class_triv RS th)) raw_axioms, [])])]
||> Sign.restore_naming def_thy;
(* result *)
- val axclass = make_axclass ((def, intro, axioms), params);
+ val axclass = make_axclass (def, intro, axioms, params);
val result_thy =
facts_thy
- |> fold put_classrel (map (pair class) super ~~ classrel)
+ |> fold (snd oo put_trancl_classrel) (map (pair class) super ~~ classrel)
|> Sign.qualified_path false bconst
|> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
|> Sign.restore_naming facts_thy
- |> map_axclasses (fn (axclasses, parameters) =>
- (Symtab.update (class, axclass) axclasses,
- fold (fn (x, _) => add_param pp (x, class)) params parameters));
+ |> map_axclasses (Symtab.update (class, axclass))
+ |> map_params (fold (fn (x, _) => add_param pp (x, class)) params);
in (class, result_thy) end;
--- a/src/Pure/display.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/display.ML Sun Apr 25 23:26:40 2010 +0200
@@ -182,7 +182,8 @@
val extern_const = Name_Space.extern (#1 constants);
val {classes, default, types, ...} = Type.rep_tsig tsig;
val (class_space, class_algebra) = classes;
- val {classes, arities} = Sorts.rep_algebra class_algebra;
+ val classes = Sorts.classes_of class_algebra;
+ val arities = Sorts.arities_of class_algebra;
val clsses = Name_Space.dest_table (class_space, Symtab.make (Graph.dest classes));
val tdecls = Name_Space.dest_table types;
--- a/src/Pure/drule.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/drule.ML Sun Apr 25 23:26:40 2010 +0200
@@ -106,7 +106,6 @@
val dummy_thm: thm
val sort_constraintI: thm
val sort_constraint_eq: thm
- val unconstrainTs: thm -> thm
val with_subgoal: int -> (thm -> thm) -> thm -> thm
val comp_no_flatten: thm * int -> int -> thm -> thm
val rename_bvars: (string * string) list -> thm -> thm
@@ -204,12 +203,6 @@
(** Standardization of rules **)
-(* type classes and sorts *)
-
-fun unconstrainTs th =
- fold (Thm.unconstrainT o Thm.ctyp_of (Thm.theory_of_thm th) o TVar)
- (Thm.fold_terms Term.add_tvars th []) th;
-
(*Generalization over a list of variables*)
val forall_intr_list = fold_rev forall_intr;
--- a/src/Pure/sorts.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/sorts.ML Sun Apr 25 23:26:40 2010 +0200
@@ -25,9 +25,8 @@
val insert_term: term -> sort OrdList.T -> sort OrdList.T
val insert_terms: term list -> sort OrdList.T -> sort OrdList.T
type algebra
- val rep_algebra: algebra ->
- {classes: serial Graph.T,
- arities: (class * (class * sort list)) list Symtab.table}
+ val classes_of: algebra -> serial Graph.T
+ val arities_of: algebra -> (class * (class * sort list)) list Symtab.table
val all_classes: algebra -> class list
val super_classes: algebra -> class -> class list
val class_less: algebra -> class * class -> bool
@@ -116,10 +115,8 @@
{classes: serial Graph.T,
arities: (class * (class * sort list)) list Symtab.table};
-fun rep_algebra (Algebra args) = args;
-
-val classes_of = #classes o rep_algebra;
-val arities_of = #arities o rep_algebra;
+fun classes_of (Algebra {classes, ...}) = classes;
+fun arities_of (Algebra {arities, ...}) = arities;
fun make_algebra (classes, arities) =
Algebra {classes = classes, arities = arities};
--- a/src/Pure/thm.ML Sun Apr 25 10:23:03 2010 -0700
+++ b/src/Pure/thm.ML Sun Apr 25 23:26:40 2010 +0200
@@ -92,8 +92,6 @@
val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
val trivial: cterm -> thm
- val of_class: ctyp * class -> thm
- val unconstrainT: ctyp -> thm -> thm
val dest_state: thm * int -> (term * term) list * term list * term * term
val lift_rule: cterm -> thm -> thm
val incr_indexes: int -> thm -> thm
@@ -139,6 +137,9 @@
val adjust_maxidx_thm: int -> thm -> thm
val varifyT_global: thm -> thm
val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
+ val of_class: ctyp * class -> thm
+ val unconstrainT: ctyp -> thm -> thm
+ val unconstrain_allTs: thm -> thm
val freezeT: thm -> thm
val assumption: int -> thm -> thm Seq.seq
val eq_assumption: int -> thm -> thm
@@ -1240,6 +1241,11 @@
prop = Logic.list_implies (constraints, unconstrain prop)})
end;
+fun unconstrain_allTs th =
+ fold (unconstrainT o ctyp_of (theory_of_thm th) o TVar)
+ (fold_terms Term.add_tvars th []) th;
+
+
(* Replace all TFrees not fixed or in the hyps by new TVars *)
fun varifyT_global' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
let