|
1 theory Term4 |
|
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 section {*** lam with indirect list recursion ***} |
|
8 |
|
9 datatype rtrm4 = |
|
10 rVr4 "name" |
|
11 | rAp4 "rtrm4" "rtrm4 list" |
|
12 | rLm4 "name" "rtrm4" --"bind (name) in (trm)" |
|
13 print_theorems |
|
14 |
|
15 thm rtrm4.recs |
|
16 |
|
17 (* there cannot be a clause for lists, as *) |
|
18 (* permutations are already defined in Nominal (also functions, options, and so on) *) |
|
19 setup {* snd o define_raw_perms ["rtrm4"] ["Term4.rtrm4"] *} |
|
20 |
|
21 (* "repairing" of the permute function *) |
|
22 lemma repaired: |
|
23 fixes ts::"rtrm4 list" |
|
24 shows "permute_rtrm4_list p ts = p \<bullet> ts" |
|
25 apply(induct ts) |
|
26 apply(simp_all) |
|
27 done |
|
28 |
|
29 thm permute_rtrm4_permute_rtrm4_list.simps |
|
30 thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] |
|
31 |
|
32 local_setup {* snd o define_fv_alpha "Term4.rtrm4" [ |
|
33 [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} |
|
34 print_theorems |
|
35 |
|
36 notation |
|
37 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
|
38 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
|
39 thm alpha_rtrm4_alpha_rtrm4_list.intros |
|
40 |
|
41 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} |
|
42 thm alpha4_inj |
|
43 thm alpha_rtrm4_alpha_rtrm4_list.induct |
|
44 |
|
45 local_setup {* |
|
46 snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct} |
|
47 *} |
|
48 print_theorems |
|
49 |
|
50 local_setup {* |
|
51 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []), |
|
52 build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt)) |
|
53 *} |
|
54 print_theorems |
|
55 |
|
56 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []), |
|
57 (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *} |
|
58 thm alpha4_equivp |
|
59 |
|
60 quotient_type |
|
61 qrtrm4 = rtrm4 / alpha_rtrm4 and |
|
62 qrtrm4list = "rtrm4 list" / alpha_rtrm4_list |
|
63 by (simp_all add: alpha4_equivp) |
|
64 |
|
65 end |