--- a/Nominal/LFex.thy Fri Mar 05 14:56:19 2010 +0100
+++ b/Nominal/LFex.thy Fri Mar 05 17:09:48 2010 +0100
@@ -1,143 +1,36 @@
theory LFex
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp"
+imports "Parser"
begin
atom_decl name
atom_decl ident
-datatype rkind =
+ML {* restricted_nominal := false *}
+
+nominal_datatype kind =
Type
- | KPi "rty" "name" "rkind"
-and rty =
+ | KPi "ty" n::"name" k::"kind" bind n in k
+and ty =
TConst "ident"
- | TApp "rty" "rtrm"
- | TPi "rty" "name" "rty"
-and rtrm =
+ | TApp "ty" "trm"
+ | TPi "ty" n::"name" t::"ty" bind n in t
+and trm =
Const "ident"
| Var "name"
- | App "rtrm" "rtrm"
- | Lam "rty" "name" "rtrm"
-
-
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "LFex.rkind") 3 *}
-print_theorems
-
-local_setup {*
- snd o define_fv_alpha (Datatype.the_info @{theory} "LFex.rkind")
- [[ [], [(NONE, 1, 2)]],
- [ [], [], [(NONE, 1, 2)] ],
- [ [], [], [], [(NONE, 1, 2)]]] *}
-notation
- alpha_rkind ("_ \<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>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
-
-lemma alpha_eqvt:
- "(t1 \<approx>ki s1 \<longrightarrow> (p \<bullet> t1) \<approx>ki (p \<bullet> s1)) \<and>
- (t2 \<approx>ty s2 \<longrightarrow> (p \<bullet> t2) \<approx>ty (p \<bullet> s2)) \<and>
- (t3 \<approx>tr s3 \<longrightarrow> (p \<bullet> t3) \<approx>tr (p \<bullet> s3))"
-apply(rule alpha_rkind_alpha_rty_alpha_rtrm.induct)
-apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
-apply (erule_tac [!] conjE)+
-apply (erule_tac [!] exi[of _ _ "p"])
-apply (erule_tac [!] alpha_gen_compose_eqvt)
-apply (simp_all add: rfv_eqvt eqvts atom_eqvt)
-done
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []),
- (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}]
- @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct}
- @{thms rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj}
- @{thms rkind.distinct rty.distinct rtrm.distinct}
- @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases}
- @{thms alpha_eqvt} ctxt)) ctxt)) *}
-thm alpha_equivps
-
-local_setup {* define_quotient_type
- [(([], @{binding kind}, NoSyn), (@{typ rkind}, @{term alpha_rkind})),
- (([], @{binding ty}, NoSyn), (@{typ rty}, @{term alpha_rty} )),
- (([], @{binding trm}, NoSyn), (@{typ rtrm}, @{term alpha_rtrm} ))]
- (ALLGOALS (resolve_tac @{thms alpha_equivps}))
-*}
-
-local_setup {*
-(fn ctxt => ctxt
- |> snd o (Quotient_Def.quotient_lift_const ("TYP", @{term Type}))
- |> snd o (Quotient_Def.quotient_lift_const ("KPI", @{term KPi}))
- |> snd o (Quotient_Def.quotient_lift_const ("TCONST", @{term TConst}))
- |> snd o (Quotient_Def.quotient_lift_const ("TAPP", @{term TApp}))
- |> snd o (Quotient_Def.quotient_lift_const ("TPI", @{term TPi}))
- |> snd o (Quotient_Def.quotient_lift_const ("CONS", @{term Const}))
- |> snd o (Quotient_Def.quotient_lift_const ("VAR", @{term Var}))
- |> snd o (Quotient_Def.quotient_lift_const ("APP", @{term App}))
- |> snd o (Quotient_Def.quotient_lift_const ("LAM", @{term Lam}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_kind", @{term fv_rkind}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_ty", @{term fv_rty}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *}
-print_theorems
-
-local_setup {* snd o prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}]
- (fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *}
-local_setup {* snd o prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}, @{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}, @{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 {* snd o prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *}
-local_setup {* snd o prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *}
-local_setup {* snd o prove_const_rsp Binding.empty [@{term Var}] const_rsp_tac *}
-local_setup {* snd o prove_const_rsp Binding.empty [@{term App}] const_rsp_tac *}
-local_setup {* snd o prove_const_rsp Binding.empty [@{term Const}] const_rsp_tac *}
-local_setup {* snd o prove_const_rsp Binding.empty [@{term KPi}] const_rsp_tac *}
-local_setup {* snd o prove_const_rsp Binding.empty [@{term TPi}] const_rsp_tac *}
-local_setup {* snd o prove_const_rsp Binding.empty [@{term Lam}] const_rsp_tac *}
-
-lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted]
-
-thm rkind_rty_rtrm.inducts
-lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted]
-
-setup {* define_lifted_perms ["LFex.kind", "LFex.ty", "LFex.trm"]
- [("permute_kind", @{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}),
- ("permute_ty", @{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}),
- ("permute_trm", @{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"})]
- @{thms permute_rkind_permute_rty_permute_rtrm_zero permute_rkind_permute_rty_permute_rtrm_append} *}
-
-(*
-Lifts, but slow and not needed?.
-lemmas alpha_kind_alpha_ty_alpha_trm_induct = alpha_rkind_alpha_rty_alpha_rtrm.induct[unfolded alpha_gen, quot_lifted, folded alpha_gen]
-*)
-
-lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted]
-
-lemmas kind_ty_trm_inj = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
-
-lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted]
-
-lemmas fv_eqvt = rfv_eqvt[quot_lifted]
+ | App "trm" "trm"
+ | Lam "ty" n::"name" t::"trm" bind n in t
lemma supports:
- "{} supports TYP"
- "(supp (atom i)) supports (TCONST i)"
- "(supp A \<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)
+ "{} supports Type"
+ "(supp (atom i)) supports (TConst i)"
+ "(supp A \<union> supp M) supports (TApp A M)"
+ "(supp (atom i)) supports (Const 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 kind_ty_trm_perm)
apply(rule_tac [!] allI)+
apply(rule_tac [!] impI)
apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})
@@ -145,10 +38,8 @@
done
lemma kind_ty_trm_fs:
- "finite (supp (x\<Colon>kind))"
- "finite (supp (y\<Colon>ty))"
- "finite (supp (z\<Colon>trm))"
-apply(induct x and y and z rule: kind_ty_trm_inducts)
+ "finite (supp (x\<Colon>kind)) \<and> finite (supp (y\<Colon>ty)) \<and> finite (supp (z\<Colon>trm))"
+apply(induct rule: kind_ty_trm_induct)
apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *})
apply(simp_all add: supp_atom)
done
@@ -166,51 +57,49 @@
apply (blast)+
done
+lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}"
+by (simp add: Collect_imp_eq Collect_neg_eq[symmetric])
+
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 permute_set_eq atom_eqvt)
- apply(simp_all only: kind_ty_trm_inj Abs_eq_iff alpha_gen)
- apply(simp_all only:ex_out)
- apply(simp_all only: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts[symmetric])
- apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric])
- apply(simp_all add: supp_at_base[simplified supp_def] Un_commute)
+ "supp Type = {}"
+ "supp rkind = fv_kind rkind \<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 (Const 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 permute_set_eq atom_eqvt kind_ty_trm_perm)
+ apply(simp_all only: kind_ty_trm_inject Abs_eq_iff alpha_gen)
+ apply(simp_all only: ex_out)
+ apply(simp_all only: eqvts[symmetric])
+ apply(simp_all only: Collect_neg_conj)
+ apply(simp_all only: supp_at_base[simplified supp_def] Un_commute Un_assoc)
+ apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Un_commute Un_assoc)
+ apply(simp_all add: Un_left_commute)
done
-
lemma supp_fv:
- "supp t1 = fv_kind t1"
- "supp t2 = fv_ty t2"
- "supp t3 = fv_trm t3"
- apply(induct t1 and t2 and t3 rule: kind_ty_trm_inducts)
- apply(simp_all (no_asm) only: supp_eqs fv_kind_ty_trm)
+ "supp t1 = fv_kind t1 \<and> supp t2 = fv_ty t2 \<and> supp t3 = fv_trm t3"
+ apply(induct rule: kind_ty_trm_induct)
+ apply(simp_all (no_asm) only: supp_eqs kind_ty_trm_fv)
apply(simp_all)
- apply(subst supp_eqs)
- apply(simp_all add: supp_Abs)
- apply(subst supp_eqs)
- apply(simp_all add: supp_Abs)
- apply(subst supp_eqs)
+ apply(simp_all add: supp_eqs)
apply(simp_all add: supp_Abs)
done
lemma supp_rkind_rty_rtrm:
- "supp TYP = {}"
- "supp (KPI A x K) = supp A \<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)
+ "supp Type = {}"
+ "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 (Const 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 add: supp_fv kind_ty_trm_fv)
end