Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/ExCoreHaskell.thy
changeset 1646 733bac87d5bf
parent 1645 bde8da26093e
child 1647 032649a694d2
equal deleted inserted replaced
1645:bde8da26093e 1646:733bac87d5bf 
    93 
    93 
    94 lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)"
 
    94 lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)"
 
    95   unfolding fresh_star_def Ball_def
 
    95   unfolding fresh_star_def Ball_def
 
    96   by auto (simp_all add: fresh_minus_perm)
 
    96   by auto (simp_all add: fresh_minus_perm)
 
    97 
    97 
       
    98 (*primrec
 
       
    99   permute_bv_raw
 
       
   100 where
 
       
   101   "permute_bv_raw p (K c l1 l2 l3) = K c (permute_.. l1) ...
 
       
   102 
       
   103 (permute_bv p (K (q \<bullet> char) (q \<bullet> tvtk_lst) (q \<bullet> tvck_lst) (q \<bullet> vt_lst)
 
       
   104 *)
 
       
   105 
       
   106 consts
 
       
   107   permute_bv :: "perm \<Rightarrow> pat \<Rightarrow> pat"
 
       
   108 
       
   109 lemma ACons_subst:
 
       
   110   "supp (Abs (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al"
 
       
   111 sorry
 
       
   112 
       
   113 lemma perm_bv:
 
       
   114   "p \<bullet> bv l = bv (permute_bv p l)"
 
       
   115   sorry
 
       
   116 
       
   117 
       
   118 
    98 lemma fv_alpha1: "fv_bv_tvtk x \<sharp>* pa \<Longrightarrow> alpha_bv_tvtk (pa \<bullet> x) x"
 
   119 lemma fv_alpha1: "fv_bv_tvtk x \<sharp>* pa \<Longrightarrow> alpha_bv_tvtk (pa \<bullet> x) x"
 
    99 apply (induct x rule: inducts(11))
 
   120 apply (induct x rule: inducts(11))
 
   100 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   121 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 
   101 apply (simp_all add: eq_iff fresh_star_union)
 
   122 apply (simp_all add: eq_iff fresh_star_union)
 
   102 apply (subst supp_perm_eq)
 
   123 apply (subst supp_perm_eq)
 
   247          P9 (i :: 'i :: pt) pat \<and>
 
   268          P9 (i :: 'i :: pt) pat \<and>
 
   248          P10 (j :: 'j :: pt) vt_lst \<and>
 
   269          P10 (j :: 'j :: pt) vt_lst \<and>
 
   249          P11 (k :: 'k :: pt) tvtk_lst \<and>
 
   270          P11 (k :: 'k :: pt) tvtk_lst \<and>
 
   250          P12 (l :: 'l :: pt) tvck_lst"
 
   271          P12 (l :: 'l :: pt) tvck_lst"
 
   251 proof -
 
   272 proof -
 
   252   have a: "(\<forall>p a. P1 a (p \<bullet> tkind)) \<and> (\<forall>p b. P2 b (p \<bullet> ckind)) \<and> (\<forall>p c. P3 c (p \<bullet> ty)) \<and> (\<forall>p d. P4 d (p \<bullet> ty_lst)) \<and> (\<forall>p e. P5 e (p \<bullet> co)) \<and> (\<forall>p f. P6 f (p \<bullet> co_lst)) \<and> (\<forall>p g. P7 g (p \<bullet> trm)) \<and> (\<forall>p h. P8 h (p \<bullet> assoc_lst)) \<and> (\<forall>p i. P9 i (p \<bullet> pat)) \<and> (\<forall>p j. P10 j (p \<bullet> vt_lst)) \<and> (\<forall>p k. P11 k (p \<bullet> tvtk_lst)) \<and> (\<forall>p l. P12 l (p \<bullet> tvck_lst))"
 
   273   have a: "(\<forall>p a. P1 a (p \<bullet> tkind)) \<and> (\<forall>p b. P2 b (p \<bullet> ckind)) \<and> (\<forall>p c. P3 c (p \<bullet> ty)) \<and> (\<forall>p d. P4 d (p \<bullet> ty_lst)) \<and> (\<forall>p e. P5 e (p \<bullet> co)) \<and> (\<forall>p f. P6 f (p \<bullet> co_lst)) \<and> (\<forall>p g. P7 g (p \<bullet> trm)) \<and> (\<forall>p h. P8 h (p \<bullet> assoc_lst)) \<and> (\<forall>p q i. P9 i (permute_bv p (q \<bullet> pat))) \<and> (\<forall>p j. P10 j (p \<bullet> vt_lst)) \<and> (\<forall>p k. P11 k (p \<bullet> tvtk_lst)) \<and> (\<forall>p l. P12 l (p \<bullet> tvck_lst))"
 
   253     apply (rule tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.induct)
 
   274     apply (rule tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.induct)
 
   254     apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})
 
   275     apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})
 
   255     apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})
 
   276     apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})
 
   256 
   277 
   257 (* GOAL1 *)
 
   278 (* GOAL1 *)
 
   373     apply (simp add: finite_supp)
 
   394     apply (simp add: finite_supp)
 
   374     apply (simp add: fresh_def)
 
   395     apply (simp add: fresh_def)
 
   375     apply (simp only: supp_Abs eqvts)
 
   396     apply (simp only: supp_Abs eqvts)
 
   376     apply blast
 
   397     apply blast
 
   377 
   398 
   378 prefer 5
 
   399 (* GOAL4 a copy-and-paste *)
 
   379 (*  using a38*)
 
   400     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and>
 
   380     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (bv (p \<bullet> pat))) \<sharp>* h \<and>
 
   401                        supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)")
 
   381                        supp (Abs (p \<bullet> (bv pat)) (p \<bullet> trm), fv_bv (p \<bullet> pat)) \<sharp>* pa)")
 
       
   382     apply clarify
 
   402     apply clarify
 
   383     apply (simp only: perm)
 
   403     apply (simp only: perm)
 
   384     apply(rule_tac t="ACons (p \<bullet> pat) (p \<bullet> trm) (p \<bullet> assoc_lst)"
 
   404     apply(rule_tac t="LAMC (p \<bullet> tvar) (p \<bullet> ckind) (p \<bullet> trm)"
 
   385                and s="ACons (pa \<bullet> p \<bullet> pat) (pa \<bullet> p \<bullet> trm) (p \<bullet> assoc_lst)" in subst)
 
   405                and s="LAMC (pa \<bullet> p \<bullet> tvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst)
 
   386     apply (simp only: eq_iff supp_Pair fresh_star_union)
 
   406     apply (simp only: eq_iff)
 
   387     apply (erule conjE)
 
       
   388     apply (rule_tac x="-pa" in exI)
 
   407     apply (rule_tac x="-pa" in exI)
 
   389     apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp)
 
   408     apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp)
 
   390     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - bv (pa \<bullet> p \<bullet> pat)"
 
   409     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
 
   391                 and s="pa \<bullet> (supp (p \<bullet> trm) - bv (p \<bullet> pat))" in subst)
 
   410                 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst)
 
   392     apply (simp add: eqvts)
 
   411     apply (simp add: eqvts)
 
       
   412     apply (simp add: eqvts[symmetric])
 
   393     apply (rule conjI)
 
   413     apply (rule conjI)
 
   394     apply (rule fv_alpha)
 
   414     apply (rule supp_perm_eq)
 
   395     apply (rule_tac s="supp (fv_bv (p \<bullet> pat))"
 
   415     apply (simp add: eqvts)
 
   396                 and t="fv_bv (p \<bullet> pat)" in subst)
 
   416     apply (subst supp_finite_atom_set)
 
   397     apply (rule supp_finite_atom_set[OF fin_fv_bv])
 
   417     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
 
   398     apply (assumption)
 
   418     apply (simp add: eqvts)
 
       
   419     apply (simp add: eqvts)
 
       
   420     apply (subst supp_perm_eq)
 
       
   421     apply (subst supp_finite_atom_set)
 
       
   422     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
 
       
   423     apply (simp add: eqvts)
 
       
   424     apply assumption
 
       
   425     apply (simp add: fresh_star_minus_perm)
 
       
   426     apply (rule a30)
 
       
   427     apply simp
 
       
   428     apply(rotate_tac 1)
 
       
   429     apply(erule_tac x="(pa + p)" in allE)
 
       
   430     apply simp
 
       
   431     apply (simp add: eqvts eqvts_raw)
 
       
   432     apply (rule at_set_avoiding2_atom)
 
       
   433     apply (simp add: finite_supp)
 
       
   434     apply (simp add: finite_supp)
 
       
   435     apply (simp add: fresh_def)
 
       
   436     apply (simp only: supp_Abs eqvts)
 
       
   437     apply blast
 
       
   438 
       
   439 
       
   440 (* GOAL5 a copy-and-paste *)
 
       
   441     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
 
       
   442                        supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm)) \<sharp>* pa)")
 
       
   443     apply clarify
 
       
   444     apply (simp only: perm)
 
       
   445     apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)"
 
       
   446                and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst)
 
       
   447     apply (simp only: eq_iff)
 
       
   448     apply (rule_tac x="-pa" in exI)
 
       
   449     apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp)
 
       
   450     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}"
 
       
   451                 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst)
 
       
   452     apply (simp add: eqvts)
 
       
   453     apply (simp add: eqvts[symmetric])
 
   399     apply (rule conjI)
 
   454     apply (rule conjI)
 
       
   455     apply (rule supp_perm_eq)
 
       
   456     apply (simp add: eqvts)
 
       
   457     apply (subst supp_finite_atom_set)
 
       
   458     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
 
       
   459     apply (simp add: eqvts)
 
       
   460     apply (simp add: eqvts)
 
       
   461     apply (subst supp_perm_eq)
 
       
   462     apply (subst supp_finite_atom_set)
 
       
   463     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
 
       
   464     apply (simp add: eqvts)
 
       
   465     apply assumption
 
       
   466     apply (simp add: fresh_star_minus_perm)
 
       
   467     apply (rule a32)
 
       
   468     apply simp
 
       
   469     apply(rotate_tac 1)
 
       
   470     apply(erule_tac x="(pa + p)" in allE)
 
       
   471     apply simp
 
       
   472     apply (simp add: eqvts eqvts_raw)
 
       
   473     apply (rule at_set_avoiding2_atom)
 
       
   474     apply (simp add: finite_supp)
 
       
   475     apply (simp add: finite_supp)
 
       
   476     apply (simp add: fresh_def)
 
       
   477     apply (simp only: supp_Abs eqvts)
 
       
   478     apply blast
 
       
   479 
       
   480 
       
   481 (* GOAL6 a copy-and-paste *)
 
       
   482     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> var))) \<sharp> g \<and>
 
       
   483                        supp (Abs (p \<bullet> {atom var}) (p \<bullet> trm2)) \<sharp>* pa)")
 
       
   484     apply clarify
 
       
   485     apply (simp only: perm)
 
       
   486     apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)"
 
       
   487                and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst)
 
       
   488     apply (simp only: eq_iff)
 
       
   489     apply (rule_tac x="-pa" in exI)
 
       
   490     apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp)
 
       
   491     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}"
 
       
   492                 and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst)
 
       
   493     apply (simp add: eqvts)
 
   400     apply (simp add: eqvts[symmetric])
 
   494     apply (simp add: eqvts[symmetric])
 
       
   495     apply (rule conjI)
 
   401     apply (rule supp_perm_eq)
 
   496     apply (rule supp_perm_eq)
 
   402     apply (simp add: eqvts)
 
   497     apply (simp add: eqvts)
 
   403     apply (subst supp_finite_atom_set)
 
   498     apply (subst supp_finite_atom_set)
 
   404     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
 
   499     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
 
   405     apply (simp add: eqvts)
 
   500     apply (simp add: eqvts)
 
   408     apply (subst supp_finite_atom_set)
 
   503     apply (subst supp_finite_atom_set)
 
   409     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
 
   504     apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
 
   410     apply (simp add: eqvts)
 
   505     apply (simp add: eqvts)
 
   411     apply assumption
 
   506     apply assumption
 
   412     apply (simp add: fresh_star_minus_perm)
 
   507     apply (simp add: fresh_star_minus_perm)
 
       
   508     apply (rule a34)
 
       
   509     apply simp
 
       
   510     apply simp
 
       
   511     apply(rotate_tac 2)
 
       
   512     apply(erule_tac x="(pa + p)" in allE)
 
       
   513     apply simp
 
       
   514     apply (simp add: eqvts eqvts_raw)
 
       
   515     apply (rule at_set_avoiding2_atom)
 
       
   516     apply (simp add: finite_supp)
 
       
   517     apply (simp add: finite_supp)
 
       
   518     apply (simp add: fresh_def)
 
       
   519     apply (simp only: supp_Abs eqvts)
 
       
   520     apply blast
 
       
   521 
       
   522 (* MAIN ACons Goal *)
 
       
   523     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (bv (p \<bullet> pat))) \<sharp>* h \<and>
 
       
   524                        supp (Abs (p \<bullet> (bv pat)) (p \<bullet> trm)) \<sharp>* pa)")
 
       
   525     apply clarify
 
       
   526     apply (simp only: perm eqvts)
 
       
   527     apply (subst ACons_subst)
 
       
   528     apply assumption
 
   413     apply (rule a38)
 
   529     apply (rule a38)
 
   414     apply(erule_tac x="(pa + p)" in allE)
 
       
   415     apply simp
 
   530     apply simp
 
   416     apply(rotate_tac 1)
 
   531     apply(rotate_tac 1)
 
   417     apply(erule_tac x="(pa + p)" in allE)
 
   532     apply(erule_tac x="(pa + p)" in allE)
 
   418     apply simp
 
   533     apply simp
 
   419     apply simp
 
   534     apply simp
 
       
   535     apply (simp add: perm_bv[symmetric])
 
   420     apply (simp add: eqvts eqvts_raw)
 
   536     apply (simp add: eqvts eqvts_raw)
 
   421     apply (rule at_set_avoiding2)
 
   537     apply (rule at_set_avoiding2)
 
   422     apply (simp add: fin_bv)
 
   538     apply (simp add: fin_bv)
 
   423     apply (simp add: finite_supp)
 
   539     apply (simp add: finite_supp)
 
   424     apply (simp add: supp_Pair supp_Abs supp_finite_atom_set[OF fin_fv_bv] fin_fv_bv)
 
   540     apply (simp add: supp_Abs)
 
   425     apply (rule finite_Diff)
 
   541     apply (rule finite_Diff)
 
   426     apply (simp add:  eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
 
   542     apply (simp add: finite_supp)
 
   427     apply (simp add: True_eqvt)
 
   543     apply (simp add: fresh_star_def fresh_def supp_Abs eqvts)
 
   428     apply (simp add: fresh_star_prod eqvts[symmetric])
 
   544 (* Goal for K *)
 
   429     apply (rule conjI)
 
   545     apply (simp)
 
   430     apply (simp add: fresh_star_def fresh_def supp_Abs)
 
       
   431     apply (simp add: fresh_star_permute_iff)
 
       
   432     sorry
 
   546     sorry
 
   433   have g1: "P1 a (0 \<bullet> tkind)" using a[THEN conjunct1] by blast
 
   547   have g1: "P1 a (0 \<bullet> tkind)" using a[THEN conjunct1] by blast
 
   434   have g2: "P2 b (0 \<bullet> ckind)" using a[THEN conjunct2,THEN conjunct1] by blast
 
   548   have g2: "P2 b (0 \<bullet> ckind)" using a[THEN conjunct2,THEN conjunct1] by blast
 
   435   have g3: "P3 c (0 \<bullet> ty) \<and>
 
   549   have g3: "P3 c (0 \<bullet> ty) \<and>
 
   436         P4 d (0 \<bullet> ty_lst) \<and> P5 e (0 \<bullet> co) \<and> P6 f (0 \<bullet> co_lst) \<and>
 
   550         P4 d (0 \<bullet> ty_lst) \<and> P5 e (0 \<bullet> co) \<and> P6 f (0 \<bullet> co_lst) \<and>
nominal2