# HG changeset patch # User Christian Urban # Date 1260055185 -3600 # Node ID e121ac0028f8cea669c9b1bff7dd3c7183de08a8 # Parent 0384e039b7f26bcf778716ca05532221219bee9b# Parent 5dffcd087e306cc1135caa7799beb92ec9261765 merged diff -r 0384e039b7f2 -r e121ac0028f8 IntEx.thy --- a/IntEx.thy Sun Dec 06 00:13:35 2009 +0100 +++ b/IntEx.thy Sun Dec 06 00:19:45 2009 +0100 @@ -162,7 +162,6 @@ apply(tactic {* procedure_tac @{context} @{thm test1} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -apply(tactic {* simp_tac (HOL_basic_ss addSolver quotient_solver addsimps @{thms all_prs}) 1 *}) apply(tactic {* clean_tac @{context} 1 *}) done @@ -217,22 +216,6 @@ apply simp done -(* I believe it's true. *) -lemma foldl_rsp[quotient_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 PLUS x [] = x" apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) diff -r 0384e039b7f2 -r e121ac0028f8 LFex.thy --- a/LFex.thy Sun Dec 06 00:13:35 2009 +0100 +++ b/LFex.thy Sun Dec 06 00:19:45 2009 +0100 @@ -220,6 +220,7 @@ val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM} val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps} val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quot + val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quot *} lemma @@ -256,12 +257,11 @@ ((x5 :: TRM) = x6 \ P3 x5 x6)" using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 apply - -apply(tactic {* lift_tac @{context} @{thm akind_aty_atrm.induct} @{thms alpha_equivps} 1 *}) -(*apply(tactic {* regularize_tac @{context} @{thms alpha_equivps} 1 *}) +apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) +apply(tactic {* regularize_tac @{context} @{thms alpha_equivps} 1 *}) apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) +apply(fold perm_kind_def perm_ty_def perm_trm_def FV_ty_def[simplified id_simps] FV_kind_def[simplified id_simps] FV_trm_def[simplified id_simps]) apply(tactic {* clean_tac @{context} 1 *}) -*) -(*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*) (* Profiling: ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} @@ -270,8 +270,6 @@ ML_prf {* PolyML.profiling 1 *} ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} *) -apply(unfold perm_kind_def perm_ty_def perm_trm_def) -apply(tactic {* clean_tac @{context} 1 *}) done (* Does not work: diff -r 0384e039b7f2 -r e121ac0028f8 LamEx.thy --- a/LamEx.thy Sun Dec 06 00:13:35 2009 +0100 +++ b/LamEx.thy Sun Dec 06 00:19:45 2009 +0100 @@ -190,14 +190,20 @@ lemma fv_var: "fv (Var (a\name)) = {a}" apply (tactic {* lift_tac_lam @{context} @{thm rfv_var} 1 *}) +apply (unfold fv_def[simplified id_simps]) +apply (tactic {* clean_tac @{context} 1 *}) done lemma fv_app: "fv (App (x\lam) (xa\lam)) = fv x \ fv xa" apply (tactic {* lift_tac_lam @{context} @{thm rfv_app} 1 *}) +apply (unfold fv_def[simplified id_simps]) +apply (tactic {* clean_tac @{context} 1 *}) done lemma fv_lam: "fv (Lam (a\name) (x\lam)) = fv x - {a}" apply (tactic {* lift_tac_lam @{context} @{thm rfv_lam} 1 *}) +apply (unfold fv_def[simplified id_simps]) +apply (tactic {* clean_tac @{context} 1 *}) done lemma a1: "(a\name) = (b\name) \ Var a = Var b" @@ -210,6 +216,8 @@ lemma a3: "\(x\lam) = [(a\name, b\name)] \ (xa\lam); a \ fv (Lam b x)\ \ Lam a x = Lam b xa" apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *}) +apply (unfold fv_def[simplified id_simps]) +apply (tactic {* clean_tac @{context} 1 *}) done lemma alpha_cases: "\a1 = a2; \a b. \a1 = Var a; a2 = Var b; a = b\ \ P; @@ -217,6 +225,8 @@ \x a b xa. \a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \ xa; a \ fv (Lam b x)\ \ P\ \ P" apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *}) +apply (unfold fv_def[simplified id_simps]) +apply (tactic {* clean_tac @{context} 1 *}) done lemma alpha_induct: "\(qx\lam) = (qxa\lam); \(a\name) b\name. a = b \ (qxb\lam \ lam \ bool) (Var a) (Var b); @@ -225,6 +235,8 @@ \x = [(a, b)] \ xa; qxb x ([(a, b)] \ xa); a \ fv (Lam b x)\ \ qxb (Lam a x) (Lam b xa)\ \ qxb qx qxa" apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *}) +apply (unfold fv_def[simplified id_simps]) +apply (tactic {* clean_tac @{context} 1 *}) done lemma var_inject: "(Var a = Var b) = (a = b)" diff -r 0384e039b7f2 -r e121ac0028f8 QuotList.thy --- a/QuotList.thy Sun Dec 06 00:13:35 2009 +0100 +++ b/QuotList.thy Sun Dec 06 00:19:45 2009 +0100 @@ -84,10 +84,22 @@ shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) -(* We need an ho version *) lemma map_rsp: assumes q1: "Quotient R1 Abs1 Rep1" and q2: "Quotient R2 Abs2 Rep2" + shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" +apply(simp) +apply(rule allI)+ +apply(rule impI) +apply(rule allI)+ +apply (induct_tac xa ya rule: list_induct2') +apply simp_all +done + +(* TODO: if the above is correct, we can remove this one *) +lemma map_rsp_lo: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" and a: "(R1 ===> R2) f1 f2" and b: "list_rel R1 l1 l2" shows "list_rel R2 (map f1 l1) (map f2 l2)" @@ -106,8 +118,35 @@ shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) +lemma list_rel_empty: "list_rel R [] b \ length b = 0" +by (induct b) (simp_all) +lemma list_rel_len: "list_rel R a b \ length a = length b" +apply (induct a arbitrary: b) +apply (simp add: list_rel_empty) +apply (case_tac b) +apply simp_all +done +(* TODO: induct_tac doesn't accept 'arbitrary'. + induct doesn't accept 'rule'. + that's why the proof uses manual generalisation and needs assumptions + both in conclusion for induction and in assumptions. *) +lemma foldl_rsp: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" +apply auto +apply (subgoal_tac "R1 xa ya \ list_rel R2 xb yb \ R1 (foldl x xa xb) (foldl y ya yb)") +apply simp +apply (rule_tac x="xa" in spec) +apply (rule_tac x="ya" in spec) +apply (rule_tac xs="xb" and ys="yb" in list_induct2) +apply (rule list_rel_len) +apply (simp_all) +done + +(* TODO: foldr_rsp should be similar *) diff -r 0384e039b7f2 -r e121ac0028f8 QuotMain.thy --- a/QuotMain.thy Sun Dec 06 00:13:35 2009 +0100 +++ b/QuotMain.thy Sun Dec 06 00:19:45 2009 +0100 @@ -149,7 +149,7 @@ fun_quotient list_quotient lemmas [quotient_rsp] = - quot_rel_rsp nil_rsp cons_rsp + quot_rel_rsp nil_rsp cons_rsp foldl_rsp ML {* maps_lookup @{theory} "List.list" *} ML {* maps_lookup @{theory} "*" *} @@ -1110,11 +1110,10 @@ fun clean_tac lthy = let val thy = ProofContext.theory_of lthy; - val defs = map (Thm.varifyT o #def) (qconsts_dest thy) - val thms1 = @{thms all_prs ex_prs} + val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) + val thms1 = @{thms all_prs ex_prs} @ defs val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} - @ defs fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver (* FIXME: use of someting smaller than HOL_basic_ss *) in