Merge with isabelle dev changes.
--- a/Admin/isatest/isatest-makedist Tue Sep 29 14:25:42 2009 +1000
+++ b/Admin/isatest/isatest-makedist Tue Sep 29 14:26:33 2009 +1000
@@ -102,8 +102,8 @@
#sleep 15
$SSH macbroy21 "$MAKEALL $HOME/settings/at64-poly-5.1-para"
sleep 15
-#$SSH macbroy23 -l HOL images "$MAKEALL $HOME/settings/at-sml-dev-e"
-#sleep 15
+$SSH macbroy23 "$MAKEALL -l HOL images $HOME/settings/at-sml-dev-e"
+sleep 15
$SSH atbroy99 "$MAKEALL $HOME/settings/at64-poly"
sleep 15
$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8; $MAKEALL $HOME/settings/mac-poly64-M4; $MAKEALL $HOME/settings/mac-poly64-M8"
--- a/src/HOL/HOL.thy Tue Sep 29 14:25:42 2009 +1000
+++ b/src/HOL/HOL.thy Tue Sep 29 14:26:33 2009 +1000
@@ -15,6 +15,7 @@
"~~/src/Tools/IsaPlanner/rw_inst.ML"
"~~/src/Tools/intuitionistic.ML"
"~~/src/Tools/project_rule.ML"
+ "~~/src/Tools/cong_tac.ML"
"~~/src/Provers/hypsubst.ML"
"~~/src/Provers/splitter.ML"
"~~/src/Provers/classical.ML"
@@ -240,15 +241,15 @@
by (rule subst)
-subsubsection {*Congruence rules for application*}
+subsubsection {* Congruence rules for application *}
-(*similar to AP_THM in Gordon's HOL*)
+text {* Similar to @{text AP_THM} in Gordon's HOL. *}
lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)"
apply (erule subst)
apply (rule refl)
done
-(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
+text {* Similar to @{text AP_TERM} in Gordon's HOL and FOL's @{text subst_context}. *}
lemma arg_cong: "x=y ==> f(x)=f(y)"
apply (erule subst)
apply (rule refl)
@@ -259,13 +260,15 @@
apply (rule refl)
done
-lemma cong: "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"
+lemma cong: "[| f = g; (x::'a) = y |] ==> f x = g y"
apply (erule subst)+
apply (rule refl)
done
+ML {* val cong_tac = Cong_Tac.cong_tac @{thm cong} *}
-subsubsection {*Equality of booleans -- iff*}
+
+subsubsection {* Equality of booleans -- iff *}
lemma iffI: assumes "P ==> Q" and "Q ==> P" shows "P=Q"
by (iprover intro: iff [THEN mp, THEN mp] impI assms)
@@ -1466,7 +1469,7 @@
subsubsection {* Coherent logic *}
ML {*
-structure Coherent = CoherentFun
+structure Coherent = Coherent
(
val atomize_elimL = @{thm atomize_elimL}
val atomize_exL = @{thm atomize_exL}
--- a/src/HOL/IsaMakefile Tue Sep 29 14:25:42 2009 +1000
+++ b/src/HOL/IsaMakefile Tue Sep 29 14:26:33 2009 +1000
@@ -87,30 +87,31 @@
$(SRC)/Provers/hypsubst.ML \
$(SRC)/Provers/quantifier1.ML \
$(SRC)/Provers/splitter.ML \
- $(SRC)/Tools/IsaPlanner/isand.ML \
- $(SRC)/Tools/IsaPlanner/rw_inst.ML \
- $(SRC)/Tools/IsaPlanner/rw_tools.ML \
- $(SRC)/Tools/IsaPlanner/zipper.ML \
- $(SRC)/Tools/atomize_elim.ML \
- $(SRC)/Tools/auto_solve.ML \
$(SRC)/Tools/Code/code_haskell.ML \
$(SRC)/Tools/Code/code_ml.ML \
$(SRC)/Tools/Code/code_preproc.ML \
$(SRC)/Tools/Code/code_printer.ML \
$(SRC)/Tools/Code/code_target.ML \
$(SRC)/Tools/Code/code_thingol.ML \
+ $(SRC)/Tools/Code_Generator.thy \
+ $(SRC)/Tools/IsaPlanner/isand.ML \
+ $(SRC)/Tools/IsaPlanner/rw_inst.ML \
+ $(SRC)/Tools/IsaPlanner/rw_tools.ML \
+ $(SRC)/Tools/IsaPlanner/zipper.ML \
+ $(SRC)/Tools/atomize_elim.ML \
+ $(SRC)/Tools/auto_solve.ML \
$(SRC)/Tools/coherent.ML \
+ $(SRC)/Tools/cong_tac.ML \
$(SRC)/Tools/eqsubst.ML \
$(SRC)/Tools/induct.ML \
+ $(SRC)/Tools/induct_tacs.ML \
$(SRC)/Tools/intuitionistic.ML \
- $(SRC)/Tools/induct_tacs.ML \
+ $(SRC)/Tools/more_conv.ML \
$(SRC)/Tools/nbe.ML \
+ $(SRC)/Tools/project_rule.ML \
$(SRC)/Tools/quickcheck.ML \
- $(SRC)/Tools/project_rule.ML \
$(SRC)/Tools/random_word.ML \
$(SRC)/Tools/value.ML \
- $(SRC)/Tools/Code_Generator.thy \
- $(SRC)/Tools/more_conv.ML \
HOL.thy \
Tools/hologic.ML \
Tools/recfun_codegen.ML \
@@ -130,9 +131,9 @@
Inductive.thy \
Lattices.thy \
Nat.thy \
+ Option.thy \
OrderedGroup.thy \
Orderings.thy \
- Option.thy \
Plain.thy \
Power.thy \
Predicate.thy \
@@ -215,8 +216,8 @@
Equiv_Relations.thy \
Groebner_Basis.thy \
Hilbert_Choice.thy \
+ Int.thy \
IntDiv.thy \
- Int.thy \
List.thy \
Main.thy \
Map.thy \
@@ -280,8 +281,8 @@
$(OUT)/HOL: ROOT.ML $(MAIN_DEPENDENCIES) \
Archimedean_Field.thy \
+ Complex.thy \
Complex_Main.thy \
- Complex.thy \
Deriv.thy \
Fact.thy \
GCD.thy \
@@ -294,18 +295,18 @@
MacLaurin.thy \
Nat_Transfer.thy \
NthRoot.thy \
+ PReal.thy \
+ Parity.thy \
+ RComplete.thy \
+ Rational.thy \
+ Real.thy \
+ RealDef.thy \
+ RealPow.thy \
+ RealVector.thy \
SEQ.thy \
Series.thy \
Taylor.thy \
Transcendental.thy \
- Parity.thy \
- PReal.thy \
- Rational.thy \
- RComplete.thy \
- RealDef.thy \
- RealPow.thy \
- Real.thy \
- RealVector.thy \
Tools/float_syntax.ML \
Tools/transfer.ML \
Tools/Qelim/ferrante_rackoff_data.ML \
--- a/src/HOL/Nominal/nominal_datatype.ML Tue Sep 29 14:25:42 2009 +1000
+++ b/src/HOL/Nominal/nominal_datatype.ML Tue Sep 29 14:26:33 2009 +1000
@@ -245,7 +245,7 @@
val (full_new_type_names',thy1) =
Datatype.add_datatype config new_type_names' dts'' thy;
- val {descr, inducts = (_, induct), ...} =
+ val {descr, induct, ...} =
Datatype.the_info thy1 (hd full_new_type_names');
fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
--- a/src/HOL/Nominal/nominal_permeq.ML Tue Sep 29 14:25:42 2009 +1000
+++ b/src/HOL/Nominal/nominal_permeq.ML Tue Sep 29 14:26:33 2009 +1000
@@ -228,11 +228,7 @@
addsimprocs [perm_compose_simproc]) i,
asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i] st);
-
-(* applying Stefan's smart congruence tac *)
-fun apply_cong_tac i =
- ("application of congruence",
- (fn st => DatatypeAux.cong_tac i st handle Subscript => no_tac st));
+fun apply_cong_tac i = ("application of congruence", cong_tac i);
(* unfolds the definition of permutations *)
--- a/src/HOL/Tools/Datatype/datatype.ML Tue Sep 29 14:25:42 2009 +1000
+++ b/src/HOL/Tools/Datatype/datatype.ML Tue Sep 29 14:26:33 2009 +1000
@@ -39,8 +39,9 @@
open DatatypeAux;
+(** theory data **)
-(* theory data *)
+(* data management *)
structure DatatypesData = TheoryDataFun
(
@@ -62,13 +63,16 @@
);
val get_all = #types o DatatypesData.get;
-val map_datatypes = DatatypesData.map;
-
+val get_info = Symtab.lookup o get_all;
+fun the_info thy name = (case get_info thy name of
+ SOME info => info
+ | NONE => error ("Unknown datatype " ^ quote name));
-(** theory information about datatypes **)
+val info_of_constr = Symtab.lookup o #constrs o DatatypesData.get;
+val info_of_case = Symtab.lookup o #cases o DatatypesData.get;
-fun put_dt_infos (dt_infos : (string * info) list) =
- map_datatypes (fn {types, constrs, cases} =>
+fun register (dt_infos : (string * info) list) =
+ DatatypesData.map (fn {types, constrs, cases} =>
{types = fold Symtab.update dt_infos types,
constrs = fold Symtab.default (*conservative wrt. overloaded constructors*)
(maps (fn (_, info as {descr, index, ...}) => map (rpair info o fst)
@@ -77,19 +81,7 @@
(map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)
cases});
-val get_info = Symtab.lookup o get_all;
-
-fun the_info thy name = (case get_info thy name of
- SOME info => info
- | NONE => error ("Unknown datatype " ^ quote name));
-
-val info_of_constr = Symtab.lookup o #constrs o DatatypesData.get;
-val info_of_case = Symtab.lookup o #cases o DatatypesData.get;
-
-fun get_info_descr thy dtco =
- get_info thy dtco
- |> Option.map (fn info as { descr, index, ... } =>
- (info, (((fn SOME (_, dtys, cos) => (dtys, cos)) o AList.lookup (op =) descr) index)));
+(* complex queries *)
fun the_spec thy dtco =
let
@@ -143,69 +135,9 @@
| NONE => NONE;
-(** induct method setup **)
-
-(* case names *)
-
-local
-
-fun dt_recs (DtTFree _) = []
- | dt_recs (DtType (_, dts)) = maps dt_recs dts
- | dt_recs (DtRec i) = [i];
-
-fun dt_cases (descr: descr) (_, args, constrs) =
- let
- fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
- val bnames = map the_bname (distinct (op =) (maps dt_recs args));
- in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
-
-
-fun induct_cases descr =
- DatatypeProp.indexify_names (maps (dt_cases descr) (map #2 descr));
-
-fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
-
-in
-
-fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
-
-fun mk_case_names_exhausts descr new =
- map (RuleCases.case_names o exhaust_cases descr o #1)
- (filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
-
-end;
+(** various auxiliary **)
-fun add_rules simps case_thms rec_thms inject distinct
- weak_case_congs cong_att =
- PureThy.add_thmss [((Binding.name "simps", simps), []),
- ((Binding.empty, flat case_thms @
- flat distinct @ rec_thms), [Simplifier.simp_add]),
- ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]),
- ((Binding.empty, flat inject), [iff_add]),
- ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
- ((Binding.empty, weak_case_congs), [cong_att])]
- #> snd;
-
-
-(* add_cases_induct *)
-
-fun add_cases_induct infos inducts thy =
- let
- fun named_rules (name, {index, exhaust, ...}: info) =
- [((Binding.empty, nth inducts index), [Induct.induct_type name]),
- ((Binding.empty, exhaust), [Induct.cases_type name])];
- fun unnamed_rule i =
- ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
- in
- thy |> PureThy.add_thms
- (maps named_rules infos @
- map unnamed_rule (length infos upto length inducts - 1)) |> snd
- |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
- end;
-
-
-
-(**** simplification procedure for showing distinctness of constructors ****)
+(* simplification procedure for showing distinctness of constructors *)
fun stripT (i, Type ("fun", [_, T])) = stripT (i + 1, T)
| stripT p = p;
@@ -233,17 +165,21 @@
etac FalseE 1]))
end;
+fun get_constr thy dtco =
+ get_info thy dtco
+ |> Option.map (fn { descr, index, ... } => (#3 o the o AList.lookup (op =) descr) index);
+
fun distinct_proc thy ss (t as Const ("op =", _) $ t1 $ t2) =
(case (stripC (0, t1), stripC (0, t2)) of
((i, Const (cname1, T1)), (j, Const (cname2, T2))) =>
(case (stripT (0, T1), stripT (0, T2)) of
((i', Type (tname1, _)), (j', Type (tname2, _))) =>
if tname1 = tname2 andalso not (cname1 = cname2) andalso i = i' andalso j = j' then
- (case (get_info_descr thy) tname1 of
- SOME (_, (_, constrs)) => let val cnames = map fst constrs
+ (case get_constr thy tname1 of
+ SOME constrs => let val cnames = map fst constrs
in if cname1 mem cnames andalso cname2 mem cnames then
SOME (distinct_rule thy ss tname1
- (Logic.mk_equals (t, Const ("False", HOLogic.boolT))))
+ (Logic.mk_equals (t, HOLogic.false_const)))
else NONE
end
| NONE => NONE)
@@ -260,29 +196,7 @@
val simproc_setup =
Simplifier.map_simpset (fn ss => ss addsimprocs [distinct_simproc]);
-
-(**** translation rules for case ****)
-
-fun make_case ctxt = DatatypeCase.make_case
- (info_of_constr (ProofContext.theory_of ctxt)) ctxt;
-
-fun strip_case ctxt = DatatypeCase.strip_case
- (info_of_case (ProofContext.theory_of ctxt));
-
-fun add_case_tr' case_names thy =
- Sign.add_advanced_trfuns ([], [],
- map (fn case_name =>
- let val case_name' = Sign.const_syntax_name thy case_name
- in (case_name', DatatypeCase.case_tr' info_of_case case_name')
- end) case_names, []) thy;
-
-val trfun_setup =
- Sign.add_advanced_trfuns ([],
- [("_case_syntax", DatatypeCase.case_tr true info_of_constr)],
- [], []);
-
-
-(* prepare types *)
+(* prepare datatype specifications *)
fun read_typ thy ((Ts, sorts), str) =
let
@@ -302,154 +216,188 @@
| dups => error ("Inconsistent sort constraints for " ^ commas dups))
end;
+(* case names *)
-(**** make datatype info ****)
+local
+
+fun dt_recs (DtTFree _) = []
+ | dt_recs (DtType (_, dts)) = maps dt_recs dts
+ | dt_recs (DtRec i) = [i];
+
+fun dt_cases (descr: descr) (_, args, constrs) =
+ let
+ fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
+ val bnames = map the_bname (distinct (op =) (maps dt_recs args));
+ in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
+
+fun induct_cases descr =
+ DatatypeProp.indexify_names (maps (dt_cases descr) (map #2 descr));
+
+fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
+
+in
+
+fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
+
+fun mk_case_names_exhausts descr new =
+ map (RuleCases.case_names o exhaust_cases descr o #1)
+ (filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
+
+end;
+
+(* translation rules for case *)
+
+fun make_case ctxt = DatatypeCase.make_case
+ (info_of_constr (ProofContext.theory_of ctxt)) ctxt;
+
+fun strip_case ctxt = DatatypeCase.strip_case
+ (info_of_case (ProofContext.theory_of ctxt));
-fun make_dt_info alt_names descr sorts inducts reccomb_names rec_thms
- ((((((((((i, (_, (tname, _, _))), case_name), case_thms),
- exhaust_thm), distinct_thm), inject), splits), nchotomy), case_cong), weak_case_cong) =
- (tname,
- {index = i,
- alt_names = alt_names,
- descr = descr,
- sorts = sorts,
- rec_names = reccomb_names,
- rec_rewrites = rec_thms,
- case_name = case_name,
- case_rewrites = case_thms,
- inducts = inducts,
- exhaust = exhaust_thm,
- distinct = distinct_thm,
- inject = inject,
- splits = splits,
- nchotomy = nchotomy,
- case_cong = case_cong,
- weak_case_cong = weak_case_cong});
+fun add_case_tr' case_names thy =
+ Sign.add_advanced_trfuns ([], [],
+ map (fn case_name =>
+ let val case_name' = Sign.const_syntax_name thy case_name
+ in (case_name', DatatypeCase.case_tr' info_of_case case_name')
+ end) case_names, []) thy;
+
+val trfun_setup =
+ Sign.add_advanced_trfuns ([],
+ [("_case_syntax", DatatypeCase.case_tr true info_of_constr)],
+ [], []);
+
+(* document antiquotation *)
+
+val _ = ThyOutput.antiquotation "datatype" Args.tyname
+ (fn {source = src, context = ctxt, ...} => fn dtco =>
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val (vs, cos) = the_spec thy dtco;
+ val ty = Type (dtco, map TFree vs);
+ fun pretty_typ_bracket (ty as Type (_, _ :: _)) =
+ Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty]
+ | pretty_typ_bracket ty =
+ Syntax.pretty_typ ctxt ty;
+ fun pretty_constr (co, tys) =
+ (Pretty.block o Pretty.breaks)
+ (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
+ map pretty_typ_bracket tys);
+ val pretty_datatype =
+ Pretty.block
+ (Pretty.command "datatype" :: Pretty.brk 1 ::
+ Syntax.pretty_typ ctxt ty ::
+ Pretty.str " =" :: Pretty.brk 1 ::
+ flat (separate [Pretty.brk 1, Pretty.str "| "]
+ (map (single o pretty_constr) cos)));
+ in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
+
+
+(** abstract theory extensions relative to a datatype characterisation **)
structure DatatypeInterpretation = InterpretationFun
(type T = config * string list val eq: T * T -> bool = eq_snd op =);
fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
-
-(******************* definitional introduction of datatypes *******************)
+fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
+ (index, (((((((((((_, (tname, _, _))), inject), distinct),
+ exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong), (split, split_asm))) =
+ (tname,
+ {index = index,
+ alt_names = alt_names,
+ descr = descr,
+ sorts = sorts,
+ inject = inject,
+ distinct = distinct,
+ induct = induct,
+ inducts = inducts,
+ exhaust = exhaust,
+ nchotomy = nchotomy,
+ rec_names = rec_names,
+ rec_rewrites = rec_rewrites,
+ case_name = case_name,
+ case_rewrites = case_rewrites,
+ case_cong = case_cong,
+ weak_case_cong = weak_case_cong,
+ split = split,
+ split_asm = split_asm});
-fun add_datatype_def (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
- case_names_induct case_names_exhausts thy =
+fun derive_datatype_props config dt_names alt_names descr sorts
+ induct inject (distinct_rules, distinct_rewrites, distinct_entry) thy1 =
let
- val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
-
- val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |>
- DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
- types_syntax constr_syntax case_names_induct;
- val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
+ val thy2 = thy1 |> Theory.checkpoint;
+ val flat_descr = flat descr;
+ val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
+ val _ = message config ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
- val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr
- sorts induct case_names_exhausts thy2;
- val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
- config new_type_names descr sorts dt_info inject dist_rewrites
- (Simplifier.theory_context thy3 dist_ss) induct thy3;
- val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
- config new_type_names descr sorts reccomb_names rec_thms thy4;
- val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms config new_type_names
- descr sorts inject dist_rewrites casedist_thms case_thms thy6;
- val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys config new_type_names
- descr sorts casedist_thms thy7;
- val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
- descr sorts nchotomys case_thms thy8;
- val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
- descr sorts thy9;
+ val (exhaust, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names
+ descr sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2;
+ val (nchotomys, thy4) = DatatypeAbsProofs.prove_nchotomys config new_type_names
+ descr sorts exhaust thy3;
+ val ((rec_names, rec_rewrites), thy5) = DatatypeAbsProofs.prove_primrec_thms
+ config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
+ inject distinct_rewrites (Simplifier.theory_context thy4 dist_ss) induct thy4;
+ val ((case_rewrites, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
+ config new_type_names descr sorts rec_names rec_rewrites thy5;
+ val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
+ descr sorts nchotomys case_rewrites thy6;
+ val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
+ descr sorts thy7;
+ val (splits, thy9) = DatatypeAbsProofs.prove_split_thms
+ config new_type_names descr sorts inject distinct_rewrites exhaust case_rewrites thy8;
- val dt_infos = map
- (make_dt_info (SOME new_type_names) (flat descr) sorts (inducts, induct) reccomb_names rec_thms)
- ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_thms ~~
- casedist_thms ~~ simproc_dists ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
-
- val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
+ val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
+ val dt_infos = map_index (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
+ (hd descr ~~ inject ~~ distinct_entry ~~ exhaust ~~ nchotomys ~~
+ case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
val dt_names = map fst dt_infos;
-
- val thy12 =
- thy10
- |> add_case_tr' case_names
- |> Sign.add_path (space_implode "_" new_type_names)
- |> add_rules simps case_thms rec_thms inject distinct
- weak_case_congs (Simplifier.attrib (op addcongs))
- |> put_dt_infos dt_infos
- |> add_cases_induct dt_infos inducts
- |> Sign.parent_path
- |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
- |> DatatypeInterpretation.data (config, map fst dt_infos);
- in (dt_names, thy12) end;
+ val prfx = Binding.qualify true (space_implode "_" new_type_names);
+ val simps = flat (inject @ distinct_rules @ case_rewrites) @ rec_rewrites;
+ val named_rules = flat (map_index (fn (index, tname) =>
+ [((Binding.empty, [nth inducts index]), [Induct.induct_type tname]),
+ ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
+ val unnamed_rules = map (fn induct =>
+ ((Binding.empty, [induct]), [Thm.kind_internal, Induct.induct_type ""]))
+ (Library.drop (length dt_names, inducts));
+ in
+ thy9
+ |> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []),
+ ((prfx (Binding.name "inducts"), inducts), []),
+ ((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []),
+ ((Binding.empty, flat case_rewrites @ flat distinct_rules @ rec_rewrites),
+ [Simplifier.simp_add]),
+ ((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]),
+ ((Binding.empty, flat inject), [iff_add]),
+ ((Binding.empty, map (fn th => th RS notE) (flat distinct_rules)),
+ [Classical.safe_elim NONE]),
+ ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)])]
+ @ named_rules @ unnamed_rules)
+ |> snd
+ |> add_case_tr' case_names
+ |> register dt_infos
+ |> DatatypeInterpretation.data (config, dt_names)
+ |> pair dt_names
+ end;
-(*********************** declare existing type as datatype *********************)
-
-fun prove_rep_datatype (config : config) alt_names new_type_names descr sorts induct inject half_distinct thy =
- let
- val ((_, [induct']), _) =
- Variable.importT [induct] (Variable.thm_context induct);
-
- fun err t = error ("Ill-formed predicate in induction rule: " ^
- Syntax.string_of_term_global thy t);
-
- fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
- ((tname, map (fst o dest_TFree) Ts) handle TERM _ => err t)
- | get_typ t = err t;
- val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct')));
-
- val dt_info = get_all thy;
-
- val distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
- val (case_names_induct, case_names_exhausts) =
- (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames));
-
- val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
+(** declare existing type as datatype **)
- val (casedist_thms, thy2) = thy |>
- DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
- case_names_exhausts;
- val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms
- config new_type_names [descr] sorts dt_info inject distinct
- (Simplifier.theory_context thy2 dist_ss) induct thy2;
- val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms
- config new_type_names [descr] sorts reccomb_names rec_thms thy3;
- val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms
- config new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
- val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys config new_type_names
- [descr] sorts casedist_thms thy5;
- val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
- [descr] sorts nchotomys case_thms thy6;
- val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
- [descr] sorts thy7;
-
- val ((_, [induct']), thy10) =
- thy8
- |> store_thmss "inject" new_type_names inject
- ||>> store_thmss "distinct" new_type_names distinct
+fun prove_rep_datatype config dt_names alt_names descr sorts raw_inject half_distinct raw_induct thy1 =
+ let
+ val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
+ val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
+ val (((inject, distinct), [induct]), thy2) =
+ thy1
+ |> store_thmss "inject" new_type_names raw_inject
+ ||>> store_thmss "distinct" new_type_names raw_distinct
||> Sign.add_path (space_implode "_" new_type_names)
- ||>> PureThy.add_thms [((Binding.name "induct", induct), [case_names_induct])];
- val inducts = Project_Rule.projections (ProofContext.init thy10) induct';
-
- val dt_infos = map (make_dt_info alt_names descr sorts (inducts, induct') reccomb_names rec_thms)
- ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
- map FewConstrs distinct ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
-
- val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
- val dt_names = map fst dt_infos;
+ ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])]
+ ||> Sign.restore_naming thy1;
+ in
+ thy2
+ |> derive_datatype_props config dt_names alt_names [descr] sorts
+ induct inject (distinct, distinct, map FewConstrs distinct)
+ end;
- val thy11 =
- thy10
- |> add_case_tr' case_names
- |> add_rules simps case_thms rec_thms inject distinct
- weak_case_congs (Simplifier.attrib (op addcongs))
- |> put_dt_infos dt_infos
- |> add_cases_induct dt_infos inducts
- |> Sign.parent_path
- |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
- |> snd
- |> DatatypeInterpretation.data (config, dt_names);
- in (dt_names, thy11) end;
-
-fun gen_rep_datatype prep_term (config : config) after_qed alt_names raw_ts thy =
+fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
let
fun constr_of_term (Const (c, T)) = (c, T)
| constr_of_term t =
@@ -487,7 +435,7 @@
val cs = map (apsnd (map norm_constr)) raw_cs;
val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
o fst o strip_type;
- val new_type_names = map Long_Name.base_name (the_default (map fst cs) alt_names);
+ val dt_names = map fst cs;
fun mk_spec (i, (tyco, constr)) = (i, (tyco,
map (DtTFree o fst) vs,
@@ -500,12 +448,12 @@
fun after_qed' raw_thms =
let
- val [[[induct]], injs, half_distincts] =
+ val [[[raw_induct]], raw_inject, half_distinct] =
unflat rules (map Drule.zero_var_indexes_list raw_thms);
(*FIXME somehow dubious*)
in
ProofContext.theory_result
- (prove_rep_datatype config alt_names new_type_names descr vs induct injs half_distincts)
+ (prove_rep_datatype config dt_names alt_names descr vs raw_inject half_distinct raw_induct)
#-> after_qed
end;
in
@@ -518,15 +466,13 @@
val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);
+(** definitional introduction of datatypes **)
-(******************************** add datatype ********************************)
-
-fun gen_add_datatype prep_typ (config : config) new_type_names dts thy =
+fun gen_add_datatype prep_typ config new_type_names dts thy =
let
val _ = Theory.requires thy "Datatype" "datatype definitions";
(* this theory is used just for parsing *)
-
val tmp_thy = thy |>
Theory.copy |>
Sign.add_types (map (fn (tvs, tname, mx, _) =>
@@ -541,6 +487,7 @@
| dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
" : " ^ commas dups))
end) dts);
+ val dt_names = map fst new_dts;
val _ = (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
[] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
@@ -583,20 +530,19 @@
if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
else raise exn;
- val descr' = flat descr;
- val case_names_induct = mk_case_names_induct descr';
- val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
+ val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
+ val ((inject, distinct_rules, distinct_rewrites, distinct_entry, induct), thy') = thy |>
+ DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
+ types_syntax constr_syntax (mk_case_names_induct (flat descr));
in
- add_datatype_def
- (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
- case_names_induct case_names_exhausts thy
+ derive_datatype_props config dt_names (SOME new_type_names) descr sorts
+ induct inject (distinct_rules, distinct_rewrites, distinct_entry) thy'
end;
val add_datatype = gen_add_datatype cert_typ;
val datatype_cmd = snd ooo gen_add_datatype read_typ default_config;
-
(** package setup **)
(* setup theory *)
@@ -607,7 +553,6 @@
trfun_setup #>
DatatypeInterpretation.init;
-
(* outer syntax *)
local
@@ -642,31 +587,5 @@
end;
-
-(* document antiquotation *)
-
-val _ = ThyOutput.antiquotation "datatype" Args.tyname
- (fn {source = src, context = ctxt, ...} => fn dtco =>
- let
- val thy = ProofContext.theory_of ctxt;
- val (vs, cos) = the_spec thy dtco;
- val ty = Type (dtco, map TFree vs);
- fun pretty_typ_bracket (ty as Type (_, _ :: _)) =
- Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty]
- | pretty_typ_bracket ty =
- Syntax.pretty_typ ctxt ty;
- fun pretty_constr (co, tys) =
- (Pretty.block o Pretty.breaks)
- (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
- map pretty_typ_bracket tys);
- val pretty_datatype =
- Pretty.block
- (Pretty.command "datatype" :: Pretty.brk 1 ::
- Syntax.pretty_typ ctxt ty ::
- Pretty.str " =" :: Pretty.brk 1 ::
- flat (separate [Pretty.brk 1, Pretty.str "| "]
- (map (single o pretty_constr) cos)));
- in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
-
end;
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Tue Sep 29 14:25:42 2009 +1000
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Tue Sep 29 14:26:33 2009 +1000
@@ -20,7 +20,7 @@
attribute list -> theory -> thm list * theory
val prove_primrec_thms : config -> string list ->
descr list -> (string * sort) list ->
- info Symtab.table -> thm list list -> thm list list ->
+ (string -> thm list) -> thm list list -> thm list list ->
simpset -> thm -> theory -> (string list * thm list) * theory
val prove_case_thms : config -> string list ->
descr list -> (string * sort) list ->
@@ -88,7 +88,7 @@
(*************************** primrec combinators ******************************)
fun prove_primrec_thms (config : config) new_type_names descr sorts
- (dt_info : info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
+ injects_of constr_inject dist_rewrites dist_ss induct thy =
let
val _ = message config "Constructing primrec combinators ...";
@@ -174,11 +174,11 @@
val inject = map (fn r => r RS iffD1)
(if i < length newTs then List.nth (constr_inject, i)
- else #inject (the (Symtab.lookup dt_info tname)));
+ else injects_of tname);
fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) =
let
- val k = length (List.filter is_rec_type cargs)
+ val k = length (filter is_rec_type cargs)
in (EVERY [DETERM tac,
REPEAT (etac ex1E 1), rtac ex1I 1,
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Tue Sep 29 14:25:42 2009 +1000
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Tue Sep 29 14:26:33 2009 +1000
@@ -35,7 +35,6 @@
val app_bnds : term -> int -> term
- val cong_tac : int -> tactic
val indtac : thm -> string list -> int -> tactic
val exh_tac : (string -> thm) -> int -> tactic
@@ -112,21 +111,6 @@
fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
-fun cong_tac i st = (case Logic.strip_assums_concl
- (List.nth (prems_of st, i - 1)) of
- _ $ (_ $ (f $ x) $ (g $ y)) =>
- let
- val cong' = Thm.lift_rule (Thm.cprem_of st i) cong;
- val _ $ (_ $ (f' $ x') $ (g' $ y')) =
- Logic.strip_assums_concl (prop_of cong');
- val insts = map (pairself (cterm_of (Thm.theory_of_thm st)) o
- apsnd (curry list_abs (Logic.strip_params (concl_of cong'))) o
- apfst head_of) [(f', f), (g', g), (x', x), (y', y)]
- in compose_tac (false, cterm_instantiate insts cong', 2) i st
- handle THM _ => no_tac st
- end
- | _ => no_tac st);
-
(* instantiate induction rule *)
fun indtac indrule indnames i st =
@@ -191,18 +175,20 @@
alt_names : string list option,
descr : descr,
sorts : (string * sort) list,
+ inject : thm list,
+ distinct : simproc_dist,
+ induct : thm,
+ inducts : thm list,
+ exhaust : thm,
+ nchotomy : thm,
rec_names : string list,
rec_rewrites : thm list,
case_name : string,
case_rewrites : thm list,
- inducts : thm list * thm,
- exhaust : thm,
- distinct : simproc_dist,
- inject : thm list,
- splits : thm * thm,
- nchotomy : thm,
case_cong : thm,
- weak_case_cong : thm};
+ weak_case_cong : thm,
+ split : thm,
+ split_asm: thm};
fun mk_Free s T i = Free (s ^ (string_of_int i), T);
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Sep 29 14:25:42 2009 +1000
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Sep 29 14:26:33 2009 +1000
@@ -38,7 +38,7 @@
fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT);
-fun make_ind sorts ({descr, rec_names, rec_rewrites, inducts = (_, induct), ...} : info) is thy =
+fun make_ind sorts ({descr, rec_names, rec_rewrites, induct, ...} : info) is thy =
let
val recTs = get_rec_types descr sorts;
val pnames = if length descr = 1 then ["P"]
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Tue Sep 29 14:25:42 2009 +1000
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Tue Sep 29 14:26:33 2009 +1000
@@ -389,7 +389,7 @@
fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
let
val (_, (tname, _, _)) = hd ds;
- val induct = (snd o #inducts o the o Symtab.lookup dt_info) tname;
+ val induct = (#induct o the o Symtab.lookup dt_info) tname;
fun mk_ind_concl (i, _) =
let
--- a/src/HOL/Tools/Function/size.ML Tue Sep 29 14:25:42 2009 +1000
+++ b/src/HOL/Tools/Function/size.ML Tue Sep 29 14:26:33 2009 +1000
@@ -59,7 +59,7 @@
fun prove_size_thms (info : info) new_type_names thy =
let
- val {descr, alt_names, sorts, rec_names, rec_rewrites, inducts = (_, induct), ...} = info;
+ val {descr, alt_names, sorts, rec_names, rec_rewrites, induct, ...} = info;
val l = length new_type_names;
val alt_names' = (case alt_names of
NONE => replicate l NONE | SOME names => map SOME names);
--- a/src/HOL/Tools/TFL/casesplit.ML Tue Sep 29 14:25:42 2009 +1000
+++ b/src/HOL/Tools/TFL/casesplit.ML Tue Sep 29 14:26:33 2009 +1000
@@ -96,7 +96,7 @@
| TVar((s,i),_) => error ("Free variable: " ^ s)
val dt = Datatype.the_info thy ty_str
in
- cases_thm_of_induct_thm (snd (#inducts dt))
+ cases_thm_of_induct_thm (#induct dt)
end;
(*
--- a/src/HOL/Tools/old_primrec.ML Tue Sep 29 14:25:42 2009 +1000
+++ b/src/HOL/Tools/old_primrec.ML Tue Sep 29 14:26:33 2009 +1000
@@ -230,7 +230,7 @@
(tname, dt)::(find_dts dt_info tnames' tnames)
else find_dts dt_info tnames' tnames);
-fun prepare_induct ({descr, inducts = (_, induct), ...}: info) rec_eqns =
+fun prepare_induct ({descr, induct, ...}: info) rec_eqns =
let
fun constrs_of (_, (_, _, cs)) =
map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
--- a/src/HOL/ex/Coherent.thy Tue Sep 29 14:25:42 2009 +1000
+++ b/src/HOL/ex/Coherent.thy Tue Sep 29 14:26:33 2009 +1000
@@ -1,14 +1,15 @@
-(* Title: HOL/ex/Coherent
- ID: $Id$
+(* Title: HOL/ex/Coherent.thy
Author: Stefan Berghofer, TU Muenchen
- Marc Bezem, Institutt for Informatikk, Universitetet i Bergen
+ Author: Marc Bezem, Institutt for Informatikk, Universitetet i Bergen
*)
-header{* Coherent Logic Problems *}
+header {* Coherent Logic Problems *}
-theory Coherent imports Main begin
+theory Coherent
+imports Main
+begin
-subsection{* Equivalence of two versions of Pappus' Axiom *}
+subsection {* Equivalence of two versions of Pappus' Axiom *}
no_notation
comp (infixl "o" 55) and
--- a/src/Pure/Concurrent/future.ML Tue Sep 29 14:25:42 2009 +1000
+++ b/src/Pure/Concurrent/future.ML Tue Sep 29 14:26:33 2009 +1000
@@ -37,10 +37,11 @@
val peek: 'a future -> 'a Exn.result option
val is_finished: 'a future -> bool
val value: 'a -> 'a future
- val fork: (unit -> 'a) -> 'a future
val fork_group: group -> (unit -> 'a) -> 'a future
+ val fork_deps_pri: 'b future list -> int -> (unit -> 'a) -> 'a future
val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
val fork_pri: int -> (unit -> 'a) -> 'a future
+ val fork: (unit -> 'a) -> 'a future
val join_results: 'a future list -> 'a Exn.result list
val join_result: 'a future -> 'a Exn.result
val join: 'a future -> 'a
@@ -322,10 +323,11 @@
in task end);
in Future {task = task, group = group, result = result} end;
-fun fork e = fork_future NONE [] 0 e;
fun fork_group group e = fork_future (SOME group) [] 0 e;
-fun fork_deps deps e = fork_future NONE (map task_of deps) 0 e;
-fun fork_pri pri e = fork_future NONE [] pri e;
+fun fork_deps_pri deps pri e = fork_future NONE (map task_of deps) pri e;
+fun fork_deps deps e = fork_deps_pri deps 0 e;
+fun fork_pri pri e = fork_deps_pri [] pri e;
+fun fork e = fork_deps [] e;
(* join *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/synchronized_dummy.ML Tue Sep 29 14:26:33 2009 +1000
@@ -0,0 +1,25 @@
+(* Title: Pure/Concurrent/synchronized_dummy.ML
+ Author: Makarius
+
+Dummy version of state variables -- plain refs for sequential access.
+*)
+
+structure Synchronized: SYNCHRONIZED =
+struct
+
+datatype 'a var = Var of 'a ref;
+
+fun var _ x = Var (ref x);
+fun value (Var var) = ! var;
+
+fun timed_access (Var var) _ f =
+ (case f (! var) of
+ SOME (y, x') => (var := x'; SOME y)
+ | NONE => Thread.unavailable ());
+
+fun guarded_access var f = the (timed_access var (K NONE) f);
+
+fun change_result var f = guarded_access var (SOME o f);
+fun change var f = change_result var (fn x => ((), f x));
+
+end;
--- a/src/Pure/IsaMakefile Tue Sep 29 14:25:42 2009 +1000
+++ b/src/Pure/IsaMakefile Tue Sep 29 14:26:33 2009 +1000
@@ -45,32 +45,33 @@
$(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/future.ML \
Concurrent/mailbox.ML Concurrent/par_list.ML \
Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML \
- Concurrent/synchronized.ML Concurrent/task_queue.ML General/alist.ML \
- General/antiquote.ML General/balanced_tree.ML General/basics.ML \
- General/binding.ML General/buffer.ML General/file.ML \
- General/graph.ML General/heap.ML General/integer.ML General/lazy.ML \
- General/long_name.ML General/markup.ML General/name_space.ML \
- General/ord_list.ML General/output.ML General/path.ML \
- General/position.ML General/pretty.ML General/print_mode.ML \
- General/properties.ML General/queue.ML General/same.ML \
- General/scan.ML General/secure.ML General/seq.ML General/source.ML \
- General/stack.ML General/symbol.ML General/symbol_pos.ML \
- General/table.ML General/url.ML General/xml.ML General/yxml.ML \
- Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML \
- Isar/class.ML Isar/class_target.ML Isar/code.ML Isar/constdefs.ML \
- Isar/context_rules.ML Isar/element.ML Isar/expression.ML \
- Isar/isar_cmd.ML Isar/isar_document.ML Isar/isar_syn.ML \
- Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML \
- Isar/locale.ML Isar/method.ML Isar/object_logic.ML Isar/obtain.ML \
- Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \
- Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \
- Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \
- Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML \
- Isar/skip_proof.ML Isar/spec_parse.ML Isar/specification.ML \
- Isar/theory_target.ML Isar/toplevel.ML Isar/value_parse.ML \
- ML/ml_antiquote.ML ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML \
- ML/ml_context.ML ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML \
- ML/ml_syntax.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
+ Concurrent/synchronized.ML Concurrent/synchronized_dummy.ML \
+ Concurrent/task_queue.ML General/alist.ML General/antiquote.ML \
+ General/balanced_tree.ML General/basics.ML General/binding.ML \
+ General/buffer.ML General/file.ML General/graph.ML General/heap.ML \
+ General/integer.ML General/lazy.ML General/long_name.ML \
+ General/markup.ML General/name_space.ML General/ord_list.ML \
+ General/output.ML General/path.ML General/position.ML \
+ General/pretty.ML General/print_mode.ML General/properties.ML \
+ General/queue.ML General/same.ML General/scan.ML General/secure.ML \
+ General/seq.ML General/source.ML General/stack.ML General/symbol.ML \
+ General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML \
+ General/yxml.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
+ Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \
+ Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \
+ Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML \
+ Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \
+ Isar/local_theory.ML Isar/locale.ML Isar/method.ML \
+ Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \
+ Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
+ Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \
+ Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \
+ Isar/rule_insts.ML Isar/runtime.ML Isar/skip_proof.ML \
+ Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML \
+ Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML \
+ ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML \
+ ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \
+ ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML \
Proof/extraction.ML Proof/proof_rewrite_rules.ML \
Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \
--- a/src/Pure/ML-Systems/thread_dummy.ML Tue Sep 29 14:25:42 2009 +1000
+++ b/src/Pure/ML-Systems/thread_dummy.ML Tue Sep 29 14:26:33 2009 +1000
@@ -35,6 +35,8 @@
datatype threadAttribute = EnableBroadcastInterrupt of bool | InterruptState of interruptState
and interruptState = InterruptDefer | InterruptSynch | InterruptAsynch | InterruptAsynchOnce;
+ fun unavailable () = fail ();
+
fun fork _ = fail ();
fun exit _ = fail ();
fun isActive _ = fail ();
--- a/src/Pure/ROOT.ML Tue Sep 29 14:25:42 2009 +1000
+++ b/src/Pure/ROOT.ML Tue Sep 29 14:26:33 2009 +1000
@@ -58,6 +58,7 @@
use "Concurrent/simple_thread.ML";
use "Concurrent/synchronized.ML";
+if Multithreading.available then () else use "Concurrent/synchronized_dummy.ML";
use "Concurrent/mailbox.ML";
use "Concurrent/task_queue.ML";
use "Concurrent/future.ML";
--- a/src/Pure/Thy/thm_deps.ML Tue Sep 29 14:25:42 2009 +1000
+++ b/src/Pure/Thy/thm_deps.ML Tue Sep 29 14:26:33 2009 +1000
@@ -40,7 +40,7 @@
path = "",
parents = parents};
in cons entry end;
- val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
+ val deps = Proofterm.fold_body_thms (add_dep o #2) (map Thm.proof_body_of thms) [];
in Present.display_graph (sort_wrt #ID deps) end;
@@ -56,7 +56,7 @@
|> sort_distinct (string_ord o pairself #1);
val tab = Proofterm.fold_body_thms
- (fn (name, prop, _) => name <> "" ? Symtab.insert_list (op =) (name, prop))
+ (fn (_, (name, prop, _)) => name <> "" ? Symtab.insert_list (op =) (name, prop))
(map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty;
fun is_unused (name, th) =
not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th));
--- a/src/Pure/proofterm.ML Tue Sep 29 14:25:42 2009 +1000
+++ b/src/Pure/proofterm.ML Tue Sep 29 14:26:33 2009 +1000
@@ -40,7 +40,8 @@
val proof_of: proof_body -> proof
val join_proof: proof_body future -> proof
val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
- val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
+ val fold_body_thms: (serial * (string * term * proof_body) -> 'a -> 'a) ->
+ proof_body list -> 'a -> 'a
val join_bodies: proof_body list -> unit
val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
@@ -109,7 +110,7 @@
val axm_proof: string -> term -> proof
val oracle_proof: string -> term -> oracle * proof
val promise_proof: theory -> serial -> term -> proof
- val fulfill_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
+ val fulfill_proof: theory -> serial -> (serial * proof_body) list -> proof_body -> proof_body
val thm_proof: theory -> string -> term list -> term ->
(serial * proof_body future) list -> proof_body -> pthm * proof
val get_name: term list -> term -> proof -> string
@@ -173,19 +174,16 @@
fun fold_body_thms f =
let
- fun app path (PBody {thms, ...}) =
+ fun app (PBody {thms, ...}) =
(Future.join_results (map (#3 o #2) thms);
thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
- if Inttab.defined path i then
- error ("Cyclic reference to theorem " ^ quote name)
- else if Inttab.defined seen i then (x, seen)
+ if Inttab.defined seen i then (x, seen)
else
let
val body' = Future.join body;
- val path' = Inttab.update (i, ()) path;
- val (x', seen') = app path' body' (x, Inttab.update (i, ()) seen);
- in (f (name, prop, body') x', seen') end));
- in fn bodies => fn x => #1 (fold (app Inttab.empty) bodies (x, Inttab.empty)) end;
+ val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
+ in (f (i, (name, prop, body')) x', seen') end));
+ in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
@@ -1281,12 +1279,16 @@
| _ => false));
in Promise (i, prop, map TVar (Term.add_tvars prop [])) end;
-fun fulfill_proof _ [] body0 = body0
- | fulfill_proof thy ps body0 =
+fun fulfill_proof _ _ [] body0 = body0
+ | fulfill_proof thy id ps body0 =
let
val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
- val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
- val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
+ val bodies = map snd ps;
+ val _ = fold_body_thms (fn (i, (name, _, _)) => fn () =>
+ if i = id then error ("Cyclic reference to theorem " ^ quote name)
+ else ()) bodies ();
+ val oracles = fold (fn PBody {oracles, ...} => merge_oracles oracles) bodies oracles0;
+ val thms = fold (fn PBody {thms, ...} => merge_thms thms) bodies thms0;
val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
fun fill (Promise (i, prop, Ts)) =
@@ -1298,10 +1300,10 @@
val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
in PBody {oracles = oracles, thms = thms, proof = proof} end;
-fun fulfill_proof_future _ [] body = Future.value body
- | fulfill_proof_future thy promises body =
+fun fulfill_proof_future _ _ [] body = Future.value body
+ | fulfill_proof_future thy id promises body =
Future.fork_deps (map snd promises) (fn () =>
- fulfill_proof thy (map (apsnd Future.join) promises) body);
+ fulfill_proof thy id (map (apsnd Future.join) promises) body);
(***** theorems *****)
@@ -1321,7 +1323,9 @@
else MinProof;
val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
- fun new_prf () = (serial (), name, prop, fulfill_proof_future thy promises body0);
+ fun new_prf () =
+ let val id = serial ()
+ in (id, name, prop, fulfill_proof_future thy id promises body0) end;
val (i, name, prop, body') =
(case strip_combt (fst (strip_combP prf)) of
(PThm (i, ((old_name, prop', NONE), body')), args') =>
--- a/src/Pure/thm.ML Tue Sep 29 14:25:42 2009 +1000
+++ b/src/Pure/thm.ML Tue Sep 29 14:26:33 2009 +1000
@@ -124,6 +124,13 @@
val hyps_of: thm -> term list
val no_prems: thm -> bool
val major_prem_of: thm -> term
+ val join_proofs: thm list -> unit
+ val proof_body_of: thm -> proof_body
+ val proof_of: thm -> proof
+ val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
+ val future: thm future -> cterm -> thm
+ val get_name: thm -> string
+ val put_name: string -> thm -> thm
val axiom: theory -> string -> thm
val axioms_of: theory -> (string * thm) list
val get_tags: thm -> Properties.T
@@ -142,13 +149,6 @@
val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
val rename_boundvars: term -> term -> thm -> thm
- val join_proofs: thm list -> unit
- val proof_body_of: thm -> proof_body
- val proof_of: thm -> proof
- val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
- val future: thm future -> cterm -> thm
- val get_name: thm -> string
- val put_name: string -> thm -> thm
val extern_oracles: theory -> xstring list
val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
end;
@@ -505,7 +505,7 @@
-(** derivations **)
+(** derivations and promised proofs **)
fun make_deriv promises oracles thms proof =
Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
@@ -536,6 +536,93 @@
fun deriv_rule0 prf = deriv_rule1 I (make_deriv [] [] [] prf);
+(* fulfilled proofs *)
+
+fun raw_body (Thm (Deriv {body, ...}, _)) = body;
+
+fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
+ Pt.fulfill_proof (Theory.deref thy_ref) ~1
+ (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
+and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
+
+val join_proofs = Pt.join_bodies o map fulfill_body;
+
+fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm);
+val proof_of = Pt.proof_of o proof_body_of;
+
+
+(* derivation status *)
+
+fun status_of (Thm (Deriv {promises, body}, _)) =
+ let
+ val ps = map (Future.peek o snd) promises;
+ val bodies = body ::
+ map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps;
+ val {oracle, unfinished, failed} = Pt.status_of bodies;
+ in
+ {oracle = oracle,
+ unfinished = unfinished orelse exists is_none ps,
+ failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
+ end;
+
+
+(* future rule *)
+
+fun future_result i orig_thy orig_shyps orig_prop raw_thm =
+ let
+ val _ = Theory.check_thy orig_thy;
+ val thm = strip_shyps (transfer orig_thy raw_thm);
+ val _ = Theory.check_thy orig_thy;
+ fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
+
+ val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
+ val _ = prop aconv orig_prop orelse err "bad prop";
+ val _ = null tpairs orelse err "bad tpairs";
+ val _ = null hyps orelse err "bad hyps";
+ val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
+ val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
+ val _ = fulfill_bodies (map #2 promises);
+ in thm end;
+
+fun future future_thm ct =
+ let
+ val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct;
+ val thy = Context.reject_draft (Theory.deref thy_ref);
+ val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
+
+ val i = serial ();
+ val future = future_thm |> Future.map (future_result i thy sorts prop);
+ in
+ Thm (make_deriv [(i, future)] [] [] (Pt.promise_proof thy i prop),
+ {thy_ref = thy_ref,
+ tags = [],
+ maxidx = maxidx,
+ shyps = sorts,
+ hyps = [],
+ tpairs = [],
+ prop = prop})
+ end;
+
+
+(* closed derivations with official name *)
+
+fun get_name thm =
+ Pt.get_name (hyps_of thm) (prop_of thm) (Pt.proof_of (raw_body thm));
+
+fun put_name name (thm as Thm (der, args)) =
+ let
+ val Deriv {promises, body} = der;
+ val {thy_ref, hyps, prop, tpairs, ...} = args;
+ val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
+
+ val ps = map (apsnd (Future.map proof_body_of)) promises;
+ val thy = Theory.deref thy_ref;
+ val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
+ val der' = make_deriv [] [] [pthm] proof;
+ val _ = Theory.check_thy thy;
+ in Thm (der', args) end;
+
+
(** Axioms **)
@@ -1610,96 +1697,6 @@
-(*** Future theorems -- proofs with promises ***)
-
-(* fulfilled proofs *)
-
-fun raw_body (Thm (Deriv {body, ...}, _)) = body;
-
-fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
- Pt.fulfill_proof (Theory.deref thy_ref)
- (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
-and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
-
-val join_proofs = Pt.join_bodies o map fulfill_body;
-
-fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm);
-val proof_of = Pt.proof_of o proof_body_of;
-
-
-(* derivation status *)
-
-fun status_of (Thm (Deriv {promises, body}, _)) =
- let
- val ps = map (Future.peek o snd) promises;
- val bodies = body ::
- map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps;
- val {oracle, unfinished, failed} = Pt.status_of bodies;
- in
- {oracle = oracle,
- unfinished = unfinished orelse exists is_none ps,
- failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
- end;
-
-
-(* future rule *)
-
-fun future_result i orig_thy orig_shyps orig_prop raw_thm =
- let
- val _ = Theory.check_thy orig_thy;
- val thm = strip_shyps (transfer orig_thy raw_thm);
- val _ = Theory.check_thy orig_thy;
- fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
-
- val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
- val _ = prop aconv orig_prop orelse err "bad prop";
- val _ = null tpairs orelse err "bad tpairs";
- val _ = null hyps orelse err "bad hyps";
- val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
- val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
- val _ = fulfill_bodies (map #2 promises);
- in thm end;
-
-fun future future_thm ct =
- let
- val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct;
- val thy = Context.reject_draft (Theory.deref thy_ref);
- val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
-
- val i = serial ();
- val future = future_thm |> Future.map (future_result i thy sorts prop);
- in
- Thm (make_deriv [(i, future)] [] [] (Pt.promise_proof thy i prop),
- {thy_ref = thy_ref,
- tags = [],
- maxidx = maxidx,
- shyps = sorts,
- hyps = [],
- tpairs = [],
- prop = prop})
- end;
-
-
-(* closed derivations with official name *)
-
-fun get_name thm =
- Pt.get_name (hyps_of thm) (prop_of thm) (Pt.proof_of (raw_body thm));
-
-fun put_name name (thm as Thm (der, args)) =
- let
- val Deriv {promises, body} = der;
- val {thy_ref, hyps, prop, tpairs, ...} = args;
- val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
-
- val ps = map (apsnd (Future.map proof_body_of)) promises;
- val thy = Theory.deref thy_ref;
- val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
- val der' = make_deriv [] [] [pthm] proof;
- val _ = Theory.check_thy thy;
- in Thm (der', args) end;
-
-
-
(*** Oracles ***)
(* oracle rule *)
--- a/src/Tools/coherent.ML Tue Sep 29 14:25:42 2009 +1000
+++ b/src/Tools/coherent.ML Tue Sep 29 14:26:33 2009 +1000
@@ -26,7 +26,7 @@
val setup: theory -> theory
end;
-functor CoherentFun(Data: COHERENT_DATA) : COHERENT =
+functor Coherent(Data: COHERENT_DATA) : COHERENT =
struct
(** misc tools **)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/cong_tac.ML Tue Sep 29 14:26:33 2009 +1000
@@ -0,0 +1,37 @@
+(* Title: Tools/cong_tac.ML
+ Author: Stefan Berghofer, TU Muenchen
+
+Congruence tactic based on explicit instantiation.
+*)
+
+signature CONG_TAC =
+sig
+ val cong_tac: thm -> int -> tactic
+end;
+
+structure Cong_Tac: CONG_TAC =
+struct
+
+fun cong_tac cong = CSUBGOAL (fn (cgoal, i) =>
+ let
+ val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
+ val goal = Thm.term_of cgoal;
+ in
+ (case Logic.strip_assums_concl goal of
+ _ $ (_ $ (f $ x) $ (g $ y)) =>
+ let
+ val cong' = Thm.lift_rule cgoal cong;
+ val _ $ (_ $ (f' $ x') $ (g' $ y')) =
+ Logic.strip_assums_concl (Thm.prop_of cong');
+ val ps = Logic.strip_params (Thm.concl_of cong');
+ val insts = [(f', f), (g', g), (x', x), (y', y)]
+ |> map (fn (t, u) => (cert (Term.head_of t), cert (Term.list_abs (ps, u))));
+ in
+ fn st => compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
+ handle THM _ => no_tac st
+ end
+ | _ => no_tac)
+ end);
+
+end;
+