diff -r db158e995bfc -r 9df6144e281b Attic/Quot/Examples/AbsRepTest.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Attic/Quot/Examples/AbsRepTest.thy Thu Feb 25 07:57:17 2010 +0100 @@ -0,0 +1,240 @@ +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 "\1" 50) +where + "erel1 \ \xs ys. \e. e \ set xs \ e \ 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 "\2" 50) +where + "erel2 \ \(xs::('a * 'a) list) ys. \e. e \ set xs \ e \ 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 "\3" 50) +where + "erel3 \ \(xs::('a * int) list) ys. \e. e \ set xs \ e \ 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 \ nat) \ (nat \ nat) \ bool" (infixl "\4" 50) +where + "intrel (x, y) (u, v) = (x + v = u + y)" + +quotient_type myint = "nat \ nat" / intrel + by (auto simp add: equivp_def expand_fun_eq) + +ML {* +test_funs AbsF @{context} + (@{typ "nat \ 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 \ 'a list"}, + @{typ "('a fset) fset \ '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: "(\e. ((e \ A) \ (e \ B))) \ A = B" + apply (rule eq_reflection) + apply auto + done + +lemma map_rel_cong: "b \1 ba \ map f b \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 \1) r s = + ((list_rel r2 OOO op \1) r r \ (list_rel r2 OOO op \1) s s \ + 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 \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 \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 \1)) + (abs_fset \ (map abs2)) ((map rep2) \ 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 \ (map abs2)) ((map rep2) \ 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