equal
deleted
inserted
replaced
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 declare [[STEPS = 18]] |
7 declare [[STEPS = 20]] |
8 |
8 |
9 nominal_datatype trm = |
9 nominal_datatype trm = |
10 Var "name" |
10 Var "name" |
11 | App "trm" "trm" |
11 | App "trm" "trm" |
12 | Lam x::"name" t::"trm" bind_set x in t |
12 | Lam x::"name" t::"trm" bind_set x in t |
30 thm trm_raw_assg_raw.size(9 - 16) |
30 thm trm_raw_assg_raw.size(9 - 16) |
31 |
31 |
32 (* cannot lift yet *) |
32 (* cannot lift yet *) |
33 thm eq_iff |
33 thm eq_iff |
34 thm eq_iff_simps |
34 thm eq_iff_simps |
35 |
|
36 instantiation trm and assg :: size |
|
37 begin |
|
38 |
|
39 quotient_definition |
|
40 "size_trm :: trm \<Rightarrow> nat" |
|
41 is "size :: trm_raw \<Rightarrow> nat" |
|
42 |
|
43 quotient_definition |
|
44 "size_assg :: assg \<Rightarrow> nat" |
|
45 is "size :: assg_raw \<Rightarrow> nat" |
|
46 |
|
47 instance .. |
|
48 |
|
49 end |
|
50 |
|
51 instantiation trm and assg :: pt |
|
52 begin |
|
53 |
|
54 quotient_definition |
|
55 "permute_trm :: perm => trm => trm" |
|
56 is "permute :: perm \<Rightarrow> trm_raw \<Rightarrow> trm_raw" |
|
57 |
|
58 quotient_definition |
|
59 "permute_assg :: perm => assg => assg" |
|
60 is "permute :: perm \<Rightarrow> assg_raw \<Rightarrow> assg_raw" |
|
61 |
|
62 lemma qperm_laws: |
|
63 fixes t::trm and a::assg |
|
64 shows "permute 0 t = t" |
|
65 and "permute 0 a = a" |
|
66 sorry |
|
67 |
|
68 instance |
|
69 apply(default) |
|
70 sorry |
|
71 |
|
72 end |
|
73 |
35 |
74 ML {* |
36 ML {* |
75 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
37 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
76 *} |
38 *} |
77 |
39 |