--- a/Attic/Quot/Examples/AbsRepTest.thy Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,240 +0,0 @@
-theory AbsRepTest
-imports "../Quotient" "../Quotient_List" "../Quotient_Option" "../Quotient_Sum" "../Quotient_Product" List
-begin
-
-
-(*
-ML_command "ProofContext.debug := false"
-ML_command "ProofContext.verbose := false"
-*)
-
-ML {* open Quotient_Term *}
-
-ML {*
-fun test_funs flag ctxt (rty, qty) =
- (absrep_fun_chk flag ctxt (rty, qty)
- |> Syntax.string_of_term ctxt
- |> writeln;
- equiv_relation_chk ctxt (rty, qty)
- |> Syntax.string_of_term ctxt
- |> writeln)
-*}
-
-definition
- erel1 (infixl "\<approx>1" 50)
-where
- "erel1 \<equiv> \<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"
-
-quotient_type
- 'a fset = "'a list" / erel1
- apply(rule equivpI)
- unfolding erel1_def reflp_def symp_def transp_def
- by auto
-
-definition
- erel2 (infixl "\<approx>2" 50)
-where
- "erel2 \<equiv> \<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"
-
-quotient_type
- 'a foo = "('a * 'a) list" / erel2
- apply(rule equivpI)
- unfolding erel2_def reflp_def symp_def transp_def
- by auto
-
-definition
- erel3 (infixl "\<approx>3" 50)
-where
- "erel3 \<equiv> \<lambda>(xs::('a * int) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"
-
-quotient_type
- 'a bar = "('a * int) list" / "erel3"
- apply(rule equivpI)
- unfolding erel3_def reflp_def symp_def transp_def
- by auto
-
-fun
- intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infixl "\<approx>4" 50)
-where
- "intrel (x, y) (u, v) = (x + v = u + y)"
-
-quotient_type myint = "nat \<times> nat" / intrel
- by (auto simp add: equivp_def expand_fun_eq)
-
-ML {*
-test_funs AbsF @{context}
- (@{typ "nat \<times> nat"},
- @{typ "myint"})
-*}
-
-ML {*
-test_funs AbsF @{context}
- (@{typ "('a * 'a) list"},
- @{typ "'a foo"})
-*}
-
-ML {*
-test_funs RepF @{context}
- (@{typ "(('a * 'a) list * 'b)"},
- @{typ "('a foo * 'b)"})
-*}
-
-ML {*
-test_funs AbsF @{context}
- (@{typ "(('a list) * int) list"},
- @{typ "('a fset) bar"})
-*}
-
-ML {*
-test_funs AbsF @{context}
- (@{typ "('a list)"},
- @{typ "('a fset)"})
-*}
-
-ML {*
-test_funs AbsF @{context}
- (@{typ "('a list) list"},
- @{typ "('a fset) fset"})
-*}
-
-
-ML {*
-test_funs AbsF @{context}
- (@{typ "((nat * nat) list) list"},
- @{typ "((myint) fset) fset"})
-*}
-
-ML {*
-test_funs AbsF @{context}
- (@{typ "(('a * 'a) list) list"},
- @{typ "(('a * 'a) fset) fset"})
-*}
-
-ML {*
-test_funs AbsF @{context}
- (@{typ "(nat * nat) list"},
- @{typ "myint fset"})
-*}
-
-ML {*
-test_funs AbsF @{context}
- (@{typ "('a list) list \<Rightarrow> 'a list"},
- @{typ "('a fset) fset \<Rightarrow> 'a fset"})
-*}
-
-lemma OO_sym_inv:
- assumes sr: "symp r"
- and ss: "symp s"
- shows "(r OO s) x y = (s OO r) y x"
- using sr ss
- unfolding symp_def
- apply (metis pred_comp.intros pred_compE ss symp_def)
- done
-
-lemma abs_o_rep:
- assumes a: "Quotient r absf repf"
- shows "absf o repf = id"
- apply(rule ext)
- apply(simp add: Quotient_abs_rep[OF a])
- done
-
-lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
- apply (rule eq_reflection)
- apply auto
- done
-
-lemma map_rel_cong: "b \<approx>1 ba \<Longrightarrow> map f b \<approx>1 map f ba"
- unfolding erel1_def
- apply(simp only: set_map set_in_eq)
- done
-
-lemma quotient_compose_list_gen_pre:
- assumes a: "equivp r2"
- and b: "Quotient r2 abs2 rep2"
- shows "(list_rel r2 OOO op \<approx>1) r s =
- ((list_rel r2 OOO op \<approx>1) r r \<and> (list_rel r2 OOO op \<approx>1) s s \<and>
- abs_fset (map abs2 r) = abs_fset (map abs2 s))"
- apply rule
- apply rule
- apply rule
- apply (rule list_rel_refl)
- apply (metis equivp_def a)
- apply rule
- apply (rule equivp_reflp[OF fset_equivp])
- apply (rule list_rel_refl)
- apply (metis equivp_def a)
- apply(rule)
- apply rule
- apply (rule list_rel_refl)
- apply (metis equivp_def a)
- apply rule
- apply (rule equivp_reflp[OF fset_equivp])
- apply (rule list_rel_refl)
- apply (metis equivp_def a)
- apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s")
- apply (metis Quotient_rel[OF Quotient_fset])
- apply (auto)[1]
- apply (subgoal_tac "map abs2 r = map abs2 b")
- prefer 2
- apply (metis Quotient_rel[OF list_quotient[OF b]])
- apply (subgoal_tac "map abs2 s = map abs2 ba")
- prefer 2
- apply (metis Quotient_rel[OF list_quotient[OF b]])
- apply (simp add: map_rel_cong)
- apply rule
- apply (rule rep_abs_rsp[of "list_rel r2" "map abs2"])
- apply (rule list_quotient)
- apply (rule b)
- apply (rule list_rel_refl)
- apply (metis equivp_def a)
- apply rule
- prefer 2
- apply (rule rep_abs_rsp_left[of "list_rel r2" "map abs2"])
- apply (rule list_quotient)
- apply (rule b)
- apply (rule list_rel_refl)
- apply (metis equivp_def a)
- apply (erule conjE)+
- apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s")
- apply (rule map_rel_cong)
- apply (assumption)
- apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp a b)
- done
-
-lemma quotient_compose_list_gen:
- assumes a: "Quotient r2 abs2 rep2"
- and b: "equivp r2" (* reflp is not enough *)
- shows "Quotient ((list_rel r2) OOO (op \<approx>1))
- (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)"
- unfolding Quotient_def comp_def
- apply (rule)+
- apply (simp add: abs_o_rep[OF a] id_simps Quotient_abs_rep[OF Quotient_fset])
- apply (rule)
- apply (rule)
- apply (rule)
- apply (rule list_rel_refl)
- apply (metis b equivp_def)
- apply (rule)
- apply (rule equivp_reflp[OF fset_equivp])
- apply (rule list_rel_refl)
- apply (metis b equivp_def)
- apply rule
- apply rule
- apply(rule quotient_compose_list_gen_pre[OF b a])
- done
-
-(* This is the general statement but the types of abs2 and rep2
- are wrong as can be seen in following exanples *)
-lemma quotient_compose_general:
- assumes a2: "Quotient r1 abs1 rep1"
- and "Quotient r2 abs2 rep2"
- shows "Quotient ((list_rel r2) OOO r1)
- (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep1)"
-sorry
-
-thm quotient_compose_list_gen[OF Quotient_fset fset_equivp]
-thm quotient_compose_general[OF Quotient_fset]
-(* Doesn't work: *)
-(* thm quotient_compose_general[OF Quotient_fset Quotient_fset] *)
-
-end