fix example files
authorkuncar
Fri, 23 Mar 2012 14:26:09 +0100
changeset 47097 987cb55cac44
parent 47096 3ea48c19673e
child 47098 bab1c32c201e
fix example files
src/HOL/Quotient_Examples/Lift_Fun.thy
src/HOL/Quotient_Examples/Lift_RBT.thy
src/HOL/Quotient_Examples/Lift_Set.thy
src/HOL/ex/Executable_Relation.thy
--- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Mar 23 14:25:31 2012 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Mar 23 14:26:09 2012 +0100
@@ -6,7 +6,7 @@
 
 
 theory Lift_Fun
-imports Main
+imports Main "~~/src/HOL/Library/Quotient_Syntax"
 begin
 
 text {* This file is meant as a test case for features introduced in the changeset 2d8949268303. 
@@ -63,6 +63,44 @@
     by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc) 
 qed
 
+text {* Relator for 'a endofun. *}
+
+definition
+  endofun_rel' :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> bool" 
+where
+  "endofun_rel' R = (\<lambda>f g. (R ===> R) f g)"
+
+quotient_definition "endofun_rel :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun \<Rightarrow> bool" is
+  endofun_rel' done
+
+lemma endofun_quotient:
+assumes a: "Quotient R Abs Rep"
+shows "Quotient (endofun_rel R) (map_endofun Abs Rep) (map_endofun Rep Abs)"
+proof (intro QuotientI)
+  show "\<And>a. map_endofun Abs Rep (map_endofun Rep Abs a) = a"
+    by (metis (hide_lams, no_types) a abs_o_rep id_apply map_endofun.comp map_endofun.id o_eq_dest_lhs)
+next
+  show "\<And>a. endofun_rel R (map_endofun Rep Abs a) (map_endofun Rep Abs a)"
+  using fun_quotient[OF a a, THEN Quotient_rep_reflp]
+  unfolding endofun_rel_def map_endofun_def map_fun_def o_def map_endofun'_def endofun_rel'_def id_def 
+    by (metis (mono_tags) Quotient_endofun rep_abs_rsp)
+next
+  show "\<And>r s. endofun_rel R r s =
+          (endofun_rel R r r \<and>
+           endofun_rel R s s \<and> map_endofun Abs Rep r = map_endofun Abs Rep s)"
+    apply(auto simp add: endofun_rel_def endofun_rel'_def map_endofun_def map_endofun'_def)
+    using fun_quotient[OF a a,THEN Quotient_refl1]
+    apply metis
+    using fun_quotient[OF a a,THEN Quotient_refl2]
+    apply metis
+    using fun_quotient[OF a a, THEN Quotient_rel]
+    apply metis
+    using fun_quotient[OF a a, THEN Quotient_rel]
+    by (smt Quotient_endofun rep_abs_rsp)
+qed
+
+declare [[map endofun = (endofun_rel, endofun_quotient)]]
+
 quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" done
 
 term  endofun_id_id
--- a/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri Mar 23 14:25:31 2012 +0100
+++ b/src/HOL/Quotient_Examples/Lift_RBT.thy	Fri Mar 23 14:26:09 2012 +0100
@@ -6,15 +6,15 @@
 imports Main "~~/src/HOL/Library/RBT_Impl"
 begin
 
-definition inv :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
-  where [simp]: "inv R = (\<lambda>x y. R x \<and> x = y)"
-
 subsection {* Type definition *}
 
-quotient_type ('a, 'b) rbt = "('a\<Colon>linorder, 'b) RBT_Impl.rbt" / "inv is_rbt" morphisms impl_of RBT
-sorry
+typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
+  morphisms impl_of RBT
+proof -
+  have "RBT_Impl.Empty \<in> ?rbt" by simp
+  then show ?thesis ..
+qed
 
-(*
 lemma rbt_eq_iff:
   "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
   by (simp add: impl_of_inject)
@@ -30,15 +30,14 @@
 lemma RBT_impl_of [simp, code abstype]:
   "RBT (impl_of t) = t"
   by (simp add: impl_of_inverse)
-*)
 
 subsection {* Primitive operations *}
 
+setup_lifting type_definition_rbt
+
 quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup"
 by simp
 
-declare lookup_def[unfolded map_fun_def comp_def id_def, code]
-
 (* FIXME: quotient_definition at the moment requires that types variables match exactly,
 i.e., sort constraints must be annotated to the constant being lifted.
 But, it should be possible to infer the necessary sort constraints, making the explicit
@@ -53,67 +52,38 @@
 *)
 
 quotient_definition empty where "empty :: ('a\<Colon>linorder, 'b) rbt"
-is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)" done
-
-lemma impl_of_empty [code abstract]:
-  "impl_of empty = RBT_Impl.Empty"
-  by (simp add: empty_def RBT_inverse)
+is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)" by (simp add: empty_def)
 
 quotient_definition insert where "insert :: 'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.insert" done
-
-lemma impl_of_insert [code abstract]:
-  "impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)"
-  by (simp add: insert_def RBT_inverse)
+is "RBT_Impl.insert" by simp
 
 quotient_definition delete where "delete :: 'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.delete" done
-
-lemma impl_of_delete [code abstract]:
-  "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)"
-  by (simp add: delete_def RBT_inverse)
+is "RBT_Impl.delete" by simp
 
 (* FIXME: unnecessary type annotations *)
 quotient_definition "entries :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
-is "RBT_Impl.entries :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a \<times> 'b) list" done
-
-lemma [code]: "entries t = RBT_Impl.entries (impl_of t)"
-unfolding entries_def map_fun_def comp_def id_def ..
+is "RBT_Impl.entries :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a \<times> 'b) list" by simp
 
 (* FIXME: unnecessary type annotations *)
 quotient_definition "keys :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list"
-is "RBT_Impl.keys :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a list" done
+is "RBT_Impl.keys :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a list" by simp
 
 quotient_definition "bulkload :: ('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.bulkload" done
-
-lemma impl_of_bulkload [code abstract]:
-  "impl_of (bulkload xs) = RBT_Impl.bulkload xs"
-  by (simp add: bulkload_def RBT_inverse)
+is "RBT_Impl.bulkload" by simp
 
 quotient_definition "map_entry :: 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.map_entry" done
-
-lemma impl_of_map_entry [code abstract]:
-  "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)"
-  by (simp add: map_entry_def RBT_inverse)
+is "RBT_Impl.map_entry" by simp
 
 (* FIXME: unnecesary type annotations *)
 quotient_definition map where "map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
 is "RBT_Impl.map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a, 'b) RBT_Impl.rbt"
-done
-
-lemma impl_of_map [code abstract]:
-  "impl_of (map f t) = RBT_Impl.map f (impl_of t)"
-  by (simp add: map_def RBT_inverse)
+by simp
 
 (* FIXME: unnecessary type annotations *)
 quotient_definition fold where "fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" 
-is "RBT_Impl.fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'c \<Rightarrow> 'c" done
+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
 
-lemma [code]: "fold f t = RBT_Impl.fold f (impl_of t)"
-unfolding fold_def map_fun_def comp_def id_def ..
-
+export_code lookup empty insert delete entries keys bulkload map_entry map fold in SML
 
 subsection {* Derived operations *}
 
@@ -177,6 +147,10 @@
   "fold f t = List.fold (prod_case f) (entries t)"
   by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
 
+lemma impl_of_empty:
+  "impl_of empty = RBT_Impl.Empty"
+  by (simp add: empty_def RBT_inverse)
+
 lemma is_empty_empty [simp]:
   "is_empty t \<longleftrightarrow> t = empty"
   by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split)
@@ -198,5 +172,4 @@
   by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
 
 
-
 end
\ No newline at end of file
--- a/src/HOL/Quotient_Examples/Lift_Set.thy	Fri Mar 23 14:25:31 2012 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Fri Mar 23 14:26:09 2012 +0100
@@ -14,25 +14,7 @@
   morphisms member Set
   unfolding set_def by auto
 
-text {* Here is some ML setup that should eventually be incorporated in the typedef command. *}
-
-local_setup {* fn lthy =>
-  let
-    val quotients =
-      {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"},
-        equiv_rel = @{term "op ="}, equiv_thm = @{thm refl}}
-    val qty_full_name = @{type_name "set"}
-
-    fun qinfo phi = Quotient_Info.transform_quotients phi quotients
-  in
-    lthy
-    |> Local_Theory.declaration {syntax = false, pervasive = true}
-        (fn phi =>
-          Quotient_Info.update_quotients qty_full_name (qinfo phi) #>
-          Quotient_Info.update_abs_rep qty_full_name
-            (Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = @{term "member"}}))
-  end
-*}
+setup_lifting type_definition_set[unfolded set_def]
 
 text {* Now, we can employ quotient_definition to lift definitions. *}
 
@@ -51,5 +33,7 @@
 term "Lift_Set.insert"
 thm Lift_Set.insert_def
 
+export_code empty insert in SML
+
 end
 
--- a/src/HOL/ex/Executable_Relation.thy	Fri Mar 23 14:25:31 2012 +0100
+++ b/src/HOL/ex/Executable_Relation.thy	Fri Mar 23 14:26:09 2012 +0100
@@ -12,6 +12,7 @@
   "(x, y) : (rel_raw X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
 unfolding rel_raw_def by auto
 
+
 lemma Id_raw:
   "Id = rel_raw UNIV {}"
 unfolding rel_raw_def by auto
@@ -74,36 +75,34 @@
 
 lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"]
 
-definition rel :: "'a set => ('a * 'a) set => 'a rel"
-where
-  "rel X R = rel_of_set (rel_raw X R)"
+quotient_definition rel where "rel :: 'a set => ('a * 'a) set => 'a rel" is rel_raw done
 
 subsubsection {* Constant definitions on relations *}
 
 hide_const (open) converse rel_comp rtrancl Image
 
 quotient_definition member :: "'a * 'a => 'a rel => bool" where
-  "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool"
+  "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool" done
 
 quotient_definition converse :: "'a rel => 'a rel"
 where
-  "converse" is "Relation.converse :: ('a * 'a) set => ('a * 'a) set"
+  "converse" is "Relation.converse :: ('a * 'a) set => ('a * 'a) set" done
 
 quotient_definition union :: "'a rel => 'a rel => 'a rel"
 where
-  "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set"
+  "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
 
 quotient_definition rel_comp :: "'a rel => 'a rel => 'a rel"
 where
-  "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set"
+  "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
 
 quotient_definition rtrancl :: "'a rel => 'a rel"
 where
-  "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set"
+  "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set" done
 
 quotient_definition Image :: "'a rel => 'a set => 'a set"
 where
-  "Image" is "Relation.Image :: ('a * 'a) set => 'a set => 'a set"
+  "Image" is "Relation.Image :: ('a * 'a) set => 'a set => 'a set" done
 
 subsubsection {* Code generation *}
 
@@ -111,33 +110,27 @@
 
 lemma [code]:
   "member (x, y) (rel X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
-unfolding rel_def member_def
-by (simp add: member_raw)
+by (lifting member_raw)
 
 lemma [code]:
   "converse (rel X R) = rel X (R^-1)"
-unfolding rel_def converse_def
-by (simp add: converse_raw)
+by (lifting converse_raw)
 
 lemma [code]:
   "union (rel X R) (rel Y S) = rel (X Un Y) (R Un S)"
-unfolding rel_def union_def
-by (simp add: union_raw)
+by (lifting union_raw)
 
 lemma [code]:
    "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))"
-unfolding rel_def rel_comp_def
-by (simp add: rel_comp_raw)
+by (lifting rel_comp_raw)
 
 lemma [code]:
   "rtrancl (rel X R) = rel UNIV (R^+)"
-unfolding rel_def rtrancl_def
-by (simp add: rtrancl_raw)
+by (lifting rtrancl_raw)
 
 lemma [code]:
   "Image (rel X R) S = (X Int S) Un (R `` S)"
-unfolding rel_def Image_def
-by (simp add: Image_raw)
+by (lifting Image_raw)
 
 quickcheck_generator rel constructors: rel