diff -r 39e687a99549 -r 2e2a3cd58f64 Nominal/LFex.thy --- a/Nominal/LFex.thy Fri Mar 05 14:56:19 2010 +0100 +++ b/Nominal/LFex.thy Fri Mar 05 17:09:48 2010 +0100 @@ -1,143 +1,36 @@ theory LFex -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" +imports "Parser" begin atom_decl name atom_decl ident -datatype rkind = +ML {* restricted_nominal := false *} + +nominal_datatype kind = Type - | KPi "rty" "name" "rkind" -and rty = + | KPi "ty" n::"name" k::"kind" bind n in k +and ty = TConst "ident" - | TApp "rty" "rtrm" - | TPi "rty" "name" "rty" -and rtrm = + | TApp "ty" "trm" + | TPi "ty" n::"name" t::"ty" bind n in t +and trm = Const "ident" | Var "name" - | App "rtrm" "rtrm" - | Lam "rty" "name" "rtrm" - - -setup {* snd o define_raw_perms (Datatype.the_info @{theory} "LFex.rkind") 3 *} -print_theorems - -local_setup {* - snd o define_fv_alpha (Datatype.the_info @{theory} "LFex.rkind") - [[ [], [(NONE, 1, 2)]], - [ [], [], [(NONE, 1, 2)] ], - [ [], [], [], [(NONE, 1, 2)]]] *} -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 \ (p \ t1) \ki (p \ s1)) \ - (t2 \ty s2 \ (p \ t2) \ty (p \ s2)) \ - (t3 \tr s3 \ (p \ t3) \tr (p \ s3))" -apply(rule alpha_rkind_alpha_rty_alpha_rtrm.induct) -apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj) -apply (erule_tac [!] conjE)+ -apply (erule_tac [!] exi[of _ _ "p"]) -apply (erule_tac [!] alpha_gen_compose_eqvt) -apply (simp_all add: rfv_eqvt eqvts atom_eqvt) -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 {* snd o 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 {* snd o prove_const_rsp Binding.empty [@{term "permute :: perm \ rkind \ rkind"}, @{term "permute :: perm \ rty \ rty"}, @{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 {* snd o prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *} -local_setup {* snd o prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *} -local_setup {* snd o prove_const_rsp Binding.empty [@{term Var}] const_rsp_tac *} -local_setup {* snd o prove_const_rsp Binding.empty [@{term App}] const_rsp_tac *} -local_setup {* snd o prove_const_rsp Binding.empty [@{term Const}] const_rsp_tac *} -local_setup {* snd o prove_const_rsp Binding.empty [@{term KPi}] const_rsp_tac *} -local_setup {* snd o prove_const_rsp Binding.empty [@{term TPi}] const_rsp_tac *} -local_setup {* snd o 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] - -setup {* define_lifted_perms ["LFex.kind", "LFex.ty", "LFex.trm"] - [("permute_kind", @{term "permute :: perm \ rkind \ rkind"}), - ("permute_ty", @{term "permute :: perm \ rty \ rty"}), - ("permute_trm", @{term "permute :: perm \ rtrm \ rtrm"})] - @{thms permute_rkind_permute_rty_permute_rtrm_zero permute_rkind_permute_rty_permute_rtrm_append} *} - -(* -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] + | App "trm" "trm" + | Lam "ty" n::"name" t::"trm" bind n in t 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) + "{} supports Type" + "(supp (atom i)) supports (TConst i)" + "(supp A \ supp M) supports (TApp A M)" + "(supp (atom i)) supports (Const 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 kind_ty_trm_perm) apply(rule_tac [!] allI)+ apply(rule_tac [!] impI) apply(tactic {* ALLGOALS (REPEAT o etac conjE) *}) @@ -145,10 +38,8 @@ 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) + "finite (supp (x\kind)) \ finite (supp (y\ty)) \ finite (supp (z\trm))" +apply(induct rule: kind_ty_trm_induct) apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *}) apply(simp_all add: supp_atom) done @@ -166,51 +57,49 @@ apply (blast)+ done +lemma Collect_neg_conj: "{x. \(P x \ Q x)} = {x. \(P x)} \ {x. \(Q x)}" +by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) + 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 permute_set_eq atom_eqvt) - apply(simp_all only: kind_ty_trm_inj Abs_eq_iff alpha_gen) - apply(simp_all only:ex_out) - apply(simp_all only: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts[symmetric]) - apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric]) - apply(simp_all add: supp_at_base[simplified supp_def] Un_commute) + "supp Type = {}" + "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 (Const 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 permute_set_eq atom_eqvt kind_ty_trm_perm) + apply(simp_all only: kind_ty_trm_inject Abs_eq_iff alpha_gen) + apply(simp_all only: ex_out) + apply(simp_all only: eqvts[symmetric]) + apply(simp_all only: Collect_neg_conj) + apply(simp_all only: supp_at_base[simplified supp_def] Un_commute Un_assoc) + apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Un_commute Un_assoc) + apply(simp_all add: Un_left_commute) 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) + "supp t1 = fv_kind t1 \ supp t2 = fv_ty t2 \ supp t3 = fv_trm t3" + apply(induct rule: kind_ty_trm_induct) + apply(simp_all (no_asm) only: supp_eqs kind_ty_trm_fv) 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_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) + "supp Type = {}" + "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 (Const 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})" +apply (simp_all add: supp_fv kind_ty_trm_fv) end