--- a/Attic/Quot/Examples/LFex.thy Mon May 10 15:44:49 2010 +0200
+++ b/Attic/Quot/Examples/LFex.thy Mon May 10 15:45:04 2010 +0200
@@ -251,16 +251,50 @@
((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and>
((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
-apply(lifting akind_aty_atrm.induct)
-(*
-Profiling:
-ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}
-ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *}
-ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *}
-ML_prf {* PolyML.profiling 1 *}
-ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}
-*)
- done
+apply(lifting_setup akind_aty_atrm.induct)
+defer
+apply injection
+apply cleaning
+apply (simp only: ball_reg_eqv[OF KIND_equivp] ball_reg_eqv[OF TRM_equivp] ball_reg_eqv[OF TY_equivp])
+apply (rule ball_reg_right)+
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply simp
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply simp
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply simp
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply simp
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply simp
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply simp
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply simp
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+defer
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+defer
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+defer
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply simp
+apply (tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+apply simp
+apply simp
+apply regularize+
+done
(* Does not work:
lemma
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/Quot/Examples/Pair.thy Mon May 10 15:45:04 2010 +0200
@@ -0,0 +1,120 @@
+theory Pair
+imports Quotient_Product "../../../Nominal/FSet"
+begin
+
+fun alpha :: "('a \<times> 'a) \<Rightarrow> ('a \<times> 'a) \<Rightarrow> bool" (infix "\<approx>" 100)
+where
+ "(a, b) \<approx> (c, d) = (a = c \<and> b = d \<or> a = d \<and> b = c)"
+
+lemma alpha_refl:
+ shows "z \<approx> z"
+ by (case_tac z, auto)
+
+lemma alpha_equivp:
+ shows "equivp op \<approx>"
+ unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
+ by auto
+
+quotient_type
+ 'a pair_set = "'a \<times> 'a" / alpha
+ by (auto intro: alpha_equivp)
+
+quotient_definition
+ "Two :: 'a \<Rightarrow> 'a \<Rightarrow> 'a pair_set"
+is
+ "Pair :: 'a \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'a)"
+
+fun
+ memb_both_lists
+where
+ "memb_both_lists a (b, c) = (memb a b \<and> memb a c)"
+
+quotient_definition
+ "mem_fsets :: 'a \<Rightarrow> 'a fset pair_set \<Rightarrow> bool"
+is memb_both_lists
+
+lemma prod_hlp: "prod_fun abs_fset abs_fset (prod_fun rep_fset rep_fset x) = x"
+ by (cases x, auto simp add: Quotient_abs_rep[OF Quotient_fset])
+
+lemma prod_hlp2:
+ "prod_rel list_eq list_eq (prod_fun rep_fset rep_fset z) (prod_fun rep_fset rep_fset z)"
+ by (cases z, simp)
+
+lemma [quot_thm]:
+ shows "Quotient ((op \<approx>) OOO (prod_rel list_eq list_eq))
+ (abs_pair_set \<circ> prod_fun abs_fset abs_fset)
+ (prod_fun rep_fset rep_fset \<circ> rep_pair_set)"
+ unfolding Quotient_def comp_def
+ apply (intro conjI allI)
+ apply (simp add: prod_hlp Quotient_abs_rep[OF Quotient_pair_set])
+ apply rule
+ apply (rule alpha_refl)
+ apply rule
+ apply (rule prod_hlp2)
+ apply (rule alpha_refl)
+ apply (intro iffI conjI)
+ sorry
+
+lemma [quot_respect]:
+ "(op = ===> op \<approx> OOO prod_rel list_eq list_eq ===> op =) memb_both_lists memb_both_lists"
+ apply (intro fun_relI)
+ apply clarify
+ apply (simp only: memb_both_lists.simps)
+ sorry
+
+lemma [quot_respect]:
+ "(list_eq ===> list_eq ===> op \<approx> OOO prod_rel list_eq list_eq) Pair Pair"
+ apply (intro fun_relI)
+ apply rule
+ apply (rule alpha_refl)
+ apply rule
+ prefer 2
+ apply (rule alpha_refl)
+ apply simp
+ done
+
+lemma [quot_preserve]:
+ "(rep_fset ---> rep_fset ---> abs_pair_set \<circ> prod_fun abs_fset abs_fset) Pair = Two"
+ by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] Two_def)
+
+lemma "mem_fsets a (Two b c) = (a |\<in>| b \<and> a |\<in>| c)"
+ by (lifting memb_both_lists.simps)
+
+(* Doing it in 2 steps *)
+
+quotient_definition
+ "mem_lists :: 'a \<Rightarrow> 'a list pair_set \<Rightarrow> bool"
+is memb_both_lists
+
+lemma [quot_respect]: "(op = ===> op \<approx> ===> op =) memb_both_lists memb_both_lists"
+ by auto
+
+lemma [quot_respect]: "(op = ===> op = ===> op \<approx>) Pair Pair"
+ by auto
+
+lemma step1: "mem_lists a (Two b c) = (memb a b \<and> memb a c)"
+ by (lifting memb_both_lists.simps)
+
+lemma step2: "mem_fsets a (Two b c) = (a |\<in>| b \<and> a |\<in>| c)"
+ (* apply (lifting step1) ??? *)
+ oops
+
+(* Doing it in 2 steps the other way *)
+
+quotient_definition
+ "memb_both_fsets :: 'a \<Rightarrow> 'a fset \<times> 'a fset \<Rightarrow> bool"
+is memb_both_lists
+
+lemma [quot_respect]:
+ "(op = ===> prod_rel list_eq list_eq ===> op =) memb_both_lists memb_both_lists"
+ by (auto simp add: memb_def[symmetric])
+
+lemma bla: "memb_both_fsets a (b, c) = (a |\<in>| b \<and> a |\<in>| c)"
+ by (lifting memb_both_lists.simps)
+
+lemma step2: "mem_fsets a (Two b c) = (a |\<in>| b \<and> a |\<in>| c)"
+ (* ??? *)
+ oops
+
+end
+
--- a/Nominal-General/Nominal2_Eqvt.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy Mon May 10 15:45:04 2010 +0200
@@ -280,6 +280,11 @@
"p \<bullet> (snd x) = snd (p \<bullet> x)"
by (cases x) simp
+lemma split_eqvt[eqvt]:
+ shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
+ unfolding split_def
+ by (perm_simp) (rule refl)
+
section {* Units *}
lemma supp_unit:
@@ -386,10 +391,16 @@
lemma
fixes P :: "(('b \<Rightarrow> bool) \<Rightarrow> ('b::pt)) \<Rightarrow> ('a::pt)"
- shows "(p \<bullet> (P The)) = foo"
+ shows "p \<bullet> (P The) = foo"
apply(perm_simp exclude: The)
oops
+lemma
+ fixes P :: "('a::pt) \<Rightarrow> ('b::pt) \<Rightarrow> bool"
+ shows "p \<bullet> (\<lambda>(a, b). P a b) = (\<lambda>(a, b). (p \<bullet> P) a b)"
+apply(perm_simp)
+oops
+
thm eqvts
thm eqvts_raw
--- a/Nominal-General/nominal_eqvt.ML Mon May 10 15:44:49 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML Mon May 10 15:45:04 2010 +0200
@@ -52,9 +52,10 @@
fun map_thm_tac ctxt tac thm =
let
val monos = Inductive.get_monos ctxt
+ val simps = HOL_basic_ss addsimps @{thms split_def}
in
- EVERY [cut_facts_tac [thm] 1, etac rev_mp 1,
- REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)),
+ EVERY [cut_facts_tac [thm] 1, etac rev_mp 1,
+ REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)),
REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]
end
@@ -89,25 +90,25 @@
val perm_boolE = @{thm permute_boolE}
val perm_cancel = @{thms permute_minus_cancel(2)}
-val perm_expand_bool = @{thms permute_fun_def minus_minus permute_bool_def}
fun eqvt_rel_single_case_tac ctxt pred_names pi intro =
let
val thy = ProofContext.theory_of ctxt
val cpi = Thm.cterm_of thy (mk_minus pi)
val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE
- val simps = HOL_basic_ss addsimps perm_expand_bool
+ val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all}
+ val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def}
in
- eqvt_strict_tac ctxt [] pred_names THEN'
+ eqvt_strict_tac ctxt [] pred_names THEN'
SUBPROOF (fn {prems, context as ctxt, ...} =>
let
val prems' = map (transform_prem ctxt pred_names) prems
-
val tac1 = resolve_tac prems'
val tac2 = EVERY' [ rtac pi_intro_rule,
eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ]
val tac3 = EVERY' [ rtac pi_intro_rule,
- eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps, resolve_tac prems']
+ eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps1,
+ simp_tac simps2, resolve_tac prems']
in
(rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1
end) ctxt
--- a/Nominal-General/nominal_permeq.ML Mon May 10 15:44:49 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML Mon May 10 15:45:04 2010 +0200
@@ -23,18 +23,11 @@
the string list contains constants that should not be
analysed (for example there is no raw eqvt-lemma for
- the constant The; therefore it should not be analysed
+ the constant The); therefore it should not be analysed
- setting [[trace_eqvt = true]] switches on tracing
information
-
-TODO:
-
- - provide a proper parser for the method (see Nominal2_Eqvt)
-
- - proably the list of bad constant should be a dataslot
-
*)
structure Nominal_Permeq: NOMINAL_PERMEQ =
@@ -76,17 +69,10 @@
Conv.no_conv ctrm
end
-(* conversion for applications:
- only applies the conversion, if the head of the
- application is not a "bad head" *)
-fun has_bad_head bad_hds trm =
- case (head_of trm) of
- Const (s, _) => member (op=) bad_hds s
- | _ => false
-
-fun eqvt_apply_conv bad_hds ctrm =
+(* conversion for applications *)
+fun eqvt_apply_conv ctrm =
case (term_of ctrm) of
- Const (@{const_name "permute"}, _) $ _ $ (trm $ _) =>
+ Const (@{const_name "permute"}, _) $ _ $ (_ $ _) =>
let
val (perm, t) = Thm.dest_comb ctrm
val (_, p) = Thm.dest_comb perm
@@ -96,9 +82,7 @@
val ty_insts = map SOME [b, a]
val term_insts = map SOME [p, f, x]
in
- if has_bad_head bad_hds trm
- then Conv.all_conv ctrm
- else Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
+ Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
end
| _ => Conv.no_conv ctrm
@@ -109,18 +93,19 @@
Conv.rewr_conv @{thm eqvt_lambda} ctrm
| _ => Conv.no_conv ctrm
+
(* conversion that raises an error or prints a warning message,
if a permutation on a constant or application cannot be analysed *)
-fun progress_info_conv ctxt strict_flag bad_hds ctrm =
+
+fun is_excluded excluded (Const (a, _)) = member (op=) excluded a
+ | is_excluded _ _ = false
+
+fun progress_info_conv ctxt strict_flag excluded ctrm =
let
fun msg trm =
- let
- val hd = head_of trm
- in
- if is_Const hd andalso member (op =) bad_hds (fst (dest_Const hd)) then ()
- else (if strict_flag then error else warning)
- ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
- end
+ if is_excluded excluded trm then () else
+ (if strict_flag then error else warning)
+ ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
val _ = case (term_of ctrm) of
Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm
@@ -131,7 +116,7 @@
end
(* main conversion *)
-fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm =
+fun eqvt_conv ctxt strict_flag user_thms excluded ctrm =
let
val first_conv_wrapper =
if trace_enabled ctxt
@@ -143,10 +128,10 @@
in
first_conv_wrapper
[ More_Conv.rewrs_conv pre_thms,
- eqvt_apply_conv bad_hds,
+ eqvt_apply_conv,
eqvt_lambda_conv,
More_Conv.rewrs_conv post_thms,
- progress_info_conv ctxt strict_flag bad_hds
+ progress_info_conv ctxt strict_flag excluded
] ctrm
end
@@ -155,14 +140,14 @@
equivaraince command. *)
(* raises an error if some permutations cannot be eliminated *)
-fun eqvt_strict_tac ctxt user_thms bad_hds =
+fun eqvt_strict_tac ctxt user_thms excluded =
CONVERSION (More_Conv.top_conv
- (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms bad_hds)) ctxt)
+ (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms excluded)) ctxt)
(* prints a warning message if some permutations cannot be eliminated *)
-fun eqvt_tac ctxt user_thms bad_hds =
+fun eqvt_tac ctxt user_thms excluded =
CONVERSION (More_Conv.top_conv
- (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms bad_hds)) ctxt)
+ (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms excluded)) ctxt)
(* setup of the configuration value *)
val setup =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/CoreHaskell.thy Mon May 10 15:45:04 2010 +0200
@@ -0,0 +1,673 @@
+theory CoreHaskell
+imports "../NewParser"
+begin
+
+(* core haskell *)
+
+atom_decl var
+atom_decl cvar
+atom_decl tvar
+
+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 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 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 tv in t
+| LAMC cv::"cvar" "ckind" t::"trm" bind cv in t
+| AppT "trm" "ty"
+| AppC "trm" "co"
+| Lam v::"var" "ty" t::"trm" bind v in t
+| App "trm" "trm"
+| Let x::"var" "ty" "trm" t::"trm" bind 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"
+
+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 pat (permute_bv q pat)"
+ apply(induct pat rule: inducts(9))
+ apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1)
+ done
+
+lemma ACons_subst:
+ "supp (Abs_lst (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (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: eqvts[symmetric])
+ apply (simp add: supp_abs)
+ apply (simp add: fv_supp)
+ 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>pat trm assoc_lst b. \<lbrakk>\<And>c. P9 c pat; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pat)) \<sharp>* b\<rbrakk>
+ \<Longrightarrow> P8 b (ACons pat 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) pat \<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> pat)))" 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: eqvts[symmetric])
+ apply (rule conjI)
+ apply (rule supp_perm_eq)
+ apply (simp add: eqvts)
+ apply (subst supp_finite_atom_set)
+ apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+ apply (simp add: eqvts)
+ apply (simp add: eqvts)
+ apply (subst supp_perm_eq)
+ apply (subst supp_finite_atom_set)
+ apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+ apply (simp add: eqvts)
+ 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: eqvts[symmetric])
+ apply (rule conjI)
+ apply (rule supp_perm_eq)
+ apply (simp add: eqvts)
+ apply (subst supp_finite_atom_set)
+ apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+ apply (simp add: eqvts)
+ apply (simp add: eqvts)
+ apply (subst supp_perm_eq)
+ apply (subst supp_finite_atom_set)
+ apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+ apply (simp add: eqvts)
+ 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: eqvts[symmetric])
+ apply (rule conjI)
+ apply (rule supp_perm_eq)
+ apply (simp add: eqvts)
+ apply (subst supp_finite_atom_set)
+ apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+ apply (simp add: eqvts)
+ apply (simp add: eqvts)
+ apply (subst supp_perm_eq)
+ apply (subst supp_finite_atom_set)
+ apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+ apply (simp add: eqvts)
+ 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: eqvts[symmetric])
+ apply (rule conjI)
+ apply (rule supp_perm_eq)
+ apply (simp add: eqvts)
+ apply (subst supp_finite_atom_set)
+ apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+ apply (simp add: eqvts)
+ apply (simp add: eqvts)
+ apply (subst supp_perm_eq)
+ apply (subst supp_finite_atom_set)
+ apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+ apply (simp add: eqvts)
+ 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: eqvts[symmetric])
+ apply (rule conjI)
+ apply (rule supp_perm_eq)
+ apply (simp add: eqvts)
+ apply (subst supp_finite_atom_set)
+ apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+ apply (simp add: eqvts)
+ apply (simp add: eqvts)
+ apply (subst supp_perm_eq)
+ apply (subst supp_finite_atom_set)
+ apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+ apply (simp add: eqvts)
+ 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: eqvts[symmetric])
+ apply (rule conjI)
+ apply (rule supp_perm_eq)
+ apply (simp add: eqvts)
+ apply (subst supp_finite_atom_set)
+ apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+ apply (simp add: eqvts)
+ apply (simp add: eqvts)
+ apply (subst supp_perm_eq)
+ apply (subst supp_finite_atom_set)
+ apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+ apply (simp add: eqvts)
+ 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> pat))" 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
+
+declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_tkind_raw
+
+thm eqvts
+thm eqvts_raw
+
+end
+
--- a/Nominal/Ex/Ex1rec.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/Ex1rec.thy Mon May 10 15:45:04 2010 +0200
@@ -29,10 +29,11 @@
ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
thm lam_bp.fv[simplified lam_bp.supp(1-2)]
-(*declare permute_lam_raw_permute_bp_raw.simps[eqvt]
+declare permute_lam_raw_permute_bp_raw.simps[eqvt]
declare alpha_gen_eqvt[eqvt]
+
equivariance alpha_lam_raw
-*)
+
end
--- a/Nominal/Ex/Ex2.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/Ex2.thy Mon May 10 15:45:04 2010 +0200
@@ -27,6 +27,12 @@
thm trm_pat.distinct
thm trm_pat.fv[simplified trm_pat.supp(1-2)]
+declare permute_trm_raw_permute_pat_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
+
end
--- a/Nominal/Ex/Ex3.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/Ex3.thy Mon May 10 15:45:04 2010 +0200
@@ -30,6 +30,13 @@
thm trm_pat.distinct
thm trm_pat.fv[simplified trm_pat.supp(1-2)]
+
+declare permute_trm_raw_permute_pat_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
+
end
--- a/Nominal/Ex/ExCoreHaskell.thy Mon May 10 15:44:49 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,675 +0,0 @@
-theory ExCoreHaskell
-imports "../NewParser"
-begin
-
-(* core haskell *)
-
-atom_decl var
-atom_decl cvar
-atom_decl tvar
-
-(* there are types, coercion types and regular types list-data-structure *)
-
-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"
-
-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 pat (permute_bv q pat)"
- apply(induct pat rule: inducts(9))
- apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1)
- done
-
-lemma ACons_subst:
- "supp (Abs_lst (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (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: eqvts[symmetric])
- apply (simp add: supp_abs)
- apply (simp add: fv_supp)
- 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>pat trm assoc_lst b. \<lbrakk>\<And>c. P9 c pat; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pat)) \<sharp>* b\<rbrakk>
- \<Longrightarrow> P8 b (ACons pat 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) pat \<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> pat)))" 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: eqvts[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
- apply (simp add: eqvts)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
- apply (simp add: eqvts)
- 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: eqvts[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
- apply (simp add: eqvts)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
- apply (simp add: eqvts)
- 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: eqvts[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
- apply (simp add: eqvts)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
- apply (simp add: eqvts)
- 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: eqvts[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
- apply (simp add: eqvts)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
- apply (simp add: eqvts)
- 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: eqvts[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
- apply (simp add: eqvts)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
- apply (simp add: eqvts)
- 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: eqvts[symmetric])
- apply (rule conjI)
- apply (rule supp_perm_eq)
- apply (simp add: eqvts)
- apply (subst supp_finite_atom_set)
- apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
- apply (simp add: eqvts)
- apply (simp add: eqvts)
- apply (subst supp_perm_eq)
- apply (subst supp_finite_atom_set)
- apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
- apply (simp add: eqvts)
- 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> pat))" 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
-
-declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
-
-equivariance alpha_tkind_raw
-
-thm eqvts
-thm eqvts_raw
-
-end
-
--- a/Nominal/Ex/ExLF.thy Mon May 10 15:44:49 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-theory ExLF
-imports "../NewParser"
-begin
-
-atom_decl name
-atom_decl ident
-
-nominal_datatype kind =
- Type
- | KPi "ty" n::"name" k::"kind" bind_set n in k
-and ty =
- TConst "ident"
- | TApp "ty" "trm"
- | TPi "ty" n::"name" t::"ty" bind_set n in t
-and trm =
- Const "ident"
- | Var "name"
- | App "trm" "trm"
- | Lam "ty" n::"name" t::"trm" bind_set n in t
-
-thm kind_ty_trm.supp
-
-end
-
-
-
-
--- a/Nominal/Ex/ExLeroy.thy Mon May 10 15:44:49 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,73 +0,0 @@
-theory ExLeroy
-imports "../NewParser"
-begin
-
-(* example form Leroy 96 about modules; OTT *)
-
-atom_decl name
-
-nominal_datatype mexp =
- Acc "path"
-| Stru "body"
-| Funct x::"name" "sexp" m::"mexp" bind_set x in m
-| FApp "mexp" "path"
-| Ascr "mexp" "sexp"
-and body =
- Empty
-| Seq c::defn d::"body" bind_set "cbinders c" in d
-and defn =
- Type "name" "tyty"
-| Dty "name"
-| DStru "name" "mexp"
-| Val "name" "trmtrm"
-and sexp =
- Sig sbody
-| SFunc "name" "sexp" "sexp"
-and sbody =
- SEmpty
-| SSeq C::spec D::sbody bind_set "Cbinders C" in D
-and spec =
- Type1 "name"
-| Type2 "name" "tyty"
-| SStru "name" "sexp"
-| SVal "name" "tyty"
-and tyty =
- Tyref1 "name"
-| Tyref2 "path" "tyty"
-| Fun "tyty" "tyty"
-and path =
- Sref1 "name"
-| Sref2 "path" "name"
-and trmtrm =
- Tref1 "name"
-| Tref2 "path" "name"
-| Lam' v::"name" "tyty" M::"trmtrm" bind_set v in M
-| App' "trmtrm" "trmtrm"
-| Let' "body" "trmtrm"
-binder
- cbinders :: "defn \<Rightarrow> atom set"
-and Cbinders :: "spec \<Rightarrow> atom set"
-where
- "cbinders (Type t T) = {atom t}"
-| "cbinders (Dty t) = {atom t}"
-| "cbinders (DStru x s) = {atom x}"
-| "cbinders (Val v M) = {atom v}"
-| "Cbinders (Type1 t) = {atom t}"
-| "Cbinders (Type2 t T) = {atom t}"
-| "Cbinders (SStru x S) = {atom x}"
-| "Cbinders (SVal v T) = {atom v}"
-
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.bn
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10)
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10)]
-
-end
-
-
-
--- a/Nominal/Ex/ExLet.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/ExLet.thy Mon May 10 15:45:04 2010 +0200
@@ -35,6 +35,13 @@
thm trm_lts.fv[simplified trm_lts.supp(1-2)]
+declare permute_trm_raw_permute_lts_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
+
+
primrec
permute_bn_raw
where
@@ -95,14 +102,14 @@
apply (rule_tac x="q" in exI)
apply (simp add: alphas)
apply (simp add: perm_bn[symmetric])
- apply (simp add: eqvts[symmetric])
- apply (simp add: supp_abs)
+ apply(rule conjI)
+ apply(drule supp_perm_eq)
+ apply(simp add: abs_eq_iff)
+ apply(simp add: alphas_abs alphas)
+ apply(drule conjunct1)
apply (simp add: trm_lts.supp)
- apply (rule supp_perm_eq[symmetric])
- apply (subst supp_finite_atom_set)
- apply (rule finite_Diff)
- apply (simp add: finite_supp)
- apply (assumption)
+ apply(simp add: supp_abs)
+ apply (simp add: trm_lts.supp)
done
--- a/Nominal/Ex/ExLetMult.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/ExLetMult.thy Mon May 10 15:45:04 2010 +0200
@@ -22,6 +22,12 @@
thm trm_lts.induct
thm trm_lts.fv[simplified trm_lts.supp]
+declare permute_trm_raw_permute_lts_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
+
end
--- a/Nominal/Ex/ExLetRec.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/ExLetRec.thy Mon May 10 15:45:04 2010 +0200
@@ -7,6 +7,9 @@
atom_decl name
+ML {* val _ = cheat_alpha_eqvt := true *}
+ML {* val _ = cheat_equivp := true *}
+
nominal_datatype trm =
Vr "name"
| Ap "trm" "trm"
@@ -30,6 +33,11 @@
thm trm_lts.supp
thm trm_lts.fv[simplified trm_lts.supp]
+declare permute_trm_raw_permute_lts_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
(* why is this not in HOL simpset? *)
lemma set_sub: "{a, b} - {b} = {a} - {b}"
by auto
--- a/Nominal/Ex/ExNotRsp.thy Mon May 10 15:44:49 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-theory ExNotRsp
-imports "../Parser"
-begin
-
-atom_decl name
-
-(* example 6 from Terms.thy *)
-
-nominal_datatype trm6 =
- Vr6 "name"
-| Lm6 x::"name" t::"trm6" bind x in t
-| Lt6 left::"trm6" right::"trm6" bind "bv6 left" in right
-binder
- bv6
-where
- "bv6 (Vr6 n) = {}"
-| "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
-| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
-
-(* example 7 from Terms.thy *)
-nominal_datatype trm7 =
- Vr7 "name"
-| Lm7 l::"name" r::"trm7" bind l in r
-| Lt7 l::"trm7" r::"trm7" bind "bv7 l" in r
-binder
- bv7
-where
- "bv7 (Vr7 n) = {atom n}"
-| "bv7 (Lm7 n t) = bv7 t - {atom n}"
-| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
-*)
-
-(* example 9 from Terms.thy *)
-nominal_datatype lam9 =
- Var9 "name"
-| Lam9 n::"name" l::"lam9" bind n in l
-and bla9 =
- Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s
-binder
- bv9
-where
- "bv9 (Var9 x) = {}"
-| "bv9 (Lam9 x b) = {atom x}"
-
-end
-
-
-
--- a/Nominal/Ex/ExPS3.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/ExPS3.thy Mon May 10 15:45:04 2010 +0200
@@ -11,29 +11,35 @@
ML {* val _ = cheat_alpha_bn_rsp := true *}
nominal_datatype exp =
- VarP "name"
-| AppP "exp" "exp"
-| LamP x::"name" e::"exp" bind_set x in e
-| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1
-and pat3 =
+ Var "name"
+| App "exp" "exp"
+| Lam x::"name" e::"exp" bind_set x in e
+| Let x::"name" p::"pat" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1
+and pat =
PVar "name"
| PUnit
-| PPair "pat3" "pat3"
+| PPair "pat" "pat"
binder
- bp :: "pat3 \<Rightarrow> atom set"
+ bp :: "pat \<Rightarrow> atom set"
where
"bp (PVar x) = {atom x}"
| "bp (PUnit) = {}"
| "bp (PPair p1 p2) = bp p1 \<union> bp p2"
-thm exp_pat3.fv
-thm exp_pat3.eq_iff
-thm exp_pat3.bn
-thm exp_pat3.perm
-thm exp_pat3.induct
-thm exp_pat3.distinct
-thm exp_pat3.fv
-thm exp_pat3.supp(1-2)
+thm exp_pat.fv
+thm exp_pat.eq_iff
+thm exp_pat.bn
+thm exp_pat.perm
+thm exp_pat.induct
+thm exp_pat.distinct
+thm exp_pat.fv
+thm exp_pat.supp(1-2)
+
+declare permute_exp_raw_permute_pat_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_exp_raw
+
end
--- a/Nominal/Ex/ExPS6.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/ExPS6.thy Mon May 10 15:45:04 2010 +0200
@@ -1,37 +1,42 @@
theory ExPS6
-imports "../Parser"
+imports "../NewParser"
begin
(* example 6 from Peter Sewell's bestiary *)
atom_decl name
-(* The binding structure is too complicated, so equivalence the
- way we define it is not true *)
+(* Is this binding structure supported - I think not
+ because e1 occurs twice as body *)
-ML {* val _ = recursive := false *}
-nominal_datatype exp6 =
- EVar name
-| EPair exp6 exp6
-| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1
-and pat6 =
- PVar' name
-| PUnit'
-| PPair' pat6 pat6
+nominal_datatype exp =
+ Var name
+| Pair exp exp
+| LetRec x::name p::pat e1::exp e2::exp bind x in e1 e2, bind "bp p" in e1
+and pat =
+ PVar name
+| PUnit
+| PPair pat pat
binder
- bp6 :: "pat6 \<Rightarrow> atom set"
+ bp :: "pat \<Rightarrow> atom list"
where
- "bp6 (PVar' x) = {atom x}"
-| "bp6 (PUnit') = {}"
-| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
+ "bp (PVar x) = [atom x]"
+| "bp (PUnit) = []"
+| "bp (PPair p1 p2) = bp p1 @ bp p2"
-thm exp6_pat6.fv
-thm exp6_pat6.eq_iff
-thm exp6_pat6.bn
-thm exp6_pat6.perm
-thm exp6_pat6.induct
-thm exp6_pat6.distinct
-thm exp6_pat6.supp
+thm exp_pat.fv
+thm exp_pat.eq_iff
+thm exp_pat.bn
+thm exp_pat.perm
+thm exp_pat.induct
+thm exp_pat.distinct
+thm exp_pat.supp
+
+declare permute_exp_raw_permute_pat_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_exp_raw
+
end
--- a/Nominal/Ex/ExPS7.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/ExPS7.thy Mon May 10 15:45:04 2010 +0200
@@ -1,3 +1,4 @@
+
theory ExPS7
imports "../NewParser"
begin
@@ -6,25 +7,31 @@
atom_decl name
-nominal_datatype exp7 =
- EVar name
-| EUnit
-| EPair exp7 exp7
-| ELetRec l::"lrbs" e::"exp7" bind_set "b7s l" in l e
+nominal_datatype exp =
+ Var name
+| Unit
+| Pair exp exp
+| LetRec l::"lrbs" e::"exp" bind_set "bs l" in l e
and lrb =
- Assign name exp7
+ Assign name exp
and lrbs =
Single lrb
| More lrb lrbs
binder
- b7 :: "lrb \<Rightarrow> atom set" and
- b7s :: "lrbs \<Rightarrow> atom set"
+ b :: "lrb \<Rightarrow> atom set" and
+ bs :: "lrbs \<Rightarrow> atom set"
where
- "b7 (Assign x e) = {atom x}"
-| "b7s (Single a) = b7 a"
-| "b7s (More a as) = (b7 a) \<union> (b7s as)"
-thm exp7_lrb_lrbs.eq_iff
-thm exp7_lrb_lrbs.supp
+ "b (Assign x e) = {atom x}"
+| "bs (Single a) = b a"
+| "bs (More a as) = (b a) \<union> (bs as)"
+
+thm exp_lrb_lrbs.eq_iff
+thm exp_lrb_lrbs.supp
+
+declare permute_exp_raw_permute_lrb_raw_permute_lrbs_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_exp_raw
end
--- a/Nominal/Ex/ExPS8.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/ExPS8.thy Mon May 10 15:45:04 2010 +0200
@@ -48,6 +48,11 @@
thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv
thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff
+
+declare permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_exp_raw
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/LF.thy Mon May 10 15:45:04 2010 +0200
@@ -0,0 +1,35 @@
+theory LF
+imports "../NewParser"
+begin
+
+atom_decl name
+atom_decl ident
+
+nominal_datatype kind =
+ Type
+ | KPi "ty" n::"name" k::"kind" bind n in k
+and ty =
+ TConst "ident"
+ | TApp "ty" "trm"
+ | TPi "ty" n::"name" t::"ty" bind n in t
+and trm =
+ Const "ident"
+ | Var "name"
+ | App "trm" "trm"
+ | Lam "ty" n::"name" t::"trm" bind n in t
+
+thm kind_ty_trm.supp
+
+declare permute_kind_raw_permute_ty_raw_permute_trm_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
+
+
+
+end
+
+
+
+
--- a/Nominal/Ex/Lambda.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/Lambda.thy Mon May 10 15:45:04 2010 +0200
@@ -15,6 +15,10 @@
declare lam.perm[eqvt]
+declare permute_lam_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+equivariance alpha_lam_raw
+
section {* Strong Induction Principles*}
(*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Modules.thy Mon May 10 15:45:04 2010 +0200
@@ -0,0 +1,80 @@
+theory Modules
+imports "../NewParser"
+begin
+
+(* example from Leroy'96 about modules;
+ see OTT example by Owens *)
+
+atom_decl name
+
+nominal_datatype mexp =
+ Acc "path"
+| Stru "body"
+| Funct x::"name" "sexp" m::"mexp" bind_set x in m
+| FApp "mexp" "path"
+| Ascr "mexp" "sexp"
+and body =
+ Empty
+| Seq c::defn d::"body" bind_set "cbinders c" in d
+and defn =
+ Type "name" "ty"
+| Dty "name"
+| DStru "name" "mexp"
+| Val "name" "trm"
+and sexp =
+ Sig sbody
+| SFunc "name" "sexp" "sexp"
+and sbody =
+ SEmpty
+| SSeq C::spec D::sbody bind_set "Cbinders C" in D
+and spec =
+ Type1 "name"
+| Type2 "name" "ty"
+| SStru "name" "sexp"
+| SVal "name" "ty"
+and ty =
+ Tyref1 "name"
+| Tyref2 "path" "ty"
+| Fun "ty" "ty"
+and path =
+ Sref1 "name"
+| Sref2 "path" "name"
+and trm =
+ Tref1 "name"
+| Tref2 "path" "name"
+| Lam' v::"name" "ty" M::"trm" bind_set v in M
+| App' "trm" "trm"
+| Let' "body" "trm"
+binder
+ cbinders :: "defn \<Rightarrow> atom set"
+and Cbinders :: "spec \<Rightarrow> atom set"
+where
+ "cbinders (Type t T) = {atom t}"
+| "cbinders (Dty t) = {atom t}"
+| "cbinders (DStru x s) = {atom x}"
+| "cbinders (Val v M) = {atom v}"
+| "Cbinders (Type1 t) = {atom t}"
+| "Cbinders (Type2 t T) = {atom t}"
+| "Cbinders (SStru x S) = {atom x}"
+| "Cbinders (SVal v T) = {atom v}"
+
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.eq_iff
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.bn
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.perm
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.induct
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.inducts
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.distinct
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)]
+
+declare permute_mexp_raw_permute_body_raw_permute_defn_raw_permute_sexp_raw_permute_sbody_raw_permute_spec_raw_permute_ty_raw_permute_path_raw_permute_trm_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
+
+end
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/NoneExamples.thy Mon May 10 15:45:04 2010 +0200
@@ -0,0 +1,54 @@
+theory NoneExamples
+imports "../NewParser"
+begin
+
+atom_decl name
+
+(* this example binds bound names and
+ so is not respectful *)
+(*
+nominal_datatype trm =
+ Vr "name"
+| Lm x::"name" t::"trm" bind x in t
+| Lt left::"trm" right::"trm" bind "bv left" in right
+binder
+ bv
+where
+ "bv (Vr n) = {}"
+| "bv (Lm n t) = {atom n} \<union> bv t"
+| "bv (Lt l r) = bv l \<union> bv r"
+*)
+
+(* this example uses "-" in the binding function;
+ at the moment this is unsupported *)
+(*
+nominal_datatype trm' =
+ Vr' "name"
+| Lm' l::"name" r::"trm'" bind l in r
+| Lt' l::"trm'" r::"trm'" bind "bv' l" in r
+binder
+ bv'
+where
+ "bv' (Vr' n) = {atom n}"
+| "bv' (Lm' n t) = bv' t - {atom n}"
+| "bv' (Lt' l r) = bv' l \<union> bv' r"
+*)
+
+(* this example again binds bound names *)
+(*
+nominal_datatype trm'' =
+ Va'' "name"
+| Lm'' n::"name" l::"trm''" bind n in l
+and bla'' =
+ Bla'' f::"trm''" s::"trm''" bind "bv'' f" in s
+binder
+ bv''
+where
+ "bv'' (Vm'' x) = {}"
+| "bv'' (Lm'' x b) = {atom x}"
+*)
+
+end
+
+
+
--- a/Nominal/Ex/Term8.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/Term8.thy Mon May 10 15:45:04 2010 +0200
@@ -2,22 +2,27 @@
imports "../NewParser"
begin
-(* example 8 from Terms.thy *)
+(* example 8 *)
atom_decl name
+(* this should work but gives an error at the moment:
+ seems like in the symmetry proof
+*)
+
nominal_datatype foo =
Foo0 "name"
| Foo1 b::"bar" f::"foo" bind_set "bv b" in f
and bar =
Bar0 "name"
-| Bar1 "name" s::"name" b::"bar" bind_set s in b
+| Bar1 "name" s::"name" b::"bar" bind s in b
binder
bv
where
"bv (Bar0 x) = {}"
| "bv (Bar1 v x b) = {atom v}"
+
end
--- a/Nominal/Ex/TestMorePerm.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/TestMorePerm.thy Mon May 10 15:45:04 2010 +0200
@@ -1,35 +1,35 @@
theory TestMorePerm
-imports "../Parser"
+imports "../NewParser"
begin
text {*
"Weirdo" example from Peter Sewell's bestiary.
- In case of deep binders, it is not coverd by our
- approach of defining alpha-equivalence with a
- single permutation.
-
- Check whether it works with shallow binders as
- defined below.
+ This example is not covered by our binding
+ specification.
*}
ML {* val _ = cheat_equivp := true *}
atom_decl name
-nominal_datatype foo =
+nominal_datatype weird =
Foo_var "name"
-| Foo_pair "foo" "foo"
-| Foo x::"name" y::"name" p1::"foo" p2::"foo" p3::"foo"
- bind x in p1, bind x in p2,
- bind y in p2, bind y in p3
+| Foo_pair "weird" "weird"
+| Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
+ bind x in p1 p2,
+ bind y in p2 p3
-thm alpha_foo_raw.intros[no_vars]
+thm alpha_weird_raw.intros[no_vars]
thm permute_weird_raw.simps[no_vars]
thm alpha_weird_raw.intros[no_vars]
thm fv_weird_raw.simps[no_vars]
+declare permute_weird_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+equivariance alpha_weird_raw
+
end
--- a/Nominal/Ex/TypeSchemes.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Ex/TypeSchemes.thy Mon May 10 15:45:04 2010 +0200
@@ -14,6 +14,11 @@
lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]
+declare permute_ty_raw_permute_tys_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+equivariance alpha_ty_raw
+
+
(* below we define manually the function for size *)
lemma size_eqvt_raw:
--- a/Nominal/FSet.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/FSet.thy Mon May 10 15:45:04 2010 +0200
@@ -1,11 +1,12 @@
-(* Title: Quotient.thy
- Author: Cezary Kaliszyk
- Author: Christian Urban
+(* Title: HOL/Quotient_Examples/FSet.thy
+ Author: Cezary Kaliszyk, TU Munich
+ Author: Christian Urban, TU Munich
- provides a reasoning infrastructure for the type of finite sets
+A reasoning infrastructure for the type of finite sets.
*)
+
theory FSet
-imports Quotient Quotient_List List
+imports Quotient_List
begin
text {* Definiton of List relation and the quotient type *}
@@ -50,11 +51,17 @@
| "finter_raw (h # t) l =
(if memb h l then h # (finter_raw t l) else finter_raw t l)"
-fun
+primrec
delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
where
"delete_raw [] x = []"
-| "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
+| "delete_raw (a # xs) x = (if (a = x) then delete_raw xs x else a # (delete_raw xs x))"
+
+primrec
+ fminus_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
+ "fminus_raw l [] = l"
+| "fminus_raw l (h # t) = fminus_raw (delete_raw l h) t"
definition
rsp_fold
@@ -65,10 +72,10 @@
ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
where
"ffold_raw f z [] = z"
-| "ffold_raw f z (a # A) =
+| "ffold_raw f z (a # xs) =
(if (rsp_fold f) then
- if memb a A then ffold_raw f z A
- else f a (ffold_raw f z A)
+ if memb a xs then ffold_raw f z xs
+ else f a (ffold_raw f z xs)
else z)"
text {* Composition Quotient *}
@@ -80,16 +87,16 @@
lemma compose_list_refl:
shows "(list_rel op \<approx> OOO op \<approx>) r r"
proof
- show c: "list_rel op \<approx> r r" by (rule list_rel_refl)
- have d: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
- show b: "(op \<approx> OO list_rel op \<approx>) r r" by (rule pred_compI) (rule d, rule c)
+ have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
+ show "list_rel op \<approx> r r" by (rule list_rel_refl)
+ with * show "(op \<approx> OO list_rel op \<approx>) r r" ..
qed
lemma Quotient_fset_list:
shows "Quotient (list_rel op \<approx>) (map abs_fset) (map rep_fset)"
by (fact list_quotient[OF Quotient_fset])
-lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
+lemma set_in_eq: "(\<forall>e. ((e \<in> xs) \<longleftrightarrow> (e \<in> ys))) \<equiv> xs = ys"
by (rule eq_reflection) auto
lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
@@ -117,7 +124,8 @@
show "(list_rel op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
next
assume a: "(list_rel op \<approx> OOO op \<approx>) r s"
- then have b: "map abs_fset r \<approx> map abs_fset s" proof (elim pred_compE)
+ then have b: "map abs_fset r \<approx> map abs_fset s"
+ proof (elim pred_compE)
fix b ba
assume c: "list_rel op \<approx> r b"
assume d: "b \<approx> ba"
@@ -208,6 +216,14 @@
"(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
by (simp add: memb_def[symmetric] memb_delete_raw)
+lemma fminus_raw_memb: "memb x (fminus_raw xs ys) = (memb x xs \<and> \<not> memb x ys)"
+ by (induct ys arbitrary: xs)
+ (simp_all add: not_memb_nil memb_delete_raw memb_cons_iff)
+
+lemma [quot_respect]:
+ "(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
+ by (simp add: memb_def[symmetric] fminus_raw_memb)
+
lemma fcard_raw_gt_0:
assumes a: "x \<in> set xs"
shows "0 < fcard_raw xs"
@@ -221,20 +237,43 @@
assumes a: "xs \<approx> ys"
shows "fcard_raw xs = fcard_raw ys"
using a
- apply (induct xs arbitrary: ys)
- apply (auto simp add: memb_def)
- apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys)")
- apply (auto)
- apply (drule_tac x="x" in spec)
- apply (blast)
- apply (drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec)
- apply (simp add: fcard_raw_delete_one memb_def)
- apply (case_tac "a \<in> set ys")
- apply (simp only: if_True)
- apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)")
- apply (drule Suc_pred'[OF fcard_raw_gt_0])
- apply (auto)
- done
+ proof (induct xs arbitrary: ys)
+ case Nil
+ show ?case using Nil.prems by simp
+ next
+ case (Cons a xs)
+ have a: "a # xs \<approx> ys" by fact
+ have b: "\<And>ys. xs \<approx> ys \<Longrightarrow> fcard_raw xs = fcard_raw ys" by fact
+ show ?case proof (cases "a \<in> set xs")
+ assume c: "a \<in> set xs"
+ have "\<forall>x. (x \<in> set xs) = (x \<in> set ys)"
+ proof (intro allI iffI)
+ fix x
+ assume "x \<in> set xs"
+ then show "x \<in> set ys" using a by auto
+ next
+ fix x
+ assume d: "x \<in> set ys"
+ have e: "(x \<in> set (a # xs)) = (x \<in> set ys)" using a by simp
+ show "x \<in> set xs" using c d e unfolding list_eq.simps by simp blast
+ qed
+ then show ?thesis using b c by (simp add: memb_def)
+ next
+ assume c: "a \<notin> set xs"
+ have d: "xs \<approx> [x\<leftarrow>ys . x \<noteq> a] \<Longrightarrow> fcard_raw xs = fcard_raw [x\<leftarrow>ys . x \<noteq> a]" using b by simp
+ have "Suc (fcard_raw xs) = fcard_raw ys"
+ proof (cases "a \<in> set ys")
+ assume e: "a \<in> set ys"
+ have f: "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)" using a c
+ by (auto simp add: fcard_raw_delete_one)
+ have "fcard_raw ys = Suc (fcard_raw ys - 1)" by (rule Suc_pred'[OF fcard_raw_gt_0]) (rule e)
+ then show ?thesis using d e f by (simp_all add: fcard_raw_delete_one memb_def)
+ next
+ case False then show ?thesis using a c d by auto
+ qed
+ then show ?thesis using a c d by (simp add: memb_def)
+ qed
+qed
lemma fcard_raw_rsp[quot_respect]:
shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
@@ -306,8 +345,8 @@
obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_rel_find_element[OF e a])
then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
- have j: "ya \<in> set y'" using b h by simp
- have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" by (rule list_rel_find_element[OF j c])
+ have "ya \<in> set y'" using b h by simp
+ then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_rel_find_element)
then show ?thesis using f i by auto
qed
@@ -334,6 +373,10 @@
then show "concat a \<approx> concat b" by simp
qed
+lemma [quot_respect]:
+ "((op =) ===> op \<approx> ===> op \<approx>) filter filter"
+ by auto
+
text {* Distributive lattice with bot *}
lemma sub_list_not_eq:
@@ -385,9 +428,10 @@
apply (induct x)
apply (simp_all add: memb_def)
apply (simp add: memb_def[symmetric] memb_finter_raw)
- by (auto simp add: memb_def)
+ apply (auto simp add: memb_def)
+ done
-instantiation fset :: (type) "{bot,distrib_lattice}"
+instantiation fset :: (type) "{bounded_lattice_bot,distrib_lattice,minus}"
begin
quotient_definition
@@ -423,12 +467,12 @@
"(op @) \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
abbreviation
- funion (infixl "|\<union>|" 65)
+ funion (infixl "|\<union>|" 65)
where
"xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys"
quotient_definition
- "inf \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
+ "inf \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
is
"finter_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
@@ -437,6 +481,11 @@
where
"xs |\<inter>| ys \<equiv> inf (xs :: 'a fset) ys"
+quotient_definition
+ "minus \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
+is
+ "fminus_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+
instance
proof
fix x y z :: "'a fset"
@@ -496,10 +545,10 @@
where
"x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
-section {* Other constants on the Quotient Type *}
+section {* Other constants on the Quotient Type *}
quotient_definition
- "fcard :: 'a fset \<Rightarrow> nat"
+ "fcard :: 'a fset \<Rightarrow> nat"
is
"fcard_raw"
@@ -509,11 +558,11 @@
"map"
quotient_definition
- "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset"
+ "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset"
is "delete_raw"
quotient_definition
- "fset_to_set :: 'a fset \<Rightarrow> 'a set"
+ "fset_to_set :: 'a fset \<Rightarrow> 'a set"
is "set"
quotient_definition
@@ -525,6 +574,11 @@
is
"concat"
+quotient_definition
+ "ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+is
+ "filter"
+
text {* Compositional Respectfullness and Preservation *}
lemma [quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
@@ -636,6 +690,10 @@
"sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
by (auto simp add: memb_def sub_list_def)
+lemma fminus_raw_red: "fminus_raw (x # xs) ys = (if memb x ys then fminus_raw xs ys else x # (fminus_raw xs ys))"
+ by (induct ys arbitrary: xs x)
+ (simp_all add: not_memb_nil memb_delete_raw memb_cons_iff)
+
text {* Cardinality of finite sets *}
lemma fcard_raw_0:
@@ -701,23 +759,37 @@
by auto
lemma fset_raw_strong_cases:
- "(xs = []) \<or> (\<exists>x ys. ((\<not> memb x ys) \<and> (xs \<approx> x # ys)))"
- apply (induct xs)
- apply (simp)
- apply (rule disjI2)
- apply (erule disjE)
- apply (rule_tac x="a" in exI)
- apply (rule_tac x="[]" in exI)
- apply (simp add: memb_def)
- apply (erule exE)+
- apply (case_tac "x = a")
- apply (rule_tac x="a" in exI)
- apply (rule_tac x="ys" in exI)
- apply (simp)
- apply (rule_tac x="x" in exI)
- apply (rule_tac x="a # ys" in exI)
- apply (auto simp add: memb_def)
- done
+ obtains "xs = []"
+ | x ys where "\<not> memb x ys" and "xs \<approx> x # ys"
+proof (induct xs arbitrary: x ys)
+ case Nil
+ then show thesis by simp
+next
+ case (Cons a xs)
+ have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis" by fact
+ have b: "\<And>x' ys'. \<lbrakk>\<not> memb x' ys'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
+ have c: "xs = [] \<Longrightarrow> thesis" by (metis no_memb_nil singleton_list_eq b)
+ have "\<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
+ proof -
+ fix x :: 'a
+ fix ys :: "'a list"
+ assume d:"\<not> memb x ys"
+ assume e:"xs \<approx> x # ys"
+ show thesis
+ proof (cases "x = a")
+ assume h: "x = a"
+ then have f: "\<not> memb a ys" using d by simp
+ have g: "a # xs \<approx> a # ys" using e h by auto
+ show thesis using b f g by simp
+ next
+ assume h: "x \<noteq> a"
+ then have f: "\<not> memb x (a # ys)" using d unfolding memb_def by auto
+ have g: "a # xs \<approx> x # (a # ys)" using e h by auto
+ show thesis using b f g by simp
+ qed
+ qed
+ then show thesis using a c by blast
+qed
section {* deletion *}
@@ -741,8 +813,8 @@
"finter_raw l [] = []"
by (induct l) (simp_all add: not_memb_nil)
-lemma set_cong:
- shows "(set x = set y) = (x \<approx> y)"
+lemma set_cong:
+ shows "(x \<approx> y) = (set x = set y)"
by auto
lemma inj_map_eq_iff:
@@ -812,13 +884,13 @@
case (Suc m)
have b: "l \<approx> r" by fact
have d: "fcard_raw l = Suc m" by fact
- have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb[OF d])
+ then have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb)
then obtain a where e: "memb a l" by auto
then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto
have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp
have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp
- have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
- have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g'])
+ have "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
+ then have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5))
have i: "list_eq2 l (a # delete_raw l a)"
by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h])
@@ -828,6 +900,42 @@
then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
qed
+text {* Set *}
+
+lemma sub_list_set: "sub_list xs ys = (set xs \<subseteq> set ys)"
+ by (metis rev_append set_append set_cong set_rev sub_list_append sub_list_append_left sub_list_def sub_list_not_eq subset_Un_eq)
+
+lemma sub_list_neq_set: "(sub_list xs ys \<and> \<not> list_eq xs ys) = (set xs \<subset> set ys)"
+ by (auto simp add: sub_list_set)
+
+lemma fcard_raw_set: "fcard_raw xs = card (set xs)"
+ by (induct xs) (auto simp add: insert_absorb memb_def card_insert_disjoint finite_set)
+
+lemma memb_set: "memb x xs = (x \<in> set xs)"
+ by (simp only: memb_def)
+
+lemma filter_set: "set (filter P xs) = P \<inter> (set xs)"
+ by (induct xs, simp)
+ (metis Int_insert_right_if0 Int_insert_right_if1 List.set.simps(2) filter.simps(2) mem_def)
+
+lemma delete_raw_set: "set (delete_raw xs x) = set xs - {x}"
+ by (induct xs) auto
+
+lemma inter_raw_set: "set (finter_raw xs ys) = set xs \<inter> set ys"
+ by (induct xs) (simp_all add: memb_def)
+
+lemma fminus_raw_set: "set (fminus_raw xs ys) = set xs - set ys"
+ by (induct ys arbitrary: xs)
+ (simp_all add: fminus_raw.simps delete_raw_set, blast)
+
+text {* Raw theorems of ffilter *}
+
+lemma sub_list_filter: "sub_list (filter P xs) (filter Q xs) = (\<forall> x. memb x xs \<longrightarrow> P x \<longrightarrow> Q x)"
+unfolding sub_list_def memb_def by auto
+
+lemma list_eq_filter: "list_eq (filter P xs) (filter Q xs) = (\<forall>x. memb x xs \<longrightarrow> P x = Q x)"
+unfolding memb_def by auto
+
text {* Lifted theorems *}
lemma not_fin_fnil: "x |\<notin>| {||}"
@@ -879,7 +987,7 @@
by (lifting none_memb_nil)
lemma fset_cong:
- "(fset_to_set S = fset_to_set T) = (S = T)"
+ "(S = T) = (fset_to_set S = fset_to_set T)"
by (lifting set_cong)
text {* fcard *}
@@ -899,11 +1007,11 @@
shows "(fcard S = 1) = (\<exists>x. S = {|x|})"
by (lifting fcard_raw_1)
-lemma fcard_gt_0:
+lemma fcard_gt_0:
shows "x \<in> fset_to_set S \<Longrightarrow> 0 < fcard S"
by (lifting fcard_raw_gt_0)
-lemma fcard_not_fin:
+lemma fcard_not_fin:
shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
by (lifting fcard_raw_not_memb)
@@ -922,14 +1030,13 @@
text {* funion *}
-lemma funion_simps[simp]:
- shows "{||} |\<union>| S = S"
- and "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
- by (lifting append.simps)
+lemmas [simp] =
+ sup_bot_left[where 'a="'a fset", standard]
+ sup_bot_right[where 'a="'a fset", standard]
-lemma funion_empty[simp]:
- shows "S |\<union>| {||} = S"
- by (lifting append_Nil2)
+lemma funion_finsert[simp]:
+ shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
+ by (lifting append.simps(2))
lemma singleton_union_left:
"{|a|} |\<union>| S = finsert a S"
@@ -942,7 +1049,8 @@
section {* Induction and Cases rules for finite sets *}
lemma fset_strong_cases:
- "S = {||} \<or> (\<exists>x T. x |\<notin>| T \<and> S = finsert x T)"
+ obtains "xs = {||}"
+ | x ys where "x |\<notin>| ys" and "xs = finsert x ys"
by (lifting fset_raw_strong_cases)
lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
@@ -954,7 +1062,7 @@
by (lifting list.induct)
lemma fset_induct[case_names fempty finsert, induct type: fset]:
- assumes prem1: "P {||}"
+ assumes prem1: "P {||}"
and prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
shows "P S"
proof(induct S rule: fset_induct_weak)
@@ -980,6 +1088,20 @@
apply simp_all
done
+lemma fset_fcard_induct:
+ assumes a: "P {||}"
+ and b: "\<And>xs ys. Suc (fcard xs) = (fcard ys) \<Longrightarrow> P xs \<Longrightarrow> P ys"
+ shows "P zs"
+proof (induct zs)
+ show "P {||}" by (rule a)
+next
+ fix x :: 'a and zs :: "'a fset"
+ assume h: "P zs"
+ assume "x |\<notin>| zs"
+ then have H1: "Suc (fcard zs) = fcard (finsert x zs)" using fcard_suc by auto
+ then show "P (finsert x zs)" using b h by simp
+qed
+
text {* fmap *}
lemma fmap_simps[simp]:
@@ -989,7 +1111,7 @@
lemma fmap_set_image:
"fset_to_set (fmap f S) = f ` (fset_to_set S)"
- by (induct S) (simp_all)
+ by (induct S) simp_all
lemma inj_fmap_eq_iff:
"inj f \<Longrightarrow> (fmap f S = fmap f T) = (S = T)"
@@ -1002,6 +1124,44 @@
"x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
by (lifting memb_append)
+text {* to_set *}
+
+lemma fin_set: "(x |\<in>| xs) = (x \<in> fset_to_set xs)"
+ by (lifting memb_set)
+
+lemma fnotin_set: "(x |\<notin>| xs) = (x \<notin> fset_to_set xs)"
+ by (simp add: fin_set)
+
+lemma fcard_set: "fcard xs = card (fset_to_set xs)"
+ by (lifting fcard_raw_set)
+
+lemma fsubseteq_set: "(xs |\<subseteq>| ys) = (fset_to_set xs \<subseteq> fset_to_set ys)"
+ by (lifting sub_list_set)
+
+lemma fsubset_set: "(xs |\<subset>| ys) = (fset_to_set xs \<subset> fset_to_set ys)"
+ unfolding less_fset by (lifting sub_list_neq_set)
+
+lemma ffilter_set: "fset_to_set (ffilter P xs) = P \<inter> fset_to_set xs"
+ by (lifting filter_set)
+
+lemma fdelete_set: "fset_to_set (fdelete xs x) = fset_to_set xs - {x}"
+ by (lifting delete_raw_set)
+
+lemma inter_set: "fset_to_set (xs |\<inter>| ys) = fset_to_set xs \<inter> fset_to_set ys"
+ by (lifting inter_raw_set)
+
+lemma union_set: "fset_to_set (xs |\<union>| ys) = fset_to_set xs \<union> fset_to_set ys"
+ by (lifting set_append)
+
+lemma fminus_set: "fset_to_set (xs - ys) = fset_to_set xs - fset_to_set ys"
+ by (lifting fminus_raw_set)
+
+lemmas fset_to_set_trans =
+ fin_set fnotin_set fcard_set fsubseteq_set fsubset_set
+ inter_set union_set ffilter_set fset_to_set_simps
+ fset_cong fdelete_set fmap_set_image fminus_set
+
+
text {* ffold *}
lemma ffold_nil: "ffold f z {||} = z"
@@ -1017,15 +1177,15 @@
text {* fdelete *}
-lemma fin_fdelete:
+lemma fin_fdelete:
shows "x |\<in>| fdelete S y \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
by (lifting memb_delete_raw)
-lemma fin_fdelete_ident:
+lemma fin_fdelete_ident:
shows "x |\<notin>| fdelete S x"
by (lifting memb_delete_raw_ident)
-lemma not_memb_fdelete_ident:
+lemma not_memb_fdelete_ident:
shows "x |\<notin>| S \<Longrightarrow> fdelete S x = S"
by (lifting not_memb_delete_raw_ident)
@@ -1060,6 +1220,18 @@
by (rule meta_eq_to_obj_eq)
(lifting sub_list_def[simplified memb_def[symmetric]])
+lemma fminus_fin: "(x |\<in>| xs - ys) = (x |\<in>| xs \<and> x |\<notin>| ys)"
+ by (lifting fminus_raw_memb)
+
+lemma fminus_red: "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
+ by (lifting fminus_raw_red)
+
+lemma fminus_red_fin[simp]: "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
+ by (simp add: fminus_red)
+
+lemma fminus_red_fnotin[simp]: "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
+ by (simp add: fminus_red)
+
lemma expand_fset_eq:
"(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
by (lifting list_eq.simps[simplified memb_def[symmetric]])
@@ -1102,8 +1274,107 @@
lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
by (lifting concat_append)
+text {* ffilter *}
+
+lemma subseteq_filter: "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
+by (lifting sub_list_filter)
+
+lemma eq_ffilter: "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
+by (lifting list_eq_filter)
+
+lemma subset_ffilter: "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"
+unfolding less_fset by (auto simp add: subseteq_filter eq_ffilter)
+
+section {* lemmas transferred from Finite_Set theory *}
+
+text {* finiteness for finite sets holds *}
+lemma finite_fset: "finite (fset_to_set S)"
+ by (induct S) auto
+
+lemma fset_choice: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
+ unfolding fset_to_set_trans
+ by (rule finite_set_choice[simplified Ball_def, OF finite_fset])
+
+lemma fsubseteq_fnil: "xs |\<subseteq>| {||} = (xs = {||})"
+ unfolding fset_to_set_trans
+ by (rule subset_empty)
+
+lemma not_fsubset_fnil: "\<not> xs |\<subset>| {||}"
+ unfolding fset_to_set_trans
+ by (rule not_psubset_empty)
+
+lemma fcard_mono: "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
+ unfolding fset_to_set_trans
+ by (rule card_mono[OF finite_fset])
+
+lemma fcard_fseteq: "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
+ unfolding fset_to_set_trans
+ by (rule card_seteq[OF finite_fset])
+
+lemma psubset_fcard_mono: "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
+ unfolding fset_to_set_trans
+ by (rule psubset_card_mono[OF finite_fset])
+
+lemma fcard_funion_finter: "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
+ unfolding fset_to_set_trans
+ by (rule card_Un_Int[OF finite_fset finite_fset])
+
+lemma fcard_funion_disjoint: "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
+ unfolding fset_to_set_trans
+ by (rule card_Un_disjoint[OF finite_fset finite_fset])
+
+lemma fcard_delete1_less: "x |\<in>| xs \<Longrightarrow> fcard (fdelete xs x) < fcard xs"
+ unfolding fset_to_set_trans
+ by (rule card_Diff1_less[OF finite_fset])
+
+lemma fcard_delete2_less: "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete (fdelete xs x) y) < fcard xs"
+ unfolding fset_to_set_trans
+ by (rule card_Diff2_less[OF finite_fset])
+
+lemma fcard_delete1_le: "fcard (fdelete xs x) <= fcard xs"
+ unfolding fset_to_set_trans
+ by (rule card_Diff1_le[OF finite_fset])
+
+lemma fcard_psubset: "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
+ unfolding fset_to_set_trans
+ by (rule card_psubset[OF finite_fset])
+
+lemma fcard_fmap_le: "fcard (fmap f xs) \<le> fcard xs"
+ unfolding fset_to_set_trans
+ by (rule card_image_le[OF finite_fset])
+
+lemma fin_fminus_fnotin: "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
+ unfolding fset_to_set_trans
+ by blast
+
+lemma fin_fnotin_fminus: "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
+ unfolding fset_to_set_trans
+ by blast
+
+lemma fin_mdef: "x |\<in>| F = ((x |\<notin>| (F - {|x|})) & (F = finsert x (F - {|x|})))"
+ unfolding fset_to_set_trans
+ by blast
+
+lemma fcard_fminus_finsert[simp]:
+ assumes "a |\<in>| A" and "a |\<notin>| B"
+ shows "fcard(A - finsert a B) = fcard(A - B) - 1"
+ using assms unfolding fset_to_set_trans
+ by (rule card_Diff_insert[OF finite_fset])
+
+lemma fcard_fminus_fsubset:
+ assumes "B |\<subseteq>| A"
+ shows "fcard (A - B) = fcard A - fcard B"
+ using assms unfolding fset_to_set_trans
+ by (rule card_Diff_subset[OF finite_fset])
+
+lemma fcard_fminus_subset_finter:
+ "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
+ unfolding fset_to_set_trans
+ by (rule card_Diff_subset_Int) (fold inter_set, rule finite_fset)
+
+
ML {*
-fun dest_fsetT (Type ("FSet.fset", [T])) = T
+fun dest_fsetT (Type (@{type_name fset}, [T])) = T
| dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
*}
--- a/Nominal/NewAlpha.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/NewAlpha.thy Mon May 10 15:45:04 2010 +0200
@@ -73,7 +73,7 @@
else Const (@{const_name supp},
Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ "atom set"})
val fvs = map fv_for_dt body_dts;
- val fv = mk_compound_fv fvs;
+ val fv = mk_compound_fv' lthy fvs;
fun alpha_for_dt dt =
if Datatype_Aux.is_rec_type dt
then nth alpha_frees (Datatype_Aux.body_index dt)
@@ -81,7 +81,7 @@
Datatype_Aux.typ_of_dtyp dt_descr sorts dt -->
Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ bool})
val alphas = map alpha_for_dt body_dts;
- val alpha = mk_compound_alpha alphas;
+ val alpha = mk_compound_alpha' lthy alphas;
val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ (Bound 0) $ rhs
val alpha_gen_ex = HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, alpha_gen_pre)
val t = Syntax.check_term lthy alpha_gen_ex
--- a/Nominal/NewParser.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/NewParser.thy Mon May 10 15:45:04 2010 +0200
@@ -519,13 +519,12 @@
val lthy17 = note_simp_suffix "bn" q_bn lthy16;
val _ = warning "Lifting eq-iff";
(*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
- val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff_simp
- val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0
- val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1
- val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2;
- val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0
- val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1
- val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2
+ val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff_simp
+ val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0
+ val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded1;
+ val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms Pair_eqvt}) q_eq_iff_pre0
+ val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1
+ val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2
val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
val q_dis = map (lift_thm qtys lthy18) rel_dists;
val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
--- a/Nominal/ROOT.ML Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/ROOT.ML Mon May 10 15:45:04 2010 +0200
@@ -2,7 +2,7 @@
no_document use_thys
["Ex/Lambda",
- "Ex/ExLF",
+ "Ex/LF",
"Ex/SingleLet",
"Ex/Ex1rec",
"Ex/Ex2",
@@ -10,10 +10,10 @@
"Ex/ExLet",
"Ex/ExLetRec",
"Ex/TypeSchemes",
- "Ex/ExLeroy",
+ "Ex/Modules",
"Ex/ExPS3",
"Ex/ExPS7",
- "Ex/ExCoreHaskell",
+ "Ex/CoreHaskell",
"Ex/Test",
"Manual/Term4"
];
--- a/Nominal/Rsp.thy Mon May 10 15:44:49 2010 +0200
+++ b/Nominal/Rsp.thy Mon May 10 15:45:04 2010 +0200
@@ -101,7 +101,7 @@
REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
asm_full_simp_tac (HOL_ss addsimps
- @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas}) THEN_ALL_NEW
+ @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas prod_rel.simps prod_fv.simps}) THEN_ALL_NEW
(split_conj_tac THEN_ALL_NEW TRY o resolve_tac
@{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
THEN_ALL_NEW
--- a/isar-keywords-quot.el Mon May 10 15:44:49 2010 +0200
+++ b/isar-keywords-quot.el Mon May 10 15:45:04 2010 +0200
@@ -61,6 +61,7 @@
"code_modulename"
"code_monad"
"code_pred"
+ "code_reflect"
"code_reserved"
"code_thms"
"code_type"
@@ -76,7 +77,7 @@
"declaration"
"declare"
"def"
- "defaultsort"
+ "default_sort"
"defer"
"defer_recdef"
"definition"
@@ -106,7 +107,10 @@
"header"
"help"
"hence"
- "hide"
+ "hide_class"
+ "hide_const"
+ "hide_fact"
+ "hide_type"
"inductive"
"inductive_cases"
"inductive_set"
@@ -205,12 +209,18 @@
"refute_params"
"remove_thy"
"rep_datatype"
+ "repdef"
+ "schematic_corollary"
+ "schematic_lemma"
+ "schematic_theorem"
"sect"
"section"
"setup"
"show"
"simproc_setup"
"sledgehammer"
+ "sledgehammer_params"
+ "smt_status"
"sorry"
"specification"
"subclass"
@@ -433,6 +443,7 @@
"code_module"
"code_modulename"
"code_monad"
+ "code_reflect"
"code_reserved"
"code_type"
"coinductive"
@@ -454,7 +465,10 @@
"finalconsts"
"fun"
"global"
- "hide"
+ "hide_class"
+ "hide_const"
+ "hide_fact"
+ "hide_type"
"inductive"
"inductive_set"
"instantiation"
@@ -487,6 +501,8 @@
"refute_params"
"setup"
"simproc_setup"
+ "sledgehammer_params"
+ "statespace"
"syntax"
"text"
"text_raw"
@@ -516,6 +532,9 @@
"quotient_type"
"recdef_tc"
"rep_datatype"
+ "schematic_corollary"
+ "schematic_lemma"
+ "schematic_theorem"
"specification"
"subclass"
"sublocale"