# HG changeset patch # User Christian Urban # Date 1267616826 -3600 # Node ID 8502c2ff3be5ed372bd7dc349dd7c452871eec94 # Parent 531dcebbf48364544f1fa9f5e8abb88631f3630d# Parent 4bc9278a808ddccbd28775fecd4b6b4a44a5e75b merged diff -r 531dcebbf483 -r 8502c2ff3be5 Nominal/Fv.thy --- 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 \ 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') diff -r 531dcebbf483 -r 8502c2ff3be5 Nominal/Nominal2_Eqvt.thy --- 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 *) diff -r 531dcebbf483 -r 8502c2ff3be5 Nominal/Parser.thy --- 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 *} diff -r 531dcebbf483 -r 8502c2ff3be5 Nominal/Test.thy --- 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 \ fv_weird_raw" -abbreviation "alpha_weird \ alpha_weird_raw" +lemma "alpha_weird_raw a b \ alpha_weird_raw (p \ a) (p \ 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}) \ (fv_weird p2 - ({atom x} \ {atom y})) \ (fv_weird p3 - {atom y})" +| "fv_weird (WV_raw x) = {atom x}" +| "fv_weird (WP_raw p1 p2) = (fv_weird p1 \ 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 \ alpha_weird (WV_raw x) (WV_raw xa)" | "alpha_weird w2 w2a \ alpha_weird w1 w1a \ alpha_weird (WP_raw w1 w2) (WP_raw w1a w2a)" -*) +(* abbreviation "WBind \ WBind_raw" -abbreviation "WP \ WP_raw" -abbreviation "WV \ WV_raw" +abbreviation "WP \ WP_raw" +abbreviation "WV \ 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 \ y)" in exI) -apply(rule conjI) -apply(simp add: flip_def) +apply(rule_tac x="(x \ 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 \ 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 \ 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 *)