1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Term4
|
1318
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
2 |
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" "Quotient_List"
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
atom_decl name
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
section {*** lam with indirect list recursion ***}
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
datatype rtrm4 =
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
rVr4 "name"
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
| rAp4 "rtrm4" "rtrm4 list"
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
| rLm4 "name" "rtrm4" --"bind (name) in (trm)"
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
print_theorems
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
thm rtrm4.recs
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
(* there cannot be a clause for lists, as *)
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
(* permutations are already defined in Nominal (also functions, options, and so on) *)
|
1277
|
19 |
setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term4.rtrm4") 1 *}
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
(* "repairing" of the permute function *)
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
lemma repaired:
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
fixes ts::"rtrm4 list"
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
24 |
shows "permute_rtrm4_list p ts = p \<bullet> ts"
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
apply(induct ts)
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
apply(simp_all)
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
done
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
thm permute_rtrm4_permute_rtrm4_list.simps
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
30 |
thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
31 |
|
1277
|
32 |
local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4")
|
1300
|
33 |
[[[], [], [(NONE, 0,1)]], [[], []] ] *}
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
34 |
print_theorems
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
35 |
|
1318
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
36 |
lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4"
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
37 |
apply (rule ext)+
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
38 |
apply (induct_tac x xa rule: list_induct2')
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
39 |
apply (simp_all add: alpha_rtrm4_alpha_rtrm4_list.intros)
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
40 |
apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all)
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
41 |
apply clarify apply (erule alpha_rtrm4_list.cases) apply(simp_all)
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
42 |
apply rule
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
43 |
apply (erule alpha_rtrm4_list.cases)
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
44 |
apply simp_all
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
45 |
apply (rule alpha_rtrm4_alpha_rtrm4_list.intros)
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
46 |
apply simp_all
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
47 |
done
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
48 |
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
49 |
(* We need sth like:
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
50 |
lemma fix3: "fv_rtrm4_list = set o map fv_rtrm4" *)
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
51 |
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
52 |
notation
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
53 |
alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
54 |
alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
|
1318
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
55 |
thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
56 |
|
1318
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
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)) *}
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
58 |
thm alpha4_inj
|
1318
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
59 |
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
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)) *}
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
61 |
thm alpha4_inj_no
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
62 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
63 |
local_setup {*
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
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}
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
65 |
*}
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
66 |
print_theorems
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
67 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
68 |
local_setup {*
|
1318
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
69 |
(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt_no}, []),
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
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))
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
71 |
*}
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
72 |
lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2]
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
73 |
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
74 |
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []),
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
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)) *}
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
76 |
lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2]
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
77 |
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
78 |
(*lemma fv_rtrm4_rsp:
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
79 |
"xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya"
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
80 |
"x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y"
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
81 |
apply (induct rule: alpha_rtrm4_alpha_rtrm4_list.inducts)
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
82 |
apply (simp_all add: alpha_gen)
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
83 |
done*)
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
84 |
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
85 |
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
86 |
quotient_type
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
87 |
trm4 = rtrm4 / alpha_rtrm4
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
88 |
(*and
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
89 |
trm4list = "rtrm4 list" / alpha_rtrm4_list*)
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
90 |
by (simp_all add: alpha4_equivp)
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
91 |
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
92 |
local_setup {*
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
93 |
(fn ctxt => ctxt
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
94 |
|> snd o (Quotient_Def.quotient_lift_const ("Vr4", @{term rVr4}))
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
95 |
|> snd o (Quotient_Def.quotient_lift_const ("Ap4", @{term rAp4}))
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
96 |
|> snd o (Quotient_Def.quotient_lift_const ("Lm4", @{term rLm4})))
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
97 |
*}
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
98 |
print_theorems
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
99 |
|
1318
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
100 |
local_setup {* snd o prove_const_rsp @{binding fv_rtrm4_rsp} [@{term fv_rtrm4}]
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
101 |
(fn _ => fvbv_rsp_tac @{thm alpha_rtrm4_alpha_rtrm4_list.inducts(1)} @{thms fv_rtrm4_fv_rtrm4_list.simps} 1) *}
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
102 |
print_theorems
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
103 |
|
1318
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
104 |
local_setup {* snd o prove_const_rsp @{binding rVr4_rsp} [@{term rVr4}]
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
105 |
(fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *}
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
106 |
lemma "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
107 |
apply simp
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
108 |
apply clarify
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
109 |
apply (simp add: alpha4_inj)
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
110 |
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
111 |
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
112 |
local_setup {* snd o prove_const_rsp @{binding rLm4_rsp} [@{term rLm4}]
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
113 |
(fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *}
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
114 |
local_setup {* snd o prove_const_rsp @{binding permute_rtrm4_rsp}
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
115 |
[@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}, @{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}]
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
116 |
(fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *}
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
117 |
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
118 |
thm rtrm4.induct
|
cce1b6d1b761
Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
119 |
lemmas trm1_bp_induct = rtrm4.induct[quot_lifted]
|
1270
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
120 |
|
8c3cf9f4f5f2
Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
121 |
end
|