diff -r 11b8798dea5d -r 4b0563bc4b03 Quot/Nominal/LFex.thy --- a/Quot/Nominal/LFex.thy Wed Feb 24 17:32:22 2010 +0100 +++ b/Quot/Nominal/LFex.thy Wed Feb 24 17:32:43 2010 +0100 @@ -1,169 +1,45 @@ theory LFex -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" +imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" begin atom_decl name atom_decl ident -datatype kind = +datatype rkind = Type - | KPi "ty" "name" "kind" -and ty = + | KPi "rty" "name" "rkind" +and rty = TConst "ident" - | TApp "ty" "trm" - | TPi "ty" "name" "ty" -and trm = + | TApp "rty" "rtrm" + | TPi "rty" "name" "rty" +and rtrm = Const "ident" | Var "name" - | App "trm" "trm" - | Lam "ty" "name" "trm" - -instantiation kind and ty and trm :: pt -begin + | App "rtrm" "rtrm" + | Lam "rty" "name" "rtrm" -primrec - permute_kind -and permute_ty -and permute_trm -where - "permute_kind pi Type = Type" -| "permute_kind pi (KPi t n k) = KPi (permute_ty pi t) (pi \ n) (permute_kind pi k)" -| "permute_ty pi (TConst i) = TConst (pi \ i)" -| "permute_ty pi (TApp A M) = TApp (permute_ty pi A) (permute_trm pi M)" -| "permute_ty pi (TPi A x B) = TPi (permute_ty pi A) (pi \ x) (permute_ty pi B)" -| "permute_trm pi (Const i) = Const (pi \ i)" -| "permute_trm pi (Var x) = Var (pi \ x)" -| "permute_trm pi (App M N) = App (permute_trm pi M) (permute_trm pi N)" -| "permute_trm pi (Lam A x M) = Lam (permute_ty pi A) (pi \ x) (permute_trm pi M)" -lemma rperm_zero_ok: - "0 \ (x :: kind) = x" - "0 \ (y :: ty) = y" - "0 \ (z :: trm) = z" -apply(induct x and y and z rule: kind_ty_trm.inducts) -apply(simp_all) -done +setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *} -lemma rperm_plus_ok: - "(p + q) \ (x :: kind) = p \ q \ x" - "(p + q) \ (y :: ty) = p \ q \ y" - "(p + q) \ (z :: trm) = p \ q \ z" -apply(induct x and y and z rule: kind_ty_trm.inducts) -apply(simp_all) -done - -instance -apply default -apply (simp_all only:rperm_zero_ok rperm_plus_ok) -done - -end - -(* -setup {* snd o define_raw_perms ["kind", "ty", "trm"] ["LFex.kind", "LFex.ty", "LFex.trm"] *} local_setup {* - snd o define_fv_alpha "LFex.kind" + snd o define_fv_alpha "LFex.rkind" [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *} notation - alpha_kind ("_ \ki _" [100, 100] 100) -and alpha_ty ("_ \ty _" [100, 100] 100) -and alpha_trm ("_ \tr _" [100, 100] 100) -thm fv_kind_fv_ty_fv_trm.simps alpha_kind_alpha_ty_alpha_trm.intros -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_inj}, []), (build_alpha_inj @{thms alpha_kind_alpha_ty_alpha_trm.intros} @{thms kind.distinct ty.distinct trm.distinct kind.inject ty.inject trm.inject} @{thms alpha_kind.cases alpha_ty.cases alpha_trm.cases} ctxt)) ctxt)) *} -thm alphas_inj - -lemma alphas_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)" -sorry - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_equivp}, []), - (build_equivps [@{term alpha_kind}, @{term alpha_ty}, @{term alpha_trm}] - @{thm kind_ty_trm.induct} @{thm alpha_kind_alpha_ty_alpha_trm.induct} - @{thms kind.inject ty.inject trm.inject} @{thms alphas_inj} - @{thms kind.distinct ty.distinct trm.distinct} - @{thms alpha_kind.cases alpha_ty.cases alpha_trm.cases} - @{thms alphas_eqvt} ctxt)) ctxt)) *} -thm alphas_equivp -*) - -primrec - rfv_kind :: "kind \ atom set" -and rfv_ty :: "ty \ atom set" -and rfv_trm :: "trm \ atom set" -where - "rfv_kind (Type) = {}" -| "rfv_kind (KPi A x K) = (rfv_ty A) \ ((rfv_kind K) - {atom x})" -| "rfv_ty (TConst i) = {atom i}" -| "rfv_ty (TApp A M) = (rfv_ty A) \ (rfv_trm M)" -| "rfv_ty (TPi A x B) = (rfv_ty A) \ ((rfv_ty B) - {atom x})" -| "rfv_trm (Const i) = {atom i}" -| "rfv_trm (Var x) = {atom x}" -| "rfv_trm (App M N) = (rfv_trm M) \ (rfv_trm N)" -| "rfv_trm (Lam A x M) = (rfv_ty A) \ ((rfv_trm M) - {atom x})" - -inductive - akind :: "kind \ kind \ bool" ("_ \ki _" [100, 100] 100) -and aty :: "ty \ ty \ bool" ("_ \ty _" [100, 100] 100) -and atrm :: "trm \ trm \ bool" ("_ \tr _" [100, 100] 100) -where - a1: "(Type) \ki (Type)" -| a2: "\A \ty A'; \pi. (({atom a}, K) \gen akind rfv_kind pi ({atom b}, K'))\ \ (KPi A a K) \ki (KPi A' b K')" -| a3: "i = j \ (TConst i) \ty (TConst j)" -| a4: "\A \ty A'; M \tr M'\ \ (TApp A M) \ty (TApp A' M')" -| a5: "\A \ty A'; \pi. (({atom a}, B) \gen aty rfv_ty pi ({atom b}, B'))\ \ (TPi A a B) \ty (TPi A' b B')" -| a6: "i = j \ (Const i) \tr (Const j)" -| a7: "x = y \ (Var x) \tr (Var y)" -| a8: "\M \tr M'; N \tr N'\ \ (App M N) \tr (App M' N')" -| a9: "\A \ty A'; \pi. (({atom a}, M) \gen atrm rfv_trm pi ({atom b}, M'))\ \ (Lam A a M) \tr (Lam A' b M')" - -lemma akind_aty_atrm_inj: - "(Type) \ki (Type) = True" - "((KPi A a K) \ki (KPi A' b K')) = ((A \ty A') \ (\pi. ({atom a}, K) \gen akind rfv_kind pi ({atom b}, K')))" - "(TConst i) \ty (TConst j) = (i = j)" - "(TApp A M) \ty (TApp A' M') = (A \ty A' \ M \tr M')" - "((TPi A a B) \ty (TPi A' b B')) = ((A \ty A') \ (\pi. (({atom a}, B) \gen aty rfv_ty pi ({atom b}, B'))))" - "(Const i) \tr (Const j) = (i = j)" - "(Var x) \tr (Var y) = (x = y)" - "(App M N) \tr (App M' N') = (M \tr M' \ N \tr N')" - "((Lam A a M) \tr (Lam A' b M')) = ((A \ty A') \ (\pi. (({atom a}, M) \gen atrm rfv_trm pi ({atom b}, M'))))" -apply - -apply (simp add: akind_aty_atrm.intros) - -apply rule apply (erule akind.cases) apply simp apply blast -apply (simp only: akind_aty_atrm.intros) - -apply rule apply (erule aty.cases) apply simp apply simp apply simp -apply (simp only: akind_aty_atrm.intros) - -apply rule apply (erule aty.cases) apply simp apply simp apply simp -apply (simp only: akind_aty_atrm.intros) - -apply rule apply (erule aty.cases) apply simp apply simp apply blast -apply (simp only: akind_aty_atrm.intros) - -apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast -apply (simp only: akind_aty_atrm.intros) - -apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast -apply (simp only: akind_aty_atrm.intros) - -apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast -apply (simp only: akind_aty_atrm.intros) - -apply rule apply (erule atrm.cases) apply simp apply simp apply simp apply blast -apply (simp only: akind_aty_atrm.intros) -done + 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\rfv_kind t1) = rfv_kind (pi\t1))" - "((pi\rfv_ty t2) = rfv_ty (pi\t2))" - "((pi\rfv_trm t3) = rfv_trm (pi\t3))" -apply(induct t1 and t2 and t3 rule: kind_ty_trm.inducts) -apply(simp_all add: union_eqvt Diff_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 @@ -171,9 +47,9 @@ "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: akind_aty_atrm.inducts) -apply (simp_all add: akind_aty_atrm.intros) -apply (simp_all add: akind_aty_atrm_inj) +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 @@ -185,387 +61,173 @@ apply assumption done -lemma al_refl: - fixes K::"kind" - and A::"ty" - and M::"trm" - shows "K \ki K" - and "A \ty A" - and "M \tr M" - apply(induct K and A and M rule: kind_ty_trm.inducts) - apply(auto intro: akind_aty_atrm.intros) - apply (rule a2) - apply auto - apply(rule_tac x="0" in exI) - apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen) - apply (rule a5) - apply auto - apply(rule_tac x="0" in exI) - apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen) - apply (rule a9) - apply auto - apply(rule_tac x="0" in exI) - apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen) - done - -lemma al_sym: - fixes K K'::"kind" and A A'::"ty" and M M'::"trm" - shows "K \ki K' \ K' \ki K" - and "A \ty A' \ A' \ty A" - and "M \tr M' \ M' \tr M" - apply(induct K K' and A A' and M M' rule: akind_aty_atrm.inducts) - apply(simp_all add: akind_aty_atrm.intros) - apply (simp_all add: akind_aty_atrm_inj) - apply(erule alpha_gen_compose_sym) - apply(erule alpha_eqvt) - apply(erule alpha_gen_compose_sym) - apply(erule alpha_eqvt) - apply(erule alpha_gen_compose_sym) - apply(erule alpha_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 -lemma al_trans: - fixes K K' K''::"kind" and A A' A''::"ty" and M M' M''::"trm" - shows "K \ki K' \ K' \ki K'' \ K \ki K''" - and "A \ty A' \ A' \ty A'' \ A \ty A''" - and "M \tr M' \ M' \tr M'' \ M \tr M''" - apply(induct K K' and A A' and M M' arbitrary: K'' and A'' and M'' rule: akind_aty_atrm.inducts) - apply(simp_all add: akind_aty_atrm.intros) - apply(erule akind.cases) - apply(simp_all add: akind_aty_atrm.intros) - apply(simp add: akind_aty_atrm_inj) - apply(erule alpha_gen_compose_trans) - apply(assumption) - apply(erule alpha_eqvt) - apply(rotate_tac 4) - apply(erule aty.cases) - apply(simp_all add: akind_aty_atrm.intros) - apply(rotate_tac 3) - apply(erule aty.cases) - apply(simp_all add: akind_aty_atrm.intros) - apply(simp add: akind_aty_atrm_inj) - apply(erule alpha_gen_compose_trans) - apply(assumption) - apply(erule alpha_eqvt) - apply(rotate_tac 4) - apply(erule atrm.cases) - apply(simp_all add: akind_aty_atrm.intros) - apply(rotate_tac 3) - apply(erule atrm.cases) - apply(simp_all add: akind_aty_atrm.intros) - apply(simp add: akind_aty_atrm_inj) - apply(erule alpha_gen_compose_trans) - apply(assumption) - apply(erule alpha_eqvt) - done - -lemma alpha_equivps: - shows "equivp akind" - and "equivp aty" - and "equivp atrm" - apply(rule equivpI) - unfolding reflp_def symp_def transp_def - apply(auto intro: al_refl al_sym al_trans) - apply(rule equivpI) - unfolding reflp_def symp_def transp_def - apply(auto intro: al_refl al_sym al_trans) - apply(rule equivpI) - unfolding reflp_def symp_def transp_def - apply(auto intro: al_refl al_sym al_trans) - done - -quotient_type KIND = kind / akind - by (rule alpha_equivps) - -quotient_type - TY = ty / aty and - TRM = trm / atrm - by (auto intro: alpha_equivps) - -quotient_definition - "TYP :: KIND" -is - "Type" - -quotient_definition - "KPI :: TY \ name \ KIND \ KIND" -is - "KPi" - -quotient_definition - "TCONST :: ident \ TY" -is - "TConst" +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})) +*} -quotient_definition - "TAPP :: TY \ TRM \ TY" -is - "TApp" - -quotient_definition - "TPI :: TY \ name \ TY \ TY" -is - "TPi" - -(* FIXME: does not work with CONST *) -quotient_definition - "CONS :: ident \ TRM" -is - "Const" - -quotient_definition - "VAR :: name \ TRM" -is - "Var" - -quotient_definition - "APP :: TRM \ TRM \ TRM" -is - "App" - -quotient_definition - "LAM :: TY \ name \ TRM \ TRM" -is - "Lam" - -(* FIXME: print out a warning if the type contains a liftet type, like kind \ name set *) -quotient_definition - "fv_kind :: KIND \ atom set" -is - "rfv_kind" - -quotient_definition - "fv_ty :: TY \ atom set" -is - "rfv_ty" - -quotient_definition - "fv_trm :: TRM \ atom set" -is - "rfv_trm" - -lemma alpha_rfv: - shows "(t \ki s \ rfv_kind t = rfv_kind s) \ - (t1 \ty s1 \ rfv_ty t1 = rfv_ty s1) \ - (t2 \tr s2 \ rfv_trm t2 = rfv_trm s2)" - apply(rule akind_aty_atrm.induct) - apply(simp_all add: alpha_gen) - done +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 -lemma perm_rsp[quot_respect]: - "(op = ===> akind ===> akind) permute permute" - "(op = ===> aty ===> aty) permute permute" - "(op = ===> atrm ===> atrm) permute permute" - by (simp_all add:alpha_eqvt) - -lemma tconst_rsp[quot_respect]: - "(op = ===> aty) TConst TConst" - apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done -lemma tapp_rsp[quot_respect]: - "(aty ===> atrm ===> aty) TApp TApp" - apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done -lemma var_rsp[quot_respect]: - "(op = ===> atrm) Var Var" - apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done -lemma app_rsp[quot_respect]: - "(atrm ===> atrm ===> atrm) App App" - apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done -lemma const_rsp[quot_respect]: - "(op = ===> atrm) Const Const" - apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done - -lemma kpi_rsp[quot_respect]: - "(aty ===> op = ===> akind ===> akind) KPi KPi" - apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) - apply (rule a2) apply assumption - apply (rule_tac x="0" in exI) - apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen) - done +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 *} -lemma tpi_rsp[quot_respect]: - "(aty ===> op = ===> aty ===> aty) TPi TPi" - apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) - apply (rule a5) apply assumption - apply (rule_tac x="0" in exI) - apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen) - done -lemma lam_rsp[quot_respect]: - "(aty ===> op = ===> atrm ===> atrm) Lam Lam" - apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) - apply (rule a9) apply assumption - apply (rule_tac x="0" in exI) - apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen) - done +lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted] -lemma rfv_ty_rsp[quot_respect]: - "(aty ===> op =) rfv_ty rfv_ty" - by (simp add: alpha_rfv) -lemma rfv_kind_rsp[quot_respect]: - "(akind ===> op =) rfv_kind rfv_kind" - by (simp add: alpha_rfv) -lemma rfv_trm_rsp[quot_respect]: - "(atrm ===> op =) rfv_trm rfv_trm" - by (simp add: alpha_rfv) +thm rkind_rty_rtrm.inducts +lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted] -thm kind_ty_trm.induct -lemmas KIND_TY_TRM_induct = kind_ty_trm.induct[quot_lifted] - -thm kind_ty_trm.inducts -lemmas KIND_TY_TRM_inducts = kind_ty_trm.inducts[quot_lifted] - -instantiation KIND and TY and TRM :: pt +instantiation kind and ty and trm :: pt begin quotient_definition - "permute_KIND :: perm \ KIND \ KIND" + "permute_kind :: perm \ kind \ kind" is - "permute :: perm \ kind \ kind" - -quotient_definition - "permute_TY :: perm \ TY \ TY" -is - "permute :: perm \ ty \ ty" + "permute :: perm \ rkind \ rkind" quotient_definition - "permute_TRM :: perm \ TRM \ TRM" + "permute_ty :: perm \ ty \ ty" is - "permute :: perm \ trm \ trm" - -lemmas permute_ktt[simp] = permute_kind_permute_ty_permute_trm.simps[quot_lifted] - -lemma perm_zero_ok: "0 \ (x :: KIND) = x \ 0 \ (y :: TY) = y \ 0 \ (z :: TRM) = z" -apply (induct rule: KIND_TY_TRM_induct) -apply (simp_all) -done + "permute :: perm \ rty \ rty" -lemma perm_add_ok: - "((p + q) \ (x1 :: KIND) = (p \ q \ x1))" - "((p + q) \ (x2 :: TY) = p \ q \ x2)" - "((p + q) \ (x3 :: TRM) = p \ q \ x3)" -apply (induct x1 and x2 and x3 rule: KIND_TY_TRM_inducts) -apply (simp_all) -done +quotient_definition + "permute_trm :: perm \ trm \ trm" +is + "permute :: perm \ rtrm \ rtrm" -instance -apply default -apply (simp_all add: perm_zero_ok perm_add_ok) -done +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 -lemmas AKIND_ATY_ATRM_inducts = akind_aty_atrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen] +(* +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 KIND_TY_TRM_INJECT = akind_aty_atrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] +lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted] -lemmas fv_kind_ty_trm = rfv_kind_rfv_ty_rfv_trm.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 supp_kind_ty_trm_easy: - "supp TYP = {}" - "supp (TCONST i) = {atom i}" - "supp (TAPP A M) = supp A \ supp M" - "supp (CONS i) = {atom i}" - "supp (VAR x) = {atom x}" - "supp (APP M N) = supp M \ supp N" -apply (simp_all add: supp_def permute_ktt KIND_TY_TRM_INJECT) -apply (simp_all only: supp_at_base[simplified supp_def]) -apply (simp_all add: Collect_imp_eq Collect_neg_eq) -done - -lemma supp_bind: - "(supp (atom na, (ty, ki))) supports (KPI ty na ki)" - "(supp (atom na, (ty, ty2))) supports (TPI ty na ty2)" - "(supp (atom na, (ty, trm))) supports (LAM ty na trm)" -apply(simp_all add: supports_def) -apply(fold fresh_def) -apply(simp_all add: fresh_Pair swap_fresh_fresh) -apply(clarify) -apply(subst swap_at_base_simps(3)) -apply(simp_all add: fresh_atom) -apply(clarify) -apply(subst swap_at_base_simps(3)) -apply(simp_all add: fresh_atom) -apply(clarify) -apply(subst swap_at_base_simps(3)) +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(simp_all add: supp_kind_ty_trm_easy) -apply(rule supports_finite) -apply(rule supp_bind(1)) -apply(simp add: supp_Pair supp_atom) -apply(rule supports_finite) -apply(rule supp_bind(2)) -apply(simp add: supp_Pair supp_atom) -apply(rule supports_finite) -apply(rule supp_bind(3)) -apply(simp add: supp_Pair supp_atom) +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 -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 add: supp_kind_ty_trm_easy) -apply (simp_all add: fv_kind_ty_trm) -apply(subgoal_tac "supp (KPI ty name kind) = supp ty \ supp (Abs {atom name} kind)") -apply(simp add: supp_Abs Set.Un_commute) -apply(simp (no_asm) add: supp_def) -apply(simp add: KIND_TY_TRM_INJECT) -apply(simp add: Abs_eq_iff) -apply(simp add: alpha_gen) -apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute insert_eqvt empty_eqvt atom_eqvt) -apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric]) -apply(subgoal_tac "supp (TPI ty1 name ty2) = supp ty1 \ supp (Abs {atom name} ty2)") -apply(simp add: supp_Abs Set.Un_commute) -apply(simp (no_asm) add: supp_def) -apply(simp add: KIND_TY_TRM_INJECT) -apply(simp add: Abs_eq_iff) -apply(simp add: alpha_gen) -apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt) -apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) -apply(subgoal_tac "supp (LAM ty name trm) = supp ty \ supp (Abs {atom name} trm)") -apply(simp add: supp_Abs Set.Un_commute) -apply(simp (no_asm) add: supp_def) -apply(simp add: KIND_TY_TRM_INJECT) -apply(simp add: Abs_eq_iff) -apply(simp add: alpha_gen) -apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric] insert_eqvt empty_eqvt atom_eqvt) -apply(simp add: Collect_imp_eq Collect_neg_eq Set.Un_commute) -done + "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 -(* Not needed anymore *) -lemma supp_kpi_pre: "supp (KPI A x K) = (supp (Abs {atom x} K)) \ supp A" -apply (simp add: permute_set_eq supp_def Abs_eq_iff KIND_TY_TRM_INJECT) -apply (simp add: alpha_gen supp_fv) -apply (simp add: Collect_imp_eq Collect_neg_eq add: atom_eqvt Set.Un_commute) -done - -lemma supp_kind_ty_trm: - "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})" -apply (simp_all only: supp_kind_ty_trm_easy) -apply (simp_all only: supp_fv fv_kind_ty_trm) -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