# HG changeset patch # User Christian Urban # Date 1268629895 -3600 # Node ID 61671de8a5450cdcee405a06a96c004cb9d303e6 # Parent 45fb38a2e3f791c5e6b3cfd78a5eb303aebc0b6f synchronised with main hg-repository; used add_typedef_global in nominal_atoms diff -r 45fb38a2e3f7 -r 61671de8a545 Attic/Quot/quotient_def.ML --- a/Attic/Quot/quotient_def.ML Sun Mar 14 11:36:15 2010 +0100 +++ b/Attic/Quot/quotient_def.ML Mon Mar 15 06:11:35 2010 +0100 @@ -1,8 +1,7 @@ -(* Title: quotient_def.thy +(* Title: HOL/Tools/Quotient/quotient_def.thy Author: Cezary Kaliszyk and Christian Urban - Definitions for constants on quotient types. - +Definitions for constants on quotient types. *) signature QUOTIENT_DEF = diff -r 45fb38a2e3f7 -r 61671de8a545 Attic/Quot/quotient_info.ML --- a/Attic/Quot/quotient_info.ML Sun Mar 14 11:36:15 2010 +0100 +++ b/Attic/Quot/quotient_info.ML Mon Mar 15 06:11:35 2010 +0100 @@ -1,11 +1,9 @@ -(* Title: quotient_info.thy +(* Title: HOL/Tools/Quotient/quotient_info.thy Author: Cezary Kaliszyk and Christian Urban - Data slots for the quotient package. - +Data slots for the quotient package. *) - signature QUOTIENT_INFO = sig exception NotFound @@ -61,7 +59,7 @@ (type T = maps_info Symtab.table val empty = Symtab.empty val extend = I - val merge = Symtab.merge (K true)) + fun merge data = Symtab.merge (K true) data) fun maps_defined thy s = Symtab.defined (MapsData.get thy) s @@ -125,7 +123,7 @@ (type T = quotdata_info Symtab.table val empty = Symtab.empty val extend = I - val merge = Symtab.merge (K true)) + fun merge data = Symtab.merge (K true) data) fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} = {qtyp = Morphism.typ phi qtyp, @@ -195,7 +193,7 @@ fun qconsts_lookup thy t = let val (name, qty) = dest_Const t - fun matches x = + fun matches (x: qconsts_info) = let val (name', qty') = dest_Const (#qconst x); in @@ -284,10 +282,9 @@ OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of))) val _ = map improper_command - [(print_mapsinfo, "print_maps", "prints out all map functions"), + [(print_mapsinfo, "print_quotmaps", "prints out all map functions"), (print_quotinfo, "print_quotients", "prints out all quotients"), (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")] end; (* structure *) - diff -r 45fb38a2e3f7 -r 61671de8a545 Attic/Quot/quotient_tacs.ML --- a/Attic/Quot/quotient_tacs.ML Sun Mar 14 11:36:15 2010 +0100 +++ b/Attic/Quot/quotient_tacs.ML Mon Mar 15 06:11:35 2010 +0100 @@ -1,8 +1,8 @@ -(* Title: quotient_tacs.thy +(* Title: HOL/Tools/Quotient/quotient_tacs.thy Author: Cezary Kaliszyk and Christian Urban - Tactics for solving goal arising from lifting - theorems to quotient types. +Tactics for solving goal arising from lifting theorems to quotient +types. *) signature QUOTIENT_TACS = @@ -89,7 +89,7 @@ fun get_match_inst thy pat trm = let val univ = Unify.matchers thy [(pat, trm)] - val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *) + val SOME (env, _) = Seq.pull univ (* raises Bind, if no unifier *) (* FIXME fragile *) val tenv = Vartab.dest (Envir.term_env env) val tyenv = Vartab.dest (Envir.type_env env) in diff -r 45fb38a2e3f7 -r 61671de8a545 Attic/Quot/quotient_term.ML --- a/Attic/Quot/quotient_term.ML Sun Mar 14 11:36:15 2010 +0100 +++ b/Attic/Quot/quotient_term.ML Mon Mar 15 06:11:35 2010 +0100 @@ -1,8 +1,8 @@ -(* Title: quotient_term.thy +(* Title: HOL/Tools/Quotient/quotient_term.thy Author: Cezary Kaliszyk and Christian Urban - Constructs terms corresponding to goals from - lifting theorems to quotient types. +Constructs terms corresponding to goals from lifting theorems to +quotient types. *) signature QUOTIENT_TERM = @@ -265,7 +265,7 @@ | is_eq _ = false fun mk_rel_compose (trm1, trm2) = - Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2 + Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2 fun get_relmap ctxt s = let @@ -779,8 +779,4 @@ lift_aux t end - end; (* structure *) - - - diff -r 45fb38a2e3f7 -r 61671de8a545 Attic/Quot/quotient_typ.ML --- a/Attic/Quot/quotient_typ.ML Sun Mar 14 11:36:15 2010 +0100 +++ b/Attic/Quot/quotient_typ.ML Mon Mar 15 06:11:35 2010 +0100 @@ -7,6 +7,9 @@ signature QUOTIENT_TYPE = sig + val add_quotient_type: ((string list * binding * mixfix) * (typ * term)) * thm + -> Proof.context -> (thm * thm) * local_theory + val quotient_type: ((string list * binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state @@ -69,12 +72,13 @@ fun typedef_make (vs, qty_name, mx, rel, rty) lthy = let val typedef_tac = - EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}]) + EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}]) in - Typedef.add_typedef false NONE - (qty_name, vs, mx) - (typedef_term rel rty lthy) - NONE typedef_tac lthy + Local_Theory.theory_result + (Typedef.add_typedef_global false NONE + (qty_name, vs, mx) + (typedef_term rel rty lthy) + NONE typedef_tac) lthy end @@ -127,7 +131,7 @@ (* main function for constructing a quotient type *) -fun mk_quotient_type (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy = +fun add_quotient_type (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy = let (* generates the typedef *) val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy @@ -263,7 +267,7 @@ val goals = map (mk_goal o snd) quot_list fun after_qed thms lthy = - fold_map mk_quotient_type (quot_list ~~ thms) lthy |> snd + fold_map add_quotient_type (quot_list ~~ thms) lthy |> snd in theorem after_qed goals lthy end @@ -272,14 +276,13 @@ let fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy = let - (* new parsing with proper declaration *) val rty = Syntax.read_typ lthy rty_str val lthy1 = Variable.declare_typ rty lthy val rel = Syntax.parse_term lthy1 rel_str |> Syntax.type_constraint (rty --> rty --> @{typ bool}) |> Syntax.check_term lthy1 - val lthy2 = Variable.declare_term rel lthy1 + val lthy2 = Variable.declare_term rel lthy1 in (((vs, qty_name, mx), (rty, rel)), lthy2) end @@ -289,20 +292,17 @@ quotient_type spec' lthy' end -local - structure P = OuterParse; -in - val quotspec_parser = - P.and_list1 ((P.type_args -- P.binding) -- P.opt_infix -- - (P.$$$ "=" |-- P.typ) -- (P.$$$ "/" |-- P.term)) -end + OuterParse.and_list1 + ((OuterParse.type_args -- OuterParse.binding) -- + OuterParse.opt_mixfix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- + (OuterParse.$$$ "/" |-- OuterParse.term)) val _ = OuterKeyword.keyword "/" val _ = - OuterSyntax.local_theory_to_proof "quotient_type" - "quotient type definitions (require equivalence proofs)" - OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd) + OuterSyntax.local_theory_to_proof "quotient_type" + "quotient type definitions (require equivalence proofs)" + OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd) end; (* structure *) diff -r 45fb38a2e3f7 -r 61671de8a545 Nominal/nominal_atoms.ML --- a/Nominal/nominal_atoms.ML Sun Mar 14 11:36:15 2010 +0100 +++ b/Nominal/nominal_atoms.ML Mon Mar 15 06:11:35 2010 +0100 @@ -44,7 +44,7 @@ val set = atom_decl_set str; val tac = rtac @{thm exists_eq_simple_sort} 1; val ((full_tname, info as {type_definition, Rep_name, Abs_name, ...}), thy) = - Typedef.add_typedef false NONE (name, [], NoSyn) set NONE tac thy; + Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy; (* definition of atom and permute *) val newT = #abs_type info;