# HG changeset patch # User Christian Urban # Date 1267029163 -3600 # Node ID 4b0563bc4b0301372af59daec0d4eb3cd295bfb5 # Parent 11b8798dea5dd9e15569090645535da661d4042a# Parent d1ab27c10049c3ae8e34567d47c428c0499955cc merged 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 diff -r 11b8798dea5d -r 4b0563bc4b03 Quot/Nominal/Perm.thy --- a/Quot/Nominal/Perm.thy Wed Feb 24 17:32:22 2010 +0100 +++ b/Quot/Nominal/Perm.thy Wed Feb 24 17:32:43 2010 +0100 @@ -9,7 +9,55 @@ *} ML {* +fun prove_perm_empty lthy induct perm_def perm_frees = +let + val perm_types = map fastype_of perm_frees; + val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); + val gl = + HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj + (map (fn ((perm, T), x) => HOLogic.mk_eq + (perm $ @{term "0 :: perm"} $ Free (x, T), + Free (x, T))) + (perm_frees ~~ + map body_type perm_types ~~ perm_indnames))); + fun tac _ = + EVERY [ + indtac induct perm_indnames 1, + ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def))) + ]; +in + split_conj_thm (Goal.prove lthy perm_indnames [] gl tac) +end; +*} +ML {* +fun prove_perm_append lthy induct perm_def perm_frees = +let + val add_perm = @{term "op + :: (perm \ perm \ perm)"} + val pi1 = Free ("pi1", @{typ perm}); + val pi2 = Free ("pi2", @{typ perm}); + val perm_types = map fastype_of perm_frees + val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); + val gl = + (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj + (map (fn ((perm, T), x) => + let + val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T) + val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T)) + in HOLogic.mk_eq (lhs, rhs) + end) + (perm_frees ~~ map body_type perm_types ~~ perm_indnames)))) + fun tac _ = + EVERY [ + indtac induct perm_indnames 1, + ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def))) + ] +in + split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] gl tac) +end; +*} + +ML {* (* TODO: full_name can be obtained from new_type_names with Datatype *) fun define_raw_perms new_type_names full_tnames thy = let @@ -22,7 +70,6 @@ val perm_types = map (fn (i, _) => let val T = nth_dtyp i in @{typ perm} --> T --> T end) descr; - val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); val perm_names_types' = perm_names' ~~ perm_types; val pi = Free ("pi", @{typ perm}); fun perm_eq_constr i (cname, dts) = @@ -60,48 +107,21 @@ (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; val perm_frees = (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef); - val perm_empty_thms = - let - val gl = - HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj - (map (fn ((perm, T), x) => HOLogic.mk_eq - (perm $ @{term "0 :: perm"} $ Free (x, T), - Free (x, T))) - (perm_frees ~~ - map body_type perm_types ~~ perm_indnames))); - fun tac {context = ctxt, ...} = - EVERY [ - indtac induct perm_indnames 1, - ALLGOALS (asm_full_simp_tac (@{simpset} addsimps perm_ldef)) - ]; - in - (List.take (split_conj_thm (Goal.prove lthy' perm_indnames [] gl tac), length new_type_names)) - end; - val add_perm = @{term "op + :: (perm \ perm \ perm)"} - val pi1 = Free ("pi1", @{typ perm}); - val pi2 = Free ("pi2", @{typ perm}); - val perm_append_thms = - List.take ((split_conj_thm - (Goal.prove lthy' ("pi1" :: "pi2" :: perm_indnames) [] - (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj - (map (fn ((perm, T), x) => - let - val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T) - val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T)) - in HOLogic.mk_eq (lhs, rhs) - end) - (perm_frees ~~ - map body_type perm_types ~~ perm_indnames)))) - (fn _ => EVERY [indtac induct perm_indnames 1, - ALLGOALS (asm_full_simp_tac (@{simpset} addsimps perm_ldef))]))), - length new_type_names); - fun tac ctxt perm_thms = + val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names); + val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names) + val perms_name = space_implode "_" perm_names' + val perms_zero_bind = Binding.name (perms_name ^ "_zero") + val perms_append_bind = Binding.name (perms_name ^ "_append") + fun tac _ perm_thms = (Class.intro_classes_tac []) THEN (ALLGOALS ( - simp_tac (@{simpset} addsimps perm_thms + simp_tac (HOL_ss addsimps perm_thms ))); fun morphism phi = map (Morphism.thm phi); in - Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms) lthy' + lthy' + |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms)) + |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms)) + |> Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms) end *} diff -r 11b8798dea5d -r 4b0563bc4b03 Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Wed Feb 24 17:32:22 2010 +0100 +++ b/Quot/Nominal/Terms.thy Wed Feb 24 17:32:43 2010 +0100 @@ -158,59 +158,43 @@ is "permute :: perm \ rtrm1 \ rtrm1" -lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted] - -instance -apply default -apply(induct_tac [!] x rule: trm1_bp_inducts(1)) -apply(simp_all) -done +instance by default + (simp_all add: permute_rtrm1_permute_bp_zero[quot_lifted] permute_rtrm1_permute_bp_append[quot_lifted]) end lemmas - fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] + permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted] +and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted] and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] -lemma lm1_supp_pre: - shows "(supp (atom x, t)) supports (Lm1 x t) " -apply(simp add: supports_def) -apply(fold fresh_def) -apply(simp add: fresh_Pair swap_fresh_fresh) -apply(clarify) -apply(subst swap_at_base_simps(3)) +lemma supports: + "(supp (atom x)) supports (Vr1 x)" + "(supp t \ supp s) supports (Ap1 t s)" + "(supp (atom x) \ supp t) supports (Lm1 x t)" + "(supp b \ supp t \ supp s) supports (Lt1 b t s)" + "{} supports BUnit" + "(supp (atom x)) supports (BVr x)" + "(supp a \ supp b) supports (BPr a b)" +apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh permute_trm1) +apply(rule_tac [!] allI)+ +apply(rule_tac [!] impI) +apply(tactic {* ALLGOALS (REPEAT o etac conjE) *}) apply(simp_all add: fresh_atom) done -lemma lt1_supp_pre: - shows "(supp (x, t, s)) supports (Lt1 t x s) " -apply(simp add: supports_def) -apply(fold fresh_def) -apply(simp add: fresh_Pair swap_fresh_fresh) -done - -lemma bp_supp: "finite (supp (bp :: bp))" - apply (induct bp) - apply(simp_all add: supp_def) - apply(simp add: supp_at_base supp_def[symmetric]) - apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric] supp_def) +lemma rtrm1_bp_fs: + "finite (supp (x :: trm1))" + "finite (supp (b :: bp))" + apply (induct x and b rule: trm1_bp_inducts) + apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *}) + apply(simp_all add: supp_atom) done instance trm1 :: fs apply default -apply(induct_tac x rule: trm1_bp_inducts(1)) -apply(simp_all) -apply(simp add: supp_def alpha1_INJ eqvts) -apply(simp add: supp_def[symmetric] supp_at_base) -apply(simp only: supp_def alpha1_INJ eqvts permute_trm1) -apply(simp add: Collect_imp_eq Collect_neg_eq) -apply(rule supports_finite) -apply(rule lm1_supp_pre) -apply(simp add: supp_Pair supp_atom) -apply(rule supports_finite) -apply(rule lt1_supp_pre) -apply(simp add: supp_Pair supp_atom bp_supp) +apply (rule rtrm1_bp_fs(1)) done lemma fv_eq_bv: "fv_bp bp = bv1 bp" @@ -235,14 +219,14 @@ apply(simp add: Collect_imp_eq Collect_neg_eq) apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)") apply(simp add: supp_Abs fv_trm1) -apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) +apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1) apply(simp add: alpha1_INJ) apply(simp add: Abs_eq_iff) apply(simp add: alpha_gen.simps) apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \ supp (Abs (bv1 bp) rtrm12)") apply(simp add: supp_Abs fv_trm1 fv_eq_bv) -apply(simp (no_asm) add: supp_def) +apply(simp (no_asm) add: supp_def permute_trm1) apply(simp add: alpha1_INJ alpha_bp_eq) apply(simp add: Abs_eq_iff) apply(simp add: alpha_gen) @@ -591,35 +575,16 @@ is "permute :: perm \ rlts \ rlts" -lemma trm5_lts_zero: - "0 \ (x\trm5) = x" - "0 \ (y\lts) = y" - apply(induct x and y rule: trm5_lts_inducts) - apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted]) - done - -lemma trm5_lts_plus: - "(p + q) \ (x\trm5) = p \ q \ x" - "(p + q) \ (y\lts) = p \ q \ y" - apply(induct x and y rule: trm5_lts_inducts) - apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted]) - done - -instance - apply default - apply (simp_all add: trm5_lts_zero trm5_lts_plus) - done +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] -and - alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] -and - bv5[simp] = rbv5.simps[quot_lifted] -and - fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] +lemmas + permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted] +and alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] +and bv5[simp] = rbv5.simps[quot_lifted] +and fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted] lemma lets_ok: "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"