diff -r 89715c48f728 -r f5057aabf5c0 Nominal/Manual/Term5.thy --- a/Nominal/Manual/Term5.thy Sat May 12 22:21:25 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,302 +0,0 @@ -theory Term5 -imports "../Nominal2_Atoms" "../Nominal2_Eqvt" "../Nominal2_Supp" "../Abs" "../Perm" "../Fv" "../Rsp" -begin - -atom_decl name - -datatype rtrm5 = - rVr5 "name" -| rAp5 "rtrm5" "rtrm5" -| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" -and rlts = - rLnil -| rLcons "name" "rtrm5" "rlts" - -primrec - rbv5 -where - "rbv5 rLnil = {}" -| "rbv5 (rLcons n t ltl) = {atom n} \ (rbv5 ltl)" - - -setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *} -print_theorems - -local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") - [[[], [], [(SOME (@{term rbv5}, true), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [(0,NONE), (2,SOME @{term rbv5})]])] *} -print_theorems - -notation - alpha_rtrm5 ("_ \5 _" [100, 100] 100) and - alpha_rlts ("_ \l _" [100, 100] 100) -thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_rel_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *} -thm alpha5_inj - -lemma rbv5_eqvt[eqvt]: - "pi \ (rbv5 x) = rbv5 (pi \ x)" - apply (induct x) - apply (simp_all add: eqvts atom_eqvt) - done - -lemma fv_rtrm5_rlts_eqvt[eqvt]: - "pi \ (fv_rtrm5 x) = fv_rtrm5 (pi \ x)" - "pi \ (fv_rlts l) = fv_rlts (pi \ l)" - apply (induct x and l) - apply (simp_all add: eqvts atom_eqvt) - done - -(*lemma alpha5_eqvt: - "(xa \5 y \ (p \ xa) \5 (p \ y)) \ - (xb \l ya \ (p \ xb) \l (p \ ya)) \ - (alpha_rbv5 b c \ alpha_rbv5 (p \ b) (p \ c))" -apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *}) -done*) - -local_setup {* -(fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []), -build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *} -print_theorems - -lemma alpha5_reflp: -"y \5 y \ (x \l x \ alpha_rbv5 x x)" -apply (rule rtrm5_rlts.induct) -apply (simp_all add: alpha5_inj) -apply (rule_tac x="0::perm" in exI) -apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm) -done - -lemma alpha5_symp: -"(a \5 b \ b \5 a) \ -(x \l y \ y \l x) \ -(alpha_rbv5 x y \ alpha_rbv5 y x)" -apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) -apply (simp_all add: alpha5_inj) -apply (erule exE) -apply (rule_tac x="-pi" in exI) -apply (rule alpha_gen_sym) -apply (simp_all add: alphas) -apply (case_tac x) -apply (case_tac y) -apply (simp add: alpha5_eqvt) -apply clarify -apply simp -done - -lemma alpha5_symp1: -"(a \5 b \ b \5 a) \ -(x \l y \ y \l x) \ -(alpha_rbv5 x y \ alpha_rbv5 y x)" -apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) -apply (simp_all add: alpha5_inj) -apply (erule exE) -apply (rule_tac x="- pi" in exI) -apply (simp add: alpha_gen) - apply(simp add: fresh_star_def fresh_minus_perm) -apply clarify -apply (rule conjI) -apply (rotate_tac 3) -apply (frule_tac p="- pi" in alpha5_eqvt(2)) -apply simp -apply (rule conjI) -apply (rotate_tac 5) -apply (frule_tac p="- pi" in alpha5_eqvt(1)) -apply simp -apply (rotate_tac 6) -apply simp -apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1]) -apply (simp) -done - -thm alpha_gen_sym[no_vars] -thm alpha_gen_compose_sym[no_vars] - -lemma tt: - "\R (- p \ x) y \ R (p \ y) x; (bs, x) \gen R f (- p) (cs, y)\ \ (cs, y) \gen R f p (bs, x)" - unfolding alphas - unfolding fresh_star_def - by (auto simp add: fresh_minus_perm) - -lemma alpha5_symp2: - shows "a \5 b \ b \5 a" - and "x \l y \ y \l x" - and "alpha_rbv5 x y \ alpha_rbv5 y x" -apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) -(* non-binding case *) -apply(simp add: alpha5_inj) -(* non-binding case *) -apply(simp add: alpha5_inj) -(* binding case *) -apply(simp add: alpha5_inj) -apply(erule exE) -apply(rule_tac x="- pi" in exI) -apply(rule tt) -apply(simp add: alphas) -apply(erule conjE)+ -apply(drule_tac p="- pi" in alpha5_eqvt(2)) -apply(drule_tac p="- pi" in alpha5_eqvt(2)) -apply(drule_tac p="- pi" in alpha5_eqvt(1)) -apply(drule_tac p="- pi" in alpha5_eqvt(1)) -apply(simp) -apply(simp add: alphas) -apply(erule conjE)+ -apply metis -(* non-binding case *) -apply(simp add: alpha5_inj) -(* non-binding case *) -apply(simp add: alpha5_inj) -(* non-binding case *) -apply(simp add: alpha5_inj) -(* non-binding case *) -apply(simp add: alpha5_inj) -done - -lemma alpha5_transp: -"(a \5 b \ (\c. b \5 c \ a \5 c)) \ -(x \l y \ (\z. y \l z \ x \l z)) \ -(alpha_rbv5 k l \ (\m. alpha_rbv5 l m \ alpha_rbv5 k m))" -(*apply (tactic {* transp_tac @{context} @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} [] @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{thms alpha5_eqvt} 1 *})*) -apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) -apply (rule_tac [!] allI) -apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) -apply (simp_all add: alpha5_inj) -apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) -apply (simp_all add: alpha5_inj) -apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) -apply (simp_all add: alpha5_inj) -defer -apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) -apply (simp_all add: alpha5_inj) -apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *}) -apply (simp_all add: alpha5_inj) -apply (tactic {* eetac @{thm exi_sum} @{context} 1 *}) -(* HERE *) -(* -apply(rule alpha_gen_trans) -thm alpha_gen_trans -defer -apply (simp add: alpha_gen) -apply clarify -apply(simp add: fresh_star_plus) -apply (rule conjI) -apply (erule_tac x="- pi \ rltsaa" in allE) -apply (rotate_tac 5) -apply (drule_tac p="- pi" in alpha5_eqvt(2)) -apply simp -apply (drule_tac p="pi" in alpha5_eqvt(2)) -apply simp -apply (erule_tac x="- pi \ rtrm5aa" in allE) -apply (rotate_tac 7) -apply (drule_tac p="- pi" in alpha5_eqvt(1)) -apply simp -apply (rotate_tac 3) -apply (drule_tac p="pi" in alpha5_eqvt(1)) -apply simp -done -*) -sorry - -lemma alpha5_equivp: - "equivp alpha_rtrm5" - "equivp alpha_rlts" - unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def - apply (simp_all only: alpha5_reflp) - apply (meson alpha5_symp alpha5_transp) - apply (meson alpha5_symp alpha5_transp) - done - -quotient_type - trm5 = rtrm5 / alpha_rtrm5 -and - lts = rlts / alpha_rlts - by (auto intro: alpha5_equivp) - -local_setup {* -(fn ctxt => ctxt - |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5})) - |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5})) - |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) - |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) - |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) - |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})) - |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5}))) -*} -print_theorems - -lemma alpha5_rfv: - "(t \5 s \ fv_rtrm5 t = fv_rtrm5 s)" - "(l \l m \ fv_rlts l = fv_rlts m)" - "(alpha_rbv5 b c \ True)" - apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) - apply(simp_all add: eqvts) - apply(simp add: alpha_gen) - apply(clarify) - apply blast -done - -lemma bv_list_rsp: - shows "x \l y \ rbv5 x = rbv5 y" - apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2)) - apply(simp_all) - apply(clarify) - apply simp - done - -local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *} -print_theorems - -local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms rtrm5.exhaust rlts.exhaust} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *} -thm alpha_bn_rsp - -lemma [quot_respect]: - "(alpha_rlts ===> op =) fv_rlts fv_rlts" - "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" - "(alpha_rlts ===> op =) rbv5 rbv5" - "(op = ===> alpha_rtrm5) rVr5 rVr5" - "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" - "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" - "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" - "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" - "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" - "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5" - apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_bn_rsp) - apply (clarify) - apply (rule_tac x="0" in exI) - apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) -done - - -lemma - shows "(alpha_rlts ===> op =) rbv5 rbv5" - by (simp add: bv_list_rsp) - -lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted] - -instantiation trm5 and lts :: pt -begin - -quotient_definition - "permute_trm5 :: perm \ trm5 \ trm5" -is - "permute :: perm \ rtrm5 \ rtrm5" - -quotient_definition - "permute_lts :: perm \ lts \ lts" -is - "permute :: perm \ rlts \ rlts" - -instance by default - (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted]) - -end - -lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] -lemmas bv5[simp] = rbv5.simps[quot_lifted] -lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] -lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen2, unfolded alpha_gen, quot_lifted, folded alpha_gen2, folded alpha_gen] -lemmas alpha5_DIS = alpha_dis[quot_lifted] - -end