--- 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 \<bullet> n) (permute_kind pi k)"
-| "permute_ty pi (TConst i) = TConst (pi \<bullet> 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 \<bullet> x) (permute_ty pi B)"
-| "permute_trm pi (Const i) = Const (pi \<bullet> i)"
-| "permute_trm pi (Var x) = Var (pi \<bullet> 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 \<bullet> x) (permute_trm pi M)"
-lemma rperm_zero_ok:
- "0 \<bullet> (x :: kind) = x"
- "0 \<bullet> (y :: ty) = y"
- "0 \<bullet> (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) \<bullet> (x :: kind) = p \<bullet> q \<bullet> x"
- "(p + q) \<bullet> (y :: ty) = p \<bullet> q \<bullet> y"
- "(p + q) \<bullet> (z :: trm) = p \<bullet> q \<bullet> 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 ("_ \<approx>ki _" [100, 100] 100)
-and alpha_ty ("_ \<approx>ty _" [100, 100] 100)
-and alpha_trm ("_ \<approx>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 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
- "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
- "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> 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 \<Rightarrow> atom set"
-and rfv_ty :: "ty \<Rightarrow> atom set"
-and rfv_trm :: "trm \<Rightarrow> atom set"
-where
- "rfv_kind (Type) = {}"
-| "rfv_kind (KPi A x K) = (rfv_ty A) \<union> ((rfv_kind K) - {atom x})"
-| "rfv_ty (TConst i) = {atom i}"
-| "rfv_ty (TApp A M) = (rfv_ty A) \<union> (rfv_trm M)"
-| "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((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) \<union> (rfv_trm N)"
-| "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})"
-
-inductive
- akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
-and aty :: "ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100)
-and atrm :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<approx>tr _" [100, 100] 100)
-where
- a1: "(Type) \<approx>ki (Type)"
-| a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, K) \<approx>gen akind rfv_kind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b K')"
-| a3: "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)"
-| a4: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')"
-| a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, B) \<approx>gen aty rfv_ty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>ty (TPi A' b B')"
-| a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)"
-| a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)"
-| a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
-| a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, M) \<approx>gen atrm rfv_trm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
-
-lemma akind_aty_atrm_inj:
- "(Type) \<approx>ki (Type) = True"
- "((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>ty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen akind rfv_kind pi ({atom b}, K')))"
- "(TConst i) \<approx>ty (TConst j) = (i = j)"
- "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
- "((TPi A a B) \<approx>ty (TPi A' b B')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen aty rfv_ty pi ({atom b}, B'))))"
- "(Const i) \<approx>tr (Const j) = (i = j)"
- "(Var x) \<approx>tr (Var y) = (x = y)"
- "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
- "((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>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 ("_ \<approx>ki _" [100, 100] 100)
+and alpha_rty ("_ \<approx>ty _" [100, 100] 100)
+and alpha_rtrm ("_ \<approx>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\<bullet>rfv_kind t1) = rfv_kind (pi\<bullet>t1))"
- "((pi\<bullet>rfv_ty t2) = rfv_ty (pi\<bullet>t2))"
- "((pi\<bullet>rfv_trm t3) = rfv_trm (pi\<bullet>t3))"
-apply(induct t1 and t2 and t3 rule: kind_ty_trm.inducts)
-apply(simp_all add: union_eqvt Diff_eqvt)
+ "((pi\<bullet>fv_rkind t1) = fv_rkind (pi\<bullet>t1))"
+ "((pi\<bullet>fv_rty t2) = fv_rty (pi\<bullet>t2))"
+ "((pi\<bullet>fv_rtrm t3) = fv_rtrm (pi\<bullet>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 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
"t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
"t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> 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 \<approx>ki K"
- and "A \<approx>ty A"
- and "M \<approx>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 \<approx>ki K' \<Longrightarrow> K' \<approx>ki K"
- and "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A"
- and "M \<approx>tr M' \<Longrightarrow> M' \<approx>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 \<approx>ki K' \<Longrightarrow> K' \<approx>ki K'' \<Longrightarrow> K \<approx>ki K''"
- and "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A'' \<Longrightarrow> A \<approx>ty A''"
- and "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M'' \<Longrightarrow> M \<approx>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 \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
-is
- "KPi"
-
-quotient_definition
- "TCONST :: ident \<Rightarrow> 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 \<Rightarrow> TRM \<Rightarrow> TY"
-is
- "TApp"
-
-quotient_definition
- "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
-is
- "TPi"
-
-(* FIXME: does not work with CONST *)
-quotient_definition
- "CONS :: ident \<Rightarrow> TRM"
-is
- "Const"
-
-quotient_definition
- "VAR :: name \<Rightarrow> TRM"
-is
- "Var"
-
-quotient_definition
- "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
-is
- "App"
-
-quotient_definition
- "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
-is
- "Lam"
-
-(* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
-quotient_definition
- "fv_kind :: KIND \<Rightarrow> atom set"
-is
- "rfv_kind"
-
-quotient_definition
- "fv_ty :: TY \<Rightarrow> atom set"
-is
- "rfv_ty"
-
-quotient_definition
- "fv_trm :: TRM \<Rightarrow> atom set"
-is
- "rfv_trm"
-
-lemma alpha_rfv:
- shows "(t \<approx>ki s \<longrightarrow> rfv_kind t = rfv_kind s) \<and>
- (t1 \<approx>ty s1 \<longrightarrow> rfv_ty t1 = rfv_ty s1) \<and>
- (t2 \<approx>tr s2 \<longrightarrow> 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 \<Rightarrow> rkind \<Rightarrow> rkind"}]
+ (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}
+local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}]
+ (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}
+local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> 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 \<Rightarrow> KIND \<Rightarrow> KIND"
+ "permute_kind :: perm \<Rightarrow> kind \<Rightarrow> kind"
is
- "permute :: perm \<Rightarrow> kind \<Rightarrow> kind"
-
-quotient_definition
- "permute_TY :: perm \<Rightarrow> TY \<Rightarrow> TY"
-is
- "permute :: perm \<Rightarrow> ty \<Rightarrow> ty"
+ "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"
quotient_definition
- "permute_TRM :: perm \<Rightarrow> TRM \<Rightarrow> TRM"
+ "permute_ty :: perm \<Rightarrow> ty \<Rightarrow> ty"
is
- "permute :: perm \<Rightarrow> trm \<Rightarrow> trm"
-
-lemmas permute_ktt[simp] = permute_kind_permute_ty_permute_trm.simps[quot_lifted]
-
-lemma perm_zero_ok: "0 \<bullet> (x :: KIND) = x \<and> 0 \<bullet> (y :: TY) = y \<and> 0 \<bullet> (z :: TRM) = z"
-apply (induct rule: KIND_TY_TRM_induct)
-apply (simp_all)
-done
+ "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"
-lemma perm_add_ok:
- "((p + q) \<bullet> (x1 :: KIND) = (p \<bullet> q \<bullet> x1))"
- "((p + q) \<bullet> (x2 :: TY) = p \<bullet> q \<bullet> x2)"
- "((p + q) \<bullet> (x3 :: TRM) = p \<bullet> q \<bullet> x3)"
-apply (induct x1 and x2 and x3 rule: KIND_TY_TRM_inducts)
-apply (simp_all)
-done
+quotient_definition
+ "permute_trm :: perm \<Rightarrow> trm \<Rightarrow> trm"
+is
+ "permute :: perm \<Rightarrow> rtrm \<Rightarrow> 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 \<union> supp M"
- "supp (CONS i) = {atom i}"
- "supp (VAR x) = {atom x}"
- "supp (APP M N) = supp M \<union> 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 \<union> supp M) supports (TAPP A M)"
+ "(supp (atom i)) supports (CONS i)"
+ "(supp (atom x)) supports (VAR x)"
+ "(supp M \<union> supp N) supports (APP M N)"
+ "(supp ty \<union> supp (atom na) \<union> supp ki) supports (KPI ty na ki)"
+ "(supp ty \<union> supp (atom na) \<union> supp ty2) supports (TPI ty na ty2)"
+ "(supp ty \<union> supp (atom na) \<union> 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\<Colon>KIND))"
- "finite (supp (y\<Colon>TY))"
- "finite (supp (z\<Colon>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\<Colon>kind))"
+ "finite (supp (y\<Colon>ty))"
+ "finite (supp (z\<Colon>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 \<Longrightarrow> supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)"
+ "supp (TCONST i) = {atom i}"
+ "supp (TAPP A M) = supp A \<union> supp M"
+ "supp rty2 = fv_ty rty2 \<Longrightarrow> supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)"
+ "supp (CONS i) = {atom i}"
+ "supp (VAR x) = {atom x}"
+ "supp (APP M N) = supp M \<union> supp N"
+ "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (LAM rty name rtrm) = supp rty \<union> 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 \<union> 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 \<union> 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 \<union> 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)) \<union> 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 \<union> (supp K - {atom x})"
- "supp (TCONST i) = {atom i}"
- "supp (TAPP A M) = supp A \<union> supp M"
- "supp (TPI A x B) = supp A \<union> (supp B - {atom x})"
- "supp (CONS i) = {atom i}"
- "supp (VAR x) = {atom x}"
- "supp (APP M N) = supp M \<union> supp N"
- "supp (LAM A x M) = supp A \<union> (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 \<union> (supp K - {atom x})"
+ "supp (TCONST i) = {atom i}"
+ "supp (TAPP A M) = supp A \<union> supp M"
+ "supp (TPI A x B) = supp A \<union> (supp B - {atom x})"
+ "supp (CONS i) = {atom i}"
+ "supp (VAR x) = {atom x}"
+ "supp (APP M N) = supp M \<union> supp N"
+ "supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
+ by (simp_all only: supp_fv fv_kind_ty_trm)
end
--- 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 \<Rightarrow> perm \<Rightarrow> 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 \<Rightarrow> perm \<Rightarrow> 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
*}
--- 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 \<Rightarrow> rtrm1 \<Rightarrow> 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 \<union> supp s) supports (Ap1 t s)"
+ "(supp (atom x) \<union> supp t) supports (Lm1 x t)"
+ "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)"
+ "{} supports BUnit"
+ "(supp (atom x)) supports (BVr x)"
+ "(supp a \<union> 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) \<union> 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 \<Rightarrow> rlts \<Rightarrow> rlts"
-lemma trm5_lts_zero:
- "0 \<bullet> (x\<Colon>trm5) = x"
- "0 \<bullet> (y\<Colon>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) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x"
- "(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> 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))"