|
1 theory Term4 |
|
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" "Quotient_List" |
|
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 (Datatype.the_info @{theory} "Term4.rtrm4") 1 *} |
|
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 (Datatype.the_info @{theory} "Term4.rtrm4") |
|
33 [[[], [], [(NONE, 0,1)]], [[], []] ] *} |
|
34 print_theorems |
|
35 |
|
36 lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4" |
|
37 apply (rule ext)+ |
|
38 apply (induct_tac x xa rule: list_induct2') |
|
39 apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros) |
|
40 apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) |
|
41 apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all) |
|
42 apply rule |
|
43 apply (erule alpha_rtrm4_list.cases) |
|
44 apply simp_all |
|
45 apply (rule alpha_rtrm4_alpha_rtrm4_list.intros) |
|
46 apply simp_all |
|
47 done |
|
48 |
|
49 (* We need sth like: |
|
50 lemma fix3: "fv_rtrm4_list = set o map fv_rtrm4" *) |
|
51 |
|
52 notation |
|
53 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
|
54 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
|
55 thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2] |
|
56 |
|
57 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *} |
|
58 thm alpha4_inj |
|
59 |
|
60 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (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)) *} |
|
61 thm alpha4_inj_no |
|
62 |
|
63 local_setup {* |
|
64 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} |
|
65 *} |
|
66 print_theorems |
|
67 |
|
68 local_setup {* |
|
69 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt_no}, []), |
|
70 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_no} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt)) |
|
71 *} |
|
72 lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2] |
|
73 |
|
74 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []), |
|
75 (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_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *} |
|
76 lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2] |
|
77 |
|
78 (*lemma fv_rtrm4_rsp: |
|
79 "xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya" |
|
80 "x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y" |
|
81 apply (induct rule: alpha_rtrm4_alpha_rtrm4_list.inducts) |
|
82 apply (simp_all add: alpha_gen) |
|
83 done*) |
|
84 |
|
85 |
|
86 quotient_type |
|
87 trm4 = rtrm4 / alpha_rtrm4 |
|
88 (*and |
|
89 trm4list = "rtrm4 list" / alpha_rtrm4_list*) |
|
90 by (simp_all add: alpha4_equivp) |
|
91 |
|
92 local_setup {* |
|
93 (fn ctxt => ctxt |
|
94 |> snd o (Quotient_Def.quotient_lift_const ("Vr4", @{term rVr4})) |
|
95 |> snd o (Quotient_Def.quotient_lift_const ("Ap4", @{term rAp4})) |
|
96 |> snd o (Quotient_Def.quotient_lift_const ("Lm4", @{term rLm4}))) |
|
97 *} |
|
98 print_theorems |
|
99 |
|
100 local_setup {* snd o prove_const_rsp @{binding fv_rtrm4_rsp} [@{term fv_rtrm4}] |
|
101 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm4_alpha_rtrm4_list.inducts(1)} @{thms fv_rtrm4_fv_rtrm4_list.simps} 1) *} |
|
102 print_theorems |
|
103 |
|
104 local_setup {* snd o prove_const_rsp @{binding rVr4_rsp} [@{term rVr4}] |
|
105 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *} |
|
106 lemma "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4" |
|
107 apply simp |
|
108 apply clarify |
|
109 apply (simp add: alpha4_inj) |
|
110 |
|
111 |
|
112 local_setup {* snd o prove_const_rsp @{binding rLm4_rsp} [@{term rLm4}] |
|
113 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *} |
|
114 local_setup {* snd o prove_const_rsp @{binding permute_rtrm4_rsp} |
|
115 [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}, @{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] |
|
116 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *} |
|
117 |
|
118 thm rtrm4.induct |
|
119 lemmas trm1_bp_induct = rtrm4.induct[quot_lifted] |
|
120 |
|
121 end |