110 val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names); |
110 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) |
111 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' |
112 val perms_name = space_implode "_" perm_names' |
113 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
113 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
114 val perms_append_bind = Binding.name (perms_name ^ "_append") |
114 val perms_append_bind = Binding.name (perms_name ^ "_append") |
115 fun tac _ perm_thms = |
115 fun tac _ (_, simps) = |
116 (Class.intro_classes_tac []) THEN (ALLGOALS ( |
116 (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps)); |
117 simp_tac (HOL_ss addsimps perm_thms |
117 fun morphism phi (dfs, simps) = (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps); |
118 ))); |
|
119 fun morphism phi = map (Morphism.thm phi); |
|
120 in |
118 in |
121 lthy' |
119 lthy' |
122 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms)) |
120 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms)) |
123 |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms)) |
121 |> 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) |
122 |> Class_Target.prove_instantiation_exit_result morphism tac (perm_ldef, (perm_empty_thms @ perm_append_thms)) |
125 end |
123 end |
126 |
124 |
|
125 *} |
|
126 |
|
127 ML {* |
|
128 fun define_lifted_perms full_tnames name_term_pairs thms thy = |
|
129 let |
|
130 val lthy = |
|
131 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
|
132 val lthy' = fold (snd oo Quotient_Def.quotient_lift_const) name_term_pairs lthy |
|
133 val lifted_thms = map (fn x => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy', x))) thms |
|
134 fun tac _ = |
|
135 Class.intro_classes_tac [] THEN |
|
136 (ALLGOALS (resolve_tac lifted_thms)) |
|
137 val lthy'' = Class.prove_instantiation_instance tac lthy' |
|
138 in |
|
139 Local_Theory.exit_global lthy'' |
|
140 end |
127 *} |
141 *} |
128 |
142 |
129 (* Test |
143 (* Test |
130 atom_decl name |
144 atom_decl name |
131 |
145 |