diff -r 4b0563bc4b03 -r 7d8949da7d99 Nominal/LFex.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/LFex.thy Thu Feb 25 07:48:33 2010 +0100 @@ -0,0 +1,236 @@ +theory LFex +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" +begin + +atom_decl name +atom_decl ident + +datatype rkind = + Type + | KPi "rty" "name" "rkind" +and rty = + TConst "ident" + | TApp "rty" "rtrm" + | TPi "rty" "name" "rty" +and rtrm = + Const "ident" + | Var "name" + | App "rtrm" "rtrm" + | Lam "rty" "name" "rtrm" + + +setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *} + +local_setup {* + snd o define_fv_alpha "LFex.rkind" + [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], + [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], + [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *} +notation + alpha_rkind ("_ \ki _" [100, 100] 100) +and alpha_rty ("_ \ty _" [100, 100] 100) +and alpha_rtrm ("_ \tr _" [100, 100] 100) +thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_rkind_alpha_rty_alpha_rtrm_inj}, []), (build_alpha_inj @{thms alpha_rkind_alpha_rty_alpha_rtrm.intros} @{thms rkind.distinct rty.distinct rtrm.distinct rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} ctxt)) ctxt)) *} +thm alpha_rkind_alpha_rty_alpha_rtrm_inj + +lemma rfv_eqvt[eqvt]: + "((pi\fv_rkind t1) = fv_rkind (pi\t1))" + "((pi\fv_rty t2) = fv_rty (pi\t2))" + "((pi\fv_rtrm t3) = fv_rtrm (pi\t3))" +apply(induct t1 and t2 and t3 rule: rkind_rty_rtrm.inducts) +apply(simp_all add: union_eqvt Diff_eqvt) +apply(simp_all add: permute_set_eq atom_eqvt) +done + +lemma alpha_eqvt: + "t1 \ki s1 \ (pi \ t1) \ki (pi \ s1)" + "t2 \ty s2 \ (pi \ t2) \ty (pi \ s2)" + "t3 \tr s3 \ (pi \ t3) \tr (pi \ s3)" +apply(induct rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts) +apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros) +apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj) +apply (rule alpha_gen_atom_eqvt) +apply (simp add: rfv_eqvt) +apply assumption +apply (rule alpha_gen_atom_eqvt) +apply (simp add: rfv_eqvt) +apply assumption +apply (rule alpha_gen_atom_eqvt) +apply (simp add: rfv_eqvt) +apply assumption +done + +local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []), + (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}] + @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} + @{thms rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj} + @{thms rkind.distinct rty.distinct rtrm.distinct} + @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} + @{thms alpha_eqvt} ctxt)) ctxt)) *} +thm alpha_equivps + +local_setup {* define_quotient_type + [(([], @{binding kind}, NoSyn), (@{typ rkind}, @{term alpha_rkind})), + (([], @{binding ty}, NoSyn), (@{typ rty}, @{term alpha_rty} )), + (([], @{binding trm}, NoSyn), (@{typ rtrm}, @{term alpha_rtrm} ))] + (ALLGOALS (resolve_tac @{thms alpha_equivps})) +*} + +local_setup {* +(fn ctxt => ctxt + |> snd o (Quotient_Def.quotient_lift_const ("TYP", @{term Type})) + |> snd o (Quotient_Def.quotient_lift_const ("KPI", @{term KPi})) + |> snd o (Quotient_Def.quotient_lift_const ("TCONST", @{term TConst})) + |> snd o (Quotient_Def.quotient_lift_const ("TAPP", @{term TApp})) + |> snd o (Quotient_Def.quotient_lift_const ("TPI", @{term TPi})) + |> snd o (Quotient_Def.quotient_lift_const ("CONS", @{term Const})) + |> snd o (Quotient_Def.quotient_lift_const ("VAR", @{term Var})) + |> snd o (Quotient_Def.quotient_lift_const ("APP", @{term App})) + |> snd o (Quotient_Def.quotient_lift_const ("LAM", @{term Lam})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_kind", @{term fv_rkind})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_ty", @{term fv_rty})) + |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *} +print_theorems + +local_setup {* prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}] + (fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *} +local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \ rkind \ rkind"}] + (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *} +local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \ rty \ rty"}] + (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *} +local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \ rtrm \ rtrm"}] + (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *} +ML {* fun const_rsp_tac _ = constr_rsp_tac @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj} + @{thms rfv_rsp} @{thms alpha_equivps} 1 *} +local_setup {* prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *} +local_setup {* prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *} +local_setup {* prove_const_rsp Binding.empty [@{term Var}] const_rsp_tac *} +local_setup {* prove_const_rsp Binding.empty [@{term App}] const_rsp_tac *} +local_setup {* prove_const_rsp Binding.empty [@{term Const}] const_rsp_tac *} +local_setup {* prove_const_rsp Binding.empty [@{term KPi}] const_rsp_tac *} +local_setup {* prove_const_rsp Binding.empty [@{term TPi}] const_rsp_tac *} +local_setup {* prove_const_rsp Binding.empty [@{term Lam}] const_rsp_tac *} + +lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted] + +thm rkind_rty_rtrm.inducts +lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted] + +instantiation kind and ty and trm :: pt +begin + +quotient_definition + "permute_kind :: perm \ kind \ kind" +is + "permute :: perm \ rkind \ rkind" + +quotient_definition + "permute_ty :: perm \ ty \ ty" +is + "permute :: perm \ rty \ rty" + +quotient_definition + "permute_trm :: perm \ trm \ trm" +is + "permute :: perm \ rtrm \ rtrm" + +instance by default (simp_all add: + permute_rkind_permute_rty_permute_rtrm_zero[quot_lifted] + permute_rkind_permute_rty_permute_rtrm_append[quot_lifted]) + +end + +(* +Lifts, but slow and not needed?. +lemmas alpha_kind_alpha_ty_alpha_trm_induct = alpha_rkind_alpha_rty_alpha_rtrm.induct[unfolded alpha_gen, quot_lifted, folded alpha_gen] +*) + +lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted] + +lemmas kind_ty_trm_inj = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] + +lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted] + +lemmas fv_eqvt = rfv_eqvt[quot_lifted] + +lemma supports: + "{} supports TYP" + "(supp (atom i)) supports (TCONST i)" + "(supp A \ supp M) supports (TAPP A M)" + "(supp (atom i)) supports (CONS i)" + "(supp (atom x)) supports (VAR x)" + "(supp M \ supp N) supports (APP M N)" + "(supp ty \ supp (atom na) \ supp ki) supports (KPI ty na ki)" + "(supp ty \ supp (atom na) \ supp ty2) supports (TPI ty na ty2)" + "(supp ty \ supp (atom na) \ supp trm) supports (LAM ty na trm)" +apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh) +apply(rule_tac [!] allI)+ +apply(rule_tac [!] impI) +apply(tactic {* ALLGOALS (REPEAT o etac conjE) *}) +apply(simp_all add: fresh_atom) +done + +lemma kind_ty_trm_fs: + "finite (supp (x\kind))" + "finite (supp (y\ty))" + "finite (supp (z\trm))" +apply(induct x and y and z rule: kind_ty_trm_inducts) +apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *}) +apply(simp_all add: supp_atom) +done + +instance kind and ty and trm :: fs +apply(default) +apply(simp_all only: kind_ty_trm_fs) +done + +lemma supp_eqs: + "supp TYP = {}" + "supp rkind = fv_kind rkind \ supp (KPI rty name rkind) = supp rty \ supp (Abs {atom name} rkind)" + "supp (TCONST i) = {atom i}" + "supp (TAPP A M) = supp A \ supp M" + "supp rty2 = fv_ty rty2 \ supp (TPI rty1 name rty2) = supp rty1 \ supp (Abs {atom name} rty2)" + "supp (CONS i) = {atom i}" + "supp (VAR x) = {atom x}" + "supp (APP M N) = supp M \ supp N" + "supp rtrm = fv_trm rtrm \ supp (LAM rty name rtrm) = supp rty \ supp (Abs {atom name} rtrm)" + apply(simp_all (no_asm) add: supp_def) + apply(simp_all only: kind_ty_trm_inj Abs_eq_iff alpha_gen) + apply(simp_all only: insert_eqvt empty_eqvt atom_eqvt supp_eqvt[symmetric] fv_eqvt[symmetric]) + apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Set.Un_commute) + apply(simp_all add: supp_at_base[simplified supp_def]) + done + +lemma supp_fv: + "supp t1 = fv_kind t1" + "supp t2 = fv_ty t2" + "supp t3 = fv_trm t3" + apply(induct t1 and t2 and t3 rule: kind_ty_trm_inducts) + apply(simp_all (no_asm) only: supp_eqs fv_kind_ty_trm) + apply(simp_all) + apply(subst supp_eqs) + apply(simp_all add: supp_Abs) + apply(subst supp_eqs) + apply(simp_all add: supp_Abs) + apply(subst supp_eqs) + apply(simp_all add: supp_Abs) + done + +lemma supp_rkind_rty_rtrm: + "supp TYP = {}" + "supp (KPI A x K) = supp A \ (supp K - {atom x})" + "supp (TCONST i) = {atom i}" + "supp (TAPP A M) = supp A \ supp M" + "supp (TPI A x B) = supp A \ (supp B - {atom x})" + "supp (CONS i) = {atom i}" + "supp (VAR x) = {atom x}" + "supp (APP M N) = supp M \ supp N" + "supp (LAM A x M) = supp A \ (supp M - {atom x})" + by (simp_all only: supp_fv fv_kind_ty_trm) + +end + + + +