--- a/Quot/Nominal/Perm.thy Wed Feb 17 10:20:26 2010 +0100
+++ b/Quot/Nominal/Perm.thy Wed Feb 17 13:54:35 2010 +0100
@@ -1,51 +1,30 @@
theory Perm
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
+imports "Nominal2_Atoms"
begin
-atom_decl name
-
-datatype rtrm1 =
- rVr1 "name"
-| rAp1 "rtrm1" "rtrm1 list"
-| rLm1 "name" "rtrm1"
-| rLt1 "bp" "rtrm1" "rtrm1"
-and bp =
- BUnit
-| BVr "name"
-| BPr "bp" "bp"
+ML {*
+ open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *)
+ fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty);
+ val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm});
+*}
ML {*
- open Datatype_Aux (* typ_of_dtyp, DtRec, ... *)
-*}
-instantiation rtrm1 and bp :: pt
-begin
-
-
-ML {*
- val {descr, induct, ...} = Datatype.the_info @{theory} "Perm.rtrm1";
- val new_type_names = ["rtrm1", "bp"];
+(* TODO: full_name can be obtained from new_type_names with Datatype *)
+fun define_raw_perms new_type_names full_tnames thy =
+let
+ val {descr, induct, ...} = Datatype.the_info thy (hd full_tnames);
(* TODO: [] should be the sorts that we'll take from the specification *)
val sorts = [];
-
fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) =>
"permute_" ^ name_of_typ (nth_dtyp i)) descr);
- val perm_names = replicate (length new_type_names) @{const_name permute} @
- map (Sign.full_bname @{theory}) (List.drop (perm_names', length new_type_names));
val perm_types = map (fn (i, _) =>
let val T = nth_dtyp i
in @{typ perm} --> T --> T end) descr;
val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
- (* TODO: Next line only needed after instantiation *)
- val perm_names_types = perm_names ~~ perm_types;
val perm_names_types' = perm_names' ~~ perm_types;
-
val pi = Free ("pi", @{typ perm});
- fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty);
- val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm});
-*}
-ML {*
fun perm_eq_constr i (cname, dts) =
let
val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -71,63 +50,78 @@
Free ("pi", @{typ perm}) $ list_comb (c, args),
list_comb (c, map perm_arg (dts ~~ args)))))
end;
- fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs;
- val perm_eqs = maps perm_eq descr;
-*}
+ fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs;
+ val perm_eqs = maps perm_eq descr;
+ val lthy =
+ Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
+ (* TODO: Use the version of prmrec that gives the names explicitely. *)
+ val (perm_ldef, lthy') =
+ Primrec.add_primrec
+ (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy;
+ val perm_frees =
+ (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef);
+ val perm_empty_thms =
+ let
+ val gl =
+ HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+ (map (fn ((perm, T), x) => HOLogic.mk_eq
+ (perm $ @{term "0 :: perm"} $ Free (x, T),
+ Free (x, T)))
+ (perm_frees ~~
+ map body_type perm_types ~~ perm_indnames)));
+ fun tac {context = ctxt, ...} =
+ EVERY [
+ indtac induct perm_indnames 1,
+ ALLGOALS (asm_full_simp_tac (@{simpset} addsimps perm_ldef))
+ ];
+ in
+ (List.take (split_conj_thm (Goal.prove lthy' perm_indnames [] gl tac), length new_type_names))
+ end;
+ val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"}
+ val pi1 = Free ("pi1", @{typ perm});
+ val pi2 = Free ("pi2", @{typ perm});
+ val perm_append_thms =
+ List.take ((split_conj_thm
+ (Goal.prove lthy' ("pi1" :: "pi2" :: perm_indnames) []
+ (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+ (map (fn ((perm, T), x) =>
+ let
+ val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T)
+ val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T))
+ in HOLogic.mk_eq (lhs, rhs)
+ end)
+ (perm_frees ~~
+ map body_type perm_types ~~ perm_indnames))))
+ (fn _ => EVERY [indtac induct perm_indnames 1,
+ ALLGOALS (asm_full_simp_tac (@{simpset} addsimps perm_ldef))]))),
+ length new_type_names);
+ fun tac ctxt perm_thms =
+ (Class.intro_classes_tac []) THEN (ALLGOALS (
+ simp_tac (@{simpset} addsimps perm_thms
+ )));
+ fun morphism phi = map (Morphism.thm phi);
+ in
+ Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms) lthy'
+ end
-local_setup {*
-snd o (Primrec.add_primrec
- (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs)
*}
-print_theorems
-
-ML {*
- val perm_empty_thms =
- let
- val gl =
- HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
- (map (fn ((s, T), x) => HOLogic.mk_eq
- (Const (s, @{typ perm} --> T --> T) $
- @{term "0 :: perm"} $ Free (x, T),
- Free (x, T)))
- (perm_names ~~
- map body_type perm_types ~~ perm_indnames)));
- fun tac _ =
- EVERY [indtac induct perm_indnames 1,
- ALLGOALS (asm_full_simp_tac @{simpset})];
- in
- map Drule.export_without_context (List.take (split_conj_thm
- (Goal.prove @{context} [] [] gl tac),
- length new_type_names))
- end
-*}
+(* Test
+atom_decl name
-ML {*
- val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"}
- val pi1 = Free ("pi1", @{typ perm});
- val pi2 = Free ("pi2", @{typ perm});
- val perm_append_thms =
- List.take (map Drule.export_without_context (split_conj_thm
- (Goal.prove @{context} [] []
- (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
- (map (fn ((s, T), x) =>
- let
- val perm = Const (s, @{typ perm} --> T --> T);
- val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T)
- val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T))
- in HOLogic.mk_eq (lhs, rhs)
- end)
- (perm_names ~~
- map body_type perm_types ~~ perm_indnames))))
- (fn _ => EVERY [indtac induct perm_indnames 1,
- ALLGOALS (asm_full_simp_tac @{simpset})]))),
- length new_type_names)
-*}
+datatype rtrm1 =
+ rVr1 "name"
+| rAp1 "rtrm1" "rtrm1 list"
+| rLm1 "name" "rtrm1"
+| rLt1 "bp" "rtrm1" "rtrm1"
+and bp =
+ BUnit
+| BVr "name"
+| BPr "bp" "bp"
-instance
-apply(tactic {*
- (Class.intro_classes_tac []) THEN
- (ALLGOALS (simp_tac (@{simpset} addsimps (perm_empty_thms @ perm_append_thms)))) *})
-done
+
+setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Perm.rtrm1", "Perm.bp"] *}
+print_theorems
+*)
+
end