--- a/Nominal/Fv.thy Wed Mar 03 12:45:55 2010 +0100
+++ b/Nominal/Fv.thy Wed Mar 03 12:47:06 2010 +0100
@@ -61,7 +61,6 @@
| map2i _ _ _ = raise UnequalLengths;
*}
-(* TODO: should be const_name union *)
ML {*
open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
(* TODO: It is the same as one in 'nominal_atoms' *)
@@ -73,7 +72,8 @@
if a = noatoms then b else
if b = noatoms then a else
if a = b then a else
- HOLogic.mk_binop "Set.union" (a, b)) (rev sets) noatoms;
+ HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;
+ val mk_inter = foldr1 (HOLogic.mk_binop @{const_name inf})
fun mk_conjl props =
fold (fn a => fn b =>
if a = @{term True} then b else
@@ -178,11 +178,14 @@
val rhs = mk_pair (rhs_binds, arg2);
val alpha = nth alpha_frees (body_index dt);
val fv = nth fv_frees (body_index dt);
- (* TODO: check that pis have empty intersection *)
val pi = foldr1 add_perm rpis;
val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
+ val alpha_gen = Syntax.check_term lthy alpha_gen_pre
+ val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis;
+ val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"})
in
- Syntax.check_term lthy alpha_gen_pre
+ if length pi_supps > 1 then
+ HOLogic.mk_conj (alpha_gen, pi_supps_eq) else alpha_gen
(* TODO Add some test that is makes sense *)
end else @{term "True"}
end
@@ -200,7 +203,7 @@
val (fvs, lthy') = (Primrec.add_primrec
(map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy)
val (alphas, lthy'') = (Inductive.add_inductive_i
- {quiet_mode = false, verbose = true, alt_name = Binding.empty,
+ {quiet_mode = true, verbose = false, alt_name = Binding.empty,
coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
(map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) []
(add_binds alpha_eqs) [] lthy')
--- a/Nominal/Nominal2_Eqvt.thy Wed Mar 03 12:45:55 2010 +0100
+++ b/Nominal/Nominal2_Eqvt.thy Wed Mar 03 12:47:06 2010 +0100
@@ -239,7 +239,8 @@
imp_eqvt [folded induct_implies_def]
(* nominal *)
- permute_eqvt supp_eqvt fresh_eqvt
+ (*permute_eqvt commented out since it loops *)
+ supp_eqvt fresh_eqvt
permute_pure
(* datatypes *)
--- a/Nominal/Parser.thy Wed Mar 03 12:45:55 2010 +0100
+++ b/Nominal/Parser.thy Wed Mar 03 12:47:06 2010 +0100
@@ -231,7 +231,7 @@
Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;
val raw_binds_flat = map (map flat) raw_binds;
val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat lthy3;
-(* val alpha_ts_loc = #preds alpha
+ val alpha_ts_loc = #preds alpha
val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3;
val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc;
val alpha_induct_loc = #induct alpha
@@ -245,7 +245,7 @@
val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms
((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5;
- val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms
+(* val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms
(raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6;
val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
@@ -256,7 +256,7 @@
(map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_names ~~ all_typs) ~~ alpha_ts))
(ALLGOALS (resolve_tac alpha_equivp)) lthy6;*)
in
- ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
+ ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy6)
end
*}
--- a/Nominal/Test.thy Wed Mar 03 12:45:55 2010 +0100
+++ b/Nominal/Test.thy Wed Mar 03 12:47:06 2010 +0100
@@ -13,11 +13,53 @@
thm permute_weird_raw.simps[no_vars]
thm alpha_weird_raw.intros[no_vars]
thm fv_weird_raw.simps[no_vars]
+(* Potential problem: Is it correct that in the fv-function
+the first two terms are created? Should be ommitted. Also
+something wrong with the permutations. *)
-abbreviation "fv_weird \<equiv> fv_weird_raw"
-abbreviation "alpha_weird \<equiv> alpha_weird_raw"
+lemma "alpha_weird_raw a b \<Longrightarrow> alpha_weird_raw (p \<bullet> a) (p \<bullet> b)"
+apply (erule alpha_weird_raw.induct)
+defer
+apply (simp add: alpha_weird_raw.intros)
+apply (simp add: alpha_weird_raw.intros)
+apply (simp only: permute_weird_raw.simps)
+apply (rule alpha_weird_raw.intros)
+apply (erule exi[of _ _ "p"])
+apply (erule exi[of _ _ "p"])
+apply (erule exi[of _ _ "p"])
+apply (erule exi[of _ _ "p"])
+apply (erule conjE)+
+apply (rule conjI)
+apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"])
+apply (simp add: eqvts)
+apply (simp add: eqvts)
+apply (rule conjI)
+defer
+apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"])
+apply (simp add: eqvts)
+apply (simp add: eqvts)
+apply (rule conjI)
+defer
+apply (simp add: supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt)
+apply(simp add: alpha_gen.simps)
+apply(erule conjE)+
+ apply(rule conjI)
+ apply(rule_tac ?p1="- p" in permute_eq_iff[THEN iffD1])
+apply (simp add: eqvts)
+ apply(rule conjI)
+ apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1])
+apply (simp add: eqvts add_perm_eqvt)
+apply (simp add: permute_eqvt[symmetric])
+done
-(*
+primrec
+ fv_weird
+where
+ "fv_weird (WBind_raw x y p1 p2 p3) =
+ (fv_weird p1 - {atom x}) \<union> (fv_weird p2 - ({atom x} \<union> {atom y})) \<union> (fv_weird p3 - {atom y})"
+| "fv_weird (WV_raw x) = {atom x}"
+| "fv_weird (WP_raw p1 p2) = (fv_weird p1 \<union> fv_weird p2)"
+
inductive
alpha_weird
where
@@ -29,55 +71,38 @@
alpha_weird (WBind_raw x y w1 w2 w3) (WBind_raw xa ya w1a w2a w3a)"
| "x = xa \<Longrightarrow> alpha_weird (WV_raw x) (WV_raw xa)"
| "alpha_weird w2 w2a \<and> alpha_weird w1 w1a \<Longrightarrow> alpha_weird (WP_raw w1 w2) (WP_raw w1a w2a)"
-*)
+(*
abbreviation "WBind \<equiv> WBind_raw"
-abbreviation "WP \<equiv> WP_raw"
-abbreviation "WV \<equiv> WV_raw"
+abbreviation "WP \<equiv> WP_raw"
+abbreviation "WV \<equiv> WV_raw"
lemma test:
assumes a: "distinct [x, y, z]"
shows "alpha_weird (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y)))
(WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))"
-apply(rule_tac alpha_weird_raw.intros)
+apply(rule_tac alpha_weird.intros)
unfolding alpha_gen
using a
apply(simp)
apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply(rule conjI)
-apply(simp add: flip_def)
+apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
apply(simp add: fresh_star_def)
-defer
-apply(rule conjI)
-apply(simp)
-apply(rule alpha_weird_raw.intros)
-apply(simp add: alpha_weird_raw.intros(2))
-apply(simp add: fresh_star_def)
-apply(rule conjI)
-apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply(rule_tac x="0" in exI)
+apply(simp add: flip_def)
+apply(auto)
+prefer 2
+apply(rule alpha_weird.intros)
+apply(simp add: alpha_weird.intros(2))
+prefer 2
+apply(rule alpha_weird.intros)
+apply(simp add: alpha_weird.intros(2))
apply(simp)
-apply(rule alpha_weird_raw.intros)
-apply(simp add: alpha_weird_raw.intros(2))
-apply(rule conjI)
-apply(auto)[1]
-apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply(rule conjI)
-apply(simp add: flip_def)
-apply(auto)[1]
-defer
+apply(rule alpha_weird.intros)
apply(simp)
-apply(rule alpha_weird_raw.intros)
-apply(simp add: alpha_weird_raw.intros(2))
-apply(simp add: fresh_perm)
-defer
-apply(simp add: fresh_perm)
-apply(simp add: atom_eqvt)
-unfolding flip_def[symmetric]
+apply(simp add: alpha_gen)
+using a
apply(simp)
-done
-
-
+*)
text {* example 1 *}
@@ -219,14 +244,15 @@
(* example 4 from Terms.thy *)
-(* fv_eqvt does not work, we need to repaire defined permute functions...
-nominal_datatype trm4 =
+(* fv_eqvt does not work, we need to repaire defined permute functions
+ defined fv and defined alpha... *)
+(*nominal_datatype trm4 =
Vr4 "name"
| Ap4 "trm4" "trm4 list"
| Lm4 x::"name" t::"trm4" bind x in t
thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
-thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
+thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]*)
(* example 5 from Terms.thy *)