4   "~~/src/HOL/Library/Monad_Syntax"

     9 

    10 ML {* trace := true *}

    16 

    17 lemma alpha_lam_raw_eqvt[eqvt]: "p \<bullet> (alpha_lam_raw x y) = alpha_lam_raw (p \<bullet> x) (p \<bullet> y)"

    18   unfolding alpha_lam_raw_def

    19   by perm_simp rule

    20 

    21 lemma abs_lam_eqvt[eqvt]: "(p \<bullet> abs_lam t) = abs_lam (p \<bullet> t)"

    22 proof -

    23   have "alpha_lam_raw (rep_lam (abs_lam t)) t"

    24     using rep_abs_rsp_left Quotient3_lam equivp_reflp lam_equivp by metis

    25   then have "alpha_lam_raw (p \<bullet> rep_lam (abs_lam t)) (p \<bullet> t)"

    26     unfolding alpha_lam_raw_eqvt[symmetric] permute_pure .

    27   then have "abs_lam (p \<bullet> rep_lam (abs_lam t)) = abs_lam (p \<bullet> t)"

    28     using Quotient3_rel Quotient3_lam by metis

    29   thus ?thesis using permute_lam_def id_apply map_fun_apply by metis

    30 qed

    31 

    52 

   612 lemma transdb_eqvt[eqvt]:

   613   "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)"

   614   apply (nominal_induct t avoiding: l rule: lam.strong_induct)

   615   apply (simp add: vindex_eqvt)

   616   apply (simp_all add: permute_pure)

   617   apply (simp add: fresh_at_list)

   618   apply (subst transdb.simps)

   619   apply (simp add: fresh_at_list[symmetric])

   620   apply (drule_tac x="name # l" in meta_spec)

   621   apply auto

   622   done

   623 

   684 (* a small test

   685 termination (eqvt) sorry

   686 

   687 lemma 

   688   assumes "x \<noteq> y"

   689   shows "eval (App (Lam [x].App (Var x) (Var x)) (Var y)) = App (Var y) (Var y)"

   690 using assms

   691 apply(simp add: lam.supp fresh_def supp_at_base)

   692 done

   693 *)

   694 

   695 

   696 text {* TODO: eqvt_at for the other side *}

   697 nominal_primrec q where

   698   "atom c \<sharp> (x, M) \<Longrightarrow> q (Lam [x]. M) (N :: lam) = Lam [x]. (Lam [c]. (App M (q (Var c) N)))"

   699 | "q (Var x) N = Var x"

   700 | "q (App l r) N = App l r"

   701 apply(simp add: eqvt_def q_graph_aux_def)

   702 apply (rule TrueI)

   703 apply (case_tac x)

   704 apply (rule_tac y="a" in lam.exhaust)

   705 using [[simproc del: alpha_lst]]

   706 apply simp_all

   707 apply blast

   708 apply blast

   709 apply (rule_tac x="(name, lam)" and ?'a="name" in obtain_fresh)

   710 apply blast

   711 apply clarify

   712 apply (rule_tac x="(x, xa, M, Ma, c, ca, Na)" and ?'a="name" in obtain_fresh)

   713 apply (subgoal_tac "eqvt_at q_sumC (Var ca, Na)") --"Could come from nominal_function?"

   714 apply (subgoal_tac "Lam [c]. App M (q_sumC (Var c, Na)) = Lam [a]. App M (q_sumC (Var a, Na))")

   715 apply (subgoal_tac "Lam [ca]. App Ma (q_sumC (Var ca, Na)) = Lam [a]. App Ma (q_sumC (Var a, Na))")

   716 apply (simp only:)

   717 apply (erule Abs_lst1_fcb)

   718 oops

   719 

   720 text {* Working Examples *}

   721 

   743 (*

   744 abbreviation

   745   mbind :: "'a option => ('a => 'b option) => 'b option"  ("_ \<guillemotright>= _" [65,65] 65) 

   746 where  

   747   "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v"

   748 

   749 lemma mbind_eqvt:

   750   fixes c::"'a::pt option"

   751   shows "(p \<bullet> (c \<guillemotright>= f)) = ((p \<bullet> c) \<guillemotright>= (p \<bullet> f))"

   752 apply(cases c)

   753 apply(simp_all)

   754 apply(perm_simp)

   755 apply(rule refl)

   756 done

   757 

   758 lemma mbind_eqvt_raw[eqvt_raw]:

   759   shows "(p \<bullet> option_case) \<equiv> option_case"

   760 apply(rule eq_reflection)

   761 apply(rule ext)+

   762 apply(case_tac xb)

   763 apply(simp_all)

   764 apply(rule_tac p="-p" in permute_boolE)

   765 apply(perm_simp add: permute_minus_cancel)

   766 apply(simp)

   767 apply(rule_tac p="-p" in permute_boolE)

   768 apply(perm_simp add: permute_minus_cancel)

   769 apply(simp)

   770 done

   771 

   772 fun

   773   index :: "atom list \<Rightarrow> nat \<Rightarrow> atom \<Rightarrow> nat option" 

   774 where

   775   "index [] n x = None"

   776 | "index (y # ys) n x = (if x = y then (Some n) else (index ys (n + 1) x))"

   777 

   778 lemma [eqvt]:

   779   shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"

   780 apply(induct xs arbitrary: n)

   781 apply(simp_all add: permute_pure)

   782 done

   783 *)

   784 

   785 (*

   786 nominal_primrec

   787   trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option"

   788 where

   789   "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n::nat. Some (DBVar n)))"

   790 | "trans2 (App t1 t2) xs = 

   791      ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1::db. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2::db. Some (DBApp db1 db2))))"

   792 | "trans2 (Lam [x].t) xs = (trans2 t (atom x # xs) \<guillemotright>= (\<lambda>db::db. Some (DBLam db)))"

   793 oops

   794 *)

   795 

   796 nominal_primrec

   797   CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"

   798 where

   799   "CPS (Var x) k = Var x"

   800 | "CPS (App M N) k = CPS M (\<lambda>m. CPS N (\<lambda>n. n))"

   801 oops

   802 

   803 consts b :: name

   804 nominal_primrec

   805   Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"

   806 where

   807   "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"

   808 | "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))"

   809 apply(simp add: eqvt_def Z_graph_aux_def)

   810 apply (rule, perm_simp, rule)

   811 oops

   812 

   813 lemma test:

   814   assumes "t = s"

   815   and "supp p \<sharp>* t" "supp p \<sharp>* x"

   816   and "(p \<bullet> t) = s \<Longrightarrow> (p \<bullet> x) = y"

   817   shows "x = y"

   818 using assms by (simp add: perm_supp_eq)

   819 

   820 lemma test2:

   821   assumes "cs \<subseteq> as \<union> bs"

   822   and "as \<sharp>* x" "bs \<sharp>* x"

   823   shows "cs \<sharp>* x"

   824 using assms

   825 by (auto simp add: fresh_star_def) 

   826 

   827 lemma test3:

   828   assumes "cs \<subseteq> as"

   829   and "as \<sharp>* x"

   830   shows "cs \<sharp>* x"

   831 using assms

   832 by (auto simp add: fresh_star_def) 

   833 

   834 

   835 

   836 nominal_primrec  (invariant "\<lambda>(_, _, xs) y. atom ` fst ` set xs \<sharp>* y \<and> atom ` snd ` set xs \<sharp>* y")

   837   aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool"

   838 where

   839   "aux (Var x) (Var y) xs = ((x, y) \<in> set xs)"

   840 | "aux (App t1 t2) (App s1 s2) xs = (aux t1 s1 xs \<and> aux t2 s2 xs)"

   841 | "aux (Var x) (App t1 t2) xs = False"

   842 | "aux (Var x) (Lam [y].t) xs = False"

   843 | "aux (App t1 t2) (Var x) xs = False"

   844 | "aux (App t1 t2) (Lam [x].t) xs = False"

   845 | "aux (Lam [x].t) (Var y) xs = False"

   846 | "aux (Lam [x].t) (App t1 t2) xs = False"

   847 | "\<lbrakk>{atom x} \<sharp>* (s, xs); {atom y} \<sharp>* (t, xs); x \<noteq> y\<rbrakk> \<Longrightarrow> 

   848        aux (Lam [x].t) (Lam [y].s) xs = aux t s ((x, y) # xs)"

   849   apply (simp add: eqvt_def aux_graph_aux_def)

   850   apply(erule aux_graph.induct)

   851   apply(simp_all add: fresh_star_def pure_fresh)[9]

   852   apply(case_tac x)

   853   apply(simp)

   854   apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)

   855   apply(simp)

   856   apply(rule_tac y="b" and c="c" in lam.strong_exhaust)

   857   apply(metis)+

   858   apply(simp)

   859   apply(rule_tac y="b" and c="c" in lam.strong_exhaust)

   860   apply(metis)+

   861   apply(simp)

   862   apply(rule_tac y="b" and c="(lam, c, name)" in lam.strong_exhaust)

   863   apply(metis)+

   864   apply(simp)

   865   apply(drule_tac x="name" in meta_spec)

   866   apply(drule_tac x="lama" in meta_spec)

   867   apply(drule_tac x="c" in meta_spec)

   868   apply(drule_tac x="namea" in meta_spec)

   869   apply(drule_tac x="lam" in meta_spec)

   870   apply(simp add: fresh_star_Pair)

   871   apply(simp add: fresh_star_def fresh_at_base )

   872   apply(auto)[1]

   873   apply(simp_all)[44]

   874   apply(simp del: Product_Type.prod.inject)  

   875   oops

   876 

   877 lemma abs_same_binder:

   878   fixes t ta s sa :: "_ :: fs"

   879   and x y::"'a::at"

   880   shows "[[atom x]]lst. t = [[atom y]]lst. ta \<and> [[atom x]]lst. s = [[atom y]]lst. sa

   881      \<longleftrightarrow> [[atom x]]lst. (t, s) = [[atom y]]lst. (ta, sa)"

   882   by (cases "atom x = atom y") (auto simp add: Abs1_eq_iff assms fresh_Pair)

   883 

   884 nominal_primrec

   885   aux2 :: "lam \<Rightarrow> lam \<Rightarrow> bool"

   886 where

   887   "aux2 (Var x) (Var y) = (x = y)"

   888 | "aux2 (App t1 t2) (App s1 s2) = (aux2 t1 s1 \<and> aux2 t2 s2)"

   889 | "aux2 (Var x) (App t1 t2) = False"

   890 | "aux2 (Var x) (Lam [y].t) = False"

   891 | "aux2 (App t1 t2) (Var x) = False"

   892 | "aux2 (App t1 t2) (Lam [x].t) = False"

   893 | "aux2 (Lam [x].t) (Var y) = False"

   894 | "aux2 (Lam [x].t) (App t1 t2) = False"

   895 | "x = y \<Longrightarrow> aux2 (Lam [x].t) (Lam [y].s) = aux2 t s"

   896   apply(simp add: eqvt_def aux2_graph_aux_def)

   897   apply(rule TrueI)

   898   apply(case_tac x)

   899   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)

   900   apply(rule_tac y="b" in lam.exhaust)

   901   apply(auto)[3]

   902   apply(rule_tac y="b" in lam.exhaust)

   903   apply(auto)[3]

   904   apply(rule_tac y="b" and c="(name, lam)" in lam.strong_exhaust)

   905   using [[simproc del: alpha_lst]]

   906   apply(auto)[3]

   907   apply(drule_tac x="name" in meta_spec)

   908   apply(drule_tac x="name" in meta_spec)

   909   apply(drule_tac x="lam" in meta_spec)

   910   apply(drule_tac x="(name \<leftrightarrow> namea) \<bullet> lama" in meta_spec)

   911   using [[simproc del: alpha_lst]]

   912   apply(simp add: Abs1_eq_iff fresh_star_def fresh_Pair_elim fresh_at_base flip_def)

   913   apply (metis Nominal2_Base.swap_commute fresh_permute_iff sort_of_atom_eq swap_atom_simps(2))

   914   using [[simproc del: alpha_lst]]

   915   apply simp_all

   916   apply (simp add: abs_same_binder)

   917   apply (erule_tac c="()" in Abs_lst1_fcb2)

   918   apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)

   919   done

   920 

   921 text {* tests of functions containing if and case *}

   922 

   923 consts P :: "lam \<Rightarrow> bool"

   924 

   925 (*

   926 nominal_primrec  

   927   A :: "lam => lam"

   928 where  

   929   "A (App M N) = (if (True \<or> P M) then (A M) else (A N))"

   930 | "A (Var x) = (Var x)" 

   931 | "A (App M N) = (if True then M else A N)"

   932 oops

   933 

   934 nominal_primrec  

   935   C :: "lam => lam"

   936 where  

   937   "C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))"

   938 | "C (Var x) = (Var x)" 

   939 | "C (App M N) = (if True then M else C N)"

   940 oops

   941 

   942 nominal_primrec  

   943   A :: "lam => lam"

   944 where  

   945   "A (Lam [x].M) = (Lam [x].M)"

   946 | "A (Var x) = (Var x)"

   947 | "A (App M N) = (if True then M else A N)"

   948 oops

   949 

   950 nominal_primrec  

   951   B :: "lam => lam"

   952 where  

   953   "B (Lam [x].M) = (Lam [x].M)"

   954 | "B (Var x) = (Var x)"

   955 | "B (App M N) = (if True then M else (B N))"

   956 unfolding eqvt_def

   957 unfolding B_graph_def

   958 apply(perm_simp)

   959 apply(rule allI)

   960 apply(rule refl)

   961 oops

   962 *)