theory CoreHaskell
imports "../NewParser"
begin
(* Core Haskell *)
atom_decl var
atom_decl cvar
atom_decl tvar
declare [[STEPS = 20]]
nominal_datatype tkind =
KStar
| KFun "tkind" "tkind"
and ckind =
CKEq "ty" "ty"
and ty =
TVar "tvar"
| TC "string"
| TApp "ty" "ty"
| TFun "string" "ty_lst"
| TAll tv::"tvar" "tkind" T::"ty" bind (set) tv in T
| TEq "ckind" "ty"
and ty_lst =
TsNil
| TsCons "ty" "ty_lst"
and co =
CVar "cvar"
| CConst "string"
| CApp "co" "co"
| CFun "string" "co_lst"
| CAll cv::"cvar" "ckind" C::"co" bind (set) cv in C
| CEq "ckind" "co"
| CRefl "ty"
| CSym "co"
| CCir "co" "co"
| CAt "co" "ty"
| CLeft "co"
| CRight "co"
| CSim "co" "co"
| CRightc "co"
| CLeftc "co"
| CCoe "co" "co"
and co_lst =
CsNil
| CsCons "co" "co_lst"
and trm =
Var "var"
| K "string"
| LAMT tv::"tvar" "tkind" t::"trm" bind (set) tv in t
| LAMC cv::"cvar" "ckind" t::"trm" bind (set) cv in t
| AppT "trm" "ty"
| AppC "trm" "co"
| Lam v::"var" "ty" t::"trm" bind (set) v in t
| App "trm" "trm"
| Let x::"var" "ty" "trm" t::"trm" bind (set) x in t
| Case "trm" "assoc_lst"
| Cast "trm" "ty" --"ty is supposed to be a coercion type only"
and assoc_lst =
ANil
| ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
and pat =
Kpat "string" "tvars" "cvars" "vars"
and vars =
VsNil
| VsCons "var" "ty" "vars"
and tvars =
TvsNil
| TvsCons "tvar" "tkind" "tvars"
and cvars =
CvsNil
| CvsCons "cvar" "ckind" "cvars"
binder
bv :: "pat \<Rightarrow> atom list"
and bv_vs :: "vars \<Rightarrow> atom list"
and bv_tvs :: "tvars \<Rightarrow> atom list"
and bv_cvs :: "cvars \<Rightarrow> atom list"
where
"bv (Kpat s tvts tvcs vs) = append (bv_tvs tvts) (append (bv_cvs tvcs) (bv_vs vs))"
| "bv_vs VsNil = []"
| "bv_vs (VsCons v k t) = (atom v) # bv_vs t"
| "bv_tvs TvsNil = []"
| "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t"
| "bv_cvs CvsNil = []"
| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
(* can lift *)
thm distinct
thm fv_defs
thm alpha_bn_imps alpha_equivp
thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts
thm perm_simps
thm perm_laws
thm tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98)
thm eq_iff
thm eq_iff_simps
ML {*
val qtys = [@{typ tkind}, @{typ ckind}, @{typ ty}, @{typ ty_lst}, @{typ co},
@{typ co_lst}, @{typ trm}, @{typ assoc_lst}, @{typ pat}, @{typ vars},
@{typ tvars}, @{typ cvars}]
*}
ML {*
fun lifted ctxt qtys rthm =
let
(* When the theorem is atomized, eta redexes are contracted,
so we do it both in the original theorem *)
val rthm' = Drule.eta_contraction_rule rthm
val ((_, [rthm'']), ctxt') = Variable.import false [rthm'] ctxt
val goal = Quotient_Term.derive_qtrm ctxt' qtys (prop_of rthm'')
in
Goal.prove ctxt' [] [] goal (K (Quotient_Tacs.lift_tac ctxt' [rthm'] 1))
|> singleton (ProofContext.export ctxt' ctxt)
end
*}
ML {*
fun lifted2 ctxt qtys rthms =
let
(* When the theorem is atomized, eta redexes are contracted,
so we do it both in the original theorem *)
val rthms' = map Drule.eta_contraction_rule rthms
val ((_, rthms''), ctxt') = Variable.import false rthms' ctxt
val goals = map (Quotient_Term.derive_qtrm ctxt' qtys o prop_of) rthms''
in
Goal.prove_multi ctxt' [] [] goals (K (Quotient_Tacs.lift_tac ctxt' rthms' 1))
|> ProofContext.export ctxt' ctxt
end
*}
ML {*
val _ = timeit (fn () => map (lifted @{context} qtys) @{thms distinct})
*}
ML {*
val _ = timeit (fn () => lifted2 @{context} qtys @{thms distinct})
*}
ML {*
val thms_i = map (lift_thm @{context} qtys) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.inducts}
*}
ML {*
val thms_f = map (lift_thm @{context} qtys) @{thms fv_defs}
*}
ML {*
val thms_i = map (lift_thm @{context} qtys) @{thms tkind_raw_ckind_raw_ty_raw_ty_lst_raw_co_raw_co_lst_raw_trm_raw_assoc_lst_raw_pat_raw_vars_raw_tvars_raw_cvars_raw.size(50 - 98)}
*}
ML {*
val thms_p = map (lift_thm @{context} qtys) @{thms perm_simps}
*}
ML {*
val thms_f = map (lift_thm @{context} qtys) @{thms perm_laws}
*}
ML {*
val thms_e = map (lift_thm @{context} qtys)
@{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
prod.cases]}
*}
ML {*
val thms_f = map (lift_thm @{context} qtys) @{thms bn_defs}
*}
ML {*
val thms_f = map (lift_thm @{context} qtys) @{thms bn_eqvt}
*}
ML {*
val thms_f = map (lift_thm @{context} qtys) @{thms fv_eqvt}
*}
ML {*
val thms_f = map (lift_thm @{context} qtys) @{thms size_eqvt}
*}
lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm
lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.eq_iff
lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts
lemmas alpha_inducts=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.inducts
lemmas alpha_intros=alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.intros
lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)"
unfolding fresh_star_def Ball_def
by auto (simp_all add: fresh_minus_perm)
primrec permute_bv_vs_raw
where "permute_bv_vs_raw p VsNil_raw = VsNil_raw"
| "permute_bv_vs_raw p (VsCons_raw v t l) = VsCons_raw (p \<bullet> v) t (permute_bv_vs_raw p l)"
primrec permute_bv_cvs_raw
where "permute_bv_cvs_raw p CvsNil_raw = CvsNil_raw"
| "permute_bv_cvs_raw p (CvsCons_raw v t l) = CvsCons_raw (p \<bullet> v) t (permute_bv_cvs_raw p l)"
primrec permute_bv_tvs_raw
where "permute_bv_tvs_raw p TvsNil_raw = TvsNil_raw"
| "permute_bv_tvs_raw p (TvsCons_raw v t l) = TvsCons_raw (p \<bullet> v) t (permute_bv_tvs_raw p l)"
primrec permute_bv_raw
where "permute_bv_raw p (Kpat_raw c l1 l2 l3) =
Kpat_raw c (permute_bv_tvs_raw p l1) (permute_bv_cvs_raw p l2) (permute_bv_vs_raw p l3)"
quotient_definition "permute_bv_vs :: perm \<Rightarrow> vars \<Rightarrow> vars"
is "permute_bv_vs_raw"
quotient_definition "permute_bv_cvs :: perm \<Rightarrow> cvars \<Rightarrow> cvars"
is "permute_bv_cvs_raw"
quotient_definition "permute_bv_tvs :: perm \<Rightarrow> tvars \<Rightarrow> tvars"
is "permute_bv_tvs_raw"
quotient_definition "permute_bv :: perm \<Rightarrow> pat \<Rightarrow> pat"
is "permute_bv_raw"
lemma rsp_pre:
"alpha_tvars_raw d a \<Longrightarrow> alpha_tvars_raw (permute_bv_tvs_raw x d) (permute_bv_tvs_raw x a)"
"alpha_cvars_raw e b \<Longrightarrow> alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)"
"alpha_vars_raw f c \<Longrightarrow> alpha_vars_raw (permute_bv_vs_raw x f) (permute_bv_vs_raw x c)"
apply (erule_tac [!] alpha_inducts)
apply (simp_all only: alpha_intros perm permute_bv_tvs_raw.simps permute_bv_cvs_raw.simps permute_bv_vs_raw.simps)
done
lemma [quot_respect]:
"(op = ===> alpha_pat_raw ===> alpha_pat_raw) permute_bv_raw permute_bv_raw"
"(op = ===> alpha_tvars_raw ===> alpha_tvars_raw) permute_bv_tvs_raw permute_bv_tvs_raw"
"(op = ===> alpha_cvars_raw ===> alpha_cvars_raw) permute_bv_cvs_raw permute_bv_cvs_raw"
"(op = ===> alpha_vars_raw ===> alpha_vars_raw) permute_bv_vs_raw permute_bv_vs_raw"
apply (simp_all add: rsp_pre)
apply clarify
apply (erule_tac alpha_inducts)
apply (simp_all)
apply (rule alpha_intros)
apply (simp_all add: rsp_pre)
done
thm permute_bv_raw.simps[no_vars]
permute_bv_vs_raw.simps[quot_lifted]
permute_bv_cvs_raw.simps[quot_lifted]
permute_bv_tvs_raw.simps[quot_lifted]
lemma permute_bv_pre:
"permute_bv p (Kpat c l1 l2 l3) =
Kpat c (permute_bv_tvs p l1) (permute_bv_cvs p l2) (permute_bv_vs p l3)"
by (lifting permute_bv_raw.simps)
lemmas permute_bv[simp] =
permute_bv_pre
permute_bv_vs_raw.simps[quot_lifted]
permute_bv_cvs_raw.simps[quot_lifted]
permute_bv_tvs_raw.simps[quot_lifted]
lemma perm_bv1:
"p \<bullet> bv_cvs b = bv_cvs (permute_bv_cvs p b)"
"p \<bullet> bv_tvs c = bv_tvs (permute_bv_tvs p c)"
"p \<bullet> bv_vs d = bv_vs (permute_bv_vs p d)"
apply(induct b rule: inducts(12))
apply(simp_all add:permute_bv eqvts)
apply(induct c rule: inducts(11))
apply(simp_all add:permute_bv eqvts)
apply(induct d rule: inducts(10))
apply(simp_all add:permute_bv eqvts)
done
lemma perm_bv2:
"p \<bullet> bv l = bv (permute_bv p l)"
apply(induct l rule: inducts(9))
apply(simp_all add:permute_bv)
apply(simp add: perm_bv1[symmetric])
apply(simp add: eqvts)
done
lemma alpha_perm_bn1:
"alpha_bv_tvs tvars (permute_bv_tvs q tvars)"
"alpha_bv_cvs cvars (permute_bv_cvs q cvars)"
"alpha_bv_vs vars (permute_bv_vs q vars)"
apply(induct tvars rule: inducts(11))
apply(simp_all add:permute_bv eqvts eq_iff)
apply(induct cvars rule: inducts(12))
apply(simp_all add:permute_bv eqvts eq_iff)
apply(induct vars rule: inducts(10))
apply(simp_all add:permute_bv eqvts eq_iff)
done
lemma alpha_perm_bn:
"alpha_bv pt (permute_bv q pt)"
apply(induct pt rule: inducts(9))
apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1)
done
lemma ACons_subst:
"supp (Abs_lst (bv pt) trm) \<sharp>* q \<Longrightarrow> (ACons pt trm al) = ACons (permute_bv q pt) (q \<bullet> trm) al"
apply (simp only: eq_iff)
apply (simp add: alpha_perm_bn)
apply (rule_tac x="q" in exI)
apply (simp add: alphas)
apply (simp add: perm_bv2[symmetric])
apply (simp add: supp_abs)
apply (simp add: fv_supp)
apply (simp add: supp_eqvt[symmetric] set_eqvt[symmetric] Diff_eqvt[symmetric])
apply (rule supp_perm_eq[symmetric])
apply (subst supp_finite_atom_set)
apply (rule finite_Diff)
apply (simp add: finite_supp)
apply (assumption)
done
lemma permute_bv_zero1:
"permute_bv_cvs 0 b = b"
"permute_bv_tvs 0 c = c"
"permute_bv_vs 0 d = d"
apply(induct b rule: inducts(12))
apply(simp_all add:permute_bv eqvts)
apply(induct c rule: inducts(11))
apply(simp_all add:permute_bv eqvts)
apply(induct d rule: inducts(10))
apply(simp_all add:permute_bv eqvts)
done
lemma permute_bv_zero2:
"permute_bv 0 a = a"
apply(induct a rule: inducts(9))
apply(simp_all add:permute_bv eqvts permute_bv_zero1)
done
lemma fv_alpha1: "fv_bv_tvs x \<sharp>* pa \<Longrightarrow> alpha_bv_tvs (pa \<bullet> x) x"
apply (induct x rule: inducts(11))
apply (simp_all add: eq_iff fresh_star_union)
done
lemma fv_alpha2: "fv_bv_cvs x \<sharp>* pa \<Longrightarrow> alpha_bv_cvs (pa \<bullet> x) x"
apply (induct x rule: inducts(12))
apply (rule TrueI)+
apply (simp_all add: eq_iff fresh_star_union)
apply (subst supp_perm_eq)
apply (simp_all add: fv_supp)
done
lemma fv_alpha3: "fv_bv_vs x \<sharp>* pa \<Longrightarrow> alpha_bv_vs (pa \<bullet> x) x"
apply (induct x rule: inducts(10))
apply (rule TrueI)+
apply (simp_all add: fresh_star_union eq_iff)
apply (subst supp_perm_eq)
apply (simp_all add: fv_supp)
done
lemma fv_alpha: "fv_bv x \<sharp>* pa \<Longrightarrow> alpha_bv (pa \<bullet> x) x"
apply (induct x rule: inducts(9))
apply (rule TrueI)+
apply (simp_all add: eq_iff fresh_star_union)
apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3)
apply (subst supp_perm_eq)
apply (simp_all add: fv_supp)
done
lemma fin1: "finite (fv_bv_tvs x)"
apply (induct x rule: inducts(11))
apply (simp_all add: fv_supp finite_supp)
done
lemma fin2: "finite (fv_bv_cvs x)"
apply (induct x rule: inducts(12))
apply (simp_all add: fv_supp finite_supp)
done
lemma fin3: "finite (fv_bv_vs x)"
apply (induct x rule: inducts(10))
apply (simp_all add: fv_supp finite_supp)
done
lemma fin_fv_bv: "finite (fv_bv x)"
apply (induct x rule: inducts(9))
apply (rule TrueI)+
defer
apply (rule TrueI)+
apply (simp add: fin1 fin2 fin3)
apply (rule finite_supp)
done
lemma finb1: "finite (set (bv_tvs x))"
apply (induct x rule: inducts(11))
apply (simp_all add: fv_supp finite_supp)
done
lemma finb2: "finite (set (bv_cvs x))"
apply (induct x rule: inducts(12))
apply (simp_all add: fv_supp finite_supp)
done
lemma finb3: "finite (set (bv_vs x))"
apply (induct x rule: inducts(10))
apply (simp_all add: fv_supp finite_supp)
done
lemma fin_bv: "finite (set (bv x))"
apply (induct x rule: inducts(9))
apply (simp_all add: finb1 finb2 finb3)
done
lemma strong_induction_principle:
assumes a01: "\<And>b. P1 b KStar"
and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"
and a04: "\<And>tvar b. P3 b (TVar tvar)"
and a05: "\<And>string b. P3 b (TC string)"
and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)"
and a07: "\<And>string ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun string ty_lst)"
and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty; atom tvar \<sharp> b\<rbrakk>
\<Longrightarrow> P3 b (TAll tvar tkind ty)"
and a09: "\<And>ck ty b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P3 b (TEq ck ty)"
and a10: "\<And>b. P4 b TsNil"
and a11: "\<And>ty ty_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P4 b (TsCons ty ty_lst)"
and a12: "\<And>string b. P5 b (CVar string)"
and a12a:"\<And>str b. P5 b (CConst str)"
and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)"
and a14: "\<And>string co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun string co_lst)"
and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co; atom tvar \<sharp> b\<rbrakk>
\<Longrightarrow> P5 b (CAll tvar ckind co)"
and a16: "\<And>ck co b. \<lbrakk>\<And>c. P2 c ck; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CEq ck co)"
and a17: "\<And>ty b. \<lbrakk>\<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CRefl ty)"
and a17a: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)"
and a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)"
and a18a:"\<And>co ty b. \<lbrakk>\<And>c. P5 c co; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P5 b (CAt co ty)"
and a19: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeft co)"
and a20: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRight co)"
and a21: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CSim co1 co2)"
and a22: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRightc co)"
and a23: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeftc co)"
and a24: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCoe co1 co2)"
and a25: "\<And>b. P6 b CsNil"
and a26: "\<And>co co_lst b. \<lbrakk>\<And>c. P5 c co; \<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P6 b (CsCons co co_lst)"
and a27: "\<And>var b. P7 b (Var var)"
and a28: "\<And>string b. P7 b (K string)"
and a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
\<Longrightarrow> P7 b (LAMT tvar tkind trm)"
and a30: "\<And>tvar ckind trm b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P7 c trm; atom tvar \<sharp> b\<rbrakk>
\<Longrightarrow> P7 b (LAMC tvar ckind trm)"
and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (AppT trm ty)"
and a31a:"\<And>trm co b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P7 b (AppC trm co)"
and a32: "\<And>var ty trm b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm; atom var \<sharp> b\<rbrakk> \<Longrightarrow> P7 b (Lam var ty trm)"
and a33: "\<And>trm1 trm2 b. \<lbrakk>\<And>c. P7 c trm1; \<And>c. P7 c trm2\<rbrakk> \<Longrightarrow> P7 b (App trm1 trm2)"
and a34: "\<And>var ty trm1 trm2 b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm1; \<And>c. P7 c trm2; atom var \<sharp> b\<rbrakk>
\<Longrightarrow> P7 b (Let var ty trm1 trm2)"
and a35: "\<And>trm assoc_lst b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P8 c assoc_lst\<rbrakk> \<Longrightarrow> P7 b (Case trm assoc_lst)"
and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)"
and a37: "\<And>b. P8 b ANil"
and a38: "\<And>pt trm assoc_lst b. \<lbrakk>\<And>c. P9 c pt; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pt)) \<sharp>* b\<rbrakk>
\<Longrightarrow> P8 b (ACons pt trm assoc_lst)"
and a39: "\<And>string tvars cvars vars b. \<lbrakk>\<And>c. P11 c tvars; \<And>c. P12 c cvars; \<And>c. P10 c vars\<rbrakk>
\<Longrightarrow> P9 b (Kpat string tvars cvars vars)"
and a40: "\<And>b. P10 b VsNil"
and a41: "\<And>var ty vars b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vars\<rbrakk> \<Longrightarrow> P10 b (VsCons var ty vars)"
and a42: "\<And>b. P11 b TvsNil"
and a43: "\<And>tvar tkind tvars b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvars\<rbrakk>
\<Longrightarrow> P11 b (TvsCons tvar tkind tvars)"
and a44: "\<And>b. P12 b CvsNil"
and a45: "\<And>tvar ckind cvars b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c cvars\<rbrakk>
\<Longrightarrow> P12 b (CvsCons tvar ckind cvars)"
shows "P1 (a :: 'a :: pt) tkind \<and>
P2 (b :: 'b :: pt) ckind \<and>
P3 (c :: 'c :: {pt,fs}) ty \<and>
P4 (d :: 'd :: pt) ty_lst \<and>
P5 (e :: 'e :: {pt,fs}) co \<and>
P6 (f :: 'f :: pt) co_lst \<and>
P7 (g :: 'g :: {pt,fs}) trm \<and>
P8 (h :: 'h :: {pt,fs}) assoc_lst \<and>
P9 (i :: 'i :: pt) pt \<and>
P10 (j :: 'j :: pt) vars \<and>
P11 (k :: 'k :: pt) tvars \<and>
P12 (l :: 'l :: pt) cvars"
proof -
have a1: "(\<forall>p a. P1 a (p \<bullet> tkind))" and "(\<forall>p b. P2 b (p \<bullet> ckind))" and "(\<forall>p c. P3 c (p \<bullet> ty))" and "(\<forall>p d. P4 d (p \<bullet> ty_lst))" and "(\<forall>p e. P5 e (p \<bullet> co))" and " (\<forall>p f. P6 f (p \<bullet> co_lst))" and "(\<forall>p g. P7 g (p \<bullet> trm))" and "(\<forall>p h. P8 h (p \<bullet> assoc_lst))" and a1:"(\<forall>p q i. P9 i (permute_bv p (q \<bullet> pt)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vs q (p \<bullet> vars)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvs q (p \<bullet> tvars)))" and a4:"(\<forall>p q l. P12 l (permute_bv_cvs q (p \<bullet> cvars)))"
apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts)
apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})
apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})
(* GOAL1 *)
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and>
supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)")
apply clarify
apply (simp only: perm)
apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)"
and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst)
apply (simp add: eq_iff)
apply (rule_tac x="-pa" in exI)
apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}"
and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst)
apply (simp add: eqvts)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
apply (rule conjI)
apply (rule supp_perm_eq)
apply (simp add: eqvts)
apply (subst supp_finite_atom_set)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
apply (simp add: eqvts)
apply (subst supp_perm_eq)
apply (subst supp_finite_atom_set)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
apply assumption
apply (simp add: fresh_star_minus_perm)
apply (rule a08)
apply simp
apply(rotate_tac 1)
apply(erule_tac x="(pa + p)" in allE)
apply simp
apply (simp add: eqvts eqvts_raw)
apply (rule at_set_avoiding2_atom)
apply (simp add: finite_supp)
apply (simp add: finite_supp)
apply (simp add: fresh_def)
apply (simp only: supp_abs eqvts)
apply blast
(* GOAL2 *)
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> e \<and>
supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> co)) \<sharp>* pa)")
apply clarify
apply (simp only: perm)
apply(rule_tac t="CAll (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> co)"
and s="CAll (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst)
apply (simp add: eq_iff)
apply (rule_tac x="-pa" in exI)
apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}"
and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom cvar})" in subst)
apply (simp add: eqvts)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
apply (rule conjI)
apply (rule supp_perm_eq)
apply (simp add: eqvts)
apply (subst supp_finite_atom_set)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
apply (simp add: eqvts)
apply (subst supp_perm_eq)
apply (subst supp_finite_atom_set)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
apply assumption
apply (simp add: fresh_star_minus_perm)
apply (rule a15)
apply simp
apply(rotate_tac 1)
apply(erule_tac x="(pa + p)" in allE)
apply simp
apply (simp add: eqvts eqvts_raw)
apply (rule at_set_avoiding2_atom)
apply (simp add: finite_supp)
apply (simp add: finite_supp)
apply (simp add: fresh_def)
apply (simp only: supp_abs eqvts)
apply blast
(* GOAL3 a copy-and-paste of Goal2 with consts and variable names changed *)
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and>
supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)")
apply clarify
apply (simp only: perm)
apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)"
and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst)
apply (simp add: eq_iff)
apply (rule_tac x="-pa" in exI)
apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst)
apply (simp add: eqvts)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
apply (rule conjI)
apply (rule supp_perm_eq)
apply (simp add: eqvts)
apply (subst supp_finite_atom_set)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
apply (simp add: eqvts)
apply (subst supp_perm_eq)
apply (subst supp_finite_atom_set)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
apply assumption
apply (simp add: fresh_star_minus_perm)
apply (rule a29)
apply simp
apply(rotate_tac 1)
apply(erule_tac x="(pa + p)" in allE)
apply simp
apply (simp add: eqvts eqvts_raw)
apply (rule at_set_avoiding2_atom)
apply (simp add: finite_supp)
apply (simp add: finite_supp)
apply (simp add: fresh_def)
apply (simp only: supp_abs eqvts)
apply blast
(* GOAL4 a copy-and-paste *)
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> cvar))) \<sharp> g \<and>
supp (Abs (p \<bullet> {atom cvar}) (p \<bullet> trm)) \<sharp>* pa)")
apply clarify
apply (simp only: perm)
apply(rule_tac t="LAMC (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> trm)"
and s="LAMC (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst)
apply (simp add: eq_iff)
apply (rule_tac x="-pa" in exI)
apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}"
and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom cvar})" in subst)
apply (simp add: eqvts)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
apply (rule conjI)
apply (rule supp_perm_eq)
apply (simp add: eqvts)
apply (subst supp_finite_atom_set)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
apply (simp add: eqvts)
apply (subst supp_perm_eq)
apply (subst supp_finite_atom_set)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
apply assumption
apply (simp add: fresh_star_minus_perm)
apply (rule a30)
apply simp
apply(rotate_tac 1)
apply(erule_tac x="(pa + p)" in allE)
apply simp
apply (simp add: eqvts eqvts_raw)
apply (rule at_set_avoiding2_atom)
apply (simp add: finite_supp)
apply (simp add: finite_supp)
apply (simp add: fresh_def)
apply (simp only: supp_abs eqvts)
apply blast
(* GOAL5 a copy-and-paste *)
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm)) \<sharp>* pa)")
apply clarify
apply (simp only: perm)
apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)"
and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst)
apply (simp add: eq_iff)
apply (rule_tac x="-pa" in exI)
apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}"
and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst)
apply (simp add: eqvts)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
apply (rule conjI)
apply (rule supp_perm_eq)
apply (simp add: eqvts)
apply (subst supp_finite_atom_set)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
apply (simp add: eqvts)
apply (subst supp_perm_eq)
apply (subst supp_finite_atom_set)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
apply assumption
apply (simp add: fresh_star_minus_perm)
apply (rule a32)
apply simp
apply(rotate_tac 1)
apply(erule_tac x="(pa + p)" in allE)
apply simp
apply (simp add: eqvts eqvts_raw)
apply (rule at_set_avoiding2_atom)
apply (simp add: finite_supp)
apply (simp add: finite_supp)
apply (simp add: fresh_def)
apply (simp only: supp_abs eqvts)
apply blast
(* GOAL6 a copy-and-paste *)
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm2)) \<sharp>* pa)")
apply clarify
apply (simp only: perm)
apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)"
and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst)
apply (simp add: eq_iff)
apply (rule_tac x="-pa" in exI)
apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}"
and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst)
apply (simp add: eqvts)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
apply (rule conjI)
apply (rule supp_perm_eq)
apply (simp add: eqvts)
apply (subst supp_finite_atom_set)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
apply (simp add: eqvts)
apply (subst supp_perm_eq)
apply (subst supp_finite_atom_set)
apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
apply assumption
apply (simp add: fresh_star_minus_perm)
apply (rule a34)
apply simp
apply simp
apply(rotate_tac 2)
apply(erule_tac x="(pa + p)" in allE)
apply simp
apply (simp add: eqvts eqvts_raw)
apply (rule at_set_avoiding2_atom)
apply (simp add: finite_supp)
apply (simp add: finite_supp)
apply (simp add: fresh_def)
apply (simp only: supp_abs eqvts)
apply blast
(* MAIN ACons Goal *)
apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (set (bv (p \<bullet> pat)))) \<sharp>* h \<and>
supp (Abs_lst (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)")
apply clarify
apply (simp only: perm eqvts)
apply (subst ACons_subst)
apply assumption
apply (rule a38)
apply simp
apply(rotate_tac 1)
apply(erule_tac x="(pa + p)" in allE)
apply simp
apply simp
apply (simp add: perm_bv2[symmetric])
apply (simp add: eqvts eqvts_raw)
apply (rule at_set_avoiding2)
apply (simp add: fin_bv)
apply (simp add: finite_supp)
apply (simp add: supp_abs)
apply (simp add: finite_supp)
apply (simp add: fresh_star_def fresh_def supp_abs eqvts)
done
then have b: "P1 a (0 \<bullet> tkind)" and "P2 b (0 \<bullet> ckind)" "P3 c (0 \<bullet> ty)" and "P4 d (0 \<bullet> ty_lst)" and "P5 e (0 \<bullet> co)" and "P6 f (0 \<bullet> co_lst)" and "P7 g (0 \<bullet> trm)" and "P8 h (0 \<bullet> assoc_lst)" by (blast+)
moreover have "P9 i (permute_bv 0 (0 \<bullet> pt))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+)
ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
qed
section {* test about equivariance for alpha *}
(* this should not be an equivariance rule *)
(* for the moment, we force it to be *)
(*declare permute_pure[eqvt]*)
(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} *)
thm eqvts
thm eqvts_raw
end