--- a/Admin/isatest/isatest-settings Tue Apr 03 15:15:00 2012 +0200
+++ b/Admin/isatest/isatest-settings Tue Apr 03 20:56:32 2012 +0200
@@ -25,7 +25,8 @@
hoelzl@in.tum.de \
krauss@in.tum.de \
noschinl@in.tum.de \
-kuncar@in.tum.de"
+kuncar@in.tum.de \
+ns441@cam.ac.uk"
LOGPREFIX=$HOME/log
MASTERLOG=$LOGPREFIX/isatest.log
--- a/etc/isar-keywords.el Tue Apr 03 15:15:00 2012 +0200
+++ b/etc/isar-keywords.el Tue Apr 03 20:56:32 2012 +0200
@@ -190,7 +190,9 @@
"print_orders"
"print_quotconsts"
"print_quotients"
+ "print_quotientsQ3"
"print_quotmaps"
+ "print_quotmapsQ3"
"print_rules"
"print_simpset"
"print_statement"
@@ -403,7 +405,9 @@
"print_orders"
"print_quotconsts"
"print_quotients"
+ "print_quotientsQ3"
"print_quotmaps"
+ "print_quotmapsQ3"
"print_rules"
"print_simpset"
"print_statement"
--- a/src/HOL/IsaMakefile Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/IsaMakefile Tue Apr 03 20:56:32 2012 +0200
@@ -281,6 +281,7 @@
Hilbert_Choice.thy \
Int.thy \
Lazy_Sequence.thy \
+ Lifting.thy \
List.thy \
Main.thy \
Map.thy \
@@ -315,6 +316,10 @@
Tools/code_evaluation.ML \
Tools/groebner.ML \
Tools/int_arith.ML \
+ Tools/Lifting/lifting_def.ML \
+ Tools/Lifting/lifting_info.ML \
+ Tools/Lifting/lifting_term.ML \
+ Tools/Lifting/lifting_setup.ML \
Tools/list_code.ML \
Tools/list_to_set_comprehension.ML \
Tools/nat_numeral_simprocs.ML \
@@ -1036,7 +1041,8 @@
$(LOG)/HOL-Isar_Examples.gz: $(OUT)/HOL Isar_Examples/Basic_Logic.thy \
Isar_Examples/Cantor.thy Isar_Examples/Drinker.thy \
Isar_Examples/Expr_Compiler.thy Isar_Examples/Fibonacci.thy \
- Isar_Examples/Group.thy Isar_Examples/Hoare.thy \
+ Isar_Examples/Group.thy Isar_Examples/Group_Context.thy \
+ Isar_Examples/Group_Notepad.thy Isar_Examples/Hoare.thy \
Isar_Examples/Hoare_Ex.thy Isar_Examples/Knaster_Tarski.thy \
Isar_Examples/Mutilated_Checkerboard.thy \
Isar_Examples/Nested_Datatype.thy Isar_Examples/Peirce.thy \
@@ -1495,7 +1501,7 @@
Quotient_Examples/FSet.thy \
Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \
Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy \
- Quotient_Examples/Lift_Fun.thy
+ Quotient_Examples/Lift_Fun.thy Quotient_Examples/Lift_DList.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_Examples/Group_Context.thy Tue Apr 03 20:56:32 2012 +0200
@@ -0,0 +1,94 @@
+(* Title: HOL/Isar_Examples/Group_Context.thy
+ Author: Makarius
+*)
+
+header {* Some algebraic identities derived from group axioms -- theory context version *}
+
+theory Group_Context
+imports Main
+begin
+
+text {* hypothetical group axiomatization *}
+
+context
+ fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "**" 70)
+ and one :: "'a"
+ and inverse :: "'a => 'a"
+ assumes assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)"
+ and left_one: "\<And>x. one ** x = x"
+ and left_inverse: "\<And>x. inverse x ** x = one"
+begin
+
+text {* some consequences *}
+
+lemma right_inverse: "x ** inverse x = one"
+proof -
+ have "x ** inverse x = one ** (x ** inverse x)"
+ by (simp only: left_one)
+ also have "\<dots> = one ** x ** inverse x"
+ by (simp only: assoc)
+ also have "\<dots> = inverse (inverse x) ** inverse x ** x ** inverse x"
+ by (simp only: left_inverse)
+ also have "\<dots> = inverse (inverse x) ** (inverse x ** x) ** inverse x"
+ by (simp only: assoc)
+ also have "\<dots> = inverse (inverse x) ** one ** inverse x"
+ by (simp only: left_inverse)
+ also have "\<dots> = inverse (inverse x) ** (one ** inverse x)"
+ by (simp only: assoc)
+ also have "\<dots> = inverse (inverse x) ** inverse x"
+ by (simp only: left_one)
+ also have "\<dots> = one"
+ by (simp only: left_inverse)
+ finally show "x ** inverse x = one" .
+qed
+
+lemma right_one: "x ** one = x"
+proof -
+ have "x ** one = x ** (inverse x ** x)"
+ by (simp only: left_inverse)
+ also have "\<dots> = x ** inverse x ** x"
+ by (simp only: assoc)
+ also have "\<dots> = one ** x"
+ by (simp only: right_inverse)
+ also have "\<dots> = x"
+ by (simp only: left_one)
+ finally show "x ** one = x" .
+qed
+
+lemma one_equality: "e ** x = x \<Longrightarrow> one = e"
+proof -
+ fix e x
+ assume eq: "e ** x = x"
+ have "one = x ** inverse x"
+ by (simp only: right_inverse)
+ also have "\<dots> = (e ** x) ** inverse x"
+ by (simp only: eq)
+ also have "\<dots> = e ** (x ** inverse x)"
+ by (simp only: assoc)
+ also have "\<dots> = e ** one"
+ by (simp only: right_inverse)
+ also have "\<dots> = e"
+ by (simp only: right_one)
+ finally show "one = e" .
+qed
+
+lemma inverse_equality: "x' ** x = one \<Longrightarrow> inverse x = x'"
+proof -
+ fix x x'
+ assume eq: "x' ** x = one"
+ have "inverse x = one ** inverse x"
+ by (simp only: left_one)
+ also have "\<dots> = (x' ** x) ** inverse x"
+ by (simp only: eq)
+ also have "\<dots> = x' ** (x ** inverse x)"
+ by (simp only: assoc)
+ also have "\<dots> = x' ** one"
+ by (simp only: right_inverse)
+ also have "\<dots> = x'"
+ by (simp only: right_one)
+ finally show "inverse x = x'" .
+qed
+
+end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_Examples/Group_Notepad.thy Tue Apr 03 20:56:32 2012 +0200
@@ -0,0 +1,96 @@
+(* Title: HOL/Isar_Examples/Group_Notepad.thy
+ Author: Makarius
+*)
+
+header {* Some algebraic identities derived from group axioms -- proof notepad version *}
+
+theory Group_Notepad
+imports Main
+begin
+
+notepad
+begin
+ txt {* hypothetical group axiomatization *}
+
+ fix prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "**" 70)
+ and one :: "'a"
+ and inverse :: "'a => 'a"
+ assume assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)"
+ and left_one: "\<And>x. one ** x = x"
+ and left_inverse: "\<And>x. inverse x ** x = one"
+
+ txt {* some consequences *}
+
+ have right_inverse: "\<And>x. x ** inverse x = one"
+ proof -
+ fix x
+ have "x ** inverse x = one ** (x ** inverse x)"
+ by (simp only: left_one)
+ also have "\<dots> = one ** x ** inverse x"
+ by (simp only: assoc)
+ also have "\<dots> = inverse (inverse x) ** inverse x ** x ** inverse x"
+ by (simp only: left_inverse)
+ also have "\<dots> = inverse (inverse x) ** (inverse x ** x) ** inverse x"
+ by (simp only: assoc)
+ also have "\<dots> = inverse (inverse x) ** one ** inverse x"
+ by (simp only: left_inverse)
+ also have "\<dots> = inverse (inverse x) ** (one ** inverse x)"
+ by (simp only: assoc)
+ also have "\<dots> = inverse (inverse x) ** inverse x"
+ by (simp only: left_one)
+ also have "\<dots> = one"
+ by (simp only: left_inverse)
+ finally show "x ** inverse x = one" .
+ qed
+
+ have right_one: "\<And>x. x ** one = x"
+ proof -
+ fix x
+ have "x ** one = x ** (inverse x ** x)"
+ by (simp only: left_inverse)
+ also have "\<dots> = x ** inverse x ** x"
+ by (simp only: assoc)
+ also have "\<dots> = one ** x"
+ by (simp only: right_inverse)
+ also have "\<dots> = x"
+ by (simp only: left_one)
+ finally show "x ** one = x" .
+ qed
+
+ have one_equality: "\<And>e x. e ** x = x \<Longrightarrow> one = e"
+ proof -
+ fix e x
+ assume eq: "e ** x = x"
+ have "one = x ** inverse x"
+ by (simp only: right_inverse)
+ also have "\<dots> = (e ** x) ** inverse x"
+ by (simp only: eq)
+ also have "\<dots> = e ** (x ** inverse x)"
+ by (simp only: assoc)
+ also have "\<dots> = e ** one"
+ by (simp only: right_inverse)
+ also have "\<dots> = e"
+ by (simp only: right_one)
+ finally show "one = e" .
+ qed
+
+ have inverse_equality: "\<And>x x'. x' ** x = one \<Longrightarrow> inverse x = x'"
+ proof -
+ fix x x'
+ assume eq: "x' ** x = one"
+ have "inverse x = one ** inverse x"
+ by (simp only: left_one)
+ also have "\<dots> = (x' ** x) ** inverse x"
+ by (simp only: eq)
+ also have "\<dots> = x' ** (x ** inverse x)"
+ by (simp only: assoc)
+ also have "\<dots> = x' ** one"
+ by (simp only: right_inverse)
+ also have "\<dots> = x'"
+ by (simp only: right_one)
+ finally show "inverse x = x'" .
+ qed
+
+end
+
+end
--- a/src/HOL/Library/DAList.thy Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Library/DAList.thy Tue Apr 03 20:56:32 2012 +0200
@@ -39,33 +39,29 @@
subsection {* Primitive operations *}
-(* FIXME: improve quotient_definition so that type annotations on the right hand sides can be removed *)
-
-quotient_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option"
-where "lookup" is "map_of :: ('key * 'value) list \<Rightarrow> 'key \<Rightarrow> 'value option" ..
+lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of ..
-quotient_definition empty :: "('key, 'value) alist"
-where "empty" is "[] :: ('key * 'value) list" by simp
+lift_definition empty :: "('key, 'value) alist" is "[]" by simp
-quotient_definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
-where "update" is "AList.update :: 'key \<Rightarrow> 'value \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
+lift_definition update :: "'key \<Rightarrow> 'value \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
+ is AList.update
by (simp add: distinct_update)
(* FIXME: we use an unoptimised delete operation. *)
-quotient_definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
-where "delete" is "AList.delete :: 'key \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
+lift_definition delete :: "'key \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
+ is AList.delete
by (simp add: distinct_delete)
-quotient_definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
-where "map_entry" is "AList.map_entry :: 'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
+lift_definition map_entry :: "'key \<Rightarrow> ('value \<Rightarrow> 'value) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
+ is AList.map_entry
by (simp add: distinct_map_entry)
-quotient_definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
-where "filter" is "List.filter :: ('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key * 'value) list \<Rightarrow> ('key * 'value) list"
+lift_definition filter :: "('key \<times> 'value \<Rightarrow> bool) \<Rightarrow> ('key, 'value) alist \<Rightarrow> ('key, 'value) alist"
+ is List.filter
by (simp add: distinct_map_fst_filter)
-quotient_definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
-where "map_default" is "AList.map_default :: 'key => 'value => ('value => 'value) => ('key * 'value) list => ('key * 'value) list"
+lift_definition map_default :: "'key => 'value => ('value => 'value) => ('key, 'value) alist => ('key, 'value) alist"
+ is AList.map_default
by (simp add: distinct_map_default)
subsection {* Abstract operation properties *}
--- a/src/HOL/Library/Multiset.thy Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Library/Multiset.thy Tue Apr 03 20:56:32 2012 +0200
@@ -1111,14 +1111,12 @@
text {* Operations on alists with distinct keys *}
-quotient_definition join :: "('a \<Rightarrow> 'b \<times> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist"
-where
- "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"
+lift_definition join :: "('a \<Rightarrow> 'b \<times> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist"
+is join_raw
by (simp add: distinct_join_raw)
-quotient_definition subtract_entries :: "('a, ('b :: minus)) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist"
-where
- "subtract_entries" is "subtract_entries_raw :: ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list"
+lift_definition subtract_entries :: "('a, ('b :: minus)) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist"
+is subtract_entries_raw
by (simp add: distinct_subtract_entries_raw)
text {* Implementing multisets by means of association lists *}
--- a/src/HOL/Library/Quotient_List.thy Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Library/Quotient_List.thy Tue Apr 03 20:56:32 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Library/Quotient_List.thy
+(* Title: HOL/Library/Quotient3_List.thy
Author: Cezary Kaliszyk and Christian Urban
*)
@@ -56,63 +56,63 @@
"equivp R \<Longrightarrow> equivp (list_all2 R)"
by (blast intro: equivpI list_reflp list_symp list_transp elim: equivpE)
-lemma list_quotient [quot_thm]:
- assumes "Quotient R Abs Rep"
- shows "Quotient (list_all2 R) (map Abs) (map Rep)"
-proof (rule QuotientI)
- from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
+lemma list_quotient3 [quot_thm]:
+ assumes "Quotient3 R Abs Rep"
+ shows "Quotient3 (list_all2 R) (map Abs) (map Rep)"
+proof (rule Quotient3I)
+ from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient3_abs_rep)
then show "\<And>xs. map Abs (map Rep xs) = xs" by (simp add: comp_def)
next
- from assms have "\<And>x y. R (Rep x) (Rep y) \<longleftrightarrow> x = y" by (rule Quotient_rel_rep)
+ from assms have "\<And>x y. R (Rep x) (Rep y) \<longleftrightarrow> x = y" by (rule Quotient3_rel_rep)
then show "\<And>xs. list_all2 R (map Rep xs) (map Rep xs)"
by (simp add: list_all2_map1 list_all2_map2 list_all2_eq)
next
fix xs ys
- 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)
+ 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)
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"
by (induct xs ys rule: list_induct2') auto
qed
-declare [[map list = (list_all2, list_quotient)]]
+declare [[mapQ3 list = (list_all2, list_quotient3)]]
lemma cons_prs [quot_preserve]:
- assumes q: "Quotient R Abs Rep"
+ assumes q: "Quotient3 R Abs Rep"
shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
- by (auto simp add: fun_eq_iff comp_def Quotient_abs_rep [OF q])
+ by (auto simp add: fun_eq_iff comp_def Quotient3_abs_rep [OF q])
lemma cons_rsp [quot_respect]:
- assumes q: "Quotient R Abs Rep"
+ assumes q: "Quotient3 R Abs Rep"
shows "(R ===> list_all2 R ===> list_all2 R) (op #) (op #)"
by auto
lemma nil_prs [quot_preserve]:
- assumes q: "Quotient R Abs Rep"
+ assumes q: "Quotient3 R Abs Rep"
shows "map Abs [] = []"
by simp
lemma nil_rsp [quot_respect]:
- assumes q: "Quotient R Abs Rep"
+ assumes q: "Quotient3 R Abs Rep"
shows "list_all2 R [] []"
by simp
lemma map_prs_aux:
- assumes a: "Quotient R1 abs1 rep1"
- and b: "Quotient R2 abs2 rep2"
+ assumes a: "Quotient3 R1 abs1 rep1"
+ and b: "Quotient3 R2 abs2 rep2"
shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"
by (induct l)
- (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
+ (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b])
lemma map_prs [quot_preserve]:
- assumes a: "Quotient R1 abs1 rep1"
- and b: "Quotient R2 abs2 rep2"
+ assumes a: "Quotient3 R1 abs1 rep1"
+ and b: "Quotient3 R2 abs2 rep2"
shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
and "((abs1 ---> id) ---> map rep1 ---> id) map = map"
by (simp_all only: fun_eq_iff map_prs_aux[OF a b] comp_def)
- (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
+ (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b])
lemma map_rsp [quot_respect]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ and q2: "Quotient3 R2 Abs2 Rep2"
shows "((R1 ===> R2) ===> (list_all2 R1) ===> list_all2 R2) map map"
and "((R1 ===> op =) ===> (list_all2 R1) ===> op =) map map"
apply (simp_all add: fun_rel_def)
@@ -124,35 +124,35 @@
done
lemma foldr_prs_aux:
- assumes a: "Quotient R1 abs1 rep1"
- and b: "Quotient R2 abs2 rep2"
+ assumes a: "Quotient3 R1 abs1 rep1"
+ and b: "Quotient3 R2 abs2 rep2"
shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
- by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
+ by (induct l) (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b])
lemma foldr_prs [quot_preserve]:
- assumes a: "Quotient R1 abs1 rep1"
- and b: "Quotient R2 abs2 rep2"
+ assumes a: "Quotient3 R1 abs1 rep1"
+ and b: "Quotient3 R2 abs2 rep2"
shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
apply (simp add: fun_eq_iff)
by (simp only: fun_eq_iff foldr_prs_aux[OF a b])
(simp)
lemma foldl_prs_aux:
- assumes a: "Quotient R1 abs1 rep1"
- and b: "Quotient R2 abs2 rep2"
+ assumes a: "Quotient3 R1 abs1 rep1"
+ and b: "Quotient3 R2 abs2 rep2"
shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
- by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
+ by (induct l arbitrary:e) (simp_all add: Quotient3_abs_rep[OF a] Quotient3_abs_rep[OF b])
lemma foldl_prs [quot_preserve]:
- assumes a: "Quotient R1 abs1 rep1"
- and b: "Quotient R2 abs2 rep2"
+ assumes a: "Quotient3 R1 abs1 rep1"
+ and b: "Quotient3 R2 abs2 rep2"
shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
by (simp add: fun_eq_iff foldl_prs_aux [OF a b])
(* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *)
lemma foldl_rsp[quot_respect]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ and q2: "Quotient3 R2 Abs2 Rep2"
shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_all2 R2 ===> R1) foldl foldl"
apply(auto simp add: fun_rel_def)
apply (erule_tac P="R1 xa ya" in rev_mp)
@@ -162,8 +162,8 @@
done
lemma foldr_rsp[quot_respect]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ and q2: "Quotient3 R2 Abs2 Rep2"
shows "((R1 ===> R2 ===> R2) ===> list_all2 R1 ===> R2 ===> R2) foldr foldr"
apply (auto simp add: fun_rel_def)
apply (erule list_all2_induct, simp_all)
@@ -183,18 +183,18 @@
by (simp add: list_all2_rsp fun_rel_def)
lemma [quot_preserve]:
- assumes a: "Quotient R abs1 rep1"
+ assumes a: "Quotient3 R abs1 rep1"
shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_all2 = list_all2"
apply (simp add: fun_eq_iff)
apply clarify
apply (induct_tac xa xb rule: list_induct2')
- apply (simp_all add: Quotient_abs_rep[OF a])
+ apply (simp_all add: Quotient3_abs_rep[OF a])
done
lemma [quot_preserve]:
- assumes a: "Quotient R abs1 rep1"
+ assumes a: "Quotient3 R abs1 rep1"
shows "(list_all2 ((rep1 ---> rep1 ---> id) R) l m) = (l = m)"
- by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a])
+ by (induct l m rule: list_induct2') (simp_all add: Quotient3_rel_rep[OF a])
lemma list_all2_find_element:
assumes a: "x \<in> set a"
@@ -207,4 +207,48 @@
shows "list_all2 R x x"
by (induct x) (auto simp add: a)
+lemma list_quotient:
+ assumes "Quotient R Abs Rep T"
+ shows "Quotient (list_all2 R) (List.map Abs) (List.map Rep) (list_all2 T)"
+proof (rule QuotientI)
+ from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
+ then show "\<And>xs. List.map Abs (List.map Rep xs) = xs" by (simp add: comp_def)
+next
+ from assms have "\<And>x y. R (Rep x) (Rep y) \<longleftrightarrow> x = y" by (rule Quotient_rel_rep)
+ then show "\<And>xs. list_all2 R (List.map Rep xs) (List.map Rep xs)"
+ by (simp add: list_all2_map1 list_all2_map2 list_all2_eq)
+next
+ fix xs ys
+ 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)
+ 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"
+ by (induct xs ys rule: list_induct2') auto
+next
+ {
+ fix l1 l2
+ have "List.length l1 = List.length l2 \<Longrightarrow>
+ (\<forall>(x, y)\<in>set (zip l1 l1). R x y) = (\<forall>(x, y)\<in>set (zip l1 l2). R x x)"
+ by (induction rule: list_induct2) auto
+ } note x = this
+ {
+ fix f g
+ 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)"
+ by (intro ext) (auto simp add: list_all2_def)
+ } note list_all2_conj = this
+ from assms have t: "T = (\<lambda>x y. R x x \<and> Abs x = y)" by (rule Quotient_cr_rel)
+ show "list_all2 T = (\<lambda>x y. list_all2 R x x \<and> List.map Abs x = y)"
+ apply (simp add: t list_all2_conj[symmetric])
+ apply (rule sym)
+ apply (simp add: list_all2_conj)
+ apply(intro ext)
+ apply (intro rev_conj_cong)
+ unfolding list_all2_def apply (metis List.list_all2_eq list_all2_def list_all2_map1)
+ apply (drule conjunct1)
+ apply (intro conj_cong)
+ apply simp
+ apply(simp add: x)
+ done
+qed
+
+declare [[map list = (list_all2, list_quotient)]]
+
end
--- a/src/HOL/Library/Quotient_Option.thy Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Library/Quotient_Option.thy Tue Apr 03 20:56:32 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Library/Quotient_Option.thy
+(* Title: HOL/Library/Quotient3_Option.thy
Author: Cezary Kaliszyk and Christian Urban
*)
@@ -55,36 +55,36 @@
by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE)
lemma option_quotient [quot_thm]:
- assumes "Quotient R Abs Rep"
- shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
- apply (rule QuotientI)
- 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])
- using Quotient_rel [OF assms]
+ assumes "Quotient3 R Abs Rep"
+ shows "Quotient3 (option_rel R) (Option.map Abs) (Option.map Rep)"
+ apply (rule Quotient3I)
+ 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])
+ using Quotient3_rel [OF assms]
apply (simp add: option_rel_unfold split: option.split)
done
-declare [[map option = (option_rel, option_quotient)]]
+declare [[mapQ3 option = (option_rel, option_quotient)]]
lemma option_None_rsp [quot_respect]:
- assumes q: "Quotient R Abs Rep"
+ assumes q: "Quotient3 R Abs Rep"
shows "option_rel R None None"
by simp
lemma option_Some_rsp [quot_respect]:
- assumes q: "Quotient R Abs Rep"
+ assumes q: "Quotient3 R Abs Rep"
shows "(R ===> option_rel R) Some Some"
by auto
lemma option_None_prs [quot_preserve]:
- assumes q: "Quotient R Abs Rep"
+ assumes q: "Quotient3 R Abs Rep"
shows "Option.map Abs None = None"
by simp
lemma option_Some_prs [quot_preserve]:
- assumes q: "Quotient R Abs Rep"
+ assumes q: "Quotient3 R Abs Rep"
shows "(Rep ---> Option.map Abs) Some = Some"
apply(simp add: fun_eq_iff)
- apply(simp add: Quotient_abs_rep[OF q])
+ apply(simp add: Quotient3_abs_rep[OF q])
done
end
--- a/src/HOL/Library/Quotient_Product.thy Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Library/Quotient_Product.thy Tue Apr 03 20:56:32 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Library/Quotient_Product.thy
+(* Title: HOL/Library/Quotient3_Product.thy
Author: Cezary Kaliszyk and Christian Urban
*)
@@ -32,56 +32,56 @@
using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE)
lemma prod_quotient [quot_thm]:
- assumes "Quotient R1 Abs1 Rep1"
- assumes "Quotient R2 Abs2 Rep2"
- shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
- apply (rule QuotientI)
+ assumes "Quotient3 R1 Abs1 Rep1"
+ assumes "Quotient3 R2 Abs2 Rep2"
+ shows "Quotient3 (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
+ apply (rule Quotient3I)
apply (simp add: map_pair.compositionality comp_def map_pair.identity
- Quotient_abs_rep [OF assms(1)] Quotient_abs_rep [OF assms(2)])
- apply (simp add: split_paired_all Quotient_rel_rep [OF assms(1)] Quotient_rel_rep [OF assms(2)])
- using Quotient_rel [OF assms(1)] Quotient_rel [OF assms(2)]
+ Quotient3_abs_rep [OF assms(1)] Quotient3_abs_rep [OF assms(2)])
+ apply (simp add: split_paired_all Quotient3_rel_rep [OF assms(1)] Quotient3_rel_rep [OF assms(2)])
+ using Quotient3_rel [OF assms(1)] Quotient3_rel [OF assms(2)]
apply (auto simp add: split_paired_all)
done
-declare [[map prod = (prod_rel, prod_quotient)]]
+declare [[mapQ3 prod = (prod_rel, prod_quotient)]]
lemma Pair_rsp [quot_respect]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ assumes q2: "Quotient3 R2 Abs2 Rep2"
shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
by (auto simp add: prod_rel_def)
lemma Pair_prs [quot_preserve]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ assumes q2: "Quotient3 R2 Abs2 Rep2"
shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair"
apply(simp add: fun_eq_iff)
- apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+ apply(simp add: Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
done
lemma fst_rsp [quot_respect]:
- assumes "Quotient R1 Abs1 Rep1"
- assumes "Quotient R2 Abs2 Rep2"
+ assumes "Quotient3 R1 Abs1 Rep1"
+ assumes "Quotient3 R2 Abs2 Rep2"
shows "(prod_rel R1 R2 ===> R1) fst fst"
by auto
lemma fst_prs [quot_preserve]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ assumes q2: "Quotient3 R2 Abs2 Rep2"
shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst"
- by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
+ by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1])
lemma snd_rsp [quot_respect]:
- assumes "Quotient R1 Abs1 Rep1"
- assumes "Quotient R2 Abs2 Rep2"
+ assumes "Quotient3 R1 Abs1 Rep1"
+ assumes "Quotient3 R2 Abs2 Rep2"
shows "(prod_rel R1 R2 ===> R2) snd snd"
by auto
lemma snd_prs [quot_preserve]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ assumes q2: "Quotient3 R2 Abs2 Rep2"
shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd"
- by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
+ by (simp add: fun_eq_iff Quotient3_abs_rep[OF q2])
lemma split_rsp [quot_respect]:
shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
@@ -89,10 +89,10 @@
by auto
lemma split_prs [quot_preserve]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ and q2: "Quotient3 R2 Abs2 Rep2"
shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split"
- by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+ by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
lemma [quot_respect]:
shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
@@ -100,11 +100,11 @@
by (auto simp add: fun_rel_def)
lemma [quot_preserve]:
- assumes q1: "Quotient R1 abs1 rep1"
- and q2: "Quotient R2 abs2 rep2"
+ assumes q1: "Quotient3 R1 abs1 rep1"
+ and q2: "Quotient3 R2 abs2 rep2"
shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
map_pair rep1 rep2 ---> map_pair rep1 rep2 ---> id) prod_rel = prod_rel"
- by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+ by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
lemma [quot_preserve]:
shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2)
--- a/src/HOL/Library/Quotient_Set.thy Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Library/Quotient_Set.thy Tue Apr 03 20:56:32 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Library/Quotient_Set.thy
+(* Title: HOL/Library/Quotient3_Set.thy
Author: Cezary Kaliszyk and Christian Urban
*)
@@ -9,77 +9,77 @@
begin
lemma set_quotient [quot_thm]:
- assumes "Quotient R Abs Rep"
- shows "Quotient (set_rel R) (vimage Rep) (vimage Abs)"
-proof (rule QuotientI)
- from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
+ assumes "Quotient3 R Abs Rep"
+ shows "Quotient3 (set_rel R) (vimage Rep) (vimage Abs)"
+proof (rule Quotient3I)
+ from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient3_abs_rep)
then show "\<And>xs. Rep -` (Abs -` xs) = xs"
unfolding vimage_def by auto
next
show "\<And>xs. set_rel R (Abs -` xs) (Abs -` xs)"
unfolding set_rel_def vimage_def
- by auto (metis Quotient_rel_abs[OF assms])+
+ by auto (metis Quotient3_rel_abs[OF assms])+
next
fix r s
show "set_rel R r s = (set_rel R r r \<and> set_rel R s s \<and> Rep -` r = Rep -` s)"
unfolding set_rel_def vimage_def set_eq_iff
- by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+
+ by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient3_def])+
qed
-declare [[map set = (set_rel, set_quotient)]]
+declare [[mapQ3 set = (set_rel, set_quotient)]]
lemma empty_set_rsp[quot_respect]:
"set_rel R {} {}"
unfolding set_rel_def by simp
lemma collect_rsp[quot_respect]:
- assumes "Quotient R Abs Rep"
+ assumes "Quotient3 R Abs Rep"
shows "((R ===> op =) ===> set_rel R) Collect Collect"
by (intro fun_relI) (simp add: fun_rel_def set_rel_def)
lemma collect_prs[quot_preserve]:
- assumes "Quotient R Abs Rep"
+ assumes "Quotient3 R Abs Rep"
shows "((Abs ---> id) ---> op -` Rep) Collect = Collect"
unfolding fun_eq_iff
- by (simp add: Quotient_abs_rep[OF assms])
+ by (simp add: Quotient3_abs_rep[OF assms])
lemma union_rsp[quot_respect]:
- assumes "Quotient R Abs Rep"
+ assumes "Quotient3 R Abs Rep"
shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"
by (intro fun_relI) (simp add: set_rel_def)
lemma union_prs[quot_preserve]:
- assumes "Quotient R Abs Rep"
+ assumes "Quotient3 R Abs Rep"
shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<union> = op \<union>"
unfolding fun_eq_iff
- by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
+ by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
lemma diff_rsp[quot_respect]:
- assumes "Quotient R Abs Rep"
+ assumes "Quotient3 R Abs Rep"
shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"
by (intro fun_relI) (simp add: set_rel_def)
lemma diff_prs[quot_preserve]:
- assumes "Quotient R Abs Rep"
+ assumes "Quotient3 R Abs Rep"
shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -"
unfolding fun_eq_iff
- by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
+ by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
lemma inter_rsp[quot_respect]:
- assumes "Quotient R Abs Rep"
+ assumes "Quotient3 R Abs Rep"
shows "(set_rel R ===> set_rel R ===> set_rel R) op \<inter> op \<inter>"
by (intro fun_relI) (auto simp add: set_rel_def)
lemma inter_prs[quot_preserve]:
- assumes "Quotient R Abs Rep"
+ assumes "Quotient3 R Abs Rep"
shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<inter> = op \<inter>"
unfolding fun_eq_iff
- by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
+ by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
lemma mem_prs[quot_preserve]:
- assumes "Quotient R Abs Rep"
+ assumes "Quotient3 R Abs Rep"
shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
- by (simp add: fun_eq_iff Quotient_abs_rep[OF assms])
+ by (simp add: fun_eq_iff Quotient3_abs_rep[OF assms])
lemma mem_rsp[quot_respect]:
shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
--- a/src/HOL/Library/Quotient_Sum.thy Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy Tue Apr 03 20:56:32 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Library/Quotient_Sum.thy
+(* Title: HOL/Library/Quotient3_Sum.thy
Author: Cezary Kaliszyk and Christian Urban
*)
@@ -55,44 +55,44 @@
by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE)
lemma sum_quotient [quot_thm]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
- shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
- apply (rule QuotientI)
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ assumes q2: "Quotient3 R2 Abs2 Rep2"
+ shows "Quotient3 (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
+ apply (rule Quotient3I)
apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
- Quotient_abs_rep [OF q1] Quotient_rel_rep [OF q1] Quotient_abs_rep [OF q2] Quotient_rel_rep [OF q2])
- using Quotient_rel [OF q1] Quotient_rel [OF q2]
+ Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2])
+ using Quotient3_rel [OF q1] Quotient3_rel [OF q2]
apply (simp add: sum_rel_unfold comp_def split: sum.split)
done
-declare [[map sum = (sum_rel, sum_quotient)]]
+declare [[mapQ3 sum = (sum_rel, sum_quotient)]]
lemma sum_Inl_rsp [quot_respect]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ assumes q2: "Quotient3 R2 Abs2 Rep2"
shows "(R1 ===> sum_rel R1 R2) Inl Inl"
by auto
lemma sum_Inr_rsp [quot_respect]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ assumes q2: "Quotient3 R2 Abs2 Rep2"
shows "(R2 ===> sum_rel R1 R2) Inr Inr"
by auto
lemma sum_Inl_prs [quot_preserve]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ assumes q2: "Quotient3 R2 Abs2 Rep2"
shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
apply(simp add: fun_eq_iff)
- apply(simp add: Quotient_abs_rep[OF q1])
+ apply(simp add: Quotient3_abs_rep[OF q1])
done
lemma sum_Inr_prs [quot_preserve]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ assumes q2: "Quotient3 R2 Abs2 Rep2"
shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
apply(simp add: fun_eq_iff)
- apply(simp add: Quotient_abs_rep[OF q2])
+ apply(simp add: Quotient3_abs_rep[OF q2])
done
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lifting.thy Tue Apr 03 20:56:32 2012 +0200
@@ -0,0 +1,316 @@
+(* Title: HOL/Lifting.thy
+ Author: Brian Huffman and Ondrej Kuncar
+ Author: Cezary Kaliszyk and Christian Urban
+*)
+
+header {* Lifting package *}
+
+theory Lifting
+imports Plain Equiv_Relations
+keywords
+ "print_quotmaps" "print_quotients" :: diag and
+ "lift_definition" :: thy_goal and
+ "setup_lifting" :: thy_decl
+uses
+ ("Tools/Lifting/lifting_info.ML")
+ ("Tools/Lifting/lifting_term.ML")
+ ("Tools/Lifting/lifting_def.ML")
+ ("Tools/Lifting/lifting_setup.ML")
+begin
+
+subsection {* Function map and function relation *}
+
+notation map_fun (infixr "--->" 55)
+
+lemma map_fun_id:
+ "(id ---> id) = id"
+ by (simp add: fun_eq_iff)
+
+definition
+ 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)
+where
+ "fun_rel R1 R2 = (\<lambda>f g. \<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
+
+lemma fun_relI [intro]:
+ assumes "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
+ shows "(R1 ===> R2) f g"
+ using assms by (simp add: fun_rel_def)
+
+lemma fun_relE:
+ assumes "(R1 ===> R2) f g" and "R1 x y"
+ obtains "R2 (f x) (g y)"
+ using assms by (simp add: fun_rel_def)
+
+lemma fun_rel_eq:
+ shows "((op =) ===> (op =)) = (op =)"
+ by (auto simp add: fun_eq_iff elim: fun_relE)
+
+lemma fun_rel_eq_rel:
+ shows "((op =) ===> R) = (\<lambda>f g. \<forall>x. R (f x) (g x))"
+ by (simp add: fun_rel_def)
+
+subsection {* Quotient Predicate *}
+
+definition
+ "Quotient R Abs Rep T \<longleftrightarrow>
+ (\<forall>a. Abs (Rep a) = a) \<and>
+ (\<forall>a. R (Rep a) (Rep a)) \<and>
+ (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and>
+ T = (\<lambda>x y. R x x \<and> Abs x = y)"
+
+lemma QuotientI:
+ assumes "\<And>a. Abs (Rep a) = a"
+ and "\<And>a. R (Rep a) (Rep a)"
+ and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
+ and "T = (\<lambda>x y. R x x \<and> Abs x = y)"
+ shows "Quotient R Abs Rep T"
+ using assms unfolding Quotient_def by blast
+
+lemma Quotient_abs_rep:
+ assumes a: "Quotient R Abs Rep T"
+ shows "Abs (Rep a) = a"
+ using a
+ unfolding Quotient_def
+ by simp
+
+lemma Quotient_rep_reflp:
+ assumes a: "Quotient R Abs Rep T"
+ shows "R (Rep a) (Rep a)"
+ using a
+ unfolding Quotient_def
+ by blast
+
+lemma Quotient_rel:
+ assumes a: "Quotient R Abs Rep T"
+ shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
+ using a
+ unfolding Quotient_def
+ by blast
+
+lemma Quotient_cr_rel:
+ assumes a: "Quotient R Abs Rep T"
+ shows "T = (\<lambda>x y. R x x \<and> Abs x = y)"
+ using a
+ unfolding Quotient_def
+ by blast
+
+lemma Quotient_refl1:
+ assumes a: "Quotient R Abs Rep T"
+ shows "R r s \<Longrightarrow> R r r"
+ using a unfolding Quotient_def
+ by fast
+
+lemma Quotient_refl2:
+ assumes a: "Quotient R Abs Rep T"
+ shows "R r s \<Longrightarrow> R s s"
+ using a unfolding Quotient_def
+ by fast
+
+lemma Quotient_rel_rep:
+ assumes a: "Quotient R Abs Rep T"
+ shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
+ using a
+ unfolding Quotient_def
+ by metis
+
+lemma Quotient_rep_abs:
+ assumes a: "Quotient R Abs Rep T"
+ shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
+ using a unfolding Quotient_def
+ by blast
+
+lemma Quotient_rel_abs:
+ assumes a: "Quotient R Abs Rep T"
+ shows "R r s \<Longrightarrow> Abs r = Abs s"
+ using a unfolding Quotient_def
+ by blast
+
+lemma Quotient_symp:
+ assumes a: "Quotient R Abs Rep T"
+ shows "symp R"
+ using a unfolding Quotient_def using sympI by (metis (full_types))
+
+lemma Quotient_transp:
+ assumes a: "Quotient R Abs Rep T"
+ shows "transp R"
+ using a unfolding Quotient_def using transpI by (metis (full_types))
+
+lemma Quotient_part_equivp:
+ assumes a: "Quotient R Abs Rep T"
+ shows "part_equivp R"
+by (metis Quotient_rep_reflp Quotient_symp Quotient_transp a part_equivpI)
+
+lemma identity_quotient: "Quotient (op =) id id (op =)"
+unfolding Quotient_def by simp
+
+lemma Quotient_alt_def:
+ "Quotient R Abs Rep T \<longleftrightarrow>
+ (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
+ (\<forall>b. T (Rep b) b) \<and>
+ (\<forall>x y. R x y \<longleftrightarrow> T x (Abs x) \<and> T y (Abs y) \<and> Abs x = Abs y)"
+apply safe
+apply (simp (no_asm_use) only: Quotient_def, fast)
+apply (simp (no_asm_use) only: Quotient_def, fast)
+apply (simp (no_asm_use) only: Quotient_def, fast)
+apply (simp (no_asm_use) only: Quotient_def, fast)
+apply (simp (no_asm_use) only: Quotient_def, fast)
+apply (simp (no_asm_use) only: Quotient_def, fast)
+apply (rule QuotientI)
+apply simp
+apply metis
+apply simp
+apply (rule ext, rule ext, metis)
+done
+
+lemma Quotient_alt_def2:
+ "Quotient R Abs Rep T \<longleftrightarrow>
+ (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and>
+ (\<forall>b. T (Rep b) b) \<and>
+ (\<forall>x y. R x y \<longleftrightarrow> T x (Abs y) \<and> T y (Abs x))"
+ unfolding Quotient_alt_def by (safe, metis+)
+
+lemma fun_quotient:
+ assumes 1: "Quotient R1 abs1 rep1 T1"
+ assumes 2: "Quotient R2 abs2 rep2 T2"
+ shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2) (T1 ===> T2)"
+ using assms unfolding Quotient_alt_def2
+ unfolding fun_rel_def fun_eq_iff map_fun_apply
+ by (safe, metis+)
+
+lemma apply_rsp:
+ fixes f g::"'a \<Rightarrow> 'c"
+ assumes q: "Quotient R1 Abs1 Rep1 T1"
+ and a: "(R1 ===> R2) f g" "R1 x y"
+ shows "R2 (f x) (g y)"
+ using a by (auto elim: fun_relE)
+
+lemma apply_rsp':
+ assumes a: "(R1 ===> R2) f g" "R1 x y"
+ shows "R2 (f x) (g y)"
+ using a by (auto elim: fun_relE)
+
+lemma apply_rsp'':
+ assumes "Quotient R Abs Rep T"
+ and "(R ===> S) f f"
+ shows "S (f (Rep x)) (f (Rep x))"
+proof -
+ from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp)
+ then show ?thesis using assms(2) by (auto intro: apply_rsp')
+qed
+
+subsection {* Quotient composition *}
+
+lemma Quotient_compose:
+ assumes 1: "Quotient R1 Abs1 Rep1 T1"
+ assumes 2: "Quotient R2 Abs2 Rep2 T2"
+ shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)"
+proof -
+ from 1 have Abs1: "\<And>a b. T1 a b \<Longrightarrow> Abs1 a = b"
+ unfolding Quotient_alt_def by simp
+ from 1 have Rep1: "\<And>b. T1 (Rep1 b) b"
+ unfolding Quotient_alt_def by simp
+ from 2 have Abs2: "\<And>a b. T2 a b \<Longrightarrow> Abs2 a = b"
+ unfolding Quotient_alt_def by simp
+ from 2 have Rep2: "\<And>b. T2 (Rep2 b) b"
+ unfolding Quotient_alt_def by simp
+ from 2 have R2:
+ "\<And>x y. R2 x y \<longleftrightarrow> T2 x (Abs2 x) \<and> T2 y (Abs2 y) \<and> Abs2 x = Abs2 y"
+ unfolding Quotient_alt_def by simp
+ show ?thesis
+ unfolding Quotient_alt_def
+ apply simp
+ apply safe
+ apply (drule Abs1, simp)
+ apply (erule Abs2)
+ apply (rule pred_compI)
+ apply (rule Rep1)
+ apply (rule Rep2)
+ apply (rule pred_compI, assumption)
+ apply (drule Abs1, simp)
+ apply (clarsimp simp add: R2)
+ apply (rule pred_compI, assumption)
+ apply (drule Abs1, simp)+
+ apply (clarsimp simp add: R2)
+ apply (drule Abs1, simp)+
+ apply (clarsimp simp add: R2)
+ apply (rule pred_compI, assumption)
+ apply (rule pred_compI [rotated])
+ apply (erule conversepI)
+ apply (drule Abs1, simp)+
+ apply (simp add: R2)
+ done
+qed
+
+subsection {* Invariant *}
+
+definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ where "invariant R = (\<lambda>x y. R x \<and> x = y)"
+
+lemma invariant_to_eq:
+ assumes "invariant P x y"
+ shows "x = y"
+using assms by (simp add: invariant_def)
+
+lemma fun_rel_eq_invariant:
+ shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
+by (auto simp add: invariant_def fun_rel_def)
+
+lemma invariant_same_args:
+ shows "invariant P x x \<equiv> P x"
+using assms by (auto simp add: invariant_def)
+
+lemma copy_type_to_Quotient:
+ assumes "type_definition Rep Abs UNIV"
+ and T_def: "T \<equiv> (\<lambda>x y. Abs x = y)"
+ shows "Quotient (op =) Abs Rep T"
+proof -
+ interpret type_definition Rep Abs UNIV by fact
+ from Abs_inject Rep_inverse T_def show ?thesis by (auto intro!: QuotientI)
+qed
+
+lemma copy_type_to_equivp:
+ fixes Abs :: "'a \<Rightarrow> 'b"
+ and Rep :: "'b \<Rightarrow> 'a"
+ assumes "type_definition Rep Abs (UNIV::'a set)"
+ shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
+by (rule identity_equivp)
+
+lemma invariant_type_to_Quotient:
+ assumes "type_definition Rep Abs {x. P x}"
+ and T_def: "T \<equiv> (\<lambda>x y. (invariant P) x x \<and> Abs x = y)"
+ shows "Quotient (invariant P) Abs Rep T"
+proof -
+ interpret type_definition Rep Abs "{x. P x}" by fact
+ from Rep Abs_inject Rep_inverse T_def show ?thesis by (auto intro!: QuotientI simp: invariant_def)
+qed
+
+lemma invariant_type_to_part_equivp:
+ assumes "type_definition Rep Abs {x. P x}"
+ shows "part_equivp (invariant P)"
+proof (intro part_equivpI)
+ interpret type_definition Rep Abs "{x. P x}" by fact
+ show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def)
+next
+ show "symp (invariant P)" by (auto intro: sympI simp: invariant_def)
+next
+ show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
+qed
+
+subsection {* ML setup *}
+
+text {* Auxiliary data for the lifting package *}
+
+use "Tools/Lifting/lifting_info.ML"
+setup Lifting_Info.setup
+
+declare [[map "fun" = (fun_rel, fun_quotient)]]
+
+use "Tools/Lifting/lifting_term.ML"
+
+use "Tools/Lifting/lifting_def.ML"
+
+use "Tools/Lifting/lifting_setup.ML"
+
+hide_const (open) invariant
+
+end
--- a/src/HOL/Metis_Examples/Clausification.thy Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Metis_Examples/Clausification.thy Tue Apr 03 20:56:32 2012 +0200
@@ -131,7 +131,7 @@
by (metis bounded_def subset_eq)
lemma
- assumes a: "Quotient R Abs Rep"
+ assumes a: "Quotient R Abs Rep T"
shows "symp R"
using a unfolding Quotient_def using sympI
by (metis (full_types))
--- a/src/HOL/Quotient.thy Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Quotient.thy Tue Apr 03 20:56:32 2012 +0200
@@ -5,11 +5,10 @@
header {* Definition of Quotient Types *}
theory Quotient
-imports Plain Hilbert_Choice Equiv_Relations
+imports Plain Hilbert_Choice Equiv_Relations Lifting
keywords
- "print_quotmaps" "print_quotients" "print_quotconsts" :: diag and
+ "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
"quotient_type" :: thy_goal and "/" and
- "setup_lifting" :: thy_decl and
"quotient_definition" :: thy_goal
uses
("Tools/Quotient/quotient_info.ML")
@@ -53,37 +52,6 @@
shows "x \<in> Respects R \<longleftrightarrow> R x x"
unfolding Respects_def by simp
-subsection {* Function map and function relation *}
-
-notation map_fun (infixr "--->" 55)
-
-lemma map_fun_id:
- "(id ---> id) = id"
- by (simp add: fun_eq_iff)
-
-definition
- 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)
-where
- "fun_rel R1 R2 = (\<lambda>f g. \<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
-
-lemma fun_relI [intro]:
- assumes "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
- shows "(R1 ===> R2) f g"
- using assms by (simp add: fun_rel_def)
-
-lemma fun_relE:
- assumes "(R1 ===> R2) f g" and "R1 x y"
- obtains "R2 (f x) (g y)"
- using assms by (simp add: fun_rel_def)
-
-lemma fun_rel_eq:
- shows "((op =) ===> (op =)) = (op =)"
- by (auto simp add: fun_eq_iff elim: fun_relE)
-
-lemma fun_rel_eq_rel:
- shows "((op =) ===> R) = (\<lambda>f g. \<forall>x. R (f x) (g x))"
- by (simp add: fun_rel_def)
-
subsection {* set map (vimage) and set relation *}
definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
@@ -106,155 +74,169 @@
subsection {* Quotient Predicate *}
definition
- "Quotient R Abs Rep \<longleftrightarrow>
+ "Quotient3 R Abs Rep \<longleftrightarrow>
(\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. R (Rep a) (Rep a)) \<and>
(\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s)"
-lemma QuotientI:
+lemma Quotient3I:
assumes "\<And>a. Abs (Rep a) = a"
and "\<And>a. R (Rep a) (Rep a)"
and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
- shows "Quotient R Abs Rep"
- using assms unfolding Quotient_def by blast
+ shows "Quotient3 R Abs Rep"
+ using assms unfolding Quotient3_def by blast
-lemma Quotient_abs_rep:
- assumes a: "Quotient R Abs Rep"
+lemma Quotient3_abs_rep:
+ assumes a: "Quotient3 R Abs Rep"
shows "Abs (Rep a) = a"
using a
- unfolding Quotient_def
+ unfolding Quotient3_def
by simp
-lemma Quotient_rep_reflp:
- assumes a: "Quotient R Abs Rep"
+lemma Quotient3_rep_reflp:
+ assumes a: "Quotient3 R Abs Rep"
shows "R (Rep a) (Rep a)"
using a
- unfolding Quotient_def
+ unfolding Quotient3_def
by blast
-lemma Quotient_rel:
- assumes a: "Quotient R Abs Rep"
+lemma Quotient3_rel:
+ assumes a: "Quotient3 R Abs Rep"
shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
using a
- unfolding Quotient_def
+ unfolding Quotient3_def
by blast
-lemma Quotient_refl1:
- assumes a: "Quotient R Abs Rep"
+lemma Quotient3_refl1:
+ assumes a: "Quotient3 R Abs Rep"
shows "R r s \<Longrightarrow> R r r"
- using a unfolding Quotient_def
+ using a unfolding Quotient3_def
by fast
-lemma Quotient_refl2:
- assumes a: "Quotient R Abs Rep"
+lemma Quotient3_refl2:
+ assumes a: "Quotient3 R Abs Rep"
shows "R r s \<Longrightarrow> R s s"
- using a unfolding Quotient_def
+ using a unfolding Quotient3_def
by fast
-lemma Quotient_rel_rep:
- assumes a: "Quotient R Abs Rep"
+lemma Quotient3_rel_rep:
+ assumes a: "Quotient3 R Abs Rep"
shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
using a
- unfolding Quotient_def
+ unfolding Quotient3_def
by metis
-lemma Quotient_rep_abs:
- assumes a: "Quotient R Abs Rep"
+lemma Quotient3_rep_abs:
+ assumes a: "Quotient3 R Abs Rep"
shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
- using a unfolding Quotient_def
+ using a unfolding Quotient3_def
+ by blast
+
+lemma Quotient3_rel_abs:
+ assumes a: "Quotient3 R Abs Rep"
+ shows "R r s \<Longrightarrow> Abs r = Abs s"
+ using a unfolding Quotient3_def
by blast
-lemma Quotient_rel_abs:
- assumes a: "Quotient R Abs Rep"
- shows "R r s \<Longrightarrow> Abs r = Abs s"
- using a unfolding Quotient_def
- by blast
-
-lemma Quotient_symp:
- assumes a: "Quotient R Abs Rep"
+lemma Quotient3_symp:
+ assumes a: "Quotient3 R Abs Rep"
shows "symp R"
- using a unfolding Quotient_def using sympI by metis
+ using a unfolding Quotient3_def using sympI by metis
-lemma Quotient_transp:
- assumes a: "Quotient R Abs Rep"
+lemma Quotient3_transp:
+ assumes a: "Quotient3 R Abs Rep"
shows "transp R"
- using a unfolding Quotient_def using transpI by metis
+ using a unfolding Quotient3_def using transpI by (metis (full_types))
-lemma identity_quotient:
- shows "Quotient (op =) id id"
- unfolding Quotient_def id_def
+lemma Quotient3_part_equivp:
+ assumes a: "Quotient3 R Abs Rep"
+ shows "part_equivp R"
+by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp a part_equivpI)
+
+lemma identity_quotient3:
+ shows "Quotient3 (op =) id id"
+ unfolding Quotient3_def id_def
by blast
-lemma fun_quotient:
- assumes q1: "Quotient R1 abs1 rep1"
- and q2: "Quotient R2 abs2 rep2"
- shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
+lemma fun_quotient3:
+ assumes q1: "Quotient3 R1 abs1 rep1"
+ and q2: "Quotient3 R2 abs2 rep2"
+ shows "Quotient3 (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
proof -
- have "\<And>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
- using q1 q2 by (simp add: Quotient_def fun_eq_iff)
+ have "\<And>a.(rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
+ using q1 q2 by (simp add: Quotient3_def fun_eq_iff)
moreover
- have "\<And>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
+ have "\<And>a.(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
by (rule fun_relI)
- (insert q1 q2 Quotient_rel_abs [of R1 abs1 rep1] Quotient_rel_rep [of R2 abs2 rep2],
- simp (no_asm) add: Quotient_def, simp)
+ (insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2],
+ simp (no_asm) add: Quotient3_def, simp)
+
moreover
- have "\<And>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
+ {
+ fix r s
+ have "(R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
(rep1 ---> abs2) r = (rep1 ---> abs2) s)"
- apply(auto simp add: fun_rel_def fun_eq_iff)
- using q1 q2 unfolding Quotient_def
- apply(metis)
- using q1 q2 unfolding Quotient_def
- apply(metis)
- using q1 q2 unfolding Quotient_def
- apply(metis)
- using q1 q2 unfolding Quotient_def
- apply(metis)
- done
- ultimately
- show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
- unfolding Quotient_def by blast
+ proof -
+
+ have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) r r" unfolding fun_rel_def
+ using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2]
+ by (metis (full_types) part_equivp_def)
+ moreover have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) s s" unfolding fun_rel_def
+ using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2]
+ by (metis (full_types) part_equivp_def)
+ moreover have "(R1 ===> R2) r s \<Longrightarrow> (rep1 ---> abs2) r = (rep1 ---> abs2) s"
+ apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def by metis
+ moreover have "((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
+ (rep1 ---> abs2) r = (rep1 ---> abs2) s) \<Longrightarrow> (R1 ===> R2) r s"
+ apply(auto simp add: fun_rel_def fun_eq_iff) using q1 q2 unfolding Quotient3_def
+ by (metis map_fun_apply)
+
+ ultimately show ?thesis by blast
+ qed
+ }
+ ultimately show ?thesis by (intro Quotient3I) (assumption+)
qed
lemma abs_o_rep:
- assumes a: "Quotient R Abs Rep"
+ assumes a: "Quotient3 R Abs Rep"
shows "Abs o Rep = id"
unfolding fun_eq_iff
- by (simp add: Quotient_abs_rep[OF a])
+ by (simp add: Quotient3_abs_rep[OF a])
lemma equals_rsp:
- assumes q: "Quotient R Abs Rep"
+ assumes q: "Quotient3 R Abs Rep"
and a: "R xa xb" "R ya yb"
shows "R xa ya = R xb yb"
- using a Quotient_symp[OF q] Quotient_transp[OF q]
+ using a Quotient3_symp[OF q] Quotient3_transp[OF q]
by (blast elim: sympE transpE)
lemma lambda_prs:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ and q2: "Quotient3 R2 Abs2 Rep2"
shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
unfolding fun_eq_iff
- using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
+ using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
by simp
lemma lambda_prs1:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ and q2: "Quotient3 R2 Abs2 Rep2"
shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
unfolding fun_eq_iff
- using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
+ using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
by simp
lemma rep_abs_rsp:
- assumes q: "Quotient R Abs Rep"
+ assumes q: "Quotient3 R Abs Rep"
and a: "R x1 x2"
shows "R x1 (Rep (Abs x2))"
- using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]
+ using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q]
by metis
lemma rep_abs_rsp_left:
- assumes q: "Quotient R Abs Rep"
+ assumes q: "Quotient3 R Abs Rep"
and a: "R x1 x2"
shows "R (Rep (Abs x1)) x2"
- using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]
+ using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q]
by metis
text{*
@@ -264,24 +246,19 @@
will be provable; which is why we need to use @{text apply_rsp} and
not the primed version *}
-lemma apply_rsp:
+lemma apply_rspQ3:
fixes f g::"'a \<Rightarrow> 'c"
- assumes q: "Quotient R1 Abs1 Rep1"
+ assumes q: "Quotient3 R1 Abs1 Rep1"
and a: "(R1 ===> R2) f g" "R1 x y"
shows "R2 (f x) (g y)"
using a by (auto elim: fun_relE)
-lemma apply_rsp':
- assumes a: "(R1 ===> R2) f g" "R1 x y"
- shows "R2 (f x) (g y)"
- using a by (auto elim: fun_relE)
-
-lemma apply_rsp'':
- assumes "Quotient R Abs Rep"
+lemma apply_rspQ3'':
+ assumes "Quotient3 R Abs Rep"
and "(R ===> S) f f"
shows "S (f (Rep x)) (f (Rep x))"
proof -
- from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp)
+ from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient3_rep_reflp)
then show ?thesis using assms(2) by (auto intro: apply_rsp')
qed
@@ -393,29 +370,29 @@
"x \<in> p \<Longrightarrow> Babs p m x = m x"
lemma babs_rsp:
- assumes q: "Quotient R1 Abs1 Rep1"
+ assumes q: "Quotient3 R1 Abs1 Rep1"
and a: "(R1 ===> R2) f g"
shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
apply (auto simp add: Babs_def in_respects fun_rel_def)
apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
using a apply (simp add: Babs_def fun_rel_def)
apply (simp add: in_respects fun_rel_def)
- using Quotient_rel[OF q]
+ using Quotient3_rel[OF q]
by metis
lemma babs_prs:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ and q2: "Quotient3 R2 Abs2 Rep2"
shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
apply (rule ext)
apply (simp add:)
apply (subgoal_tac "Rep1 x \<in> Respects R1")
- apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
- apply (simp add: in_respects Quotient_rel_rep[OF q1])
+ apply (simp add: Babs_def Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
+ apply (simp add: in_respects Quotient3_rel_rep[OF q1])
done
lemma babs_simp:
- assumes q: "Quotient R1 Abs Rep"
+ assumes q: "Quotient3 R1 Abs Rep"
shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
apply(rule iffI)
apply(simp_all only: babs_rsp[OF q])
@@ -423,7 +400,7 @@
apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
apply(metis Babs_def)
apply (simp add: in_respects)
- using Quotient_rel[OF q]
+ using Quotient3_rel[OF q]
by metis
(* If a user proves that a particular functional relation
@@ -451,15 +428,15 @@
(* 2 lemmas needed for cleaning of quantifiers *)
lemma all_prs:
- assumes a: "Quotient R absf repf"
+ assumes a: "Quotient3 R absf repf"
shows "Ball (Respects R) ((absf ---> id) f) = All f"
- using a unfolding Quotient_def Ball_def in_respects id_apply comp_def map_fun_def
+ using a unfolding Quotient3_def Ball_def in_respects id_apply comp_def map_fun_def
by metis
lemma ex_prs:
- assumes a: "Quotient R absf repf"
+ assumes a: "Quotient3 R absf repf"
shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
- using a unfolding Quotient_def Bex_def in_respects id_apply comp_def map_fun_def
+ using a unfolding Quotient3_def Bex_def in_respects id_apply comp_def map_fun_def
by metis
subsection {* @{text Bex1_rel} quantifier *}
@@ -508,7 +485,7 @@
done
lemma bex1_rel_rsp:
- assumes a: "Quotient R absf repf"
+ assumes a: "Quotient3 R absf repf"
shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
apply (simp add: fun_rel_def)
apply clarify
@@ -520,7 +497,7 @@
lemma ex1_prs:
- assumes a: "Quotient R absf repf"
+ assumes a: "Quotient3 R absf repf"
shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
apply (simp add:)
apply (subst Bex1_rel_def)
@@ -535,7 +512,7 @@
apply (rule_tac x="absf x" in exI)
apply (simp)
apply rule+
- using a unfolding Quotient_def
+ using a unfolding Quotient3_def
apply metis
apply rule+
apply (erule_tac x="x" in ballE)
@@ -548,10 +525,10 @@
apply (rule_tac x="repf x" in exI)
apply (simp only: in_respects)
apply rule
- apply (metis Quotient_rel_rep[OF a])
-using a unfolding Quotient_def apply (simp)
+ apply (metis Quotient3_rel_rep[OF a])
+using a unfolding Quotient3_def apply (simp)
apply rule+
-using a unfolding Quotient_def in_respects
+using a unfolding Quotient3_def in_respects
apply metis
done
@@ -587,7 +564,7 @@
subsection {* Various respects and preserve lemmas *}
lemma quot_rel_rsp:
- assumes a: "Quotient R Abs Rep"
+ assumes a: "Quotient3 R Abs Rep"
shows "(R ===> R ===> op =) R R"
apply(rule fun_relI)+
apply(rule equals_rsp[OF a])
@@ -595,12 +572,12 @@
done
lemma o_prs:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
- and q3: "Quotient R3 Abs3 Rep3"
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ and q2: "Quotient3 R2 Abs2 Rep2"
+ and q3: "Quotient3 R3 Abs3 Rep3"
shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \<circ> = op \<circ>"
and "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \<circ> = op \<circ>"
- using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
+ using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] Quotient3_abs_rep[OF q3]
by (simp_all add: fun_eq_iff)
lemma o_rsp:
@@ -609,26 +586,26 @@
by (force elim: fun_relE)+
lemma cond_prs:
- assumes a: "Quotient R absf repf"
+ assumes a: "Quotient3 R absf repf"
shows "absf (if a then repf b else repf c) = (if a then b else c)"
- using a unfolding Quotient_def by auto
+ using a unfolding Quotient3_def by auto
lemma if_prs:
- assumes q: "Quotient R Abs Rep"
+ assumes q: "Quotient3 R Abs Rep"
shows "(id ---> Rep ---> Rep ---> Abs) If = If"
- using Quotient_abs_rep[OF q]
+ using Quotient3_abs_rep[OF q]
by (auto simp add: fun_eq_iff)
lemma if_rsp:
- assumes q: "Quotient R Abs Rep"
+ assumes q: "Quotient3 R Abs Rep"
shows "(op = ===> R ===> R ===> R) If If"
by force
lemma let_prs:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
+ assumes q1: "Quotient3 R1 Abs1 Rep1"
+ and q2: "Quotient3 R2 Abs2 Rep2"
shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let"
- using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
+ using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
by (auto simp add: fun_eq_iff)
lemma let_rsp:
@@ -640,9 +617,9 @@
by auto
lemma id_prs:
- assumes a: "Quotient R Abs Rep"
+ assumes a: "Quotient3 R Abs Rep"
shows "(Rep ---> Abs) id = id"
- by (simp add: fun_eq_iff Quotient_abs_rep [OF a])
+ by (simp add: fun_eq_iff Quotient3_abs_rep [OF a])
locale quot_type =
@@ -673,8 +650,8 @@
by (metis assms exE_some equivp[simplified part_equivp_def])
lemma Quotient:
- shows "Quotient R abs rep"
- unfolding Quotient_def abs_def rep_def
+ shows "Quotient3 R abs rep"
+ unfolding Quotient3_def abs_def rep_def
proof (intro conjI allI)
fix a r s
show x: "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" proof -
@@ -703,149 +680,114 @@
subsection {* Quotient composition *}
-lemma OOO_quotient:
+lemma OOO_quotient3:
fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
fixes R2' :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
fixes R2 :: "'b \<Rightarrow> 'b \<Rightarrow> bool"
- assumes R1: "Quotient R1 Abs1 Rep1"
- assumes R2: "Quotient R2 Abs2 Rep2"
+ assumes R1: "Quotient3 R1 Abs1 Rep1"
+ assumes R2: "Quotient3 R2 Abs2 Rep2"
assumes Abs1: "\<And>x y. R2' x y \<Longrightarrow> R1 x x \<Longrightarrow> R1 y y \<Longrightarrow> R2 (Abs1 x) (Abs1 y)"
assumes Rep1: "\<And>x y. R2 x y \<Longrightarrow> R2' (Rep1 x) (Rep1 y)"
- shows "Quotient (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
-apply (rule QuotientI)
- apply (simp add: o_def Quotient_abs_rep [OF R2] Quotient_abs_rep [OF R1])
+ shows "Quotient3 (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
+apply (rule Quotient3I)
+ apply (simp add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1])
apply simp
apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI)
- apply (rule Quotient_rep_reflp [OF R1])
+ apply (rule Quotient3_rep_reflp [OF R1])
apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated])
- apply (rule Quotient_rep_reflp [OF R1])
+ apply (rule Quotient3_rep_reflp [OF R1])
apply (rule Rep1)
- apply (rule Quotient_rep_reflp [OF R2])
+ apply (rule Quotient3_rep_reflp [OF R2])
apply safe
apply (rename_tac x y)
apply (drule Abs1)
- apply (erule Quotient_refl2 [OF R1])
- apply (erule Quotient_refl1 [OF R1])
- apply (drule Quotient_refl1 [OF R2], drule Rep1)
+ apply (erule Quotient3_refl2 [OF R1])
+ apply (erule Quotient3_refl1 [OF R1])
+ apply (drule Quotient3_refl1 [OF R2], drule Rep1)
apply (subgoal_tac "R1 r (Rep1 (Abs1 x))")
apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption)
apply (erule pred_compI)
- apply (erule Quotient_symp [OF R1, THEN sympD])
- apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
- apply (rule conjI, erule Quotient_refl1 [OF R1])
- apply (rule conjI, rule Quotient_rep_reflp [OF R1])
- apply (subst Quotient_abs_rep [OF R1])
- apply (erule Quotient_rel_abs [OF R1])
+ apply (erule Quotient3_symp [OF R1, THEN sympD])
+ apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
+ apply (rule conjI, erule Quotient3_refl1 [OF R1])
+ apply (rule conjI, rule Quotient3_rep_reflp [OF R1])
+ apply (subst Quotient3_abs_rep [OF R1])
+ apply (erule Quotient3_rel_abs [OF R1])
apply (rename_tac x y)
apply (drule Abs1)
- apply (erule Quotient_refl2 [OF R1])
- apply (erule Quotient_refl1 [OF R1])
- apply (drule Quotient_refl2 [OF R2], drule Rep1)
+ apply (erule Quotient3_refl2 [OF R1])
+ apply (erule Quotient3_refl1 [OF R1])
+ apply (drule Quotient3_refl2 [OF R2], drule Rep1)
apply (subgoal_tac "R1 s (Rep1 (Abs1 y))")
apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption)
apply (erule pred_compI)
- apply (erule Quotient_symp [OF R1, THEN sympD])
- apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
- apply (rule conjI, erule Quotient_refl2 [OF R1])
- apply (rule conjI, rule Quotient_rep_reflp [OF R1])
- apply (subst Quotient_abs_rep [OF R1])
- apply (erule Quotient_rel_abs [OF R1, THEN sym])
+ apply (erule Quotient3_symp [OF R1, THEN sympD])
+ apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
+ apply (rule conjI, erule Quotient3_refl2 [OF R1])
+ apply (rule conjI, rule Quotient3_rep_reflp [OF R1])
+ apply (subst Quotient3_abs_rep [OF R1])
+ apply (erule Quotient3_rel_abs [OF R1, THEN sym])
apply simp
- apply (rule Quotient_rel_abs [OF R2])
- apply (rule Quotient_rel_abs [OF R1, THEN ssubst], assumption)
- apply (rule Quotient_rel_abs [OF R1, THEN subst], assumption)
+ apply (rule Quotient3_rel_abs [OF R2])
+ apply (rule Quotient3_rel_abs [OF R1, THEN ssubst], assumption)
+ apply (rule Quotient3_rel_abs [OF R1, THEN subst], assumption)
apply (erule Abs1)
- apply (erule Quotient_refl2 [OF R1])
- apply (erule Quotient_refl1 [OF R1])
+ apply (erule Quotient3_refl2 [OF R1])
+ apply (erule Quotient3_refl1 [OF R1])
apply (rename_tac a b c d)
apply simp
apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI)
- apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
- apply (rule conjI, erule Quotient_refl1 [OF R1])
- apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
+ apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
+ apply (rule conjI, erule Quotient3_refl1 [OF R1])
+ apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1])
apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated])
- apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
- apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
- apply (erule Quotient_refl2 [OF R1])
+ apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2])
+ apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1])
+ apply (erule Quotient3_refl2 [OF R1])
apply (rule Rep1)
apply (drule Abs1)
- apply (erule Quotient_refl2 [OF R1])
- apply (erule Quotient_refl1 [OF R1])
+ apply (erule Quotient3_refl2 [OF R1])
+ apply (erule Quotient3_refl1 [OF R1])
apply (drule Abs1)
- apply (erule Quotient_refl2 [OF R1])
- apply (erule Quotient_refl1 [OF R1])
- apply (drule Quotient_rel_abs [OF R1])
- apply (drule Quotient_rel_abs [OF R1])
- apply (drule Quotient_rel_abs [OF R1])
- apply (drule Quotient_rel_abs [OF R1])
+ apply (erule Quotient3_refl2 [OF R1])
+ apply (erule Quotient3_refl1 [OF R1])
+ apply (drule Quotient3_rel_abs [OF R1])
+ apply (drule Quotient3_rel_abs [OF R1])
+ apply (drule Quotient3_rel_abs [OF R1])
+ apply (drule Quotient3_rel_abs [OF R1])
apply simp
- apply (rule Quotient_rel[symmetric, OF R2, THEN iffD2])
+ apply (rule Quotient3_rel[symmetric, OF R2, THEN iffD2])
apply simp
done
-lemma OOO_eq_quotient:
+lemma OOO_eq_quotient3:
fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
- assumes R1: "Quotient R1 Abs1 Rep1"
- assumes R2: "Quotient op= Abs2 Rep2"
- shows "Quotient (R1 OOO op=) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
+ assumes R1: "Quotient3 R1 Abs1 Rep1"
+ assumes R2: "Quotient3 op= Abs2 Rep2"
+ shows "Quotient3 (R1 OOO op=) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
using assms
-by (rule OOO_quotient) auto
+by (rule OOO_quotient3) auto
subsection {* Invariant *}
-definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
- where "invariant R = (\<lambda>x y. R x \<and> x = y)"
-
-lemma invariant_to_eq:
- assumes "invariant P x y"
- shows "x = y"
-using assms by (simp add: invariant_def)
-
-lemma fun_rel_eq_invariant:
- shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
-by (auto simp add: invariant_def fun_rel_def)
-
-lemma invariant_same_args:
- shows "invariant P x x \<equiv> P x"
-using assms by (auto simp add: invariant_def)
-
-lemma copy_type_to_Quotient:
+lemma copy_type_to_Quotient3:
assumes "type_definition Rep Abs UNIV"
- shows "Quotient (op =) Abs Rep"
+ shows "Quotient3 (op =) Abs Rep"
proof -
interpret type_definition Rep Abs UNIV by fact
- from Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI)
+ from Abs_inject Rep_inverse show ?thesis by (auto intro!: Quotient3I)
qed
-lemma copy_type_to_equivp:
- fixes Abs :: "'a \<Rightarrow> 'b"
- and Rep :: "'b \<Rightarrow> 'a"
- assumes "type_definition Rep Abs (UNIV::'a set)"
- shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
-by (rule identity_equivp)
-
-lemma invariant_type_to_Quotient:
+lemma invariant_type_to_Quotient3:
assumes "type_definition Rep Abs {x. P x}"
- shows "Quotient (invariant P) Abs Rep"
+ shows "Quotient3 (Lifting.invariant P) Abs Rep"
proof -
interpret type_definition Rep Abs "{x. P x}" by fact
- from Rep Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI simp: invariant_def)
-qed
-
-lemma invariant_type_to_part_equivp:
- assumes "type_definition Rep Abs {x. P x}"
- shows "part_equivp (invariant P)"
-proof (intro part_equivpI)
- interpret type_definition Rep Abs "{x. P x}" by fact
- show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def)
-next
- show "symp (invariant P)" by (auto intro: sympI simp: invariant_def)
-next
- show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
+ from Rep Abs_inject Rep_inverse show ?thesis by (auto intro!: Quotient3I simp: invariant_def)
qed
subsection {* ML setup *}
@@ -855,9 +797,9 @@
use "Tools/Quotient/quotient_info.ML"
setup Quotient_Info.setup
-declare [[map "fun" = (fun_rel, fun_quotient)]]
+declare [[mapQ3 "fun" = (fun_rel, fun_quotient3)]]
-lemmas [quot_thm] = fun_quotient
+lemmas [quot_thm] = fun_quotient3
lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp
lemmas [quot_preserve] = if_prs o_prs let_prs id_prs
lemmas [quot_equiv] = identity_equivp
@@ -960,6 +902,4 @@
map_fun (infixr "--->" 55) and
fun_rel (infixr "===>" 55)
-hide_const (open) invariant
-
end
--- a/src/HOL/Quotient_Examples/DList.thy Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Quotient_Examples/DList.thy Tue Apr 03 20:56:32 2012 +0200
@@ -227,7 +227,7 @@
lemma list_of_dlist_dlist [simp]:
"list_of_dlist (dlist xs) = remdups xs"
unfolding list_of_dlist_def map_fun_apply id_def
- by (metis Quotient_rep_abs[OF Quotient_dlist] dlist_eq_def)
+ by (metis Quotient3_rep_abs[OF Quotient3_dlist] dlist_eq_def)
lemma remdups_list_of_dlist [simp]:
"remdups (list_of_dlist dxs) = list_of_dlist dxs"
@@ -236,7 +236,7 @@
lemma dlist_list_of_dlist [simp, code abstype]:
"dlist (list_of_dlist dxs) = dxs"
by (simp add: list_of_dlist_def)
- (metis Quotient_def Quotient_dlist dlist_eqI list_of_dlist_dlist remdups_list_of_dlist)
+ (metis Quotient3_def Quotient3_dlist dlist_eqI list_of_dlist_dlist remdups_list_of_dlist)
lemma dlist_filter_simps:
"filter P empty = empty"
--- a/src/HOL/Quotient_Examples/FSet.thy Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy Tue Apr 03 20:56:32 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Quotient_Examples/FSet.thy
+(* Title: HOL/Quotient3_Examples/FSet.thy
Author: Cezary Kaliszyk, TU Munich
Author: Christian Urban, TU Munich
@@ -117,15 +117,15 @@
by (simp only: list_eq_def set_map)
lemma quotient_compose_list_g:
- assumes q: "Quotient R Abs Rep"
+ assumes q: "Quotient3 R Abs Rep"
and e: "equivp R"
- shows "Quotient ((list_all2 R) OOO (op \<approx>))
+ shows "Quotient3 ((list_all2 R) OOO (op \<approx>))
(abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)"
- unfolding Quotient_def comp_def
+ unfolding Quotient3_def comp_def
proof (intro conjI allI)
fix a r s
show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
- by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] List.map.id)
+ by (simp add: abs_o_rep[OF q] Quotient3_abs_rep[OF Quotient3_fset] List.map.id)
have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
by (rule list_all2_refl'[OF e])
have c: "(op \<approx> OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
@@ -146,37 +146,37 @@
assume d: "b \<approx> ba"
assume e: "list_all2 R ba s"
have f: "map Abs r = map Abs b"
- using Quotient_rel[OF list_quotient[OF q]] c by blast
+ using Quotient3_rel[OF list_quotient3[OF q]] c by blast
have "map Abs ba = map Abs s"
- using Quotient_rel[OF list_quotient[OF q]] e by blast
+ using Quotient3_rel[OF list_quotient3[OF q]] e by blast
then have g: "map Abs s = map Abs ba" by simp
then show "map Abs r \<approx> map Abs s" using d f map_list_eq_cong by simp
qed
then show "abs_fset (map Abs r) = abs_fset (map Abs s)"
- using Quotient_rel[OF Quotient_fset] by blast
+ using Quotient3_rel[OF Quotient3_fset] by blast
next
assume a: "(list_all2 R OOO op \<approx>) r r \<and> (list_all2 R OOO op \<approx>) s s
\<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
then have s: "(list_all2 R OOO op \<approx>) s s" by simp
have d: "map Abs r \<approx> map Abs s"
- by (subst Quotient_rel [OF Quotient_fset, symmetric]) (simp add: a)
+ by (subst Quotient3_rel [OF Quotient3_fset, symmetric]) (simp add: a)
have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
by (rule map_list_eq_cong[OF d])
have y: "list_all2 R (map Rep (map Abs s)) s"
- by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl'[OF e, of s]])
+ by (fact rep_abs_rsp_left[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of s]])
have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"
by (rule pred_compI) (rule b, rule y)
have z: "list_all2 R r (map Rep (map Abs r))"
- by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl'[OF e, of r]])
+ by (fact rep_abs_rsp[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of r]])
then show "(list_all2 R OOO op \<approx>) r s"
using a c pred_compI by simp
qed
qed
lemma quotient_compose_list[quot_thm]:
- shows "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))
+ shows "Quotient3 ((list_all2 op \<approx>) OOO (op \<approx>))
(abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
- by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp)
+ by (rule quotient_compose_list_g, rule Quotient3_fset, rule list_eq_equivp)
section {* Quotient definitions for fsets *}
@@ -404,19 +404,19 @@
done
lemma Nil_prs2 [quot_preserve]:
- assumes "Quotient R Abs Rep"
+ assumes "Quotient3 R Abs Rep"
shows "(Abs \<circ> map f) [] = Abs []"
by simp
lemma Cons_prs2 [quot_preserve]:
- assumes q: "Quotient R1 Abs1 Rep1"
- and r: "Quotient R2 Abs2 Rep2"
+ assumes q: "Quotient3 R1 Abs1 Rep1"
+ and r: "Quotient3 R2 Abs2 Rep2"
shows "(Rep1 ---> (map Rep1 \<circ> Rep2) ---> (Abs2 \<circ> map Abs1)) (op #) = (id ---> Rep2 ---> Abs2) (op #)"
- by (auto simp add: fun_eq_iff comp_def Quotient_abs_rep [OF q])
+ by (auto simp add: fun_eq_iff comp_def Quotient3_abs_rep [OF q])
lemma append_prs2 [quot_preserve]:
- assumes q: "Quotient R1 Abs1 Rep1"
- and r: "Quotient R2 Abs2 Rep2"
+ assumes q: "Quotient3 R1 Abs1 Rep1"
+ and r: "Quotient3 R2 Abs2 Rep2"
shows "((map Rep1 \<circ> Rep2) ---> (map Rep1 \<circ> Rep2) ---> (Abs2 \<circ> map Abs1)) op @ =
(Rep2 ---> Rep2 ---> Abs2) op @"
by (simp add: fun_eq_iff abs_o_rep[OF q] List.map.id)
@@ -485,7 +485,7 @@
lemma map_prs2 [quot_preserve]:
shows "((abs_fset ---> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> abs_fset \<circ> map abs_fset) map = (id ---> rep_fset ---> abs_fset) map"
by (auto simp add: fun_eq_iff)
- (simp only: map_map[symmetric] map_prs_aux[OF Quotient_fset Quotient_fset])
+ (simp only: map_map[symmetric] map_prs_aux[OF Quotient3_fset Quotient3_fset])
section {* Lifted theorems *}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/Lift_DList.thy Tue Apr 03 20:56:32 2012 +0200
@@ -0,0 +1,86 @@
+(* Title: HOL/Quotient_Examples/Lift_DList.thy
+ Author: Ondrej Kuncar
+*)
+
+theory Lift_DList
+imports Main "~~/src/HOL/Library/Quotient_List"
+begin
+
+subsection {* The type of distinct lists *}
+
+typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
+ morphisms list_of_dlist Abs_dlist
+proof
+ show "[] \<in> {xs. distinct xs}" by simp
+qed
+
+setup_lifting type_definition_dlist
+
+text {* Fundamental operations: *}
+
+lift_definition empty :: "'a dlist" is "[]"
+by simp
+
+lift_definition insert :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" is List.insert
+by simp
+
+lift_definition remove :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" is List.remove1
+by simp
+
+lift_definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist" is "\<lambda>f. remdups o List.map f"
+by simp
+
+lift_definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" is List.filter
+by simp
+
+text {* Derived operations: *}
+
+lift_definition null :: "'a dlist \<Rightarrow> bool" is List.null
+by simp
+
+lift_definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" is List.member
+by simp
+
+lift_definition length :: "'a dlist \<Rightarrow> nat" is List.length
+by simp
+
+lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.fold
+by simp
+
+lift_definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" is List.foldr
+by simp
+
+lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat"
+proof -
+ {
+ fix x y
+ have "list_all2 cr_dlist x y \<Longrightarrow>
+ List.map Abs_dlist x = y \<and> list_all2 (Lifting.invariant distinct) x x"
+ unfolding list_all2_def cr_dlist_def by (induction x y rule: list_induct2') auto
+ }
+ note cr = this
+
+ fix x :: "'a list list" and y :: "'a list list"
+ assume a: "(list_all2 cr_dlist OO Lifting.invariant distinct OO (list_all2 cr_dlist)\<inverse>\<inverse>) x y"
+ from a have l_x: "list_all2 (Lifting.invariant distinct) x x" by (auto simp add: cr)
+ from a have l_y: "list_all2 (Lifting.invariant distinct) y y" by (auto simp add: cr)
+ from a have m: "(Lifting.invariant distinct) (List.map Abs_dlist x) (List.map Abs_dlist y)"
+ by (auto simp add: cr)
+
+ have "x = y"
+ proof -
+ have m':"List.map Abs_dlist x = List.map Abs_dlist y" using m unfolding Lifting.invariant_def by simp
+ have dist: "\<And>l. list_all2 (Lifting.invariant distinct) l l \<Longrightarrow> !x. x \<in> (set l) \<longrightarrow> distinct x"
+ unfolding list_all2_def Lifting.invariant_def by (auto simp add: zip_same)
+ from dist[OF l_x] dist[OF l_y] have "inj_on Abs_dlist (set x \<union> set y)" by (intro inj_onI)
+ (metis CollectI UnE Abs_dlist_inverse)
+ with m' show ?thesis by (rule map_inj_on)
+ qed
+ then show "?thesis x y" unfolding Lifting.invariant_def by auto
+qed
+
+text {* We can export code: *}
+
+export_code empty insert remove map filter null member length fold foldr concat in SML
+
+end
--- a/src/HOL/Quotient_Examples/Lift_Fun.thy Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Quotient_Examples/Lift_Fun.thy Tue Apr 03 20:56:32 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Quotient_Examples/Lift_Fun.thy
+(* Title: HOL/Quotient3_Examples/Lift_Fun.thy
Author: Ondrej Kuncar
*)
@@ -53,12 +53,12 @@
enriched_type map_endofun : map_endofun
proof -
- have "\<forall> x. abs_endofun (rep_endofun x) = x" using Quotient_endofun by (auto simp: Quotient_def)
+ have "\<forall> x. abs_endofun (rep_endofun x) = x" using Quotient3_endofun by (auto simp: Quotient3_def)
then show "map_endofun id id = id"
by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff)
- have a:"\<forall> x. rep_endofun (abs_endofun x) = x" using Quotient_endofun
- Quotient_rep_abs[of "(op =)" abs_endofun rep_endofun] by blast
+ have a:"\<forall> x. rep_endofun (abs_endofun x) = x" using Quotient3_endofun
+ Quotient3_rep_abs[of "(op =)" abs_endofun rep_endofun] by blast
show "\<And>f g h i. map_endofun f g \<circ> map_endofun h i = map_endofun (f \<circ> h) (i \<circ> g)"
by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc)
qed
@@ -74,34 +74,34 @@
endofun_rel' done
lemma endofun_quotient:
-assumes a: "Quotient R Abs Rep"
-shows "Quotient (endofun_rel R) (map_endofun Abs Rep) (map_endofun Rep Abs)"
-proof (intro QuotientI)
+assumes a: "Quotient3 R Abs Rep"
+shows "Quotient3 (endofun_rel R) (map_endofun Abs Rep) (map_endofun Rep Abs)"
+proof (intro Quotient3I)
show "\<And>a. map_endofun Abs Rep (map_endofun Rep Abs a) = a"
by (metis (hide_lams, no_types) a abs_o_rep id_apply map_endofun.comp map_endofun.id o_eq_dest_lhs)
next
show "\<And>a. endofun_rel R (map_endofun Rep Abs a) (map_endofun Rep Abs a)"
- using fun_quotient[OF a a, THEN Quotient_rep_reflp]
+ using fun_quotient3[OF a a, THEN Quotient3_rep_reflp]
unfolding endofun_rel_def map_endofun_def map_fun_def o_def map_endofun'_def endofun_rel'_def id_def
- by (metis (mono_tags) Quotient_endofun rep_abs_rsp)
+ by (metis (mono_tags) Quotient3_endofun rep_abs_rsp)
next
have abs_to_eq: "\<And> x y. abs_endofun x = abs_endofun y \<Longrightarrow> x = y"
- by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient_rep_abs[OF Quotient_endofun])
+ by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient3_rep_abs[OF Quotient3_endofun])
fix r s
show "endofun_rel R r s =
(endofun_rel R r r \<and>
endofun_rel R s s \<and> map_endofun Abs Rep r = map_endofun Abs Rep s)"
apply(auto simp add: endofun_rel_def endofun_rel'_def map_endofun_def map_endofun'_def)
- using fun_quotient[OF a a,THEN Quotient_refl1]
+ using fun_quotient3[OF a a,THEN Quotient3_refl1]
apply metis
- using fun_quotient[OF a a,THEN Quotient_refl2]
+ using fun_quotient3[OF a a,THEN Quotient3_refl2]
apply metis
- using fun_quotient[OF a a, THEN Quotient_rel]
+ using fun_quotient3[OF a a, THEN Quotient3_rel]
apply metis
- by (auto intro: fun_quotient[OF a a, THEN Quotient_rel, THEN iffD1] simp add: abs_to_eq)
+ by (auto intro: fun_quotient3[OF a a, THEN Quotient3_rel, THEN iffD1] simp add: abs_to_eq)
qed
-declare [[map endofun = (endofun_rel, endofun_quotient)]]
+declare [[mapQ3 endofun = (endofun_rel, endofun_quotient)]]
quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" done
--- a/src/HOL/Quotient_Examples/Lift_RBT.thy Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Quotient_Examples/Lift_RBT.thy Tue Apr 03 20:56:32 2012 +0200
@@ -1,4 +1,6 @@
-(* Author: Lukas Bulwahn, TU Muenchen *)
+(* Title: HOL/Quotient_Examples/Lift_RBT.thy
+ Author: Lukas Bulwahn and Ondrej Kuncar
+*)
header {* Lifting operations of RBT trees *}
@@ -35,53 +37,35 @@
setup_lifting type_definition_rbt
-quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup"
+lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup"
+by simp
+
+lift_definition empty :: "('a\<Colon>linorder, 'b) rbt" is RBT_Impl.Empty
+by (simp add: empty_def)
+
+lift_definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.insert"
+by simp
+
+lift_definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.delete"
+by simp
+
+lift_definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries
by simp
-(* FIXME: quotient_definition at the moment requires that types variables match exactly,
-i.e., sort constraints must be annotated to the constant being lifted.
-But, it should be possible to infer the necessary sort constraints, making the explicit
-sort constraints unnecessary.
-
-Hence this unannotated quotient_definition fails:
-
-quotient_definition empty where "empty :: ('a\<Colon>linorder, 'b) rbt"
-is "RBT_Impl.Empty"
-
-Similar issue for quotient_definition for entries, keys, map, and fold.
-*)
-
-quotient_definition empty where "empty :: ('a\<Colon>linorder, 'b) rbt"
-is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)" by (simp add: empty_def)
-
-quotient_definition insert where "insert :: 'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.insert" by simp
+lift_definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys
+by simp
-quotient_definition delete where "delete :: 'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.delete" by simp
-
-(* FIXME: unnecessary type annotations *)
-quotient_definition "entries :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
-is "RBT_Impl.entries :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a \<times> 'b) list" by simp
-
-(* FIXME: unnecessary type annotations *)
-quotient_definition "keys :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list"
-is "RBT_Impl.keys :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a list" by simp
-
-quotient_definition "bulkload :: ('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.bulkload" by simp
-
-quotient_definition "map_entry :: 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.map_entry" by simp
-
-(* FIXME: unnecesary type annotations *)
-quotient_definition map where "map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a, 'b) RBT_Impl.rbt"
+lift_definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.bulkload"
by simp
-(* FIXME: unnecessary type annotations *)
-quotient_definition fold where "fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
-is "RBT_Impl.fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'c \<Rightarrow> 'c" by simp
+lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is RBT_Impl.map_entry
+by simp
+
+lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is RBT_Impl.map
+by simp
+
+lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" is RBT_Impl.fold
+by simp
export_code lookup empty insert delete entries keys bulkload map_entry map fold in SML
--- a/src/HOL/Quotient_Examples/Lift_Set.thy Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy Tue Apr 03 20:56:32 2012 +0200
@@ -2,7 +2,7 @@
Author: Lukas Bulwahn and Ondrej Kuncar
*)
-header {* Example of lifting definitions with the quotient infrastructure *}
+header {* Example of lifting definitions with the lifting infrastructure *}
theory Lift_Set
imports Main
@@ -16,19 +16,14 @@
setup_lifting type_definition_set[unfolded set_def]
-text {* Now, we can employ quotient_definition to lift definitions. *}
+text {* Now, we can employ lift_definition to lift definitions. *}
-quotient_definition empty where "empty :: 'a set"
-is "bot :: 'a \<Rightarrow> bool" done
+lift_definition empty :: "'a set" is "bot :: 'a \<Rightarrow> bool" done
term "Lift_Set.empty"
thm Lift_Set.empty_def
-definition insertp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
- "insertp x P y \<longleftrightarrow> y = x \<or> P y"
-
-quotient_definition insert where "insert :: 'a => 'a set => 'a set"
-is insertp done
+lift_definition insert :: "'a => 'a set => 'a set" is "\<lambda> x P y. y = x \<or> P y" done
term "Lift_Set.insert"
thm Lift_Set.insert_def
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Tue Apr 03 20:56:32 2012 +0200
@@ -145,9 +145,9 @@
(abs_int (x + u, y + v))"
apply(simp add: plus_int_def id_simps)
apply(fold plus_int_raw.simps)
- apply(rule Quotient_rel_abs[OF Quotient_int])
+ apply(rule Quotient3_rel_abs[OF Quotient3_int])
apply(rule plus_int_raw_rsp_aux)
- apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
+ apply(simp_all add: rep_abs_rsp_left[OF Quotient3_int])
done
definition int_of_nat_raw:
--- a/src/HOL/Quotient_Examples/ROOT.ML Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Quotient_Examples/ROOT.ML Tue Apr 03 20:56:32 2012 +0200
@@ -5,5 +5,5 @@
*)
use_thys ["DList", "FSet", "Quotient_Int", "Quotient_Message",
- "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat"];
+ "Lift_Set", "Lift_RBT", "Lift_Fun", "Quotient_Rat", "Lift_DList"];
--- a/src/HOL/TPTP/TPTP_Parser/make_tptp_parser Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/make_tptp_parser Tue Apr 03 20:56:32 2012 +0200
@@ -30,7 +30,9 @@
for FILE in $INTERMEDIATE_FILES
do
- perl -p -e 's/\bref\b/Unsynchronized.ref/g;' -e 's/Unsafe\.(.*)/\1/g;' $FILE
+ perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \
+ -e 's/Unsafe\.(.*)/\1/g;' \
+ -e 's/\b(Char\.ord\()CharVector\.sub\b/\1String\.sub/g;' $FILE
done
) > tptp_lexyacc.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML Tue Apr 03 20:56:32 2012 +0200
@@ -1342,9 +1342,9 @@
yybl := size (!yyb);
scan (s,AcceptingLeaves,l-i0,0))
end
- else let val NewChar = Char.ord(CharVector.sub(!yyb,l))
+ else let val NewChar = Char.ord(String.sub(!yyb,l))
val NewChar = if NewChar<128 then NewChar else 128
- val NewState = Char.ord(CharVector.sub(trans,NewChar))
+ val NewState = Char.ord(String.sub(trans,NewChar))
in if NewState=0 then action(l,NewAcceptingLeaves)
else scan(NewState,NewAcceptingLeaves,l+1,i0)
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Tue Apr 03 20:56:32 2012 +0200
@@ -0,0 +1,291 @@
+(* Title: HOL/Tools/Lifting/lifting_def.ML
+ Author: Ondrej Kuncar
+
+Definitions for constants on quotient types.
+*)
+
+signature LIFTING_DEF =
+sig
+ val add_lift_def:
+ (binding * mixfix) -> typ -> term -> thm -> local_theory -> local_theory
+
+ val lift_def_cmd:
+ (binding * string option * mixfix) * string -> local_theory -> Proof.state
+
+ val can_generate_code_cert: thm -> bool
+end;
+
+structure Lifting_Def: LIFTING_DEF =
+struct
+
+(** Interface and Syntax Setup **)
+
+(* Generation of the code certificate from the rsp theorem *)
+
+infix 0 MRSL
+
+fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+
+fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
+ | get_body_types (U, V) = (U, V)
+
+fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
+ | get_binder_types _ = []
+
+fun force_rty_type ctxt rty rhs =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val rhs_schematic = singleton (Variable.polymorphic ctxt) rhs
+ val rty_schematic = fastype_of rhs_schematic
+ val match = Sign.typ_match thy (rty_schematic, rty) Vartab.empty
+ in
+ Envir.subst_term_types match rhs_schematic
+ end
+
+fun unabs_def ctxt def =
+ let
+ val (_, rhs) = Thm.dest_equals (cprop_of def)
+ fun dest_abs (Abs (var_name, T, _)) = (var_name, T)
+ | dest_abs tm = raise TERM("get_abs_var",[tm])
+ val (var_name, T) = dest_abs (term_of rhs)
+ val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt
+ val thy = Proof_Context.theory_of ctxt'
+ val refl_thm = Thm.reflexive (cterm_of thy (Free (hd new_var_names, T)))
+ in
+ Thm.combination def refl_thm |>
+ singleton (Proof_Context.export ctxt' ctxt)
+ end
+
+fun unabs_all_def ctxt def =
+ let
+ val (_, rhs) = Thm.dest_equals (cprop_of def)
+ val xs = strip_abs_vars (term_of rhs)
+ in
+ fold (K (unabs_def ctxt)) xs def
+ end
+
+val map_fun_unfolded =
+ @{thm map_fun_def[abs_def]} |>
+ unabs_def @{context} |>
+ unabs_def @{context} |>
+ Local_Defs.unfold @{context} [@{thm comp_def}]
+
+fun unfold_fun_maps ctm =
+ let
+ fun unfold_conv ctm =
+ case (Thm.term_of ctm) of
+ Const (@{const_name "map_fun"}, _) $ _ $ _ =>
+ (Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm
+ | _ => Conv.all_conv ctm
+ val try_beta_conv = Conv.try_conv (Thm.beta_conversion false)
+ in
+ (Conv.arg_conv (Conv.fun_conv unfold_conv then_conv try_beta_conv)) ctm
+ end
+
+fun prove_rel ctxt rsp_thm (rty, qty) =
+ let
+ val ty_args = get_binder_types (rty, qty)
+ fun disch_arg args_ty thm =
+ let
+ val quot_thm = Lifting_Term.prove_quot_theorem ctxt args_ty
+ in
+ [quot_thm, thm] MRSL @{thm apply_rsp''}
+ end
+ in
+ fold disch_arg ty_args rsp_thm
+ end
+
+exception CODE_CERT_GEN of string
+
+fun simplify_code_eq ctxt def_thm =
+ Local_Defs.unfold ctxt [@{thm o_def}, @{thm map_fun_def}, @{thm id_def}] def_thm
+
+fun can_generate_code_cert quot_thm =
+ case Lifting_Term.quot_thm_rel quot_thm of
+ Const (@{const_name HOL.eq}, _) => true
+ | Const (@{const_name invariant}, _) $ _ => true
+ | _ => false
+
+fun generate_code_cert ctxt def_thm rsp_thm (rty, qty) =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val quot_thm = Lifting_Term.prove_quot_theorem ctxt (get_body_types (rty, qty))
+ val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
+ val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs}
+ val abs_rep_eq =
+ case (HOLogic.dest_Trueprop o prop_of) fun_rel of
+ Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm
+ | Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq}
+ | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant"
+ val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
+ val unabs_def = unabs_all_def ctxt unfolded_def
+ val rep = (cterm_of thy o Lifting_Term.quot_thm_rep) quot_thm
+ val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
+ val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
+ val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans}
+ in
+ simplify_code_eq ctxt code_cert
+ end
+
+fun define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy =
+ let
+ val quot_thm = Lifting_Term.prove_quot_theorem lthy (get_body_types (rty, qty))
+ in
+ if can_generate_code_cert quot_thm then
+ let
+ val code_cert = generate_code_cert lthy def_thm rsp_thm (rty, qty)
+ val add_abs_eqn_attribute =
+ Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I)
+ val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
+ in
+ lthy
+ |> (snd oo Local_Theory.note) ((code_eqn_thm_name, [add_abs_eqn_attrib]), [code_cert])
+ end
+ else
+ lthy
+ end
+
+fun define_code_eq code_eqn_thm_name def_thm lthy =
+ let
+ val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
+ val code_eq = unabs_all_def lthy unfolded_def
+ val simp_code_eq = simplify_code_eq lthy code_eq
+ in
+ lthy
+ |> (snd oo Local_Theory.note) ((code_eqn_thm_name, [Code.add_default_eqn_attrib]), [simp_code_eq])
+ end
+
+fun define_code code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy =
+ if body_type rty = body_type qty then
+ define_code_eq code_eqn_thm_name def_thm lthy
+ else
+ define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy
+
+
+fun add_lift_def var qty rhs rsp_thm lthy =
+ let
+ val rty = fastype_of rhs
+ val absrep_trm = Lifting_Term.absrep_fun lthy (rty, qty)
+ val rty_forced = (domain_type o fastype_of) absrep_trm
+ val forced_rhs = force_rty_type lthy rty_forced rhs
+ val lhs = Free (Binding.print (#1 var), qty)
+ val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs)
+ val (_, prop') = Local_Defs.cert_def lthy prop
+ val (_, newrhs) = Local_Defs.abs_def prop'
+
+ val ((_, (_ , def_thm)), lthy') =
+ Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
+
+ fun qualify defname suffix = Binding.name suffix
+ |> Binding.qualify true defname
+
+ val lhs_name = Binding.name_of (#1 var)
+ val rsp_thm_name = qualify lhs_name "rsp"
+ val code_eqn_thm_name = qualify lhs_name "rep_eq"
+ in
+ lthy'
+ |> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm])
+ |> define_code code_eqn_thm_name def_thm rsp_thm (rty_forced, qty)
+ end
+
+fun mk_readable_rsp_thm_eq tm lthy =
+ let
+ val ctm = cterm_of (Proof_Context.theory_of lthy) tm
+
+ fun norm_fun_eq ctm =
+ let
+ fun abs_conv2 cv = Conv.abs_conv (K (Conv.abs_conv (K cv) lthy)) lthy
+ fun erase_quants ctm' =
+ case (Thm.term_of ctm') of
+ Const ("HOL.eq", _) $ _ $ _ => Conv.all_conv ctm'
+ | _ => (Conv.binder_conv (K erase_quants) lthy then_conv
+ Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
+ in
+ (abs_conv2 erase_quants then_conv Thm.eta_conversion) ctm
+ end
+
+ fun simp_arrows_conv ctm =
+ let
+ val unfold_conv = Conv.rewrs_conv
+ [@{thm fun_rel_eq_invariant[THEN eq_reflection]}, @{thm fun_rel_eq_rel[THEN eq_reflection]},
+ @{thm fun_rel_def[THEN eq_reflection]}]
+ val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
+ fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
+ in
+ case (Thm.term_of ctm) of
+ Const (@{const_name "fun_rel"}, _) $ _ $ _ =>
+ (binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm
+ | _ => Conv.all_conv ctm
+ end
+
+ val unfold_ret_val_invs = Conv.bottom_conv
+ (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy
+ val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
+ val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
+ val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
+ val beta_conv = Thm.beta_conversion true
+ val eq_thm =
+ (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
+ in
+ Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2)
+ end
+
+
+
+fun lift_def_cmd (raw_var, rhs_raw) lthy =
+ let
+ val ((binding, SOME qty, mx), ctxt) = yield_singleton Proof_Context.read_vars raw_var lthy
+ val rhs = (Syntax.check_term ctxt o Syntax.parse_term ctxt) rhs_raw
+
+ fun try_to_prove_refl thm =
+ let
+ val lhs_eq =
+ thm
+ |> prop_of
+ |> Logic.dest_implies
+ |> fst
+ |> strip_all_body
+ |> try HOLogic.dest_Trueprop
+ in
+ case lhs_eq of
+ SOME (Const ("HOL.eq", _) $ _ $ _) => SOME (@{thm refl} RS thm)
+ | _ => NONE
+ end
+
+ val rsp_rel = Lifting_Term.equiv_relation lthy (fastype_of rhs, qty)
+ val rty_forced = (domain_type o fastype_of) rsp_rel;
+ val forced_rhs = force_rty_type lthy rty_forced rhs;
+ val internal_rsp_tm = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
+ val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy
+ val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
+ val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq)
+
+ fun after_qed thm_list lthy =
+ let
+ val internal_rsp_thm =
+ case thm_list of
+ [] => the maybe_proven_rsp_thm
+ | [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm
+ (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1)
+ in
+ add_lift_def (binding, mx) qty rhs internal_rsp_thm lthy
+ end
+
+ in
+ case maybe_proven_rsp_thm of
+ SOME _ => Proof.theorem NONE after_qed [] lthy
+ | NONE => Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy
+ end
+
+(* parser and command *)
+val liftdef_parser =
+ ((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2)
+ --| @{keyword "is"} -- Parse.term
+
+val _ =
+ Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"}
+ "definition for constants over the quotient type"
+ (liftdef_parser >> lift_def_cmd)
+
+
+end; (* structure *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Tue Apr 03 20:56:32 2012 +0200
@@ -0,0 +1,125 @@
+(* Title: HOL/Tools/Lifting/lifting_info.ML
+ Author: Ondrej Kuncar
+
+Context data for the lifting package.
+*)
+
+signature LIFTING_INFO =
+sig
+ type quotmaps = {relmap: string, quot_thm: thm}
+ val lookup_quotmaps: Proof.context -> string -> quotmaps option
+ val lookup_quotmaps_global: theory -> string -> quotmaps option
+ val print_quotmaps: Proof.context -> unit
+
+ type quotients = {quot_thm: thm}
+ val transform_quotients: morphism -> quotients -> quotients
+ val lookup_quotients: Proof.context -> string -> quotients option
+ val lookup_quotients_global: theory -> string -> quotients option
+ val update_quotients: string -> quotients -> Context.generic -> Context.generic
+ val dest_quotients: Proof.context -> quotients list
+ val print_quotients: Proof.context -> unit
+
+ val setup: theory -> theory
+end;
+
+structure Lifting_Info: LIFTING_INFO =
+struct
+
+(** data containers **)
+
+(* FIXME just one data slot (record) per program unit *)
+
+(* info about map- and rel-functions for a type *)
+type quotmaps = {relmap: string, quot_thm: thm}
+
+structure Quotmaps = Generic_Data
+(
+ type T = quotmaps Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ fun merge data = Symtab.merge (K true) data
+)
+
+val lookup_quotmaps = Symtab.lookup o Quotmaps.get o Context.Proof
+val lookup_quotmaps_global = Symtab.lookup o Quotmaps.get o Context.Theory
+
+(* FIXME export proper internal update operation!? *)
+
+val quotmaps_attribute_setup =
+ Attrib.setup @{binding map}
+ ((Args.type_name true --| Scan.lift @{keyword "="}) --
+ (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} --
+ Attrib.thm --| Scan.lift @{keyword ")"}) >>
+ (fn (tyname, (relname, qthm)) =>
+ let val minfo = {relmap = relname, quot_thm = qthm}
+ in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
+ "declaration of map information"
+
+fun print_quotmaps ctxt =
+ let
+ fun prt_map (ty_name, {relmap, quot_thm}) =
+ Pretty.block (separate (Pretty.brk 2)
+ [Pretty.str "type:",
+ Pretty.str ty_name,
+ Pretty.str "relation map:",
+ Pretty.str relmap,
+ Pretty.str "quot. theorem:",
+ Syntax.pretty_term ctxt (prop_of quot_thm)])
+ in
+ map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
+ |> Pretty.big_list "maps for type constructors:"
+ |> Pretty.writeln
+ end
+
+(* info about quotient types *)
+type quotients = {quot_thm: thm}
+
+structure Quotients = Generic_Data
+(
+ type T = quotients Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ fun merge data = Symtab.merge (K true) data
+)
+
+fun transform_quotients phi {quot_thm} =
+ {quot_thm = Morphism.thm phi quot_thm}
+
+val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
+val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
+
+fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo))
+
+fun dest_quotients ctxt = (* FIXME slightly expensive way to retrieve data *)
+ map snd (Symtab.dest (Quotients.get (Context.Proof ctxt)))
+
+fun print_quotients ctxt =
+ let
+ fun prt_quot (qty_name, {quot_thm}) =
+ Pretty.block (separate (Pretty.brk 2)
+ [Pretty.str "type:",
+ Pretty.str qty_name,
+ Pretty.str "quot. thm:",
+ Syntax.pretty_term ctxt (prop_of quot_thm)])
+ in
+ map prt_quot (Symtab.dest (Quotients.get (Context.Proof ctxt)))
+ |> Pretty.big_list "quotients:"
+ |> Pretty.writeln
+ end
+
+(* theory setup *)
+
+val setup =
+ quotmaps_attribute_setup
+
+(* outer syntax commands *)
+
+val _ =
+ Outer_Syntax.improper_command @{command_spec "print_quotmaps"} "print quotient map functions"
+ (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
+
+val _ =
+ Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
+ (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
+
+end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Apr 03 20:56:32 2012 +0200
@@ -0,0 +1,113 @@
+(* Title: HOL/Tools/Lifting/lifting_setup.ML
+ Author: Ondrej Kuncar
+
+Setting the lifting infranstructure up.
+*)
+
+signature LIFTING_SETUP =
+sig
+ exception SETUP_LIFTING_INFR of string
+
+ val setup_lifting_infr: thm -> thm -> local_theory -> local_theory
+
+ val setup_by_typedef_thm: thm -> local_theory -> local_theory
+end;
+
+structure Lifting_Seup: LIFTING_SETUP =
+struct
+
+infix 0 MRSL
+
+fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+
+exception SETUP_LIFTING_INFR of string
+
+fun define_cr_rel equiv_thm abs_fun lthy =
+ let
+ fun force_type_of_rel rel forced_ty =
+ let
+ val thy = Proof_Context.theory_of lthy
+ val rel_ty = (domain_type o fastype_of) rel
+ val ty_inst = Sign.typ_match thy (rel_ty, forced_ty) Vartab.empty
+ in
+ Envir.subst_term_types ty_inst rel
+ end
+
+ val (rty, qty) = (dest_funT o fastype_of) abs_fun
+ val abs_fun_graph = HOLogic.mk_eq(abs_fun $ Bound 1, Bound 0)
+ val Abs_body = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
+ Const (@{const_name equivp}, _) $ _ => abs_fun_graph
+ | Const (@{const_name part_equivp}, _) $ rel =>
+ HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
+ | _ => raise SETUP_LIFTING_INFR "unsopported equivalence theorem"
+ )
+ val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body));
+ val qty_name = (fst o dest_Type) qty
+ val cr_rel_name = Binding.prefix_name "cr_" (Binding.qualified_name qty_name)
+ val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
+ val ((_, (_ , def_thm)), lthy'') =
+ Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy'
+ in
+ (def_thm, lthy'')
+ end
+
+fun define_abs_type quot_thm lthy =
+ if Lifting_Def.can_generate_code_cert quot_thm then
+ let
+ val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
+ val add_abstype_attribute =
+ Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
+ val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
+ in
+ lthy
+ |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
+ end
+ else
+ lthy
+
+fun setup_lifting_infr quot_thm equiv_thm lthy =
+ let
+ val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
+ val qty_full_name = (fst o dest_Type) qtyp
+ val quotients = { quot_thm = quot_thm }
+ fun quot_info phi = Lifting_Info.transform_quotients phi quotients
+ in
+ lthy
+ |> Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
+ |> define_abs_type quot_thm
+ end
+
+fun setup_by_typedef_thm typedef_thm lthy =
+ let
+ fun derive_quot_and_equiv_thm to_quot_thm to_equiv_thm typedef_thm lthy =
+ let
+ val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
+ val equiv_thm = typedef_thm RS to_equiv_thm
+ val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
+ val quot_thm = [typedef_thm, T_def] MRSL to_quot_thm
+ in
+ (quot_thm, equiv_thm, lthy')
+ end
+
+ val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm
+ val (quot_thm, equiv_thm, lthy') = (case typedef_set of
+ Const ("Orderings.top_class.top", _) =>
+ derive_quot_and_equiv_thm @{thm copy_type_to_Quotient} @{thm copy_type_to_equivp}
+ typedef_thm lthy
+ | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) =>
+ derive_quot_and_equiv_thm @{thm invariant_type_to_Quotient} @{thm invariant_type_to_part_equivp}
+ typedef_thm lthy
+ | _ => raise SETUP_LIFTING_INFR "unsupported typedef theorem")
+ in
+ setup_lifting_infr quot_thm equiv_thm lthy'
+ end
+
+fun setup_by_typedef_thm_aux xthm lthy = setup_by_typedef_thm (singleton (Attrib.eval_thms lthy) xthm) lthy
+
+val _ =
+ Outer_Syntax.local_theory @{command_spec "setup_lifting"}
+ "Setup lifting infrastracture"
+ (Parse_Spec.xthm >> (fn xthm => setup_by_typedef_thm_aux xthm))
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Tue Apr 03 20:56:32 2012 +0200
@@ -0,0 +1,173 @@
+(* Title: HOL/Tools/Lifting/lifting_term.ML
+ Author: Ondrej Kuncar
+
+Proves Quotient theorem.
+*)
+
+signature LIFTING_TERM =
+sig
+ val prove_quot_theorem: Proof.context -> typ * typ -> thm
+
+ val absrep_fun: Proof.context -> typ * typ -> term
+
+ (* Allows Nitpick to represent quotient types as single elements from raw type *)
+ (* val absrep_const_chk: Proof.context -> flag -> string -> term *)
+
+ val equiv_relation: Proof.context -> typ * typ -> term
+
+ val quot_thm_rel: thm -> term
+ val quot_thm_abs: thm -> term
+ val quot_thm_rep: thm -> term
+ val quot_thm_rty_qty: thm -> typ * typ
+end
+
+structure Lifting_Term: LIFTING_TERM =
+struct
+
+exception LIFT_MATCH of string
+
+(* matches a type pattern with a type *)
+fun match ctxt err ty_pat ty =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ in
+ Sign.typ_match thy (ty_pat, ty) Vartab.empty
+ handle Type.TYPE_MATCH => err ctxt ty_pat ty
+ end
+
+fun equiv_match_err ctxt ty_pat ty =
+ let
+ val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
+ val ty_str = Syntax.string_of_typ ctxt ty
+ in
+ raise LIFT_MATCH (space_implode " "
+ ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
+ end
+
+(* generation of the Quotient theorem *)
+
+exception QUOT_THM of string
+
+fun get_quot_thm ctxt s =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ in
+ (case Lifting_Info.lookup_quotients ctxt s of
+ SOME qdata => Thm.transfer thy (#quot_thm qdata)
+ | NONE => raise QUOT_THM ("No quotient type " ^ quote s ^ " found."))
+ end
+
+fun get_rel_quot_thm ctxt s =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ in
+ (case Lifting_Info.lookup_quotmaps ctxt s of
+ SOME map_data => Thm.transfer thy (#quot_thm map_data)
+ | NONE => raise QUOT_THM ("get_relmap (no relation map function found for type " ^ s ^ ")"))
+ end
+
+fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
+
+infix 0 MRSL
+
+fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+
+exception NOT_IMPL of string
+
+fun quot_thm_rel quot_thm =
+ let
+ val (Const (@{const_name Quotient}, _) $ rel $ _ $ _ $ _) =
+ (HOLogic.dest_Trueprop o prop_of) quot_thm
+ in
+ rel
+ end
+
+fun quot_thm_abs quot_thm =
+ let
+ val (Const (@{const_name Quotient}, _) $ _ $ abs $ _ $ _) =
+ (HOLogic.dest_Trueprop o prop_of) quot_thm
+ in
+ abs
+ end
+
+fun quot_thm_rep quot_thm =
+ let
+ val (Const (@{const_name Quotient}, _) $ _ $ _ $ rep $ _) =
+ (HOLogic.dest_Trueprop o prop_of) quot_thm
+ in
+ rep
+ end
+
+fun quot_thm_rty_qty quot_thm =
+ let
+ val abs = quot_thm_abs quot_thm
+ val abs_type = fastype_of abs
+ in
+ (domain_type abs_type, range_type abs_type)
+ end
+
+fun prove_quot_theorem ctxt (rty, qty) =
+ case (rty, qty) of
+ (Type (s, tys), Type (s', tys')) =>
+ if s = s'
+ then
+ let
+ val args = map (prove_quot_theorem ctxt) (tys ~~ tys')
+ in
+ if forall is_id_quot args
+ then
+ @{thm identity_quotient}
+ else
+ args MRSL (get_rel_quot_thm ctxt s)
+ end
+ else
+ let
+ val quot_thm = get_quot_thm ctxt s'
+ val (Type (_, rtys), qty_pat) = quot_thm_rty_qty quot_thm
+ val qtyenv = match ctxt equiv_match_err qty_pat qty
+ val rtys' = map (Envir.subst_type qtyenv) rtys
+ val args = map (prove_quot_theorem ctxt) (tys ~~ rtys')
+ in
+ if forall is_id_quot args
+ then
+ quot_thm
+ else
+ let
+ val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s)
+ in
+ [rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose}
+ end
+ end
+ | _ => @{thm identity_quotient}
+
+fun force_qty_type thy qty quot_thm =
+ let
+ val abs_schematic = quot_thm_abs quot_thm
+ val qty_schematic = (range_type o fastype_of) abs_schematic
+ val match_env = Sign.typ_match thy (qty_schematic, qty) Vartab.empty
+ fun prep_ty thy (x, (S, ty)) =
+ (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
+ val ty_inst = Vartab.fold (cons o (prep_ty thy)) match_env []
+ in
+ Thm.instantiate (ty_inst, []) quot_thm
+ end
+
+fun absrep_fun ctxt (rty, qty) =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val quot_thm = prove_quot_theorem ctxt (rty, qty)
+ val forced_quot_thm = force_qty_type thy qty quot_thm
+ in
+ quot_thm_abs forced_quot_thm
+ end
+
+fun equiv_relation ctxt (rty, qty) =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val quot_thm = prove_quot_theorem ctxt (rty, qty)
+ val forced_quot_thm = force_qty_type thy qty quot_thm
+ in
+ quot_thm_rel forced_quot_thm
+ end
+
+end;
--- a/src/HOL/Tools/Quotient/quotient_def.ML Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Tue Apr 03 20:56:32 2012 +0200
@@ -86,7 +86,7 @@
let
val quot_thm = Quotient_Term.prove_quot_theorem ctxt args_ty
in
- [quot_thm, thm] MRSL @{thm apply_rsp''}
+ [quot_thm, thm] MRSL @{thm apply_rspQ3''}
end
in
fold disch_arg ty_args rsp_thm
@@ -101,11 +101,11 @@
let
val quot_thm = Quotient_Term.prove_quot_theorem ctxt (get_body_types (rty, qty))
val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
- val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs}
+ val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient3_rep_abs}
val abs_rep_eq =
case (HOLogic.dest_Trueprop o prop_of) fun_rel of
Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm
- | Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq}
+ | Const (@{const_name Lifting.invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq}
| _ => raise CODE_CERT_GEN "relation is neither equality nor invariant"
val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
val unabs_def = unabs_all_def ctxt unfolded_def
--- a/src/HOL/Tools/Quotient/quotient_info.ML Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Tue Apr 03 20:56:32 2012 +0200
@@ -70,7 +70,7 @@
(* FIXME export proper internal update operation!? *)
val quotmaps_attribute_setup =
- Attrib.setup @{binding map}
+ Attrib.setup @{binding mapQ3}
((Args.type_name true --| Scan.lift @{keyword "="}) --
(Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} --
Attrib.thm --| Scan.lift @{keyword ")"}) >>
@@ -298,11 +298,11 @@
(* outer syntax commands *)
val _ =
- Outer_Syntax.improper_command @{command_spec "print_quotmaps"} "print quotient map functions"
+ Outer_Syntax.improper_command @{command_spec "print_quotmapsQ3"} "print quotient map functions"
(Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
val _ =
- Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
+ Outer_Syntax.improper_command @{command_spec "print_quotientsQ3"} "print quotients"
(Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
val _ =
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Apr 03 20:56:32 2012 +0200
@@ -62,7 +62,7 @@
fun quotient_tac ctxt =
(REPEAT_ALL_NEW (FIRST'
- [rtac @{thm identity_quotient},
+ [rtac @{thm identity_quotient3},
resolve_tac (Quotient_Info.quotient_rules ctxt)]))
fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
@@ -259,7 +259,7 @@
val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
val inst_thm = Drule.instantiate' ty_inst
- ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
+ ([NONE, NONE, NONE] @ t_inst) @{thm apply_rspQ3}
in
(rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1
end
@@ -529,7 +529,7 @@
val prs = Quotient_Info.prs_rules lthy
val ids = Quotient_Info.id_simps lthy
val thms =
- @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
+ @{thms Quotient3_abs_rep Quotient3_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
in
--- a/src/HOL/Tools/Quotient/quotient_term.ML Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Tue Apr 03 20:56:32 2012 +0200
@@ -356,7 +356,7 @@
| NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")"))
end
-fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
+fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient3})
infix 0 MRSL
@@ -375,13 +375,13 @@
let
val quot_thm_rel = get_rel_from_quot_thm quot_thm
in
- if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient}
+ if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient3}
else raise NOT_IMPL "nested quotients: not implemented yet"
end
fun prove_quot_theorem ctxt (rty, qty) =
if rty = qty
- then @{thm identity_quotient}
+ then @{thm identity_quotient3}
else
case (rty, qty) of
(Type (s, tys), Type (s', tys')) =>
@@ -410,7 +410,7 @@
mk_quot_thm_compose (rel_quot_thm, quot_thm)
end
end
- | _ => @{thm identity_quotient}
+ | _ => @{thm identity_quotient3}
--- a/src/HOL/Tools/Quotient/quotient_type.ML Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Tue Apr 03 20:56:32 2012 +0200
@@ -82,13 +82,13 @@
fun can_generate_code_cert quot_thm =
case Quotient_Term.get_rel_from_quot_thm quot_thm of
Const (@{const_name HOL.eq}, _) => true
- | Const (@{const_name invariant}, _) $ _ => true
+ | Const (@{const_name Lifting.invariant}, _) $ _ => true
| _ => false
fun define_abs_type quot_thm lthy =
if can_generate_code_cert quot_thm then
let
- val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
+ val abs_type_thm = quot_thm RS @{thm Quotient3_abs_rep}
val add_abstype_attribute =
Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
@@ -157,7 +157,7 @@
val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
(* quotient theorem *)
- val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
+ val quotient_thm_name = Binding.prefix_name "Quotient3_" qty_name
val quotient_thm =
(quot_thm RS @{thm quot_type.Quotient})
|> fold_rule [abs_def, rep_def]
@@ -313,30 +313,5 @@
"quotient type definitions (require equivalence proofs)"
(quotspec_parser >> quotient_type_cmd)
-(* Setup lifting using type_def_thm *)
-
-exception SETUP_LIFT_TYPE of string
-
-fun setup_lift_type typedef_thm =
- let
- val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm
- val (quot_thm, equivp_thm) = (case typedef_set of
- Const ("Orderings.top_class.top", _) =>
- (typedef_thm RS @{thm copy_type_to_Quotient},
- typedef_thm RS @{thm copy_type_to_equivp})
- | Const (@{const_name "Collect"}, _) $ Abs (_, _, _ $ Bound 0) =>
- (typedef_thm RS @{thm invariant_type_to_Quotient},
- typedef_thm RS @{thm invariant_type_to_part_equivp})
- | _ => raise SETUP_LIFT_TYPE "unsupported typedef theorem")
- in
- init_quotient_infr quot_thm equivp_thm
- end
-
-fun setup_lift_type_aux xthm lthy = setup_lift_type (singleton (Attrib.eval_thms lthy) xthm) lthy
-
-val _ =
- Outer_Syntax.local_theory @{command_spec "setup_lifting"}
- "Setup lifting infrastracture"
- (Parse_Spec.xthm >> (fn xthm => setup_lift_type_aux xthm))
end;
--- a/src/HOL/ex/Executable_Relation.thy Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/ex/Executable_Relation.thy Tue Apr 03 20:56:32 2012 +0200
@@ -67,11 +67,11 @@
lemma [simp]:
"rel_of_set (set_of_rel S) = S"
-by (rule Quotient_abs_rep[OF Quotient_rel])
+by (rule Quotient3_abs_rep[OF Quotient3_rel])
lemma [simp]:
"set_of_rel (rel_of_set R) = R"
-by (rule Quotient_rep_abs[OF Quotient_rel]) (rule refl)
+by (rule Quotient3_rep_abs[OF Quotient3_rel]) (rule refl)
lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"]
--- a/src/Pure/Isar/class.ML Tue Apr 03 15:15:00 2012 +0200
+++ b/src/Pure/Isar/class.ML Tue Apr 03 20:56:32 2012 +0200
@@ -486,13 +486,12 @@
##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
##> Local_Theory.map_contexts (K synchronize_inst_syntax);
-fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+fun foundation (((b, U), mx), (b_def, rhs)) params lthy =
(case instantiation_param lthy b of
SOME c =>
if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
- | NONE => lthy |>
- Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params));
+ | NONE => lthy |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) params);
fun pretty lthy =
let
@@ -553,10 +552,8 @@
|> Local_Theory.init naming
{define = Generic_Target.define foundation,
notes = Generic_Target.notes Generic_Target.theory_notes,
- abbrev = Generic_Target.abbrev
- (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
- Generic_Target.theory_abbrev prmode ((b, mx), t)),
- declaration = K Generic_Target.standard_declaration,
+ abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
+ declaration = K Generic_Target.theory_declaration,
pretty = pretty,
exit = Local_Theory.target_of o conclude}
end;
--- a/src/Pure/Isar/expression.ML Tue Apr 03 15:15:00 2012 +0200
+++ b/src/Pure/Isar/expression.ML Tue Apr 03 20:56:32 2012 +0200
@@ -43,12 +43,9 @@
(Attrib.binding * term) list -> theory -> Proof.state
val sublocale_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
(Attrib.binding * string) list -> theory -> Proof.state
- val interpretation: expression_i -> (Attrib.binding * term) list ->
- theory -> Proof.state
- val interpretation_cmd: expression -> (Attrib.binding * string) list ->
- theory -> Proof.state
- val interpret: expression_i -> (Attrib.binding * term) list ->
- bool -> Proof.state -> Proof.state
+ val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state
+ val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state
+ val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
val interpret_cmd: expression -> (Attrib.binding * string) list ->
bool -> Proof.state -> Proof.state
--- a/src/Pure/Isar/generic_target.ML Tue Apr 03 15:15:00 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML Tue Apr 03 20:56:32 2012 +0200
@@ -24,15 +24,23 @@
term list -> local_theory -> local_theory) ->
string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
val background_declaration: declaration -> local_theory -> local_theory
- val standard_declaration: declaration -> local_theory -> local_theory
val locale_declaration: string -> bool -> declaration -> local_theory -> local_theory
+ val standard_declaration: (int -> bool) -> declaration -> local_theory -> local_theory
+ val generic_const: bool -> Syntax.mode -> (binding * mixfix) * term ->
+ Context.generic -> Context.generic
+ val const_declaration: (int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
+ local_theory -> local_theory
+ val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
+ term list * term list -> local_theory -> (term * thm) * local_theory
val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
term list * term list -> local_theory -> (term * thm) * local_theory
val theory_notes: string ->
(Attrib.binding * (thm list * Args.src list) list) list ->
(Attrib.binding * (thm list * Args.src list) list) list ->
local_theory -> local_theory
- val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
+ val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term * term -> term list ->
+ local_theory -> local_theory
+ val theory_declaration: declaration -> local_theory -> local_theory
end
structure Generic_Target: GENERIC_TARGET =
@@ -52,6 +60,11 @@
else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)));
NoSyn);
+fun check_mixfix_global (b, no_params) mx =
+ if no_params orelse mx = NoSyn then mx
+ else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^
+ Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn);
+
(* define *)
@@ -61,21 +74,17 @@
val thy_ctxt = Proof_Context.init_global thy;
(*term and type parameters*)
- val crhs = Thm.cterm_of thy rhs;
- val ((defs, _), rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of;
+ val ((defs, _), rhs') = Thm.cterm_of thy rhs
+ |> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of;
- val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
+ val xs = Variable.add_fixed lthy rhs' [];
val T = Term.fastype_of rhs;
val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []);
val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs []));
val mx' = check_mixfix lthy (b, extra_tfrees) mx;
val type_params = map (Logic.mk_type o TFree) extra_tfrees;
- val target_ctxt = Local_Theory.target_of lthy;
- val term_params =
- filter (Variable.is_fixed target_ctxt o #1) xs
- |> sort (Variable.fixed_ord target_ctxt o pairself #1)
- |> map Free;
+ val term_params = map Free (sort (Variable.fixed_ord lthy o pairself #1) xs);
val params = type_params @ term_params;
val U = map Term.fastype_of params ---> T;
@@ -184,18 +193,15 @@
fun abbrev target_abbrev prmode ((b, mx), t) lthy =
let
val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
- val target_ctxt = Local_Theory.target_of lthy;
- val t' = Assumption.export_term lthy target_ctxt t;
- val xs = map Free (rev (Variable.add_fixed target_ctxt t' []));
+ val t' = Assumption.export_term lthy (Local_Theory.target_of lthy) t;
+ val xs = map Free (sort (Variable.fixed_ord lthy o pairself #1) (Variable.add_fixed lthy t' []));
val u = fold_rev lambda xs t';
+ val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
val extra_tfrees =
subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
val mx' = check_mixfix lthy (b, extra_tfrees) mx;
-
- val global_rhs =
- singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
in
lthy
|> target_abbrev prmode (b, mx') (global_rhs, t') xs
@@ -213,31 +219,83 @@
(Proof_Context.init_global (Proof_Context.theory_of lthy)) decl;
in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end;
-fun standard_declaration decl =
- background_declaration decl #>
- (fn lthy => Local_Theory.map_contexts (fn _ => fn ctxt =>
- Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt) lthy);
-
fun locale_declaration locale syntax decl lthy = lthy
|> Local_Theory.target (fn ctxt => ctxt |>
Locale.add_declaration locale syntax
(Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
+fun standard_declaration pred decl lthy =
+ Local_Theory.map_contexts (fn level => fn ctxt =>
+ if pred level then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt
+ else ctxt) lthy;
+
+
+(* const declaration *)
+
+fun generic_const same_shape prmode ((b, mx), t) context =
+ let
+ val const_alias =
+ if same_shape then
+ (case t of
+ Const (c, T) =>
+ let
+ val thy = Context.theory_of context;
+ val ctxt = Context.proof_of context;
+ in
+ (case Type_Infer_Context.const_type ctxt c of
+ SOME T' => if Sign.typ_equiv thy (T, T') then SOME c else NONE
+ | NONE => NONE)
+ end
+ | _ => NONE)
+ else NONE;
+ in
+ (case const_alias of
+ SOME c =>
+ context
+ |> Context.mapping (Sign.const_alias b c) (Proof_Context.const_alias b c)
+ |> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)])
+ | NONE =>
+ context
+ |> Proof_Context.generic_add_abbrev Print_Mode.internal (b, Term.close_schematic_term t)
+ |-> (fn (const as Const (c, _), _) => same_shape ?
+ (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
+ Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
+ end;
+
+fun const_declaration pred prmode ((b, mx), rhs) =
+ standard_declaration pred (fn phi =>
+ let
+ val b' = Morphism.binding phi b;
+ val rhs' = Morphism.term phi rhs;
+ val same_shape = Term.aconv_untyped (rhs, rhs');
+ in generic_const same_shape prmode ((b', mx), rhs') end);
+
(** primitive theory operations **)
-fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
let
+ val params = type_params @ term_params;
+ val mx' = check_mixfix_global (b, null params) mx;
+
val (const, lthy2) = lthy
- |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx));
- val lhs = list_comb (const, type_params @ term_params);
+ |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx'));
+ val lhs = Term.list_comb (const, params);
+
val ((_, def), lthy3) = lthy2
|> Local_Theory.background_theory_result
(Thm.add_def lthy2 false false
(Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
in ((lhs, def), lthy3) end;
+fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
+ background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)
+ #-> (fn (lhs, def) => fn lthy' => lthy' |>
+ const_declaration (fn level => level <> Local_Theory.level lthy')
+ Syntax.mode_default ((b, mx), lhs)
+ |> pair (lhs, def));
+
fun theory_notes kind global_facts local_facts =
Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #>
(fn lthy => lthy |> Local_Theory.map_contexts (fn level => fn ctxt =>
@@ -246,9 +304,16 @@
ctxt |> Attrib.local_notes kind
(Element.transform_facts (Local_Theory.standard_morphism lthy ctxt) local_facts) |> snd));
-fun theory_abbrev prmode ((b, mx), t) =
- Local_Theory.background_theory
+fun theory_abbrev prmode (b, mx) (t, _) xs =
+ Local_Theory.background_theory_result
(Sign.add_abbrev (#1 prmode) (b, t) #->
- (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
+ (fn (lhs, _) => (* FIXME type_params!? *)
+ Sign.notation true prmode [(lhs, check_mixfix_global (b, null xs) mx)] #> pair lhs))
+ #-> (fn lhs => fn lthy' => lthy' |>
+ const_declaration (fn level => level <> Local_Theory.level lthy') prmode
+ ((b, if null xs then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
+
+fun theory_declaration decl =
+ background_declaration decl #> standard_declaration (K true) decl;
end;
--- a/src/Pure/Isar/local_defs.ML Tue Apr 03 15:15:00 2012 +0200
+++ b/src/Pure/Isar/local_defs.ML Tue Apr 03 20:56:32 2012 +0200
@@ -135,22 +135,22 @@
let
val exp = Assumption.export false inner outer;
val exp_term = Assumption.export_term inner outer;
- val prems = Assumption.local_prems_of inner outer;
+ val asms = Assumption.local_assms_of inner outer;
in
fn th =>
let
val th' = exp th;
- val defs_asms = prems |> map (fn prem =>
- (case try (head_of_def o Thm.prop_of) prem of
- NONE => (prem, false)
+ val defs_asms = asms |> map (Thm.assume #> (fn asm =>
+ (case try (head_of_def o Thm.prop_of) asm of
+ NONE => (asm, false)
| SOME x =>
let val t = Free x in
(case try exp_term t of
- NONE => (prem, false)
+ NONE => (asm, false)
| SOME u =>
- if t aconv u then (prem, false)
- else (Drule.abs_def prem, true))
- end));
+ if t aconv u then (asm, false)
+ else (Drule.abs_def (Drule.gen_all asm), true))
+ end)));
in (pairself (map #1) (List.partition #2 defs_asms), th') end
end;
--- a/src/Pure/Isar/local_theory.ML Tue Apr 03 15:15:00 2012 +0200
+++ b/src/Pure/Isar/local_theory.ML Tue Apr 03 20:56:32 2012 +0200
@@ -11,6 +11,7 @@
sig
type operations
val assert: local_theory -> local_theory
+ val restore: local_theory -> local_theory
val level: Proof.context -> int
val assert_bottom: bool -> local_theory -> local_theory
val open_target: Name_Space.naming -> operations -> local_theory -> local_theory
@@ -54,7 +55,6 @@
val type_alias: binding -> string -> local_theory -> local_theory
val const_alias: binding -> string -> local_theory -> local_theory
val init: Name_Space.naming -> operations -> Proof.context -> local_theory
- val restore: local_theory -> local_theory
val exit: local_theory -> Proof.context
val exit_global: local_theory -> theory
val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
@@ -107,6 +107,8 @@
Data.map (fn {naming, operations, target} :: parents =>
make_lthy (f (naming, operations, target)) :: parents);
+fun restore lthy = #target (get_first_lthy lthy) |> Data.put (Data.get lthy);
+
(* nested structure *)
@@ -126,7 +128,7 @@
|> Data.map (cons (make_lthy (naming, operations, target)));
fun close_target lthy =
- assert_bottom false lthy |> Data.map tl;
+ assert_bottom false lthy |> Data.map tl |> restore;
fun map_contexts f lthy =
let val n = level lthy in
@@ -281,10 +283,6 @@
| _ => error "Local theory already initialized")
|> checkpoint;
-fun restore lthy =
- let val {naming, operations, target} = get_first_lthy lthy
- in init naming operations target end;
-
(* exit *)
--- a/src/Pure/Isar/named_target.ML Tue Apr 03 15:15:00 2012 +0200
+++ b/src/Pure/Isar/named_target.ML Tue Apr 03 20:56:32 2012 +0200
@@ -46,12 +46,11 @@
(* consts in locale *)
-fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) =
+fun locale_const (Target {target, is_class, ...}) prmode ((b, mx), rhs) =
Generic_Target.locale_declaration target true (fn phi =>
let
val b' = Morphism.binding phi b;
val rhs' = Morphism.term phi rhs;
- val arg = (b', Term.close_schematic_term rhs');
val same_shape = Term.aconv_untyped (rhs, rhs');
(* FIXME workaround based on educated guess *)
@@ -62,31 +61,24 @@
andalso List.last prefix' = (Class.class_prefix target, false)
orelse same_shape);
in
- not is_canonical_class ?
- (Context.mapping_result
- (Sign.add_abbrev Print_Mode.internal arg)
- (Proof_Context.add_abbrev Print_Mode.internal arg)
- #-> (fn (lhs' as Const (d, _), _) =>
- same_shape ?
- (Context.mapping
- (Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #>
- Morphism.form (Proof_Context.generic_notation true prmode [(lhs', mx)]))))
- end);
+ not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', mx), rhs')
+ end) #>
+ (fn lthy => lthy |> Generic_Target.const_declaration
+ (fn level => level <> 0 andalso level <> Local_Theory.level lthy) prmode ((b, mx), rhs));
(* define *)
-fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
- Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
+fun locale_foundation ta (((b, U), mx), (b_def, rhs)) params =
+ Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params
#-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs)
- #> pair (lhs, def))
+ #> pair (lhs, def));
-fun class_foundation (ta as Target {target, ...})
- (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
- Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
+fun class_foundation (ta as Target {target, ...}) (((b, U), mx), (b_def, rhs)) params =
+ Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params
#-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs)
- #> Class.const target ((b, mx), (type_params, lhs))
- #> pair (lhs, def))
+ #> Class.const target ((b, mx), (#1 params, lhs))
+ #> pair (lhs, def));
fun target_foundation (ta as Target {is_locale, is_class, ...}) =
if is_class then class_foundation ta
@@ -106,31 +98,26 @@
fun locale_abbrev ta prmode ((b, mx), t) xs =
Local_Theory.background_theory_result
(Sign.add_abbrev Print_Mode.internal (b, t)) #->
- (fn (lhs, _) => locale_const ta prmode
- ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
+ (fn (lhs, _) =>
+ locale_const ta prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
-fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
- prmode (b, mx) (global_rhs, t') xs lthy =
+fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) prmode (b, mx) (t, t') xs lthy =
if is_locale then
lthy
- |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
+ |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), t) xs
|> is_class ? Class.abbrev target prmode ((b, mx), t')
- else
- lthy
- |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
+ else lthy |> Generic_Target.theory_abbrev prmode (b, mx) (t, t') xs;
(* declaration *)
fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
- if target = "" then Generic_Target.standard_declaration decl lthy
+ if target = "" then Generic_Target.theory_declaration decl lthy
else
lthy
|> pervasive ? Generic_Target.background_declaration decl
|> Generic_Target.locale_declaration target syntax decl
- |> (fn lthy' => lthy' |> Local_Theory.map_contexts (fn level => fn ctxt =>
- if level = 0 then ctxt
- else Context.proof_map (Local_Theory.standard_form lthy' ctxt decl) ctxt));
+ |> (fn lthy' => lthy' |> Generic_Target.standard_declaration (fn level => level <> 0) decl);
(* pretty *)
@@ -192,7 +179,7 @@
Local_Theory.assert_bottom true #> Data.get #> the #>
(fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target);
-fun context_cmd ("-", _) thy = init I "" thy
+fun context_cmd ("-", _) thy = theory_init thy
| context_cmd target thy = init I (Locale.check thy target) thy;
end;
--- a/src/Pure/Isar/overloading.ML Tue Apr 03 15:15:00 2012 +0200
+++ b/src/Pure/Isar/overloading.ML Tue Apr 03 20:56:32 2012 +0200
@@ -158,14 +158,13 @@
##> Local_Theory.map_contexts (K synchronize_syntax)
#-> (fn (_, def) => pair (Const (c, U), def));
-fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+fun foundation (((b, U), mx), (b_def, rhs)) params lthy =
(case operation lthy b of
SOME (c, (v, checked)) =>
if mx <> NoSyn
then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
- | NONE => lthy
- |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params));
+ | NONE => lthy |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) params);
fun pretty lthy =
let
@@ -204,10 +203,8 @@
|> Local_Theory.init naming
{define = Generic_Target.define foundation,
notes = Generic_Target.notes Generic_Target.theory_notes,
- abbrev = Generic_Target.abbrev
- (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
- Generic_Target.theory_abbrev prmode ((b, mx), t)),
- declaration = K Generic_Target.standard_declaration,
+ abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
+ declaration = K Generic_Target.theory_declaration,
pretty = pretty,
exit = Local_Theory.target_of o conclude}
end;
--- a/src/Pure/Isar/proof_context.ML Tue Apr 03 15:15:00 2012 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Apr 03 20:56:32 2012 +0200
@@ -146,6 +146,9 @@
val add_const_constraint: string * typ option -> Proof.context -> Proof.context
val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context
val revert_abbrev: string -> string -> Proof.context -> Proof.context
+ val generic_add_abbrev: string -> binding * term -> Context.generic ->
+ (term * term) * Context.generic
+ val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
val print_syntax: Proof.context -> unit
val print_abbrevs: Proof.context -> unit
val print_binds: Proof.context -> unit
@@ -1021,6 +1024,12 @@
fun revert_abbrev mode c = (map_consts o apfst) (Consts.revert_abbrev mode c);
+fun generic_add_abbrev mode arg =
+ Context.mapping_result (Sign.add_abbrev mode arg) (add_abbrev mode arg);
+
+fun generic_revert_abbrev mode arg =
+ Context.mapping (Sign.revert_abbrev mode arg) (revert_abbrev mode arg);
+
(* fixes *)
--- a/src/Pure/Isar/toplevel.ML Tue Apr 03 15:15:00 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Apr 03 20:56:32 2012 +0200
@@ -109,13 +109,12 @@
val loc_init = Named_Target.context_cmd;
val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
-fun loc_begin loc (Context.Theory thy) = loc_init (the_default ("-", Position.none) loc) thy
- | loc_begin NONE (Context.Proof lthy) = lthy
- | loc_begin (SOME loc) (Context.Proof lthy) = (loc_init loc o loc_exit) lthy;
-
-fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
- | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore
- | loc_finish (SOME _) (Context.Proof lthy) = Context.Proof o Named_Target.reinit lthy;
+fun loc_begin loc (Context.Theory thy) =
+ (Context.Theory o loc_exit, loc_init (the_default ("-", Position.none) loc) thy)
+ | loc_begin NONE (Context.Proof lthy) =
+ (Context.Proof o Local_Theory.restore, lthy)
+ | loc_begin (SOME loc) (Context.Proof lthy) =
+ (Context.Proof o Named_Target.reinit lthy, loc_init loc (loc_exit lthy));
(* datatype node *)
@@ -477,8 +476,8 @@
fun local_theory_presentation loc f = present_transaction (fn int =>
(fn Theory (gthy, _) =>
let
- val finish = loc_finish loc gthy;
- val lthy' = loc_begin loc gthy
+ val (finish, lthy) = loc_begin loc gthy;
+ val lthy' = lthy
|> local_theory_group
|> f int
|> Local_Theory.reset_group;
@@ -511,34 +510,37 @@
local
-fun begin_proof init finish = transaction (fn int =>
+fun begin_proof init = transaction (fn int =>
(fn Theory (gthy, _) =>
let
- val prf = init int gthy;
+ val (finish, prf) = init int gthy;
val skip = ! skip_proofs;
val (is_goal, no_skip) =
(true, Proof.schematic_goal prf) handle ERROR _ => (false, true);
+ val _ =
+ if is_goal andalso skip andalso no_skip then
+ warning "Cannot skip proof of schematic goal statement"
+ else ();
in
- if is_goal andalso skip andalso no_skip then
- warning "Cannot skip proof of schematic goal statement"
- else ();
if skip andalso not no_skip then
- SkipProof (0, (finish gthy (Proof.global_skip_proof int prf), gthy))
- else Proof (Proof_Node.init prf, (finish gthy, gthy))
+ SkipProof (0, (finish (Proof.global_skip_proof int prf), gthy))
+ else Proof (Proof_Node.init prf, (finish, gthy))
end
| _ => raise UNDEF));
in
fun local_theory_to_proof' loc f = begin_proof
- (fn int => fn gthy => f int (local_theory_group (loc_begin loc gthy)))
- (fn gthy => loc_finish loc gthy o Local_Theory.reset_group);
+ (fn int => fn gthy =>
+ let val (finish, lthy) = loc_begin loc gthy
+ in (finish o Local_Theory.reset_group, f int (local_theory_group lthy)) end);
fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
fun theory_to_proof f = begin_proof
- (K (fn Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF))
- (K (Context.Theory o Sign.reset_group o Proof_Context.theory_of));
+ (fn _ => fn gthy =>
+ (Context.Theory o Sign.reset_group o Proof_Context.theory_of,
+ (case gthy of Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF)));
end;
--- a/src/Pure/type_infer_context.ML Tue Apr 03 15:15:00 2012 +0200
+++ b/src/Pure/type_infer_context.ML Tue Apr 03 20:56:32 2012 +0200
@@ -7,6 +7,7 @@
signature TYPE_INFER_CONTEXT =
sig
val const_sorts: bool Config.T
+ val const_type: Proof.context -> string -> typ option
val prepare_positions: Proof.context -> term list -> term list * (Position.T * typ) list
val prepare: Proof.context -> term list -> int * term list
val infer_types: Proof.context -> term list -> term list