diff -r a8627c3bdd0c -r cce1b6d1b761 Nominal/Term4.thy --- a/Nominal/Term4.thy Tue Mar 02 17:48:56 2010 +0100 +++ b/Nominal/Term4.thy Tue Mar 02 19:48:44 2010 +0100 @@ -1,5 +1,5 @@ theory Term4 -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" "Quotient_List" begin atom_decl name @@ -33,14 +33,32 @@ [[[], [], [(NONE, 0,1)]], [[], []] ] *} print_theorems +lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4" +apply (rule ext)+ +apply (induct_tac x xa rule: list_induct2') +apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros) +apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) +apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) +apply rule +apply (erule alpha_rtrm4_list.cases) +apply simp_all +apply (rule alpha_rtrm4_alpha_rtrm4_list.intros) +apply simp_all +done + +(* We need sth like: +lemma fix3: "fv_rtrm4_list = set o map fv_rtrm4" *) + notation alpha_rtrm4 ("_ \4 _" [100, 100] 100) and alpha_rtrm4_list ("_ \4l _" [100, 100] 100) -thm alpha_rtrm4_alpha_rtrm4_list.intros +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} @{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}, []), (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)) *} thm alpha4_inj -thm alpha_rtrm4_alpha_rtrm4_list.induct + +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)) *} +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} @@ -48,18 +66,56 @@ print_theorems local_setup {* -(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []), - 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} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt)) +(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)) +*} +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] + +(*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*) + + +quotient_type + trm4 = rtrm4 / alpha_rtrm4 +(*and + trm4list = "rtrm4 list" / alpha_rtrm4_list*) + by (simp_all add: alpha4_equivp) + +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}))) *} print_theorems -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []), - (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} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *} -thm alpha4_equivp +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) *} +print_theorems -quotient_type - qrtrm4 = rtrm4 / alpha_rtrm4 and - qrtrm4list = "rtrm4 list" / alpha_rtrm4_list - by (simp_all add: alpha4_equivp) +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) + + +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) *} + +thm rtrm4.induct +lemmas trm1_bp_induct = rtrm4.induct[quot_lifted] end