Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorChristian Urban <urbanc@in.tum.de>
Thu, 10 Dec 2009 18:28:41 +0100
changeset 701 1f4dfcd9351b
parent 700 91b079db7380 (current diff)
parent 698 ed44eaaea63e (diff)
child 702 b89b578d15e6
merged
Quot/Quotients.thy file | annotate | diff | comparison | revisions 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/QuotOption.thy	Thu Dec 10 18:28:41 2009 +0100
@@ -0,0 +1,82 @@
+theory QuotOption
+imports QuotMain
+begin
+
+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"
+
+fun
+  option_map
+where
+  "option_map f None = None"
+| "option_map f (Some x) = Some (f x)"
+
+declare [[map * = (option_map, option_rel)]]
+
+lemma option_quotient[quot_thm]:
+  assumes q: "Quotient R Abs Rep"
+  shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)"
+  apply (unfold Quotient_def)
+  apply (rule conjI)
+  apply (rule allI)
+  apply (case_tac a)
+  apply (simp_all add: Quotient_abs_rep[OF q])
+  apply (rule conjI)
+  apply (rule allI)
+  apply (case_tac a)
+  apply (simp_all add: Quotient_rel_rep[OF q])
+  apply (rule allI)+
+  apply (case_tac r)
+  apply (case_tac s)
+  apply (simp_all add: Quotient_abs_rep[OF q] add: Quotient_rel_rep[OF q])
+  apply (case_tac s)
+  apply (simp_all add: Quotient_abs_rep[OF q] add: Quotient_rel_rep[OF q])
+  using q
+  unfolding Quotient_def
+  apply metis
+done
+
+lemma option_rel_some:
+  assumes e: "equivp R"
+  and     a: "option_rel R (Some a) = option_rel R (Some aa)"
+  shows      "R a aa"
+using a apply(drule_tac x="Some aa" in fun_cong)
+apply(simp add: equivp_reflp[OF e])
+done
+
+lemma option_equivp[quot_equiv]:
+  assumes a: "equivp R"
+  shows "equivp (option_rel R)"
+  unfolding equivp_def
+  apply(rule allI)+
+  apply(case_tac x)
+  apply(case_tac y)
+  apply(simp_all)
+  apply(unfold not_def)
+  apply(rule impI)
+  apply(drule_tac x="None" in fun_cong)
+  apply simp
+  apply(case_tac y)
+  apply(simp_all)
+  apply(unfold not_def)
+  apply(rule impI)
+  apply(drule_tac x="None" in fun_cong)
+  apply simp
+  apply(rule iffI)
+  apply(rule ext)
+  apply(case_tac xa)
+  apply(auto)
+  apply(rule equivp_transp[OF a])
+  apply(rule equivp_symp[OF a])
+  apply(assumption)+
+  apply(rule equivp_transp[OF a])
+  apply(assumption)+
+  apply(simp only: option_rel_some[OF a])
+  done
+
+end
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/QuotSum.thy	Thu Dec 10 18:28:41 2009 +0100
@@ -0,0 +1,84 @@
+theory QuotSum
+imports QuotMain
+begin
+
+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)]]
+
+lemma sum_equivp[quot_equiv]:
+  assumes a: "equivp R1"
+  assumes b: "equivp R2"
+  shows "equivp (sum_rel R1 R2)"
+unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
+apply(auto)
+apply(case_tac x)
+apply(auto simp add: equivp_reflp[OF a] equivp_reflp[OF b])
+apply(case_tac x)
+apply(case_tac y)
+prefer 3
+apply(case_tac y)
+apply(auto simp add: equivp_symp[OF a] equivp_symp[OF b])
+apply(case_tac x)
+apply(case_tac y)
+apply(case_tac z)
+prefer 3
+apply(case_tac z)
+prefer 5
+apply(case_tac y)
+apply(case_tac z)
+prefer 3
+apply(case_tac z)
+apply(auto)
+apply(metis equivp_transp[OF b])
+apply(metis equivp_transp[OF a])
+done
+
+lemma sum_fun_fun:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  assumes q2: "Quotient R2 Abs2 Rep2"
+  shows  "sum_rel R1 R2 r s =
+          (sum_rel R1 R2 r r \<and> sum_rel R1 R2 s s \<and> sum_map Abs1 Abs2 r = sum_map Abs1 Abs2 s)"
+  using q1 q2
+  apply(case_tac r)
+  apply(case_tac s)
+  apply(simp_all)
+  prefer 2
+  apply(case_tac s)
+  apply(auto)
+  unfolding Quotient_def 
+  apply metis+
+  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(rule conjI)
+  apply(rule allI)
+  apply(case_tac a)
+  apply(simp add: Quotient_abs_rep[OF q1])
+  apply(simp add: Quotient_abs_rep[OF q2])
+  apply(rule conjI)
+  apply(rule allI)
+  apply(case_tac a)
+  apply(simp add: Quotient_rel_rep[OF q1])
+  apply(simp add: Quotient_rel_rep[OF q2])
+  apply(rule allI)+
+  apply(rule sum_fun_fun[OF q1 q2])
+  done
+
+end
\ No newline at end of file
--- a/Quot/Quotients.thy	Thu Dec 10 18:28:30 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-theory Quotients
-imports Main
-begin
-
-(* Other quotients that have not been proved yet *)
-
-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"
-
-fun
-  option_map
-where
-  "option_map f None = None"
-| "option_map f (Some x) = Some (f x)"
-
-fun
-  prod_rel
-where
-  "prod_rel R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \<and> R2 a2 b2)"
-
-fun
-  prod_map
-where
-  "prod_map f1 f2 (a,b) = (f1 a, f2 b)"
-
-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)"
-
-fun
-  noption_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)"
-where
-  "noption_map f (nSome x) = nSome (f x)"
-| "noption_map f nNone = nNone"
-
-fun
-  noption_rel
-where
-  "noption_rel r (nSome x) (nSome y) = r x y"
-| "noption_rel r _ _ = False"
-
-declare [[map noption = (noption_map, noption_rel)]]
-
-lemma "noption_map id = id"
-sorry
-
-lemma noption_Quotient:
-  assumes q: "Quotient R Abs Rep"
-  shows "Quotient (noption_rel R) (noption_map Abs) (noption_map Rep)"
-  apply (unfold Quotient_def)
-  apply (auto)
-  using q
-  apply (unfold Quotient_def)
-  apply (case_tac "a :: 'b noption")
-  apply (simp)
-  apply (simp)
-  apply (case_tac "a :: 'b noption")
-  apply (simp only: option_map.simps)
-  apply (subst option_rel.simps)
-  (* Simp starts hanging so don't know how to continue *)
-  sorry
nominal2