19 |
19 |
20 |
20 |
21 (** proves the two pt-type class properties **) |
21 (** proves the two pt-type class properties **) |
22 |
22 |
23 fun prove_permute_zero induct perm_defs perm_fns lthy = |
23 fun prove_permute_zero induct perm_defs perm_fns lthy = |
24 let |
24 let |
25 val perm_types = map (body_type o fastype_of) perm_fns |
25 val perm_types = map (body_type o fastype_of) perm_fns |
26 val perm_indnames = Datatype_Prop.make_tnames perm_types |
26 val perm_indnames = Datatype_Prop.make_tnames perm_types |
27 |
27 |
28 fun single_goal ((perm_fn, T), x) = |
28 fun single_goal ((perm_fn, T), x) = |
29 HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) |
29 HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) |
30 |
30 |
31 val goals = |
31 val goals = |
32 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
32 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
33 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
33 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
34 |
34 |
35 val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) |
35 val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) |
36 |
36 |
37 val tac = (Datatype_Aux.indtac induct perm_indnames |
37 val tac = (Datatype_Aux.indtac induct perm_indnames |
38 THEN_ALL_NEW asm_simp_tac simps) 1 |
38 THEN_ALL_NEW asm_simp_tac simps) 1 |
39 in |
39 in |
40 Goal.prove lthy perm_indnames [] goals (K tac) |
40 Goal.prove lthy perm_indnames [] goals (K tac) |
41 |> Datatype_Aux.split_conj_thm |
41 |> Datatype_Aux.split_conj_thm |
42 end |
42 end |
43 |
43 |
44 |
44 |
45 fun prove_permute_plus induct perm_defs perm_fns lthy = |
45 fun prove_permute_plus induct perm_defs perm_fns lthy = |
46 let |
46 let |
47 val p = Free ("p", @{typ perm}) |
47 val p = Free ("p", @{typ perm}) |
48 val q = Free ("q", @{typ perm}) |
48 val q = Free ("q", @{typ perm}) |
49 val perm_types = map (body_type o fastype_of) perm_fns |
49 val perm_types = map (body_type o fastype_of) perm_fns |
50 val perm_indnames = Datatype_Prop.make_tnames perm_types |
50 val perm_indnames = Datatype_Prop.make_tnames perm_types |
51 |
51 |
52 fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq |
52 fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq |
53 (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T))) |
53 (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T))) |
54 |
54 |
55 val goals = |
55 val goals = |
56 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
56 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
57 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
57 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
58 |
58 |
59 val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) |
59 val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) |
60 |
60 |
61 val tac = (Datatype_Aux.indtac induct perm_indnames |
61 val tac = (Datatype_Aux.indtac induct perm_indnames |
62 THEN_ALL_NEW asm_simp_tac simps) 1 |
62 THEN_ALL_NEW asm_simp_tac simps) 1 |
63 in |
63 in |
64 Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) |
64 Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) |
65 |> Datatype_Aux.split_conj_thm |
65 |> Datatype_Aux.split_conj_thm |
66 end |
66 end |
67 |
67 |
68 |
68 |
69 fun mk_perm_eq ty_perm_assoc cnstr = |
69 fun mk_perm_eq ty_perm_assoc cnstr = |
70 let |
70 let |
71 fun lookup_perm p (ty, arg) = |
71 fun lookup_perm p (ty, arg) = |
72 case (AList.lookup (op=) ty_perm_assoc ty) of |
72 case (AList.lookup (op=) ty_perm_assoc ty) of |
73 SOME perm => perm $ p $ arg |
73 SOME perm => perm $ p $ arg |
74 | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg |
74 | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg |
75 |
75 |
76 val p = Free ("p", @{typ perm}) |
76 val p = Free ("p", @{typ perm}) |
77 val (arg_tys, ty) = |
77 val (arg_tys, ty) = |
78 fastype_of cnstr |
78 fastype_of cnstr |
79 |> strip_type |
79 |> strip_type |
80 |
80 |
81 val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) |
81 val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) |
82 val args = map Free (arg_names ~~ arg_tys) |
82 val args = map Free (arg_names ~~ arg_tys) |
83 |
83 |
84 val lhs = lookup_perm p (ty, list_comb (cnstr, args)) |
84 val lhs = lookup_perm p (ty, list_comb (cnstr, args)) |
85 val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args)) |
85 val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args)) |
86 |
86 |
87 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
87 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
88 in |
88 in |
89 (Attrib.empty_binding, eq) |
89 (Attrib.empty_binding, eq) |
90 end |
90 end |
91 |
91 |
92 |
92 |
93 fun define_raw_perms full_ty_names tys tvs constrs induct_thm lthy = |
93 fun define_raw_perms full_ty_names tys tvs constrs induct_thm lthy = |
94 let |
94 let |
95 val perm_fn_names = full_ty_names |
95 val perm_fn_names = full_ty_names |
96 |> map Long_Name.base_name |
96 |> map Long_Name.base_name |
97 |> map (prefix "permute_") |
97 |> map (prefix "permute_") |
98 |
98 |
99 val perm_fn_types = map perm_ty tys |
99 val perm_fn_types = map perm_ty tys |
100 val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) |
100 val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) |
101 val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names |
101 val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names |
102 |
102 |
103 val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs |
103 val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs |
104 |
104 |
105 fun tac _ (_, _, simps) = |
105 fun tac _ (_, _, simps) = |
106 Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) |
106 Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) |
107 |
107 |
108 fun morphism phi (fvs, dfs, simps) = |
108 fun morphism phi (fvs, dfs, simps) = |
109 (map (Morphism.term phi) fvs, |
109 (map (Morphism.term phi) fvs, |
110 map (Morphism.thm phi) dfs, |
110 map (Morphism.thm phi) dfs, |
111 map (Morphism.thm phi) simps); |
111 map (Morphism.thm phi) simps); |
112 |
112 |
113 val ((perm_funs, perm_eq_thms), lthy') = |
113 val ((perm_funs, perm_eq_thms), lthy') = |
114 lthy |
114 lthy |
115 |> Local_Theory.exit_global |
115 |> Local_Theory.exit_global |
116 |> Class.instantiation (full_ty_names, tvs, @{sort pt}) |
116 |> Class.instantiation (full_ty_names, tvs, @{sort pt}) |
117 |> Primrec.add_primrec perm_fn_binds perm_eqs |
117 |> Primrec.add_primrec perm_fn_binds perm_eqs |
118 |
118 |
119 val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy' |
119 val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy' |
120 val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy' |
120 val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy' |
121 in |
121 in |
122 lthy' |
122 lthy' |
123 |> Class.prove_instantiation_exit_result morphism tac |
123 |> Class.prove_instantiation_exit_result morphism tac |
124 (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms) |
124 (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms) |
125 ||> Named_Target.theory_init |
125 ||> Named_Target.theory_init |
126 end |
126 end |
127 |
127 |
128 |
128 |
129 end (* structure *) |
129 end (* structure *) |
130 |
130 |