equal
deleted
inserted
replaced
591 transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option" |
591 transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option" |
592 where |
592 where |
593 "transdb (Var x) l = vindex l x 0" |
593 "transdb (Var x) l = vindex l x 0" |
594 | "transdb (App t1 t2) xs = |
594 | "transdb (App t1 t2) xs = |
595 Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))" |
595 Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))" |
596 | "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))" |
596 | "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map_option DBLam (transdb t (x # xs))" |
597 apply(simp add: eqvt_def transdb_graph_aux_def) |
597 apply(simp add: eqvt_def transdb_graph_aux_def) |
598 apply(rule TrueI) |
598 apply(rule TrueI) |
599 apply (case_tac x) |
599 apply (case_tac x) |
600 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
600 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
601 apply (auto simp add: fresh_star_def fresh_at_list)[3] |
601 apply (auto simp add: fresh_star_def fresh_at_list)[3] |