1.1 --- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Mar 23 14:25:31 2012 +0100
     1.2 +++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Mar 23 14:26:09 2012 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  
     1.6  theory Lift_Fun
     1.7 -imports Main
     1.8 +imports Main "~~/src/HOL/Library/Quotient_Syntax"
     1.9  begin
    1.10  
    1.11  text {* This file is meant as a test case for features introduced in the changeset 2d8949268303. 
    1.12 @@ -63,6 +63,44 @@
    1.13      by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc) 
    1.14  qed
    1.15  
    1.16 +text {* Relator for 'a endofun. *}
    1.17 +
    1.18 +definition
    1.19 +  endofun_rel' :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> bool" 
    1.20 +where
    1.21 +  "endofun_rel' R = (\<lambda>f g. (R ===> R) f g)"
    1.22 +
    1.23 +quotient_definition "endofun_rel :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun \<Rightarrow> bool" is
    1.24 +  endofun_rel' done
    1.25 +
    1.26 +lemma endofun_quotient:
    1.27 +assumes a: "Quotient R Abs Rep"
    1.28 +shows "Quotient (endofun_rel R) (map_endofun Abs Rep) (map_endofun Rep Abs)"
    1.29 +proof (intro QuotientI)
    1.30 +  show "\<And>a. map_endofun Abs Rep (map_endofun Rep Abs a) = a"
    1.31 +    by (metis (hide_lams, no_types) a abs_o_rep id_apply map_endofun.comp map_endofun.id o_eq_dest_lhs)
    1.32 +next
    1.33 +  show "\<And>a. endofun_rel R (map_endofun Rep Abs a) (map_endofun Rep Abs a)"
    1.34 +  using fun_quotient[OF a a, THEN Quotient_rep_reflp]
    1.35 +  unfolding endofun_rel_def map_endofun_def map_fun_def o_def map_endofun'_def endofun_rel'_def id_def 
    1.36 +    by (metis (mono_tags) Quotient_endofun rep_abs_rsp)
    1.37 +next
    1.38 +  show "\<And>r s. endofun_rel R r s =
    1.39 +          (endofun_rel R r r \<and>
    1.40 +           endofun_rel R s s \<and> map_endofun Abs Rep r = map_endofun Abs Rep s)"
    1.41 +    apply(auto simp add: endofun_rel_def endofun_rel'_def map_endofun_def map_endofun'_def)
    1.42 +    using fun_quotient[OF a a,THEN Quotient_refl1]
    1.43 +    apply metis
    1.44 +    using fun_quotient[OF a a,THEN Quotient_refl2]
    1.45 +    apply metis
    1.46 +    using fun_quotient[OF a a, THEN Quotient_rel]
    1.47 +    apply metis
    1.48 +    using fun_quotient[OF a a, THEN Quotient_rel]
    1.49 +    by (smt Quotient_endofun rep_abs_rsp)
    1.50 +qed
    1.51 +
    1.52 +declare [[map endofun = (endofun_rel, endofun_quotient)]]
    1.53 +
    1.54  quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" done
    1.55  
    1.56  term  endofun_id_id

     2.1 --- a/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri Mar 23 14:25:31 2012 +0100
     2.2 +++ b/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri Mar 23 14:26:09 2012 +0100
     2.3 @@ -6,15 +6,15 @@
     2.4  imports Main "~~/src/HOL/Library/RBT_Impl"
     2.5  begin
     2.6  
     2.7 -definition inv :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
     2.8 -  where [simp]: "inv R = (\<lambda>x y. R x \<and> x = y)"
     2.9 -
    2.10  subsection {* Type definition *}
    2.11  
    2.12 -quotient_type ('a, 'b) rbt = "('a\<Colon>linorder, 'b) RBT_Impl.rbt" / "inv is_rbt" morphisms impl_of RBT
    2.13 -sorry
    2.14 +typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
    2.15 +  morphisms impl_of RBT
    2.16 +proof -
    2.17 +  have "RBT_Impl.Empty \<in> ?rbt" by simp
    2.18 +  then show ?thesis ..
    2.19 +qed
    2.20  
    2.21 -(*
    2.22  lemma rbt_eq_iff:
    2.23    "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
    2.24    by (simp add: impl_of_inject)
    2.25 @@ -30,15 +30,14 @@
    2.26  lemma RBT_impl_of [simp, code abstype]:
    2.27    "RBT (impl_of t) = t"
    2.28    by (simp add: impl_of_inverse)
    2.29 -*)
    2.30  
    2.31  subsection {* Primitive operations *}
    2.32  
    2.33 +setup_lifting type_definition_rbt
    2.34 +
    2.35  quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup"
    2.36  by simp
    2.37  
    2.38 -declare lookup_def[unfolded map_fun_def comp_def id_def, code]
    2.39 -
    2.40  (* FIXME: quotient_definition at the moment requires that types variables match exactly,
    2.41  i.e., sort constraints must be annotated to the constant being lifted.
    2.42  But, it should be possible to infer the necessary sort constraints, making the explicit
    2.43 @@ -53,67 +52,38 @@
    2.44  *)
    2.45  
    2.46  quotient_definition empty where "empty :: ('a\<Colon>linorder, 'b) rbt"
    2.47 -is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)" done
    2.48 -
    2.49 -lemma impl_of_empty [code abstract]:
    2.50 -  "impl_of empty = RBT_Impl.Empty"
    2.51 -  by (simp add: empty_def RBT_inverse)
    2.52 +is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)" by (simp add: empty_def)
    2.53  
    2.54  quotient_definition insert where "insert :: 'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
    2.55 -is "RBT_Impl.insert" done
    2.56 -
    2.57 -lemma impl_of_insert [code abstract]:
    2.58 -  "impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)"
    2.59 -  by (simp add: insert_def RBT_inverse)
    2.60 +is "RBT_Impl.insert" by simp
    2.61  
    2.62  quotient_definition delete where "delete :: 'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
    2.63 -is "RBT_Impl.delete" done
    2.64 -
    2.65 -lemma impl_of_delete [code abstract]:
    2.66 -  "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)"
    2.67 -  by (simp add: delete_def RBT_inverse)
    2.68 +is "RBT_Impl.delete" by simp
    2.69  
    2.70  (* FIXME: unnecessary type annotations *)
    2.71  quotient_definition "entries :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
    2.72 -is "RBT_Impl.entries :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a \<times> 'b) list" done
    2.73 -
    2.74 -lemma [code]: "entries t = RBT_Impl.entries (impl_of t)"
    2.75 -unfolding entries_def map_fun_def comp_def id_def ..
    2.76 +is "RBT_Impl.entries :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a \<times> 'b) list" by simp
    2.77  
    2.78  (* FIXME: unnecessary type annotations *)
    2.79  quotient_definition "keys :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list"
    2.80 -is "RBT_Impl.keys :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a list" done
    2.81 +is "RBT_Impl.keys :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a list" by simp
    2.82  
    2.83  quotient_definition "bulkload :: ('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt"
    2.84 -is "RBT_Impl.bulkload" done
    2.85 -
    2.86 -lemma impl_of_bulkload [code abstract]:
    2.87 -  "impl_of (bulkload xs) = RBT_Impl.bulkload xs"
    2.88 -  by (simp add: bulkload_def RBT_inverse)
    2.89 +is "RBT_Impl.bulkload" by simp
    2.90  
    2.91  quotient_definition "map_entry :: 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
    2.92 -is "RBT_Impl.map_entry" done
    2.93 -
    2.94 -lemma impl_of_map_entry [code abstract]:
    2.95 -  "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)"
    2.96 -  by (simp add: map_entry_def RBT_inverse)
    2.97 +is "RBT_Impl.map_entry" by simp
    2.98  
    2.99  (* FIXME: unnecesary type annotations *)
   2.100  quotient_definition map where "map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
   2.101  is "RBT_Impl.map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a, 'b) RBT_Impl.rbt"
   2.102 -done
   2.103 -
   2.104 -lemma impl_of_map [code abstract]:
   2.105 -  "impl_of (map f t) = RBT_Impl.map f (impl_of t)"
   2.106 -  by (simp add: map_def RBT_inverse)
   2.107 +by simp
   2.108  
   2.109  (* FIXME: unnecessary type annotations *)
   2.110  quotient_definition fold where "fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" 
   2.111 -is "RBT_Impl.fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'c \<Rightarrow> 'c" done
   2.112 +is "RBT_Impl.fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'c \<Rightarrow> 'c" by simp
   2.113  
   2.114 -lemma [code]: "fold f t = RBT_Impl.fold f (impl_of t)"
   2.115 -unfolding fold_def map_fun_def comp_def id_def ..
   2.116 -
   2.117 +export_code lookup empty insert delete entries keys bulkload map_entry map fold in SML
   2.118  
   2.119  subsection {* Derived operations *}
   2.120  
   2.121 @@ -177,6 +147,10 @@
   2.122    "fold f t = List.fold (prod_case f) (entries t)"
   2.123    by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
   2.124  
   2.125 +lemma impl_of_empty:
   2.126 +  "impl_of empty = RBT_Impl.Empty"
   2.127 +  by (simp add: empty_def RBT_inverse)
   2.128 +
   2.129  lemma is_empty_empty [simp]:
   2.130    "is_empty t \<longleftrightarrow> t = empty"
   2.131    by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split)
   2.132 @@ -198,5 +172,4 @@
   2.133    by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
   2.134  
   2.135  
   2.136 -
   2.137  end
   2.138 \ No newline at end of file

     3.1 --- a/src/HOL/Quotient_Examples/Lift_Set.thy	Fri Mar 23 14:25:31 2012 +0100
     3.2 +++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Fri Mar 23 14:26:09 2012 +0100
     3.3 @@ -14,25 +14,7 @@
     3.4    morphisms member Set
     3.5    unfolding set_def by auto
     3.6  
     3.7 -text {* Here is some ML setup that should eventually be incorporated in the typedef command. *}
     3.8 -
     3.9 -local_setup {* fn lthy =>
    3.10 -  let
    3.11 -    val quotients =
    3.12 -      {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"},
    3.13 -        equiv_rel = @{term "op ="}, equiv_thm = @{thm refl}}
    3.14 -    val qty_full_name = @{type_name "set"}
    3.15 -
    3.16 -    fun qinfo phi = Quotient_Info.transform_quotients phi quotients
    3.17 -  in
    3.18 -    lthy
    3.19 -    |> Local_Theory.declaration {syntax = false, pervasive = true}
    3.20 -        (fn phi =>
    3.21 -          Quotient_Info.update_quotients qty_full_name (qinfo phi) #>
    3.22 -          Quotient_Info.update_abs_rep qty_full_name
    3.23 -            (Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = @{term "member"}}))
    3.24 -  end
    3.25 -*}
    3.26 +setup_lifting type_definition_set[unfolded set_def]
    3.27  
    3.28  text {* Now, we can employ quotient_definition to lift definitions. *}
    3.29  
    3.30 @@ -51,5 +33,7 @@
    3.31  term "Lift_Set.insert"
    3.32  thm Lift_Set.insert_def
    3.33  
    3.34 +export_code empty insert in SML
    3.35 +
    3.36  end
    3.37  

     4.1 --- a/src/HOL/ex/Executable_Relation.thy	Fri Mar 23 14:25:31 2012 +0100
     4.2 +++ b/src/HOL/ex/Executable_Relation.thy	Fri Mar 23 14:26:09 2012 +0100
     4.3 @@ -12,6 +12,7 @@
     4.4    "(x, y) : (rel_raw X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
     4.5  unfolding rel_raw_def by auto
     4.6  
     4.7 +
     4.8  lemma Id_raw:
     4.9    "Id = rel_raw UNIV {}"
    4.10  unfolding rel_raw_def by auto
    4.11 @@ -74,36 +75,34 @@
    4.12  
    4.13  lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"]
    4.14  
    4.15 -definition rel :: "'a set => ('a * 'a) set => 'a rel"
    4.16 -where
    4.17 -  "rel X R = rel_of_set (rel_raw X R)"
    4.18 +quotient_definition rel where "rel :: 'a set => ('a * 'a) set => 'a rel" is rel_raw done
    4.19  
    4.20  subsubsection {* Constant definitions on relations *}
    4.21  
    4.22  hide_const (open) converse rel_comp rtrancl Image
    4.23  
    4.24  quotient_definition member :: "'a * 'a => 'a rel => bool" where
    4.25 -  "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool"
    4.26 +  "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool" done
    4.27  
    4.28  quotient_definition converse :: "'a rel => 'a rel"
    4.29  where
    4.30 -  "converse" is "Relation.converse :: ('a * 'a) set => ('a * 'a) set"
    4.31 +  "converse" is "Relation.converse :: ('a * 'a) set => ('a * 'a) set" done
    4.32  
    4.33  quotient_definition union :: "'a rel => 'a rel => 'a rel"
    4.34  where
    4.35 -  "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set"
    4.36 +  "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
    4.37  
    4.38  quotient_definition rel_comp :: "'a rel => 'a rel => 'a rel"
    4.39  where
    4.40 -  "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set"
    4.41 +  "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
    4.42  
    4.43  quotient_definition rtrancl :: "'a rel => 'a rel"
    4.44  where
    4.45 -  "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set"
    4.46 +  "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set" done
    4.47  
    4.48  quotient_definition Image :: "'a rel => 'a set => 'a set"
    4.49  where
    4.50 -  "Image" is "Relation.Image :: ('a * 'a) set => 'a set => 'a set"
    4.51 +  "Image" is "Relation.Image :: ('a * 'a) set => 'a set => 'a set" done
    4.52  
    4.53  subsubsection {* Code generation *}
    4.54  
    4.55 @@ -111,33 +110,27 @@
    4.56  
    4.57  lemma [code]:
    4.58    "member (x, y) (rel X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
    4.59 -unfolding rel_def member_def
    4.60 -by (simp add: member_raw)
    4.61 +by (lifting member_raw)
    4.62  
    4.63  lemma [code]:
    4.64    "converse (rel X R) = rel X (R^-1)"
    4.65 -unfolding rel_def converse_def
    4.66 -by (simp add: converse_raw)
    4.67 +by (lifting converse_raw)
    4.68  
    4.69  lemma [code]:
    4.70    "union (rel X R) (rel Y S) = rel (X Un Y) (R Un S)"
    4.71 -unfolding rel_def union_def
    4.72 -by (simp add: union_raw)
    4.73 +by (lifting union_raw)
    4.74  
    4.75  lemma [code]:
    4.76     "rel_comp (rel X R) (rel Y S) = rel (X Int Y) (Set.project (%(x, y). y : Y) R Un (Set.project (%(x, y). x : X) S Un R O S))"
    4.77 -unfolding rel_def rel_comp_def
    4.78 -by (simp add: rel_comp_raw)
    4.79 +by (lifting rel_comp_raw)
    4.80  
    4.81  lemma [code]:
    4.82    "rtrancl (rel X R) = rel UNIV (R^+)"
    4.83 -unfolding rel_def rtrancl_def
    4.84 -by (simp add: rtrancl_raw)
    4.85 +by (lifting rtrancl_raw)
    4.86  
    4.87  lemma [code]:
    4.88    "Image (rel X R) S = (X Int S) Un (R `` S)"
    4.89 -unfolding rel_def Image_def
    4.90 -by (simp add: Image_raw)
    4.91 +by (lifting Image_raw)
    4.92  
    4.93  quickcheck_generator rel constructors: rel
    4.94