15 ML {* Method.SIMPLE_METHOD' *}

    16 ML {* Sign.intern_const *}

    17 

    18 ML {*

    19 val test:((Proof.context -> Method.method) context_parser) =

    20 Scan.succeed (fn ctxt =>

    21  let

    22    val _ = Inductive.the_inductive ctxt "local.frees_lst_graph"

    23  in 

    24    Method.SIMPLE_METHOD' (K (all_tac))

    25  end)

    26 *}

    27 

    28 method_setup test = {* test *} {* test *}

   611 (* function that evaluates a lambda term *)

   612 nominal_primrec

   613    eval :: "lam \<Rightarrow> lam" and

   614    apply_subst :: "lam \<Rightarrow> lam \<Rightarrow> lam"

   615 where

   616   "eval (Var x) = Var x"

   617 | "eval (Lam [x].t) = Lam [x].(eval t)"

   618 | "eval (App t1 t2) = apply_subst (eval t1) (eval t2)"

   619 | "apply_subst (Var x) t2 = App (Var x) t2"

   620 | "apply_subst (App t0 t1) t2 = App (App t0 t1) t2"

   621 | "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])"

   622   apply(simp add: eval_apply_subst_graph_def eqvt_def)

   623   apply(rule, perm_simp, rule)

   624   apply(rule TrueI)

   625   apply (case_tac x)

   626   apply (case_tac a rule: lam.exhaust)

   627   apply simp_all[3]

   628   apply blast

   629   apply (case_tac b)

   630   apply (rule_tac y="a" and c="ba" in lam.strong_exhaust)

   631   apply simp_all[3]

   632   apply blast

   633   apply blast

   634   apply (simp add: Abs1_eq_iff fresh_star_def)

   635   apply(simp_all)

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

   637   apply (simp add: Abs_fresh_iff)

   638   apply(simp add: fresh_star_def fresh_Unit)

   639   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

   640   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)

   641   apply(erule conjE)

   642   apply(erule_tac c="t2a" in Abs_lst1_fcb2')

   643   apply (erule fresh_eqvt_at)

   644   apply (simp add: finite_supp)

   645   apply (simp add: fresh_Inl var_fresh_subst)

   646   apply(simp add: fresh_star_def)

   647   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt)

   648   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst.eqvt)

   649 done

   650 

   651 

   652 (* a small test

   653 termination (eqvt) sorry

   654 

   655 lemma 

   656   assumes "x \<noteq> y"

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

   658 using assms

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

   660 done

   661 *)

   662 

   663 

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

   665 nominal_primrec q where

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

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

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

   669 unfolding eqvt_def q_graph_def

   670 apply (rule, perm_simp, rule)

   671 apply (rule TrueI)

   672 apply (case_tac x)

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

   674 apply simp_all

   675 apply blast

   676 apply blast

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

   678 apply blast

   679 apply clarify

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

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

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

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

   684 apply (simp only:)

   685 apply (erule Abs_lst1_fcb)

   686 oops

   687 

   688 text {* Working Examples *}

   689 

   690 nominal_primrec

   691   map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam"

   692 where

   693   "eqvt f \<Longrightarrow> map_term f (Var x) = f (Var x)"

   694 | "eqvt f \<Longrightarrow> map_term f (App t1 t2) = App (f t1) (f t2)"

   695 | "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)"

   696 | "\<not>eqvt f \<Longrightarrow> map_term f t = t"

   697   apply (simp add: eqvt_def map_term_graph_def)

   698   apply (rule, perm_simp, rule)

   699   apply(rule TrueI)

   700   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)

   701   apply auto

   702   apply (erule Abs_lst1_fcb)

   703   apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)

   704   apply (simp add: eqvt_def permute_fun_app_eq)

   705   done

   706 

   707 termination (eqvt)

   708   by lexicographic_order

   709 

   710 

   711 (*

   712 abbreviation

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

   714 where  

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

   716 

   717 lemma mbind_eqvt:

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

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

   720 apply(cases c)

   721 apply(simp_all)

   722 apply(perm_simp)

   723 apply(rule refl)

   724 done

   725 

   726 lemma mbind_eqvt_raw[eqvt_raw]:

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

   728 apply(rule eq_reflection)

   729 apply(rule ext)+

   730 apply(case_tac xb)

   731 apply(simp_all)

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

   733 apply(perm_simp add: permute_minus_cancel)

   734 apply(simp)

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

   736 apply(perm_simp add: permute_minus_cancel)

   737 apply(simp)

   738 done

   739 

   740 fun

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

   742 where

   743   "index [] n x = None"

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

   745 

   746 lemma [eqvt]:

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

   748 apply(induct xs arbitrary: n)

   749 apply(simp_all add: permute_pure)

   750 done

   751 *)

   752 

   753 (*

   754 nominal_primrec

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

   756 where

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

   758 | "trans2 (App t1 t2) xs = 

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

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

   761 oops

   762 *)

   763 

   764 nominal_primrec

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

   766 where

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

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

   769 oops

   770 

   771 consts b :: name

   772 nominal_primrec

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

   774 where

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

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

   777 unfolding eqvt_def Z_graph_def

   778 apply (rule, perm_simp, rule)

   779 oops

   780 

   781 lemma test:

   782   assumes "t = s"

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

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

   785   shows "x = y"

   786 using assms by (simp add: perm_supp_eq)

   787 

   788 lemma test2:

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

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

   791   shows "cs \<sharp>* x"

   792 using assms

   793 by (auto simp add: fresh_star_def) 

   794 

   795 lemma test3:

   796   assumes "cs \<subseteq> as"

   797   and "as \<sharp>* x"

   798   shows "cs \<sharp>* x"

   799 using assms

   800 by (auto simp add: fresh_star_def) 

   801 

   802 

   803 

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

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

   806 where

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

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

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

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

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

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

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

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

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

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

   817   apply (simp add: eqvt_def aux_graph_def)

   818   apply (rule, perm_simp, rule)

   819   apply(erule aux_graph.induct)

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

   821   apply(case_tac x)

   822   apply(simp)

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

   824   apply(simp)

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

   826   apply(metis)+

   827   apply(simp)

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

   829   apply(metis)+

   830   apply(simp)

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

   832   apply(metis)+

   833   apply(simp)

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

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

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

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

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

   839   apply(simp add: fresh_star_Pair)

   840   apply(simp add: fresh_star_def fresh_at_base lam.fresh)

   841   apply(auto)[1]

   842   apply(simp_all)[44]

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

   844   oops

   845 

   846 lemma abs_same_binder:

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

   848   assumes "sort_of (atom x) = sort_of (atom y)"

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

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

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

   852 

   853 nominal_primrec

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

   855 where

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

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

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

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

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

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

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

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

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

   865   apply(simp add: eqvt_def aux2_graph_def)

   866   apply(rule, perm_simp, rule, rule)

   867   apply(case_tac x)

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

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

   870   apply(auto)[3]

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

   872   apply(auto)[3]

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

   874   apply(auto)[3]

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

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

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

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

   879   apply(simp add: Abs1_eq_iff fresh_star_def fresh_Pair_elim fresh_at_base lam.fresh flip_def)

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

   881   apply simp_all

   882   apply (simp add: abs_same_binder)

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

   884   apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)

   885   done

   886 

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

   888 

   889 (*consts P :: "lam \<Rightarrow> bool"

   890 

   891 nominal_primrec  

   892   A :: "lam => lam"

   893 where  

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

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

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

   897 oops

   898 

   899 nominal_primrec  

   900   C :: "lam => lam"

   901 where  

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

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

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

   905 oops

   906 

   907 nominal_primrec  

   908   A :: "lam => lam"

   909 where  

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

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

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

   913 oops

   914 

   915 nominal_primrec  

   916   B :: "lam => lam"

   917 where  

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

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

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

   921 unfolding eqvt_def

   922 unfolding B_graph_def

   923 apply(perm_simp)

   924 apply(rule allI)

   925 apply(rule refl)

   926 oops*)

   927