equal
deleted
inserted
replaced
6 Var "name" |
6 Var "name" |
7 | App "lam" "lam" |
7 | App "lam" "lam" |
8 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
8 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
9 |
9 |
10 nominal_primrec lam2_rec where |
10 nominal_primrec lam2_rec where |
11 "lam2_rec faa fll xs (Var n) (Var m) = ((n, m) \<in> set xs)" |
11 "lam2_rec faa fll xs (Var n) (Var m) = (n = m \<or> (n, m) \<in> set xs)" |
12 | "lam2_rec faa fll xs (Var n) (App l r) = False" |
12 | "lam2_rec faa fll xs (Var n) (App l r) = False" |
13 | "lam2_rec faa fll xs (Var n) (Lam [x]. t) = False" |
13 | "lam2_rec faa fll xs (Var n) (Lam [x]. t) = False" |
14 | "lam2_rec faa fll xs (App l r) (Var n) = False" |
14 | "lam2_rec faa fll xs (App l r) (Var n) = False" |
15 | "lam2_rec faa fll xs (App l1 r1) (App l2 r2) = faa l1 r1 l2 r2" |
15 | "lam2_rec faa fll xs (App l1 r1) (App l2 r2) = faa l1 r1 l2 r2" |
16 | "lam2_rec faa fll xs (App l r) (Lam [x]. t) = False" |
16 | "lam2_rec faa fll xs (App l r) (Lam [x]. t) = False" |
115 by pat_completeness auto |
115 by pat_completeness auto |
116 |
116 |
117 termination (eqvt) |
117 termination (eqvt) |
118 by (relation "measure (\<lambda>(l, r, xs). size l + size r)") simp_all |
118 by (relation "measure (\<lambda>(l, r, xs). size l + size r)") simp_all |
119 |
119 |
120 lemma aux_simps: |
120 lemma aux_simps[simp]: |
121 "aux (Var x) (Var y) xs = ((x, y) \<in> set xs)" |
121 "aux (Var x) (Var y) xs = (x = y \<or> (x, y) \<in> set xs)" |
122 "aux (App t1 t2) (App s1 s2) xs = (aux t1 s1 xs \<and> aux t2 s2 xs)" |
122 "aux (App t1 t2) (App s1 s2) xs = (aux t1 s1 xs \<and> aux t2 s2 xs)" |
123 "aux (Var x) (App t1 t2) xs = False" |
123 "aux (Var x) (App t1 t2) xs = False" |
124 "aux (Var x) (Lam [y].t) xs = False" |
124 "aux (Var x) (Lam [y].t) xs = False" |
125 "aux (App t1 t2) (Var x) xs = False" |
125 "aux (App t1 t2) (Var x) xs = False" |
126 "aux (App t1 t2) (Lam [x].t) xs = False" |
126 "aux (App t1 t2) (Lam [x].t) xs = False" |