diff -r f89ee40fbb08 -r 78d828f43cdf Attic/Quot/Examples/AbsRepTest.thy --- a/Attic/Quot/Examples/AbsRepTest.thy Sat Dec 17 16:57:25 2011 +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 "\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