diff -r 4b0563bc4b03 -r 7d8949da7d99 Quot/Nominal/LFex.thy --- a/Quot/Nominal/LFex.thy Wed Feb 24 17:32:43 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,236 +0,0 @@ -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 - - - -