# HG changeset patch # User Cezary Kaliszyk # Date 1259770536 -3600 # Node ID 4efb104514f7ea9129fb45b04b0d0ee7bc06ea3c # Parent 74348dc2f8bb6ca3f8f6b512fcda01fb41075fa1 More experiments with higher order quotients and theorems with non-lifted constants. diff -r 74348dc2f8bb -r 4efb104514f7 IntEx.thy --- a/IntEx.thy Wed Dec 02 14:37:21 2009 +0100 +++ b/IntEx.thy Wed Dec 02 17:15:36 2009 +0100 @@ -151,9 +151,6 @@ apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) prefer 2 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) -apply(simp add: id_def) -apply(tactic {* inj_repabs_tac_intex @{context} 1*}) -apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) apply(tactic {* inj_repabs_tac_intex @{context} 1*}) @@ -190,7 +187,6 @@ lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) -apply(simp) apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) apply(tactic {* clean_tac @{context} [quot] defs 1 *}) done @@ -199,35 +195,88 @@ apply simp done -(* FIXME/TODO: is this a respectfulness theorem? Does not look like one. *) -lemma map_prs: - "map REP_my_int (map ABS_my_int x) = x" + +lemma foldr_prs: + 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" +apply (induct l) +apply (simp add: QUOTIENT_ABS_REP[OF b]) +apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b]) +done + +lemma foldl_prs: + 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" +apply (induct l arbitrary:e) +apply (simp add: QUOTIENT_ABS_REP[OF a]) +apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b]) +done + +lemma map_prs: + 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" +apply (induct l) +apply (simp) +apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b]) +done + + +(* Removed unneeded assumption: "QUOTIENT R abs1 rep1" *) +lemma nil_prs: + shows "map abs1 [] = []" +by simp + +lemma cons_prs: + assumes a: "QUOTIENT R1 abs1 rep1" + shows "(map abs1) ((rep1 h) # (map rep1 t)) = h # t" + apply (induct t) +by (simp_all add: QUOTIENT_ABS_REP[OF a]) + +lemma cons_rsp[quot_rsp]: + "(op \ ===> LIST_REL op \ ===> LIST_REL op \) op # op #" +by simp + +(* I believe it's true. *) +lemma foldl_rsp[quot_rsp]: + "((op \ ===> op \ ===> op \) ===> op \ ===> LIST_REL op \ ===> op \) foldl foldl" +apply (simp only: FUN_REL.simps) +apply (rule allI) +apply (rule allI) +apply (rule impI) +apply (rule allI) +apply (rule allI) +apply (rule impI) +apply (rule allI) +apply (rule allI) +apply (rule impI) +apply (induct_tac xb yb rule:list_induct2) (* To finish I need to give it: arbitrary:xa ya *) sorry -lemma foldl_prs[quot_rsp]: - "((op \ ===> op \ ===> op \) ===> op \ ===> op = ===> op \) foldl foldl" -sorry +lemma nil_listrel_rsp[quot_rsp]: + "(LIST_REL R) [] []" +by simp lemma "foldl PLUS x [] = x" apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -apply(simp add: map_prs) -apply(simp only: map_prs) -apply(tactic {* clean_tac @{context} [quot] defs 1 *}) -sorry - -(* - FIXME: All below is your construction code; mostly commented out as it - does not work. -*) - -lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" -apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) -apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) -apply(simp) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) +apply(simp only: nil_prs) apply(tactic {* clean_tac @{context} [quot] defs 1 *}) done +lemma ho_tst2: "foldl my_plus x (h # t) \ my_plus h (foldl my_plus x t)" +sorry +lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" +apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) +apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) +apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) +apply(simp only: cons_prs[OF QUOTIENT_my_int]) +apply(tactic {* clean_tac @{context} [quot] defs 1 *}) +done + diff -r 74348dc2f8bb -r 4efb104514f7 QuotMain.thy --- a/QuotMain.thy Wed Dec 02 14:37:21 2009 +0100 +++ b/QuotMain.thy Wed Dec 02 17:15:36 2009 +0100 @@ -787,6 +787,7 @@ [rtac @{thm FUN_QUOTIENT}, resolve_tac quot_thms, rtac @{thm IDENTITY_QUOTIENT}, + rtac @{thm LIST_QUOTIENT}, (* For functional identity quotients, (op = ---> op =) *) (* TODO: think about the other way around, if we need to shorten the relation *) CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))]) @@ -1222,7 +1223,7 @@ val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs) in - EVERY' [lambda_prs_tac lthy quot, + EVERY' [TRY o lambda_prs_tac lthy quot, TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), TRY o simp_tac simp_ctxt, TRY o rtac refl]