Main renaming + fixes for new Isabelle in IntEx2.
--- a/Quot/Examples/AbsRepTest.thy Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy Thu Feb 11 10:06:02 2010 +0100
@@ -1,5 +1,5 @@
theory AbsRepTest
-imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List
+imports "../Quotient" "../Quotient_List" "../Quotient_Option" "../Quotient_Sum" "../Quotient_Product" List
begin
--- a/Quot/Examples/FSet.thy Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Examples/FSet.thy Thu Feb 11 10:06:02 2010 +0100
@@ -1,5 +1,5 @@
theory FSet
-imports "../QuotMain" "../QuotList" "../QuotProd" List
+imports "../Quotient" "../Quotient_List" "../Quotient_Product" List
begin
inductive
--- a/Quot/Examples/FSet2.thy Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Examples/FSet2.thy Thu Feb 11 10:06:02 2010 +0100
@@ -1,5 +1,5 @@
theory FSet2
-imports "../QuotMain" "../QuotList" List
+imports "../Quotient" "../Quotient_List" List
begin
inductive
--- a/Quot/Examples/FSet3.thy Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Examples/FSet3.thy Thu Feb 11 10:06:02 2010 +0100
@@ -1,5 +1,5 @@
theory FSet3
-imports "../QuotMain" "../QuotList" List
+imports "../Quotient" "../Quotient_List" List
begin
ML {*
--- a/Quot/Examples/IntEx.thy Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Examples/IntEx.thy Thu Feb 11 10:06:02 2010 +0100
@@ -1,5 +1,5 @@
theory IntEx
-imports "../QuotProd" "../QuotList"
+imports "../Quotient_Product" "../Quotient_List"
begin
fun
--- a/Quot/Examples/IntEx2.thy Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Examples/IntEx2.thy Thu Feb 11 10:06:02 2010 +0100
@@ -1,5 +1,5 @@
theory IntEx2
-imports "../QuotMain" "../QuotProd" Nat
+imports "../Quotient" "../Quotient_Product" Nat
(*uses
("Tools/numeral.ML")
("Tools/numeral_syntax.ML")
@@ -271,7 +271,7 @@
by (cases i, cases j, cases k) (simp)
-instance int :: pordered_cancel_ab_semigroup_add
+instance int :: ordered_cancel_ab_semigroup_add
proof
fix i j k :: int
show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
@@ -318,7 +318,7 @@
done
text{*The integers form an ordered integral domain*}
-instance int :: ordered_idom
+instance int :: linordered_idom
proof
fix i j k :: int
show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
@@ -329,11 +329,11 @@
by (simp only: zsgn_def)
qed
-instance int :: lordered_ring
+instance int :: linordered_ring
proof
- fix k :: int
+(* fix k :: int
show "abs k = sup k (- k)"
- by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
+ by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])*)
qed
lemmas int_distrib =
--- a/Quot/Examples/LFex.thy Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Examples/LFex.thy Thu Feb 11 10:06:02 2010 +0100
@@ -1,5 +1,5 @@
theory LFex
-imports Nominal "../QuotList"
+imports Nominal "../Quotient_List"
begin
atom_decl name ident
--- a/Quot/Examples/LamEx.thy Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Examples/LamEx.thy Thu Feb 11 10:06:02 2010 +0100
@@ -1,5 +1,5 @@
theory LamEx
-imports Nominal "../QuotMain" "../QuotList"
+imports Nominal "../Quotient" "../Quotient_List"
begin
atom_decl name
--- a/Quot/Examples/LarryDatatype.thy Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Examples/LarryDatatype.thy Thu Feb 11 10:06:02 2010 +0100
@@ -1,5 +1,5 @@
theory LarryDatatype
-imports Main "../QuotMain"
+imports Main "../Quotient"
begin
subsection{*Defining the Free Algebra*}
--- a/Quot/Examples/LarryInt.thy Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Examples/LarryInt.thy Thu Feb 11 10:06:02 2010 +0100
@@ -2,7 +2,7 @@
header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
theory LarryInt
-imports Nat "../QuotMain" "../QuotProd"
+imports Nat "../Quotient" "../Quotient_Product"
begin
fun
--- a/Quot/Examples/SigmaEx.thy Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy Thu Feb 11 10:06:02 2010 +0100
@@ -1,5 +1,5 @@
theory SigmaEx
-imports Nominal "../QuotMain" "../QuotList" "../QuotProd"
+imports Nominal "../Quotient" "../Quotient_List" "../Quotient_Product"
begin
atom_decl name
--- a/Quot/Examples/Terms.thy Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Examples/Terms.thy Thu Feb 11 10:06:02 2010 +0100
@@ -1,5 +1,5 @@
theory Terms
-imports Nominal "../QuotMain" "../QuotList"
+imports Nominal "../Quotient" "../Quotient_List"
begin
atom_decl name
--- a/Quot/Nominal/Abs.thy Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Nominal/Abs.thy Thu Feb 11 10:06:02 2010 +0100
@@ -1,5 +1,5 @@
theory Abs
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "../QuotProd"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product"
begin
(* the next three lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
--- a/Quot/Nominal/LFex.thy Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Nominal/LFex.thy Thu Feb 11 10:06:02 2010 +0100
@@ -1,5 +1,5 @@
theory LFex
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "Abs"
begin
atom_decl name
--- a/Quot/Nominal/LamEx.thy Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Nominal/LamEx.thy Thu Feb 11 10:06:02 2010 +0100
@@ -1,5 +1,5 @@
theory LamEx
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "Abs"
begin
atom_decl name
--- a/Quot/Nominal/LamEx2.thy Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy Thu Feb 11 10:06:02 2010 +0100
@@ -1,5 +1,5 @@
theory LamEx
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs" "../QuotProd"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "Abs" "../Quotient_Product"
begin
atom_decl name
--- a/Quot/Nominal/Terms.thy Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/Nominal/Terms.thy Thu Feb 11 10:06:02 2010 +0100
@@ -1,5 +1,5 @@
theory Terms
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "Abs"
begin
atom_decl name
--- a/Quot/QuotList.thy Thu Feb 11 09:23:59 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,232 +0,0 @@
-(* Title: QuotList.thy
- Author: Cezary Kaliszyk and Christian Urban
-*)
-theory QuotList
-imports QuotMain List
-begin
-
-section {* Quotient infrastructure for the list type. *}
-
-fun
- list_rel
-where
- "list_rel R [] [] = True"
-| "list_rel R (x#xs) [] = False"
-| "list_rel R [] (x#xs) = False"
-| "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)"
-
-declare [[map list = (map, list_rel)]]
-
-lemma split_list_all:
- shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))"
- apply(auto)
- apply(case_tac x)
- apply(simp_all)
- done
-
-lemma map_id[id_simps]:
- shows "map id = id"
- apply(simp add: expand_fun_eq)
- apply(rule allI)
- apply(induct_tac x)
- apply(simp_all)
- done
-
-
-lemma list_rel_reflp:
- shows "equivp R \<Longrightarrow> list_rel R xs xs"
- apply(induct xs)
- apply(simp_all add: equivp_reflp)
- done
-
-lemma list_rel_symp:
- assumes a: "equivp R"
- shows "list_rel R xs ys \<Longrightarrow> list_rel R ys xs"
- apply(induct xs ys rule: list_induct2')
- apply(simp_all)
- apply(rule equivp_symp[OF a])
- apply(simp)
- done
-
-lemma list_rel_transp:
- assumes a: "equivp R"
- shows "list_rel R xs1 xs2 \<Longrightarrow> list_rel R xs2 xs3 \<Longrightarrow> list_rel R xs1 xs3"
- apply(induct xs1 xs2 arbitrary: xs3 rule: list_induct2')
- apply(simp_all)
- apply(case_tac xs3)
- apply(simp_all)
- apply(rule equivp_transp[OF a])
- apply(auto)
- done
-
-lemma list_equivp[quot_equiv]:
- assumes a: "equivp R"
- shows "equivp (list_rel R)"
- apply(rule equivpI)
- unfolding reflp_def symp_def transp_def
- apply(subst split_list_all)
- apply(simp add: equivp_reflp[OF a] list_rel_reflp[OF a])
- apply(blast intro: list_rel_symp[OF a])
- apply(blast intro: list_rel_transp[OF a])
- done
-
-lemma list_rel_rel:
- assumes q: "Quotient R Abs Rep"
- shows "list_rel R r s = (list_rel R r r \<and> list_rel R s s \<and> (map Abs r = map Abs s))"
- apply(induct r s rule: list_induct2')
- apply(simp_all)
- using Quotient_rel[OF q]
- apply(metis)
- done
-
-lemma list_quotient[quot_thm]:
- assumes q: "Quotient R Abs Rep"
- shows "Quotient (list_rel R) (map Abs) (map Rep)"
- unfolding Quotient_def
- apply(subst split_list_all)
- apply(simp add: Quotient_abs_rep[OF q] abs_o_rep[OF q] map_id)
- apply(rule conjI)
- apply(rule allI)
- apply(induct_tac a)
- apply(simp)
- apply(simp)
- apply(simp add: Quotient_rep_reflp[OF q])
- apply(rule allI)+
- apply(rule list_rel_rel[OF q])
- done
-
-
-lemma cons_prs_aux:
- assumes q: "Quotient R Abs Rep"
- shows "(map Abs) ((Rep h) # (map Rep t)) = h # t"
- by (induct t) (simp_all add: Quotient_abs_rep[OF q])
-
-lemma cons_prs[quot_preserve]:
- assumes q: "Quotient R Abs Rep"
- shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
- by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q])
- (simp)
-
-lemma cons_rsp[quot_respect]:
- assumes q: "Quotient R Abs Rep"
- shows "(R ===> list_rel R ===> list_rel R) (op #) (op #)"
- by (auto)
-
-lemma nil_prs[quot_preserve]:
- assumes q: "Quotient R Abs Rep"
- shows "map Abs [] = []"
- by simp
-
-lemma nil_rsp[quot_respect]:
- assumes q: "Quotient R Abs Rep"
- shows "list_rel R [] []"
- by simp
-
-lemma map_prs_aux:
- assumes a: "Quotient R1 abs1 rep1"
- and b: "Quotient 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])
-
-
-lemma map_prs[quot_preserve]:
- assumes a: "Quotient R1 abs1 rep1"
- and b: "Quotient R2 abs2 rep2"
- shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
- by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b])
- (simp)
-
-
-lemma map_rsp[quot_respect]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
- shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map"
- apply(simp)
- apply(rule allI)+
- apply(rule impI)
- apply(rule allI)+
- apply (induct_tac xa ya rule: list_induct2')
- apply simp_all
- done
-
-lemma foldr_prs_aux:
- assumes a: "Quotient R1 abs1 rep1"
- and b: "Quotient 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])
-
-lemma foldr_prs[quot_preserve]:
- assumes a: "Quotient R1 abs1 rep1"
- and b: "Quotient R2 abs2 rep2"
- shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
- by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b])
- (simp)
-
-lemma foldl_prs_aux:
- assumes a: "Quotient R1 abs1 rep1"
- and b: "Quotient 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])
-
-
-lemma foldl_prs[quot_preserve]:
- assumes a: "Quotient R1 abs1 rep1"
- and b: "Quotient R2 abs2 rep2"
- shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
- by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b])
- (simp)
-
-lemma list_rel_empty:
- shows "list_rel R [] b \<Longrightarrow> length b = 0"
- by (induct b) (simp_all)
-
-lemma list_rel_len:
- shows "list_rel R a b \<Longrightarrow> length a = length b"
- apply (induct a arbitrary: b)
- apply (simp add: list_rel_empty)
- apply (case_tac b)
- apply simp_all
- done
-
-(* 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"
- shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl"
- apply(auto)
- apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)")
- apply simp
- apply (rule_tac x="xa" in spec)
- apply (rule_tac x="ya" in spec)
- apply (rule_tac xs="xb" and ys="yb" in list_induct2)
- apply (rule list_rel_len)
- apply (simp_all)
- done
-
-lemma foldr_rsp[quot_respect]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
- shows "((R1 ===> R2 ===> R2) ===> list_rel R1 ===> R2 ===> R2) foldr foldr"
- apply auto
- apply(subgoal_tac "R2 xb yb \<longrightarrow> list_rel R1 xa ya \<longrightarrow> R2 (foldr x xa xb) (foldr y ya yb)")
- apply simp
- apply (rule_tac xs="xa" and ys="ya" in list_induct2)
- apply (rule list_rel_len)
- apply (simp_all)
- done
-
-lemma list_rel_eq[id_simps]:
- shows "(list_rel (op =)) = (op =)"
- unfolding expand_fun_eq
- apply(rule allI)+
- apply(induct_tac x xa rule: list_induct2')
- apply(simp_all)
- done
-
-lemma list_rel_refl:
- assumes a: "\<And>x y. R x y = (R x = R y)"
- shows "list_rel R x x"
- by (induct x) (auto simp add: a)
-
-end
--- a/Quot/QuotMain.thy Thu Feb 11 09:23:59 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,802 +0,0 @@
-(* Title: QuotMain.thy
- Author: Cezary Kaliszyk and Christian Urban
-*)
-
-theory QuotMain
-imports Plain ATP_Linkup
-uses
- ("quotient_info.ML")
- ("quotient_typ.ML")
- ("quotient_def.ML")
- ("quotient_term.ML")
- ("quotient_tacs.ML")
-begin
-
-text {*
- Basic definition for equivalence relations
- that are represented by predicates.
-*}
-
-definition
- "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))"
-
-definition
- "reflp E \<longleftrightarrow> (\<forall>x. E x x)"
-
-definition
- "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)"
-
-definition
- "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
-
-lemma equivp_reflp_symp_transp:
- shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
- unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq
- by blast
-
-lemma equivp_reflp:
- shows "equivp E \<Longrightarrow> E x x"
- by (simp only: equivp_reflp_symp_transp reflp_def)
-
-lemma equivp_symp:
- shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
- by (metis equivp_reflp_symp_transp symp_def)
-
-lemma equivp_transp:
- shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
- by (metis equivp_reflp_symp_transp transp_def)
-
-lemma equivpI:
- assumes "reflp R" "symp R" "transp R"
- shows "equivp R"
- using assms by (simp add: equivp_reflp_symp_transp)
-
-lemma eq_imp_rel:
- shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
- by (simp add: equivp_reflp)
-
-lemma identity_equivp:
- shows "equivp (op =)"
- unfolding equivp_def
- by auto
-
-
-text {* Partial equivalences: not yet used anywhere *}
-definition
- "part_equivp E \<longleftrightarrow> ((\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y))))"
-
-lemma equivp_implies_part_equivp:
- assumes a: "equivp E"
- shows "part_equivp E"
- using a
- unfolding equivp_def part_equivp_def
- by auto
-
-text {* Composition of Relations *}
-
-abbreviation
- rel_conj (infixr "OOO" 75)
-where
- "r1 OOO r2 \<equiv> r1 OO r2 OO r1"
-
-lemma eq_comp_r:
- shows "((op =) OOO R) = R"
- by (auto simp add: expand_fun_eq)
-
-section {* Respects predicate *}
-
-definition
- Respects
-where
- "Respects R x \<longleftrightarrow> (R x x)"
-
-lemma in_respects:
- shows "(x \<in> Respects R) = R x x"
- unfolding mem_def Respects_def
- by simp
-
-section {* Function map and function relation *}
-
-definition
- fun_map (infixr "--->" 55)
-where
-[simp]: "fun_map f g h x = g (h (f x))"
-
-definition
- fun_rel (infixr "===>" 55)
-where
-[simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
-
-
-lemma fun_map_id:
- shows "(id ---> id) = id"
- by (simp add: expand_fun_eq id_def)
-
-lemma fun_rel_eq:
- shows "((op =) ===> (op =)) = (op =)"
- by (simp add: expand_fun_eq)
-
-lemma fun_rel_id:
- assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
- shows "(R1 ===> R2) f g"
- using a by simp
-
-lemma fun_rel_id_asm:
- assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))"
- shows "A \<longrightarrow> (R1 ===> R2) f g"
- using a by auto
-
-
-section {* Quotient Predicate *}
-
-definition
- "Quotient E Abs Rep \<longleftrightarrow>
- (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
- (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
-
-lemma Quotient_abs_rep:
- assumes a: "Quotient E Abs Rep"
- shows "Abs (Rep a) = a"
- using a
- unfolding Quotient_def
- by simp
-
-lemma Quotient_rep_reflp:
- assumes a: "Quotient E Abs Rep"
- shows "E (Rep a) (Rep a)"
- using a
- unfolding Quotient_def
- by blast
-
-lemma Quotient_rel:
- assumes a: "Quotient E Abs Rep"
- shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
- using a
- unfolding Quotient_def
- by blast
-
-lemma Quotient_rel_rep:
- assumes a: "Quotient R Abs Rep"
- shows "R (Rep a) (Rep b) = (a = b)"
- using a
- unfolding Quotient_def
- by metis
-
-lemma Quotient_rep_abs:
- assumes a: "Quotient R Abs Rep"
- shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
- using a unfolding Quotient_def
- by blast
-
-lemma Quotient_rel_abs:
- assumes a: "Quotient E Abs Rep"
- shows "E r s \<Longrightarrow> Abs r = Abs s"
- using a unfolding Quotient_def
- by blast
-
-lemma Quotient_symp:
- assumes a: "Quotient E Abs Rep"
- shows "symp E"
- using a unfolding Quotient_def symp_def
- by metis
-
-lemma Quotient_transp:
- assumes a: "Quotient E Abs Rep"
- shows "transp E"
- using a unfolding Quotient_def transp_def
- by metis
-
-lemma identity_quotient:
- shows "Quotient (op =) id id"
- unfolding Quotient_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)"
-proof -
- have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
- using q1 q2
- unfolding Quotient_def
- unfolding expand_fun_eq
- by simp
- moreover
- have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
- using q1 q2
- unfolding Quotient_def
- by (simp (no_asm)) (metis)
- moreover
- have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
- (rep1 ---> abs2) r = (rep1 ---> abs2) s)"
- unfolding expand_fun_eq
- apply(auto)
- 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
-qed
-
-lemma abs_o_rep:
- assumes a: "Quotient R Abs Rep"
- shows "Abs o Rep = id"
- unfolding expand_fun_eq
- by (simp add: Quotient_abs_rep[OF a])
-
-lemma equals_rsp:
- assumes q: "Quotient 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]
- unfolding symp_def transp_def
- by blast
-
-lemma lambda_prs:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
- shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
- unfolding expand_fun_eq
- using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
- by simp
-
-lemma lambda_prs1:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
- shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
- unfolding expand_fun_eq
- using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
- by simp
-
-lemma rep_abs_rsp:
- assumes q: "Quotient 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]
- by metis
-
-lemma rep_abs_rsp_left:
- assumes q: "Quotient 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]
- by metis
-
-text{*
- In the following theorem R1 can be instantiated with anything,
- but we know some of the types of the Rep and Abs functions;
- so by solving Quotient assumptions we can get a unique R1 that
- will be provable; which is why we need to use apply_rsp and
- not the primed version *}
-
-lemma apply_rsp:
- fixes f g::"'a \<Rightarrow> 'c"
- assumes q: "Quotient R1 Abs1 Rep1"
- and a: "(R1 ===> R2) f g" "R1 x y"
- shows "R2 (f x) (g y)"
- using a by simp
-
-lemma apply_rsp':
- assumes a: "(R1 ===> R2) f g" "R1 x y"
- shows "R2 (f x) (g y)"
- using a by simp
-
-section {* lemmas for regularisation of ball and bex *}
-
-lemma ball_reg_eqv:
- fixes P :: "'a \<Rightarrow> bool"
- assumes a: "equivp R"
- shows "Ball (Respects R) P = (All P)"
- using a
- unfolding equivp_def
- by (auto simp add: in_respects)
-
-lemma bex_reg_eqv:
- fixes P :: "'a \<Rightarrow> bool"
- assumes a: "equivp R"
- shows "Bex (Respects R) P = (Ex P)"
- using a
- unfolding equivp_def
- by (auto simp add: in_respects)
-
-lemma ball_reg_right:
- assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
- shows "All P \<longrightarrow> Ball R Q"
- using a by (metis COMBC_def Collect_def Collect_mem_eq)
-
-lemma bex_reg_left:
- assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
- shows "Bex R Q \<longrightarrow> Ex P"
- using a by (metis COMBC_def Collect_def Collect_mem_eq)
-
-lemma ball_reg_left:
- assumes a: "equivp R"
- shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
- using a by (metis equivp_reflp in_respects)
-
-lemma bex_reg_right:
- assumes a: "equivp R"
- shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
- using a by (metis equivp_reflp in_respects)
-
-lemma ball_reg_eqv_range:
- fixes P::"'a \<Rightarrow> bool"
- and x::"'a"
- assumes a: "equivp R2"
- shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
- apply(rule iffI)
- apply(rule allI)
- apply(drule_tac x="\<lambda>y. f x" in bspec)
- apply(simp add: in_respects)
- apply(rule impI)
- using a equivp_reflp_symp_transp[of "R2"]
- apply(simp add: reflp_def)
- apply(simp)
- apply(simp)
- done
-
-lemma bex_reg_eqv_range:
- assumes a: "equivp R2"
- shows "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
- apply(auto)
- apply(rule_tac x="\<lambda>y. f x" in bexI)
- apply(simp)
- apply(simp add: Respects_def in_respects)
- apply(rule impI)
- using a equivp_reflp_symp_transp[of "R2"]
- apply(simp add: reflp_def)
- done
-
-lemma all_reg:
- assumes a: "!x :: 'a. (P x --> Q x)"
- and b: "All P"
- shows "All Q"
- using a b by (metis)
-
-lemma ex_reg:
- assumes a: "!x :: 'a. (P x --> Q x)"
- and b: "Ex P"
- shows "Ex Q"
- using a b by metis
-
-lemma ball_reg:
- assumes a: "!x :: 'a. (R x --> P x --> Q x)"
- and b: "Ball R P"
- shows "Ball R Q"
- using a b by (metis COMBC_def Collect_def Collect_mem_eq)
-
-lemma bex_reg:
- assumes a: "!x :: 'a. (R x --> P x --> Q x)"
- and b: "Bex R P"
- shows "Bex R Q"
- using a b by (metis COMBC_def Collect_def Collect_mem_eq)
-
-lemma ball_all_comm:
- assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)"
- shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)"
- using assms by auto
-
-lemma bex_ex_comm:
- assumes "(\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)"
- shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)"
- using assms by auto
-
-section {* Bounded abstraction *}
-
-definition
- Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-where
- "x \<in> p \<Longrightarrow> Babs p m x = m x"
-
-lemma babs_rsp:
- assumes q: "Quotient 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)
- apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
- using a apply (simp add: Babs_def)
- apply (simp add: in_respects)
- using Quotient_rel[OF q]
- by metis
-
-lemma babs_prs:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
- shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
- apply (rule ext)
- apply (simp)
- 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])
- done
-
-lemma babs_simp:
- assumes q: "Quotient 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])
- apply(auto simp add: Babs_def)
- 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]
- by metis
-
-(* If a user proves that a particular functional relation
- is an equivalence this may be useful in regularising *)
-lemma babs_reg_eqv:
- shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
- by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)
-
-
-(* 3 lemmas needed for proving repabs_inj *)
-lemma ball_rsp:
- assumes a: "(R ===> (op =)) f g"
- shows "Ball (Respects R) f = Ball (Respects R) g"
- using a by (simp add: Ball_def in_respects)
-
-lemma bex_rsp:
- assumes a: "(R ===> (op =)) f g"
- shows "(Bex (Respects R) f = Bex (Respects R) g)"
- using a by (simp add: Bex_def in_respects)
-
-lemma bex1_rsp:
- assumes a: "(R ===> (op =)) f g"
- shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
- using a
- by (simp add: Ex1_def in_respects) auto
-
-(* 2 lemmas needed for cleaning of quantifiers *)
-lemma all_prs:
- assumes a: "Quotient R absf repf"
- shows "Ball (Respects R) ((absf ---> id) f) = All f"
- using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply
- by metis
-
-lemma ex_prs:
- assumes a: "Quotient R absf repf"
- shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
- using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
- by metis
-
-section {* Bex1_rel quantifier *}
-
-definition
- Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-where
- "Bex1_rel R P \<longleftrightarrow> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
-
-lemma bex1_rel_aux:
- "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y"
- unfolding Bex1_rel_def
- apply (erule conjE)+
- apply (erule bexE)
- apply rule
- apply (rule_tac x="xa" in bexI)
- apply metis
- apply metis
- apply rule+
- apply (erule_tac x="xaa" in ballE)
- prefer 2
- apply (metis)
- apply (erule_tac x="ya" in ballE)
- prefer 2
- apply (metis)
- apply (metis in_respects)
- done
-
-lemma bex1_rel_aux2:
- "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R y\<rbrakk> \<Longrightarrow> Bex1_rel R x"
- unfolding Bex1_rel_def
- apply (erule conjE)+
- apply (erule bexE)
- apply rule
- apply (rule_tac x="xa" in bexI)
- apply metis
- apply metis
- apply rule+
- apply (erule_tac x="xaa" in ballE)
- prefer 2
- apply (metis)
- apply (erule_tac x="ya" in ballE)
- prefer 2
- apply (metis)
- apply (metis in_respects)
- done
-
-lemma bex1_rel_rsp:
- assumes a: "Quotient R absf repf"
- shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
- apply simp
- apply clarify
- apply rule
- apply (simp_all add: bex1_rel_aux bex1_rel_aux2)
- apply (erule bex1_rel_aux2)
- apply assumption
- done
-
-
-lemma ex1_prs:
- assumes a: "Quotient R absf repf"
- shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
-apply simp
-apply (subst Bex1_rel_def)
-apply (subst Bex_def)
-apply (subst Ex1_def)
-apply simp
-apply rule
- apply (erule conjE)+
- apply (erule_tac exE)
- apply (erule conjE)
- apply (subgoal_tac "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> R x y")
- apply (rule_tac x="absf x" in exI)
- apply (simp)
- apply rule+
- using a unfolding Quotient_def
- apply metis
- apply rule+
- apply (erule_tac x="x" in ballE)
- apply (erule_tac x="y" in ballE)
- apply simp
- apply (simp add: in_respects)
- apply (simp add: in_respects)
-apply (erule_tac exE)
- apply rule
- 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 rule+
-using a unfolding Quotient_def in_respects
-apply metis
-done
-
-lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
- apply (simp add: Ex1_def Bex1_rel_def in_respects)
- apply clarify
- apply auto
- apply (rule bexI)
- apply assumption
- apply (simp add: in_respects)
- apply (simp add: in_respects)
- apply auto
- done
-
-section {* Various respects and preserve lemmas *}
-
-lemma quot_rel_rsp:
- assumes a: "Quotient R Abs Rep"
- shows "(R ===> R ===> op =) R R"
- apply(rule fun_rel_id)+
- apply(rule equals_rsp[OF a])
- apply(assumption)+
- done
-
-lemma o_prs:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
- and q3: "Quotient R3 Abs3 Rep3"
- shows "(Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g)) = f o g"
- using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
- unfolding o_def expand_fun_eq by simp
-
-lemma o_rsp:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
- and q3: "Quotient R3 Abs3 Rep3"
- and a1: "(R2 ===> R3) f1 f2"
- and a2: "(R1 ===> R2) g1 g2"
- shows "(R1 ===> R3) (f1 o g1) (f2 o g2)"
- using a1 a2 unfolding o_def expand_fun_eq
- by (auto)
-
-lemma cond_prs:
- assumes a: "Quotient 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
-
-lemma if_prs:
- assumes q: "Quotient R Abs Rep"
- shows "Abs (If a (Rep b) (Rep c)) = If a b c"
- using Quotient_abs_rep[OF q] by auto
-
-(* q not used *)
-lemma if_rsp:
- assumes q: "Quotient R Abs Rep"
- and a: "a1 = a2" "R b1 b2" "R c1 c2"
- shows "R (If a1 b1 c1) (If a2 b2 c2)"
- using a by auto
-
-lemma let_prs:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
- shows "Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f)) = Let x f"
- using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto
-
-lemma let_rsp:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and a1: "(R1 ===> R2) f g"
- and a2: "R1 x y"
- shows "R2 ((Let x f)::'c) ((Let y g)::'c)"
- using apply_rsp[OF q1 a1] a2 by auto
-
-locale quot_type =
- fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
- and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
- and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
- assumes equivp: "equivp R"
- and rep_prop: "\<And>y. \<exists>x. Rep y = R x"
- and rep_inverse: "\<And>x. Abs (Rep x) = x"
- and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
- and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
-begin
-
-definition
- abs::"'a \<Rightarrow> 'b"
-where
- "abs x \<equiv> Abs (R x)"
-
-definition
- rep::"'b \<Rightarrow> 'a"
-where
- "rep a = Eps (Rep a)"
-
-lemma homeier_lem9:
- shows "R (Eps (R x)) = R x"
-proof -
- have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
- then have "R x (Eps (R x))" by (rule someI)
- then show "R (Eps (R x)) = R x"
- using equivp unfolding equivp_def by simp
-qed
-
-theorem homeier_thm10:
- shows "abs (rep a) = a"
- unfolding abs_def rep_def
-proof -
- from rep_prop
- obtain x where eq: "Rep a = R x" by auto
- have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
- also have "\<dots> = Abs (R x)" using homeier_lem9 by simp
- also have "\<dots> = Abs (Rep a)" using eq by simp
- also have "\<dots> = a" using rep_inverse by simp
- finally
- show "Abs (R (Eps (Rep a))) = a" by simp
-qed
-
-lemma homeier_lem7:
- shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS")
-proof -
- have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject)
- also have "\<dots> = ?LHS" by (simp add: abs_inverse)
- finally show "?LHS = ?RHS" by simp
-qed
-
-theorem homeier_thm11:
- shows "R r r' = (abs r = abs r')"
- unfolding abs_def
- by (simp only: equivp[simplified equivp_def] homeier_lem7)
-
-lemma rep_refl:
- shows "R (rep a) (rep a)"
- unfolding rep_def
- by (simp add: equivp[simplified equivp_def])
-
-
-lemma rep_abs_rsp:
- shows "R f (rep (abs g)) = R f g"
- and "R (rep (abs g)) f = R g f"
- by (simp_all add: homeier_thm10 homeier_thm11)
-
-lemma Quotient:
- shows "Quotient R abs rep"
- unfolding Quotient_def
- apply(simp add: homeier_thm10)
- apply(simp add: rep_refl)
- apply(subst homeier_thm11[symmetric])
- apply(simp add: equivp[simplified equivp_def])
- done
-
-end
-
-section {* ML setup *}
-
-text {* Auxiliary data for the quotient package *}
-
-use "quotient_info.ML"
-
-declare [[map "fun" = (fun_map, fun_rel)]]
-
-lemmas [quot_thm] = fun_quotient
-lemmas [quot_respect] = quot_rel_rsp
-lemmas [quot_equiv] = identity_equivp
-
-
-text {* Lemmas about simplifying id's. *}
-lemmas [id_simps] =
- id_def[symmetric]
- fun_map_id
- id_apply
- id_o
- o_id
- eq_comp_r
-
-text {* Translation functions for the lifting process. *}
-use "quotient_term.ML"
-
-
-text {* Definitions of the quotient types. *}
-use "quotient_typ.ML"
-
-
-text {* Definitions for quotient constants. *}
-use "quotient_def.ML"
-
-
-text {*
- An auxiliary constant for recording some information
- about the lifted theorem in a tactic.
-*}
-definition
- "Quot_True x \<equiv> True"
-
-lemma
- shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
- and QT_ex: "Quot_True (Ex P) \<Longrightarrow> Quot_True P"
- and QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P"
- and QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))"
- and QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
- by (simp_all add: Quot_True_def ext)
-
-lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
- by (simp add: Quot_True_def)
-
-
-text {* Tactics for proving the lifted theorems *}
-use "quotient_tacs.ML"
-
-section {* Methods / Interface *}
-
-(* TODO inline *)
-ML {*
-fun mk_method1 tac thms ctxt =
- SIMPLE_METHOD (HEADGOAL (tac ctxt thms))
-
-fun mk_method2 tac ctxt =
- SIMPLE_METHOD (HEADGOAL (tac ctxt))
-*}
-
-method_setup lifting =
- {* Attrib.thms >> (mk_method1 Quotient_Tacs.lift_tac) *}
- {* lifts theorems to quotient types *}
-
-method_setup lifting_setup =
- {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *}
- {* sets up the three goals for the quotient lifting procedure *}
-
-method_setup regularize =
- {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *}
- {* proves the regularization goals from the quotient lifting procedure *}
-
-method_setup injection =
- {* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *}
- {* proves the rep/abs injection goals from the quotient lifting procedure *}
-
-method_setup cleaning =
- {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *}
- {* proves the cleaning goals from the quotient lifting procedure *}
-
-attribute_setup quot_lifted =
- {* Scan.succeed Quotient_Tacs.lifted_attrib *}
- {* lifts theorems to quotient types *}
-
-end
-
--- a/Quot/QuotOption.thy Thu Feb 11 09:23:59 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-(* Title: QuotOption.thy
- Author: Cezary Kaliszyk and Christian Urban
-*)
-theory QuotOption
-imports QuotMain
-begin
-
-section {* Quotient infrastructure for the option type. *}
-
-fun
- option_rel
-where
- "option_rel R None None = True"
-| "option_rel R (Some x) None = False"
-| "option_rel R None (Some x) = False"
-| "option_rel R (Some x) (Some y) = R x y"
-
-declare [[map option = (Option.map, option_rel)]]
-
-text {* should probably be in Option.thy *}
-lemma split_option_all:
- shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))"
- apply(auto)
- apply(case_tac x)
- apply(simp_all)
- done
-
-lemma option_quotient[quot_thm]:
- assumes q: "Quotient R Abs Rep"
- shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
- unfolding Quotient_def
- apply(simp add: split_option_all)
- apply(simp add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q])
- using q
- unfolding Quotient_def
- apply(blast)
- done
-
-lemma option_equivp[quot_equiv]:
- assumes a: "equivp R"
- shows "equivp (option_rel R)"
- apply(rule equivpI)
- unfolding reflp_def symp_def transp_def
- apply(simp_all add: split_option_all)
- apply(blast intro: equivp_reflp[OF a])
- apply(blast intro: equivp_symp[OF a])
- apply(blast intro: equivp_transp[OF a])
- done
-
-lemma option_None_rsp[quot_respect]:
- assumes q: "Quotient R Abs Rep"
- shows "option_rel R None None"
- by simp
-
-lemma option_Some_rsp[quot_respect]:
- assumes q: "Quotient R Abs Rep"
- shows "(R ===> option_rel R) Some Some"
- by simp
-
-lemma option_None_prs[quot_preserve]:
- assumes q: "Quotient R Abs Rep"
- shows "Option.map Abs None = None"
- by simp
-
-lemma option_Some_prs[quot_preserve]:
- assumes q: "Quotient R Abs Rep"
- shows "(Rep ---> Option.map Abs) Some = Some"
- apply(simp add: expand_fun_eq)
- apply(simp add: Quotient_abs_rep[OF q])
- done
-
-lemma option_map_id[id_simps]:
- shows "Option.map id = id"
- by (simp add: expand_fun_eq split_option_all)
-
-lemma option_rel_eq[id_simps]:
- shows "option_rel (op =) = (op =)"
- by (simp add: expand_fun_eq split_option_all)
-
-end
--- a/Quot/QuotProd.thy Thu Feb 11 09:23:59 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,104 +0,0 @@
-(* Title: QuotProd.thy
- Author: Cezary Kaliszyk and Christian Urban
-*)
-theory QuotProd
-imports QuotMain
-begin
-
-section {* Quotient infrastructure for the product type. *}
-
-fun
- prod_rel
-where
- "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
-
-declare [[map * = (prod_fun, prod_rel)]]
-
-
-lemma prod_equivp[quot_equiv]:
- assumes a: "equivp R1"
- assumes b: "equivp R2"
- shows "equivp (prod_rel R1 R2)"
- apply(rule equivpI)
- unfolding reflp_def symp_def transp_def
- apply(simp_all add: split_paired_all)
- apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
- apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
- apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
- done
-
-lemma prod_quotient[quot_thm]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
- shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)"
- unfolding Quotient_def
- apply(simp add: split_paired_all)
- apply(simp add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
- apply(simp add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
- using q1 q2
- unfolding Quotient_def
- apply(blast)
- done
-
-lemma Pair_rsp[quot_respect]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
- shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
- by simp
-
-lemma Pair_prs[quot_preserve]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
- shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair"
- apply(simp add: expand_fun_eq)
- apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
- done
-
-lemma fst_rsp[quot_respect]:
- assumes "Quotient R1 Abs1 Rep1"
- assumes "Quotient R2 Abs2 Rep2"
- shows "(prod_rel R1 R2 ===> R1) fst fst"
- by simp
-
-lemma fst_prs[quot_preserve]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
- shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst"
- apply(simp add: expand_fun_eq)
- apply(simp add: Quotient_abs_rep[OF q1])
- done
-
-lemma snd_rsp[quot_respect]:
- assumes "Quotient R1 Abs1 Rep1"
- assumes "Quotient R2 Abs2 Rep2"
- shows "(prod_rel R1 R2 ===> R2) snd snd"
- by simp
-
-lemma snd_prs[quot_preserve]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
- shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd"
- apply(simp add: expand_fun_eq)
- apply(simp add: Quotient_abs_rep[OF q2])
- done
-
-lemma split_rsp[quot_respect]:
- shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
- by auto
-
-lemma split_prs[quot_preserve]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- and q2: "Quotient R2 Abs2 Rep2"
- shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split"
- by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
-
-lemma prod_fun_id[id_simps]:
- shows "prod_fun id id = id"
- by (simp add: prod_fun_def)
-
-lemma prod_rel_eq[id_simps]:
- shows "prod_rel (op =) (op =) = (op =)"
- by (simp add: expand_fun_eq)
-
-
-end
--- a/Quot/QuotSum.thy Thu Feb 11 09:23:59 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-(* Title: QuotSum.thy
- Author: Cezary Kaliszyk and Christian Urban
-*)
-theory QuotSum
-imports QuotMain
-begin
-
-section {* Quotient infrastructure for the sum type. *}
-
-fun
- sum_rel
-where
- "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
-| "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
-| "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
-| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
-
-fun
- sum_map
-where
- "sum_map f1 f2 (Inl a) = Inl (f1 a)"
-| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
-
-declare [[map "+" = (sum_map, sum_rel)]]
-
-
-text {* should probably be in Sum_Type.thy *}
-lemma split_sum_all:
- shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
- apply(auto)
- apply(case_tac x)
- apply(simp_all)
- done
-
-lemma sum_equivp[quot_equiv]:
- assumes a: "equivp R1"
- assumes b: "equivp R2"
- shows "equivp (sum_rel R1 R2)"
- apply(rule equivpI)
- unfolding reflp_def symp_def transp_def
- apply(simp_all add: split_sum_all)
- apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
- apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
- apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
- done
-
-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)"
- unfolding Quotient_def
- apply(simp add: split_sum_all)
- apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
- apply(simp_all add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
- using q1 q2
- unfolding Quotient_def
- apply(blast)+
- done
-
-lemma sum_Inl_rsp[quot_respect]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
- shows "(R1 ===> sum_rel R1 R2) Inl Inl"
- by simp
-
-lemma sum_Inr_rsp[quot_respect]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
- shows "(R2 ===> sum_rel R1 R2) Inr Inr"
- by simp
-
-lemma sum_Inl_prs[quot_preserve]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
- shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
- apply(simp add: expand_fun_eq)
- apply(simp add: Quotient_abs_rep[OF q1])
- done
-
-lemma sum_Inr_prs[quot_preserve]:
- assumes q1: "Quotient R1 Abs1 Rep1"
- assumes q2: "Quotient R2 Abs2 Rep2"
- shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
- apply(simp add: expand_fun_eq)
- apply(simp add: Quotient_abs_rep[OF q2])
- done
-
-lemma sum_map_id[id_simps]:
- shows "sum_map id id = id"
- by (simp add: expand_fun_eq split_sum_all)
-
-lemma sum_rel_eq[id_simps]:
- shows "sum_rel (op =) (op =) = (op =)"
- by (simp add: expand_fun_eq split_sum_all)
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Quotient.thy Thu Feb 11 10:06:02 2010 +0100
@@ -0,0 +1,802 @@
+(* Title: QuotMain.thy
+ Author: Cezary Kaliszyk and Christian Urban
+*)
+
+theory Quotient
+imports Plain ATP_Linkup
+uses
+ ("quotient_info.ML")
+ ("quotient_typ.ML")
+ ("quotient_def.ML")
+ ("quotient_term.ML")
+ ("quotient_tacs.ML")
+begin
+
+text {*
+ Basic definition for equivalence relations
+ that are represented by predicates.
+*}
+
+definition
+ "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))"
+
+definition
+ "reflp E \<longleftrightarrow> (\<forall>x. E x x)"
+
+definition
+ "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)"
+
+definition
+ "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
+
+lemma equivp_reflp_symp_transp:
+ shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
+ unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq
+ by blast
+
+lemma equivp_reflp:
+ shows "equivp E \<Longrightarrow> E x x"
+ by (simp only: equivp_reflp_symp_transp reflp_def)
+
+lemma equivp_symp:
+ shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
+ by (metis equivp_reflp_symp_transp symp_def)
+
+lemma equivp_transp:
+ shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
+ by (metis equivp_reflp_symp_transp transp_def)
+
+lemma equivpI:
+ assumes "reflp R" "symp R" "transp R"
+ shows "equivp R"
+ using assms by (simp add: equivp_reflp_symp_transp)
+
+lemma eq_imp_rel:
+ shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
+ by (simp add: equivp_reflp)
+
+lemma identity_equivp:
+ shows "equivp (op =)"
+ unfolding equivp_def
+ by auto
+
+
+text {* Partial equivalences: not yet used anywhere *}
+definition
+ "part_equivp E \<longleftrightarrow> ((\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y))))"
+
+lemma equivp_implies_part_equivp:
+ assumes a: "equivp E"
+ shows "part_equivp E"
+ using a
+ unfolding equivp_def part_equivp_def
+ by auto
+
+text {* Composition of Relations *}
+
+abbreviation
+ rel_conj (infixr "OOO" 75)
+where
+ "r1 OOO r2 \<equiv> r1 OO r2 OO r1"
+
+lemma eq_comp_r:
+ shows "((op =) OOO R) = R"
+ by (auto simp add: expand_fun_eq)
+
+section {* Respects predicate *}
+
+definition
+ Respects
+where
+ "Respects R x \<longleftrightarrow> (R x x)"
+
+lemma in_respects:
+ shows "(x \<in> Respects R) = R x x"
+ unfolding mem_def Respects_def
+ by simp
+
+section {* Function map and function relation *}
+
+definition
+ fun_map (infixr "--->" 55)
+where
+[simp]: "fun_map f g h x = g (h (f x))"
+
+definition
+ fun_rel (infixr "===>" 55)
+where
+[simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
+
+
+lemma fun_map_id:
+ shows "(id ---> id) = id"
+ by (simp add: expand_fun_eq id_def)
+
+lemma fun_rel_eq:
+ shows "((op =) ===> (op =)) = (op =)"
+ by (simp add: expand_fun_eq)
+
+lemma fun_rel_id:
+ assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
+ shows "(R1 ===> R2) f g"
+ using a by simp
+
+lemma fun_rel_id_asm:
+ assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))"
+ shows "A \<longrightarrow> (R1 ===> R2) f g"
+ using a by auto
+
+
+section {* Quotient Predicate *}
+
+definition
+ "Quotient E Abs Rep \<longleftrightarrow>
+ (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
+ (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
+
+lemma Quotient_abs_rep:
+ assumes a: "Quotient E Abs Rep"
+ shows "Abs (Rep a) = a"
+ using a
+ unfolding Quotient_def
+ by simp
+
+lemma Quotient_rep_reflp:
+ assumes a: "Quotient E Abs Rep"
+ shows "E (Rep a) (Rep a)"
+ using a
+ unfolding Quotient_def
+ by blast
+
+lemma Quotient_rel:
+ assumes a: "Quotient E Abs Rep"
+ shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
+ using a
+ unfolding Quotient_def
+ by blast
+
+lemma Quotient_rel_rep:
+ assumes a: "Quotient R Abs Rep"
+ shows "R (Rep a) (Rep b) = (a = b)"
+ using a
+ unfolding Quotient_def
+ by metis
+
+lemma Quotient_rep_abs:
+ assumes a: "Quotient R Abs Rep"
+ shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
+ using a unfolding Quotient_def
+ by blast
+
+lemma Quotient_rel_abs:
+ assumes a: "Quotient E Abs Rep"
+ shows "E r s \<Longrightarrow> Abs r = Abs s"
+ using a unfolding Quotient_def
+ by blast
+
+lemma Quotient_symp:
+ assumes a: "Quotient E Abs Rep"
+ shows "symp E"
+ using a unfolding Quotient_def symp_def
+ by metis
+
+lemma Quotient_transp:
+ assumes a: "Quotient E Abs Rep"
+ shows "transp E"
+ using a unfolding Quotient_def transp_def
+ by metis
+
+lemma identity_quotient:
+ shows "Quotient (op =) id id"
+ unfolding Quotient_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)"
+proof -
+ have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
+ using q1 q2
+ unfolding Quotient_def
+ unfolding expand_fun_eq
+ by simp
+ moreover
+ have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
+ using q1 q2
+ unfolding Quotient_def
+ by (simp (no_asm)) (metis)
+ moreover
+ have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
+ (rep1 ---> abs2) r = (rep1 ---> abs2) s)"
+ unfolding expand_fun_eq
+ apply(auto)
+ 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
+qed
+
+lemma abs_o_rep:
+ assumes a: "Quotient R Abs Rep"
+ shows "Abs o Rep = id"
+ unfolding expand_fun_eq
+ by (simp add: Quotient_abs_rep[OF a])
+
+lemma equals_rsp:
+ assumes q: "Quotient 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]
+ unfolding symp_def transp_def
+ by blast
+
+lemma lambda_prs:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ and q2: "Quotient R2 Abs2 Rep2"
+ shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
+ unfolding expand_fun_eq
+ using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
+ by simp
+
+lemma lambda_prs1:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ and q2: "Quotient R2 Abs2 Rep2"
+ shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
+ unfolding expand_fun_eq
+ using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
+ by simp
+
+lemma rep_abs_rsp:
+ assumes q: "Quotient 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]
+ by metis
+
+lemma rep_abs_rsp_left:
+ assumes q: "Quotient 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]
+ by metis
+
+text{*
+ In the following theorem R1 can be instantiated with anything,
+ but we know some of the types of the Rep and Abs functions;
+ so by solving Quotient assumptions we can get a unique R1 that
+ will be provable; which is why we need to use apply_rsp and
+ not the primed version *}
+
+lemma apply_rsp:
+ fixes f g::"'a \<Rightarrow> 'c"
+ assumes q: "Quotient R1 Abs1 Rep1"
+ and a: "(R1 ===> R2) f g" "R1 x y"
+ shows "R2 (f x) (g y)"
+ using a by simp
+
+lemma apply_rsp':
+ assumes a: "(R1 ===> R2) f g" "R1 x y"
+ shows "R2 (f x) (g y)"
+ using a by simp
+
+section {* lemmas for regularisation of ball and bex *}
+
+lemma ball_reg_eqv:
+ fixes P :: "'a \<Rightarrow> bool"
+ assumes a: "equivp R"
+ shows "Ball (Respects R) P = (All P)"
+ using a
+ unfolding equivp_def
+ by (auto simp add: in_respects)
+
+lemma bex_reg_eqv:
+ fixes P :: "'a \<Rightarrow> bool"
+ assumes a: "equivp R"
+ shows "Bex (Respects R) P = (Ex P)"
+ using a
+ unfolding equivp_def
+ by (auto simp add: in_respects)
+
+lemma ball_reg_right:
+ assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
+ shows "All P \<longrightarrow> Ball R Q"
+ using a by (metis COMBC_def Collect_def Collect_mem_eq)
+
+lemma bex_reg_left:
+ assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
+ shows "Bex R Q \<longrightarrow> Ex P"
+ using a by (metis COMBC_def Collect_def Collect_mem_eq)
+
+lemma ball_reg_left:
+ assumes a: "equivp R"
+ shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
+ using a by (metis equivp_reflp in_respects)
+
+lemma bex_reg_right:
+ assumes a: "equivp R"
+ shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
+ using a by (metis equivp_reflp in_respects)
+
+lemma ball_reg_eqv_range:
+ fixes P::"'a \<Rightarrow> bool"
+ and x::"'a"
+ assumes a: "equivp R2"
+ shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
+ apply(rule iffI)
+ apply(rule allI)
+ apply(drule_tac x="\<lambda>y. f x" in bspec)
+ apply(simp add: in_respects)
+ apply(rule impI)
+ using a equivp_reflp_symp_transp[of "R2"]
+ apply(simp add: reflp_def)
+ apply(simp)
+ apply(simp)
+ done
+
+lemma bex_reg_eqv_range:
+ assumes a: "equivp R2"
+ shows "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
+ apply(auto)
+ apply(rule_tac x="\<lambda>y. f x" in bexI)
+ apply(simp)
+ apply(simp add: Respects_def in_respects)
+ apply(rule impI)
+ using a equivp_reflp_symp_transp[of "R2"]
+ apply(simp add: reflp_def)
+ done
+
+lemma all_reg:
+ assumes a: "!x :: 'a. (P x --> Q x)"
+ and b: "All P"
+ shows "All Q"
+ using a b by (metis)
+
+lemma ex_reg:
+ assumes a: "!x :: 'a. (P x --> Q x)"
+ and b: "Ex P"
+ shows "Ex Q"
+ using a b by metis
+
+lemma ball_reg:
+ assumes a: "!x :: 'a. (R x --> P x --> Q x)"
+ and b: "Ball R P"
+ shows "Ball R Q"
+ using a b by (metis COMBC_def Collect_def Collect_mem_eq)
+
+lemma bex_reg:
+ assumes a: "!x :: 'a. (R x --> P x --> Q x)"
+ and b: "Bex R P"
+ shows "Bex R Q"
+ using a b by (metis COMBC_def Collect_def Collect_mem_eq)
+
+lemma ball_all_comm:
+ assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)"
+ shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)"
+ using assms by auto
+
+lemma bex_ex_comm:
+ assumes "(\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)"
+ shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)"
+ using assms by auto
+
+section {* Bounded abstraction *}
+
+definition
+ Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+where
+ "x \<in> p \<Longrightarrow> Babs p m x = m x"
+
+lemma babs_rsp:
+ assumes q: "Quotient 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)
+ apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
+ using a apply (simp add: Babs_def)
+ apply (simp add: in_respects)
+ using Quotient_rel[OF q]
+ by metis
+
+lemma babs_prs:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ and q2: "Quotient R2 Abs2 Rep2"
+ shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
+ apply (rule ext)
+ apply (simp)
+ 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])
+ done
+
+lemma babs_simp:
+ assumes q: "Quotient 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])
+ apply(auto simp add: Babs_def)
+ 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]
+ by metis
+
+(* If a user proves that a particular functional relation
+ is an equivalence this may be useful in regularising *)
+lemma babs_reg_eqv:
+ shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
+ by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)
+
+
+(* 3 lemmas needed for proving repabs_inj *)
+lemma ball_rsp:
+ assumes a: "(R ===> (op =)) f g"
+ shows "Ball (Respects R) f = Ball (Respects R) g"
+ using a by (simp add: Ball_def in_respects)
+
+lemma bex_rsp:
+ assumes a: "(R ===> (op =)) f g"
+ shows "(Bex (Respects R) f = Bex (Respects R) g)"
+ using a by (simp add: Bex_def in_respects)
+
+lemma bex1_rsp:
+ assumes a: "(R ===> (op =)) f g"
+ shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
+ using a
+ by (simp add: Ex1_def in_respects) auto
+
+(* 2 lemmas needed for cleaning of quantifiers *)
+lemma all_prs:
+ assumes a: "Quotient R absf repf"
+ shows "Ball (Respects R) ((absf ---> id) f) = All f"
+ using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply
+ by metis
+
+lemma ex_prs:
+ assumes a: "Quotient R absf repf"
+ shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
+ using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
+ by metis
+
+section {* Bex1_rel quantifier *}
+
+definition
+ Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+where
+ "Bex1_rel R P \<longleftrightarrow> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
+
+lemma bex1_rel_aux:
+ "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y"
+ unfolding Bex1_rel_def
+ apply (erule conjE)+
+ apply (erule bexE)
+ apply rule
+ apply (rule_tac x="xa" in bexI)
+ apply metis
+ apply metis
+ apply rule+
+ apply (erule_tac x="xaa" in ballE)
+ prefer 2
+ apply (metis)
+ apply (erule_tac x="ya" in ballE)
+ prefer 2
+ apply (metis)
+ apply (metis in_respects)
+ done
+
+lemma bex1_rel_aux2:
+ "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R y\<rbrakk> \<Longrightarrow> Bex1_rel R x"
+ unfolding Bex1_rel_def
+ apply (erule conjE)+
+ apply (erule bexE)
+ apply rule
+ apply (rule_tac x="xa" in bexI)
+ apply metis
+ apply metis
+ apply rule+
+ apply (erule_tac x="xaa" in ballE)
+ prefer 2
+ apply (metis)
+ apply (erule_tac x="ya" in ballE)
+ prefer 2
+ apply (metis)
+ apply (metis in_respects)
+ done
+
+lemma bex1_rel_rsp:
+ assumes a: "Quotient R absf repf"
+ shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
+ apply simp
+ apply clarify
+ apply rule
+ apply (simp_all add: bex1_rel_aux bex1_rel_aux2)
+ apply (erule bex1_rel_aux2)
+ apply assumption
+ done
+
+
+lemma ex1_prs:
+ assumes a: "Quotient R absf repf"
+ shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
+apply simp
+apply (subst Bex1_rel_def)
+apply (subst Bex_def)
+apply (subst Ex1_def)
+apply simp
+apply rule
+ apply (erule conjE)+
+ apply (erule_tac exE)
+ apply (erule conjE)
+ apply (subgoal_tac "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> R x y")
+ apply (rule_tac x="absf x" in exI)
+ apply (simp)
+ apply rule+
+ using a unfolding Quotient_def
+ apply metis
+ apply rule+
+ apply (erule_tac x="x" in ballE)
+ apply (erule_tac x="y" in ballE)
+ apply simp
+ apply (simp add: in_respects)
+ apply (simp add: in_respects)
+apply (erule_tac exE)
+ apply rule
+ 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 rule+
+using a unfolding Quotient_def in_respects
+apply metis
+done
+
+lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
+ apply (simp add: Ex1_def Bex1_rel_def in_respects)
+ apply clarify
+ apply auto
+ apply (rule bexI)
+ apply assumption
+ apply (simp add: in_respects)
+ apply (simp add: in_respects)
+ apply auto
+ done
+
+section {* Various respects and preserve lemmas *}
+
+lemma quot_rel_rsp:
+ assumes a: "Quotient R Abs Rep"
+ shows "(R ===> R ===> op =) R R"
+ apply(rule fun_rel_id)+
+ apply(rule equals_rsp[OF a])
+ apply(assumption)+
+ done
+
+lemma o_prs:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ and q2: "Quotient R2 Abs2 Rep2"
+ and q3: "Quotient R3 Abs3 Rep3"
+ shows "(Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g)) = f o g"
+ using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
+ unfolding o_def expand_fun_eq by simp
+
+lemma o_rsp:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ and q2: "Quotient R2 Abs2 Rep2"
+ and q3: "Quotient R3 Abs3 Rep3"
+ and a1: "(R2 ===> R3) f1 f2"
+ and a2: "(R1 ===> R2) g1 g2"
+ shows "(R1 ===> R3) (f1 o g1) (f2 o g2)"
+ using a1 a2 unfolding o_def expand_fun_eq
+ by (auto)
+
+lemma cond_prs:
+ assumes a: "Quotient 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
+
+lemma if_prs:
+ assumes q: "Quotient R Abs Rep"
+ shows "Abs (If a (Rep b) (Rep c)) = If a b c"
+ using Quotient_abs_rep[OF q] by auto
+
+(* q not used *)
+lemma if_rsp:
+ assumes q: "Quotient R Abs Rep"
+ and a: "a1 = a2" "R b1 b2" "R c1 c2"
+ shows "R (If a1 b1 c1) (If a2 b2 c2)"
+ using a by auto
+
+lemma let_prs:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ and q2: "Quotient R2 Abs2 Rep2"
+ shows "Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f)) = Let x f"
+ using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto
+
+lemma let_rsp:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ and a1: "(R1 ===> R2) f g"
+ and a2: "R1 x y"
+ shows "R2 ((Let x f)::'c) ((Let y g)::'c)"
+ using apply_rsp[OF q1 a1] a2 by auto
+
+locale quot_type =
+ fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
+ and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
+ assumes equivp: "equivp R"
+ and rep_prop: "\<And>y. \<exists>x. Rep y = R x"
+ and rep_inverse: "\<And>x. Abs (Rep x) = x"
+ and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
+ and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
+begin
+
+definition
+ abs::"'a \<Rightarrow> 'b"
+where
+ "abs x \<equiv> Abs (R x)"
+
+definition
+ rep::"'b \<Rightarrow> 'a"
+where
+ "rep a = Eps (Rep a)"
+
+lemma homeier_lem9:
+ shows "R (Eps (R x)) = R x"
+proof -
+ have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
+ then have "R x (Eps (R x))" by (rule someI)
+ then show "R (Eps (R x)) = R x"
+ using equivp unfolding equivp_def by simp
+qed
+
+theorem homeier_thm10:
+ shows "abs (rep a) = a"
+ unfolding abs_def rep_def
+proof -
+ from rep_prop
+ obtain x where eq: "Rep a = R x" by auto
+ have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
+ also have "\<dots> = Abs (R x)" using homeier_lem9 by simp
+ also have "\<dots> = Abs (Rep a)" using eq by simp
+ also have "\<dots> = a" using rep_inverse by simp
+ finally
+ show "Abs (R (Eps (Rep a))) = a" by simp
+qed
+
+lemma homeier_lem7:
+ shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS")
+proof -
+ have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject)
+ also have "\<dots> = ?LHS" by (simp add: abs_inverse)
+ finally show "?LHS = ?RHS" by simp
+qed
+
+theorem homeier_thm11:
+ shows "R r r' = (abs r = abs r')"
+ unfolding abs_def
+ by (simp only: equivp[simplified equivp_def] homeier_lem7)
+
+lemma rep_refl:
+ shows "R (rep a) (rep a)"
+ unfolding rep_def
+ by (simp add: equivp[simplified equivp_def])
+
+
+lemma rep_abs_rsp:
+ shows "R f (rep (abs g)) = R f g"
+ and "R (rep (abs g)) f = R g f"
+ by (simp_all add: homeier_thm10 homeier_thm11)
+
+lemma Quotient:
+ shows "Quotient R abs rep"
+ unfolding Quotient_def
+ apply(simp add: homeier_thm10)
+ apply(simp add: rep_refl)
+ apply(subst homeier_thm11[symmetric])
+ apply(simp add: equivp[simplified equivp_def])
+ done
+
+end
+
+section {* ML setup *}
+
+text {* Auxiliary data for the quotient package *}
+
+use "quotient_info.ML"
+
+declare [[map "fun" = (fun_map, fun_rel)]]
+
+lemmas [quot_thm] = fun_quotient
+lemmas [quot_respect] = quot_rel_rsp
+lemmas [quot_equiv] = identity_equivp
+
+
+text {* Lemmas about simplifying id's. *}
+lemmas [id_simps] =
+ id_def[symmetric]
+ fun_map_id
+ id_apply
+ id_o
+ o_id
+ eq_comp_r
+
+text {* Translation functions for the lifting process. *}
+use "quotient_term.ML"
+
+
+text {* Definitions of the quotient types. *}
+use "quotient_typ.ML"
+
+
+text {* Definitions for quotient constants. *}
+use "quotient_def.ML"
+
+
+text {*
+ An auxiliary constant for recording some information
+ about the lifted theorem in a tactic.
+*}
+definition
+ "Quot_True x \<equiv> True"
+
+lemma
+ shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
+ and QT_ex: "Quot_True (Ex P) \<Longrightarrow> Quot_True P"
+ and QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P"
+ and QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))"
+ and QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
+ by (simp_all add: Quot_True_def ext)
+
+lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
+ by (simp add: Quot_True_def)
+
+
+text {* Tactics for proving the lifted theorems *}
+use "quotient_tacs.ML"
+
+section {* Methods / Interface *}
+
+(* TODO inline *)
+ML {*
+fun mk_method1 tac thms ctxt =
+ SIMPLE_METHOD (HEADGOAL (tac ctxt thms))
+
+fun mk_method2 tac ctxt =
+ SIMPLE_METHOD (HEADGOAL (tac ctxt))
+*}
+
+method_setup lifting =
+ {* Attrib.thms >> (mk_method1 Quotient_Tacs.lift_tac) *}
+ {* lifts theorems to quotient types *}
+
+method_setup lifting_setup =
+ {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *}
+ {* sets up the three goals for the quotient lifting procedure *}
+
+method_setup regularize =
+ {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *}
+ {* proves the regularization goals from the quotient lifting procedure *}
+
+method_setup injection =
+ {* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *}
+ {* proves the rep/abs injection goals from the quotient lifting procedure *}
+
+method_setup cleaning =
+ {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *}
+ {* proves the cleaning goals from the quotient lifting procedure *}
+
+attribute_setup quot_lifted =
+ {* Scan.succeed Quotient_Tacs.lifted_attrib *}
+ {* lifts theorems to quotient types *}
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Quotient_List.thy Thu Feb 11 10:06:02 2010 +0100
@@ -0,0 +1,232 @@
+(* Title: Quotient_List.thy
+ Author: Cezary Kaliszyk and Christian Urban
+*)
+theory Quotient_List
+imports Quotient List
+begin
+
+section {* Quotient infrastructure for the list type. *}
+
+fun
+ list_rel
+where
+ "list_rel R [] [] = True"
+| "list_rel R (x#xs) [] = False"
+| "list_rel R [] (x#xs) = False"
+| "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)"
+
+declare [[map list = (map, list_rel)]]
+
+lemma split_list_all:
+ shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))"
+ apply(auto)
+ apply(case_tac x)
+ apply(simp_all)
+ done
+
+lemma map_id[id_simps]:
+ shows "map id = id"
+ apply(simp add: expand_fun_eq)
+ apply(rule allI)
+ apply(induct_tac x)
+ apply(simp_all)
+ done
+
+
+lemma list_rel_reflp:
+ shows "equivp R \<Longrightarrow> list_rel R xs xs"
+ apply(induct xs)
+ apply(simp_all add: equivp_reflp)
+ done
+
+lemma list_rel_symp:
+ assumes a: "equivp R"
+ shows "list_rel R xs ys \<Longrightarrow> list_rel R ys xs"
+ apply(induct xs ys rule: list_induct2')
+ apply(simp_all)
+ apply(rule equivp_symp[OF a])
+ apply(simp)
+ done
+
+lemma list_rel_transp:
+ assumes a: "equivp R"
+ shows "list_rel R xs1 xs2 \<Longrightarrow> list_rel R xs2 xs3 \<Longrightarrow> list_rel R xs1 xs3"
+ apply(induct xs1 xs2 arbitrary: xs3 rule: list_induct2')
+ apply(simp_all)
+ apply(case_tac xs3)
+ apply(simp_all)
+ apply(rule equivp_transp[OF a])
+ apply(auto)
+ done
+
+lemma list_equivp[quot_equiv]:
+ assumes a: "equivp R"
+ shows "equivp (list_rel R)"
+ apply(rule equivpI)
+ unfolding reflp_def symp_def transp_def
+ apply(subst split_list_all)
+ apply(simp add: equivp_reflp[OF a] list_rel_reflp[OF a])
+ apply(blast intro: list_rel_symp[OF a])
+ apply(blast intro: list_rel_transp[OF a])
+ done
+
+lemma list_rel_rel:
+ assumes q: "Quotient R Abs Rep"
+ shows "list_rel R r s = (list_rel R r r \<and> list_rel R s s \<and> (map Abs r = map Abs s))"
+ apply(induct r s rule: list_induct2')
+ apply(simp_all)
+ using Quotient_rel[OF q]
+ apply(metis)
+ done
+
+lemma list_quotient[quot_thm]:
+ assumes q: "Quotient R Abs Rep"
+ shows "Quotient (list_rel R) (map Abs) (map Rep)"
+ unfolding Quotient_def
+ apply(subst split_list_all)
+ apply(simp add: Quotient_abs_rep[OF q] abs_o_rep[OF q] map_id)
+ apply(rule conjI)
+ apply(rule allI)
+ apply(induct_tac a)
+ apply(simp)
+ apply(simp)
+ apply(simp add: Quotient_rep_reflp[OF q])
+ apply(rule allI)+
+ apply(rule list_rel_rel[OF q])
+ done
+
+
+lemma cons_prs_aux:
+ assumes q: "Quotient R Abs Rep"
+ shows "(map Abs) ((Rep h) # (map Rep t)) = h # t"
+ by (induct t) (simp_all add: Quotient_abs_rep[OF q])
+
+lemma cons_prs[quot_preserve]:
+ assumes q: "Quotient R Abs Rep"
+ shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
+ by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q])
+ (simp)
+
+lemma cons_rsp[quot_respect]:
+ assumes q: "Quotient R Abs Rep"
+ shows "(R ===> list_rel R ===> list_rel R) (op #) (op #)"
+ by (auto)
+
+lemma nil_prs[quot_preserve]:
+ assumes q: "Quotient R Abs Rep"
+ shows "map Abs [] = []"
+ by simp
+
+lemma nil_rsp[quot_respect]:
+ assumes q: "Quotient R Abs Rep"
+ shows "list_rel R [] []"
+ by simp
+
+lemma map_prs_aux:
+ assumes a: "Quotient R1 abs1 rep1"
+ and b: "Quotient 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])
+
+
+lemma map_prs[quot_preserve]:
+ assumes a: "Quotient R1 abs1 rep1"
+ and b: "Quotient R2 abs2 rep2"
+ shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
+ by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b])
+ (simp)
+
+
+lemma map_rsp[quot_respect]:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ and q2: "Quotient R2 Abs2 Rep2"
+ shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map"
+ apply(simp)
+ apply(rule allI)+
+ apply(rule impI)
+ apply(rule allI)+
+ apply (induct_tac xa ya rule: list_induct2')
+ apply simp_all
+ done
+
+lemma foldr_prs_aux:
+ assumes a: "Quotient R1 abs1 rep1"
+ and b: "Quotient 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])
+
+lemma foldr_prs[quot_preserve]:
+ assumes a: "Quotient R1 abs1 rep1"
+ and b: "Quotient R2 abs2 rep2"
+ shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
+ by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b])
+ (simp)
+
+lemma foldl_prs_aux:
+ assumes a: "Quotient R1 abs1 rep1"
+ and b: "Quotient 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])
+
+
+lemma foldl_prs[quot_preserve]:
+ assumes a: "Quotient R1 abs1 rep1"
+ and b: "Quotient R2 abs2 rep2"
+ shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
+ by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b])
+ (simp)
+
+lemma list_rel_empty:
+ shows "list_rel R [] b \<Longrightarrow> length b = 0"
+ by (induct b) (simp_all)
+
+lemma list_rel_len:
+ shows "list_rel R a b \<Longrightarrow> length a = length b"
+ apply (induct a arbitrary: b)
+ apply (simp add: list_rel_empty)
+ apply (case_tac b)
+ apply simp_all
+ done
+
+(* 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"
+ shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl"
+ apply(auto)
+ apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)")
+ apply simp
+ apply (rule_tac x="xa" in spec)
+ apply (rule_tac x="ya" in spec)
+ apply (rule_tac xs="xb" and ys="yb" in list_induct2)
+ apply (rule list_rel_len)
+ apply (simp_all)
+ done
+
+lemma foldr_rsp[quot_respect]:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ and q2: "Quotient R2 Abs2 Rep2"
+ shows "((R1 ===> R2 ===> R2) ===> list_rel R1 ===> R2 ===> R2) foldr foldr"
+ apply auto
+ apply(subgoal_tac "R2 xb yb \<longrightarrow> list_rel R1 xa ya \<longrightarrow> R2 (foldr x xa xb) (foldr y ya yb)")
+ apply simp
+ apply (rule_tac xs="xa" and ys="ya" in list_induct2)
+ apply (rule list_rel_len)
+ apply (simp_all)
+ done
+
+lemma list_rel_eq[id_simps]:
+ shows "(list_rel (op =)) = (op =)"
+ unfolding expand_fun_eq
+ apply(rule allI)+
+ apply(induct_tac x xa rule: list_induct2')
+ apply(simp_all)
+ done
+
+lemma list_rel_refl:
+ assumes a: "\<And>x y. R x y = (R x = R y)"
+ shows "list_rel R x x"
+ by (induct x) (auto simp add: a)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Quotient_Option.thy Thu Feb 11 10:06:02 2010 +0100
@@ -0,0 +1,80 @@
+(* Title: Quotient_Option.thy
+ Author: Cezary Kaliszyk and Christian Urban
+*)
+theory Quotient_Option
+imports Quotient
+begin
+
+section {* Quotient infrastructure for the option type. *}
+
+fun
+ option_rel
+where
+ "option_rel R None None = True"
+| "option_rel R (Some x) None = False"
+| "option_rel R None (Some x) = False"
+| "option_rel R (Some x) (Some y) = R x y"
+
+declare [[map option = (Option.map, option_rel)]]
+
+text {* should probably be in Option.thy *}
+lemma split_option_all:
+ shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))"
+ apply(auto)
+ apply(case_tac x)
+ apply(simp_all)
+ done
+
+lemma option_quotient[quot_thm]:
+ assumes q: "Quotient R Abs Rep"
+ shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
+ unfolding Quotient_def
+ apply(simp add: split_option_all)
+ apply(simp add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q])
+ using q
+ unfolding Quotient_def
+ apply(blast)
+ done
+
+lemma option_equivp[quot_equiv]:
+ assumes a: "equivp R"
+ shows "equivp (option_rel R)"
+ apply(rule equivpI)
+ unfolding reflp_def symp_def transp_def
+ apply(simp_all add: split_option_all)
+ apply(blast intro: equivp_reflp[OF a])
+ apply(blast intro: equivp_symp[OF a])
+ apply(blast intro: equivp_transp[OF a])
+ done
+
+lemma option_None_rsp[quot_respect]:
+ assumes q: "Quotient R Abs Rep"
+ shows "option_rel R None None"
+ by simp
+
+lemma option_Some_rsp[quot_respect]:
+ assumes q: "Quotient R Abs Rep"
+ shows "(R ===> option_rel R) Some Some"
+ by simp
+
+lemma option_None_prs[quot_preserve]:
+ assumes q: "Quotient R Abs Rep"
+ shows "Option.map Abs None = None"
+ by simp
+
+lemma option_Some_prs[quot_preserve]:
+ assumes q: "Quotient R Abs Rep"
+ shows "(Rep ---> Option.map Abs) Some = Some"
+ apply(simp add: expand_fun_eq)
+ apply(simp add: Quotient_abs_rep[OF q])
+ done
+
+lemma option_map_id[id_simps]:
+ shows "Option.map id = id"
+ by (simp add: expand_fun_eq split_option_all)
+
+lemma option_rel_eq[id_simps]:
+ shows "option_rel (op =) = (op =)"
+ by (simp add: expand_fun_eq split_option_all)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Quotient_Product.thy Thu Feb 11 10:06:02 2010 +0100
@@ -0,0 +1,104 @@
+(* Title: Quotient_Product.thy
+ Author: Cezary Kaliszyk and Christian Urban
+*)
+theory Quotient_Product
+imports Quotient
+begin
+
+section {* Quotient infrastructure for the product type. *}
+
+fun
+ prod_rel
+where
+ "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
+
+declare [[map * = (prod_fun, prod_rel)]]
+
+
+lemma prod_equivp[quot_equiv]:
+ assumes a: "equivp R1"
+ assumes b: "equivp R2"
+ shows "equivp (prod_rel R1 R2)"
+ apply(rule equivpI)
+ unfolding reflp_def symp_def transp_def
+ apply(simp_all add: split_paired_all)
+ apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
+ apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
+ apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
+ done
+
+lemma prod_quotient[quot_thm]:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ assumes q2: "Quotient R2 Abs2 Rep2"
+ shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)"
+ unfolding Quotient_def
+ apply(simp add: split_paired_all)
+ apply(simp add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
+ apply(simp add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
+ using q1 q2
+ unfolding Quotient_def
+ apply(blast)
+ done
+
+lemma Pair_rsp[quot_respect]:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ assumes q2: "Quotient R2 Abs2 Rep2"
+ shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
+ by simp
+
+lemma Pair_prs[quot_preserve]:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ assumes q2: "Quotient R2 Abs2 Rep2"
+ shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair"
+ apply(simp add: expand_fun_eq)
+ apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+ done
+
+lemma fst_rsp[quot_respect]:
+ assumes "Quotient R1 Abs1 Rep1"
+ assumes "Quotient R2 Abs2 Rep2"
+ shows "(prod_rel R1 R2 ===> R1) fst fst"
+ by simp
+
+lemma fst_prs[quot_preserve]:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ assumes q2: "Quotient R2 Abs2 Rep2"
+ shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst"
+ apply(simp add: expand_fun_eq)
+ apply(simp add: Quotient_abs_rep[OF q1])
+ done
+
+lemma snd_rsp[quot_respect]:
+ assumes "Quotient R1 Abs1 Rep1"
+ assumes "Quotient R2 Abs2 Rep2"
+ shows "(prod_rel R1 R2 ===> R2) snd snd"
+ by simp
+
+lemma snd_prs[quot_preserve]:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ assumes q2: "Quotient R2 Abs2 Rep2"
+ shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd"
+ apply(simp add: expand_fun_eq)
+ apply(simp add: Quotient_abs_rep[OF q2])
+ done
+
+lemma split_rsp[quot_respect]:
+ shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
+ by auto
+
+lemma split_prs[quot_preserve]:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ and q2: "Quotient R2 Abs2 Rep2"
+ shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split"
+ by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+
+lemma prod_fun_id[id_simps]:
+ shows "prod_fun id id = id"
+ by (simp add: prod_fun_def)
+
+lemma prod_rel_eq[id_simps]:
+ shows "prod_rel (op =) (op =) = (op =)"
+ by (simp add: expand_fun_eq)
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Quotient_Sum.thy Thu Feb 11 10:06:02 2010 +0100
@@ -0,0 +1,96 @@
+(* Title: Quotient_Sum.thy
+ Author: Cezary Kaliszyk and Christian Urban
+*)
+theory Quotient_Sum
+imports Quotient
+begin
+
+section {* Quotient infrastructure for the sum type. *}
+
+fun
+ sum_rel
+where
+ "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
+| "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
+| "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
+| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
+
+fun
+ sum_map
+where
+ "sum_map f1 f2 (Inl a) = Inl (f1 a)"
+| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
+
+declare [[map "+" = (sum_map, sum_rel)]]
+
+
+text {* should probably be in Sum_Type.thy *}
+lemma split_sum_all:
+ shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
+ apply(auto)
+ apply(case_tac x)
+ apply(simp_all)
+ done
+
+lemma sum_equivp[quot_equiv]:
+ assumes a: "equivp R1"
+ assumes b: "equivp R2"
+ shows "equivp (sum_rel R1 R2)"
+ apply(rule equivpI)
+ unfolding reflp_def symp_def transp_def
+ apply(simp_all add: split_sum_all)
+ apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
+ apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
+ apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
+ done
+
+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)"
+ unfolding Quotient_def
+ apply(simp add: split_sum_all)
+ apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
+ apply(simp_all add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
+ using q1 q2
+ unfolding Quotient_def
+ apply(blast)+
+ done
+
+lemma sum_Inl_rsp[quot_respect]:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ assumes q2: "Quotient R2 Abs2 Rep2"
+ shows "(R1 ===> sum_rel R1 R2) Inl Inl"
+ by simp
+
+lemma sum_Inr_rsp[quot_respect]:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ assumes q2: "Quotient R2 Abs2 Rep2"
+ shows "(R2 ===> sum_rel R1 R2) Inr Inr"
+ by simp
+
+lemma sum_Inl_prs[quot_preserve]:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ assumes q2: "Quotient R2 Abs2 Rep2"
+ shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
+ apply(simp add: expand_fun_eq)
+ apply(simp add: Quotient_abs_rep[OF q1])
+ done
+
+lemma sum_Inr_prs[quot_preserve]:
+ assumes q1: "Quotient R1 Abs1 Rep1"
+ assumes q2: "Quotient R2 Abs2 Rep2"
+ shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
+ apply(simp add: expand_fun_eq)
+ apply(simp add: Quotient_abs_rep[OF q2])
+ done
+
+lemma sum_map_id[id_simps]:
+ shows "sum_map id id = id"
+ by (simp add: expand_fun_eq split_sum_all)
+
+lemma sum_rel_eq[id_simps]:
+ shows "sum_rel (op =) (op =) = (op =)"
+ by (simp add: expand_fun_eq split_sum_all)
+
+end
--- a/Quot/ROOT.ML Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/ROOT.ML Thu Feb 11 10:06:02 2010 +0100
@@ -1,7 +1,7 @@
quick_and_dirty := true;
no_document use_thys
- ["QuotMain",
+ ["Quotient",
"Examples/AbsRepTest",
"Examples/FSet",
"Examples/FSet2",
--- a/Quot/quotient_def.ML Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/quotient_def.ML Thu Feb 11 10:06:02 2010 +0100
@@ -6,7 +6,7 @@
*)
signature QUOTIENT_DEF =
-sig
+sig
val quotient_def: mixfix -> Attrib.binding -> term -> term ->
local_theory -> (term * thm) * local_theory
@@ -32,7 +32,7 @@
(** Interface and Syntax Setup **)
-(* The ML-interface for a quotient definition takes
+(* The ML-interface for a quotient definition takes
as argument:
- the mixfix annotation
@@ -41,11 +41,11 @@
- the rhs of the definition as term
It returns the defined constant and its definition
- theorem; stores the data in the qconsts data slot.
+ theorem; stores the data in the qconsts data slot.
Restriction: At the moment the right-hand side must
- be a terms composed of constant. Similarly the
- left-hand side must be a single constant.
+ be a terms composed of constant. Similarly the
+ left-hand side must be a single constant.
*)
fun quotient_def mx attr lhs rhs lthy =
let
@@ -87,7 +87,7 @@
(OuterParse.opt_mixfix' --| OuterParse.$$$ "as" --
OuterParse.term)
-val _ = OuterSyntax.local_theory "quotient_definition"
+val _ = OuterSyntax.local_theory "quotient_definition"
"definition for constants over the quotient type"
OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
--- a/Quot/quotient_info.ML Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/quotient_info.ML Thu Feb 11 10:06:02 2010 +0100
@@ -13,8 +13,8 @@
type maps_info = {mapfun: string, relmap: string}
val maps_defined: theory -> string -> bool
val maps_lookup: theory -> string -> maps_info (* raises NotFound *)
- val maps_update_thy: string -> maps_info -> theory -> theory
- val maps_update: string -> maps_info -> Proof.context -> Proof.context
+ val maps_update_thy: string -> maps_info -> theory -> theory
+ val maps_update: string -> maps_info -> Proof.context -> Proof.context
val print_mapsinfo: Proof.context -> unit
type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
@@ -36,8 +36,8 @@
val equiv_rules_get: Proof.context -> thm list
val equiv_rules_add: attribute
- val rsp_rules_get: Proof.context -> thm list
- val prs_rules_get: Proof.context -> thm list
+ val rsp_rules_get: Proof.context -> thm list
+ val prs_rules_get: Proof.context -> thm list
val id_simps_get: Proof.context -> thm list
val quotient_rules_get: Proof.context -> thm list
val quotient_rules_add: attribute
@@ -61,10 +61,10 @@
val extend = I
val merge = Symtab.merge (K true))
-fun maps_defined thy s =
+fun maps_defined thy s =
Symtab.defined (MapsData.get thy) s
-fun maps_lookup thy s =
+fun maps_lookup thy s =
case (Symtab.lookup (MapsData.get thy) s) of
SOME map_fun => map_fun
| NONE => raise NotFound
@@ -72,12 +72,12 @@
fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
-fun maps_attribute_aux s minfo = Thm.declaration_attribute
+fun maps_attribute_aux s minfo = Thm.declaration_attribute
(fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
(* attribute to be used in declare statements *)
-fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) =
-let
+fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) =
+let
val thy = ProofContext.theory_of ctxt
val tyname = Sign.intern_type thy tystr
val mapname = Sign.intern_const thy mapstr
@@ -89,21 +89,21 @@
maps_attribute_aux tyname {mapfun = mapname, relmap = relname}
end
-val maps_attr_parser =
+val maps_attr_parser =
Args.context -- Scan.lift
- ((Args.name --| OuterParse.$$$ "=") --
- (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," --
+ ((Args.name --| OuterParse.$$$ "=") --
+ (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," --
Args.name --| OuterParse.$$$ ")"))
val _ = Context.>> (Context.map_theory
- (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
+ (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
"declaration of map information"))
fun print_mapsinfo ctxt =
let
- fun prt_map (ty_name, {mapfun, relmap}) =
+ fun prt_map (ty_name, {mapfun, relmap}) =
Pretty.block (Library.separate (Pretty.brk 2)
- (map Pretty.str
+ (map Pretty.str
["type:", ty_name,
"map:", mapfun,
"relation map:", relmap]))
@@ -111,11 +111,11 @@
MapsData.get (ProofContext.theory_of ctxt)
|> Symtab.dest
|> map (prt_map)
- |> Pretty.big_list "maps for type constructors:"
+ |> Pretty.big_list "maps for type constructors:"
|> Pretty.writeln
end
-
+
(* info about quotient types *)
type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
@@ -123,7 +123,7 @@
(type T = quotdata_info Symtab.table
val empty = Symtab.empty
val extend = I
- val merge = Symtab.merge (K true))
+ val merge = Symtab.merge (K true))
fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} =
{qtyp = Morphism.typ phi qtyp,
@@ -160,7 +160,7 @@
QuotData.get (ProofContext.theory_of ctxt)
|> Symtab.dest
|> map (prt_quot o snd)
- |> Pretty.big_list "quotients:"
+ |> Pretty.big_list "quotients:"
|> Pretty.writeln
end
@@ -223,7 +223,7 @@
|> map snd
|> flat
|> map prt_qconst
- |> Pretty.big_list "quotient constants:"
+ |> Pretty.big_list "quotient constants:"
|> Pretty.writeln
end
@@ -266,7 +266,7 @@
(* setup of the theorem lists *)
-val _ = Context.>> (Context.map_theory
+val _ = Context.>> (Context.map_theory
(EquivRules.setup #>
RspRules.setup #>
PrsRules.setup #>
--- a/Quot/quotient_tacs.ML Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/quotient_tacs.ML Thu Feb 11 10:06:02 2010 +0100
@@ -102,7 +102,7 @@
Since the left-hand-side contains a non-pattern '?P (f ?x)'
we rely on unification/instantiation to check whether the
- theorem applies and return NONE if it doesn't.
+ theorem applies and return NONE if it doesn't.
*)
fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
let
@@ -122,14 +122,14 @@
fun ball_bex_range_simproc ss redex =
let
val ctxt = Simplifier.the_context ss
-in
+in
case redex of
- (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
+ (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
(Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
- | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
- (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
+ | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
+ (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
| _ => NONE
@@ -151,7 +151,7 @@
5. then simplification like 0
- finally jump back to 1
+ finally jump back to 1
*)
fun regularize_tac ctxt =
let
@@ -159,18 +159,18 @@
val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"}
val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
- val simpset = (mk_minimal_ss ctxt)
+ val simpset = (mk_minimal_ss ctxt)
addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
- addsimprocs [simproc]
+ addsimprocs [simproc]
addSolver equiv_solver addSolver quotient_solver
val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)
in
simp_tac simpset THEN'
- REPEAT_ALL_NEW (CHANGED o FIRST'
+ REPEAT_ALL_NEW (CHANGED o FIRST'
[resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
resolve_tac (Inductive.get_monos ctxt),
resolve_tac @{thms ball_all_comm bex_ex_comm},
- resolve_tac eq_eqvs,
+ resolve_tac eq_eqvs,
simp_tac simpset])
end
@@ -179,7 +179,7 @@
(*** Injection Tactic ***)
(* Looks for Quot_True assumptions, and in case its parameter
- is an application, it returns the function and the argument.
+ is an application, it returns the function and the argument.
*)
fun find_qt_asm asms =
let
@@ -216,13 +216,13 @@
| Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
| _ => Conv.all_conv ctrm
-fun quot_true_tac ctxt fnctn =
+fun quot_true_tac ctxt fnctn =
CONVERSION
((Conv.params_conv ~1 (fn ctxt =>
(Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
-fun dest_comb (f $ a) = (f, a)
-fun dest_bcomb ((_ $ l) $ r) = (l, r)
+fun dest_comb (f $ a) = (f, a)
+fun dest_bcomb ((_ $ l) $ r) = (l, r)
fun unlam t =
case t of
@@ -236,7 +236,7 @@
(* We apply apply_rsp only in case if the type needs lifting.
This is the case if the type of the data in the Quot_True
- assumption is different from the corresponding type in the goal.
+ assumption is different from the corresponding type in the goal.
*)
val apply_rsp_tac =
Subgoal.FOCUS (fn {concl, asms, context,...} =>
@@ -265,7 +265,7 @@
end)
(* Instantiates and applies 'equals_rsp'. Since the theorem is
- complex we rely on instantiation to tell us if it applies
+ complex we rely on instantiation to tell us if it applies
*)
fun equals_rsp_tac R ctxt =
let
@@ -304,7 +304,7 @@
-(* Injection means to prove that the regularised theorem implies
+(* Injection means to prove that the regularised theorem implies
the abs/rep injected one.
The deterministic part:
@@ -317,7 +317,7 @@
- solve 'relation of relations' goals using quot_rel_rsp
- remove rep_abs from the right side
(Lambdas under respects may have left us some assumptions)
-
+
Then in order:
- split applications of lifted type (apply_rsp)
- split applications of non-lifted type (cong_tac)
@@ -364,7 +364,7 @@
(Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
=> rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
-| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
+| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
(rtac @{thm refl} ORELSE'
(equals_rsp_tac R ctxt THEN' RANGE [
quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
@@ -379,7 +379,7 @@
(* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
(* observe fun_map *)
| _ $ _ $ _
- => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
+ => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
ORELSE' rep_abs_rsp_tac ctxt
| _ => K no_tac
@@ -428,7 +428,7 @@
((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
if member (op=) xs h
then Conv.all_conv ctrm
- else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm
+ else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm
| _ => Conv.all_conv ctrm
fun fun_map_conv xs ctxt ctrm =
@@ -470,7 +470,7 @@
Then solves the quotient assumptions to get Rep2 and Abs1
Finally instantiates the function f using make_inst
If Rep2 is an identity then the pattern is simpler and
- make_inst_id is used
+ make_inst_id is used
*)
fun lambda_prs_simple_conv ctxt ctrm =
case (term_of ctrm) of
@@ -501,20 +501,20 @@
(* Cleaning consists of:
1. unfolding of ---> in front of everything, except
- bound variables (this prevents lambda_prs from
+ bound variables (this prevents lambda_prs from
becoming stuck)
2. simplification with lambda_prs
- 3. simplification with:
+ 3. simplification with:
- - Quotient_abs_rep Quotient_rel_rep
+ - Quotient_abs_rep Quotient_rel_rep
babs_prs all_prs ex_prs ex1_prs
- - id_simps and preservation lemmas and
+ - id_simps and preservation lemmas and
- - symmetric versions of the definitions
- (that is definitions of quotient constants
+ - symmetric versions of the definitions
+ (that is definitions of quotient constants
are folded)
4. test for refl
@@ -545,10 +545,10 @@
fun inst_spec_tac ctrms =
EVERY' (map (dtac o inst_spec) ctrms)
-fun all_list xs trm =
+fun all_list xs trm =
fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
-fun apply_under_Trueprop f =
+fun apply_under_Trueprop f =
HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
fun gen_frees_tac ctxt =
@@ -577,7 +577,7 @@
- 2nd prem is the rep/abs injection step
- 3rd prem is the cleaning part
- the Quot_True premise in 2nd records the lifted theorem
+ the Quot_True premise in 2nd records the lifted theorem
*)
val lifting_procedure_thm =
@{lemma "[|A;
@@ -590,7 +590,7 @@
let
val rtrm_str = Syntax.string_of_term ctxt rtrm
val qtrm_str = Syntax.string_of_term ctxt qtrm
- val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str,
+ val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str,
"", "does not match with original theorem", rtrm_str]
in
error msg
@@ -629,22 +629,22 @@
(* Automatic Proofs *)
val msg1 = "The regularize proof failed."
-val msg2 = cat_lines ["The injection proof failed.",
+val msg2 = cat_lines ["The injection proof failed.",
"This is probably due to missing respects lemmas.",
- "Try invoking the injection method manually to see",
+ "Try invoking the injection method manually to see",
"which lemmas are missing."]
val msg3 = "The cleaning proof failed."
fun lift_tac ctxt rthms =
let
- fun mk_tac rthm =
+ fun mk_tac rthm =
procedure_tac ctxt rthm
- THEN' RANGE_WARN
+ THEN' RANGE_WARN
[(regularize_tac ctxt, msg1),
(all_injection_tac ctxt, msg2),
(clean_tac ctxt, msg3)]
in
- simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *)
+ simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *)
THEN' RANGE (map mk_tac rthms)
end
--- a/Quot/quotient_term.ML Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/quotient_term.ML Thu Feb 11 10:06:02 2010 +0100
@@ -41,9 +41,9 @@
(*** Aggregate Rep/Abs Function ***)
-(* The flag RepF is for types in negative position; AbsF is for types
- in positive position. Because of this, function types need to be
- treated specially, since there the polarity changes.
+(* The flag RepF is for types in negative position; AbsF is for types
+ in positive position. Because of this, function types need to be
+ treated specially, since there the polarity changes.
*)
datatype flag = AbsF | RepF
@@ -56,7 +56,7 @@
fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
-fun mk_fun_compose flag (trm1, trm2) =
+fun mk_fun_compose flag (trm1, trm2) =
case flag of
AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
| RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
@@ -73,13 +73,13 @@
(* makes a Free out of a TVar *)
fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
-(* produces an aggregate map function for the
- rty-part of a quotient definition; abstracts
- over all variables listed in vs (these variables
- correspond to the type variables in rty)
-
- for example for: (?'a list * ?'b)
- it produces: %a b. prod_map (map a) b
+(* produces an aggregate map function for the
+ rty-part of a quotient definition; abstracts
+ over all variables listed in vs (these variables
+ correspond to the type variables in rty)
+
+ for example for: (?'a list * ?'b)
+ it produces: %a b. prod_map (map a) b
*)
fun mk_mapfun ctxt vs rty =
let
@@ -95,8 +95,8 @@
fold_rev Term.lambda vs' (mk_mapfun_aux rty)
end
-(* looks up the (varified) rty and qty for
- a quotient definition
+(* looks up the (varified) rty and qty for
+ a quotient definition
*)
fun get_rty_qty ctxt s =
let
@@ -107,9 +107,9 @@
(#rtyp qdata, #qtyp qdata)
end
-(* takes two type-environments and looks
- up in both of them the variable v, which
- must be listed in the environment
+(* takes two type-environments and looks
+ up in both of them the variable v, which
+ must be listed in the environment
*)
fun double_lookup rtyenv qtyenv v =
let
@@ -145,58 +145,58 @@
fun absrep_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
+ val ty_str = Syntax.string_of_typ ctxt ty
in
- raise LIFT_MATCH (space_implode " "
+ raise LIFT_MATCH (space_implode " "
["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
end
(** generation of an aggregate absrep function **)
-(* - In case of equal types we just return the identity.
-
+(* - In case of equal types we just return the identity.
+
- In case of TFrees we also return the identity.
-
- - In case of function types we recurse taking
- the polarity change into account.
-
- - If the type constructors are equal, we recurse for the
- arguments and build the appropriate map function.
-
- - If the type constructors are unequal, there must be an
- instance of quotient types:
-
- - we first look up the corresponding rty_pat and qty_pat
- from the quotient definition; the arguments of qty_pat
- must be some distinct TVars
- - we then match the rty_pat with rty and qty_pat with qty;
- if matching fails the types do not correspond -> error
- - the matching produces two environments; we look up the
- assignments for the qty_pat variables and recurse on the
- assignments
- - we prefix the aggregate map function for the rty_pat,
- which is an abstraction over all type variables
- - finally we compose the result with the appropriate
+
+ - In case of function types we recurse taking
+ the polarity change into account.
+
+ - If the type constructors are equal, we recurse for the
+ arguments and build the appropriate map function.
+
+ - If the type constructors are unequal, there must be an
+ instance of quotient types:
+
+ - we first look up the corresponding rty_pat and qty_pat
+ from the quotient definition; the arguments of qty_pat
+ must be some distinct TVars
+ - we then match the rty_pat with rty and qty_pat with qty;
+ if matching fails the types do not correspond -> error
+ - the matching produces two environments; we look up the
+ assignments for the qty_pat variables and recurse on the
+ assignments
+ - we prefix the aggregate map function for the rty_pat,
+ which is an abstraction over all type variables
+ - finally we compose the result with the appropriate
absrep function in case at least one argument produced
a non-identity function /
otherwise we just return the appropriate absrep
- function
-
- The composition is necessary for types like
-
- ('a list) list / ('a foo) foo
-
- The matching is necessary for types like
-
- ('a * 'a) list / 'a bar
+ function
+
+ The composition is necessary for types like
+
+ ('a list) list / ('a foo) foo
+
+ The matching is necessary for types like
+
+ ('a * 'a) list / 'a bar
The test is necessary in order to eliminate superfluous
- identity maps.
-*)
+ identity maps.
+*)
fun absrep_fun flag ctxt (rty, qty) =
- if rty = qty
+ if rty = qty
then mk_identity rty
else
case (rty, qty) of
@@ -209,12 +209,12 @@
end
| (Type (s, tys), Type (s', tys')) =>
if s = s'
- then
+ then
let
val args = map (absrep_fun flag ctxt) (tys ~~ tys')
in
list_comb (get_mapfun ctxt s, args)
- end
+ end
else
let
val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
@@ -222,8 +222,8 @@
val qtyenv = match ctxt absrep_match_err qty_pat qty
val args_aux = map (double_lookup rtyenv qtyenv) vs
val args = map (absrep_fun flag ctxt) args_aux
- val map_fun = mk_mapfun ctxt vs rty_pat
- val result = list_comb (map_fun, args)
+ val map_fun = mk_mapfun ctxt vs rty_pat
+ val result = list_comb (map_fun, args)
in
if forall is_identity args
then absrep_const flag ctxt s'
@@ -253,7 +253,7 @@
(* instantiates TVars so that the term is of type ty *)
fun force_typ ctxt trm ty =
let
- val thy = ProofContext.theory_of ctxt
+ val thy = ProofContext.theory_of ctxt
val trm_ty = fastype_of trm
val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
in
@@ -269,7 +269,7 @@
fun get_relmap ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
+ val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
in
Const (relmap, dummyT)
@@ -292,7 +292,7 @@
fun get_equiv_rel ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
+ val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
in
#equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
end
@@ -300,14 +300,14 @@
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
+ val ty_str = Syntax.string_of_typ ctxt ty
in
- raise LIFT_MATCH (space_implode " "
+ raise LIFT_MATCH (space_implode " "
["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
end
-(* builds the aggregate equivalence relation
- that will be the argument of Respects
+(* builds the aggregate equivalence relation
+ that will be the argument of Respects
*)
fun equiv_relation ctxt (rty, qty) =
if rty = qty
@@ -315,26 +315,26 @@
else
case (rty, qty) of
(Type (s, tys), Type (s', tys')) =>
- if s = s'
- then
+ if s = s'
+ then
let
val args = map (equiv_relation ctxt) (tys ~~ tys')
in
- list_comb (get_relmap ctxt s, args)
- end
- else
+ list_comb (get_relmap ctxt s, args)
+ end
+ else
let
val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
val rtyenv = match ctxt equiv_match_err rty_pat rty
val qtyenv = match ctxt equiv_match_err qty_pat qty
- val args_aux = map (double_lookup rtyenv qtyenv) vs
+ val args_aux = map (double_lookup rtyenv qtyenv) vs
val args = map (equiv_relation ctxt) args_aux
- val rel_map = mk_relmap ctxt vs rty_pat
+ val rel_map = mk_relmap ctxt vs rty_pat
val result = list_comb (rel_map, args)
val eqv_rel = get_equiv_rel ctxt s'
val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
in
- if forall is_eq args
+ if forall is_eq args
then eqv_rel'
else mk_rel_compose (result, eqv_rel')
end
@@ -349,17 +349,17 @@
(*** Regularization ***)
(* Regularizing an rtrm means:
-
- - Quantifiers over types that need lifting are replaced
+
+ - Quantifiers over types that need lifting are replaced
by bounded quantifiers, for example:
All P ----> All (Respects R) P
where the aggregate relation R is given by the rty and qty;
-
+
- Abstractions over types that need lifting are replaced
by bounded abstractions, for example:
-
+
%x. P ----> Ball (Respects R) %x. P
- Equalities over types that need lifting are replaced by
@@ -392,10 +392,10 @@
val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT)
val mk_resp = Const (@{const_name Respects}, dummyT)
-(* - applies f to the subterm of an abstraction,
- otherwise to the given term,
- - used by regularize, therefore abstracted
- variables do not have to be treated specially
+(* - applies f to the subterm of an abstraction,
+ otherwise to the given term,
+ - used by regularize, therefore abstracted
+ variables do not have to be treated specially
*)
fun apply_subt f (trm1, trm2) =
case (trm1, trm2) of
@@ -433,10 +433,10 @@
(* produces a regularized version of rtrm
- - the result might contain dummyTs
+ - the result might contain dummyTs
- - for regularisation we do not need any
- special treatment of bound variables
+ - for regularisation we do not need any
+ special treatment of bound variables
*)
fun regularize_trm ctxt (rtrm, qtrm) =
case (rtrm, qtrm) of
@@ -474,8 +474,8 @@
end
| (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _,
- (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $
- (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))),
+ (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $
+ (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))),
Const (@{const_name "Ex1"}, ty') $ t') =>
let
val t_ = incr_boundvars (~1) t
@@ -495,7 +495,7 @@
else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
end
- | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
+ | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
Const (@{const_name "All"}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
@@ -506,7 +506,7 @@
else mk_ball $ (mk_resp $ resrel) $ subtrm
end
- | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
+ | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
Const (@{const_name "Ex"}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
@@ -527,18 +527,18 @@
else mk_bex1_rel $ resrel $ subtrm
end
- | (* equalities need to be replaced by appropriate equivalence relations *)
+ | (* equalities need to be replaced by appropriate equivalence relations *)
(Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
if ty = ty' then rtrm
- else equiv_relation ctxt (domain_type ty, domain_type ty')
+ else equiv_relation ctxt (domain_type ty, domain_type ty')
- | (* in this case we just check whether the given equivalence relation is correct *)
+ | (* in this case we just check whether the given equivalence relation is correct *)
(rel, Const (@{const_name "op ="}, ty')) =>
let
val rel_ty = fastype_of rel
- val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
+ val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
in
- if rel' aconv rel then rtrm
+ if rel' aconv rel then rtrm
else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
end
@@ -557,7 +557,7 @@
if Pattern.matches thy (rtrm', rtrm)
then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm
end
- end
+ end
| (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) =>
@@ -571,11 +571,11 @@
regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2')
| (Bound i, Bound i') =>
- if i = i' then rtrm
+ if i = i' then rtrm
else raise (LIFT_MATCH "regularize (bounds mismatch)")
| _ =>
- let
+ let
val rtrm_str = Syntax.string_of_term ctxt rtrm
val qtrm_str = Syntax.string_of_term ctxt qtrm
in
@@ -583,7 +583,7 @@
end
fun regularize_trm_chk ctxt (rtrm, qtrm) =
- regularize_trm ctxt (rtrm, qtrm)
+ regularize_trm ctxt (rtrm, qtrm)
|> Syntax.check_term ctxt
@@ -595,22 +595,22 @@
For abstractions:
- * If the type of the abstraction needs lifting, then we add Rep/Abs
+ * If the type of the abstraction needs lifting, then we add Rep/Abs
around the abstraction; otherwise we leave it unchanged.
-
+
For applications:
-
- * If the application involves a bounded quantifier, we recurse on
+
+ * If the application involves a bounded quantifier, we recurse on
the second argument. If the application is a bounded abstraction,
we always put an Rep/Abs around it (since bounded abstractions
- are assumed to always need lifting). Otherwise we recurse on both
+ are assumed to always need lifting). Otherwise we recurse on both
arguments.
For constants:
- * If the constant is (op =), we leave it always unchanged.
+ * If the constant is (op =), we leave it always unchanged.
Otherwise the type of the constant needs lifting, we put
- and Rep/Abs around it.
+ and Rep/Abs around it.
For free variables:
@@ -619,13 +619,13 @@
Vars case cannot occur.
*)
-fun mk_repabs ctxt (T, T') trm =
+fun mk_repabs ctxt (T, T') trm =
absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm)
fun inj_repabs_err ctxt msg rtrm qtrm =
let
val rtrm_str = Syntax.string_of_term ctxt rtrm
- val qtrm_str = Syntax.string_of_term ctxt qtrm
+ val qtrm_str = Syntax.string_of_term ctxt qtrm
in
raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
end
@@ -662,11 +662,11 @@
else mk_repabs ctxt (rty, qty) result
end
- | (t $ s, t' $ s') =>
+ | (t $ s, t' $ s') =>
(inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s'))
- | (Free (_, T), Free (_, T')) =>
- if T = T' then rtrm
+ | (Free (_, T), Free (_, T')) =>
+ if T = T' then rtrm
else mk_repabs ctxt (T, T') rtrm
| (_, Const (@{const_name "op ="}, _)) => rtrm
@@ -674,15 +674,15 @@
| (_, Const (_, T')) =>
let
val rty = fastype_of rtrm
- in
+ in
if rty = T' then rtrm
else mk_repabs ctxt (rty, T') rtrm
- end
-
+ end
+
| _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm
fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
- inj_repabs_trm ctxt (rtrm, qtrm)
+ inj_repabs_trm ctxt (rtrm, qtrm)
|> Syntax.check_term ctxt
--- a/Quot/quotient_typ.ML Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/quotient_typ.ML Thu Feb 11 10:06:02 2010 +0100
@@ -7,10 +7,10 @@
signature QUOTIENT_TYPE =
sig
- val quotient_type: ((string list * binding * mixfix) * (typ * term)) list
+ val quotient_type: ((string list * binding * mixfix) * (typ * term)) list
-> Proof.context -> Proof.state
- val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list
+ val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list
-> Proof.context -> Proof.state
end;
@@ -41,7 +41,7 @@
let
val goals' = map (rpair []) goals
fun after_qed' thms = after_qed (the_single thms)
-in
+in
Proof.theorem_i NONE after_qed' [goals'] ctxt
end
@@ -155,7 +155,7 @@
(* quot_type theorem *)
val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, equiv_thm, typedef_info) lthy3
- (* quotient theorem *)
+ (* quotient theorem *)
val quotient_thm = typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_thm) lthy3
val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
@@ -189,22 +189,22 @@
else [qty_str ^ "illegal schematic variable(s) in the relation."]
val dup_vs =
- (case duplicates (op =) vs of
+ (case duplicates (op =) vs of
[] => []
| dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups])
val extra_rty_tfrees =
- (case subtract (op =) vs rty_tfreesT of
+ (case subtract (op =) vs rty_tfreesT of
[] => []
| extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras])
val extra_rel_tfrees =
- (case subtract (op =) vs rel_tfrees of
+ (case subtract (op =) vs rel_tfrees of
[] => []
| extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras])
-
+
val illegal_rel_frees =
- (case rel_frees of
+ (case rel_frees of
[] => []
| xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs])
@@ -248,28 +248,28 @@
relations are equivalence relations
*)
-fun quotient_type quot_list lthy =
+fun quotient_type quot_list lthy =
let
- (* sanity check *)
- val _ = List.app sanity_check quot_list
+ (* sanity check *)
+ val _ = List.app sanity_check quot_list
val _ = List.app (map_check lthy) quot_list
fun mk_goal (rty, rel) =
let
val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
- in
+ in
HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel)
end
val goals = map (mk_goal o snd) quot_list
-
+
fun after_qed thms lthy =
fold_map mk_quotient_type (quot_list ~~ thms) lthy |> snd
in
theorem after_qed goals lthy
end
-
-fun quotient_type_cmd specs lthy =
+
+fun quotient_type_cmd specs lthy =
let
fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy =
let
@@ -278,12 +278,12 @@
val lthy1 = Variable.declare_typ rty lthy
val pre_rel = Syntax.parse_term lthy1 rel_str
val pre_rel' = Syntax.type_constraint (rty --> rty --> @{typ bool}) pre_rel
- val rel = Syntax.check_term lthy1 pre_rel'
+ val rel = Syntax.check_term lthy1 pre_rel'
val lthy2 = Variable.declare_term rel lthy1
-
+
(* old parsing *)
(* val rty = Syntax.read_typ lthy rty_str
- val rel = Syntax.read_term lthy rel_str *)
+ val rel = Syntax.read_term lthy rel_str *)
in
(((vs, qty_name, mx), (rty, rel)), lthy2)
end
@@ -293,16 +293,16 @@
quotient_type spec' lthy'
end
-val quotspec_parser =
+val quotspec_parser =
OuterParse.and_list1
- ((OuterParse.type_args -- OuterParse.binding) --
- OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) --
+ ((OuterParse.type_args -- OuterParse.binding) --
+ OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) --
(OuterParse.$$$ "/" |-- OuterParse.term))
val _ = OuterKeyword.keyword "/"
-val _ =
- OuterSyntax.local_theory_to_proof "quotient_type"
+val _ =
+ OuterSyntax.local_theory_to_proof "quotient_type"
"quotient type definitions (require equivalence proofs)"
OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)