44 val pi = Free ("pi", @{typ perm}); |
44 val pi = Free ("pi", @{typ perm}); |
45 fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty); |
45 fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty); |
46 val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm}); |
46 val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm}); |
47 *} |
47 *} |
48 ML {* |
48 ML {* |
49 val perm_eqs = maps (fn (i, (_, _, constrs)) => |
49 fun perm_eq (i, (_, _, constrs)) = |
50 let val T = nth_dtyp i |
50 map (fn (cname, dts) => |
51 in map (fn (cname, dts) => |
|
52 let |
51 let |
53 val Ts = map (typ_of_dtyp descr sorts) dts; |
52 val Ts = map (typ_of_dtyp descr sorts) dts; |
54 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
53 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
55 val args = map Free (names ~~ Ts); |
54 val args = map Free (names ~~ Ts); |
56 val c = Const (cname, Ts ---> T); |
55 val c = Const (cname, Ts ---> (nth_dtyp i)); |
57 fun perm_arg (dt, x) = |
56 fun perm_arg (dt, x) = |
58 let val T = type_of x |
57 let val T = type_of x |
59 in |
58 in |
60 if is_rec_type dt then |
59 if is_rec_type dt then |
61 let val (Us, _) = strip_type T |
60 let val (Us, _) = strip_type T |
70 in |
69 in |
71 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
70 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
72 (Free (nth perm_names_types' i) $ |
71 (Free (nth perm_names_types' i) $ |
73 Free ("pi", @{typ perm}) $ list_comb (c, args), |
72 Free ("pi", @{typ perm}) $ list_comb (c, args), |
74 list_comb (c, map perm_arg (dts ~~ args))))) |
73 list_comb (c, map perm_arg (dts ~~ args))))) |
75 end) constrs |
74 end) constrs; |
76 end) descr; |
75 val perm_eqs = maps perm_eq descr; |
77 *} |
76 *} |
78 |
77 |
79 local_setup {* |
78 local_setup {* |
80 snd o (Primrec.add_primrec |
79 snd o (Primrec.add_primrec |
81 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs) |
80 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs) |
97 fun tac _ = |
96 fun tac _ = |
98 EVERY [indtac induct perm_indnames 1, |
97 EVERY [indtac induct perm_indnames 1, |
99 ALLGOALS (asm_full_simp_tac @{simpset})]; |
98 ALLGOALS (asm_full_simp_tac @{simpset})]; |
100 in |
99 in |
101 map Drule.export_without_context (List.take (split_conj_thm |
100 map Drule.export_without_context (List.take (split_conj_thm |
102 (Goal.prove_global @{theory} [] [] gl tac), |
101 (Goal.prove @{context} [] [] gl tac), |
103 length new_type_names)) |
102 length new_type_names)) |
104 end |
103 end |
105 *} |
104 *} |
106 |
105 |
107 ML {* |
106 ML {* |
108 val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"} |
107 val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"} |
109 val pi1 = Free ("pi1", @{typ perm}); |
108 val pi1 = Free ("pi1", @{typ perm}); |
110 val pi2 = Free ("pi2", @{typ perm}); |
109 val pi2 = Free ("pi2", @{typ perm}); |
111 val perm_append_thms = |
110 val perm_append_thms = |
112 List.take (map Drule.export_without_context (split_conj_thm |
111 List.take (map Drule.export_without_context (split_conj_thm |
113 (Goal.prove_global @{theory} [] [] |
112 (Goal.prove @{context} [] [] |
114 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
113 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
115 (map (fn ((s, T), x) => |
114 (map (fn ((s, T), x) => |
116 let |
115 let |
117 val perm = Const (s, @{typ perm} --> T --> T); |
116 val perm = Const (s, @{typ perm} --> T --> T); |
118 val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T) |
117 val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T) |