# HG changeset patch # User Cezary Kaliszyk # Date 1273499104 -7200 # Node ID 751d1349329b35050ca99bc455c8b253aa1d1ea4 # Parent c0ab7451b20dd1f697a439680aaf1d509be0189c# Parent 1f38489f1cf0f7ed0ef3f737b8d67589ea25daa0 merge diff -r c0ab7451b20d -r 751d1349329b Attic/Quot/Examples/LFex.thy --- 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 \ P2 x3 x4) \ ((x5 :: TRM) = x6 \ 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 diff -r c0ab7451b20d -r 751d1349329b Attic/Quot/Examples/Pair.thy --- /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 \ 'a) \ ('a \ 'a) \ bool" (infix "\" 100) +where + "(a, b) \ (c, d) = (a = c \ b = d \ a = d \ b = c)" + +lemma alpha_refl: + shows "z \ z" + by (case_tac z, auto) + +lemma alpha_equivp: + shows "equivp op \" + unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def + by auto + +quotient_type + 'a pair_set = "'a \ 'a" / alpha + by (auto intro: alpha_equivp) + +quotient_definition + "Two :: 'a \ 'a \ 'a pair_set" +is + "Pair :: 'a \ 'a \ ('a \ 'a)" + +fun + memb_both_lists +where + "memb_both_lists a (b, c) = (memb a b \ memb a c)" + +quotient_definition + "mem_fsets :: 'a \ 'a fset pair_set \ 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 \) OOO (prod_rel list_eq list_eq)) + (abs_pair_set \ prod_fun abs_fset abs_fset) + (prod_fun rep_fset rep_fset \ 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 \ 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 \ 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 \ 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 |\| b \ a |\| c)" + by (lifting memb_both_lists.simps) + +(* Doing it in 2 steps *) + +quotient_definition + "mem_lists :: 'a \ 'a list pair_set \ bool" +is memb_both_lists + +lemma [quot_respect]: "(op = ===> op \ ===> op =) memb_both_lists memb_both_lists" + by auto + +lemma [quot_respect]: "(op = ===> op = ===> op \) Pair Pair" + by auto + +lemma step1: "mem_lists a (Two b c) = (memb a b \ memb a c)" + by (lifting memb_both_lists.simps) + +lemma step2: "mem_fsets a (Two b c) = (a |\| b \ a |\| c)" + (* apply (lifting step1) ??? *) + oops + +(* Doing it in 2 steps the other way *) + +quotient_definition + "memb_both_fsets :: 'a \ 'a fset \ 'a fset \ 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 |\| b \ a |\| c)" + by (lifting memb_both_lists.simps) + +lemma step2: "mem_fsets a (Two b c) = (a |\| b \ a |\| c)" + (* ??? *) + oops + +end + diff -r c0ab7451b20d -r 751d1349329b Nominal-General/Nominal2_Eqvt.thy --- 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 \ (snd x) = snd (p \ x)" by (cases x) simp +lemma split_eqvt[eqvt]: + shows "p \ (split P x) = split (p \ P) (p \ x)" + unfolding split_def + by (perm_simp) (rule refl) + section {* Units *} lemma supp_unit: @@ -386,10 +391,16 @@ lemma fixes P :: "(('b \ bool) \ ('b::pt)) \ ('a::pt)" - shows "(p \ (P The)) = foo" + shows "p \ (P The) = foo" apply(perm_simp exclude: The) oops +lemma + fixes P :: "('a::pt) \ ('b::pt) \ bool" + shows "p \ (\(a, b). P a b) = (\(a, b). (p \ P) a b)" +apply(perm_simp) +oops + thm eqvts thm eqvts_raw diff -r c0ab7451b20d -r 751d1349329b Nominal-General/nominal_eqvt.ML --- 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 diff -r c0ab7451b20d -r 751d1349329b Nominal-General/nominal_permeq.ML --- 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 = diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/CoreHaskell.thy --- /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 \ atom list" +and bv_vs :: "vars \ atom list" +and bv_tvs :: "tvars \ atom list" +and bv_cvs :: "cvars \ 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 \* - p = as \* (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 \ 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 \ 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 \ 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 \ vars \ vars" +is "permute_bv_vs_raw" +quotient_definition "permute_bv_cvs :: perm \ cvars \ cvars" +is "permute_bv_cvs_raw" +quotient_definition "permute_bv_tvs :: perm \ tvars \ tvars" +is "permute_bv_tvs_raw" +quotient_definition "permute_bv :: perm \ pat \ pat" +is "permute_bv_raw" + +lemma rsp_pre: + "alpha_tvars_raw d a \ alpha_tvars_raw (permute_bv_tvs_raw x d) (permute_bv_tvs_raw x a)" + "alpha_cvars_raw e b \ alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)" + "alpha_vars_raw f c \ 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 \ bv_cvs b = bv_cvs (permute_bv_cvs p b)" + "p \ bv_tvs c = bv_tvs (permute_bv_tvs p c)" + "p \ 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 \ 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) \* q \ (ACons pat trm al) = ACons (permute_bv q pat) (q \ 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 \* pa \ alpha_bv_tvs (pa \ 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 \* pa \ alpha_bv_cvs (pa \ 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 \* pa \ alpha_bv_vs (pa \ 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 \* pa \ alpha_bv (pa \ 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: "\b. P1 b KStar" + and a02: "\tkind1 tkind2 b. \\c. P1 c tkind1; \c. P1 c tkind2\ \ P1 b (KFun tkind1 tkind2)" + and a03: "\ty1 ty2 b. \\c. P3 c ty1; \c. P3 c ty2\ \ P2 b (CKEq ty1 ty2)" + and a04: "\tvar b. P3 b (TVar tvar)" + and a05: "\string b. P3 b (TC string)" + and a06: "\ty1 ty2 b. \\c. P3 c ty1; \c. P3 c ty2\ \ P3 b (TApp ty1 ty2)" + and a07: "\string ty_lst b. \\c. P4 c ty_lst\ \ P3 b (TFun string ty_lst)" + and a08: "\tvar tkind ty b. \\c. P1 c tkind; \c. P3 c ty; atom tvar \ b\ + \ P3 b (TAll tvar tkind ty)" + and a09: "\ck ty b. \\c. P2 c ck; \c. P3 c ty\ \ P3 b (TEq ck ty)" + and a10: "\b. P4 b TsNil" + and a11: "\ty ty_lst b. \\c. P3 c ty; \c. P4 c ty_lst\ \ P4 b (TsCons ty ty_lst)" + and a12: "\string b. P5 b (CVar string)" + and a12a:"\str b. P5 b (CConst str)" + and a13: "\co1 co2 b. \\c. P5 c co1; \c. P5 c co2\ \ P5 b (CApp co1 co2)" + and a14: "\string co_lst b. \\c. P6 c co_lst\ \ P5 b (CFun string co_lst)" + and a15: "\tvar ckind co b. \\c. P2 c ckind; \c. P5 c co; atom tvar \ b\ + \ P5 b (CAll tvar ckind co)" + and a16: "\ck co b. \\c. P2 c ck; \c. P5 c co\ \ P5 b (CEq ck co)" + and a17: "\ty b. \\c. P3 c ty\ \ P5 b (CRefl ty)" + and a17a: "\co b. \\c. P5 c co\ \ P5 b (CSym co)" + and a18: "\co1 co2 b. \\c. P5 c co1; \c. P5 c co2\ \ P5 b (CCir co1 co2)" + and a18a:"\co ty b. \\c. P5 c co; \c. P3 c ty\ \ P5 b (CAt co ty)" + and a19: "\co b. \\c. P5 c co\ \ P5 b (CLeft co)" + and a20: "\co b. \\c. P5 c co\ \ P5 b (CRight co)" + and a21: "\co1 co2 b. \\c. P5 c co1; \c. P5 c co2\ \ P5 b (CSim co1 co2)" + and a22: "\co b. \\c. P5 c co\ \ P5 b (CRightc co)" + and a23: "\co b. \\c. P5 c co\ \ P5 b (CLeftc co)" + and a24: "\co1 co2 b. \\c. P5 c co1; \c. P5 c co2\ \ P5 b (CCoe co1 co2)" + and a25: "\b. P6 b CsNil" + and a26: "\co co_lst b. \\c. P5 c co; \c. P6 c co_lst\ \ P6 b (CsCons co co_lst)" + and a27: "\var b. P7 b (Var var)" + and a28: "\string b. P7 b (K string)" + and a29: "\tvar tkind trm b. \\c. P1 c tkind; \c. P7 c trm; atom tvar \ b\ + \ P7 b (LAMT tvar tkind trm)" + and a30: "\tvar ckind trm b. \\c. P2 c ckind; \c. P7 c trm; atom tvar \ b\ + \ P7 b (LAMC tvar ckind trm)" + and a31: "\trm ty b. \\c. P7 c trm; \c. P3 c ty\ \ P7 b (AppT trm ty)" + and a31a:"\trm co b. \\c. P7 c trm; \c. P5 c co\ \ P7 b (AppC trm co)" + and a32: "\var ty trm b. \\c. P3 c ty; \c. P7 c trm; atom var \ b\ \ P7 b (Lam var ty trm)" + and a33: "\trm1 trm2 b. \\c. P7 c trm1; \c. P7 c trm2\ \ P7 b (App trm1 trm2)" + and a34: "\var ty trm1 trm2 b. \\c. P3 c ty; \c. P7 c trm1; \c. P7 c trm2; atom var \ b\ + \ P7 b (Let var ty trm1 trm2)" + and a35: "\trm assoc_lst b. \\c. P7 c trm; \c. P8 c assoc_lst\ \ P7 b (Case trm assoc_lst)" + and a36: "\trm ty b. \\c. P7 c trm; \c. P3 c ty\ \ P7 b (Cast trm ty)" + and a37: "\b. P8 b ANil" + and a38: "\pat trm assoc_lst b. \\c. P9 c pat; \c. P7 c trm; \c. P8 c assoc_lst; set (bv (pat)) \* b\ + \ P8 b (ACons pat trm assoc_lst)" + and a39: "\string tvars cvars vars b. \\c. P11 c tvars; \c. P12 c cvars; \c. P10 c vars\ + \ P9 b (Kpat string tvars cvars vars)" + and a40: "\b. P10 b VsNil" + and a41: "\var ty vars b. \\c. P3 c ty; \c. P10 c vars\ \ P10 b (VsCons var ty vars)" + and a42: "\b. P11 b TvsNil" + and a43: "\tvar tkind tvars b. \\c. P1 c tkind; \c. P11 c tvars\ + \ P11 b (TvsCons tvar tkind tvars)" + and a44: "\b. P12 b CvsNil" + and a45: "\tvar ckind cvars b. \\c. P2 c ckind; \c. P12 c cvars\ + \ P12 b (CvsCons tvar ckind cvars)" + shows "P1 (a :: 'a :: pt) tkind \ + P2 (b :: 'b :: pt) ckind \ + P3 (c :: 'c :: {pt,fs}) ty \ + P4 (d :: 'd :: pt) ty_lst \ + P5 (e :: 'e :: {pt,fs}) co \ + P6 (f :: 'f :: pt) co_lst \ + P7 (g :: 'g :: {pt,fs}) trm \ + P8 (h :: 'h :: {pt,fs}) assoc_lst \ + P9 (i :: 'i :: pt) pat \ + P10 (j :: 'j :: pt) vars \ + P11 (k :: 'k :: pt) tvars \ + P12 (l :: 'l :: pt) cvars" +proof - + have a1: "(\p a. P1 a (p \ tkind))" and "(\p b. P2 b (p \ ckind))" and "(\p c. P3 c (p \ ty))" and "(\p d. P4 d (p \ ty_lst))" and "(\p e. P5 e (p \ co))" and " (\p f. P6 f (p \ co_lst))" and "(\p g. P7 g (p \ trm))" and "(\p h. P8 h (p \ assoc_lst))" and a1:"(\p q i. P9 i (permute_bv p (q \ pat)))" and a2:"(\p q j. P10 j (permute_bv_vs q (p \ vars)))" and a3:"(\p q k. P11 k ( permute_bv_tvs q (p \ tvars)))" and a4:"(\p q l. P12 l (permute_bv_cvs q (p \ 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 "\pa. ((pa \ (atom (p \ tvar))) \ c \ + supp (Abs (p \ {atom tvar}) (p \ ty)) \* pa)") + apply clarify + apply (simp only: perm) + apply(rule_tac t="TAll (p \ tvar) (p \ tkind) (p \ ty)" + and s="TAll (pa \ p \ tvar) (p \ tkind) (pa \ p \ 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 \ p \ ty) - {atom (pa \ p \ tvar)}" + and s="pa \ (p \ supp ty - {p \ 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 "\pa. ((pa \ (atom (p \ cvar))) \ e \ + supp (Abs (p \ {atom cvar}) (p \ co)) \* pa)") + apply clarify + apply (simp only: perm) + apply(rule_tac t="CAll (p \ cvar) (p \ ckind) (p \ co)" + and s="CAll (pa \ p \ cvar) (p \ ckind) (pa \ p \ 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 \ p \ co) - {atom (pa \ p \ cvar)}" + and s="pa \ (p \ supp co - {p \ 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 "\pa. ((pa \ (atom (p \ tvar))) \ g \ + supp (Abs (p \ {atom tvar}) (p \ trm)) \* pa)") + apply clarify + apply (simp only: perm) + apply(rule_tac t="LAMT (p \ tvar) (p \ tkind) (p \ trm)" + and s="LAMT (pa \ p \ tvar) (p \ tkind) (pa \ p \ 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 \ p \ trm) - {atom (pa \ p \ tvar)}" + and s="pa \ (p \ supp trm - {p \ 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 "\pa. ((pa \ (atom (p \ cvar))) \ g \ + supp (Abs (p \ {atom cvar}) (p \ trm)) \* pa)") + apply clarify + apply (simp only: perm) + apply(rule_tac t="LAMC (p \ cvar) (p \ ckind) (p \ trm)" + and s="LAMC (pa \ p \ cvar) (p \ ckind) (pa \ p \ 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 \ p \ trm) - {atom (pa \ p \ cvar)}" + and s="pa \ (p \ supp trm - {p \ 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 "\pa. ((pa \ (atom (p \ var))) \ g \ + supp (Abs (p \ {atom var}) (p \ trm)) \* pa)") + apply clarify + apply (simp only: perm) + apply(rule_tac t="Lam (p \ var) (p \ ty) (p \ trm)" + and s="Lam (pa \ p \ var) (p \ ty) (pa \ p \ 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 \ p \ trm) - {atom (pa \ p \ var)}" + and s="pa \ (p \ supp trm - {p \ 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 "\pa. ((pa \ (atom (p \ var))) \ g \ + supp (Abs (p \ {atom var}) (p \ trm2)) \* pa)") + apply clarify + apply (simp only: perm) + apply(rule_tac t="Let (p \ var) (p \ ty) (p \ trm1) (p \ trm2)" + and s="Let (pa \ p \ var) (p \ ty) (p \ trm1) (pa \ p \ 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 \ p \ trm2) - {atom (pa \ p \ var)}" + and s="pa \ (p \ supp trm2 - {p \ 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 "\pa. ((pa \ (set (bv (p \ pat)))) \* h \ + supp (Abs_lst (p \ (bv pat)) (p \ trm)) \* 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 \ tkind)" and "P2 b (0 \ ckind)" "P3 c (0 \ ty)" and "P4 d (0 \ ty_lst)" and "P5 e (0 \ co)" and "P6 f (0 \ co_lst)" and "P7 g (0 \ trm)" and "P8 h (0 \ assoc_lst)" by (blast+) + moreover have "P9 i (permute_bv 0 (0 \ pat))" and "P10 j (permute_bv_vs 0 (0 \ vars))" and "P11 k (permute_bv_tvs 0 (0 \ tvars))" and "P12 l (permute_bv_cvs 0 (0 \ 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 + diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/Ex1rec.thy --- 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 diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/Ex2.thy --- 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 diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/Ex3.thy --- 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 diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/ExCoreHaskell.thy --- 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 \ atom list" -and bv_vs :: "vars \ atom list" -and bv_tvs :: "tvars \ atom list" -and bv_cvs :: "cvars \ 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 \* - p = as \* (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 \ 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 \ 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 \ 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 \ vars \ vars" -is "permute_bv_vs_raw" -quotient_definition "permute_bv_cvs :: perm \ cvars \ cvars" -is "permute_bv_cvs_raw" -quotient_definition "permute_bv_tvs :: perm \ tvars \ tvars" -is "permute_bv_tvs_raw" -quotient_definition "permute_bv :: perm \ pat \ pat" -is "permute_bv_raw" - -lemma rsp_pre: - "alpha_tvars_raw d a \ alpha_tvars_raw (permute_bv_tvs_raw x d) (permute_bv_tvs_raw x a)" - "alpha_cvars_raw e b \ alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)" - "alpha_vars_raw f c \ 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 \ bv_cvs b = bv_cvs (permute_bv_cvs p b)" - "p \ bv_tvs c = bv_tvs (permute_bv_tvs p c)" - "p \ 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 \ 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) \* q \ (ACons pat trm al) = ACons (permute_bv q pat) (q \ 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 \* pa \ alpha_bv_tvs (pa \ 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 \* pa \ alpha_bv_cvs (pa \ 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 \* pa \ alpha_bv_vs (pa \ 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 \* pa \ alpha_bv (pa \ 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: "\b. P1 b KStar" - and a02: "\tkind1 tkind2 b. \\c. P1 c tkind1; \c. P1 c tkind2\ \ P1 b (KFun tkind1 tkind2)" - and a03: "\ty1 ty2 b. \\c. P3 c ty1; \c. P3 c ty2\ \ P2 b (CKEq ty1 ty2)" - and a04: "\tvar b. P3 b (TVar tvar)" - and a05: "\string b. P3 b (TC string)" - and a06: "\ty1 ty2 b. \\c. P3 c ty1; \c. P3 c ty2\ \ P3 b (TApp ty1 ty2)" - and a07: "\string ty_lst b. \\c. P4 c ty_lst\ \ P3 b (TFun string ty_lst)" - and a08: "\tvar tkind ty b. \\c. P1 c tkind; \c. P3 c ty; atom tvar \ b\ - \ P3 b (TAll tvar tkind ty)" - and a09: "\ck ty b. \\c. P2 c ck; \c. P3 c ty\ \ P3 b (TEq ck ty)" - and a10: "\b. P4 b TsNil" - and a11: "\ty ty_lst b. \\c. P3 c ty; \c. P4 c ty_lst\ \ P4 b (TsCons ty ty_lst)" - and a12: "\string b. P5 b (CVar string)" - and a12a:"\str b. P5 b (CConst str)" - and a13: "\co1 co2 b. \\c. P5 c co1; \c. P5 c co2\ \ P5 b (CApp co1 co2)" - and a14: "\string co_lst b. \\c. P6 c co_lst\ \ P5 b (CFun string co_lst)" - and a15: "\tvar ckind co b. \\c. P2 c ckind; \c. P5 c co; atom tvar \ b\ - \ P5 b (CAll tvar ckind co)" - and a16: "\ck co b. \\c. P2 c ck; \c. P5 c co\ \ P5 b (CEq ck co)" - and a17: "\ty b. \\c. P3 c ty\ \ P5 b (CRefl ty)" - and a17a: "\co b. \\c. P5 c co\ \ P5 b (CSym co)" - and a18: "\co1 co2 b. \\c. P5 c co1; \c. P5 c co2\ \ P5 b (CCir co1 co2)" - and a18a:"\co ty b. \\c. P5 c co; \c. P3 c ty\ \ P5 b (CAt co ty)" - and a19: "\co b. \\c. P5 c co\ \ P5 b (CLeft co)" - and a20: "\co b. \\c. P5 c co\ \ P5 b (CRight co)" - and a21: "\co1 co2 b. \\c. P5 c co1; \c. P5 c co2\ \ P5 b (CSim co1 co2)" - and a22: "\co b. \\c. P5 c co\ \ P5 b (CRightc co)" - and a23: "\co b. \\c. P5 c co\ \ P5 b (CLeftc co)" - and a24: "\co1 co2 b. \\c. P5 c co1; \c. P5 c co2\ \ P5 b (CCoe co1 co2)" - and a25: "\b. P6 b CsNil" - and a26: "\co co_lst b. \\c. P5 c co; \c. P6 c co_lst\ \ P6 b (CsCons co co_lst)" - and a27: "\var b. P7 b (Var var)" - and a28: "\string b. P7 b (K string)" - and a29: "\tvar tkind trm b. \\c. P1 c tkind; \c. P7 c trm; atom tvar \ b\ - \ P7 b (LAMT tvar tkind trm)" - and a30: "\tvar ckind trm b. \\c. P2 c ckind; \c. P7 c trm; atom tvar \ b\ - \ P7 b (LAMC tvar ckind trm)" - and a31: "\trm ty b. \\c. P7 c trm; \c. P3 c ty\ \ P7 b (AppT trm ty)" - and a31a:"\trm co b. \\c. P7 c trm; \c. P5 c co\ \ P7 b (AppC trm co)" - and a32: "\var ty trm b. \\c. P3 c ty; \c. P7 c trm; atom var \ b\ \ P7 b (Lam var ty trm)" - and a33: "\trm1 trm2 b. \\c. P7 c trm1; \c. P7 c trm2\ \ P7 b (App trm1 trm2)" - and a34: "\var ty trm1 trm2 b. \\c. P3 c ty; \c. P7 c trm1; \c. P7 c trm2; atom var \ b\ - \ P7 b (Let var ty trm1 trm2)" - and a35: "\trm assoc_lst b. \\c. P7 c trm; \c. P8 c assoc_lst\ \ P7 b (Case trm assoc_lst)" - and a36: "\trm ty b. \\c. P7 c trm; \c. P3 c ty\ \ P7 b (Cast trm ty)" - and a37: "\b. P8 b ANil" - and a38: "\pat trm assoc_lst b. \\c. P9 c pat; \c. P7 c trm; \c. P8 c assoc_lst; set (bv (pat)) \* b\ - \ P8 b (ACons pat trm assoc_lst)" - and a39: "\string tvars cvars vars b. \\c. P11 c tvars; \c. P12 c cvars; \c. P10 c vars\ - \ P9 b (Kpat string tvars cvars vars)" - and a40: "\b. P10 b VsNil" - and a41: "\var ty vars b. \\c. P3 c ty; \c. P10 c vars\ \ P10 b (VsCons var ty vars)" - and a42: "\b. P11 b TvsNil" - and a43: "\tvar tkind tvars b. \\c. P1 c tkind; \c. P11 c tvars\ - \ P11 b (TvsCons tvar tkind tvars)" - and a44: "\b. P12 b CvsNil" - and a45: "\tvar ckind cvars b. \\c. P2 c ckind; \c. P12 c cvars\ - \ P12 b (CvsCons tvar ckind cvars)" - shows "P1 (a :: 'a :: pt) tkind \ - P2 (b :: 'b :: pt) ckind \ - P3 (c :: 'c :: {pt,fs}) ty \ - P4 (d :: 'd :: pt) ty_lst \ - P5 (e :: 'e :: {pt,fs}) co \ - P6 (f :: 'f :: pt) co_lst \ - P7 (g :: 'g :: {pt,fs}) trm \ - P8 (h :: 'h :: {pt,fs}) assoc_lst \ - P9 (i :: 'i :: pt) pat \ - P10 (j :: 'j :: pt) vars \ - P11 (k :: 'k :: pt) tvars \ - P12 (l :: 'l :: pt) cvars" -proof - - have a1: "(\p a. P1 a (p \ tkind))" and "(\p b. P2 b (p \ ckind))" and "(\p c. P3 c (p \ ty))" and "(\p d. P4 d (p \ ty_lst))" and "(\p e. P5 e (p \ co))" and " (\p f. P6 f (p \ co_lst))" and "(\p g. P7 g (p \ trm))" and "(\p h. P8 h (p \ assoc_lst))" and a1:"(\p q i. P9 i (permute_bv p (q \ pat)))" and a2:"(\p q j. P10 j (permute_bv_vs q (p \ vars)))" and a3:"(\p q k. P11 k ( permute_bv_tvs q (p \ tvars)))" and a4:"(\p q l. P12 l (permute_bv_cvs q (p \ 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 "\pa. ((pa \ (atom (p \ tvar))) \ c \ - supp (Abs (p \ {atom tvar}) (p \ ty)) \* pa)") - apply clarify - apply (simp only: perm) - apply(rule_tac t="TAll (p \ tvar) (p \ tkind) (p \ ty)" - and s="TAll (pa \ p \ tvar) (p \ tkind) (pa \ p \ 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 \ p \ ty) - {atom (pa \ p \ tvar)}" - and s="pa \ (p \ supp ty - {p \ 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 "\pa. ((pa \ (atom (p \ cvar))) \ e \ - supp (Abs (p \ {atom cvar}) (p \ co)) \* pa)") - apply clarify - apply (simp only: perm) - apply(rule_tac t="CAll (p \ cvar) (p \ ckind) (p \ co)" - and s="CAll (pa \ p \ cvar) (p \ ckind) (pa \ p \ 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 \ p \ co) - {atom (pa \ p \ cvar)}" - and s="pa \ (p \ supp co - {p \ 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 "\pa. ((pa \ (atom (p \ tvar))) \ g \ - supp (Abs (p \ {atom tvar}) (p \ trm)) \* pa)") - apply clarify - apply (simp only: perm) - apply(rule_tac t="LAMT (p \ tvar) (p \ tkind) (p \ trm)" - and s="LAMT (pa \ p \ tvar) (p \ tkind) (pa \ p \ 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 \ p \ trm) - {atom (pa \ p \ tvar)}" - and s="pa \ (p \ supp trm - {p \ 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 "\pa. ((pa \ (atom (p \ cvar))) \ g \ - supp (Abs (p \ {atom cvar}) (p \ trm)) \* pa)") - apply clarify - apply (simp only: perm) - apply(rule_tac t="LAMC (p \ cvar) (p \ ckind) (p \ trm)" - and s="LAMC (pa \ p \ cvar) (p \ ckind) (pa \ p \ 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 \ p \ trm) - {atom (pa \ p \ cvar)}" - and s="pa \ (p \ supp trm - {p \ 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 "\pa. ((pa \ (atom (p \ var))) \ g \ - supp (Abs (p \ {atom var}) (p \ trm)) \* pa)") - apply clarify - apply (simp only: perm) - apply(rule_tac t="Lam (p \ var) (p \ ty) (p \ trm)" - and s="Lam (pa \ p \ var) (p \ ty) (pa \ p \ 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 \ p \ trm) - {atom (pa \ p \ var)}" - and s="pa \ (p \ supp trm - {p \ 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 "\pa. ((pa \ (atom (p \ var))) \ g \ - supp (Abs (p \ {atom var}) (p \ trm2)) \* pa)") - apply clarify - apply (simp only: perm) - apply(rule_tac t="Let (p \ var) (p \ ty) (p \ trm1) (p \ trm2)" - and s="Let (pa \ p \ var) (p \ ty) (p \ trm1) (pa \ p \ 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 \ p \ trm2) - {atom (pa \ p \ var)}" - and s="pa \ (p \ supp trm2 - {p \ 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 "\pa. ((pa \ (set (bv (p \ pat)))) \* h \ - supp (Abs_lst (p \ (bv pat)) (p \ trm)) \* 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 \ tkind)" and "P2 b (0 \ ckind)" "P3 c (0 \ ty)" and "P4 d (0 \ ty_lst)" and "P5 e (0 \ co)" and "P6 f (0 \ co_lst)" and "P7 g (0 \ trm)" and "P8 h (0 \ assoc_lst)" by (blast+) - moreover have "P9 i (permute_bv 0 (0 \ pat))" and "P10 j (permute_bv_vs 0 (0 \ vars))" and "P11 k (permute_bv_tvs 0 (0 \ tvars))" and "P12 l (permute_bv_cvs 0 (0 \ 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 - diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/ExLF.thy --- 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 - - - - diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/ExLeroy.thy --- 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 \ atom set" -and Cbinders :: "spec \ 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 - - - diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/ExLet.thy --- 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 diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/ExLetMult.thy --- 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 diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/ExLetRec.thy --- 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 diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/ExNotRsp.thy --- 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} \ bv6 t" -| "bv6 (Lt6 l r) = bv6 l \ 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 \ 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 - - - diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/ExPS3.thy --- 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 \ atom set" + bp :: "pat \ atom set" where "bp (PVar x) = {atom x}" | "bp (PUnit) = {}" | "bp (PPair p1 p2) = bp p1 \ 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 diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/ExPS6.thy --- 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 \ atom set" + bp :: "pat \ atom list" where - "bp6 (PVar' x) = {atom x}" -| "bp6 (PUnit') = {}" -| "bp6 (PPair' p1 p2) = bp6 p1 \ 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 diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/ExPS7.thy --- 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 \ atom set" and - b7s :: "lrbs \ atom set" + b :: "lrb \ atom set" and + bs :: "lrbs \ atom set" where - "b7 (Assign x e) = {atom x}" -| "b7s (Single a) = b7 a" -| "b7s (More a as) = (b7 a) \ (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) \ (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 diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/ExPS8.thy --- 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 diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/LF.thy --- /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 + + + + diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/Lambda.thy --- 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*} (* diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/Modules.thy --- /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 \ atom set" +and Cbinders :: "spec \ 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 + + + diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/NoneExamples.thy --- /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} \ bv t" +| "bv (Lt l r) = bv l \ 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 \ 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 + + + diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/Term8.thy --- 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 diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/TestMorePerm.thy --- 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 diff -r c0ab7451b20d -r 751d1349329b Nominal/Ex/TypeSchemes.thy --- 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: diff -r c0ab7451b20d -r 751d1349329b Nominal/FSet.thy --- 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 \ 'a \ '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 \ 'a list \ '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 \ 'b \ 'b) \ 'b \ 'a list \ '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 \ OOO op \) r r" proof - show c: "list_rel op \ r r" by (rule list_rel_refl) - have d: "r \ r" by (rule equivp_reflp[OF fset_equivp]) - show b: "(op \ OO list_rel op \) r r" by (rule pred_compI) (rule d, rule c) + have *: "r \ r" by (rule equivp_reflp[OF fset_equivp]) + show "list_rel op \ r r" by (rule list_rel_refl) + with * show "(op \ OO list_rel op \) r r" .. qed lemma Quotient_fset_list: shows "Quotient (list_rel op \) (map abs_fset) (map rep_fset)" by (fact list_quotient[OF Quotient_fset]) -lemma set_in_eq: "(\e. ((e \ A) \ (e \ B))) \ A = B" +lemma set_in_eq: "(\e. ((e \ xs) \ (e \ ys))) \ xs = ys" by (rule eq_reflection) auto lemma map_rel_cong: "b \ ba \ map f b \ map f ba" @@ -117,7 +124,8 @@ show "(list_rel op \ OOO op \) s s" by (rule compose_list_refl) next assume a: "(list_rel op \ OOO op \) r s" - then have b: "map abs_fset r \ map abs_fset s" proof (elim pred_compE) + then have b: "map abs_fset r \ map abs_fset s" + proof (elim pred_compE) fix b ba assume c: "list_rel op \ r b" assume d: "b \ ba" @@ -208,6 +216,14 @@ "(op \ ===> op = ===> op \) 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 \ \ memb x ys)" + by (induct ys arbitrary: xs) + (simp_all add: not_memb_nil memb_delete_raw memb_cons_iff) + +lemma [quot_respect]: + "(op \ ===> op \ ===> op \) fminus_raw fminus_raw" + by (simp add: memb_def[symmetric] fminus_raw_memb) + lemma fcard_raw_gt_0: assumes a: "x \ set xs" shows "0 < fcard_raw xs" @@ -221,20 +237,43 @@ assumes a: "xs \ ys" shows "fcard_raw xs = fcard_raw ys" using a - apply (induct xs arbitrary: ys) - apply (auto simp add: memb_def) - apply (subgoal_tac "\x. (x \ set xs) = (x \ set ys)") - apply (auto) - apply (drule_tac x="x" in spec) - apply (blast) - apply (drule_tac x="[x \ ys. x \ a]" in meta_spec) - apply (simp add: fcard_raw_delete_one memb_def) - apply (case_tac "a \ set ys") - apply (simp only: if_True) - apply (subgoal_tac "\x. (x \ set xs) = (x \ set ys \ x \ 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 \ ys" by fact + have b: "\ys. xs \ ys \ fcard_raw xs = fcard_raw ys" by fact + show ?case proof (cases "a \ set xs") + assume c: "a \ set xs" + have "\x. (x \ set xs) = (x \ set ys)" + proof (intro allI iffI) + fix x + assume "x \ set xs" + then show "x \ set ys" using a by auto + next + fix x + assume d: "x \ set ys" + have e: "(x \ set (a # xs)) = (x \ set ys)" using a by simp + show "x \ 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 \ set xs" + have d: "xs \ [x\ys . x \ a] \ fcard_raw xs = fcard_raw [x\ys . x \ a]" using b by simp + have "Suc (fcard_raw xs) = fcard_raw ys" + proof (cases "a \ set ys") + assume e: "a \ set ys" + have f: "\x. (x \ set xs) = (x \ set ys \ x \ 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 \ ===> op =) fcard_raw fcard_raw" @@ -306,8 +345,8 @@ obtain xb where e: "xb \ set x" and f: "xa \ set xb" using d by auto have "\y. y \ set x' \ xb \ y" by (rule list_rel_find_element[OF e a]) then obtain ya where h: "ya \ set x'" and i: "xb \ ya" by auto - have j: "ya \ set y'" using b h by simp - have "\yb. yb \ set y \ ya \ yb" by (rule list_rel_find_element[OF j c]) + have "ya \ set y'" using b h by simp + then have "\yb. yb \ set y \ ya \ 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 \ concat b" by simp qed +lemma [quot_respect]: + "((op =) ===> op \ ===> op \) 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 @) \ ('a list \ 'a list \ 'a list)" abbreviation - funion (infixl "|\|" 65) + funion (infixl "|\|" 65) where "xs |\| ys \ sup (xs :: 'a fset) ys" quotient_definition - "inf \ ('a fset \ 'a fset \ 'a fset)" + "inf \ ('a fset \ 'a fset \ 'a fset)" is "finter_raw \ ('a list \ 'a list \ 'a list)" @@ -437,6 +481,11 @@ where "xs |\| ys \ inf (xs :: 'a fset) ys" +quotient_definition + "minus \ ('a fset \ 'a fset \ 'a fset)" +is + "fminus_raw \ ('a list \ 'a list \ 'a list)" + instance proof fix x y z :: "'a fset" @@ -496,10 +545,10 @@ where "x |\| S \ \ (x |\| S)" -section {* Other constants on the Quotient Type *} +section {* Other constants on the Quotient Type *} quotient_definition - "fcard :: 'a fset \ nat" + "fcard :: 'a fset \ nat" is "fcard_raw" @@ -509,11 +558,11 @@ "map" quotient_definition - "fdelete :: 'a fset \ 'a \ 'a fset" + "fdelete :: 'a fset \ 'a \ 'a fset" is "delete_raw" quotient_definition - "fset_to_set :: 'a fset \ 'a set" + "fset_to_set :: 'a fset \ 'a set" is "set" quotient_definition @@ -525,6 +574,11 @@ is "concat" +quotient_definition + "ffilter :: ('a \ bool) \ 'a fset \ 'a fset" +is + "filter" + text {* Compositional Respectfullness and Preservation *} lemma [quot_respect]: "(list_rel op \ OOO op \) [] []" @@ -636,6 +690,10 @@ "sub_list (x # xs) ys = (memb x ys \ 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 = []) \ (\x ys. ((\ memb x ys) \ (xs \ 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 "\ memb x ys" and "xs \ x # ys" +proof (induct xs arbitrary: x ys) + case Nil + then show thesis by simp +next + case (Cons a xs) + have a: "\xs = [] \ thesis; \x ys. \\ memb x ys; xs \ x # ys\ \ thesis\ \ thesis" by fact + have b: "\x' ys'. \\ memb x' ys'; a # xs \ x' # ys'\ \ thesis" by fact + have c: "xs = [] \ thesis" by (metis no_memb_nil singleton_list_eq b) + have "\x ys. \\ memb x ys; xs \ x # ys\ \ thesis" + proof - + fix x :: 'a + fix ys :: "'a list" + assume d:"\ memb x ys" + assume e:"xs \ x # ys" + show thesis + proof (cases "x = a") + assume h: "x = a" + then have f: "\ memb a ys" using d by simp + have g: "a # xs \ a # ys" using e h by auto + show thesis using b f g by simp + next + assume h: "x \ a" + then have f: "\ memb x (a # ys)" using d unfolding memb_def by auto + have g: "a # xs \ 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 \ y)" +lemma set_cong: + shows "(x \ y) = (set x = set y)" by auto lemma inj_map_eq_iff: @@ -812,13 +884,13 @@ case (Suc m) have b: "l \ r" by fact have d: "fcard_raw l = Suc m" by fact - have "\a. memb a l" by (rule fcard_raw_suc_memb[OF d]) + then have "\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 \ 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 \ r \ list_eq2 l r" by blast qed +text {* Set *} + +lemma sub_list_set: "sub_list xs ys = (set xs \ 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 \ \ list_eq xs ys) = (set xs \ 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 \ set xs)" + by (simp only: memb_def) + +lemma filter_set: "set (filter P xs) = P \ (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 \ 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) = (\ x. memb x xs \ P x \ Q x)" +unfolding sub_list_def memb_def by auto + +lemma list_eq_filter: "list_eq (filter P xs) (filter Q xs) = (\x. memb x xs \ P x = Q x)" +unfolding memb_def by auto + text {* Lifted theorems *} lemma not_fin_fnil: "x |\| {||}" @@ -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) = (\x. S = {|x|})" by (lifting fcard_raw_1) -lemma fcard_gt_0: +lemma fcard_gt_0: shows "x \ fset_to_set S \ 0 < fcard S" by (lifting fcard_raw_gt_0) -lemma fcard_not_fin: +lemma fcard_not_fin: shows "(x |\| 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 "{||} |\| S = S" - and "finsert x S |\| T = finsert x (S |\| 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 |\| {||} = S" - by (lifting append_Nil2) +lemma funion_finsert[simp]: + shows "finsert x S |\| T = finsert x (S |\| T)" + by (lifting append.simps(2)) lemma singleton_union_left: "{|a|} |\| S = finsert a S" @@ -942,7 +1049,8 @@ section {* Induction and Cases rules for finite sets *} lemma fset_strong_cases: - "S = {||} \ (\x T. x |\| T \ S = finsert x T)" + obtains "xs = {||}" + | x ys where "x |\| 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: "\x S. \x |\| S; P S\ \ 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: "\xs ys. Suc (fcard xs) = (fcard ys) \ P xs \ 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 |\| 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 \ (fmap f S = fmap f T) = (S = T)" @@ -1002,6 +1124,44 @@ "x |\| S |\| T \ x |\| S \ x |\| T" by (lifting memb_append) +text {* to_set *} + +lemma fin_set: "(x |\| xs) = (x \ fset_to_set xs)" + by (lifting memb_set) + +lemma fnotin_set: "(x |\| xs) = (x \ 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 |\| ys) = (fset_to_set xs \ fset_to_set ys)" + by (lifting sub_list_set) + +lemma fsubset_set: "(xs |\| ys) = (fset_to_set xs \ fset_to_set ys)" + unfolding less_fset by (lifting sub_list_neq_set) + +lemma ffilter_set: "fset_to_set (ffilter P xs) = P \ 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 |\| ys) = fset_to_set xs \ fset_to_set ys" + by (lifting inter_raw_set) + +lemma union_set: "fset_to_set (xs |\| ys) = fset_to_set xs \ 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 |\| fdelete S y \ x |\| S \ x \ y" by (lifting memb_delete_raw) -lemma fin_fdelete_ident: +lemma fin_fdelete_ident: shows "x |\| fdelete S x" by (lifting memb_delete_raw_ident) -lemma not_memb_fdelete_ident: +lemma not_memb_fdelete_ident: shows "x |\| S \ 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 |\| xs - ys) = (x |\| xs \ x |\| ys)" + by (lifting fminus_raw_memb) + +lemma fminus_red: "finsert x xs - ys = (if x |\| ys then xs - ys else finsert x (xs - ys))" + by (lifting fminus_raw_red) + +lemma fminus_red_fin[simp]: "x |\| ys \ finsert x xs - ys = xs - ys" + by (simp add: fminus_red) + +lemma fminus_red_fnotin[simp]: "x |\| ys \ finsert x xs - ys = finsert x (xs - ys)" + by (simp add: fminus_red) + lemma expand_fset_eq: "(S = T) = (\x. (x |\| S) = (x |\| T))" by (lifting list_eq.simps[simplified memb_def[symmetric]]) @@ -1102,8 +1274,107 @@ lemma "fconcat (xs |\| ys) = fconcat xs |\| fconcat ys" by (lifting concat_append) +text {* ffilter *} + +lemma subseteq_filter: "ffilter P xs <= ffilter Q xs = (\ x. x |\| xs \ P x \ Q x)" +by (lifting sub_list_filter) + +lemma eq_ffilter: "(ffilter P xs = ffilter Q xs) = (\x. x |\| xs \ P x = Q x)" +by (lifting list_eq_filter) + +lemma subset_ffilter: "(\x. x |\| xs \ P x \ Q x) \ (x |\| xs & \ P x & Q x) \ 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: "\x. x |\| A \ (\y. P x y) \ \f. \x. x |\| A \ P x (f x)" + unfolding fset_to_set_trans + by (rule finite_set_choice[simplified Ball_def, OF finite_fset]) + +lemma fsubseteq_fnil: "xs |\| {||} = (xs = {||})" + unfolding fset_to_set_trans + by (rule subset_empty) + +lemma not_fsubset_fnil: "\ xs |\| {||}" + unfolding fset_to_set_trans + by (rule not_psubset_empty) + +lemma fcard_mono: "xs |\| ys \ fcard xs \ fcard ys" + unfolding fset_to_set_trans + by (rule card_mono[OF finite_fset]) + +lemma fcard_fseteq: "xs |\| ys \ fcard ys \ fcard xs \ xs = ys" + unfolding fset_to_set_trans + by (rule card_seteq[OF finite_fset]) + +lemma psubset_fcard_mono: "xs |\| ys \ 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 |\| ys) + fcard (xs |\| ys)" + unfolding fset_to_set_trans + by (rule card_Un_Int[OF finite_fset finite_fset]) + +lemma fcard_funion_disjoint: "xs |\| ys = {||} \ fcard (xs |\| 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 |\| xs \ fcard (fdelete xs x) < fcard xs" + unfolding fset_to_set_trans + by (rule card_Diff1_less[OF finite_fset]) + +lemma fcard_delete2_less: "x |\| xs \ y |\| xs \ 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 |\| xs \ fcard ys < fcard xs \ ys |\| xs" + unfolding fset_to_set_trans + by (rule card_psubset[OF finite_fset]) + +lemma fcard_fmap_le: "fcard (fmap f xs) \ fcard xs" + unfolding fset_to_set_trans + by (rule card_image_le[OF finite_fset]) + +lemma fin_fminus_fnotin: "x |\| F - S \ x |\| S" + unfolding fset_to_set_trans + by blast + +lemma fin_fnotin_fminus: "x |\| S \ x |\| F - S" + unfolding fset_to_set_trans + by blast + +lemma fin_mdef: "x |\| F = ((x |\| (F - {|x|})) & (F = finsert x (F - {|x|})))" + unfolding fset_to_set_trans + by blast + +lemma fcard_fminus_finsert[simp]: + assumes "a |\| A" and "a |\| 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 |\| 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 |\| 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], []); *} diff -r c0ab7451b20d -r 751d1349329b Nominal/NewAlpha.thy --- 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 diff -r c0ab7451b20d -r 751d1349329b Nominal/NewParser.thy --- 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; diff -r c0ab7451b20d -r 751d1349329b Nominal/ROOT.ML --- 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" ]; diff -r c0ab7451b20d -r 751d1349329b Nominal/Rsp.thy --- 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 diff -r c0ab7451b20d -r 751d1349329b isar-keywords-quot.el --- 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"