# HG changeset patch # User Christian Urban # Date 1261690099 -3600 # Node ID 5cf83fa5b36c9fafc58e6e43ae1c65fe67adcd92 # Parent d6407afb913c6ac28edad342f87b6e9e0f0a6e3c made the quotient_type definition more like typedef; now type variables need to be explicitly given diff -r d6407afb913c -r 5cf83fa5b36c Quot/Examples/AbsRepTest.thy --- a/Quot/Examples/AbsRepTest.thy Thu Dec 24 00:58:50 2009 +0100 +++ b/Quot/Examples/AbsRepTest.thy Thu Dec 24 22:28:19 2009 +0100 @@ -5,7 +5,14 @@ print_maps quotient_type - fset = "'a list" / "\(xs::'a list) ys. \e. e \ set xs \ e \ set ys" + 'a fset = "'a list" / "\xs ys. \e. e \ set xs \ e \ set ys" + apply(rule equivpI) + unfolding reflp_def symp_def transp_def + apply(auto) + done + +quotient_type + 'a foo = "('a * 'a) list" / "\(xs::('a * 'a) list) ys. \e. e \ set xs \ e \ set ys" apply(rule equivpI) unfolding reflp_def symp_def transp_def apply(auto) @@ -17,13 +24,11 @@ Quotient_Info.quotient_rules_get @{context} *} -fun - intrel :: "(nat \ nat) \ (nat \ nat) \ bool" -where - "intrel (x, y) (u, v) = (x + v = u + y)" - -quotient_type int = "nat \ nat" / intrel - sorry +quotient_type int = "nat \ nat" / "\(x, y) (u, v). x + v = u + (y::nat)" + apply(rule equivpI) + unfolding reflp_def symp_def transp_def + apply(auto) + done print_quotients @@ -32,11 +37,23 @@ *} ML {* -absrep_fun_chk absF @{context} (@{typ "(((nat * nat) list) * 'a) option"}, @{typ "((int fset) * 'a) option"}) +absrep_fun_chk absF @{context} + (@{typ "(('a * 'a) list) list"}, + @{typ "(('a * 'a) fset) fset"}) |> Syntax.string_of_term @{context} |> writeln *} +(* +ML {* +absrep_fun_chk absF @{context} + (@{typ "('a * 'a) list"}, + @{typ "'a foo"}) +|> Syntax.string_of_term @{context} +|> writeln +*} +*) + term "option_map (prod_fun (abs_fset \ map abs_int) id)" term "option_map (prod_fun (map rep_int \ rep_fset) id)" term "option_map (map rep_int \ rep_fset)" diff -r d6407afb913c -r 5cf83fa5b36c Quot/Examples/FSet.thy --- a/Quot/Examples/FSet.thy Thu Dec 24 00:58:50 2009 +0100 +++ b/Quot/Examples/FSet.thy Thu Dec 24 22:28:19 2009 +0100 @@ -23,7 +23,7 @@ done quotient_type - fset = "'a list" / "list_eq" + 'a fset = "'a list" / "list_eq" by (rule equivp_list_eq) quotient_definition @@ -280,7 +280,7 @@ apply (lifting list_induct_part) done -quotient_type fset2 = "'a list" / "list_eq" +quotient_type 'a fset2 = "'a list" / "list_eq" by (rule equivp_list_eq) quotient_definition diff -r d6407afb913c -r 5cf83fa5b36c Quot/Examples/FSet2.thy --- a/Quot/Examples/FSet2.thy Thu Dec 24 00:58:50 2009 +0100 +++ b/Quot/Examples/FSet2.thy Thu Dec 24 22:28:19 2009 +0100 @@ -21,7 +21,8 @@ unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def by (auto intro: list_eq.intros list_eq_refl) -quotient_type fset = "'a list" / "list_eq" +quotient_type + 'a fset = "'a list" / "list_eq" by (rule equivp_list_eq) quotient_definition diff -r d6407afb913c -r 5cf83fa5b36c Quot/Examples/FSet3.thy --- a/Quot/Examples/FSet3.thy Thu Dec 24 00:58:50 2009 +0100 +++ b/Quot/Examples/FSet3.thy Thu Dec 24 22:28:19 2009 +0100 @@ -15,7 +15,7 @@ (* FIXME-TODO: because of beta-reduction, one cannot give the *) (* FIXME-TODO: relation as a term or abbreviation *) quotient_type - fset = "'a list" / "list_eq" + 'a fset = "'a list" / "list_eq" by (rule list_eq_equivp) diff -r d6407afb913c -r 5cf83fa5b36c Quot/Examples/IntEx.thy --- a/Quot/Examples/IntEx.thy Thu Dec 24 00:58:50 2009 +0100 +++ b/Quot/Examples/IntEx.thy Thu Dec 24 22:28:19 2009 +0100 @@ -7,7 +7,8 @@ where "intrel (x, y) (u, v) = (x + v = u + y)" -quotient_type my_int = "nat \ nat" / intrel +quotient_type + my_int = "nat \ nat" / intrel apply(unfold equivp_def) apply(auto simp add: mem_def expand_fun_eq) done diff -r d6407afb913c -r 5cf83fa5b36c Quot/quotient_typ.ML --- a/Quot/quotient_typ.ML Thu Dec 24 00:58:50 2009 +0100 +++ b/Quot/quotient_typ.ML Thu Dec 24 22:28:19 2009 +0100 @@ -2,9 +2,10 @@ sig exception LIFT_MATCH of string - val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state - val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state - + val quotient_type: ((string list * binding * mixfix) * (typ * term)) list + -> Proof.context -> Proof.state + val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list + -> Proof.context -> Proof.state end; structure Quotient_Type: QUOTIENT_TYPE = @@ -60,18 +61,17 @@ end (* makes the new type definitions and proves non-emptyness*) -fun typedef_make (qty_name, mx, rel, rty) lthy = +fun typedef_make (vs, qty_name, mx, rel, rty) lthy = let val typedef_tac = EVERY1 [rtac @{thm exI}, rtac mem_def2, rtac @{thm exI}, rtac @{thm refl}] - val tfrees = map fst (Term.add_tfreesT rty []) in Local_Theory.theory_result (Typedef.add_typedef false NONE - (qty_name, tfrees, mx) + (qty_name, vs, mx) (typedef_term rel rty lthy) NONE typedef_tac) lthy end @@ -120,10 +120,10 @@ end (* main function for constructing a quotient type *) -fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy = +fun mk_typedef_main (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy = let (* generates the typedef *) - val ((qty_full_name, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy + val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy (* abs and rep functions from the typedef *) val Abs_ty = #abs_type typedef_info @@ -196,13 +196,12 @@ fun quotient_type_cmd spec lthy = let - fun parse_spec (((qty_str, mx), rty_str), rel_str) = + fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) = let - val qty_name = Binding.name qty_str val rty = Syntax.read_typ lthy rty_str val rel = Syntax.read_term lthy rel_str in - ((qty_name, mx), (rty, rel)) + ((vs, qty_name, mx), (rty, rel)) end in quotient_type (map parse_spec spec) lthy @@ -210,8 +209,8 @@ val quotspec_parser = OuterParse.and_list1 - (OuterParse.short_ident -- OuterParse.opt_infix -- - (OuterParse.$$$ "=" |-- OuterParse.typ) -- + ((OuterParse.type_args -- OuterParse.binding) -- + OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- (OuterParse.$$$ "/" |-- OuterParse.term)) val _ = OuterKeyword.keyword "/"