new package Lifting - initial commit
authorkuncar
Tue Apr 03 16:26:48 2012 +0200 (2012-04-03)
changeset 473089caab698dbe4
parent 47307 5e5ca36692b3
child 47309 9d02327ede56
new package Lifting - initial commit
etc/isar-keywords.el
src/HOL/IsaMakefile
src/HOL/Library/DAList.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Quotient_List.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Set.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/Lifting.thy
src/HOL/Metis_Examples/Clausification.thy
src/HOL/Quotient.thy
src/HOL/Quotient_Examples/DList.thy
src/HOL/Quotient_Examples/FSet.thy
src/HOL/Quotient_Examples/Lift_DList.thy
src/HOL/Quotient_Examples/Lift_Fun.thy
src/HOL/Quotient_Examples/Lift_RBT.thy
src/HOL/Quotient_Examples/Lift_Set.thy
src/HOL/Quotient_Examples/Quotient_Int.thy
src/HOL/Quotient_Examples/ROOT.ML
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_info.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Lifting/lifting_term.ML
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_info.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/Quotient/quotient_type.ML
src/HOL/ex/Executable_Relation.thy
     1.1 --- a/etc/isar-keywords.el	Tue Apr 03 14:09:37 2012 +0200
     1.2 +++ b/etc/isar-keywords.el	Tue Apr 03 16:26:48 2012 +0200
     1.3 @@ -190,7 +190,9 @@
     1.4      "print_orders"
     1.5      "print_quotconsts"
     1.6      "print_quotients"
     1.7 +    "print_quotientsQ3"
     1.8      "print_quotmaps"
     1.9 +    "print_quotmapsQ3"
    1.10      "print_rules"
    1.11      "print_simpset"
    1.12      "print_statement"
    1.13 @@ -403,7 +405,9 @@
    1.14      "print_orders"
    1.15      "print_quotconsts"
    1.16      "print_quotients"
    1.17 +    "print_quotientsQ3"
    1.18      "print_quotmaps"
    1.19 +    "print_quotmapsQ3"
    1.20      "print_rules"
    1.21      "print_simpset"
    1.22      "print_statement"
     2.1 --- a/src/HOL/IsaMakefile	Tue Apr 03 14:09:37 2012 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Tue Apr 03 16:26:48 2012 +0200
     2.3 @@ -281,6 +281,7 @@
     2.4    Hilbert_Choice.thy \
     2.5    Int.thy \
     2.6    Lazy_Sequence.thy \
     2.7 +  Lifting.thy \
     2.8    List.thy \
     2.9    Main.thy \
    2.10    Map.thy \
    2.11 @@ -315,6 +316,10 @@
    2.12    Tools/code_evaluation.ML \
    2.13    Tools/groebner.ML \
    2.14    Tools/int_arith.ML \
    2.15 +  Tools/Lifting/lifting_def.ML \
    2.16 +  Tools/Lifting/lifting_info.ML \
    2.17 +  Tools/Lifting/lifting_term.ML \
    2.18 +  Tools/Lifting/lifting_setup.ML \
    2.19    Tools/list_code.ML \
    2.20    Tools/list_to_set_comprehension.ML \
    2.21    Tools/nat_numeral_simprocs.ML \
    2.22 @@ -1495,7 +1500,7 @@
    2.23    Quotient_Examples/FSet.thy \
    2.24    Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \
    2.25    Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy \
    2.26 -  Quotient_Examples/Lift_Fun.thy 
    2.27 +  Quotient_Examples/Lift_Fun.thy Quotient_Examples/Lift_DList.thy
    2.28  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
    2.29  
    2.30  
     3.1 --- a/src/HOL/Library/DAList.thy	Tue Apr 03 14:09:37 2012 +0200
     3.2 +++ b/src/HOL/Library/DAList.thy	Tue Apr 03 16:26:48 2012 +0200
     3.3 @@ -39,33 +39,29 @@
     3.4  
     3.5  subsection {* Primitive operations *}
     3.6  
     3.7 -(* FIXME: improve quotient_definition so that type annotations on the right hand sides can be removed *) 
     3.8 -
     3.9 -quotient_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option"
    3.10 -where "lookup" is "map_of :: ('key * 'value) list \<Rightarrow> 'key \<Rightarrow> 'value option" ..
    3.11 +lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of  ..
    3.12  
    3.13 -quotient_definition empty :: "('key, 'value) alist"
    3.14 -where "empty" is "[] :: ('key * 'value) list" by simp
    3.15 +lift_definition empty :: "('key, 'value) alist" is "[]" by simp
    3.16  
    3.17 -quotient_definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    3.18 -where "update" is "AList.update :: 'key \<Rightarrow> 'value \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
    3.19 +lift_definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    3.20 +  is AList.update
    3.21  by (simp add: distinct_update)
    3.22  
    3.23  (* FIXME: we use an unoptimised delete operation. *)
    3.24 -quotient_definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    3.25 -where "delete" is "AList.delete :: 'key \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
    3.26 +lift_definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    3.27 +  is AList.delete
    3.28  by (simp add: distinct_delete)
    3.29  
    3.30 -quotient_definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    3.31 -where "map_entry" is "AList.map_entry :: 'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
    3.32 +lift_definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    3.33 +  is AList.map_entry
    3.34  by (simp add: distinct_map_entry)
    3.35  
    3.36 -quotient_definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    3.37 -where "filter" is "List.filter :: ('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
    3.38 +lift_definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
    3.39 +  is List.filter
    3.40  by (simp add: distinct_map_fst_filter)
    3.41  
    3.42 -quotient_definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
    3.43 -where "map_default" is "AList.map_default :: 'key => 'value => ('value => 'value) => ('key * 'value) list => ('key * 'value) list"
    3.44 +lift_definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
    3.45 +  is AList.map_default
    3.46  by (simp add: distinct_map_default)
    3.47  
    3.48  subsection {* Abstract operation properties *}
     4.1 --- a/src/HOL/Library/Multiset.thy	Tue Apr 03 14:09:37 2012 +0200
     4.2 +++ b/src/HOL/Library/Multiset.thy	Tue Apr 03 16:26:48 2012 +0200
     4.3 @@ -1111,14 +1111,12 @@
     4.4  
     4.5  text {* Operations on alists with distinct keys *}
     4.6  
     4.7 -quotient_definition join :: "('a \<Rightarrow> 'b \<times> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist" 
     4.8 -where
     4.9 -  "join" is "join_raw :: ('a \<Rightarrow> 'b \<times> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list"
    4.10 +lift_definition join :: "('a \<Rightarrow> 'b \<times> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist" 
    4.11 +is join_raw
    4.12  by (simp add: distinct_join_raw)
    4.13  
    4.14 -quotient_definition subtract_entries :: "('a, ('b :: minus)) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist"
    4.15 -where
    4.16 -  "subtract_entries" is "subtract_entries_raw :: ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list" 
    4.17 +lift_definition subtract_entries :: "('a, ('b :: minus)) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist"
    4.18 +is subtract_entries_raw 
    4.19  by (simp add: distinct_subtract_entries_raw)
    4.20  
    4.21  text {* Implementing multisets by means of association lists *}
     5.1 --- a/src/HOL/Library/Quotient_List.thy	Tue Apr 03 14:09:37 2012 +0200
     5.2 +++ b/src/HOL/Library/Quotient_List.thy	Tue Apr 03 16:26:48 2012 +0200
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      HOL/Library/Quotient_List.thy
     5.5 +(*  Title:      HOL/Library/Quotient3_List.thy
     5.6      Author:     Cezary Kaliszyk and Christian Urban
     5.7  *)
     5.8  
     5.9 @@ -56,63 +56,63 @@
    5.10    "equivp R \<Longrightarrow> equivp (list_all2 R)"
    5.11    by (blast intro: equivpI list_reflp list_symp list_transp elim: equivpE)
    5.12  
    5.13 -lemma list_quotient [quot_thm]:
    5.14 -  assumes "Quotient R Abs Rep"
    5.15 -  shows "Quotient (list_all2 R) (map Abs) (map Rep)"
    5.16 -proof (rule QuotientI)
    5.17 -  from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
    5.18 +lemma list_quotient3 [quot_thm]:
    5.19 +  assumes "Quotient3 R Abs Rep"
    5.20 +  shows "Quotient3 (list_all2 R) (map Abs) (map Rep)"
    5.21 +proof (rule Quotient3I)
    5.22 +  from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient3_abs_rep)
    5.23    then show "\<And>xs. map Abs (map Rep xs) = xs" by (simp add: comp_def)
    5.24  next
    5.25 -  from assms have "\<And>x y. R (Rep x) (Rep y) \<longleftrightarrow> x = y" by (rule Quotient_rel_rep)
    5.26 +  from assms have "\<And>x y. R (Rep x) (Rep y) \<longleftrightarrow> x = y" by (rule Quotient3_rel_rep)
    5.27    then show "\<And>xs. list_all2 R (map Rep xs) (map Rep xs)"
    5.28      by (simp add: list_all2_map1 list_all2_map2 list_all2_eq)
    5.29  next
    5.30    fix xs ys
    5.31 -  from assms have "\<And>x y. R x x \<and> R y y \<and> Abs x = Abs y \<longleftrightarrow> R x y" by (rule Quotient_rel)
    5.32 +  from assms have "\<And>x y. R x x \<and> R y y \<and> Abs x = Abs y \<longleftrightarrow> R x y" by (rule Quotient3_rel)
    5.33    then show "list_all2 R xs ys \<longleftrightarrow> list_all2 R xs xs \<and> list_all2 R ys ys \<and> map Abs xs = map Abs ys"
    5.34      by (induct xs ys rule: list_induct2') auto
    5.35  qed
    5.36  
    5.37 -declare [[map list = (list_all2, list_quotient)]]
    5.38 +declare [[mapQ3 list = (list_all2, list_quotient3)]]
    5.39  
    5.40  lemma cons_prs [quot_preserve]:
    5.41 -  assumes q: "Quotient R Abs Rep"
    5.42 +  assumes q: "Quotient3 R Abs Rep"
    5.43    shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
    5.44 -  by (auto simp add: fun_eq_iff comp_def Quotient_abs_rep [OF q])
    5.45 +  by (auto simp add: fun_eq_iff comp_def Quotient3_abs_rep [OF q])
    5.46  
    5.47  lemma cons_rsp [quot_respect]:
    5.48 -  assumes q: "Quotient R Abs Rep"
    5.49 +  assumes q: "Quotient3 R Abs Rep"
    5.50    shows "(R ===> list_all2 R ===> list_all2 R) (op #) (op #)"
    5.51    by auto
    5.52  
    5.53  lemma nil_prs [quot_preserve]:
    5.54 -  assumes q: "Quotient R Abs Rep"
    5.55 +  assumes q: "Quotient3 R Abs Rep"
    5.56    shows "map Abs [] = []"
    5.57    by simp
    5.58  
    5.59  lemma nil_rsp [quot_respect]:
    5.60 -  assumes q: "Quotient R Abs Rep"
    5.61 +  assumes q: "Quotient3 R Abs Rep"
    5.62    shows "list_all2 R [] []"
    5.63    by simp
    5.64  
    5.65  lemma map_prs_aux:
    5.66 -  assumes a: "Quotient R1 abs1 rep1"
    5.67 -  and     b: "Quotient R2 abs2 rep2"
    5.68 +  assumes a: "Quotient3 R1 abs1 rep1"
    5.69 +  and     b: "Quotient3 R2 abs2 rep2"
    5.70    shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"
    5.71    by (induct l)
    5.72 -     (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
    5.73 +     (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b])
    5.74  
    5.75  lemma map_prs [quot_preserve]:
    5.76 -  assumes a: "Quotient R1 abs1 rep1"
    5.77 -  and     b: "Quotient R2 abs2 rep2"
    5.78 +  assumes a: "Quotient3 R1 abs1 rep1"
    5.79 +  and     b: "Quotient3 R2 abs2 rep2"
    5.80    shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
    5.81    and   "((abs1 ---> id) ---> map rep1 ---> id) map = map"
    5.82    by (simp_all only: fun_eq_iff map_prs_aux[OF a b] comp_def)
    5.83 -    (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
    5.84 +    (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b])
    5.85  
    5.86  lemma map_rsp [quot_respect]:
    5.87 -  assumes q1: "Quotient R1 Abs1 Rep1"
    5.88 -  and     q2: "Quotient R2 Abs2 Rep2"
    5.89 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    5.90 +  and     q2: "Quotient3 R2 Abs2 Rep2"
    5.91    shows "((R1 ===> R2) ===> (list_all2 R1) ===> list_all2 R2) map map"
    5.92    and   "((R1 ===> op =) ===> (list_all2 R1) ===> op =) map map"
    5.93    apply (simp_all add: fun_rel_def)
    5.94 @@ -124,35 +124,35 @@
    5.95    done
    5.96  
    5.97  lemma foldr_prs_aux:
    5.98 -  assumes a: "Quotient R1 abs1 rep1"
    5.99 -  and     b: "Quotient R2 abs2 rep2"
   5.100 +  assumes a: "Quotient3 R1 abs1 rep1"
   5.101 +  and     b: "Quotient3 R2 abs2 rep2"
   5.102    shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
   5.103 -  by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
   5.104 +  by (induct l) (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b])
   5.105  
   5.106  lemma foldr_prs [quot_preserve]:
   5.107 -  assumes a: "Quotient R1 abs1 rep1"
   5.108 -  and     b: "Quotient R2 abs2 rep2"
   5.109 +  assumes a: "Quotient3 R1 abs1 rep1"
   5.110 +  and     b: "Quotient3 R2 abs2 rep2"
   5.111    shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
   5.112    apply (simp add: fun_eq_iff)
   5.113    by (simp only: fun_eq_iff foldr_prs_aux[OF a b])
   5.114       (simp)
   5.115  
   5.116  lemma foldl_prs_aux:
   5.117 -  assumes a: "Quotient R1 abs1 rep1"
   5.118 -  and     b: "Quotient R2 abs2 rep2"
   5.119 +  assumes a: "Quotient3 R1 abs1 rep1"
   5.120 +  and     b: "Quotient3 R2 abs2 rep2"
   5.121    shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
   5.122 -  by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
   5.123 +  by (induct l arbitrary:e) (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b])
   5.124  
   5.125  lemma foldl_prs [quot_preserve]:
   5.126 -  assumes a: "Quotient R1 abs1 rep1"
   5.127 -  and     b: "Quotient R2 abs2 rep2"
   5.128 +  assumes a: "Quotient3 R1 abs1 rep1"
   5.129 +  and     b: "Quotient3 R2 abs2 rep2"
   5.130    shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
   5.131    by (simp add: fun_eq_iff foldl_prs_aux [OF a b])
   5.132  
   5.133  (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *)
   5.134  lemma foldl_rsp[quot_respect]:
   5.135 -  assumes q1: "Quotient R1 Abs1 Rep1"
   5.136 -  and     q2: "Quotient R2 Abs2 Rep2"
   5.137 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
   5.138 +  and     q2: "Quotient3 R2 Abs2 Rep2"
   5.139    shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_all2 R2 ===> R1) foldl foldl"
   5.140    apply(auto simp add: fun_rel_def)
   5.141    apply (erule_tac P="R1 xa ya" in rev_mp)
   5.142 @@ -162,8 +162,8 @@
   5.143    done
   5.144  
   5.145  lemma foldr_rsp[quot_respect]:
   5.146 -  assumes q1: "Quotient R1 Abs1 Rep1"
   5.147 -  and     q2: "Quotient R2 Abs2 Rep2"
   5.148 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
   5.149 +  and     q2: "Quotient3 R2 Abs2 Rep2"
   5.150    shows "((R1 ===> R2 ===> R2) ===> list_all2 R1 ===> R2 ===> R2) foldr foldr"
   5.151    apply (auto simp add: fun_rel_def)
   5.152    apply (erule list_all2_induct, simp_all)
   5.153 @@ -183,18 +183,18 @@
   5.154    by (simp add: list_all2_rsp fun_rel_def)
   5.155  
   5.156  lemma [quot_preserve]:
   5.157 -  assumes a: "Quotient R abs1 rep1"
   5.158 +  assumes a: "Quotient3 R abs1 rep1"
   5.159    shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_all2 = list_all2"
   5.160    apply (simp add: fun_eq_iff)
   5.161    apply clarify
   5.162    apply (induct_tac xa xb rule: list_induct2')
   5.163 -  apply (simp_all add: Quotient_abs_rep[OF a])
   5.164 +  apply (simp_all add: Quotient3_abs_rep[OF a])
   5.165    done
   5.166  
   5.167  lemma [quot_preserve]:
   5.168 -  assumes a: "Quotient R abs1 rep1"
   5.169 +  assumes a: "Quotient3 R abs1 rep1"
   5.170    shows "(list_all2 ((rep1 ---> rep1 ---> id) R) l m) = (l = m)"
   5.171 -  by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a])
   5.172 +  by (induct l m rule: list_induct2') (simp_all add: Quotient3_rel_rep[OF a])
   5.173  
   5.174  lemma list_all2_find_element:
   5.175    assumes a: "x \<in> set a"
   5.176 @@ -207,4 +207,48 @@
   5.177    shows "list_all2 R x x"
   5.178    by (induct x) (auto simp add: a)
   5.179  
   5.180 +lemma list_quotient:
   5.181 +  assumes "Quotient R Abs Rep T"
   5.182 +  shows "Quotient (list_all2 R) (List.map Abs) (List.map Rep) (list_all2 T)"
   5.183 +proof (rule QuotientI)
   5.184 +  from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
   5.185 +  then show "\<And>xs. List.map Abs (List.map Rep xs) = xs" by (simp add: comp_def)
   5.186 +next
   5.187 +  from assms have "\<And>x y. R (Rep x) (Rep y) \<longleftrightarrow> x = y" by (rule Quotient_rel_rep)
   5.188 +  then show "\<And>xs. list_all2 R (List.map Rep xs) (List.map Rep xs)"
   5.189 +    by (simp add: list_all2_map1 list_all2_map2 list_all2_eq)
   5.190 +next
   5.191 +  fix xs ys
   5.192 +  from assms have "\<And>x y. R x x \<and> R y y \<and> Abs x = Abs y \<longleftrightarrow> R x y" by (rule Quotient_rel)
   5.193 +  then show "list_all2 R xs ys \<longleftrightarrow> list_all2 R xs xs \<and> list_all2 R ys ys \<and> List.map Abs xs = List.map Abs ys"
   5.194 +    by (induct xs ys rule: list_induct2') auto
   5.195 +next
   5.196 +  {
   5.197 +    fix l1 l2
   5.198 +    have "List.length l1 = List.length l2 \<Longrightarrow>
   5.199 +         (\<forall>(x, y)\<in>set (zip l1 l1). R x y) = (\<forall>(x, y)\<in>set (zip l1 l2). R x x)"
   5.200 +     by (induction rule: list_induct2) auto
   5.201 +  } note x = this
   5.202 +  {
   5.203 +    fix f g
   5.204 +    have "list_all2 (\<lambda>x y. f x y \<and> g x y) = (\<lambda> x y. list_all2 f x y \<and> list_all2 g x y)"
   5.205 +      by (intro ext) (auto simp add: list_all2_def)
   5.206 +  } note list_all2_conj = this
   5.207 +  from assms have t: "T = (\<lambda>x y. R x x \<and> Abs x = y)" by (rule Quotient_cr_rel)
   5.208 +  show "list_all2 T = (\<lambda>x y. list_all2 R x x \<and> List.map Abs x = y)" 
   5.209 +    apply (simp add: t list_all2_conj[symmetric])
   5.210 +    apply (rule sym) 
   5.211 +    apply (simp add: list_all2_conj) 
   5.212 +    apply(intro ext) 
   5.213 +    apply (intro rev_conj_cong)
   5.214 +      unfolding list_all2_def apply (metis List.list_all2_eq list_all2_def list_all2_map1)
   5.215 +    apply (drule conjunct1) 
   5.216 +    apply (intro conj_cong) 
   5.217 +      apply simp 
   5.218 +    apply(simp add: x)
   5.219 +  done
   5.220 +qed
   5.221 +
   5.222 +declare [[map list = (list_all2, list_quotient)]]
   5.223 +
   5.224  end
     6.1 --- a/src/HOL/Library/Quotient_Option.thy	Tue Apr 03 14:09:37 2012 +0200
     6.2 +++ b/src/HOL/Library/Quotient_Option.thy	Tue Apr 03 16:26:48 2012 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:      HOL/Library/Quotient_Option.thy
     6.5 +(*  Title:      HOL/Library/Quotient3_Option.thy
     6.6      Author:     Cezary Kaliszyk and Christian Urban
     6.7  *)
     6.8  
     6.9 @@ -55,36 +55,36 @@
    6.10    by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE)
    6.11  
    6.12  lemma option_quotient [quot_thm]:
    6.13 -  assumes "Quotient R Abs Rep"
    6.14 -  shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
    6.15 -  apply (rule QuotientI)
    6.16 -  apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient_abs_rep [OF assms] Quotient_rel_rep [OF assms])
    6.17 -  using Quotient_rel [OF assms]
    6.18 +  assumes "Quotient3 R Abs Rep"
    6.19 +  shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)"
    6.20 +  apply (rule Quotient3I)
    6.21 +  apply (simp_all add: Option.map.compositionality comp_def Option.map.identity option_rel_eq option_rel_map1 option_rel_map2 Quotient3_abs_rep [OF assms] Quotient3_rel_rep [OF assms])
    6.22 +  using Quotient3_rel [OF assms]
    6.23    apply (simp add: option_rel_unfold split: option.split)
    6.24    done
    6.25  
    6.26 -declare [[map option = (option_rel, option_quotient)]]
    6.27 +declare [[mapQ3 option = (option_rel, option_quotient)]]
    6.28  
    6.29  lemma option_None_rsp [quot_respect]:
    6.30 -  assumes q: "Quotient R Abs Rep"
    6.31 +  assumes q: "Quotient3 R Abs Rep"
    6.32    shows "option_rel R None None"
    6.33    by simp
    6.34  
    6.35  lemma option_Some_rsp [quot_respect]:
    6.36 -  assumes q: "Quotient R Abs Rep"
    6.37 +  assumes q: "Quotient3 R Abs Rep"
    6.38    shows "(R ===> option_rel R) Some Some"
    6.39    by auto
    6.40  
    6.41  lemma option_None_prs [quot_preserve]:
    6.42 -  assumes q: "Quotient R Abs Rep"
    6.43 +  assumes q: "Quotient3 R Abs Rep"
    6.44    shows "Option.map Abs None = None"
    6.45    by simp
    6.46  
    6.47  lemma option_Some_prs [quot_preserve]:
    6.48 -  assumes q: "Quotient R Abs Rep"
    6.49 +  assumes q: "Quotient3 R Abs Rep"
    6.50    shows "(Rep ---> Option.map Abs) Some = Some"
    6.51    apply(simp add: fun_eq_iff)
    6.52 -  apply(simp add: Quotient_abs_rep[OF q])
    6.53 +  apply(simp add: Quotient3_abs_rep[OF q])
    6.54    done
    6.55  
    6.56  end
     7.1 --- a/src/HOL/Library/Quotient_Product.thy	Tue Apr 03 14:09:37 2012 +0200
     7.2 +++ b/src/HOL/Library/Quotient_Product.thy	Tue Apr 03 16:26:48 2012 +0200
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  Title:      HOL/Library/Quotient_Product.thy
     7.5 +(*  Title:      HOL/Library/Quotient3_Product.thy
     7.6      Author:     Cezary Kaliszyk and Christian Urban
     7.7  *)
     7.8  
     7.9 @@ -32,56 +32,56 @@
    7.10    using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE)
    7.11  
    7.12  lemma prod_quotient [quot_thm]:
    7.13 -  assumes "Quotient R1 Abs1 Rep1"
    7.14 -  assumes "Quotient R2 Abs2 Rep2"
    7.15 -  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
    7.16 -  apply (rule QuotientI)
    7.17 +  assumes "Quotient3 R1 Abs1 Rep1"
    7.18 +  assumes "Quotient3 R2 Abs2 Rep2"
    7.19 +  shows "Quotient3 (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
    7.20 +  apply (rule Quotient3I)
    7.21    apply (simp add: map_pair.compositionality comp_def map_pair.identity
    7.22 -     Quotient_abs_rep [OF assms(1)] Quotient_abs_rep [OF assms(2)])
    7.23 -  apply (simp add: split_paired_all Quotient_rel_rep [OF assms(1)] Quotient_rel_rep [OF assms(2)])
    7.24 -  using Quotient_rel [OF assms(1)] Quotient_rel [OF assms(2)]
    7.25 +     Quotient3_abs_rep [OF assms(1)] Quotient3_abs_rep [OF assms(2)])
    7.26 +  apply (simp add: split_paired_all Quotient3_rel_rep [OF assms(1)] Quotient3_rel_rep [OF assms(2)])
    7.27 +  using Quotient3_rel [OF assms(1)] Quotient3_rel [OF assms(2)]
    7.28    apply (auto simp add: split_paired_all)
    7.29    done
    7.30  
    7.31 -declare [[map prod = (prod_rel, prod_quotient)]]
    7.32 +declare [[mapQ3 prod = (prod_rel, prod_quotient)]]
    7.33  
    7.34  lemma Pair_rsp [quot_respect]:
    7.35 -  assumes q1: "Quotient R1 Abs1 Rep1"
    7.36 -  assumes q2: "Quotient R2 Abs2 Rep2"
    7.37 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    7.38 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    7.39    shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
    7.40    by (auto simp add: prod_rel_def)
    7.41  
    7.42  lemma Pair_prs [quot_preserve]:
    7.43 -  assumes q1: "Quotient R1 Abs1 Rep1"
    7.44 -  assumes q2: "Quotient R2 Abs2 Rep2"
    7.45 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    7.46 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    7.47    shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair"
    7.48    apply(simp add: fun_eq_iff)
    7.49 -  apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    7.50 +  apply(simp add: Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
    7.51    done
    7.52  
    7.53  lemma fst_rsp [quot_respect]:
    7.54 -  assumes "Quotient R1 Abs1 Rep1"
    7.55 -  assumes "Quotient R2 Abs2 Rep2"
    7.56 +  assumes "Quotient3 R1 Abs1 Rep1"
    7.57 +  assumes "Quotient3 R2 Abs2 Rep2"
    7.58    shows "(prod_rel R1 R2 ===> R1) fst fst"
    7.59    by auto
    7.60  
    7.61  lemma fst_prs [quot_preserve]:
    7.62 -  assumes q1: "Quotient R1 Abs1 Rep1"
    7.63 -  assumes q2: "Quotient R2 Abs2 Rep2"
    7.64 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    7.65 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    7.66    shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst"
    7.67 -  by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
    7.68 +  by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1])
    7.69  
    7.70  lemma snd_rsp [quot_respect]:
    7.71 -  assumes "Quotient R1 Abs1 Rep1"
    7.72 -  assumes "Quotient R2 Abs2 Rep2"
    7.73 +  assumes "Quotient3 R1 Abs1 Rep1"
    7.74 +  assumes "Quotient3 R2 Abs2 Rep2"
    7.75    shows "(prod_rel R1 R2 ===> R2) snd snd"
    7.76    by auto
    7.77  
    7.78  lemma snd_prs [quot_preserve]:
    7.79 -  assumes q1: "Quotient R1 Abs1 Rep1"
    7.80 -  assumes q2: "Quotient R2 Abs2 Rep2"
    7.81 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    7.82 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    7.83    shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd"
    7.84 -  by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
    7.85 +  by (simp add: fun_eq_iff Quotient3_abs_rep[OF q2])
    7.86  
    7.87  lemma split_rsp [quot_respect]:
    7.88    shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
    7.89 @@ -89,10 +89,10 @@
    7.90    by auto
    7.91  
    7.92  lemma split_prs [quot_preserve]:
    7.93 -  assumes q1: "Quotient R1 Abs1 Rep1"
    7.94 -  and     q2: "Quotient R2 Abs2 Rep2"
    7.95 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    7.96 +  and     q2: "Quotient3 R2 Abs2 Rep2"
    7.97    shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split"
    7.98 -  by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    7.99 +  by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
   7.100  
   7.101  lemma [quot_respect]:
   7.102    shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
   7.103 @@ -100,11 +100,11 @@
   7.104    by (auto simp add: fun_rel_def)
   7.105  
   7.106  lemma [quot_preserve]:
   7.107 -  assumes q1: "Quotient R1 abs1 rep1"
   7.108 -  and     q2: "Quotient R2 abs2 rep2"
   7.109 +  assumes q1: "Quotient3 R1 abs1 rep1"
   7.110 +  and     q2: "Quotient3 R2 abs2 rep2"
   7.111    shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
   7.112    map_pair rep1 rep2 ---> map_pair rep1 rep2 ---> id) prod_rel = prod_rel"
   7.113 -  by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   7.114 +  by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
   7.115  
   7.116  lemma [quot_preserve]:
   7.117    shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2)
     8.1 --- a/src/HOL/Library/Quotient_Set.thy	Tue Apr 03 14:09:37 2012 +0200
     8.2 +++ b/src/HOL/Library/Quotient_Set.thy	Tue Apr 03 16:26:48 2012 +0200
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      HOL/Library/Quotient_Set.thy
     8.5 +(*  Title:      HOL/Library/Quotient3_Set.thy
     8.6      Author:     Cezary Kaliszyk and Christian Urban
     8.7  *)
     8.8  
     8.9 @@ -9,77 +9,77 @@
    8.10  begin
    8.11  
    8.12  lemma set_quotient [quot_thm]:
    8.13 -  assumes "Quotient R Abs Rep"
    8.14 -  shows "Quotient (set_rel R) (vimage Rep) (vimage Abs)"
    8.15 -proof (rule QuotientI)
    8.16 -  from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
    8.17 +  assumes "Quotient3 R Abs Rep"
    8.18 +  shows "Quotient3 (set_rel R) (vimage Rep) (vimage Abs)"
    8.19 +proof (rule Quotient3I)
    8.20 +  from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient3_abs_rep)
    8.21    then show "\<And>xs. Rep -` (Abs -` xs) = xs"
    8.22      unfolding vimage_def by auto
    8.23  next
    8.24    show "\<And>xs. set_rel R (Abs -` xs) (Abs -` xs)"
    8.25      unfolding set_rel_def vimage_def
    8.26 -    by auto (metis Quotient_rel_abs[OF assms])+
    8.27 +    by auto (metis Quotient3_rel_abs[OF assms])+
    8.28  next
    8.29    fix r s
    8.30    show "set_rel R r s = (set_rel R r r \<and> set_rel R s s \<and> Rep -` r = Rep -` s)"
    8.31      unfolding set_rel_def vimage_def set_eq_iff
    8.32 -    by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+
    8.33 +    by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient3_def])+
    8.34  qed
    8.35  
    8.36 -declare [[map set = (set_rel, set_quotient)]]
    8.37 +declare [[mapQ3 set = (set_rel, set_quotient)]]
    8.38  
    8.39  lemma empty_set_rsp[quot_respect]:
    8.40    "set_rel R {} {}"
    8.41    unfolding set_rel_def by simp
    8.42  
    8.43  lemma collect_rsp[quot_respect]:
    8.44 -  assumes "Quotient R Abs Rep"
    8.45 +  assumes "Quotient3 R Abs Rep"
    8.46    shows "((R ===> op =) ===> set_rel R) Collect Collect"
    8.47    by (intro fun_relI) (simp add: fun_rel_def set_rel_def)
    8.48  
    8.49  lemma collect_prs[quot_preserve]:
    8.50 -  assumes "Quotient R Abs Rep"
    8.51 +  assumes "Quotient3 R Abs Rep"
    8.52    shows "((Abs ---> id) ---> op -` Rep) Collect = Collect"
    8.53    unfolding fun_eq_iff
    8.54 -  by (simp add: Quotient_abs_rep[OF assms])
    8.55 +  by (simp add: Quotient3_abs_rep[OF assms])
    8.56  
    8.57  lemma union_rsp[quot_respect]:
    8.58 -  assumes "Quotient R Abs Rep"
    8.59 +  assumes "Quotient3 R Abs Rep"
    8.60    shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"
    8.61    by (intro fun_relI) (simp add: set_rel_def)
    8.62  
    8.63  lemma union_prs[quot_preserve]:
    8.64 -  assumes "Quotient R Abs Rep"
    8.65 +  assumes "Quotient3 R Abs Rep"
    8.66    shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<union> = op \<union>"
    8.67    unfolding fun_eq_iff
    8.68 -  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
    8.69 +  by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
    8.70  
    8.71  lemma diff_rsp[quot_respect]:
    8.72 -  assumes "Quotient R Abs Rep"
    8.73 +  assumes "Quotient3 R Abs Rep"
    8.74    shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"
    8.75    by (intro fun_relI) (simp add: set_rel_def)
    8.76  
    8.77  lemma diff_prs[quot_preserve]:
    8.78 -  assumes "Quotient R Abs Rep"
    8.79 +  assumes "Quotient3 R Abs Rep"
    8.80    shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -"
    8.81    unfolding fun_eq_iff
    8.82 -  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
    8.83 +  by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
    8.84  
    8.85  lemma inter_rsp[quot_respect]:
    8.86 -  assumes "Quotient R Abs Rep"
    8.87 +  assumes "Quotient3 R Abs Rep"
    8.88    shows "(set_rel R ===> set_rel R ===> set_rel R) op \<inter> op \<inter>"
    8.89    by (intro fun_relI) (auto simp add: set_rel_def)
    8.90  
    8.91  lemma inter_prs[quot_preserve]:
    8.92 -  assumes "Quotient R Abs Rep"
    8.93 +  assumes "Quotient3 R Abs Rep"
    8.94    shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<inter> = op \<inter>"
    8.95    unfolding fun_eq_iff
    8.96 -  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
    8.97 +  by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
    8.98  
    8.99  lemma mem_prs[quot_preserve]:
   8.100 -  assumes "Quotient R Abs Rep"
   8.101 +  assumes "Quotient3 R Abs Rep"
   8.102    shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
   8.103 -  by (simp add: fun_eq_iff Quotient_abs_rep[OF assms])
   8.104 +  by (simp add: fun_eq_iff Quotient3_abs_rep[OF assms])
   8.105  
   8.106  lemma mem_rsp[quot_respect]:
   8.107    shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
     9.1 --- a/src/HOL/Library/Quotient_Sum.thy	Tue Apr 03 14:09:37 2012 +0200
     9.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Tue Apr 03 16:26:48 2012 +0200
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      HOL/Library/Quotient_Sum.thy
     9.5 +(*  Title:      HOL/Library/Quotient3_Sum.thy
     9.6      Author:     Cezary Kaliszyk and Christian Urban
     9.7  *)
     9.8  
     9.9 @@ -55,44 +55,44 @@
    9.10    by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE)
    9.11    
    9.12  lemma sum_quotient [quot_thm]:
    9.13 -  assumes q1: "Quotient R1 Abs1 Rep1"
    9.14 -  assumes q2: "Quotient R2 Abs2 Rep2"
    9.15 -  shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
    9.16 -  apply (rule QuotientI)
    9.17 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    9.18 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    9.19 +  shows "Quotient3 (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
    9.20 +  apply (rule Quotient3I)
    9.21    apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
    9.22 -    Quotient_abs_rep [OF q1] Quotient_rel_rep [OF q1] Quotient_abs_rep [OF q2] Quotient_rel_rep [OF q2])
    9.23 -  using Quotient_rel [OF q1] Quotient_rel [OF q2]
    9.24 +    Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2])
    9.25 +  using Quotient3_rel [OF q1] Quotient3_rel [OF q2]
    9.26    apply (simp add: sum_rel_unfold comp_def split: sum.split)
    9.27    done
    9.28  
    9.29 -declare [[map sum = (sum_rel, sum_quotient)]]
    9.30 +declare [[mapQ3 sum = (sum_rel, sum_quotient)]]
    9.31  
    9.32  lemma sum_Inl_rsp [quot_respect]:
    9.33 -  assumes q1: "Quotient R1 Abs1 Rep1"
    9.34 -  assumes q2: "Quotient R2 Abs2 Rep2"
    9.35 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    9.36 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    9.37    shows "(R1 ===> sum_rel R1 R2) Inl Inl"
    9.38    by auto
    9.39  
    9.40  lemma sum_Inr_rsp [quot_respect]:
    9.41 -  assumes q1: "Quotient R1 Abs1 Rep1"
    9.42 -  assumes q2: "Quotient R2 Abs2 Rep2"
    9.43 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    9.44 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    9.45    shows "(R2 ===> sum_rel R1 R2) Inr Inr"
    9.46    by auto
    9.47  
    9.48  lemma sum_Inl_prs [quot_preserve]:
    9.49 -  assumes q1: "Quotient R1 Abs1 Rep1"
    9.50 -  assumes q2: "Quotient R2 Abs2 Rep2"
    9.51 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    9.52 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    9.53    shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
    9.54    apply(simp add: fun_eq_iff)
    9.55 -  apply(simp add: Quotient_abs_rep[OF q1])
    9.56 +  apply(simp add: Quotient3_abs_rep[OF q1])
    9.57    done
    9.58  
    9.59  lemma sum_Inr_prs [quot_preserve]:
    9.60 -  assumes q1: "Quotient R1 Abs1 Rep1"
    9.61 -  assumes q2: "Quotient R2 Abs2 Rep2"
    9.62 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    9.63 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    9.64    shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
    9.65    apply(simp add: fun_eq_iff)
    9.66 -  apply(simp add: Quotient_abs_rep[OF q2])
    9.67 +  apply(simp add: Quotient3_abs_rep[OF q2])
    9.68    done
    9.69  
    9.70  end
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Lifting.thy	Tue Apr 03 16:26:48 2012 +0200
    10.3 @@ -0,0 +1,316 @@
    10.4 +(*  Title:      HOL/Lifting.thy
    10.5 +    Author:     Brian Huffman and Ondrej Kuncar
    10.6 +    Author:     Cezary Kaliszyk and Christian Urban
    10.7 +*)
    10.8 +
    10.9 +header {* Lifting package *}
   10.10 +
   10.11 +theory Lifting
   10.12 +imports Plain Equiv_Relations
   10.13 +keywords
   10.14 +  "print_quotmaps" "print_quotients" :: diag and
   10.15 +  "lift_definition" :: thy_goal and
   10.16 +  "setup_lifting" :: thy_decl
   10.17 +uses
   10.18 +  ("Tools/Lifting/lifting_info.ML")
   10.19 +  ("Tools/Lifting/lifting_term.ML")
   10.20 +  ("Tools/Lifting/lifting_def.ML")
   10.21 +  ("Tools/Lifting/lifting_setup.ML")
   10.22 +begin
   10.23 +
   10.24 +subsection {* Function map and function relation *}
   10.25 +
   10.26 +notation map_fun (infixr "--->" 55)
   10.27 +
   10.28 +lemma map_fun_id:
   10.29 +  "(id ---> id) = id"
   10.30 +  by (simp add: fun_eq_iff)
   10.31 +
   10.32 +definition
   10.33 +  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool" (infixr "===>" 55)
   10.34 +where
   10.35 +  "fun_rel R1 R2 = (\<lambda>f g. \<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
   10.36 +
   10.37 +lemma fun_relI [intro]:
   10.38 +  assumes "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
   10.39 +  shows "(R1 ===> R2) f g"
   10.40 +  using assms by (simp add: fun_rel_def)
   10.41 +
   10.42 +lemma fun_relE:
   10.43 +  assumes "(R1 ===> R2) f g" and "R1 x y"
   10.44 +  obtains "R2 (f x) (g y)"
   10.45 +  using assms by (simp add: fun_rel_def)
   10.46 +
   10.47 +lemma fun_rel_eq:
   10.48 +  shows "((op =) ===> (op =)) = (op =)"
   10.49 +  by (auto simp add: fun_eq_iff elim: fun_relE)
   10.50 +
   10.51 +lemma fun_rel_eq_rel:
   10.52 +  shows "((op =) ===> R) = (\<lambda>f g. \<forall>x. R (f x) (g x))"
   10.53 +  by (simp add: fun_rel_def)
   10.54 +
   10.55 +subsection {* Quotient Predicate *}
   10.56 +
   10.57 +definition
   10.58 +  "Quotient R Abs Rep T \<longleftrightarrow>
   10.59 +     (\<forall>a. Abs (Rep a) = a) \<and> 
   10.60 +     (\<forall>a. R (Rep a) (Rep a)) \<and>
   10.61 +     (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and>
   10.62 +     T = (\<lambda>x y. R x x \<and> Abs x = y)"
   10.63 +
   10.64 +lemma QuotientI:
   10.65 +  assumes "\<And>a. Abs (Rep a) = a"
   10.66 +    and "\<And>a. R (Rep a) (Rep a)"
   10.67 +    and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
   10.68 +    and "T = (\<lambda>x y. R x x \<and> Abs x = y)"
   10.69 +  shows "Quotient R Abs Rep T"
   10.70 +  using assms unfolding Quotient_def by blast
   10.71 +
   10.72 +lemma Quotient_abs_rep:
   10.73 +  assumes a: "Quotient R Abs Rep T"
   10.74 +  shows "Abs (Rep a) = a"
   10.75 +  using a
   10.76 +  unfolding Quotient_def
   10.77 +  by simp
   10.78 +
   10.79 +lemma Quotient_rep_reflp:
   10.80 +  assumes a: "Quotient R Abs Rep T"
   10.81 +  shows "R (Rep a) (Rep a)"
   10.82 +  using a
   10.83 +  unfolding Quotient_def
   10.84 +  by blast
   10.85 +
   10.86 +lemma Quotient_rel:
   10.87 +  assumes a: "Quotient R Abs Rep T"
   10.88 +  shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
   10.89 +  using a
   10.90 +  unfolding Quotient_def
   10.91 +  by blast
   10.92 +
   10.93 +lemma Quotient_cr_rel:
   10.94 +  assumes a: "Quotient R Abs Rep T"
   10.95 +  shows "T = (\<lambda>x y. R x x \<and> Abs x = y)"
   10.96 +  using a
   10.97 +  unfolding Quotient_def
   10.98 +  by blast
   10.99 +
  10.100 +lemma Quotient_refl1: 
  10.101 +  assumes a: "Quotient R Abs Rep T" 
  10.102 +  shows "R r s \<Longrightarrow> R r r"
  10.103 +  using a unfolding Quotient_def 
  10.104 +  by fast
  10.105 +
  10.106 +lemma Quotient_refl2: 
  10.107 +  assumes a: "Quotient R Abs Rep T" 
  10.108 +  shows "R r s \<Longrightarrow> R s s"
  10.109 +  using a unfolding Quotient_def 
  10.110 +  by fast
  10.111 +
  10.112 +lemma Quotient_rel_rep:
  10.113 +  assumes a: "Quotient R Abs Rep T"
  10.114 +  shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
  10.115 +  using a
  10.116 +  unfolding Quotient_def
  10.117 +  by metis
  10.118 +
  10.119 +lemma Quotient_rep_abs:
  10.120 +  assumes a: "Quotient R Abs Rep T"
  10.121 +  shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
  10.122 +  using a unfolding Quotient_def
  10.123 +  by blast
  10.124 +
  10.125 +lemma Quotient_rel_abs:
  10.126 +  assumes a: "Quotient R Abs Rep T"
  10.127 +  shows "R r s \<Longrightarrow> Abs r = Abs s"
  10.128 +  using a unfolding Quotient_def
  10.129 +  by blast
  10.130 +
  10.131 +lemma Quotient_symp:
  10.132 +  assumes a: "Quotient R Abs Rep T"
  10.133 +  shows "symp R"
  10.134 +  using a unfolding Quotient_def using sympI by (metis (full_types))
  10.135 +
  10.136 +lemma Quotient_transp:
  10.137 +  assumes a: "Quotient R Abs Rep T"
  10.138 +  shows "transp R"
  10.139 +  using a unfolding Quotient_def using transpI by (metis (full_types))
  10.140 +
  10.141 +lemma Quotient_part_equivp:
  10.142 +  assumes a: "Quotient R Abs Rep T"
  10.143 +  shows "part_equivp R"
  10.144 +by (metis Quotient_rep_reflp Quotient_symp Quotient_transp a part_equivpI)
  10.145 +
  10.146 +lemma identity_quotient: "Quotient (op =) id id (op =)"
  10.147 +unfolding Quotient_def by simp 
  10.148 +
  10.149 +lemma Quotient_alt_def:
  10.150 +  "Quotient R Abs Rep T \<longleftrightarrow>
  10.151 +    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
  10.152 +    (\<forall>b. T (Rep b) b) \<and>
  10.153 +    (\<forall>x y. R x y \<longleftrightarrow> T x (Abs x) \<and> T y (Abs y) \<and> Abs x = Abs y)"
  10.154 +apply safe
  10.155 +apply (simp (no_asm_use) only: Quotient_def, fast)
  10.156 +apply (simp (no_asm_use) only: Quotient_def, fast)
  10.157 +apply (simp (no_asm_use) only: Quotient_def, fast)
  10.158 +apply (simp (no_asm_use) only: Quotient_def, fast)
  10.159 +apply (simp (no_asm_use) only: Quotient_def, fast)
  10.160 +apply (simp (no_asm_use) only: Quotient_def, fast)
  10.161 +apply (rule QuotientI)
  10.162 +apply simp
  10.163 +apply metis
  10.164 +apply simp
  10.165 +apply (rule ext, rule ext, metis)
  10.166 +done
  10.167 +
  10.168 +lemma Quotient_alt_def2:
  10.169 +  "Quotient R Abs Rep T \<longleftrightarrow>
  10.170 +    (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
  10.171 +    (\<forall>b. T (Rep b) b) \<and>
  10.172 +    (\<forall>x y. R x y \<longleftrightarrow> T x (Abs y) \<and> T y (Abs x))"
  10.173 +  unfolding Quotient_alt_def by (safe, metis+)
  10.174 +
  10.175 +lemma fun_quotient:
  10.176 +  assumes 1: "Quotient R1 abs1 rep1 T1"
  10.177 +  assumes 2: "Quotient R2 abs2 rep2 T2"
  10.178 +  shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2) (T1 ===> T2)"
  10.179 +  using assms unfolding Quotient_alt_def2
  10.180 +  unfolding fun_rel_def fun_eq_iff map_fun_apply
  10.181 +  by (safe, metis+)
  10.182 +
  10.183 +lemma apply_rsp:
  10.184 +  fixes f g::"'a \<Rightarrow> 'c"
  10.185 +  assumes q: "Quotient R1 Abs1 Rep1 T1"
  10.186 +  and     a: "(R1 ===> R2) f g" "R1 x y"
  10.187 +  shows "R2 (f x) (g y)"
  10.188 +  using a by (auto elim: fun_relE)
  10.189 +
  10.190 +lemma apply_rsp':
  10.191 +  assumes a: "(R1 ===> R2) f g" "R1 x y"
  10.192 +  shows "R2 (f x) (g y)"
  10.193 +  using a by (auto elim: fun_relE)
  10.194 +
  10.195 +lemma apply_rsp'':
  10.196 +  assumes "Quotient R Abs Rep T"
  10.197 +  and "(R ===> S) f f"
  10.198 +  shows "S (f (Rep x)) (f (Rep x))"
  10.199 +proof -
  10.200 +  from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp)
  10.201 +  then show ?thesis using assms(2) by (auto intro: apply_rsp')
  10.202 +qed
  10.203 +
  10.204 +subsection {* Quotient composition *}
  10.205 +
  10.206 +lemma Quotient_compose:
  10.207 +  assumes 1: "Quotient R1 Abs1 Rep1 T1"
  10.208 +  assumes 2: "Quotient R2 Abs2 Rep2 T2"
  10.209 +  shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)"
  10.210 +proof -
  10.211 +  from 1 have Abs1: "\<And>a b. T1 a b \<Longrightarrow> Abs1 a = b"
  10.212 +    unfolding Quotient_alt_def by simp
  10.213 +  from 1 have Rep1: "\<And>b. T1 (Rep1 b) b"
  10.214 +    unfolding Quotient_alt_def by simp
  10.215 +  from 2 have Abs2: "\<And>a b. T2 a b \<Longrightarrow> Abs2 a = b"
  10.216 +    unfolding Quotient_alt_def by simp
  10.217 +  from 2 have Rep2: "\<And>b. T2 (Rep2 b) b"
  10.218 +    unfolding Quotient_alt_def by simp
  10.219 +  from 2 have R2:
  10.220 +    "\<And>x y. R2 x y \<longleftrightarrow> T2 x (Abs2 x) \<and> T2 y (Abs2 y) \<and> Abs2 x = Abs2 y"
  10.221 +    unfolding Quotient_alt_def by simp
  10.222 +  show ?thesis
  10.223 +    unfolding Quotient_alt_def
  10.224 +    apply simp
  10.225 +    apply safe
  10.226 +    apply (drule Abs1, simp)
  10.227 +    apply (erule Abs2)
  10.228 +    apply (rule pred_compI)
  10.229 +    apply (rule Rep1)
  10.230 +    apply (rule Rep2)
  10.231 +    apply (rule pred_compI, assumption)
  10.232 +    apply (drule Abs1, simp)
  10.233 +    apply (clarsimp simp add: R2)
  10.234 +    apply (rule pred_compI, assumption)
  10.235 +    apply (drule Abs1, simp)+
  10.236 +    apply (clarsimp simp add: R2)
  10.237 +    apply (drule Abs1, simp)+
  10.238 +    apply (clarsimp simp add: R2)
  10.239 +    apply (rule pred_compI, assumption)
  10.240 +    apply (rule pred_compI [rotated])
  10.241 +    apply (erule conversepI)
  10.242 +    apply (drule Abs1, simp)+
  10.243 +    apply (simp add: R2)
  10.244 +    done
  10.245 +qed
  10.246 +
  10.247 +subsection {* Invariant *}
  10.248 +
  10.249 +definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
  10.250 +  where "invariant R = (\<lambda>x y. R x \<and> x = y)"
  10.251 +
  10.252 +lemma invariant_to_eq:
  10.253 +  assumes "invariant P x y"
  10.254 +  shows "x = y"
  10.255 +using assms by (simp add: invariant_def)
  10.256 +
  10.257 +lemma fun_rel_eq_invariant:
  10.258 +  shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
  10.259 +by (auto simp add: invariant_def fun_rel_def)
  10.260 +
  10.261 +lemma invariant_same_args:
  10.262 +  shows "invariant P x x \<equiv> P x"
  10.263 +using assms by (auto simp add: invariant_def)
  10.264 +
  10.265 +lemma copy_type_to_Quotient:
  10.266 +  assumes "type_definition Rep Abs UNIV"
  10.267 +  and T_def: "T \<equiv> (\<lambda>x y. Abs x = y)"
  10.268 +  shows "Quotient (op =) Abs Rep T"
  10.269 +proof -
  10.270 +  interpret type_definition Rep Abs UNIV by fact
  10.271 +  from Abs_inject Rep_inverse T_def show ?thesis by (auto intro!: QuotientI)
  10.272 +qed
  10.273 +
  10.274 +lemma copy_type_to_equivp:
  10.275 +  fixes Abs :: "'a \<Rightarrow> 'b"
  10.276 +  and Rep :: "'b \<Rightarrow> 'a"
  10.277 +  assumes "type_definition Rep Abs (UNIV::'a set)"
  10.278 +  shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
  10.279 +by (rule identity_equivp)
  10.280 +
  10.281 +lemma invariant_type_to_Quotient:
  10.282 +  assumes "type_definition Rep Abs {x. P x}"
  10.283 +  and T_def: "T \<equiv> (\<lambda>x y. (invariant P) x x \<and> Abs x = y)"
  10.284 +  shows "Quotient (invariant P) Abs Rep T"
  10.285 +proof -
  10.286 +  interpret type_definition Rep Abs "{x. P x}" by fact
  10.287 +  from Rep Abs_inject Rep_inverse T_def show ?thesis by (auto intro!: QuotientI simp: invariant_def)
  10.288 +qed
  10.289 +
  10.290 +lemma invariant_type_to_part_equivp:
  10.291 +  assumes "type_definition Rep Abs {x. P x}"
  10.292 +  shows "part_equivp (invariant P)"
  10.293 +proof (intro part_equivpI)
  10.294 +  interpret type_definition Rep Abs "{x. P x}" by fact
  10.295 +  show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def)
  10.296 +next
  10.297 +  show "symp (invariant P)" by (auto intro: sympI simp: invariant_def)
  10.298 +next
  10.299 +  show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
  10.300 +qed
  10.301 +
  10.302 +subsection {* ML setup *}
  10.303 +
  10.304 +text {* Auxiliary data for the lifting package *}
  10.305 +
  10.306 +use "Tools/Lifting/lifting_info.ML"
  10.307 +setup Lifting_Info.setup
  10.308 +
  10.309 +declare [[map "fun" = (fun_rel, fun_quotient)]]
  10.310 +
  10.311 +use "Tools/Lifting/lifting_term.ML"
  10.312 +
  10.313 +use "Tools/Lifting/lifting_def.ML"
  10.314 +
  10.315 +use "Tools/Lifting/lifting_setup.ML"
  10.316 +
  10.317 +hide_const (open) invariant
  10.318 +
  10.319 +end
    11.1 --- a/src/HOL/Metis_Examples/Clausification.thy	Tue Apr 03 14:09:37 2012 +0200
    11.2 +++ b/src/HOL/Metis_Examples/Clausification.thy	Tue Apr 03 16:26:48 2012 +0200
    11.3 @@ -131,7 +131,7 @@
    11.4  by (metis bounded_def subset_eq)
    11.5  
    11.6  lemma
    11.7 -  assumes a: "Quotient R Abs Rep"
    11.8 +  assumes a: "Quotient R Abs Rep T"
    11.9    shows "symp R"
   11.10  using a unfolding Quotient_def using sympI
   11.11  by (metis (full_types))
    12.1 --- a/src/HOL/Quotient.thy	Tue Apr 03 14:09:37 2012 +0200
    12.2 +++ b/src/HOL/Quotient.thy	Tue Apr 03 16:26:48 2012 +0200
    12.3 @@ -5,11 +5,10 @@
    12.4  header {* Definition of Quotient Types *}
    12.5  
    12.6  theory Quotient
    12.7 -imports Plain Hilbert_Choice Equiv_Relations
    12.8 +imports Plain Hilbert_Choice Equiv_Relations Lifting
    12.9  keywords
   12.10 -  "print_quotmaps" "print_quotients" "print_quotconsts" :: diag and
   12.11 +  "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
   12.12    "quotient_type" :: thy_goal and "/" and
   12.13 -  "setup_lifting" :: thy_decl and
   12.14    "quotient_definition" :: thy_goal
   12.15  uses
   12.16    ("Tools/Quotient/quotient_info.ML")
   12.17 @@ -53,37 +52,6 @@
   12.18    shows "x \<in> Respects R \<longleftrightarrow> R x x"
   12.19    unfolding Respects_def by simp
   12.20  
   12.21 -subsection {* Function map and function relation *}
   12.22 -
   12.23 -notation map_fun (infixr "--->" 55)
   12.24 -
   12.25 -lemma map_fun_id:
   12.26 -  "(id ---> id) = id"
   12.27 -  by (simp add: fun_eq_iff)
   12.28 -
   12.29 -definition
   12.30 -  fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool" (infixr "===>" 55)
   12.31 -where
   12.32 -  "fun_rel R1 R2 = (\<lambda>f g. \<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
   12.33 -
   12.34 -lemma fun_relI [intro]:
   12.35 -  assumes "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
   12.36 -  shows "(R1 ===> R2) f g"
   12.37 -  using assms by (simp add: fun_rel_def)
   12.38 -
   12.39 -lemma fun_relE:
   12.40 -  assumes "(R1 ===> R2) f g" and "R1 x y"
   12.41 -  obtains "R2 (f x) (g y)"
   12.42 -  using assms by (simp add: fun_rel_def)
   12.43 -
   12.44 -lemma fun_rel_eq:
   12.45 -  shows "((op =) ===> (op =)) = (op =)"
   12.46 -  by (auto simp add: fun_eq_iff elim: fun_relE)
   12.47 -
   12.48 -lemma fun_rel_eq_rel:
   12.49 -  shows "((op =) ===> R) = (\<lambda>f g. \<forall>x. R (f x) (g x))"
   12.50 -  by (simp add: fun_rel_def)
   12.51 -
   12.52  subsection {* set map (vimage) and set relation *}
   12.53  
   12.54  definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
   12.55 @@ -106,155 +74,169 @@
   12.56  subsection {* Quotient Predicate *}
   12.57  
   12.58  definition
   12.59 -  "Quotient R Abs Rep \<longleftrightarrow>
   12.60 +  "Quotient3 R Abs Rep \<longleftrightarrow>
   12.61       (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. R (Rep a) (Rep a)) \<and>
   12.62       (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s)"
   12.63  
   12.64 -lemma QuotientI:
   12.65 +lemma Quotient3I:
   12.66    assumes "\<And>a. Abs (Rep a) = a"
   12.67      and "\<And>a. R (Rep a) (Rep a)"
   12.68      and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
   12.69 -  shows "Quotient R Abs Rep"
   12.70 -  using assms unfolding Quotient_def by blast
   12.71 +  shows "Quotient3 R Abs Rep"
   12.72 +  using assms unfolding Quotient3_def by blast
   12.73  
   12.74 -lemma Quotient_abs_rep:
   12.75 -  assumes a: "Quotient R Abs Rep"
   12.76 +lemma Quotient3_abs_rep:
   12.77 +  assumes a: "Quotient3 R Abs Rep"
   12.78    shows "Abs (Rep a) = a"
   12.79    using a
   12.80 -  unfolding Quotient_def
   12.81 +  unfolding Quotient3_def
   12.82    by simp
   12.83  
   12.84 -lemma Quotient_rep_reflp:
   12.85 -  assumes a: "Quotient R Abs Rep"
   12.86 +lemma Quotient3_rep_reflp:
   12.87 +  assumes a: "Quotient3 R Abs Rep"
   12.88    shows "R (Rep a) (Rep a)"
   12.89    using a
   12.90 -  unfolding Quotient_def
   12.91 +  unfolding Quotient3_def
   12.92    by blast
   12.93  
   12.94 -lemma Quotient_rel:
   12.95 -  assumes a: "Quotient R Abs Rep"
   12.96 +lemma Quotient3_rel:
   12.97 +  assumes a: "Quotient3 R Abs Rep"
   12.98    shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
   12.99    using a
  12.100 -  unfolding Quotient_def
  12.101 +  unfolding Quotient3_def
  12.102    by blast
  12.103  
  12.104 -lemma Quotient_refl1: 
  12.105 -  assumes a: "Quotient R Abs Rep" 
  12.106 +lemma Quotient3_refl1: 
  12.107 +  assumes a: "Quotient3 R Abs Rep" 
  12.108    shows "R r s \<Longrightarrow> R r r"
  12.109 -  using a unfolding Quotient_def 
  12.110 +  using a unfolding Quotient3_def 
  12.111    by fast
  12.112  
  12.113 -lemma Quotient_refl2: 
  12.114 -  assumes a: "Quotient R Abs Rep" 
  12.115 +lemma Quotient3_refl2: 
  12.116 +  assumes a: "Quotient3 R Abs Rep" 
  12.117    shows "R r s \<Longrightarrow> R s s"
  12.118 -  using a unfolding Quotient_def 
  12.119 +  using a unfolding Quotient3_def 
  12.120    by fast
  12.121  
  12.122 -lemma Quotient_rel_rep:
  12.123 -  assumes a: "Quotient R Abs Rep"
  12.124 +lemma Quotient3_rel_rep:
  12.125 +  assumes a: "Quotient3 R Abs Rep"
  12.126    shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
  12.127    using a
  12.128 -  unfolding Quotient_def
  12.129 +  unfolding Quotient3_def
  12.130    by metis
  12.131  
  12.132 -lemma Quotient_rep_abs:
  12.133 -  assumes a: "Quotient R Abs Rep"
  12.134 +lemma Quotient3_rep_abs:
  12.135 +  assumes a: "Quotient3 R Abs Rep"
  12.136    shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
  12.137 -  using a unfolding Quotient_def
  12.138 +  using a unfolding Quotient3_def
  12.139 +  by blast
  12.140 +
  12.141 +lemma Quotient3_rel_abs:
  12.142 +  assumes a: "Quotient3 R Abs Rep"
  12.143 +  shows "R r s \<Longrightarrow> Abs r = Abs s"
  12.144 +  using a unfolding Quotient3_def
  12.145    by blast
  12.146  
  12.147 -lemma Quotient_rel_abs:
  12.148 -  assumes a: "Quotient R Abs Rep"
  12.149 -  shows "R r s \<Longrightarrow> Abs r = Abs s"
  12.150 -  using a unfolding Quotient_def
  12.151 -  by blast
  12.152 -
  12.153 -lemma Quotient_symp:
  12.154 -  assumes a: "Quotient R Abs Rep"
  12.155 +lemma Quotient3_symp:
  12.156 +  assumes a: "Quotient3 R Abs Rep"
  12.157    shows "symp R"
  12.158 -  using a unfolding Quotient_def using sympI by metis
  12.159 +  using a unfolding Quotient3_def using sympI by metis
  12.160  
  12.161 -lemma Quotient_transp:
  12.162 -  assumes a: "Quotient R Abs Rep"
  12.163 +lemma Quotient3_transp:
  12.164 +  assumes a: "Quotient3 R Abs Rep"
  12.165    shows "transp R"
  12.166 -  using a unfolding Quotient_def using transpI by metis
  12.167 +  using a unfolding Quotient3_def using transpI by (metis (full_types))
  12.168  
  12.169 -lemma identity_quotient:
  12.170 -  shows "Quotient (op =) id id"
  12.171 -  unfolding Quotient_def id_def
  12.172 +lemma Quotient3_part_equivp:
  12.173 +  assumes a: "Quotient3 R Abs Rep"
  12.174 +  shows "part_equivp R"
  12.175 +by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp a part_equivpI)
  12.176 +
  12.177 +lemma identity_quotient3:
  12.178 +  shows "Quotient3 (op =) id id"
  12.179 +  unfolding Quotient3_def id_def
  12.180    by blast
  12.181  
  12.182 -lemma fun_quotient:
  12.183 -  assumes q1: "Quotient R1 abs1 rep1"
  12.184 -  and     q2: "Quotient R2 abs2 rep2"
  12.185 -  shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
  12.186 +lemma fun_quotient3:
  12.187 +  assumes q1: "Quotient3 R1 abs1 rep1"
  12.188 +  and     q2: "Quotient3 R2 abs2 rep2"
  12.189 +  shows "Quotient3 (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
  12.190  proof -
  12.191 -  have "\<And>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
  12.192 -    using q1 q2 by (simp add: Quotient_def fun_eq_iff)
  12.193 +  have "\<And>a.(rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
  12.194 +    using q1 q2 by (simp add: Quotient3_def fun_eq_iff)
  12.195    moreover
  12.196 -  have "\<And>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
  12.197 +  have "\<And>a.(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
  12.198      by (rule fun_relI)
  12.199 -      (insert q1 q2 Quotient_rel_abs [of R1 abs1 rep1] Quotient_rel_rep [of R2 abs2 rep2],
  12.200 -        simp (no_asm) add: Quotient_def, simp)
  12.201 +      (insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2],
  12.202 +        simp (no_asm) add: Quotient3_def, simp)
  12.203 +  
  12.204    moreover
  12.205 -  have "\<And>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
  12.206 +  {
  12.207 +  fix r s
  12.208 +  have "(R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
  12.209          (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
  12.210 -    apply(auto simp add: fun_rel_def fun_eq_iff)
  12.211 -    using q1 q2 unfolding Quotient_def
  12.212 -    apply(metis)
  12.213 -    using q1 q2 unfolding Quotient_def
  12.214 -    apply(metis)
  12.215 -    using q1 q2 unfolding Quotient_def
  12.216 -    apply(metis)
  12.217 -    using q1 q2 unfolding Quotient_def
  12.218 -    apply(metis)
  12.219 -    done
  12.220 -  ultimately
  12.221 -  show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
  12.222 -    unfolding Quotient_def by blast
  12.223 +  proof -
  12.224 +    
  12.225 +    have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) r r" unfolding fun_rel_def
  12.226 +      using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] 
  12.227 +      by (metis (full_types) part_equivp_def)
  12.228 +    moreover have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) s s" unfolding fun_rel_def
  12.229 +      using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2] 
  12.230 +      by (metis (full_types) part_equivp_def)
  12.231 +    moreover have "(R1 ===> R2) r s \<Longrightarrow> (rep1 ---> abs2) r  = (rep1 ---> abs2) s"
  12.232 +      apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def by metis
  12.233 +    moreover have "((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
  12.234 +        (rep1 ---> abs2) r  = (rep1 ---> abs2) s) \<Longrightarrow> (R1 ===> R2) r s"
  12.235 +      apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def 
  12.236 +    by (metis map_fun_apply)
  12.237 +  
  12.238 +    ultimately show ?thesis by blast
  12.239 + qed
  12.240 + }
  12.241 + ultimately show ?thesis by (intro Quotient3I) (assumption+)
  12.242  qed
  12.243  
  12.244  lemma abs_o_rep:
  12.245 -  assumes a: "Quotient R Abs Rep"
  12.246 +  assumes a: "Quotient3 R Abs Rep"
  12.247    shows "Abs o Rep = id"
  12.248    unfolding fun_eq_iff
  12.249 -  by (simp add: Quotient_abs_rep[OF a])
  12.250 +  by (simp add: Quotient3_abs_rep[OF a])
  12.251  
  12.252  lemma equals_rsp:
  12.253 -  assumes q: "Quotient R Abs Rep"
  12.254 +  assumes q: "Quotient3 R Abs Rep"
  12.255    and     a: "R xa xb" "R ya yb"
  12.256    shows "R xa ya = R xb yb"
  12.257 -  using a Quotient_symp[OF q] Quotient_transp[OF q]
  12.258 +  using a Quotient3_symp[OF q] Quotient3_transp[OF q]
  12.259    by (blast elim: sympE transpE)
  12.260  
  12.261  lemma lambda_prs:
  12.262 -  assumes q1: "Quotient R1 Abs1 Rep1"
  12.263 -  and     q2: "Quotient R2 Abs2 Rep2"
  12.264 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
  12.265 +  and     q2: "Quotient3 R2 Abs2 Rep2"
  12.266    shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
  12.267    unfolding fun_eq_iff
  12.268 -  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
  12.269 +  using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
  12.270    by simp
  12.271  
  12.272  lemma lambda_prs1:
  12.273 -  assumes q1: "Quotient R1 Abs1 Rep1"
  12.274 -  and     q2: "Quotient R2 Abs2 Rep2"
  12.275 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
  12.276 +  and     q2: "Quotient3 R2 Abs2 Rep2"
  12.277    shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
  12.278    unfolding fun_eq_iff
  12.279 -  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
  12.280 +  using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
  12.281    by simp
  12.282  
  12.283  lemma rep_abs_rsp:
  12.284 -  assumes q: "Quotient R Abs Rep"
  12.285 +  assumes q: "Quotient3 R Abs Rep"
  12.286    and     a: "R x1 x2"
  12.287    shows "R x1 (Rep (Abs x2))"
  12.288 -  using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]
  12.289 +  using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q]
  12.290    by metis
  12.291  
  12.292  lemma rep_abs_rsp_left:
  12.293 -  assumes q: "Quotient R Abs Rep"
  12.294 +  assumes q: "Quotient3 R Abs Rep"
  12.295    and     a: "R x1 x2"
  12.296    shows "R (Rep (Abs x1)) x2"
  12.297 -  using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]
  12.298 +  using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q]
  12.299    by metis
  12.300  
  12.301  text{*
  12.302 @@ -264,24 +246,19 @@
  12.303    will be provable; which is why we need to use @{text apply_rsp} and
  12.304    not the primed version *}
  12.305  
  12.306 -lemma apply_rsp:
  12.307 +lemma apply_rspQ3:
  12.308    fixes f g::"'a \<Rightarrow> 'c"
  12.309 -  assumes q: "Quotient R1 Abs1 Rep1"
  12.310 +  assumes q: "Quotient3 R1 Abs1 Rep1"
  12.311    and     a: "(R1 ===> R2) f g" "R1 x y"
  12.312    shows "R2 (f x) (g y)"
  12.313    using a by (auto elim: fun_relE)
  12.314  
  12.315 -lemma apply_rsp':
  12.316 -  assumes a: "(R1 ===> R2) f g" "R1 x y"
  12.317 -  shows "R2 (f x) (g y)"
  12.318 -  using a by (auto elim: fun_relE)
  12.319 -
  12.320 -lemma apply_rsp'':
  12.321 -  assumes "Quotient R Abs Rep"
  12.322 +lemma apply_rspQ3'':
  12.323 +  assumes "Quotient3 R Abs Rep"
  12.324    and "(R ===> S) f f"
  12.325    shows "S (f (Rep x)) (f (Rep x))"
  12.326  proof -
  12.327 -  from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp)
  12.328 +  from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient3_rep_reflp)
  12.329    then show ?thesis using assms(2) by (auto intro: apply_rsp')
  12.330  qed
  12.331  
  12.332 @@ -393,29 +370,29 @@
  12.333    "x \<in> p \<Longrightarrow> Babs p m x = m x"
  12.334  
  12.335  lemma babs_rsp:
  12.336 -  assumes q: "Quotient R1 Abs1 Rep1"
  12.337 +  assumes q: "Quotient3 R1 Abs1 Rep1"
  12.338    and     a: "(R1 ===> R2) f g"
  12.339    shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
  12.340    apply (auto simp add: Babs_def in_respects fun_rel_def)
  12.341    apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
  12.342    using a apply (simp add: Babs_def fun_rel_def)
  12.343    apply (simp add: in_respects fun_rel_def)
  12.344 -  using Quotient_rel[OF q]
  12.345 +  using Quotient3_rel[OF q]
  12.346    by metis
  12.347  
  12.348  lemma babs_prs:
  12.349 -  assumes q1: "Quotient R1 Abs1 Rep1"
  12.350 -  and     q2: "Quotient R2 Abs2 Rep2"
  12.351 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
  12.352 +  and     q2: "Quotient3 R2 Abs2 Rep2"
  12.353    shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
  12.354    apply (rule ext)
  12.355    apply (simp add:)
  12.356    apply (subgoal_tac "Rep1 x \<in> Respects R1")
  12.357 -  apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
  12.358 -  apply (simp add: in_respects Quotient_rel_rep[OF q1])
  12.359 +  apply (simp add: Babs_def Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
  12.360 +  apply (simp add: in_respects Quotient3_rel_rep[OF q1])
  12.361    done
  12.362  
  12.363  lemma babs_simp:
  12.364 -  assumes q: "Quotient R1 Abs Rep"
  12.365 +  assumes q: "Quotient3 R1 Abs Rep"
  12.366    shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
  12.367    apply(rule iffI)
  12.368    apply(simp_all only: babs_rsp[OF q])
  12.369 @@ -423,7 +400,7 @@
  12.370    apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
  12.371    apply(metis Babs_def)
  12.372    apply (simp add: in_respects)
  12.373 -  using Quotient_rel[OF q]
  12.374 +  using Quotient3_rel[OF q]
  12.375    by metis
  12.376  
  12.377  (* If a user proves that a particular functional relation
  12.378 @@ -451,15 +428,15 @@
  12.379  
  12.380  (* 2 lemmas needed for cleaning of quantifiers *)
  12.381  lemma all_prs:
  12.382 -  assumes a: "Quotient R absf repf"
  12.383 +  assumes a: "Quotient3 R absf repf"
  12.384    shows "Ball (Respects R) ((absf ---> id) f) = All f"
  12.385 -  using a unfolding Quotient_def Ball_def in_respects id_apply comp_def map_fun_def
  12.386 +  using a unfolding Quotient3_def Ball_def in_respects id_apply comp_def map_fun_def
  12.387    by metis
  12.388  
  12.389  lemma ex_prs:
  12.390 -  assumes a: "Quotient R absf repf"
  12.391 +  assumes a: "Quotient3 R absf repf"
  12.392    shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
  12.393 -  using a unfolding Quotient_def Bex_def in_respects id_apply comp_def map_fun_def
  12.394 +  using a unfolding Quotient3_def Bex_def in_respects id_apply comp_def map_fun_def
  12.395    by metis
  12.396  
  12.397  subsection {* @{text Bex1_rel} quantifier *}
  12.398 @@ -508,7 +485,7 @@
  12.399    done
  12.400  
  12.401  lemma bex1_rel_rsp:
  12.402 -  assumes a: "Quotient R absf repf"
  12.403 +  assumes a: "Quotient3 R absf repf"
  12.404    shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
  12.405    apply (simp add: fun_rel_def)
  12.406    apply clarify
  12.407 @@ -520,7 +497,7 @@
  12.408  
  12.409  
  12.410  lemma ex1_prs:
  12.411 -  assumes a: "Quotient R absf repf"
  12.412 +  assumes a: "Quotient3 R absf repf"
  12.413    shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
  12.414  apply (simp add:)
  12.415  apply (subst Bex1_rel_def)
  12.416 @@ -535,7 +512,7 @@
  12.417    apply (rule_tac x="absf x" in exI)
  12.418    apply (simp)
  12.419    apply rule+
  12.420 -  using a unfolding Quotient_def
  12.421 +  using a unfolding Quotient3_def
  12.422    apply metis
  12.423   apply rule+
  12.424   apply (erule_tac x="x" in ballE)
  12.425 @@ -548,10 +525,10 @@
  12.426   apply (rule_tac x="repf x" in exI)
  12.427   apply (simp only: in_respects)
  12.428    apply rule
  12.429 - apply (metis Quotient_rel_rep[OF a])
  12.430 -using a unfolding Quotient_def apply (simp)
  12.431 + apply (metis Quotient3_rel_rep[OF a])
  12.432 +using a unfolding Quotient3_def apply (simp)
  12.433  apply rule+
  12.434 -using a unfolding Quotient_def in_respects
  12.435 +using a unfolding Quotient3_def in_respects
  12.436  apply metis
  12.437  done
  12.438  
  12.439 @@ -587,7 +564,7 @@
  12.440  subsection {* Various respects and preserve lemmas *}
  12.441  
  12.442  lemma quot_rel_rsp:
  12.443 -  assumes a: "Quotient R Abs Rep"
  12.444 +  assumes a: "Quotient3 R Abs Rep"
  12.445    shows "(R ===> R ===> op =) R R"
  12.446    apply(rule fun_relI)+
  12.447    apply(rule equals_rsp[OF a])
  12.448 @@ -595,12 +572,12 @@
  12.449    done
  12.450  
  12.451  lemma o_prs:
  12.452 -  assumes q1: "Quotient R1 Abs1 Rep1"
  12.453 -  and     q2: "Quotient R2 Abs2 Rep2"
  12.454 -  and     q3: "Quotient R3 Abs3 Rep3"
  12.455 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
  12.456 +  and     q2: "Quotient3 R2 Abs2 Rep2"
  12.457 +  and     q3: "Quotient3 R3 Abs3 Rep3"
  12.458    shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \<circ> = op \<circ>"
  12.459    and   "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \<circ> = op \<circ>"
  12.460 -  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
  12.461 +  using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] Quotient3_abs_rep[OF q3]
  12.462    by (simp_all add: fun_eq_iff)
  12.463  
  12.464  lemma o_rsp:
  12.465 @@ -609,26 +586,26 @@
  12.466    by (force elim: fun_relE)+
  12.467  
  12.468  lemma cond_prs:
  12.469 -  assumes a: "Quotient R absf repf"
  12.470 +  assumes a: "Quotient3 R absf repf"
  12.471    shows "absf (if a then repf b else repf c) = (if a then b else c)"
  12.472 -  using a unfolding Quotient_def by auto
  12.473 +  using a unfolding Quotient3_def by auto
  12.474  
  12.475  lemma if_prs:
  12.476 -  assumes q: "Quotient R Abs Rep"
  12.477 +  assumes q: "Quotient3 R Abs Rep"
  12.478    shows "(id ---> Rep ---> Rep ---> Abs) If = If"
  12.479 -  using Quotient_abs_rep[OF q]
  12.480 +  using Quotient3_abs_rep[OF q]
  12.481    by (auto simp add: fun_eq_iff)
  12.482  
  12.483  lemma if_rsp:
  12.484 -  assumes q: "Quotient R Abs Rep"
  12.485 +  assumes q: "Quotient3 R Abs Rep"
  12.486    shows "(op = ===> R ===> R ===> R) If If"
  12.487    by force
  12.488  
  12.489  lemma let_prs:
  12.490 -  assumes q1: "Quotient R1 Abs1 Rep1"
  12.491 -  and     q2: "Quotient R2 Abs2 Rep2"
  12.492 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
  12.493 +  and     q2: "Quotient3 R2 Abs2 Rep2"
  12.494    shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let"
  12.495 -  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
  12.496 +  using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
  12.497    by (auto simp add: fun_eq_iff)
  12.498  
  12.499  lemma let_rsp:
  12.500 @@ -640,9 +617,9 @@
  12.501    by auto
  12.502  
  12.503  lemma id_prs:
  12.504 -  assumes a: "Quotient R Abs Rep"
  12.505 +  assumes a: "Quotient3 R Abs Rep"
  12.506    shows "(Rep ---> Abs) id = id"
  12.507 -  by (simp add: fun_eq_iff Quotient_abs_rep [OF a])
  12.508 +  by (simp add: fun_eq_iff Quotient3_abs_rep [OF a])
  12.509  
  12.510  
  12.511  locale quot_type =
  12.512 @@ -673,8 +650,8 @@
  12.513    by (metis assms exE_some equivp[simplified part_equivp_def])
  12.514  
  12.515  lemma Quotient:
  12.516 -  shows "Quotient R abs rep"
  12.517 -  unfolding Quotient_def abs_def rep_def
  12.518 +  shows "Quotient3 R abs rep"
  12.519 +  unfolding Quotient3_def abs_def rep_def
  12.520    proof (intro conjI allI)
  12.521      fix a r s
  12.522      show x: "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" proof -
  12.523 @@ -703,149 +680,114 @@
  12.524  
  12.525  subsection {* Quotient composition *}
  12.526  
  12.527 -lemma OOO_quotient:
  12.528 +lemma OOO_quotient3:
  12.529    fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  12.530    fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
  12.531    fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
  12.532    fixes R2' :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  12.533    fixes R2 :: "'b \<Rightarrow> 'b \<Rightarrow> bool"
  12.534 -  assumes R1: "Quotient R1 Abs1 Rep1"
  12.535 -  assumes R2: "Quotient R2 Abs2 Rep2"
  12.536 +  assumes R1: "Quotient3 R1 Abs1 Rep1"
  12.537 +  assumes R2: "Quotient3 R2 Abs2 Rep2"
  12.538    assumes Abs1: "\<And>x y. R2' x y \<Longrightarrow> R1 x x \<Longrightarrow> R1 y y \<Longrightarrow> R2 (Abs1 x) (Abs1 y)"
  12.539    assumes Rep1: "\<And>x y. R2 x y \<Longrightarrow> R2' (Rep1 x) (Rep1 y)"
  12.540 -  shows "Quotient (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
  12.541 -apply (rule QuotientI)
  12.542 -   apply (simp add: o_def Quotient_abs_rep [OF R2] Quotient_abs_rep [OF R1])
  12.543 +  shows "Quotient3 (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
  12.544 +apply (rule Quotient3I)
  12.545 +   apply (simp add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1])
  12.546    apply simp
  12.547    apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI)
  12.548 -   apply (rule Quotient_rep_reflp [OF R1])
  12.549 +   apply (rule Quotient3_rep_reflp [OF R1])
  12.550    apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated])
  12.551 -   apply (rule Quotient_rep_reflp [OF R1])
  12.552 +   apply (rule Quotient3_rep_reflp [OF R1])
  12.553    apply (rule Rep1)
  12.554 -  apply (rule Quotient_rep_reflp [OF R2])
  12.555 +  apply (rule Quotient3_rep_reflp [OF R2])
  12.556   apply safe
  12.557      apply (rename_tac x y)
  12.558      apply (drule Abs1)
  12.559 -      apply (erule Quotient_refl2 [OF R1])
  12.560 -     apply (erule Quotient_refl1 [OF R1])
  12.561 -    apply (drule Quotient_refl1 [OF R2], drule Rep1)
  12.562 +      apply (erule Quotient3_refl2 [OF R1])
  12.563 +     apply (erule Quotient3_refl1 [OF R1])
  12.564 +    apply (drule Quotient3_refl1 [OF R2], drule Rep1)
  12.565      apply (subgoal_tac "R1 r (Rep1 (Abs1 x))")
  12.566       apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption)
  12.567       apply (erule pred_compI)
  12.568 -     apply (erule Quotient_symp [OF R1, THEN sympD])
  12.569 -    apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
  12.570 -    apply (rule conjI, erule Quotient_refl1 [OF R1])
  12.571 -    apply (rule conjI, rule Quotient_rep_reflp [OF R1])
  12.572 -    apply (subst Quotient_abs_rep [OF R1])
  12.573 -    apply (erule Quotient_rel_abs [OF R1])
  12.574 +     apply (erule Quotient3_symp [OF R1, THEN sympD])
  12.575 +    apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
  12.576 +    apply (rule conjI, erule Quotient3_refl1 [OF R1])
  12.577 +    apply (rule conjI, rule Quotient3_rep_reflp [OF R1])
  12.578 +    apply (subst Quotient3_abs_rep [OF R1])
  12.579 +    apply (erule Quotient3_rel_abs [OF R1])
  12.580     apply (rename_tac x y)
  12.581     apply (drule Abs1)
  12.582 -     apply (erule Quotient_refl2 [OF R1])
  12.583 -    apply (erule Quotient_refl1 [OF R1])
  12.584 -   apply (drule Quotient_refl2 [OF R2], drule Rep1)
  12.585 +     apply (erule Quotient3_refl2 [OF R1])
  12.586 +    apply (erule Quotient3_refl1 [OF R1])
  12.587 +   apply (drule Quotient3_refl2 [OF R2], drule Rep1)
  12.588     apply (subgoal_tac "R1 s (Rep1 (Abs1 y))")
  12.589      apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption)
  12.590      apply (erule pred_compI)
  12.591 -    apply (erule Quotient_symp [OF R1, THEN sympD])
  12.592 -   apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
  12.593 -   apply (rule conjI, erule Quotient_refl2 [OF R1])
  12.594 -   apply (rule conjI, rule Quotient_rep_reflp [OF R1])
  12.595 -   apply (subst Quotient_abs_rep [OF R1])
  12.596 -   apply (erule Quotient_rel_abs [OF R1, THEN sym])
  12.597 +    apply (erule Quotient3_symp [OF R1, THEN sympD])
  12.598 +   apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
  12.599 +   apply (rule conjI, erule Quotient3_refl2 [OF R1])
  12.600 +   apply (rule conjI, rule Quotient3_rep_reflp [OF R1])
  12.601 +   apply (subst Quotient3_abs_rep [OF R1])
  12.602 +   apply (erule Quotient3_rel_abs [OF R1, THEN sym])
  12.603    apply simp
  12.604 -  apply (rule Quotient_rel_abs [OF R2])
  12.605 -  apply (rule Quotient_rel_abs [OF R1, THEN ssubst], assumption)
  12.606 -  apply (rule Quotient_rel_abs [OF R1, THEN subst], assumption)
  12.607 +  apply (rule Quotient3_rel_abs [OF R2])
  12.608 +  apply (rule Quotient3_rel_abs [OF R1, THEN ssubst], assumption)
  12.609 +  apply (rule Quotient3_rel_abs [OF R1, THEN subst], assumption)
  12.610    apply (erule Abs1)
  12.611 -   apply (erule Quotient_refl2 [OF R1])
  12.612 -  apply (erule Quotient_refl1 [OF R1])
  12.613 +   apply (erule Quotient3_refl2 [OF R1])
  12.614 +  apply (erule Quotient3_refl1 [OF R1])
  12.615   apply (rename_tac a b c d)
  12.616   apply simp
  12.617   apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI)
  12.618 -  apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
  12.619 -  apply (rule conjI, erule Quotient_refl1 [OF R1])
  12.620 -  apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
  12.621 +  apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
  12.622 +  apply (rule conjI, erule Quotient3_refl1 [OF R1])
  12.623 +  apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1])
  12.624   apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated])
  12.625 -  apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
  12.626 -  apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
  12.627 -  apply (erule Quotient_refl2 [OF R1])
  12.628 +  apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
  12.629 +  apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1])
  12.630 +  apply (erule Quotient3_refl2 [OF R1])
  12.631   apply (rule Rep1)
  12.632   apply (drule Abs1)
  12.633 -   apply (erule Quotient_refl2 [OF R1])
  12.634 -  apply (erule Quotient_refl1 [OF R1])
  12.635 +   apply (erule Quotient3_refl2 [OF R1])
  12.636 +  apply (erule Quotient3_refl1 [OF R1])
  12.637   apply (drule Abs1)
  12.638 -  apply (erule Quotient_refl2 [OF R1])
  12.639 - apply (erule Quotient_refl1 [OF R1])
  12.640 - apply (drule Quotient_rel_abs [OF R1])
  12.641 - apply (drule Quotient_rel_abs [OF R1])
  12.642 - apply (drule Quotient_rel_abs [OF R1])
  12.643 - apply (drule Quotient_rel_abs [OF R1])
  12.644 +  apply (erule Quotient3_refl2 [OF R1])
  12.645 + apply (erule Quotient3_refl1 [OF R1])
  12.646 + apply (drule Quotient3_rel_abs [OF R1])
  12.647 + apply (drule Quotient3_rel_abs [OF R1])
  12.648 + apply (drule Quotient3_rel_abs [OF R1])
  12.649 + apply (drule Quotient3_rel_abs [OF R1])
  12.650   apply simp
  12.651 - apply (rule Quotient_rel[symmetric, OF R2, THEN iffD2])
  12.652 + apply (rule Quotient3_rel[symmetric, OF R2, THEN iffD2])
  12.653   apply simp
  12.654  done
  12.655  
  12.656 -lemma OOO_eq_quotient:
  12.657 +lemma OOO_eq_quotient3:
  12.658    fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  12.659    fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
  12.660    fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
  12.661 -  assumes R1: "Quotient R1 Abs1 Rep1"
  12.662 -  assumes R2: "Quotient op= Abs2 Rep2"
  12.663 -  shows "Quotient (R1 OOO op=) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
  12.664 +  assumes R1: "Quotient3 R1 Abs1 Rep1"
  12.665 +  assumes R2: "Quotient3 op= Abs2 Rep2"
  12.666 +  shows "Quotient3 (R1 OOO op=) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
  12.667  using assms
  12.668 -by (rule OOO_quotient) auto
  12.669 +by (rule OOO_quotient3) auto
  12.670  
  12.671  subsection {* Invariant *}
  12.672  
  12.673 -definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
  12.674 -  where "invariant R = (\<lambda>x y. R x \<and> x = y)"
  12.675 -
  12.676 -lemma invariant_to_eq:
  12.677 -  assumes "invariant P x y"
  12.678 -  shows "x = y"
  12.679 -using assms by (simp add: invariant_def)
  12.680 -
  12.681 -lemma fun_rel_eq_invariant:
  12.682 -  shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
  12.683 -by (auto simp add: invariant_def fun_rel_def)
  12.684 -
  12.685 -lemma invariant_same_args:
  12.686 -  shows "invariant P x x \<equiv> P x"
  12.687 -using assms by (auto simp add: invariant_def)
  12.688 -
  12.689 -lemma copy_type_to_Quotient:
  12.690 +lemma copy_type_to_Quotient3:
  12.691    assumes "type_definition Rep Abs UNIV"
  12.692 -  shows "Quotient (op =) Abs Rep"
  12.693 +  shows "Quotient3 (op =) Abs Rep"
  12.694  proof -
  12.695    interpret type_definition Rep Abs UNIV by fact
  12.696 -  from Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI)
  12.697 +  from Abs_inject Rep_inverse show ?thesis by (auto intro!: Quotient3I)
  12.698  qed
  12.699  
  12.700 -lemma copy_type_to_equivp:
  12.701 -  fixes Abs :: "'a \<Rightarrow> 'b"
  12.702 -  and Rep :: "'b \<Rightarrow> 'a"
  12.703 -  assumes "type_definition Rep Abs (UNIV::'a set)"
  12.704 -  shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
  12.705 -by (rule identity_equivp)
  12.706 -
  12.707 -lemma invariant_type_to_Quotient:
  12.708 +lemma invariant_type_to_Quotient3:
  12.709    assumes "type_definition Rep Abs {x. P x}"
  12.710 -  shows "Quotient (invariant P) Abs Rep"
  12.711 +  shows "Quotient3 (Lifting.invariant P) Abs Rep"
  12.712  proof -
  12.713    interpret type_definition Rep Abs "{x. P x}" by fact
  12.714 -  from Rep Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI simp: invariant_def)
  12.715 -qed
  12.716 -
  12.717 -lemma invariant_type_to_part_equivp:
  12.718 -  assumes "type_definition Rep Abs {x. P x}"
  12.719 -  shows "part_equivp (invariant P)"
  12.720 -proof (intro part_equivpI)
  12.721 -  interpret type_definition Rep Abs "{x. P x}" by fact
  12.722 -  show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def)
  12.723 -next
  12.724 -  show "symp (invariant P)" by (auto intro: sympI simp: invariant_def)
  12.725 -next
  12.726 -  show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
  12.727 +  from Rep Abs_inject Rep_inverse show ?thesis by (auto intro!: Quotient3I simp: invariant_def)
  12.728  qed
  12.729  
  12.730  subsection {* ML setup *}
  12.731 @@ -855,9 +797,9 @@
  12.732  use "Tools/Quotient/quotient_info.ML"
  12.733  setup Quotient_Info.setup
  12.734  
  12.735 -declare [[map "fun" = (fun_rel, fun_quotient)]]
  12.736 +declare [[mapQ3 "fun" = (fun_rel, fun_quotient3)]]
  12.737  
  12.738 -lemmas [quot_thm] = fun_quotient
  12.739 +lemmas [quot_thm] = fun_quotient3
  12.740  lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp
  12.741  lemmas [quot_preserve] = if_prs o_prs let_prs id_prs
  12.742  lemmas [quot_equiv] = identity_equivp
  12.743 @@ -960,6 +902,4 @@
  12.744    map_fun (infixr "--->" 55) and
  12.745    fun_rel (infixr "===>" 55)
  12.746  
  12.747 -hide_const (open) invariant
  12.748 -
  12.749  end
    13.1 --- a/src/HOL/Quotient_Examples/DList.thy	Tue Apr 03 14:09:37 2012 +0200
    13.2 +++ b/src/HOL/Quotient_Examples/DList.thy	Tue Apr 03 16:26:48 2012 +0200
    13.3 @@ -227,7 +227,7 @@
    13.4  lemma list_of_dlist_dlist [simp]:
    13.5    "list_of_dlist (dlist xs) = remdups xs"
    13.6    unfolding list_of_dlist_def map_fun_apply id_def
    13.7 -  by (metis Quotient_rep_abs[OF Quotient_dlist] dlist_eq_def)
    13.8 +  by (metis Quotient3_rep_abs[OF Quotient3_dlist] dlist_eq_def)
    13.9  
   13.10  lemma remdups_list_of_dlist [simp]:
   13.11    "remdups (list_of_dlist dxs) = list_of_dlist dxs"
   13.12 @@ -236,7 +236,7 @@
   13.13  lemma dlist_list_of_dlist [simp, code abstype]:
   13.14    "dlist (list_of_dlist dxs) = dxs"
   13.15    by (simp add: list_of_dlist_def)
   13.16 -  (metis Quotient_def Quotient_dlist dlist_eqI list_of_dlist_dlist remdups_list_of_dlist)
   13.17 +  (metis Quotient3_def Quotient3_dlist dlist_eqI list_of_dlist_dlist remdups_list_of_dlist)
   13.18  
   13.19  lemma dlist_filter_simps:
   13.20    "filter P empty = empty"
    14.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Tue Apr 03 14:09:37 2012 +0200
    14.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Tue Apr 03 16:26:48 2012 +0200
    14.3 @@ -1,4 +1,4 @@
    14.4 -(*  Title:      HOL/Quotient_Examples/FSet.thy
    14.5 +(*  Title:      HOL/Quotient3_Examples/FSet.thy
    14.6      Author:     Cezary Kaliszyk, TU Munich
    14.7      Author:     Christian Urban, TU Munich
    14.8  
    14.9 @@ -117,15 +117,15 @@
   14.10    by (simp only: list_eq_def set_map)
   14.11  
   14.12  lemma quotient_compose_list_g:
   14.13 -  assumes q: "Quotient R Abs Rep"
   14.14 +  assumes q: "Quotient3 R Abs Rep"
   14.15    and     e: "equivp R"
   14.16 -  shows  "Quotient ((list_all2 R) OOO (op \<approx>))
   14.17 +  shows  "Quotient3 ((list_all2 R) OOO (op \<approx>))
   14.18      (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)"
   14.19 -  unfolding Quotient_def comp_def
   14.20 +  unfolding Quotient3_def comp_def
   14.21  proof (intro conjI allI)
   14.22    fix a r s
   14.23    show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
   14.24 -    by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] List.map.id)
   14.25 +    by (simp add: abs_o_rep[OF q] Quotient3_abs_rep[OF Quotient3_fset] List.map.id)
   14.26    have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
   14.27      by (rule list_all2_refl'[OF e])
   14.28    have c: "(op \<approx> OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
   14.29 @@ -146,37 +146,37 @@
   14.30        assume d: "b \<approx> ba"
   14.31        assume e: "list_all2 R ba s"
   14.32        have f: "map Abs r = map Abs b"
   14.33 -        using Quotient_rel[OF list_quotient[OF q]] c by blast
   14.34 +        using Quotient3_rel[OF list_quotient3[OF q]] c by blast
   14.35        have "map Abs ba = map Abs s"
   14.36 -        using Quotient_rel[OF list_quotient[OF q]] e by blast
   14.37 +        using Quotient3_rel[OF list_quotient3[OF q]] e by blast
   14.38        then have g: "map Abs s = map Abs ba" by simp
   14.39        then show "map Abs r \<approx> map Abs s" using d f map_list_eq_cong by simp
   14.40      qed
   14.41      then show "abs_fset (map Abs r) = abs_fset (map Abs s)"
   14.42 -      using Quotient_rel[OF Quotient_fset] by blast
   14.43 +      using Quotient3_rel[OF Quotient3_fset] by blast
   14.44    next
   14.45      assume a: "(list_all2 R OOO op \<approx>) r r \<and> (list_all2 R OOO op \<approx>) s s
   14.46        \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
   14.47      then have s: "(list_all2 R OOO op \<approx>) s s" by simp
   14.48      have d: "map Abs r \<approx> map Abs s"
   14.49 -      by (subst Quotient_rel [OF Quotient_fset, symmetric]) (simp add: a)
   14.50 +      by (subst Quotient3_rel [OF Quotient3_fset, symmetric]) (simp add: a)
   14.51      have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
   14.52        by (rule map_list_eq_cong[OF d])
   14.53      have y: "list_all2 R (map Rep (map Abs s)) s"
   14.54 -      by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl'[OF e, of s]])
   14.55 +      by (fact rep_abs_rsp_left[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of s]])
   14.56      have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"
   14.57        by (rule pred_compI) (rule b, rule y)
   14.58      have z: "list_all2 R r (map Rep (map Abs r))"
   14.59 -      by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl'[OF e, of r]])
   14.60 +      by (fact rep_abs_rsp[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of r]])
   14.61      then show "(list_all2 R OOO op \<approx>) r s"
   14.62        using a c pred_compI by simp
   14.63    qed
   14.64  qed
   14.65  
   14.66  lemma quotient_compose_list[quot_thm]:
   14.67 -  shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))
   14.68 +  shows  "Quotient3 ((list_all2 op \<approx>) OOO (op \<approx>))
   14.69      (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
   14.70 -  by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp)
   14.71 +  by (rule quotient_compose_list_g, rule Quotient3_fset, rule list_eq_equivp)
   14.72  
   14.73  
   14.74  section {* Quotient definitions for fsets *}
   14.75 @@ -404,19 +404,19 @@
   14.76    done
   14.77  
   14.78  lemma Nil_prs2 [quot_preserve]:
   14.79 -  assumes "Quotient R Abs Rep"
   14.80 +  assumes "Quotient3 R Abs Rep"
   14.81    shows "(Abs \<circ> map f) [] = Abs []"
   14.82    by simp
   14.83  
   14.84  lemma Cons_prs2 [quot_preserve]:
   14.85 -  assumes q: "Quotient R1 Abs1 Rep1"
   14.86 -  and     r: "Quotient R2 Abs2 Rep2"
   14.87 +  assumes q: "Quotient3 R1 Abs1 Rep1"
   14.88 +  and     r: "Quotient3 R2 Abs2 Rep2"
   14.89    shows "(Rep1 ---> (map Rep1 \<circ> Rep2) ---> (Abs2 \<circ> map Abs1)) (op #) = (id ---> Rep2 ---> Abs2) (op #)"
   14.90 -  by (auto simp add: fun_eq_iff comp_def Quotient_abs_rep [OF q])
   14.91 +  by (auto simp add: fun_eq_iff comp_def Quotient3_abs_rep [OF q])
   14.92  
   14.93  lemma append_prs2 [quot_preserve]:
   14.94 -  assumes q: "Quotient R1 Abs1 Rep1"
   14.95 -  and     r: "Quotient R2 Abs2 Rep2"
   14.96 +  assumes q: "Quotient3 R1 Abs1 Rep1"
   14.97 +  and     r: "Quotient3 R2 Abs2 Rep2"
   14.98    shows "((map Rep1 \<circ> Rep2) ---> (map Rep1 \<circ> Rep2) ---> (Abs2 \<circ> map Abs1)) op @ =
   14.99      (Rep2 ---> Rep2 ---> Abs2) op @"
  14.100    by (simp add: fun_eq_iff abs_o_rep[OF q] List.map.id)
  14.101 @@ -485,7 +485,7 @@
  14.102  lemma map_prs2 [quot_preserve]:
  14.103    shows "((abs_fset ---> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> abs_fset \<circ> map abs_fset) map = (id ---> rep_fset ---> abs_fset) map"
  14.104    by (auto simp add: fun_eq_iff)
  14.105 -     (simp only: map_map[symmetric] map_prs_aux[OF Quotient_fset Quotient_fset])
  14.106 +     (simp only: map_map[symmetric] map_prs_aux[OF Quotient3_fset Quotient3_fset])
  14.107  
  14.108  section {* Lifted theorems *}
  14.109  
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/Quotient_Examples/Lift_DList.thy	Tue Apr 03 16:26:48 2012 +0200
    15.3 @@ -0,0 +1,86 @@
    15.4 +(*  Title:      HOL/Quotient_Examples/Lift_DList.thy
    15.5 +    Author:     Ondrej Kuncar
    15.6 +*)
    15.7 +
    15.8 +theory Lift_DList
    15.9 +imports Main "~~/src/HOL/Library/Quotient_List"
   15.10 +begin
   15.11 +
   15.12 +subsection {* The type of distinct lists *}
   15.13 +
   15.14 +typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
   15.15 +  morphisms list_of_dlist Abs_dlist
   15.16 +proof
   15.17 +  show "[] \<in> {xs. distinct xs}" by simp
   15.18 +qed
   15.19 +
   15.20 +setup_lifting type_definition_dlist
   15.21 +
   15.22 +text {* Fundamental operations: *}
   15.23 +
   15.24 +lift_definition empty :: "'a dlist" is "[]"
   15.25 +by simp
   15.26 +  
   15.27 +lift_definition insert :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" is List.insert
   15.28 +by simp
   15.29 +
   15.30 +lift_definition remove :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" is List.remove1
   15.31 +by simp
   15.32 +
   15.33 +lift_definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist" is "\<lambda>f. remdups o List.map f"
   15.34 +by simp
   15.35 +
   15.36 +lift_definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" is List.filter
   15.37 +by simp
   15.38 +
   15.39 +text {* Derived operations: *}
   15.40 +
   15.41 +lift_definition null :: "'a dlist \<Rightarrow> bool" is List.null
   15.42 +by simp
   15.43 +
   15.44 +lift_definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" is List.member
   15.45 +by simp
   15.46 +
   15.47 +lift_definition length :: "'a dlist \<Rightarrow> nat" is List.length
   15.48 +by simp
   15.49 +
   15.50 +lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.fold
   15.51 +by simp
   15.52 +
   15.53 +lift_definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.foldr
   15.54 +by simp
   15.55 +
   15.56 +lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat"
   15.57 +proof -
   15.58 +  {
   15.59 +    fix x y
   15.60 +    have "list_all2 cr_dlist x y \<Longrightarrow> 
   15.61 +      List.map Abs_dlist x = y \<and> list_all2 (Lifting.invariant distinct) x x"
   15.62 +      unfolding list_all2_def cr_dlist_def by (induction x y rule: list_induct2') auto
   15.63 +  }
   15.64 +  note cr = this
   15.65 +
   15.66 +  fix x :: "'a list list" and y :: "'a list list"
   15.67 +  assume a: "(list_all2 cr_dlist OO Lifting.invariant distinct OO (list_all2 cr_dlist)\<inverse>\<inverse>) x y"
   15.68 +  from a have l_x: "list_all2 (Lifting.invariant distinct) x x" by (auto simp add: cr)
   15.69 +  from a have l_y: "list_all2 (Lifting.invariant distinct) y y" by (auto simp add: cr)
   15.70 +  from a have m: "(Lifting.invariant distinct) (List.map Abs_dlist x) (List.map Abs_dlist y)" 
   15.71 +    by (auto simp add: cr)
   15.72 +
   15.73 +  have "x = y" 
   15.74 +  proof -
   15.75 +    have m':"List.map Abs_dlist x = List.map Abs_dlist y" using m unfolding Lifting.invariant_def by simp
   15.76 +    have dist: "\<And>l. list_all2 (Lifting.invariant distinct) l l \<Longrightarrow> !x. x \<in> (set l) \<longrightarrow> distinct x"
   15.77 +      unfolding list_all2_def Lifting.invariant_def by (auto simp add: zip_same)
   15.78 +    from dist[OF l_x] dist[OF l_y] have "inj_on Abs_dlist (set x \<union> set y)" by (intro inj_onI) 
   15.79 +      (metis CollectI UnE Abs_dlist_inverse)
   15.80 +    with m' show ?thesis by (rule map_inj_on)
   15.81 +  qed
   15.82 +  then show "?thesis x y" unfolding Lifting.invariant_def by auto
   15.83 +qed
   15.84 +
   15.85 +text {* We can export code: *}
   15.86 +
   15.87 +export_code empty insert remove map filter null member length fold foldr concat in SML
   15.88 +
   15.89 +end
    16.1 --- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Tue Apr 03 14:09:37 2012 +0200
    16.2 +++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Tue Apr 03 16:26:48 2012 +0200
    16.3 @@ -1,4 +1,4 @@
    16.4 -(*  Title:      HOL/Quotient_Examples/Lift_Fun.thy
    16.5 +(*  Title:      HOL/Quotient3_Examples/Lift_Fun.thy
    16.6      Author:     Ondrej Kuncar
    16.7  *)
    16.8  
    16.9 @@ -53,12 +53,12 @@
   16.10  
   16.11  enriched_type map_endofun : map_endofun
   16.12  proof -
   16.13 -  have "\<forall> x. abs_endofun (rep_endofun x) = x" using Quotient_endofun by (auto simp: Quotient_def)
   16.14 +  have "\<forall> x. abs_endofun (rep_endofun x) = x" using Quotient3_endofun by (auto simp: Quotient3_def)
   16.15    then show "map_endofun id id = id" 
   16.16      by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff)
   16.17    
   16.18 -  have a:"\<forall> x. rep_endofun (abs_endofun x) = x" using Quotient_endofun 
   16.19 -    Quotient_rep_abs[of "(op =)" abs_endofun rep_endofun] by blast
   16.20 +  have a:"\<forall> x. rep_endofun (abs_endofun x) = x" using Quotient3_endofun 
   16.21 +    Quotient3_rep_abs[of "(op =)" abs_endofun rep_endofun] by blast
   16.22    show "\<And>f g h i. map_endofun f g \<circ> map_endofun h i = map_endofun (f \<circ> h) (i \<circ> g)"
   16.23      by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc) 
   16.24  qed
   16.25 @@ -74,34 +74,34 @@
   16.26    endofun_rel' done
   16.27  
   16.28  lemma endofun_quotient:
   16.29 -assumes a: "Quotient R Abs Rep"
   16.30 -shows "Quotient (endofun_rel R) (map_endofun Abs Rep) (map_endofun Rep Abs)"
   16.31 -proof (intro QuotientI)
   16.32 +assumes a: "Quotient3 R Abs Rep"
   16.33 +shows "Quotient3 (endofun_rel R) (map_endofun Abs Rep) (map_endofun Rep Abs)"
   16.34 +proof (intro Quotient3I)
   16.35    show "\<And>a. map_endofun Abs Rep (map_endofun Rep Abs a) = a"
   16.36      by (metis (hide_lams, no_types) a abs_o_rep id_apply map_endofun.comp map_endofun.id o_eq_dest_lhs)
   16.37  next
   16.38    show "\<And>a. endofun_rel R (map_endofun Rep Abs a) (map_endofun Rep Abs a)"
   16.39 -  using fun_quotient[OF a a, THEN Quotient_rep_reflp]
   16.40 +  using fun_quotient3[OF a a, THEN Quotient3_rep_reflp]
   16.41    unfolding endofun_rel_def map_endofun_def map_fun_def o_def map_endofun'_def endofun_rel'_def id_def 
   16.42 -    by (metis (mono_tags) Quotient_endofun rep_abs_rsp)
   16.43 +    by (metis (mono_tags) Quotient3_endofun rep_abs_rsp)
   16.44  next
   16.45    have abs_to_eq: "\<And> x y. abs_endofun x = abs_endofun y \<Longrightarrow> x = y" 
   16.46 -  by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient_rep_abs[OF Quotient_endofun])
   16.47 +  by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient3_rep_abs[OF Quotient3_endofun])
   16.48    fix r s
   16.49    show "endofun_rel R r s =
   16.50            (endofun_rel R r r \<and>
   16.51             endofun_rel R s s \<and> map_endofun Abs Rep r = map_endofun Abs Rep s)"
   16.52      apply(auto simp add: endofun_rel_def endofun_rel'_def map_endofun_def map_endofun'_def)
   16.53 -    using fun_quotient[OF a a,THEN Quotient_refl1]
   16.54 +    using fun_quotient3[OF a a,THEN Quotient3_refl1]
   16.55      apply metis
   16.56 -    using fun_quotient[OF a a,THEN Quotient_refl2]
   16.57 +    using fun_quotient3[OF a a,THEN Quotient3_refl2]
   16.58      apply metis
   16.59 -    using fun_quotient[OF a a, THEN Quotient_rel]
   16.60 +    using fun_quotient3[OF a a, THEN Quotient3_rel]
   16.61      apply metis
   16.62 -    by (auto intro: fun_quotient[OF a a, THEN Quotient_rel, THEN iffD1] simp add: abs_to_eq)
   16.63 +    by (auto intro: fun_quotient3[OF a a, THEN Quotient3_rel, THEN iffD1] simp add: abs_to_eq)
   16.64  qed
   16.65  
   16.66 -declare [[map endofun = (endofun_rel, endofun_quotient)]]
   16.67 +declare [[mapQ3 endofun = (endofun_rel, endofun_quotient)]]
   16.68  
   16.69  quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" done
   16.70  
    17.1 --- a/src/HOL/Quotient_Examples/Lift_RBT.thy	Tue Apr 03 14:09:37 2012 +0200
    17.2 +++ b/src/HOL/Quotient_Examples/Lift_RBT.thy	Tue Apr 03 16:26:48 2012 +0200
    17.3 @@ -1,4 +1,6 @@
    17.4 -(* Author: Lukas Bulwahn, TU Muenchen *)
    17.5 +(*  Title:      HOL/Quotient_Examples/Lift_RBT.thy
    17.6 +    Author:     Lukas Bulwahn and Ondrej Kuncar
    17.7 +*)
    17.8  
    17.9  header {* Lifting operations of RBT trees *}
   17.10  
   17.11 @@ -35,53 +37,35 @@
   17.12  
   17.13  setup_lifting type_definition_rbt
   17.14  
   17.15 -quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup"
   17.16 +lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup" 
   17.17 +by simp
   17.18 +
   17.19 +lift_definition empty :: "('a\<Colon>linorder, 'b) rbt" is RBT_Impl.Empty 
   17.20 +by (simp add: empty_def)
   17.21 +
   17.22 +lift_definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.insert" 
   17.23 +by simp
   17.24 +
   17.25 +lift_definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.delete" 
   17.26 +by simp
   17.27 +
   17.28 +lift_definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries
   17.29  by simp
   17.30  
   17.31 -(* FIXME: quotient_definition at the moment requires that types variables match exactly,
   17.32 -i.e., sort constraints must be annotated to the constant being lifted.
   17.33 -But, it should be possible to infer the necessary sort constraints, making the explicit
   17.34 -sort constraints unnecessary.
   17.35 -
   17.36 -Hence this unannotated quotient_definition fails:
   17.37 -
   17.38 -quotient_definition empty where "empty :: ('a\<Colon>linorder, 'b) rbt"
   17.39 -is "RBT_Impl.Empty"
   17.40 -
   17.41 -Similar issue for quotient_definition for entries, keys, map, and fold.
   17.42 -*)
   17.43 -
   17.44 -quotient_definition empty where "empty :: ('a\<Colon>linorder, 'b) rbt"
   17.45 -is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)" by (simp add: empty_def)
   17.46 -
   17.47 -quotient_definition insert where "insert :: 'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
   17.48 -is "RBT_Impl.insert" by simp
   17.49 +lift_definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys 
   17.50 +by simp
   17.51  
   17.52 -quotient_definition delete where "delete :: 'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
   17.53 -is "RBT_Impl.delete" by simp
   17.54 -
   17.55 -(* FIXME: unnecessary type annotations *)
   17.56 -quotient_definition "entries :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
   17.57 -is "RBT_Impl.entries :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a \<times> 'b) list" by simp
   17.58 -
   17.59 -(* FIXME: unnecessary type annotations *)
   17.60 -quotient_definition "keys :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list"
   17.61 -is "RBT_Impl.keys :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a list" by simp
   17.62 -
   17.63 -quotient_definition "bulkload :: ('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt"
   17.64 -is "RBT_Impl.bulkload" by simp
   17.65 -
   17.66 -quotient_definition "map_entry :: 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
   17.67 -is "RBT_Impl.map_entry" by simp
   17.68 -
   17.69 -(* FIXME: unnecesary type annotations *)
   17.70 -quotient_definition map where "map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
   17.71 -is "RBT_Impl.map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a, 'b) RBT_Impl.rbt"
   17.72 +lift_definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.bulkload" 
   17.73  by simp
   17.74  
   17.75 -(* FIXME: unnecessary type annotations *)
   17.76 -quotient_definition fold where "fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" 
   17.77 -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
   17.78 +lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is RBT_Impl.map_entry 
   17.79 +by simp
   17.80 +
   17.81 +lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is RBT_Impl.map
   17.82 +by simp
   17.83 +
   17.84 +lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"  is RBT_Impl.fold 
   17.85 +by simp
   17.86  
   17.87  export_code lookup empty insert delete entries keys bulkload map_entry map fold in SML
   17.88  
    18.1 --- a/src/HOL/Quotient_Examples/Lift_Set.thy	Tue Apr 03 14:09:37 2012 +0200
    18.2 +++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Tue Apr 03 16:26:48 2012 +0200
    18.3 @@ -2,7 +2,7 @@
    18.4      Author:     Lukas Bulwahn and Ondrej Kuncar
    18.5  *)
    18.6  
    18.7 -header {* Example of lifting definitions with the quotient infrastructure *}
    18.8 +header {* Example of lifting definitions with the lifting infrastructure *}
    18.9  
   18.10  theory Lift_Set
   18.11  imports Main
   18.12 @@ -16,19 +16,14 @@
   18.13  
   18.14  setup_lifting type_definition_set[unfolded set_def]
   18.15  
   18.16 -text {* Now, we can employ quotient_definition to lift definitions. *}
   18.17 +text {* Now, we can employ lift_definition to lift definitions. *}
   18.18  
   18.19 -quotient_definition empty where "empty :: 'a set"
   18.20 -is "bot :: 'a \<Rightarrow> bool" done
   18.21 +lift_definition empty :: "'a set" is "bot :: 'a \<Rightarrow> bool" done
   18.22  
   18.23  term "Lift_Set.empty"
   18.24  thm Lift_Set.empty_def
   18.25  
   18.26 -definition insertp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
   18.27 -  "insertp x P y \<longleftrightarrow> y = x \<or> P y"
   18.28 -
   18.29 -quotient_definition insert where "insert :: 'a => 'a set => 'a set"
   18.30 -is insertp done
   18.31 +lift_definition insert :: "'a => 'a set => 'a set" is "\<lambda> x P y. y = x \<or> P y" done 
   18.32  
   18.33  term "Lift_Set.insert"
   18.34  thm Lift_Set.insert_def
    19.1 --- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Tue Apr 03 14:09:37 2012 +0200
    19.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Tue Apr 03 16:26:48 2012 +0200
    19.3 @@ -145,9 +145,9 @@
    19.4     (abs_int (x + u, y + v))"
    19.5    apply(simp add: plus_int_def id_simps)
    19.6    apply(fold plus_int_raw.simps)
    19.7 -  apply(rule Quotient_rel_abs[OF Quotient_int])
    19.8 +  apply(rule Quotient3_rel_abs[OF Quotient3_int])
    19.9    apply(rule plus_int_raw_rsp_aux)
   19.10 -  apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
   19.11 +  apply(simp_all add: rep_abs_rsp_left[OF Quotient3_int])
   19.12    done
   19.13  
   19.14  definition int_of_nat_raw:
    20.1 --- a/src/HOL/Quotient_Examples/ROOT.ML	Tue Apr 03 14:09:37 2012 +0200
    20.2 +++ b/src/HOL/Quotient_Examples/ROOT.ML	Tue Apr 03 16:26:48 2012 +0200
    20.3 @@ -5,5 +5,5 @@
    20.4  *)
    20.5  
    20.6  use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message",
    20.7 -  "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat"];
    20.8 +  "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat", "Lift_DList"];
    20.9  
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue Apr 03 16:26:48 2012 +0200
    21.3 @@ -0,0 +1,291 @@
    21.4 +(*  Title:      HOL/Tools/Lifting/lifting_def.ML
    21.5 +    Author:     Ondrej Kuncar
    21.6 +
    21.7 +Definitions for constants on quotient types.
    21.8 +*)
    21.9 +
   21.10 +signature LIFTING_DEF =
   21.11 +sig
   21.12 +  val add_lift_def:
   21.13 +    (binding * mixfix) -> typ -> term -> thm -> local_theory -> local_theory
   21.14 +
   21.15 +  val lift_def_cmd:
   21.16 +    (binding * string option * mixfix) * string -> local_theory -> Proof.state
   21.17 +
   21.18 +  val can_generate_code_cert: thm -> bool
   21.19 +end;
   21.20 +
   21.21 +structure Lifting_Def: LIFTING_DEF =
   21.22 +struct
   21.23 +
   21.24 +(** Interface and Syntax Setup **)
   21.25 +
   21.26 +(* Generation of the code certificate from the rsp theorem *)
   21.27 +
   21.28 +infix 0 MRSL
   21.29 +
   21.30 +fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
   21.31 +
   21.32 +fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
   21.33 +  | get_body_types (U, V)  = (U, V)
   21.34 +
   21.35 +fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
   21.36 +  | get_binder_types _ = []
   21.37 +
   21.38 +fun force_rty_type ctxt rty rhs = 
   21.39 +  let
   21.40 +    val thy = Proof_Context.theory_of ctxt
   21.41 +    val rhs_schematic = singleton (Variable.polymorphic ctxt) rhs
   21.42 +    val rty_schematic = fastype_of rhs_schematic
   21.43 +    val match = Sign.typ_match thy (rty_schematic, rty) Vartab.empty
   21.44 +  in
   21.45 +    Envir.subst_term_types match rhs_schematic
   21.46 +  end
   21.47 +
   21.48 +fun unabs_def ctxt def = 
   21.49 +  let
   21.50 +    val (_, rhs) = Thm.dest_equals (cprop_of def)
   21.51 +    fun dest_abs (Abs (var_name, T, _)) = (var_name, T)
   21.52 +      | dest_abs tm = raise TERM("get_abs_var",[tm])
   21.53 +    val (var_name, T) = dest_abs (term_of rhs)
   21.54 +    val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt
   21.55 +    val thy = Proof_Context.theory_of ctxt'
   21.56 +    val refl_thm = Thm.reflexive (cterm_of thy (Free (hd new_var_names, T)))
   21.57 +  in
   21.58 +    Thm.combination def refl_thm |>
   21.59 +    singleton (Proof_Context.export ctxt' ctxt)
   21.60 +  end
   21.61 +
   21.62 +fun unabs_all_def ctxt def = 
   21.63 +  let
   21.64 +    val (_, rhs) = Thm.dest_equals (cprop_of def)
   21.65 +    val xs = strip_abs_vars (term_of rhs)
   21.66 +  in  
   21.67 +    fold (K (unabs_def ctxt)) xs def
   21.68 +  end
   21.69 +
   21.70 +val map_fun_unfolded = 
   21.71 +  @{thm map_fun_def[abs_def]} |>
   21.72 +  unabs_def @{context} |>
   21.73 +  unabs_def @{context} |>
   21.74 +  Local_Defs.unfold @{context} [@{thm comp_def}]
   21.75 +
   21.76 +fun unfold_fun_maps ctm =
   21.77 +  let
   21.78 +    fun unfold_conv ctm =
   21.79 +      case (Thm.term_of ctm) of
   21.80 +        Const (@{const_name "map_fun"}, _) $ _ $ _ => 
   21.81 +          (Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm
   21.82 +        | _ => Conv.all_conv ctm
   21.83 +    val try_beta_conv = Conv.try_conv (Thm.beta_conversion false)
   21.84 +  in
   21.85 +    (Conv.arg_conv (Conv.fun_conv unfold_conv then_conv try_beta_conv)) ctm
   21.86 +  end
   21.87 +
   21.88 +fun prove_rel ctxt rsp_thm (rty, qty) =
   21.89 +  let
   21.90 +    val ty_args = get_binder_types (rty, qty)
   21.91 +    fun disch_arg args_ty thm = 
   21.92 +      let
   21.93 +        val quot_thm = Lifting_Term.prove_quot_theorem ctxt args_ty
   21.94 +      in
   21.95 +        [quot_thm, thm] MRSL @{thm apply_rsp''}
   21.96 +      end
   21.97 +  in
   21.98 +    fold disch_arg ty_args rsp_thm
   21.99 +  end
  21.100 +
  21.101 +exception CODE_CERT_GEN of string
  21.102 +
  21.103 +fun simplify_code_eq ctxt def_thm = 
  21.104 +  Local_Defs.unfold ctxt [@{thm o_def}, @{thm map_fun_def}, @{thm id_def}] def_thm
  21.105 +
  21.106 +fun can_generate_code_cert quot_thm  =
  21.107 +  case Lifting_Term.quot_thm_rel quot_thm of
  21.108 +    Const (@{const_name HOL.eq}, _) => true
  21.109 +    | Const (@{const_name invariant}, _) $ _  => true
  21.110 +    | _ => false
  21.111 +
  21.112 +fun generate_code_cert ctxt def_thm rsp_thm (rty, qty) =
  21.113 +  let
  21.114 +    val thy = Proof_Context.theory_of ctxt
  21.115 +    val quot_thm = Lifting_Term.prove_quot_theorem ctxt (get_body_types (rty, qty))
  21.116 +    val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
  21.117 +    val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs}
  21.118 +    val abs_rep_eq = 
  21.119 +      case (HOLogic.dest_Trueprop o prop_of) fun_rel of
  21.120 +        Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm
  21.121 +        | Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq}
  21.122 +        | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant"
  21.123 +    val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
  21.124 +    val unabs_def = unabs_all_def ctxt unfolded_def
  21.125 +    val rep = (cterm_of thy o Lifting_Term.quot_thm_rep) quot_thm
  21.126 +    val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
  21.127 +    val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
  21.128 +    val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans}
  21.129 +  in
  21.130 +    simplify_code_eq ctxt code_cert
  21.131 +  end
  21.132 +
  21.133 +fun define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = 
  21.134 +  let
  21.135 +    val quot_thm = Lifting_Term.prove_quot_theorem lthy (get_body_types (rty, qty))
  21.136 +  in
  21.137 +    if can_generate_code_cert quot_thm then
  21.138 +      let
  21.139 +        val code_cert = generate_code_cert lthy def_thm rsp_thm (rty, qty)
  21.140 +        val add_abs_eqn_attribute = 
  21.141 +          Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I)
  21.142 +        val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
  21.143 +      in
  21.144 +        lthy
  21.145 +          |> (snd oo Local_Theory.note) ((code_eqn_thm_name, [add_abs_eqn_attrib]), [code_cert])
  21.146 +      end
  21.147 +    else
  21.148 +      lthy
  21.149 +  end
  21.150 +
  21.151 +fun define_code_eq code_eqn_thm_name def_thm lthy =
  21.152 +  let
  21.153 +    val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
  21.154 +    val code_eq = unabs_all_def lthy unfolded_def
  21.155 +    val simp_code_eq = simplify_code_eq lthy code_eq
  21.156 +  in
  21.157 +    lthy
  21.158 +      |> (snd oo Local_Theory.note) ((code_eqn_thm_name, [Code.add_default_eqn_attrib]), [simp_code_eq])
  21.159 +  end
  21.160 +
  21.161 +fun define_code code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy =
  21.162 +  if body_type rty = body_type qty then 
  21.163 +    define_code_eq code_eqn_thm_name def_thm lthy
  21.164 +  else 
  21.165 +    define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy
  21.166 +
  21.167 +
  21.168 +fun add_lift_def var qty rhs rsp_thm lthy =
  21.169 +  let
  21.170 +    val rty = fastype_of rhs
  21.171 +    val absrep_trm =  Lifting_Term.absrep_fun lthy (rty, qty)
  21.172 +    val rty_forced = (domain_type o fastype_of) absrep_trm
  21.173 +    val forced_rhs = force_rty_type lthy rty_forced rhs
  21.174 +    val lhs = Free (Binding.print (#1 var), qty)
  21.175 +    val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs)
  21.176 +    val (_, prop') = Local_Defs.cert_def lthy prop
  21.177 +    val (_, newrhs) = Local_Defs.abs_def prop'
  21.178 +
  21.179 +    val ((_, (_ , def_thm)), lthy') = 
  21.180 +      Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
  21.181 +
  21.182 +    fun qualify defname suffix = Binding.name suffix
  21.183 +      |> Binding.qualify true defname
  21.184 +
  21.185 +    val lhs_name = Binding.name_of (#1 var)
  21.186 +    val rsp_thm_name = qualify lhs_name "rsp"
  21.187 +    val code_eqn_thm_name = qualify lhs_name "rep_eq"
  21.188 +  in
  21.189 +    lthy'
  21.190 +      |> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm])
  21.191 +      |> define_code code_eqn_thm_name def_thm rsp_thm (rty_forced, qty)
  21.192 +  end
  21.193 +
  21.194 +fun mk_readable_rsp_thm_eq tm lthy =
  21.195 +  let
  21.196 +    val ctm = cterm_of (Proof_Context.theory_of lthy) tm
  21.197 +    
  21.198 +    fun norm_fun_eq ctm = 
  21.199 +      let
  21.200 +        fun abs_conv2 cv = Conv.abs_conv (K (Conv.abs_conv (K cv) lthy)) lthy
  21.201 +        fun erase_quants ctm' =
  21.202 +          case (Thm.term_of ctm') of
  21.203 +            Const ("HOL.eq", _) $ _ $ _ => Conv.all_conv ctm'
  21.204 +            | _ => (Conv.binder_conv (K erase_quants) lthy then_conv 
  21.205 +              Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
  21.206 +      in
  21.207 +        (abs_conv2 erase_quants then_conv Thm.eta_conversion) ctm
  21.208 +      end
  21.209 +
  21.210 +    fun simp_arrows_conv ctm =
  21.211 +      let
  21.212 +        val unfold_conv = Conv.rewrs_conv 
  21.213 +          [@{thm fun_rel_eq_invariant[THEN eq_reflection]}, @{thm fun_rel_eq_rel[THEN eq_reflection]}, 
  21.214 +            @{thm fun_rel_def[THEN eq_reflection]}]
  21.215 +        val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
  21.216 +        fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
  21.217 +      in
  21.218 +        case (Thm.term_of ctm) of
  21.219 +          Const (@{const_name "fun_rel"}, _) $ _ $ _ => 
  21.220 +            (binop_conv2  left_conv simp_arrows_conv then_conv unfold_conv) ctm
  21.221 +          | _ => Conv.all_conv ctm
  21.222 +      end
  21.223 +
  21.224 +    val unfold_ret_val_invs = Conv.bottom_conv 
  21.225 +      (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy 
  21.226 +    val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
  21.227 +    val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
  21.228 +    val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
  21.229 +    val beta_conv = Thm.beta_conversion true
  21.230 +    val eq_thm = 
  21.231 +      (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
  21.232 +  in
  21.233 +    Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2)
  21.234 +  end
  21.235 +
  21.236 +
  21.237 +
  21.238 +fun lift_def_cmd (raw_var, rhs_raw) lthy =
  21.239 +  let
  21.240 +    val ((binding, SOME qty, mx), ctxt) = yield_singleton Proof_Context.read_vars raw_var lthy 
  21.241 +    val rhs = (Syntax.check_term ctxt o Syntax.parse_term ctxt) rhs_raw
  21.242 + 
  21.243 +    fun try_to_prove_refl thm = 
  21.244 +      let
  21.245 +        val lhs_eq =
  21.246 +          thm
  21.247 +          |> prop_of
  21.248 +          |> Logic.dest_implies
  21.249 +          |> fst
  21.250 +          |> strip_all_body
  21.251 +          |> try HOLogic.dest_Trueprop
  21.252 +      in
  21.253 +        case lhs_eq of
  21.254 +          SOME (Const ("HOL.eq", _) $ _ $ _) => SOME (@{thm refl} RS thm)
  21.255 +          | _ => NONE
  21.256 +      end
  21.257 +
  21.258 +    val rsp_rel = Lifting_Term.equiv_relation lthy (fastype_of rhs, qty)
  21.259 +    val rty_forced = (domain_type o fastype_of) rsp_rel;
  21.260 +    val forced_rhs = force_rty_type lthy rty_forced rhs;
  21.261 +    val internal_rsp_tm = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
  21.262 +    val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy
  21.263 +    val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
  21.264 +    val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq)
  21.265 +  
  21.266 +    fun after_qed thm_list lthy = 
  21.267 +      let
  21.268 +        val internal_rsp_thm =
  21.269 +          case thm_list of
  21.270 +            [] => the maybe_proven_rsp_thm
  21.271 +          | [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm 
  21.272 +            (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1)
  21.273 +      in
  21.274 +        add_lift_def (binding, mx) qty rhs internal_rsp_thm lthy
  21.275 +      end
  21.276 +
  21.277 +  in
  21.278 +    case maybe_proven_rsp_thm of
  21.279 +      SOME _ => Proof.theorem NONE after_qed [] lthy
  21.280 +      | NONE =>  Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy
  21.281 +  end
  21.282 +
  21.283 +(* parser and command *)
  21.284 +val liftdef_parser =
  21.285 +  ((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2)
  21.286 +    --| @{keyword "is"} -- Parse.term
  21.287 +
  21.288 +val _ =
  21.289 +  Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"}
  21.290 +    "definition for constants over the quotient type"
  21.291 +      (liftdef_parser >> lift_def_cmd)
  21.292 +
  21.293 +
  21.294 +end; (* structure *)
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Tue Apr 03 16:26:48 2012 +0200
    22.3 @@ -0,0 +1,125 @@
    22.4 +(*  Title:      HOL/Tools/Lifting/lifting_info.ML
    22.5 +    Author:     Ondrej Kuncar
    22.6 +
    22.7 +Context data for the lifting package.
    22.8 +*)
    22.9 +
   22.10 +signature LIFTING_INFO =
   22.11 +sig
   22.12 +  type quotmaps = {relmap: string, quot_thm: thm}
   22.13 +  val lookup_quotmaps: Proof.context -> string -> quotmaps option
   22.14 +  val lookup_quotmaps_global: theory -> string -> quotmaps option
   22.15 +  val print_quotmaps: Proof.context -> unit
   22.16 +
   22.17 +  type quotients = {quot_thm: thm}
   22.18 +  val transform_quotients: morphism -> quotients -> quotients
   22.19 +  val lookup_quotients: Proof.context -> string -> quotients option
   22.20 +  val lookup_quotients_global: theory -> string -> quotients option
   22.21 +  val update_quotients: string -> quotients -> Context.generic -> Context.generic
   22.22 +  val dest_quotients: Proof.context -> quotients list
   22.23 +  val print_quotients: Proof.context -> unit
   22.24 +
   22.25 +  val setup: theory -> theory
   22.26 +end;
   22.27 +
   22.28 +structure Lifting_Info: LIFTING_INFO =
   22.29 +struct
   22.30 +
   22.31 +(** data containers **)
   22.32 +
   22.33 +(* FIXME just one data slot (record) per program unit *)
   22.34 +
   22.35 +(* info about map- and rel-functions for a type *)
   22.36 +type quotmaps = {relmap: string, quot_thm: thm}
   22.37 +
   22.38 +structure Quotmaps = Generic_Data
   22.39 +(
   22.40 +  type T = quotmaps Symtab.table
   22.41 +  val empty = Symtab.empty
   22.42 +  val extend = I
   22.43 +  fun merge data = Symtab.merge (K true) data
   22.44 +)
   22.45 +
   22.46 +val lookup_quotmaps = Symtab.lookup o Quotmaps.get o Context.Proof
   22.47 +val lookup_quotmaps_global = Symtab.lookup o Quotmaps.get o Context.Theory
   22.48 +
   22.49 +(* FIXME export proper internal update operation!? *)
   22.50 +
   22.51 +val quotmaps_attribute_setup =
   22.52 +  Attrib.setup @{binding map}
   22.53 +    ((Args.type_name true --| Scan.lift @{keyword "="}) --
   22.54 +      (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} --
   22.55 +        Attrib.thm --| Scan.lift @{keyword ")"}) >>
   22.56 +      (fn (tyname, (relname, qthm)) =>
   22.57 +        let val minfo = {relmap = relname, quot_thm = qthm}
   22.58 +        in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
   22.59 +    "declaration of map information"
   22.60 +
   22.61 +fun print_quotmaps ctxt =
   22.62 +  let
   22.63 +    fun prt_map (ty_name, {relmap, quot_thm}) =
   22.64 +      Pretty.block (separate (Pretty.brk 2)
   22.65 +         [Pretty.str "type:", 
   22.66 +          Pretty.str ty_name,
   22.67 +          Pretty.str "relation map:", 
   22.68 +          Pretty.str relmap,
   22.69 +          Pretty.str "quot. theorem:", 
   22.70 +          Syntax.pretty_term ctxt (prop_of quot_thm)])
   22.71 +  in
   22.72 +    map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
   22.73 +    |> Pretty.big_list "maps for type constructors:"
   22.74 +    |> Pretty.writeln
   22.75 +  end
   22.76 +
   22.77 +(* info about quotient types *)
   22.78 +type quotients = {quot_thm: thm}
   22.79 +
   22.80 +structure Quotients = Generic_Data
   22.81 +(
   22.82 +  type T = quotients Symtab.table
   22.83 +  val empty = Symtab.empty
   22.84 +  val extend = I
   22.85 +  fun merge data = Symtab.merge (K true) data
   22.86 +)
   22.87 +
   22.88 +fun transform_quotients phi {quot_thm} =
   22.89 +  {quot_thm = Morphism.thm phi quot_thm}
   22.90 +
   22.91 +val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
   22.92 +val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
   22.93 +
   22.94 +fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo))
   22.95 +
   22.96 +fun dest_quotients ctxt =  (* FIXME slightly expensive way to retrieve data *)
   22.97 +  map snd (Symtab.dest (Quotients.get (Context.Proof ctxt)))
   22.98 +
   22.99 +fun print_quotients ctxt =
  22.100 +  let
  22.101 +    fun prt_quot (qty_name, {quot_thm}) =
  22.102 +      Pretty.block (separate (Pretty.brk 2)
  22.103 +       [Pretty.str "type:", 
  22.104 +        Pretty.str qty_name,
  22.105 +        Pretty.str "quot. thm:",
  22.106 +        Syntax.pretty_term ctxt (prop_of quot_thm)])
  22.107 +  in
  22.108 +    map prt_quot (Symtab.dest (Quotients.get (Context.Proof ctxt)))
  22.109 +    |> Pretty.big_list "quotients:"
  22.110 +    |> Pretty.writeln
  22.111 +  end
  22.112 +
  22.113 +(* theory setup *)
  22.114 +
  22.115 +val setup =
  22.116 +  quotmaps_attribute_setup
  22.117 +
  22.118 +(* outer syntax commands *)
  22.119 +
  22.120 +val _ =
  22.121 +  Outer_Syntax.improper_command @{command_spec "print_quotmaps"} "print quotient map functions"
  22.122 +    (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
  22.123 +
  22.124 +val _ =
  22.125 +  Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
  22.126 +    (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
  22.127 +
  22.128 +end;
  22.129 \ No newline at end of file
    23.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Apr 03 16:26:48 2012 +0200
    23.3 @@ -0,0 +1,113 @@
    23.4 +(*  Title:      HOL/Tools/Lifting/lifting_setup.ML
    23.5 +    Author:     Ondrej Kuncar
    23.6 +
    23.7 +Setting the lifting infranstructure up.
    23.8 +*)
    23.9 +
   23.10 +signature LIFTING_SETUP =
   23.11 +sig
   23.12 +  exception SETUP_LIFTING_INFR of string
   23.13 +
   23.14 +  val setup_lifting_infr: thm -> thm -> local_theory -> local_theory
   23.15 +
   23.16 +  val setup_by_typedef_thm: thm -> local_theory -> local_theory
   23.17 +end;
   23.18 +
   23.19 +structure Lifting_Seup: LIFTING_SETUP =
   23.20 +struct
   23.21 +
   23.22 +infix 0 MRSL
   23.23 +
   23.24 +fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
   23.25 +
   23.26 +exception SETUP_LIFTING_INFR of string
   23.27 +
   23.28 +fun define_cr_rel equiv_thm abs_fun lthy =
   23.29 +  let
   23.30 +    fun force_type_of_rel rel forced_ty =
   23.31 +      let
   23.32 +        val thy = Proof_Context.theory_of lthy
   23.33 +        val rel_ty = (domain_type o fastype_of) rel
   23.34 +        val ty_inst = Sign.typ_match thy (rel_ty, forced_ty) Vartab.empty
   23.35 +      in
   23.36 +        Envir.subst_term_types ty_inst rel
   23.37 +      end
   23.38 +
   23.39 +    val (rty, qty) = (dest_funT o fastype_of) abs_fun
   23.40 +    val abs_fun_graph = HOLogic.mk_eq(abs_fun $ Bound 1, Bound 0)
   23.41 +    val Abs_body = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
   23.42 +      Const (@{const_name equivp}, _) $ _ => abs_fun_graph
   23.43 +      | Const (@{const_name part_equivp}, _) $ rel => 
   23.44 +        HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
   23.45 +      | _ => raise SETUP_LIFTING_INFR "unsopported equivalence theorem"
   23.46 +      )
   23.47 +    val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body));
   23.48 +    val qty_name = (fst o dest_Type) qty
   23.49 +    val cr_rel_name = Binding.prefix_name "cr_" (Binding.qualified_name qty_name)  
   23.50 +    val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
   23.51 +    val ((_, (_ , def_thm)), lthy'') =
   23.52 +      Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy'
   23.53 +  in
   23.54 +    (def_thm, lthy'')
   23.55 +  end
   23.56 +
   23.57 +fun define_abs_type quot_thm lthy =
   23.58 +  if Lifting_Def.can_generate_code_cert quot_thm then
   23.59 +    let
   23.60 +      val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
   23.61 +      val add_abstype_attribute = 
   23.62 +          Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
   23.63 +        val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
   23.64 +    in
   23.65 +      lthy
   23.66 +        |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
   23.67 +    end
   23.68 +  else
   23.69 +    lthy
   23.70 +
   23.71 +fun setup_lifting_infr quot_thm equiv_thm lthy =
   23.72 +  let
   23.73 +    val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
   23.74 +    val qty_full_name = (fst o dest_Type) qtyp
   23.75 +    val quotients = { quot_thm = quot_thm }
   23.76 +    fun quot_info phi = Lifting_Info.transform_quotients phi quotients
   23.77 +  in
   23.78 +    lthy
   23.79 +      |> Local_Theory.declaration {syntax = false, pervasive = true}
   23.80 +        (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
   23.81 +      |> define_abs_type quot_thm
   23.82 +  end
   23.83 +
   23.84 +fun setup_by_typedef_thm typedef_thm lthy =
   23.85 +  let
   23.86 +    fun derive_quot_and_equiv_thm to_quot_thm to_equiv_thm typedef_thm lthy =
   23.87 +      let
   23.88 +        val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
   23.89 +        val equiv_thm = typedef_thm RS to_equiv_thm
   23.90 +        val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
   23.91 +        val quot_thm =  [typedef_thm, T_def] MRSL to_quot_thm
   23.92 +      in
   23.93 +        (quot_thm, equiv_thm, lthy')
   23.94 +      end
   23.95 +
   23.96 +    val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm
   23.97 +    val (quot_thm, equiv_thm, lthy') = (case typedef_set of
   23.98 +      Const ("Orderings.top_class.top", _) => 
   23.99 +        derive_quot_and_equiv_thm @{thm copy_type_to_Quotient} @{thm copy_type_to_equivp} 
  23.100 +          typedef_thm lthy
  23.101 +      | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => 
  23.102 +        derive_quot_and_equiv_thm @{thm invariant_type_to_Quotient} @{thm invariant_type_to_part_equivp} 
  23.103 +          typedef_thm lthy
  23.104 +      | _ => raise SETUP_LIFTING_INFR "unsupported typedef theorem")
  23.105 +  in
  23.106 +    setup_lifting_infr quot_thm equiv_thm lthy'
  23.107 +  end
  23.108 +
  23.109 +fun setup_by_typedef_thm_aux xthm lthy = setup_by_typedef_thm (singleton (Attrib.eval_thms lthy) xthm) lthy
  23.110 +
  23.111 +val _ = 
  23.112 +  Outer_Syntax.local_theory @{command_spec "setup_lifting"}
  23.113 +    "Setup lifting infrastracture" 
  23.114 +      (Parse_Spec.xthm >> (fn xthm => setup_by_typedef_thm_aux xthm))
  23.115 +
  23.116 +end;
    24.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Tue Apr 03 16:26:48 2012 +0200
    24.3 @@ -0,0 +1,173 @@
    24.4 +(*  Title:      HOL/Tools/Lifting/lifting_term.ML
    24.5 +    Author:     Ondrej Kuncar
    24.6 +
    24.7 +Proves Quotient theorem.
    24.8 +*)
    24.9 +
   24.10 +signature LIFTING_TERM =
   24.11 +sig
   24.12 +  val prove_quot_theorem: Proof.context -> typ * typ -> thm
   24.13 +
   24.14 +  val absrep_fun: Proof.context -> typ * typ -> term
   24.15 +
   24.16 +  (* Allows Nitpick to represent quotient types as single elements from raw type *)
   24.17 +  (* val absrep_const_chk: Proof.context -> flag -> string -> term *)
   24.18 +
   24.19 +  val equiv_relation: Proof.context -> typ * typ -> term
   24.20 +
   24.21 +  val quot_thm_rel: thm -> term
   24.22 +  val quot_thm_abs: thm -> term
   24.23 +  val quot_thm_rep: thm -> term
   24.24 +  val quot_thm_rty_qty: thm -> typ * typ
   24.25 +end
   24.26 +
   24.27 +structure Lifting_Term: LIFTING_TERM =
   24.28 +struct
   24.29 +
   24.30 +exception LIFT_MATCH of string
   24.31 +
   24.32 +(* matches a type pattern with a type *)
   24.33 +fun match ctxt err ty_pat ty =
   24.34 +  let
   24.35 +    val thy = Proof_Context.theory_of ctxt
   24.36 +  in
   24.37 +    Sign.typ_match thy (ty_pat, ty) Vartab.empty
   24.38 +      handle Type.TYPE_MATCH => err ctxt ty_pat ty
   24.39 +  end
   24.40 +
   24.41 +fun equiv_match_err ctxt ty_pat ty =
   24.42 +  let
   24.43 +    val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
   24.44 +    val ty_str = Syntax.string_of_typ ctxt ty
   24.45 +  in
   24.46 +    raise LIFT_MATCH (space_implode " "
   24.47 +      ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
   24.48 +  end
   24.49 +
   24.50 +(* generation of the Quotient theorem  *)
   24.51 +
   24.52 +exception QUOT_THM of string
   24.53 +
   24.54 +fun get_quot_thm ctxt s =
   24.55 +  let
   24.56 +    val thy = Proof_Context.theory_of ctxt
   24.57 +  in
   24.58 +    (case Lifting_Info.lookup_quotients ctxt s of
   24.59 +      SOME qdata => Thm.transfer thy (#quot_thm qdata)
   24.60 +    | NONE => raise QUOT_THM ("No quotient type " ^ quote s ^ " found."))
   24.61 +  end
   24.62 +
   24.63 +fun get_rel_quot_thm ctxt s =
   24.64 +   let
   24.65 +    val thy = Proof_Context.theory_of ctxt
   24.66 +  in
   24.67 +    (case Lifting_Info.lookup_quotmaps ctxt s of
   24.68 +      SOME map_data => Thm.transfer thy (#quot_thm map_data)
   24.69 +    | NONE => raise QUOT_THM ("get_relmap (no relation map function found for type " ^ s ^ ")"))
   24.70 +  end
   24.71 +
   24.72 +fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
   24.73 +
   24.74 +infix 0 MRSL
   24.75 +
   24.76 +fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
   24.77 +
   24.78 +exception NOT_IMPL of string
   24.79 +
   24.80 +fun quot_thm_rel quot_thm = 
   24.81 +  let
   24.82 +    val (Const (@{const_name Quotient}, _) $ rel $ _ $ _ $ _) = 
   24.83 +      (HOLogic.dest_Trueprop o prop_of) quot_thm
   24.84 +  in
   24.85 +    rel
   24.86 +  end
   24.87 +
   24.88 +fun quot_thm_abs quot_thm =
   24.89 +  let
   24.90 +    val (Const (@{const_name Quotient}, _) $ _ $ abs $ _ $ _) = 
   24.91 +      (HOLogic.dest_Trueprop o prop_of) quot_thm
   24.92 +  in
   24.93 +    abs
   24.94 +  end
   24.95 +
   24.96 +fun quot_thm_rep quot_thm =
   24.97 +  let
   24.98 +    val (Const (@{const_name Quotient}, _) $ _ $ _ $ rep $ _) = 
   24.99 +      (HOLogic.dest_Trueprop o prop_of) quot_thm
  24.100 +  in
  24.101 +    rep
  24.102 +  end
  24.103 +
  24.104 +fun quot_thm_rty_qty quot_thm =
  24.105 +  let
  24.106 +    val abs = quot_thm_abs quot_thm
  24.107 +    val abs_type = fastype_of abs  
  24.108 +  in
  24.109 +    (domain_type abs_type, range_type abs_type)
  24.110 +  end
  24.111 +
  24.112 +fun prove_quot_theorem ctxt (rty, qty) =
  24.113 +  case (rty, qty) of
  24.114 +    (Type (s, tys), Type (s', tys')) =>
  24.115 +      if s = s'
  24.116 +      then
  24.117 +        let
  24.118 +          val args = map (prove_quot_theorem ctxt) (tys ~~ tys')
  24.119 +        in
  24.120 +          if forall is_id_quot args
  24.121 +          then
  24.122 +            @{thm identity_quotient}
  24.123 +          else
  24.124 +            args MRSL (get_rel_quot_thm ctxt s)
  24.125 +        end
  24.126 +      else
  24.127 +        let
  24.128 +          val quot_thm = get_quot_thm ctxt s'
  24.129 +          val (Type (_, rtys), qty_pat) = quot_thm_rty_qty quot_thm
  24.130 +          val qtyenv = match ctxt equiv_match_err qty_pat qty
  24.131 +          val rtys' = map (Envir.subst_type qtyenv) rtys
  24.132 +          val args = map (prove_quot_theorem ctxt) (tys ~~ rtys')
  24.133 +        in
  24.134 +          if forall is_id_quot args
  24.135 +          then
  24.136 +            quot_thm
  24.137 +          else
  24.138 +            let
  24.139 +              val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s)
  24.140 +            in
  24.141 +              [rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose}
  24.142 +           end
  24.143 +        end
  24.144 +  | _ => @{thm identity_quotient}
  24.145 +
  24.146 +fun force_qty_type thy qty quot_thm =
  24.147 +  let
  24.148 +    val abs_schematic = quot_thm_abs quot_thm 
  24.149 +    val qty_schematic = (range_type o fastype_of) abs_schematic  
  24.150 +    val match_env = Sign.typ_match thy (qty_schematic, qty) Vartab.empty
  24.151 +    fun prep_ty thy (x, (S, ty)) =
  24.152 +      (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
  24.153 +    val ty_inst = Vartab.fold (cons o (prep_ty thy)) match_env []
  24.154 +  in
  24.155 +    Thm.instantiate (ty_inst, []) quot_thm
  24.156 +  end
  24.157 +
  24.158 +fun absrep_fun ctxt (rty, qty) = 
  24.159 +  let
  24.160 +    val thy = Proof_Context.theory_of ctxt
  24.161 +    val quot_thm = prove_quot_theorem ctxt (rty, qty)
  24.162 +    val forced_quot_thm = force_qty_type thy qty quot_thm
  24.163 +  in
  24.164 +    quot_thm_abs forced_quot_thm
  24.165 +  end
  24.166 +
  24.167 +fun equiv_relation ctxt (rty, qty) =
  24.168 +  let
  24.169 +    val thy = Proof_Context.theory_of ctxt
  24.170 +    val quot_thm = prove_quot_theorem ctxt (rty, qty)
  24.171 +    val forced_quot_thm = force_qty_type thy qty quot_thm
  24.172 +  in
  24.173 +    quot_thm_rel forced_quot_thm
  24.174 +  end
  24.175 +
  24.176 +end;
    25.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Tue Apr 03 14:09:37 2012 +0200
    25.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Tue Apr 03 16:26:48 2012 +0200
    25.3 @@ -86,7 +86,7 @@
    25.4        let
    25.5          val quot_thm = Quotient_Term.prove_quot_theorem ctxt args_ty
    25.6        in
    25.7 -        [quot_thm, thm] MRSL @{thm apply_rsp''}
    25.8 +        [quot_thm, thm] MRSL @{thm apply_rspQ3''}
    25.9        end
   25.10    in
   25.11      fold disch_arg ty_args rsp_thm
   25.12 @@ -101,11 +101,11 @@
   25.13    let
   25.14      val quot_thm = Quotient_Term.prove_quot_theorem ctxt (get_body_types (rty, qty))
   25.15      val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
   25.16 -    val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs}
   25.17 +    val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient3_rep_abs}
   25.18      val abs_rep_eq = 
   25.19        case (HOLogic.dest_Trueprop o prop_of) fun_rel of
   25.20          Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm
   25.21 -        | Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq}
   25.22 +        | Const (@{const_name Lifting.invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq}
   25.23          | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant"
   25.24      val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
   25.25      val unabs_def = unabs_all_def ctxt unfolded_def
    26.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Tue Apr 03 14:09:37 2012 +0200
    26.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Tue Apr 03 16:26:48 2012 +0200
    26.3 @@ -70,7 +70,7 @@
    26.4  (* FIXME export proper internal update operation!? *)
    26.5  
    26.6  val quotmaps_attribute_setup =
    26.7 -  Attrib.setup @{binding map}
    26.8 +  Attrib.setup @{binding mapQ3}
    26.9      ((Args.type_name true --| Scan.lift @{keyword "="}) --
   26.10        (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} --
   26.11          Attrib.thm --| Scan.lift @{keyword ")"}) >>
   26.12 @@ -298,11 +298,11 @@
   26.13  (* outer syntax commands *)
   26.14  
   26.15  val _ =
   26.16 -  Outer_Syntax.improper_command @{command_spec "print_quotmaps"} "print quotient map functions"
   26.17 +  Outer_Syntax.improper_command @{command_spec "print_quotmapsQ3"} "print quotient map functions"
   26.18      (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
   26.19  
   26.20  val _ =
   26.21 -  Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
   26.22 +  Outer_Syntax.improper_command @{command_spec "print_quotientsQ3"} "print quotients"
   26.23      (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
   26.24  
   26.25  val _ =
    27.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Apr 03 14:09:37 2012 +0200
    27.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Apr 03 16:26:48 2012 +0200
    27.3 @@ -62,7 +62,7 @@
    27.4  
    27.5  fun quotient_tac ctxt =
    27.6    (REPEAT_ALL_NEW (FIRST'
    27.7 -    [rtac @{thm identity_quotient},
    27.8 +    [rtac @{thm identity_quotient3},
    27.9       resolve_tac (Quotient_Info.quotient_rules ctxt)]))
   27.10  
   27.11  fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
   27.12 @@ -259,7 +259,7 @@
   27.13                val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
   27.14                val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
   27.15                val inst_thm = Drule.instantiate' ty_inst
   27.16 -                ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
   27.17 +                ([NONE, NONE, NONE] @ t_inst) @{thm apply_rspQ3}
   27.18              in
   27.19                (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1
   27.20              end
   27.21 @@ -529,7 +529,7 @@
   27.22      val prs = Quotient_Info.prs_rules lthy
   27.23      val ids = Quotient_Info.id_simps lthy
   27.24      val thms =
   27.25 -      @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
   27.26 +      @{thms Quotient3_abs_rep Quotient3_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
   27.27  
   27.28      val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   27.29    in
    28.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Tue Apr 03 14:09:37 2012 +0200
    28.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Tue Apr 03 16:26:48 2012 +0200
    28.3 @@ -356,7 +356,7 @@
    28.4      | NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")"))
    28.5    end
    28.6  
    28.7 -fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
    28.8 +fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient3})
    28.9  
   28.10  infix 0 MRSL
   28.11  
   28.12 @@ -375,13 +375,13 @@
   28.13    let
   28.14      val quot_thm_rel = get_rel_from_quot_thm quot_thm
   28.15    in
   28.16 -    if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient}
   28.17 +    if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient3}
   28.18      else raise NOT_IMPL "nested quotients: not implemented yet"
   28.19    end
   28.20  
   28.21  fun prove_quot_theorem ctxt (rty, qty) =
   28.22    if rty = qty
   28.23 -  then @{thm identity_quotient}
   28.24 +  then @{thm identity_quotient3}
   28.25    else
   28.26      case (rty, qty) of
   28.27        (Type (s, tys), Type (s', tys')) =>
   28.28 @@ -410,7 +410,7 @@
   28.29                  mk_quot_thm_compose (rel_quot_thm, quot_thm)
   28.30               end
   28.31            end
   28.32 -    | _ => @{thm identity_quotient}
   28.33 +    | _ => @{thm identity_quotient3}
   28.34  
   28.35  
   28.36  
    29.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Tue Apr 03 14:09:37 2012 +0200
    29.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Tue Apr 03 16:26:48 2012 +0200
    29.3 @@ -82,13 +82,13 @@
    29.4  fun can_generate_code_cert quot_thm  =
    29.5     case Quotient_Term.get_rel_from_quot_thm quot_thm of
    29.6        Const (@{const_name HOL.eq}, _) => true
    29.7 -      | Const (@{const_name invariant}, _) $ _  => true
    29.8 +      | Const (@{const_name Lifting.invariant}, _) $ _  => true
    29.9        | _ => false
   29.10  
   29.11  fun define_abs_type quot_thm lthy =
   29.12    if can_generate_code_cert quot_thm then
   29.13      let
   29.14 -      val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
   29.15 +      val abs_type_thm = quot_thm RS @{thm Quotient3_abs_rep}
   29.16        val add_abstype_attribute = 
   29.17            Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
   29.18          val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
   29.19 @@ -157,7 +157,7 @@
   29.20      val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
   29.21  
   29.22      (* quotient theorem *)
   29.23 -    val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
   29.24 +    val quotient_thm_name = Binding.prefix_name "Quotient3_" qty_name
   29.25      val quotient_thm =
   29.26        (quot_thm RS @{thm quot_type.Quotient})
   29.27        |> fold_rule [abs_def, rep_def]
   29.28 @@ -313,30 +313,5 @@
   29.29      "quotient type definitions (require equivalence proofs)"
   29.30        (quotspec_parser >> quotient_type_cmd)
   29.31  
   29.32 -(* Setup lifting using type_def_thm *)
   29.33 -
   29.34 -exception SETUP_LIFT_TYPE of string
   29.35 -
   29.36 -fun setup_lift_type typedef_thm =
   29.37 -  let
   29.38 -    val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm
   29.39 -    val (quot_thm, equivp_thm) = (case typedef_set of
   29.40 -      Const ("Orderings.top_class.top", _) => 
   29.41 -        (typedef_thm RS @{thm copy_type_to_Quotient}, 
   29.42 -         typedef_thm RS @{thm copy_type_to_equivp})
   29.43 -      | Const (@{const_name "Collect"}, _) $ Abs (_, _, _ $ Bound 0) => 
   29.44 -        (typedef_thm RS @{thm invariant_type_to_Quotient}, 
   29.45 -         typedef_thm RS @{thm invariant_type_to_part_equivp})
   29.46 -      | _ => raise SETUP_LIFT_TYPE "unsupported typedef theorem")
   29.47 -  in
   29.48 -    init_quotient_infr quot_thm equivp_thm
   29.49 -  end
   29.50 -
   29.51 -fun setup_lift_type_aux xthm lthy = setup_lift_type (singleton (Attrib.eval_thms lthy) xthm) lthy
   29.52 -
   29.53 -val _ = 
   29.54 -  Outer_Syntax.local_theory @{command_spec "setup_lifting"}
   29.55 -    "Setup lifting infrastracture" 
   29.56 -      (Parse_Spec.xthm >> (fn xthm => setup_lift_type_aux xthm))
   29.57  
   29.58  end;
    30.1 --- a/src/HOL/ex/Executable_Relation.thy	Tue Apr 03 14:09:37 2012 +0200
    30.2 +++ b/src/HOL/ex/Executable_Relation.thy	Tue Apr 03 16:26:48 2012 +0200
    30.3 @@ -67,11 +67,11 @@
    30.4  
    30.5  lemma [simp]:
    30.6    "rel_of_set (set_of_rel S) = S"
    30.7 -by (rule Quotient_abs_rep[OF Quotient_rel])
    30.8 +by (rule Quotient3_abs_rep[OF Quotient3_rel])
    30.9  
   30.10  lemma [simp]:
   30.11    "set_of_rel (rel_of_set R) = R"
   30.12 -by (rule Quotient_rep_abs[OF Quotient_rel]) (rule refl)
   30.13 +by (rule Quotient3_rep_abs[OF Quotient3_rel]) (rule refl)
   30.14  
   30.15  lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"]
   30.16