equal
deleted
inserted
replaced
20 |
20 |
21 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term6.rtrm6") 1 *} |
21 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term6.rtrm6") 1 *} |
22 print_theorems |
22 print_theorems |
23 |
23 |
24 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term6.rtrm6") [ |
24 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term6.rtrm6") [ |
25 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *} |
25 [[], [(NONE, 0, 1)], [(SOME @{term rbv6}, 0, 1)]]] *} |
26 notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100) |
26 notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100) |
27 thm alpha_rtrm6.intros |
27 thm alpha_rtrm6.intros |
28 |
28 |
29 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *} |
29 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *} |
30 thm alpha6_inj |
30 thm alpha6_inj |
39 |
39 |
40 local_setup {* |
40 local_setup {* |
41 (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_eqvt}, []), |
41 (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_eqvt}, []), |
42 build_alpha_eqvts [@{term alpha_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] @{thms permute_rtrm6.simps alpha6_inj} @{thm alpha_rtrm6.induct} ctxt) ctxt)) |
42 build_alpha_eqvts [@{term alpha_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] @{thms permute_rtrm6.simps alpha6_inj} @{thm alpha_rtrm6.induct} ctxt) ctxt)) |
43 *} |
43 *} |
44 |
44 thm alpha6_eqvt |
45 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []), |
45 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []), |
46 (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *} |
46 (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *} |
47 thm alpha6_equivp |
47 thm alpha6_equivp |
48 |
48 |
49 quotient_type |
49 quotient_type |