11 ML {* |
11 ML {* |
12 fun prove_perm_empty lthy induct perm_def perm_frees = |
12 fun prove_perm_empty lthy induct perm_def perm_frees = |
13 let |
13 let |
14 val perm_types = map fastype_of perm_frees; |
14 val perm_types = map fastype_of perm_frees; |
15 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
15 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
|
16 fun glc ((perm, T), x) = |
|
17 HOLogic.mk_eq (perm $ @{term "0 :: perm"} $ Free (x, T), Free (x, T)) |
16 val gl = |
18 val gl = |
17 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
19 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
18 (map (fn ((perm, T), x) => HOLogic.mk_eq |
20 (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))); |
19 (perm $ @{term "0 :: perm"} $ Free (x, T), |
|
20 Free (x, T))) |
|
21 (perm_frees ~~ |
|
22 map body_type perm_types ~~ perm_indnames))); |
|
23 fun tac _ = |
21 fun tac _ = |
24 EVERY [ |
22 EVERY [ |
25 indtac induct perm_indnames 1, |
23 indtac induct perm_indnames 1, |
26 ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def))) |
24 ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def))) |
27 ]; |
25 ]; |
36 val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"} |
34 val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"} |
37 val pi1 = Free ("pi1", @{typ perm}); |
35 val pi1 = Free ("pi1", @{typ perm}); |
38 val pi2 = Free ("pi2", @{typ perm}); |
36 val pi2 = Free ("pi2", @{typ perm}); |
39 val perm_types = map fastype_of perm_frees |
37 val perm_types = map fastype_of perm_frees |
40 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
38 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
|
39 fun glc ((perm, T), x) = |
|
40 HOLogic.mk_eq ( |
|
41 perm $ (add_perm $ pi1 $ pi2) $ Free (x, T), |
|
42 perm $ pi1 $ (perm $ pi2 $ Free (x, T))) |
41 val gl = |
43 val gl = |
42 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
44 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
43 (map (fn ((perm, T), x) => |
45 (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames)))) |
44 let |
|
45 val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T) |
|
46 val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T)) |
|
47 in HOLogic.mk_eq (lhs, rhs) |
|
48 end) |
|
49 (perm_frees ~~ map body_type perm_types ~~ perm_indnames)))) |
|
50 fun tac _ = |
46 fun tac _ = |
51 EVERY [ |
47 EVERY [ |
52 indtac induct perm_indnames 1, |
48 indtac induct perm_indnames 1, |
53 ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def))) |
49 ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def))) |
54 ] |
50 ] |
100 fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs; |
96 fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs; |
101 val perm_eqs = maps perm_eq descr; |
97 val perm_eqs = maps perm_eq descr; |
102 val lthy = |
98 val lthy = |
103 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
99 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
104 (* TODO: Use the version of prmrec that gives the names explicitely. *) |
100 (* TODO: Use the version of prmrec that gives the names explicitely. *) |
105 val ((_, perm_ldef), lthy') = |
101 val ((perm_frees, perm_ldef), lthy') = |
106 Primrec.add_primrec |
102 Primrec.add_primrec |
107 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
103 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
108 val perm_frees = |
|
109 (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef); |
|
110 val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names); |
104 val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names); |
111 val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names) |
105 val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names) |
112 val perms_name = space_implode "_" perm_names' |
106 val perms_name = space_implode "_" perm_names' |
113 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
107 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
114 val perms_append_bind = Binding.name (perms_name ^ "_append") |
108 val perms_append_bind = Binding.name (perms_name ^ "_append") |
115 fun tac _ perm_thms = |
109 fun tac _ (_, simps, _) = |
116 (Class.intro_classes_tac []) THEN (ALLGOALS ( |
110 (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps)); |
117 simp_tac (HOL_ss addsimps perm_thms |
111 fun morphism phi (dfs, simps, fvs) = |
118 ))); |
112 (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs); |
119 fun morphism phi = map (Morphism.thm phi); |
|
120 in |
113 in |
121 lthy' |
114 lthy' |
122 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms)) |
115 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms)) |
123 |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms)) |
116 |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms)) |
124 |> Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms) |
117 |> Class_Target.prove_instantiation_exit_result morphism tac (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees) |
125 end |
118 end |
126 |
119 |
|
120 *} |
|
121 |
|
122 ML {* |
|
123 fun define_lifted_perms full_tnames name_term_pairs thms thy = |
|
124 let |
|
125 val lthy = |
|
126 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
|
127 val lthy' = fold (snd oo Quotient_Def.quotient_lift_const) name_term_pairs lthy |
|
128 val lifted_thms = map (fn x => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy', x))) thms |
|
129 fun tac _ = |
|
130 Class.intro_classes_tac [] THEN |
|
131 (ALLGOALS (resolve_tac lifted_thms)) |
|
132 val lthy'' = Class.prove_instantiation_instance tac lthy' |
|
133 in |
|
134 Local_Theory.exit_global lthy'' |
|
135 end |
127 *} |
136 *} |
128 |
137 |
129 (* Test |
138 (* Test |
130 atom_decl name |
139 atom_decl name |
131 |
140 |