# HG changeset patch # User Christian Urban # Date 1271339798 -7200 # Node ID d744b157dd2ac0615d2bcbb33eb5254410a8cce6 # Parent 591cc76da570dc733dc8961a53b4fafde017098a# Parent c8e406f64db081ed302ed85022309568c43a54cd merged diff -r 591cc76da570 -r d744b157dd2a Attic/Quot/Examples/FSet3.thy --- a/Attic/Quot/Examples/FSet3.thy Thu Apr 15 15:56:21 2010 +0200 +++ b/Attic/Quot/Examples/FSet3.thy Thu Apr 15 15:56:38 2010 +0200 @@ -72,9 +72,13 @@ shows "[] \ []" by simp -lemma cons_rsp[quot_respect]: +lemma cons_rsp: + "xa \ ya \ y # xa \ y # ya" + by simp + +lemma [quot_respect]: shows "(op = ===> op \ ===> op \) op # op #" -by simp + by simp section {* Augmenting a set -- @{const finsert} *} @@ -257,11 +261,11 @@ lemma concat2: shows "concat (x # xs) \ x @ concat xs" -by (simp add: id_simps) +by (simp) lemma concat_rsp[quot_respect]: shows "(list_rel op \ OOO op \ ===> op \) concat concat" -sorry + sorry lemma nil_rsp2[quot_respect]: "(list_rel op \ OOO op \) [] []" apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros) @@ -344,25 +348,31 @@ apply (metis equivp_def fset_equivp) apply rule apply rule - apply(rule quotient_compose_list_pre) + apply (rule quotient_compose_list_pre) done lemma fconcat_empty: shows "fconcat {||} = {||}" -apply(lifting concat1) -apply(cleaning) -apply(simp add: comp_def) -apply(fold fempty_def[simplified id_simps]) -apply(rule refl) -done + apply(lifting concat1) + apply(cleaning) + apply(simp add: comp_def) + apply(fold fempty_def[simplified id_simps]) + apply(rule refl) + done (* Should be true *) lemma insert_rsp2[quot_respect]: "(op \ ===> list_rel op \ OOO op \ ===> list_rel op \ OOO op \) op # op #" -apply auto -apply (simp add: set_in_eq) -sorry + apply auto + apply (simp add: set_in_eq) + apply (rule_tac b="x # b" in pred_compI) + apply auto + apply (rule_tac b="x # ba" in pred_compI) + apply (rule cons_rsp) + apply simp + apply (auto)[1] + done lemma append_rsp[quot_respect]: "(op \ ===> op \ ===> op \) op @ op @" @@ -370,11 +380,11 @@ lemma fconcat_insert: shows "fconcat (finsert x S) = x |\| fconcat S" -apply(lifting concat2) -apply(cleaning) -apply (simp add: finsert_def fconcat_def comp_def) -apply cleaning -done + apply(lifting concat2) + apply(cleaning) + apply (simp add: finsert_def fconcat_def comp_def) + apply cleaning + done text {* raw section *} diff -r 591cc76da570 -r d744b157dd2a Nominal/Manual/Term4.thy --- a/Nominal/Manual/Term4.thy Thu Apr 15 15:56:21 2010 +0200 +++ b/Nominal/Manual/Term4.thy Thu Apr 15 15:56:38 2010 +0200 @@ -1,5 +1,5 @@ theory Term4 -imports "../Abs" "../Perm" "../Fv" "../Rsp" "Quotient_List" +imports "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "Quotient_List" begin atom_decl name @@ -29,8 +29,8 @@ thm permute_rtrm4_permute_rtrm4_list.simps thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] -local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4") - [[[], [], [(NONE, 0,1)]], [[], []] ] *} +local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term4.rtrm4") + [[[], [], [(NONE, 0, 1, AlphaGen)]], [[], []] ] [] *} print_theorems lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4" @@ -54,34 +54,29 @@ alpha_rtrm4_list ("_ \4l _" [100, 100] 100) thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2] -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *} +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *} thm alpha4_inj -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} thm alpha4_inj_no -local_setup {* -snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \ rtrm4 \ rtrm4"},@{term "permute :: perm \ rtrm4 list \ rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct} -*} -print_theorems +local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] fv_rtrm4_fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *} +thm eqvts(1-2) local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt_no}, []), - build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \ rtrm4 \ rtrm4"},@{term "permute :: perm \ rtrm4 list \ rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj_no} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt)) + build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj_no} ctxt 1) ctxt) ctxt)) *} lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2] -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []), - (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *} -lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2] +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []), + build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj_no} ctxt) ctxt)) *} +thm alpha4_reflp +ML build_equivps -(*lemma fv_rtrm4_rsp: - "xa \4 ya \ fv_rtrm4 xa = fv_rtrm4 ya" - "x \4l y \ fv_rtrm4_list x = fv_rtrm4_list y" - apply (induct rule: alpha_rtrm4_alpha_rtrm4_list.inducts) - apply (simp_all add: alpha_gen) -done*) - +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []), + (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *} +lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2] quotient_type trm4 = rtrm4 / alpha_rtrm4 @@ -91,31 +86,84 @@ local_setup {* (fn ctxt => ctxt - |> snd o (Quotient_Def.quotient_lift_const ("Vr4", @{term rVr4})) - |> snd o (Quotient_Def.quotient_lift_const ("Ap4", @{term rAp4})) - |> snd o (Quotient_Def.quotient_lift_const ("Lm4", @{term rLm4}))) + |> snd o (Quotient_Def.quotient_lift_const [] ("Vr4", @{term rVr4})) + |> snd o (Quotient_Def.quotient_lift_const [@{typ "trm4"}] ("Ap4", @{term rAp4})) + |> snd o (Quotient_Def.quotient_lift_const [] ("Lm4", @{term rLm4})) + |> snd o (Quotient_Def.quotient_lift_const [] ("fv_trm4", @{term fv_rtrm4}))) *} print_theorems -local_setup {* snd o prove_const_rsp @{binding fv_rtrm4_rsp} [@{term fv_rtrm4}] - (fn _ => fvbv_rsp_tac @{thm alpha_rtrm4_alpha_rtrm4_list.inducts(1)} @{thms fv_rtrm4_fv_rtrm4_list.simps} 1) *} + + +lemma fv_rtrm4_rsp: + "xa \4 ya \ fv_rtrm4 xa = fv_rtrm4 ya" + "x \4l y \ fv_rtrm4_list x = fv_rtrm4_list y" + apply (induct rule: alpha_rtrm4_alpha_rtrm4_list.inducts) + apply (simp_all add: alpha_gen) +done + +local_setup {* snd o prove_const_rsp [] @{binding fv_rtrm4_rsp'} [@{term fv_rtrm4}] + (fn _ => asm_full_simp_tac (@{simpset} addsimps @{thms fv_rtrm4_rsp}) 1) *} +print_theorems + +ML constr_rsp_tac + +local_setup {* snd o prove_const_rsp [] @{binding rVr4_rsp} [@{term rVr4}] + (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *} +local_setup {* snd o prove_const_rsp [] @{binding rLm4_rsp} [@{term rLm4}] + (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *} + +lemma [quot_respect]: + "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4" + by (simp add: alpha4_inj) + +(* Maybe also need: @{term "permute :: perm \ rtrm4 list \ rtrm4 list"} *) +local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp} + [@{term "permute :: perm \ rtrm4 \ rtrm4"}] + (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *} print_theorems -local_setup {* snd o prove_const_rsp @{binding rVr4_rsp} [@{term rVr4}] - (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *} -lemma "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4" -apply simp -apply clarify -apply (simp add: alpha4_inj) +lemma list_rel_rsp: + "\\x y. R x y \ (\a b. R a b \ S x a = T y b); list_rel R x y; list_rel R a b\ + \ list_rel S x a = list_rel T y b" + sorry + +lemma[quot_respect]: + "((R ===> R ===> op =) ===> list_rel R ===> list_rel R ===> op =) list_rel list_rel" + by (simp add: list_rel_rsp) +lemma[quot_preserve]: + assumes a: "Quotient R abs1 rep1" + shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_rel = list_rel" + apply (simp add: expand_fun_eq) + apply clarify + apply (induct_tac xa xb rule: list_induct2') + apply (simp_all add: Quotient_abs_rep[OF a]) + done -local_setup {* snd o prove_const_rsp @{binding rLm4_rsp} [@{term rLm4}] - (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *} -local_setup {* snd o prove_const_rsp @{binding permute_rtrm4_rsp} - [@{term "permute :: perm \ rtrm4 \ rtrm4"}, @{term "permute :: perm \ rtrm4 list \ rtrm4 list"}] - (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *} +lemma[quot_preserve]: + assumes a: "Quotient R abs1 rep1" + shows "(list_rel ((rep1 ---> rep1 ---> id) R) l m) = (l = m)" + by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a]) + +lemma bla: "(Ap4 trm4 list = Ap4 trm4a lista) = + (trm4 = trm4a \ list_rel (op =) list lista)" + by (lifting alpha4_inj(2)) + +thm bla[simplified list_rel_eq] -thm rtrm4.induct -lemmas trm1_bp_induct = rtrm4.induct[quot_lifted] +lemma " (Lm4 name rtrm4 = Lm4 namea rtrm4a) = + (\pi\perm. + fv_trm4 rtrm4 - {atom name} = fv_trm4 rtrm4a - {atom namea} \ + (fv_trm4 rtrm4 - {atom name}) \* pi \ + pi \ rtrm4 = rtrm4a \ pi \ {atom name} = {atom namea})" + +ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(1)} *} +ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(2)} *} +ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(3)[unfolded alpha_gen]} *} +ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *} +. + +(*lemmas trm1_bp_induct = rtrm4.induct[quot_lifted]*) end