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/Ex/Lambda.thy
changeset 3197 25d11b449e92
parent 3192 14c7d7e29c44
child 3208 da575186d492
child 3219 e5d9b6bca88c
equal deleted inserted replaced
3196:ca6ca6fc28af 3197:25d11b449e92 
     4   "~~/src/HOL/Library/Monad_Syntax"
 
     4   "~~/src/HOL/Library/Monad_Syntax"
 
     5 begin
 
     5 begin
 
     6 
     6 
     7 
     7 
     8 atom_decl name
 
     8 atom_decl name
 
     9 
       
    10 
     9 
    11 ML {* trace := true *}
 
    10 ML {* trace := true *}
 
    12 
    11 
    13 nominal_datatype lam =
 
    12 nominal_datatype lam =
 
    14   Var "name"
 
    13   Var "name"
 
    37   is_app :: "lam \<Rightarrow> bool"
 
    36   is_app :: "lam \<Rightarrow> bool"
 
    38 where
 
    37 where
 
    39   "is_app (Var x) = False"
 
    38   "is_app (Var x) = False"
 
    40 | "is_app (App t1 t2) = True"
 
    39 | "is_app (App t1 t2) = True"
 
    41 | "is_app (Lam [x]. t) = False"
 
    40 | "is_app (Lam [x]. t) = False"
 
    42 apply(simp add: eqvt_def is_app_graph_def)
 
    41 apply(simp add: eqvt_def is_app_graph_aux_def)
 
    43 apply(rule TrueI)
 
    42 apply(rule TrueI)
 
    44 apply(rule_tac y="x" in lam.exhaust)
 
    43 apply(rule_tac y="x" in lam.exhaust)
 
    45 apply(auto)[3]
 
    44 apply(auto)[3]
 
    46 apply(all_trivials)
 
    45 apply(all_trivials)
 
    47 done
 
    46 done
 
    57   rator :: "lam \<Rightarrow> lam option"
 
    56   rator :: "lam \<Rightarrow> lam option"
 
    58 where
 
    57 where
 
    59   "rator (Var x) = None"
 
    58   "rator (Var x) = None"
 
    60 | "rator (App t1 t2) = Some t1"
 
    59 | "rator (App t1 t2) = Some t1"
 
    61 | "rator (Lam [x]. t) = None"
 
    60 | "rator (Lam [x]. t) = None"
 
    62 apply(simp add: eqvt_def rator_graph_def)
 
    61 apply(simp add: eqvt_def rator_graph_aux_def)
 
    63 apply(rule TrueI)
 
    62 apply(rule TrueI)
 
    64 apply(rule_tac y="x" in lam.exhaust)
 
    63 apply(rule_tac y="x" in lam.exhaust)
 
    65 apply(auto)[3]
 
    64 apply(auto)[3]
 
    66 apply(simp_all)
 
    65 apply(simp_all)
 
    67 done
 
    66 done
 
    72   rand :: "lam \<Rightarrow> lam option"
 
    71   rand :: "lam \<Rightarrow> lam option"
 
    73 where
 
    72 where
 
    74   "rand (Var x) = None"
 
    73   "rand (Var x) = None"
 
    75 | "rand (App t1 t2) = Some t2"
 
    74 | "rand (App t1 t2) = Some t2"
 
    76 | "rand (Lam [x]. t) = None"
 
    75 | "rand (Lam [x]. t) = None"
 
    77 apply(simp add: eqvt_def rand_graph_def)
 
    76 apply(simp add: eqvt_def rand_graph_aux_def)
 
    78 apply(rule TrueI)
 
    77 apply(rule TrueI)
 
    79 apply(rule_tac y="x" in lam.exhaust)
 
    78 apply(rule_tac y="x" in lam.exhaust)
 
    80 apply(auto)[3]
 
    79 apply(auto)[3]
 
    81 apply(simp_all)
 
    80 apply(simp_all)
 
    82 done
 
    81 done
 
    88 where
 
    87 where
 
    89   "is_eta_nf (Var x) = True"
 
    88   "is_eta_nf (Var x) = True"
 
    90 | "is_eta_nf (App t1 t2) = (is_eta_nf t1 \<and> is_eta_nf t2)"
 
    89 | "is_eta_nf (App t1 t2) = (is_eta_nf t1 \<and> is_eta_nf t2)"
 
    91 | "is_eta_nf (Lam [x]. t) = (is_eta_nf t \<and> 
    90 | "is_eta_nf (Lam [x]. t) = (is_eta_nf t \<and> 
    92                              ((is_app t \<and> rand t = Some (Var x)) \<longrightarrow> atom x \<in> supp (rator t)))"
 
    91                              ((is_app t \<and> rand t = Some (Var x)) \<longrightarrow> atom x \<in> supp (rator t)))"
 
    93 apply(simp add: eqvt_def is_eta_nf_graph_def)
 
    92 apply(simp add: eqvt_def is_eta_nf_graph_aux_def)
 
    94 apply(rule TrueI)
 
    93 apply(rule TrueI)
 
    95 apply(rule_tac y="x" in lam.exhaust)
 
    94 apply(rule_tac y="x" in lam.exhaust)
 
    96 apply(auto)[3]
 
    95 apply(auto)[3]
 
    97 using [[simproc del: alpha_lst]]
 
    96 using [[simproc del: alpha_lst]]
 
    98 apply(simp_all)
 
    97 apply(simp_all)
 
   118   var_pos :: "name \<Rightarrow> lam \<Rightarrow> (path list) set"
 
   117   var_pos :: "name \<Rightarrow> lam \<Rightarrow> (path list) set"
 
   119 where
 
   118 where
 
   120   "var_pos y (Var x) = (if y = x then {[]} else {})"
 
   119   "var_pos y (Var x) = (if y = x then {[]} else {})"
 
   121 | "var_pos y (App t1 t2) = (Cons Left ` (var_pos y t1)) \<union> (Cons Right ` (var_pos y t2))"
 
   120 | "var_pos y (App t1 t2) = (Cons Left ` (var_pos y t1)) \<union> (Cons Right ` (var_pos y t2))"
 
   122 | "atom x \<sharp> y \<Longrightarrow> var_pos y (Lam [x]. t) = (Cons In ` (var_pos y t))"
 
   121 | "atom x \<sharp> y \<Longrightarrow> var_pos y (Lam [x]. t) = (Cons In ` (var_pos y t))"
 
   123 apply(simp add: eqvt_def var_pos_graph_def)
 
   122 apply(simp add: eqvt_def var_pos_graph_aux_def)
 
   124 apply(rule TrueI)
 
   123 apply(rule TrueI)
 
   125 apply(case_tac x)
 
   124 apply(case_tac x)
 
   126 apply(rule_tac y="b" and c="a" in lam.strong_exhaust)
 
   125 apply(rule_tac y="b" and c="a" in lam.strong_exhaust)
 
   127 apply(auto simp add: fresh_star_def)[3]
 
   126 apply(auto simp add: fresh_star_def)[3]
 
   128 using [[simproc del: alpha_lst]]
 
   127 using [[simproc del: alpha_lst]]
 
   164   subst' :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::== _]" [90, 90, 90] 90)
 
   163   subst' :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::== _]" [90, 90, 90] 90)
 
   165 where
 
   164 where
 
   166   "(Var x)[y ::== s] = (if x = y then s else (Var x))"
 
   165   "(Var x)[y ::== s] = (if x = y then s else (Var x))"
 
   167 | "(App t1 t2)[y ::== s] = App (t1[y ::== s]) (t2[y ::== s])"
 
   166 | "(App t1 t2)[y ::== s] = App (t1[y ::== s]) (t2[y ::== s])"
 
   168 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::== s] = Lam [x].(t[y ::== (App (Var y) s)])"
 
   167 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::== s] = Lam [x].(t[y ::== (App (Var y) s)])"
 
   169   apply(simp add: eqvt_def subst'_graph_def)
 
   168   apply(simp add: eqvt_def subst'_graph_aux_def)
 
   170   apply(rule TrueI)
 
   169   apply(rule TrueI)
 
   171   apply(case_tac x)
 
   170   apply(case_tac x)
 
   172   apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
 
   171   apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
 
   173   apply(auto simp add: fresh_star_def)[3]
 
   172   apply(auto simp add: fresh_star_def)[3]
 
   174   using [[simproc del: alpha_lst]]
 
   173   using [[simproc del: alpha_lst]]
 
   198   frees_lst :: "lam \<Rightarrow> atom list"
 
   197   frees_lst :: "lam \<Rightarrow> atom list"
 
   199 where
 
   198 where
 
   200   "frees_lst (Var x) = [atom x]"
 
   199   "frees_lst (Var x) = [atom x]"
 
   201 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2"
 
   200 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2"
 
   202 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
 
   201 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)"
 
   203   unfolding eqvt_def
 
   202 apply(simp add: eqvt_def frees_lst_graph_aux_def)
 
   204   unfolding frees_lst_graph_def
 
       
   205 apply(simp)
 
       
   206 apply(rule TrueI)
 
   203 apply(rule TrueI)
 
   207 apply(rule_tac y="x" in lam.exhaust)
 
   204 apply(rule_tac y="x" in lam.exhaust)
 
   208 using [[simproc del: alpha_lst]]
 
   205 using [[simproc del: alpha_lst]]
 
   209 apply(auto)
 
   206 apply(auto)
 
   210 apply (erule_tac c="()" in Abs_lst1_fcb2)
 
   207 apply (erule_tac c="()" in Abs_lst1_fcb2)
 
   226   frees_set :: "lam \<Rightarrow> atom set"
 
   223   frees_set :: "lam \<Rightarrow> atom set"
 
   227 where
 
   224 where
 
   228   "frees_set (Var x) = {atom x}"
 
   225   "frees_set (Var x) = {atom x}"
 
   229 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2"
 
   226 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2"
 
   230 | "frees_set (Lam [x]. t) = (frees_set t) - {atom x}"
 
   227 | "frees_set (Lam [x]. t) = (frees_set t) - {atom x}"
 
   231   apply(simp add: eqvt_def frees_set_graph_def)
 
   228   apply(simp add: eqvt_def frees_set_graph_aux_def)
 
   232   apply(erule frees_set_graph.induct)
 
   229   apply(erule frees_set_graph.induct)
 
   233   apply(auto)[9]
 
   230   apply(auto)[9]
 
   234   apply(rule_tac y="x" in lam.exhaust)
 
   231   apply(rule_tac y="x" in lam.exhaust)
 
   235   apply(auto)[3]
 
   232   apply(auto)[3]
 
   236   using [[simproc del: alpha_lst]]
 
   233   using [[simproc del: alpha_lst]]
 
   254   height :: "lam \<Rightarrow> int"
 
   251   height :: "lam \<Rightarrow> int"
 
   255 where
 
   252 where
 
   256   "height (Var x) = 1"
 
   253   "height (Var x) = 1"
 
   257 | "height (App t1 t2) = max (height t1) (height t2) + 1"
 
   254 | "height (App t1 t2) = max (height t1) (height t2) + 1"
 
   258 | "height (Lam [x].t) = height t + 1"
 
   255 | "height (Lam [x].t) = height t + 1"
 
   259   apply(simp add: eqvt_def height_graph_def)
 
   256   apply(simp add: eqvt_def height_graph_aux_def)
 
   260   apply(rule TrueI)
 
   257   apply(rule TrueI)
 
   261   apply(rule_tac y="x" in lam.exhaust)
 
   258   apply(rule_tac y="x" in lam.exhaust)
 
   262   using [[simproc del: alpha_lst]]
 
   259   using [[simproc del: alpha_lst]]
 
   263   apply(auto)
 
   260   apply(auto)
 
   264   apply (erule_tac c="()" in Abs_lst1_fcb2)
 
   261   apply (erule_tac c="()" in Abs_lst1_fcb2)
 
   277   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
 
   274   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
 
   278 where
 
   275 where
 
   279   "(Var x)[y ::= s] = (if x = y then s else (Var x))"
 
   276   "(Var x)[y ::= s] = (if x = y then s else (Var x))"
 
   280 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
 
   277 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
 
   281 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
 
   278 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
 
   282   unfolding eqvt_def subst_graph_def
 
   279   apply(simp add: eqvt_def subst_graph_aux_def)
 
   283   apply(simp)
 
       
   284   apply(rule TrueI)
 
   280   apply(rule TrueI)
 
   285   using [[simproc del: alpha_lst]]
 
   281   using [[simproc del: alpha_lst]]
 
   286   apply(auto)
 
   282   apply(auto)
 
   287   apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
 
   283   apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
 
   288   apply(blast)+
 
   284   apply(blast)+
 
   466   trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
 
   462   trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
 
   467 where
 
   463 where
 
   468   "trans (Var x) xs = lookup xs 0 x"
 
   464   "trans (Var x) xs = lookup xs 0 x"
 
   469 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
 
   465 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
 
   470 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"
 
   466 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"
 
   471   apply (simp add: eqvt_def trans_graph_def)
 
   467   apply (simp add: eqvt_def trans_graph_aux_def)
 
   472   apply (erule trans_graph.induct)
 
   468   apply (erule trans_graph.induct)
 
   473   apply (auto simp add: ln.fresh)[3]
 
   469   apply (auto simp add: ln.fresh)[3]
 
   474   apply (simp add: supp_lookup_fresh)
 
   470   apply (simp add: supp_lookup_fresh)
 
   475   apply (simp add: fresh_star_def ln.fresh)
 
   471   apply (simp add: fresh_star_def ln.fresh)
 
   476   apply (simp add: ln.fresh fresh_star_def)
 
   472   apply (simp add: ln.fresh fresh_star_def)
 
   501   cntlams :: "lam  \<Rightarrow> nat"
 
   497   cntlams :: "lam  \<Rightarrow> nat"
 
   502 where
 
   498 where
 
   503   "cntlams (Var x) = 0"
 
   499   "cntlams (Var x) = 0"
 
   504 | "cntlams (App t1 t2) = (cntlams t1) + (cntlams t2)"
 
   500 | "cntlams (App t1 t2) = (cntlams t1) + (cntlams t2)"
 
   505 | "cntlams (Lam [x]. t) = Suc (cntlams t)"
 
   501 | "cntlams (Lam [x]. t) = Suc (cntlams t)"
 
   506   apply(simp add: eqvt_def cntlams_graph_def)
 
   502   apply(simp add: eqvt_def cntlams_graph_aux_def)
 
   507   apply(rule TrueI)
 
   503   apply(rule TrueI)
 
   508   apply(rule_tac y="x" in lam.exhaust)
 
   504   apply(rule_tac y="x" in lam.exhaust)
 
   509   apply(auto)[3]
 
   505   apply(auto)[3]
 
   510   apply(all_trivials)
 
   506   apply(all_trivials)
 
   511   apply(simp)
 
   507   apply(simp)
 
   528   cntbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat"
 
   524   cntbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat"
 
   529 where
 
   525 where
 
   530   "cntbvs (Var x) xs = (if x \<in> set xs then 1 else 0)"
 
   526   "cntbvs (Var x) xs = (if x \<in> set xs then 1 else 0)"
 
   531 | "cntbvs (App t1 t2) xs = (cntbvs t1 xs) + (cntbvs t2 xs)"
 
   527 | "cntbvs (App t1 t2) xs = (cntbvs t1 xs) + (cntbvs t2 xs)"
 
   532 | "atom x \<sharp> xs \<Longrightarrow> cntbvs (Lam [x]. t) xs = cntbvs t (x # xs)"
 
   528 | "atom x \<sharp> xs \<Longrightarrow> cntbvs (Lam [x]. t) xs = cntbvs t (x # xs)"
 
   533   apply(simp add: eqvt_def cntbvs_graph_def)
 
   529   apply(simp add: eqvt_def cntbvs_graph_aux_def)
 
   534   apply(rule TrueI)
 
   530   apply(rule TrueI)
 
   535   apply(case_tac x)
 
   531   apply(case_tac x)
 
   536   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
 
   532   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
 
   537   apply(auto simp add: fresh_star_def)[3]
 
   533   apply(auto simp add: fresh_star_def)[3]
 
   538   apply(all_trivials)
 
   534   apply(all_trivials)
 
   587 where
 
   583 where
 
   588   "transdb (Var x) l = vindex l x 0"
 
   584   "transdb (Var x) l = vindex l x 0"
 
   589 | "transdb (App t1 t2) xs = 
   585 | "transdb (App t1 t2) xs = 
   590       Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))"
 
   586       Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))"
 
   591 | "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))"
 
   587 | "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))"
 
   592   unfolding eqvt_def transdb_graph_def
 
   588   apply(simp add: eqvt_def transdb_graph_aux_def)
 
   593   apply(simp)
 
       
   594   apply(rule TrueI)
 
   589   apply(rule TrueI)
 
   595   apply (case_tac x)
 
   590   apply (case_tac x)
 
   596   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
 
   591   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
 
   597   apply (auto simp add: fresh_star_def fresh_at_list)[3]
 
   592   apply (auto simp add: fresh_star_def fresh_at_list)[3]
 
   598   using [[simproc del: alpha_lst]]
 
   593   using [[simproc del: alpha_lst]]
 
   649 | "eval (Lam [x].t) = Lam [x].(eval t)"
 
   644 | "eval (Lam [x].t) = Lam [x].(eval t)"
 
   650 | "eval (App t1 t2) = apply_subst (eval t1) (eval t2)"
 
   645 | "eval (App t1 t2) = apply_subst (eval t1) (eval t2)"
 
   651 | "apply_subst (Var x) t2 = App (Var x) t2"
 
   646 | "apply_subst (Var x) t2 = App (Var x) t2"
 
   652 | "apply_subst (App t0 t1) t2 = App (App t0 t1) t2"
 
   647 | "apply_subst (App t0 t1) t2 = App (App t0 t1) t2"
 
   653 | "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])"
 
   648 | "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])"
 
   654   apply(simp add: eval_apply_subst_graph_def eqvt_def)
 
   649   apply(simp add: eval_apply_subst_graph_aux_def eqvt_def)
 
   655   apply(rule TrueI)
 
   650   apply(rule TrueI)
 
   656   apply (case_tac x)
 
   651   apply (case_tac x)
 
   657   apply (case_tac a rule: lam.exhaust)
 
   652   apply (case_tac a rule: lam.exhaust)
 
   658   using [[simproc del: alpha_lst]]
 
   653   using [[simproc del: alpha_lst]]
 
   659   apply simp_all[3]
 
   654   apply simp_all[3]
 
   701 text {* TODO: eqvt_at for the other side *}
 
   696 text {* TODO: eqvt_at for the other side *}
 
   702 nominal_primrec q where
 
   697 nominal_primrec q where
 
   703   "atom c \<sharp> (x, M) \<Longrightarrow> q (Lam [x]. M) (N :: lam) = Lam [x]. (Lam [c]. (App M (q (Var c) N)))"
 
   698   "atom c \<sharp> (x, M) \<Longrightarrow> q (Lam [x]. M) (N :: lam) = Lam [x]. (Lam [c]. (App M (q (Var c) N)))"
 
   704 | "q (Var x) N = Var x"
 
   699 | "q (Var x) N = Var x"
 
   705 | "q (App l r) N = App l r"
 
   700 | "q (App l r) N = App l r"
 
   706 unfolding eqvt_def q_graph_def
 
   701 apply(simp add: eqvt_def q_graph_aux_def)
 
   707 apply (simp)
 
       
   708 apply (rule TrueI)
 
   702 apply (rule TrueI)
 
   709 apply (case_tac x)
 
   703 apply (case_tac x)
 
   710 apply (rule_tac y="a" in lam.exhaust)
 
   704 apply (rule_tac y="a" in lam.exhaust)
 
   711 using [[simproc del: alpha_lst]]
 
   705 using [[simproc del: alpha_lst]]
 
   712 apply simp_all
 
   706 apply simp_all
 
   730 where
 
   724 where
 
   731   "eqvt f \<Longrightarrow> map_term f (Var x) = f (Var x)"
 
   725   "eqvt f \<Longrightarrow> map_term f (Var x) = f (Var x)"
 
   732 | "eqvt f \<Longrightarrow> map_term f (App t1 t2) = App (f t1) (f t2)"
 
   726 | "eqvt f \<Longrightarrow> map_term f (App t1 t2) = App (f t1) (f t2)"
 
   733 | "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)"
 
   727 | "eqvt f \<Longrightarrow> map_term f (Lam [x].t) = Lam [x].(f t)"
 
   734 | "\<not>eqvt f \<Longrightarrow> map_term f t = t"
 
   728 | "\<not>eqvt f \<Longrightarrow> map_term f t = t"
 
   735   apply (simp add: eqvt_def map_term_graph_def)
 
   729   apply (simp add: eqvt_def map_term_graph_aux_def)
 
   736   apply(rule TrueI)
 
   730   apply(rule TrueI)
 
   737   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
 
   731   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
 
   738   using [[simproc del: alpha_lst]]
 
   732   using [[simproc del: alpha_lst]]
 
   739   apply auto
 
   733   apply auto
 
   740   apply (erule Abs_lst1_fcb)
 
   734   apply (erule Abs_lst1_fcb)
 
   810 nominal_primrec
 
   804 nominal_primrec
 
   811   Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
 
   805   Z :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
 
   812 where
 
   806 where
 
   813   "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"
 
   807   "Z (App M N) k = Z M (%m. (Z N (%n.(App m n))))"
 
   814 | "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))"
 
   808 | "Z (App M N) k = Z M (%m. (Z N (%n.(App (App m n) (Abs b (k (Var b)))))))"
 
   815 unfolding eqvt_def Z_graph_def
 
   809 apply(simp add: eqvt_def Z_graph_aux_def)
 
   816 apply (rule, perm_simp, rule)
 
   810 apply (rule, perm_simp, rule)
 
   817 oops
 
   811 oops
 
   818 
   812 
   819 lemma test:
 
   813 lemma test:
 
   820   assumes "t = s"
 
   814   assumes "t = s"
 
   850 | "aux (App t1 t2) (Lam [x].t) xs = False"
 
   844 | "aux (App t1 t2) (Lam [x].t) xs = False"
 
   851 | "aux (Lam [x].t) (Var y) xs = False"
 
   845 | "aux (Lam [x].t) (Var y) xs = False"
 
   852 | "aux (Lam [x].t) (App t1 t2) xs = False"
 
   846 | "aux (Lam [x].t) (App t1 t2) xs = False"
 
   853 | "\<lbrakk>{atom x} \<sharp>* (s, xs); {atom y} \<sharp>* (t, xs); x \<noteq> y\<rbrakk> \<Longrightarrow> 
   847 | "\<lbrakk>{atom x} \<sharp>* (s, xs); {atom y} \<sharp>* (t, xs); x \<noteq> y\<rbrakk> \<Longrightarrow> 
   854        aux (Lam [x].t) (Lam [y].s) xs = aux t s ((x, y) # xs)"
 
   848        aux (Lam [x].t) (Lam [y].s) xs = aux t s ((x, y) # xs)"
 
   855   apply (simp add: eqvt_def aux_graph_def)
 
   849   apply (simp add: eqvt_def aux_graph_aux_def)
 
   856   apply(erule aux_graph.induct)
 
   850   apply(erule aux_graph.induct)
 
   857   apply(simp_all add: fresh_star_def pure_fresh)[9]
 
   851   apply(simp_all add: fresh_star_def pure_fresh)[9]
 
   858   apply(case_tac x)
 
   852   apply(case_tac x)
 
   859   apply(simp)
 
   853   apply(simp)
 
   860   apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
 
   854   apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
 
   897 | "aux2 (App t1 t2) (Var x) = False"
 
   891 | "aux2 (App t1 t2) (Var x) = False"
 
   898 | "aux2 (App t1 t2) (Lam [x].t) = False"
 
   892 | "aux2 (App t1 t2) (Lam [x].t) = False"
 
   899 | "aux2 (Lam [x].t) (Var y) = False"
 
   893 | "aux2 (Lam [x].t) (Var y) = False"
 
   900 | "aux2 (Lam [x].t) (App t1 t2) = False"
 
   894 | "aux2 (Lam [x].t) (App t1 t2) = False"
 
   901 | "x = y \<Longrightarrow> aux2 (Lam [x].t) (Lam [y].s) = aux2 t s"
 
   895 | "x = y \<Longrightarrow> aux2 (Lam [x].t) (Lam [y].s) = aux2 t s"
 
   902   apply(simp add: eqvt_def aux2_graph_def)
 
   896   apply(simp add: eqvt_def aux2_graph_aux_def)
 
   903   apply(simp)
 
   897   apply(rule TrueI)
 
   904   apply(case_tac x)
 
   898   apply(case_tac x)
 
   905   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
 
   899   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
 
   906   apply(rule_tac y="b" in lam.exhaust)
 
   900   apply(rule_tac y="b" in lam.exhaust)
 
   907   apply(auto)[3]
 
   901   apply(auto)[3]
 
   908   apply(rule_tac y="b" in lam.exhaust)
 
   902   apply(rule_tac y="b" in lam.exhaust)
nominal2