# HG changeset patch # User Thomas Sewell # Date 1254198393 -36000 # Node ID 1476fe841023bec865e000a2ec4de582d768efa0 # Parent cd47afaf0d78d2b979a68ddca3de44ccace0779b# Parent f126e68d003d74128f3d7394052fea905a7bf42a Merge with isabelle dev changes. diff -r cd47afaf0d78 -r 1476fe841023 Admin/isatest/isatest-makedist --- 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" diff -r cd47afaf0d78 -r 1476fe841023 src/HOL/HOL.thy --- 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} diff -r cd47afaf0d78 -r 1476fe841023 src/HOL/IsaMakefile --- 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 \ diff -r cd47afaf0d78 -r 1476fe841023 src/HOL/Nominal/nominal_datatype.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); diff -r cd47afaf0d78 -r 1476fe841023 src/HOL/Nominal/nominal_permeq.ML --- 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 *) diff -r cd47afaf0d78 -r 1476fe841023 src/HOL/Tools/Datatype/datatype.ML --- 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; diff -r cd47afaf0d78 -r 1476fe841023 src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- 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, diff -r cd47afaf0d78 -r 1476fe841023 src/HOL/Tools/Datatype/datatype_aux.ML --- 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); diff -r cd47afaf0d78 -r 1476fe841023 src/HOL/Tools/Datatype/datatype_realizer.ML --- 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"] diff -r cd47afaf0d78 -r 1476fe841023 src/HOL/Tools/Datatype/datatype_rep_proofs.ML --- 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 diff -r cd47afaf0d78 -r 1476fe841023 src/HOL/Tools/Function/size.ML --- 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); diff -r cd47afaf0d78 -r 1476fe841023 src/HOL/Tools/TFL/casesplit.ML --- 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; (* diff -r cd47afaf0d78 -r 1476fe841023 src/HOL/Tools/old_primrec.ML --- 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; diff -r cd47afaf0d78 -r 1476fe841023 src/HOL/ex/Coherent.thy --- 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 diff -r cd47afaf0d78 -r 1476fe841023 src/Pure/Concurrent/future.ML --- 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 *) diff -r cd47afaf0d78 -r 1476fe841023 src/Pure/Concurrent/synchronized_dummy.ML --- /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; diff -r cd47afaf0d78 -r 1476fe841023 src/Pure/IsaMakefile --- 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 \ diff -r cd47afaf0d78 -r 1476fe841023 src/Pure/ML-Systems/thread_dummy.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 (); diff -r cd47afaf0d78 -r 1476fe841023 src/Pure/ROOT.ML --- 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"; diff -r cd47afaf0d78 -r 1476fe841023 src/Pure/Thy/thm_deps.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)); diff -r cd47afaf0d78 -r 1476fe841023 src/Pure/proofterm.ML --- 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') => diff -r cd47afaf0d78 -r 1476fe841023 src/Pure/thm.ML --- 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 *) diff -r cd47afaf0d78 -r 1476fe841023 src/Tools/coherent.ML --- 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 **) diff -r cd47afaf0d78 -r 1476fe841023 src/Tools/cong_tac.ML --- /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; +