--- a/Attic/Quot/Examples/FSet3.thy Mon Apr 19 09:59:32 2010 +0200
+++ b/Attic/Quot/Examples/FSet3.thy Mon Apr 19 10:00:52 2010 +0200
@@ -72,9 +72,13 @@
shows "[] \<approx> []"
by simp
-lemma cons_rsp[quot_respect]:
+lemma cons_rsp:
+ "xa \<approx> ya \<Longrightarrow> y # xa \<approx> y # ya"
+ by simp
+
+lemma [quot_respect]:
shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
-by simp
+ by simp
section {* Augmenting a set -- @{const finsert} *}
@@ -241,12 +245,6 @@
is
"concat"
-(*lemma fconcat_rsp[quot_respect]:
- shows "((list_rel op \<approx>) ===> op \<approx>) concat concat"
-apply(auto)
-sorry
-*)
-
(* PROBLEM: these lemmas needs to be restated, since *)
(* concat.simps(1) and concat.simps(2) contain the *)
(* type variables ?'a1.0 (which are turned into frees *)
@@ -257,11 +255,23 @@
lemma concat2:
shows "concat (x # xs) \<approx> x @ concat xs"
-by (simp add: id_simps)
+by (simp)
-lemma concat_rsp[quot_respect]:
+lemma concat_rsp:
+ "\<lbrakk>list_rel op \<approx> x x'; x' \<approx> y'; list_rel op \<approx> y' y\<rbrakk> \<Longrightarrow> concat x \<approx> concat y"
+ apply (induct x y arbitrary: x' y' rule: list_induct2')
+ apply simp
+ defer defer
+ apply (simp only: concat.simps)
+ sorry
+
+lemma [quot_respect]:
shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
-sorry
+ apply (simp only: fun_rel_def)
+ apply clarify
+ apply (rule concat_rsp)
+ apply assumption+
+ done
lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)
@@ -344,25 +354,29 @@
apply (metis equivp_def fset_equivp)
apply rule
apply rule
- apply(rule quotient_compose_list_pre)
+ apply (rule quotient_compose_list_pre)
done
lemma fconcat_empty:
shows "fconcat {||} = {||}"
-apply(lifting concat1)
-apply(cleaning)
-apply(simp add: comp_def)
-apply(fold fempty_def[simplified id_simps])
-apply(rule refl)
-done
-
-(* Should be true *)
+ apply(lifting concat1)
+ apply(cleaning)
+ apply(simp add: comp_def)
+ apply(fold fempty_def[simplified id_simps])
+ apply(rule refl)
+ done
lemma insert_rsp2[quot_respect]:
"(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #"
-apply auto
-apply (simp add: set_in_eq)
-sorry
+ apply auto
+ apply (simp add: set_in_eq)
+ apply (rule_tac b="x # b" in pred_compI)
+ apply auto
+ apply (rule_tac b="x # ba" in pred_compI)
+ apply (rule cons_rsp)
+ apply simp
+ apply (auto)[1]
+ done
lemma append_rsp[quot_respect]:
"(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
@@ -370,11 +384,11 @@
lemma fconcat_insert:
shows "fconcat (finsert x S) = x |\<union>| fconcat S"
-apply(lifting concat2)
-apply(cleaning)
-apply (simp add: finsert_def fconcat_def comp_def)
-apply cleaning
-done
+ apply(lifting concat2)
+ apply(cleaning)
+ apply (simp add: finsert_def fconcat_def comp_def)
+ apply cleaning
+ done
text {* raw section *}
@@ -699,19 +713,4 @@
lemma "funion (funion x xa) xb = funion x (funion xa xb)"
by (lifting append_assoc)
-quotient_definition
- "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
-is
- "list_case"
-
-(* NOT SURE IF TRUE *)
-lemma list_case_rsp[quot_respect]:
- "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
- apply (auto)
- sorry
-
-lemma "fset_case (f1::'t) f2 (finsert a xa) = f2 a xa"
-apply (lifting list.cases(2))
-done
-
end
--- a/Nominal-General/Nominal2_Base.thy Mon Apr 19 09:59:32 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy Mon Apr 19 10:00:52 2010 +0200
@@ -6,6 +6,7 @@
*)
theory Nominal2_Base
imports Main Infinite_Set
+uses ("nominal_library.ML")
begin
section {* Atoms and Sorts *}
@@ -1059,4 +1060,7 @@
by auto
qed
+(* nominal infrastructure *)
+use "nominal_library.ML"
+
end
--- a/Nominal-General/Nominal2_Eqvt.thy Mon Apr 19 09:59:32 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy Mon Apr 19 10:00:52 2010 +0200
@@ -2,16 +2,16 @@
Author: Brian Huffman,
Author: Christian Urban
- Equivariance, Supp and Fresh Lemmas for Operators.
- (Contains many, but not all such lemmas.)
+ Equivariance, supp and freshness lemmas for various operators
+ (contains many, but not all such lemmas).
*)
theory Nominal2_Eqvt
imports Nominal2_Base Nominal2_Atoms
uses ("nominal_thmdecls.ML")
("nominal_permeq.ML")
+ ("nominal_eqvt.ML")
begin
-
section {* Logical Operators *}
lemma eq_eqvt:
@@ -237,7 +237,7 @@
section {* Equivariance automation *}
-text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *}
+text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
use "nominal_thmdecls.ML"
setup "Nominal_ThmDecls.setup"
@@ -284,17 +284,25 @@
shows "p \<bullet> unpermute p x \<equiv> x"
unfolding unpermute_def by simp
+(* provides perm_simp methods *)
use "nominal_permeq.ML"
setup Nominal_Permeq.setup
+ML {*
+val test1 = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [];
+val test2 = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |--
+ (Scan.repeat (Args.const true))) []
+*}
+
method_setup perm_simp =
- {* Attrib.thms >>
- (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms ["The"]))) *}
+ {* test1 -- test2 >>
+ (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt [] consts))) *}
{* pushes permutations inside *}
method_setup perm_strict_simp =
- {* Attrib.thms >>
- (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_strict_tac ctxt thms ["The"]))) *}
+ {* test1 -- test2 >>
+ (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL
+ (Nominal_Permeq.eqvt_strict_tac ctxt thms consts))) *}
{* pushes permutations inside, raises an error if it cannot solve all permutations *}
declare [[trace_eqvt = true]]
@@ -367,148 +375,12 @@
text {* Problem: there is no raw eqvt-rule for The *}
lemma "p \<bullet> (THE x. P x) = foo"
-apply(perm_simp)
-(* apply(perm_strict_simp) *)
+apply(perm_strict_simp exclude: The)
+apply(perm_simp exclude: The)
oops
-atom_decl var
-
-ML {*
-val inductive_atomize = @{thms induct_atomize};
-
-val atomize_conv =
- MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE))
- (HOL_basic_ss addsimps inductive_atomize);
-val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
-fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
- (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
-
-fun map_term f t u = (case f t u of
- NONE => map_term' f t u | x => x)
-and map_term' f (t $ u) (t' $ u') = (case (map_term f t t', map_term f u u') of
- (NONE, NONE) => NONE
- | (SOME t'', NONE) => SOME (t'' $ u)
- | (NONE, SOME u'') => SOME (t $ u'')
- | (SOME t'', SOME u'') => SOME (t'' $ u''))
- | map_term' f (Abs (s, T, t)) (Abs (s', T', t')) = (case map_term f t t' of
- NONE => NONE
- | SOME t'' => SOME (Abs (s, T, t'')))
- | map_term' _ _ _ = NONE;
-
-
-fun map_thm ctxt f tac monos opt th =
- let
- val prop = prop_of th;
- fun prove t =
- Goal.prove ctxt [] [] t (fn _ =>
- EVERY [cut_facts_tac [th] 1, etac rev_mp 1,
- REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)),
- REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))])
- in Option.map prove (map_term f prop (the_default prop opt)) end;
-
-fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of
- Const (name, _) =>
- if name mem names then SOME (f p q) else NONE
- | _ => NONE)
- | split_conj _ _ _ _ = NONE;
-*}
-
-ML {*
-val perm_bool = @{thm "permute_bool_def"};
-val perm_boolI = @{thm "permute_boolI"};
-val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
- (Drule.strip_imp_concl (cprop_of perm_boolI))));
-
-fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
- [(perm_boolI_pi, pi)] perm_boolI;
-
-*}
-
-ML {*
-fun transp ([] :: _) = []
- | transp xs = map hd xs :: transp (map tl xs);
-
-fun prove_eqvt s xatoms ctxt =
- let
- val thy = ProofContext.theory_of ctxt;
- val ({names, ...}, {raw_induct, intrs, elims, ...}) =
- Inductive.the_inductive ctxt (Sign.intern_const thy s);
- val raw_induct = atomize_induct ctxt raw_induct;
- val elims = map (atomize_induct ctxt) elims;
- val intrs = map atomize_intr intrs;
- val monos = Inductive.get_monos ctxt;
- val intrs' = Inductive.unpartition_rules intrs
- (map (fn (((s, ths), (_, k)), th) =>
- (s, ths ~~ Inductive.infer_intro_vars th k ths))
- (Inductive.partition_rules raw_induct intrs ~~
- Inductive.arities_of raw_induct ~~ elims));
- val k = length (Inductive.params_of raw_induct);
- val atoms' = ["var"];
- val atoms =
- if null xatoms then atoms' else
- let val atoms = map (Sign.intern_type thy) xatoms
- in
- (case duplicates op = atoms of
- [] => ()
- | xs => error ("Duplicate atoms: " ^ commas xs);
- case subtract (op =) atoms' atoms of
- [] => ()
- | xs => error ("No such atoms: " ^ commas xs);
- atoms)
- end;
- val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
- val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps
- (Nominal_ThmDecls.get_eqvts_thms ctxt @ perm_pi_simp);
- val (([t], [pi]), ctxt') = ctxt |>
- Variable.import_terms false [concl_of raw_induct] ||>>
- Variable.variant_fixes ["pi"];
- val ps = map (fst o HOLogic.dest_imp)
- (HOLogic.dest_conj (HOLogic.dest_Trueprop t));
- fun eqvt_tac ctxt'' pi (intr, vs) st =
- let
- fun eqvt_err s =
- let val ([t], ctxt''') = Variable.import_terms true [prop_of intr] ctxt
- in error ("Could not prove equivariance for introduction rule\n" ^
- Syntax.string_of_term ctxt''' t ^ "\n" ^ s)
- end;
- val res = SUBPROOF (fn {prems, params, ...} =>
- let
- val prems' = map (fn th => the_default th (map_thm ctxt'
- (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems;
- val prems'' = map (fn th => Simplifier.simplify eqvt_ss
- (mk_perm_bool (cterm_of thy pi) th)) prems';
- val intr' = intr
- in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1
- end) ctxt' 1 st
- in
- case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of
- NONE => eqvt_err ("Rule does not match goal\n" ^
- Syntax.string_of_term ctxt'' (hd (prems_of st)))
- | SOME (th, _) => Seq.single th
- end;
- val thss = map (fn atom =>
- let val pi' = Free (pi, @{typ perm})
- in map (fn th => zero_var_indexes (th RS mp))
- (Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] []
- (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p =>
- let
- val (h, ts) = strip_comb p;
- val (ts1, ts2) = chop k ts
- in
- HOLogic.mk_imp (p, list_comb (h, ts1))
- end) ps)))
- (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>
- full_simp_tac eqvt_ss 1 THEN
- eqvt_tac context pi' intr_vs) intrs')) |>
- singleton (ProofContext.export ctxt' ctxt)))
- end) atoms
- in
- ctxt |>
- Local_Theory.notes (map (fn (name, ths) =>
- ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
- [Attrib.internal (K Nominal_ThmDecls.eqvt_add)]), [(ths, [])]))
- (names ~~ transp thss)) |> snd
- end;
-*}
+(* automatic equivariance procedure for
+ inductive definitions *)
+use "nominal_eqvt.ML"
end
--- a/Nominal-General/Nominal2_Supp.thy Mon Apr 19 09:59:32 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy Mon Apr 19 10:00:52 2010 +0200
@@ -68,7 +68,7 @@
unfolding fresh_star_def
by (metis mem_permute_iff permute_minus_cancel fresh_permute_iff)
-lemma fresh_star_eqvt:
+lemma fresh_star_eqvt[eqvt]:
shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)"
unfolding fresh_star_def
unfolding Ball_def
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal-General/nominal_eqvt.ML Mon Apr 19 10:00:52 2010 +0200
@@ -0,0 +1,178 @@
+(* Title: nominal_eqvt.ML
+ Author: Stefan Berghofer (original code)
+ Author: Christian Urban
+
+ Automatic proofs for equivariance of inductive predicates.
+*)
+
+signature NOMINAL_EQVT =
+sig
+ val equivariance: string -> Proof.context -> local_theory
+ val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic
+ val eqvt_rel_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic
+end
+
+structure Nominal_Eqvt : NOMINAL_EQVT =
+struct
+
+open Nominal_Permeq;
+open Nominal_ThmDecls;
+
+val atomize_conv =
+ MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE))
+ (HOL_basic_ss addsimps @{thms induct_atomize});
+val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
+fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
+ (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
+
+
+(**
+ proves F[f t] from F[t] which is the given theorem
+ - F needs to be monotone
+ - f returns either SOME for a term it fires
+ and NONE elsewhere
+**)
+fun map_term f t =
+ (case f t of
+ NONE => map_term' f t
+ | x => x)
+and map_term' f (t $ u) =
+ (case (map_term f t, map_term f u) of
+ (NONE, NONE) => NONE
+ | (SOME t'', NONE) => SOME (t'' $ u)
+ | (NONE, SOME u'') => SOME (t $ u'')
+ | (SOME t'', SOME u'') => SOME (t'' $ u''))
+ | map_term' f (Abs (s, T, t)) =
+ (case map_term f t of
+ NONE => NONE
+ | SOME t'' => SOME (Abs (s, T, t'')))
+ | map_term' _ _ = NONE;
+
+fun map_thm_tac ctxt tac thm =
+let
+ val monos = Inductive.get_monos ctxt
+in
+ EVERY [cut_facts_tac [thm] 1, etac rev_mp 1,
+ REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)),
+ REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]
+end
+
+fun map_thm ctxt f tac thm =
+let
+ val opt_goal_trm = map_term f (prop_of thm)
+in
+ case opt_goal_trm of
+ NONE => thm
+ | SOME goal =>
+ Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm)
+end
+
+(*
+ inductive premises can be of the form
+ R ... /\ P ...; split_conj picks out
+ the part P ...
+*)
+fun transform_prem ctxt names thm =
+let
+ fun split_conj names (Const ("op &", _) $ p $ q) =
+ (case head_of p of
+ Const (name, _) => if name mem names then SOME q else NONE
+ | _ => NONE)
+ | split_conj _ _ = NONE;
+in
+ map_thm ctxt (split_conj names) (etac conjunct2 1) thm
+end
+
+
+(** equivariance tactics **)
+
+val perm_boolE = @{thm permute_boolE}
+val perm_cancel = @{thms permute_minus_cancel(2)}
+val perm_expand_bool = @{thms permute_fun_def minus_minus permute_bool_def}
+
+fun eqvt_rel_case_tac ctxt pred_names pi intro =
+let
+ val thy = ProofContext.theory_of ctxt
+ val cpi = Thm.cterm_of thy (mk_minus pi)
+ val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE
+ val simps = HOL_basic_ss addsimps perm_expand_bool
+in
+ eqvt_strict_tac ctxt [] pred_names THEN'
+ SUBPROOF (fn {prems, context as ctxt, ...} =>
+ let
+ val prems' = map (transform_prem ctxt pred_names) prems
+ val tac1 = resolve_tac prems'
+ val tac2 = EVERY' [ rtac pi_intro_rule,
+ eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ]
+ val tac3 = EVERY' [ rtac pi_intro_rule,
+ eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps, resolve_tac prems']
+ in
+ (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1
+ end) ctxt
+end
+
+fun eqvt_rel_tac ctxt pred_names pi induct intros =
+let
+ val cases = map (eqvt_rel_case_tac ctxt pred_names pi) intros
+in
+ EVERY' (rtac induct :: cases)
+end
+
+
+(** equivariance procedure *)
+
+(* sets up goal and makes sure parameters
+ are untouched PROBLEM: this violates the
+ form of eqvt lemmas *)
+fun prepare_goal params_no pi pred =
+let
+ val (c, xs) = strip_comb pred;
+ val (xs1, xs2) = chop params_no xs
+in
+ HOLogic.mk_imp (pred, list_comb (c, xs1 @ map (mk_perm pi) xs2))
+end
+
+(* stores thm under name.eqvt and adds [eqvt]-attribute *)
+fun note_named_thm (name, thm) ctxt =
+let
+ val thm_name = Binding.qualified_name
+ (Long_Name.qualify (Long_Name.base_name name) "eqvt")
+ val attr = Attrib.internal (K eqvt_add)
+in
+ Local_Theory.note ((thm_name, [attr]), [thm]) ctxt
+end
+
+fun equivariance pred_name ctxt =
+let
+ val thy = ProofContext.theory_of ctxt
+ val ({names, ...}, {raw_induct, intrs, ...}) =
+ Inductive.the_inductive ctxt (Sign.intern_const thy pred_name)
+ val raw_induct = atomize_induct ctxt raw_induct
+ val intros = map atomize_intr intrs
+ val params_no = length (Inductive.params_of raw_induct)
+ val (([raw_concl], [raw_pi]), ctxt') = ctxt
+ |> Variable.import_terms false [concl_of raw_induct]
+ ||>> Variable.variant_fixes ["p"]
+ val pi = Free (raw_pi, @{typ perm})
+ val preds = map (fst o HOLogic.dest_imp)
+ (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl));
+ val goal = HOLogic.mk_Trueprop
+ (foldr1 HOLogic.mk_conj (map (prepare_goal params_no pi) preds))
+ val thms = Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] [] goal
+ (fn {context,...} => eqvt_rel_tac context names pi raw_induct intros 1)
+ |> singleton (ProofContext.export ctxt' ctxt))
+ val thms' = map (fn th => zero_var_indexes (th RS mp)) thms
+in
+ ctxt |> fold_map note_named_thm (names ~~ thms') |> snd
+end
+
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val _ =
+ OuterSyntax.local_theory "equivariance"
+ "prove equivariance for inductive predicate involving nominal datatypes"
+ K.thy_decl (P.xname >> equivariance);
+end;
+
+end (* structure *)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal-General/nominal_library.ML Mon Apr 19 10:00:52 2010 +0200
@@ -0,0 +1,38 @@
+(* Title: nominal_library.ML
+ Author: Christian Urban
+
+ Basic function for nominal.
+*)
+
+signature NOMINAL_LIBRARY =
+sig
+ val mk_minus: term -> term
+ val mk_perm_ty: typ -> term -> term -> term
+ val mk_perm: term -> term -> term
+ val dest_perm: term -> term * term
+
+ val mk_equiv: thm -> thm
+ val safe_mk_equiv: thm -> thm
+end
+
+
+structure Nominal_Library: NOMINAL_LIBRARY =
+struct
+
+fun mk_minus p =
+ Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p
+
+fun mk_perm_ty ty p trm =
+ Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm
+
+fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm
+
+fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
+ | dest_perm t = raise TERM ("dest_perm", [t])
+
+fun mk_equiv r = r RS @{thm eq_reflection};
+fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
+
+end (* structure *)
+
+open Nominal_Library;
\ No newline at end of file
--- a/Nominal-General/nominal_permeq.ML Mon Apr 19 09:59:32 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML Mon Apr 19 10:00:52 2010 +0200
@@ -106,11 +106,16 @@
(* conversion that raises an error or prints a warning message,
if a permutation on a constant or application cannot be analysed *)
-fun progress_info_conv ctxt strict_flag ctrm =
+fun progress_info_conv ctxt strict_flag bad_hds ctrm =
let
- fun msg trm =
- (if strict_flag then error else warning)
- ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
+ fun msg trm =
+ let
+ val hd = head_of trm
+ in
+ if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then ()
+ else (if strict_flag then error else warning)
+ ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
+ end
val _ = case (term_of ctrm) of
Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm
@@ -120,9 +125,6 @@
Conv.all_conv ctrm
end
-fun mk_equiv r = r RS @{thm eq_reflection};
-fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
-
(* main conversion *)
fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm =
let
@@ -139,7 +141,7 @@
eqvt_apply_conv bad_hds,
eqvt_lambda_conv,
More_Conv.rewrs_conv post_thms,
- progress_info_conv ctxt strict_flag
+ progress_info_conv ctxt strict_flag bad_hds
] ctrm
end
--- a/Nominal-General/nominal_thmdecls.ML Mon Apr 19 09:59:32 2010 +0200
+++ b/Nominal-General/nominal_thmdecls.ML Mon Apr 19 10:00:52 2010 +0200
@@ -33,12 +33,38 @@
val setup: theory -> theory
val get_eqvts_thms: Proof.context -> thm list
val get_eqvts_raw_thms: Proof.context -> thm list
+ val eqvt_transform: Proof.context -> thm -> thm
+ (* TEMPORARY FIX *)
+ val add_thm: thm -> Context.generic -> Context.generic
+ val add_raw_thm: thm -> Context.generic -> Context.generic
end;
structure Nominal_ThmDecls: NOMINAL_THMDECLS =
struct
+fun get_ps trm =
+ case trm of
+ Const (@{const_name permute}, _) $ p $ (Bound _) => raise TERM ("get_ps", [trm])
+ | Const (@{const_name permute}, _) $ p $ _ => [p]
+ | t $ u => get_ps t @ get_ps u
+ | Abs (_, _, t) => get_ps t
+ | _ => []
+
+fun put_p p trm =
+ case trm of
+ Bound _ => trm
+ | Const _ => trm
+ | t $ u => put_p p t $ put_p p u
+ | Abs (x, ty, t) => Abs (x, ty, put_p p t)
+ | _ => mk_perm p trm
+
+(* tests whether the lists of ps all agree, and that there is at least one p *)
+fun is_bad_list [] = true
+ | is_bad_list [_] = false
+ | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true
+
+
structure EqvtData = Generic_Data
( type T = thm Item_Net.T;
val empty = Thm.full_rules;
@@ -60,63 +86,62 @@
val add_thm = EqvtData.map o Item_Net.update;
val del_thm = EqvtData.map o Item_Net.remove;
-fun is_equiv (Const ("==", _) $ _ $ _) = true
- | is_equiv _ = false
-
fun add_raw_thm thm =
case prop_of thm of
- Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update thm)
+ Const ("==", _) $ _ $ _ =>
+ EqvtRawData.map (Item_Net.update (zero_var_indexes thm))
| _ => raise THM ("Theorem must be a meta-equality", 0, [thm])
val del_raw_thm = EqvtRawData.map o Item_Net.remove;
-fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
- | dest_perm t = raise TERM ("dest_perm", [t])
+
+(** transformation of eqvt lemmas **)
+
+
+(* transforms equations into the "p o c = c"-form
+ from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *)
-fun mk_perm p trm =
+fun eqvt_transform_eq_tac thm =
let
- val ty = fastype_of trm
+ val ss_thms = @{thms permute_minus_cancel permute_prod.simps split_paired_all}
in
- Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm
+ REPEAT o FIRST'
+ [CHANGED o simp_tac (HOL_basic_ss addsimps ss_thms),
+ rtac (thm RS @{thm trans}),
+ rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]
end
-fun eq_transform_tac thm = REPEAT o FIRST'
- [CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}),
- rtac (thm RS @{thm trans}),
- rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]
-
-(* transform equations into the "p o c = c"-form *)
-fun transform_eq ctxt thm =
+fun eqvt_transform_eq ctxt thm =
let
- val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))
- val (p, t) = dest_perm lhs
- val (c, args) = strip_comb t
- val (c', args') = strip_comb rhs
- val eargs = map Envir.eta_contract args
- val eargs' = map Envir.eta_contract args'
- val p_str = fst (fst (dest_Var p))
- val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c))
+ val ((p, t), rhs) = apfst dest_perm
+ (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)))
+ handle TERM _ => error "Eqvt lemma is not of the form p \<bullet> c... = c..."
+ val ps = get_ps rhs handle TERM _ => []
+ val (c, c') = (head_of t, head_of rhs)
in
if c <> c'
then error "Eqvt lemma is not of the right form (constants do not agree)"
- else if eargs' <> map (mk_perm p) eargs
+ else if is_bad_list (p::ps)
+ then error "Eqvt lemma is not of the right form (permutations do not agree)"
+ else if not (rhs aconv (put_p p t))
then error "Eqvt lemma is not of the right form (arguments do not agree)"
- else if args = []
- then thm
- else Goal.prove ctxt [p_str] [] goal
- (fn _ => eq_transform_tac thm 1)
+ else if is_Const t
+ then safe_mk_equiv thm
+ else
+ let
+ val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c))
+ val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
+ in
+ Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1)
+ |> singleton (ProofContext.export ctxt' ctxt)
+ |> safe_mk_equiv
+ end
end
+(* transforms equations into the "p o c = c"-form
+ from R x1 ...xn ==> R (p o x1) ... (p o xn) *)
-(* tests whether the lists of pis all agree, and that there is at least one p *)
-fun is_bad_list [] = true
- | is_bad_list [_] = false
- | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true
-
-fun mk_minus p =
- Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p
-
-fun imp_transform_tac thy p p' thm =
+fun eqvt_transform_imp_tac thy p p' thm =
let
val cp = Thm.cterm_of thy p
val cp' = Thm.cterm_of thy (mk_minus p')
@@ -127,56 +152,67 @@
rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp]
end
-fun transform_imp ctxt thm =
+fun eqvt_transform_imp ctxt thm =
let
val thy = ProofContext.theory_of ctxt
val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm))
- val (c, prem_args) = strip_comb prem
- val (c', concl_args) = strip_comb concl
- val ps = map (fst o dest_perm) concl_args handle TERM _ => []
+ val (c, c') = (head_of prem, head_of concl)
+ val ps = get_ps concl handle TERM _ => []
val p = try hd ps
in
if c <> c'
then error "Eqvt lemma is not of the right form (constants do not agree)"
else if is_bad_list ps
then error "Eqvt lemma is not of the right form (permutations do not agree)"
- else if concl_args <> map (mk_perm (the p)) prem_args
+ else if not (concl aconv (put_p (the p) prem))
then error "Eqvt lemma is not of the right form (arguments do not agree)"
else
let
- val prem' = Const (@{const_name "permute"}, @{typ "perm => bool => bool"}) $ (the p) $ prem
+ val prem' = mk_perm (the p) prem
val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl))
val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt
in
Goal.prove ctxt' [] [] goal'
- (fn _ => imp_transform_tac thy (the p) p' thm 1)
+ (fn _ => eqvt_transform_imp_tac thy (the p) p' thm 1)
|> singleton (ProofContext.export ctxt' ctxt)
- |> transform_eq ctxt
+ |> eqvt_transform_eq ctxt
end
end
-fun mk_equiv r = r RS @{thm eq_reflection};
-fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
+fun eqvt_transform ctxt thm =
+ case (prop_of thm) of
+ @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $
+ (Const (@{const_name "permute"}, _) $ _ $ _) $ _) =>
+ eqvt_transform_eq ctxt thm
+ | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) =>
+ eqvt_transform_imp ctxt thm
+ | _ => raise error "Only _ = _ and _ ==> _ cases are implemented."
+
+
+(** attributes **)
-fun transform addel_fun thm context =
-let
- val ctxt = Context.proof_of context
-in
- case (prop_of thm) of
- @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $
- (Const (@{const_name "permute"}, _) $ _ $ _) $ _) =>
- addel_fun (safe_mk_equiv (transform_eq ctxt thm)) context
- | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) =>
- addel_fun (safe_mk_equiv (transform_imp ctxt thm)) context
- | _ => raise error "Only _ = _ and _ ==> _ cases are implemented."
-end
+val eqvt_add = Thm.declaration_attribute
+ (fn thm => fn context =>
+ let
+ val thm' = eqvt_transform (Context.proof_of context) thm
+ in
+ context |> add_thm thm |> add_raw_thm thm'
+ end)
-val eqvt_add = Thm.declaration_attribute (fn thm => (add_thm thm) o (transform add_raw_thm thm));
-val eqvt_del = Thm.declaration_attribute (fn thm => (del_thm thm) o (transform del_raw_thm thm));
+val eqvt_del = Thm.declaration_attribute
+ (fn thm => fn context =>
+ let
+ val thm' = eqvt_transform (Context.proof_of context) thm
+ in
+ context |> del_thm thm |> del_raw_thm thm'
+ end)
val eqvt_raw_add = Thm.declaration_attribute add_raw_thm;
val eqvt_raw_del = Thm.declaration_attribute del_raw_thm;
+
+(** setup function **)
+
val setup =
Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del)
(cat_lines ["Declaration of equivariance lemmas - they will automtically be",
--- a/Nominal/Abs.thy Mon Apr 19 09:59:32 2010 +0200
+++ b/Nominal/Abs.thy Mon Apr 19 10:00:52 2010 +0200
@@ -397,6 +397,58 @@
section {* BELOW is stuff that may or may not be needed *}
+lemma
+ fixes t1 s1::"'a::fs"
+ and t2 s2::"'b::fs"
+ shows "Abs as (t1, t2) = Abs as (s1, s2) \<longrightarrow> (Abs as t1 = Abs as s1 \<and> Abs as t2 = Abs as s2)"
+apply(subst abs_eq_iff)
+apply(subst alphas_abs)
+apply(subst alphas)
+apply(rule impI)
+apply(erule exE)
+apply(simp add: supp_Pair)
+apply(simp add: Un_Diff)
+apply(simp add: fresh_star_union)
+apply(erule conjE)+
+apply(rule conjI)
+apply(rule trans)
+apply(rule sym)
+apply(rule_tac p="p" in supp_perm_eq)
+apply(simp add: supp_abs)
+apply(simp)
+apply(rule trans)
+apply(rule sym)
+apply(rule_tac p="p" in supp_perm_eq)
+apply(simp add: supp_abs)
+apply(simp)
+done
+
+
+
+(* support of concrete atom sets *)
+
+lemma
+ fixes t1 s1::"'a::fs"
+ and t2 s2::"'b::fs"
+ assumes asm: "finite as"
+ shows "(Abs as t1 = Abs as s1 \<and> Abs as t2 = Abs as s2) \<longrightarrow> Abs as (t1, t2) = Abs as (s1, s2)"
+apply(subst abs_eq_iff)
+apply(subst abs_eq_iff)
+apply(subst alphas_abs)
+apply(subst alphas_abs)
+apply(subst alphas)
+apply(subst alphas)
+apply(rule impI)
+apply(erule exE | erule conjE)+
+apply(simp add: abs_eq_iff)
+apply(simp add: alphas_abs)
+apply(simp add: alphas)
+apply(rule conjI)
+apply(simp add: supp_Pair Un_Diff)
+oops
+
+
+
(* support of concrete atom sets *)
lemma supp_atom_image:
@@ -762,8 +814,7 @@
by (simp_all add: fresh_plus_perm)
-(* PROBLEM: this should be the real eqvt lemma for the alphas *)
-lemma alpha_gen_real_eqvt:
+lemma alpha_gen_eqvt(*[eqvt]*):
shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
and "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
and "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)"
@@ -774,23 +825,6 @@
unfolding Diff_eqvt[symmetric]
by (auto simp add: permute_bool_def fresh_star_permute_iff)
-
-lemma alpha_gen_eqvt:
- assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
- and b: "p \<bullet> (f x) = f (p \<bullet> x)"
- and c: "p \<bullet> (f y) = f (p \<bullet> y)"
- shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
- and "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
- and "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst R f (p \<bullet> q) (p \<bullet> es, p \<bullet> y)"
- unfolding alphas
- unfolding set_eqvt[symmetric]
- unfolding b[symmetric] c[symmetric]
- unfolding Diff_eqvt[symmetric]
- unfolding permute_eqvt[symmetric]
- using a
- by (auto simp add: fresh_star_permute_iff)
-
-
lemma alpha_gen_simpler:
assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
and fin_fv: "finite (f x)"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Equivp.thy Mon Apr 19 10:00:52 2010 +0200
@@ -0,0 +1,367 @@
+theory Equivp
+imports "Fv"
+begin
+
+ML {*
+fun build_alpha_sym_trans_gl alphas (x, y, z) =
+let
+ fun build_alpha alpha =
+ let
+ val ty = domain_type (fastype_of alpha);
+ val var = Free(x, ty);
+ val var2 = Free(y, ty);
+ val var3 = Free(z, ty);
+ val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var);
+ val transp = HOLogic.mk_imp (alpha $ var $ var2,
+ HOLogic.mk_all (z, ty,
+ HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3)))
+ in
+ (symp, transp)
+ end;
+ val eqs = map build_alpha alphas
+ val (sym_eqs, trans_eqs) = split_list eqs
+ fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l
+in
+ (conj sym_eqs, conj trans_eqs)
+end
+*}
+
+ML {*
+fun build_alpha_refl_gl fv_alphas_lst alphas =
+let
+ val (fvs_alphas, _) = split_list fv_alphas_lst;
+ val (_, alpha_ts) = split_list fvs_alphas;
+ val tys = map (domain_type o fastype_of) alpha_ts;
+ val names = Datatype_Prop.make_tnames tys;
+ val args = map Free (names ~~ tys);
+ fun find_alphas ty x =
+ domain_type (fastype_of x) = ty;
+ fun refl_eq_arg (ty, arg) =
+ let
+ val rel_alphas = filter (find_alphas ty) alphas;
+ in
+ map (fn x => x $ arg $ arg) rel_alphas
+ end;
+ (* Flattening loses the induction structure *)
+ val eqs = map (foldr1 HOLogic.mk_conj) (map refl_eq_arg (tys ~~ args))
+in
+ (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs))
+end
+*}
+
+ML {*
+fun reflp_tac induct eq_iff =
+ rtac induct THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
+ split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
+ THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
+ @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv
+ add_0_left supp_zero_perm Int_empty_left split_conv})
+*}
+
+ML {*
+fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt =
+let
+ val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas;
+ val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff 1);
+in
+ HOLogic.conj_elims refl_conj
+end
+*}
+
+lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
+apply (erule exE)
+apply (rule_tac x="-pi" in exI)
+by auto
+
+ML {*
+fun symp_tac induct inj eqvt ctxt =
+ rel_indtac induct THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac
+ THEN_ALL_NEW
+ REPEAT o etac @{thm exi_neg}
+ THEN_ALL_NEW
+ split_conj_tac THEN_ALL_NEW
+ asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
+ TRY o (resolve_tac @{thms alphas_compose_sym2} ORELSE' resolve_tac @{thms alphas_compose_sym}) THEN_ALL_NEW
+ (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
+*}
+
+
+lemma exi_sum: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>pi. R pi"
+apply (erule exE)+
+apply (rule_tac x="pia + pi" in exI)
+by auto
+
+
+ML {*
+fun eetac rule =
+ Subgoal.FOCUS_PARAMS (fn focus =>
+ let
+ val concl = #concl focus
+ val prems = Logic.strip_imp_prems (term_of concl)
+ val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems
+ val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs
+ val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs
+ in
+ (etac rule THEN' RANGE[atac, eresolve_tac thins]) 1
+ end
+ )
+*}
+
+ML {*
+fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
+ rel_indtac induct THEN_ALL_NEW
+ (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
+ asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW
+ split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac
+ THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct)))
+ THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
+ TRY o (eresolve_tac @{thms alphas_compose_trans2} ORELSE' eresolve_tac @{thms alphas_compose_trans}) THEN_ALL_NEW
+ (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct)))
+*}
+
+lemma transpI:
+ "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R"
+ unfolding transp_def
+ by blast
+
+ML {*
+fun equivp_tac reflps symps transps =
+ (*let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in *)
+ simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
+ THEN' rtac conjI THEN' rtac allI THEN'
+ resolve_tac reflps THEN'
+ rtac conjI THEN' rtac allI THEN' rtac allI THEN'
+ resolve_tac symps THEN'
+ rtac @{thm transpI} THEN' resolve_tac transps
+*}
+
+ML {*
+fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =
+let
+ val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt;
+ val (symg, transg) = build_alpha_sym_trans_gl alphas (x, y, z)
+ fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1;
+ fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1;
+ val symp_loc = Goal.prove ctxt' [] [] symg symp_tac';
+ val transp_loc = Goal.prove ctxt' [] [] transg transp_tac';
+ val [symp, transp] = Variable.export ctxt' ctxt [symp_loc, transp_loc]
+ val symps = HOLogic.conj_elims symp
+ val transps = HOLogic.conj_elims transp
+ fun equivp alpha =
+ let
+ val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool})
+ val goal = @{term Trueprop} $ (equivp $ alpha)
+ fun tac _ = equivp_tac reflps symps transps 1
+ in
+ Goal.prove ctxt [] [] goal tac
+ end
+in
+ map equivp alphas
+end
+*}
+
+lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)"
+by auto
+
+ML {*
+fun supports_tac perm =
+ simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW (
+ REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conj_tac THEN'
+ asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric]
+ swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh
+ supp_fset_to_set supp_fmap_atom}))
+*}
+
+ML {*
+fun mk_supp ty x =
+ Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x
+*}
+
+ML {*
+fun mk_supports_eq thy cnstr =
+let
+ val (tys, ty) = (strip_type o fastype_of) cnstr
+ val names = Datatype_Prop.make_tnames tys
+ val frees = map Free (names ~~ tys)
+ val rhs = list_comb (cnstr, frees)
+
+ fun mk_supp_arg (x, ty) =
+ if is_atom thy ty then mk_supp @{typ atom} (mk_atom ty $ x) else
+ if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else
+ if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x)
+ else mk_supp ty x
+ val lhss = map mk_supp_arg (frees ~~ tys)
+ val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool})
+ val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs)
+in
+ (names, eq)
+end
+*}
+
+ML {*
+fun prove_supports ctxt perms cnst =
+let
+ val (names, eq) = mk_supports_eq (ProofContext.theory_of ctxt) cnst
+in
+ Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1)
+end
+*}
+
+ML {*
+fun mk_fs tys =
+let
+ val names = Datatype_Prop.make_tnames tys
+ val frees = map Free (names ~~ tys)
+ val supps = map2 mk_supp tys frees
+ val fin_supps = map (fn x => @{term "finite :: atom set \<Rightarrow> bool"} $ x) supps
+in
+ (names, HOLogic.mk_Trueprop (mk_conjl fin_supps))
+end
+*}
+
+ML {*
+fun fs_tac induct supports = rel_indtac induct THEN_ALL_NEW (
+ rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW
+ asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set
+ supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp})
+*}
+
+ML {*
+fun prove_fs ctxt induct supports tys =
+let
+ val (names, eq) = mk_fs tys
+in
+ Goal.prove ctxt names [] eq (fn _ => fs_tac induct supports 1)
+end
+*}
+
+ML {*
+fun mk_supp x = Const (@{const_name supp}, fastype_of x --> @{typ "atom set"}) $ x;
+
+fun mk_supp_neq arg (fv, alpha) =
+let
+ val collect = Const ("Collect", @{typ "(atom \<Rightarrow> bool) \<Rightarrow> atom \<Rightarrow> bool"});
+ val ty = fastype_of arg;
+ val perm = Const ("Nominal2_Base.pt_class.permute", @{typ perm} --> ty --> ty);
+ val finite = @{term "finite :: atom set \<Rightarrow> bool"}
+ val rhs = collect $ Abs ("a", @{typ atom},
+ HOLogic.mk_not (finite $
+ (collect $ Abs ("b", @{typ atom},
+ HOLogic.mk_not (alpha $ (perm $ (@{term swap} $ Bound 1 $ Bound 0) $ arg) $ arg)))))
+in
+ HOLogic.mk_eq (fv $ arg, rhs)
+end;
+
+fun supp_eq fv_alphas_lst =
+let
+ val (fvs_alphas, ls) = split_list fv_alphas_lst;
+ val (fv_ts, _) = split_list fvs_alphas;
+ val tys = map (domain_type o fastype_of) fv_ts;
+ val names = Datatype_Prop.make_tnames tys;
+ val args = map Free (names ~~ tys);
+ fun supp_eq_arg ((fv, arg), l) =
+ mk_conjl
+ ((HOLogic.mk_eq (fv $ arg, mk_supp arg)) ::
+ (map (mk_supp_neq arg) l))
+ val eqs = mk_conjl (map supp_eq_arg ((fv_ts ~~ args) ~~ ls))
+in
+ (names, HOLogic.mk_Trueprop eqs)
+end
+*}
+
+ML {*
+fun combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos =
+if length fv_ts_bn < length alpha_ts_bn then
+ (fv_ts_nobn ~~ alpha_ts_nobn) ~~ (replicate (length fv_ts_nobn) [])
+else let
+ val fv_alpha_nos = 0 upto (length fv_ts_nobn - 1);
+ fun filter_fn i (x, j) = if j = i then SOME x else NONE;
+ val fv_alpha_bn_nos = (fv_ts_bn ~~ alpha_ts_bn) ~~ bn_nos;
+ val fv_alpha_bn_all = map (fn i => map_filter (filter_fn i) fv_alpha_bn_nos) fv_alpha_nos;
+in
+ (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all
+end
+*}
+
+(* TODO: this is a hack, it assumes that only one type of Abs's is present
+ in the type and chooses this supp_abs. Additionally single atoms are
+ treated properly. *)
+ML {*
+fun choose_alpha_abs eqiff =
+let
+ fun exists_subterms f ts = true mem (map (exists_subterm f) ts);
+ val terms = map prop_of eqiff;
+ fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms
+ val no =
+ if check @{const_name alpha_lst} then 2 else
+ if check @{const_name alpha_res} then 1 else
+ if check @{const_name alpha_gen} then 0 else
+ error "Failure choosing supp_abs"
+in
+ nth @{thms supp_abs[symmetric]} no
+end
+*}
+lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}"
+by (rule supp_abs(1))
+
+lemma supp_abs_sum:
+ "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
+ "supp (Abs_res x (a :: 'a :: fs)) \<union> supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))"
+ "supp (Abs_lst y (a :: 'a :: fs)) \<union> supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))"
+ apply (simp_all add: supp_abs supp_Pair)
+ apply blast+
+ done
+
+
+ML {*
+fun supp_eq_tac ind fv perm eqiff ctxt =
+ rel_indtac ind THEN_ALL_NEW
+ asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
+ asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW
+ asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps @{thms alphas3 alphas2}) THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW
+ asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
+ asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW
+ simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW
+ simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI})
+*}
+
+
+
+ML {*
+fun build_eqvt_gl pi frees fnctn ctxt =
+let
+ val typ = domain_type (fastype_of fnctn);
+ val arg = the (AList.lookup (op=) frees typ);
+in
+ ([HOLogic.mk_eq ((perm_arg (fnctn $ arg) $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt)
+end
+*}
+
+ML {*
+fun prove_eqvt tys ind simps funs ctxt =
+let
+ val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt;
+ val pi = Free (pi, @{typ perm});
+ val tac = asm_full_simp_tac (HOL_ss addsimps (@{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt'))
+ val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt'
+ val ths = Variable.export ctxt' ctxt ths_loc
+ val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)
+in
+ (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt))
+end
+*}
+
+end
--- a/Nominal/Ex/Classical.thy Mon Apr 19 09:59:32 2010 +0200
+++ b/Nominal/Ex/Classical.thy Mon Apr 19 10:00:52 2010 +0200
@@ -63,6 +63,14 @@
alpha (ImpR_raw coname1 name trm_raw coname2)
(ImpR_raw coname1a namea trm_rawa coname2a)"
+thm alpha.intros
+
+declare permute_trm_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha
+thm eqvts_raw
+
end
--- a/Nominal/Ex/ExCoreHaskell.thy Mon Apr 19 09:59:32 2010 +0200
+++ b/Nominal/Ex/ExCoreHaskell.thy Mon Apr 19 10:00:52 2010 +0200
@@ -5,9 +5,11 @@
(* core haskell *)
ML {* val _ = recursive := false *}
-(* this should not be a raw equivariant rule *)
-declare permute_pure[eqvt]
-
+(* this should not be an equivariance rule *)
+(* for the moment, we force it to be *)
+setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
+thm eqvts
+(*declare permute_pure[eqvt]*)
atom_decl var
atom_decl cvar
@@ -677,5 +679,18 @@
ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
qed
+section {* test about equivariance for alpha *}
+
+thm eqvts
+thm eqvts_raw
+
+declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_tkind_raw
+
+thm eqvts
+thm eqvts_raw
+
end
--- a/Nominal/Ex/Lambda.thy Mon Apr 19 09:59:32 2010 +0200
+++ b/Nominal/Ex/Lambda.thy Mon Apr 19 10:00:52 2010 +0200
@@ -9,6 +9,8 @@
| App "lam" "lam"
| Lam x::"name" l::"lam" bind x in l
+thm lam.fv
+thm lam.supp
lemmas supp_fn' = lam.fv[simplified lam.supp]
declare lam.perm[eqvt]
@@ -120,174 +122,94 @@
"valid []"
| "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T)#Gamma)"
-ML {*
-fun my_tac ctxt intros =
- Nominal_Permeq.eqvt_strict_tac ctxt [] []
- THEN' resolve_tac intros
- THEN_ALL_NEW
- (atac ORELSE'
- EVERY'
- [ rtac (Drule.instantiate' [] [SOME @{cterm "- p::perm"}] @{thm permute_boolE}),
- Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel(2)} [],
- atac ])
-*}
-
-lemma [eqvt]:
- assumes a: "valid Gamma"
- shows "valid (p \<bullet> Gamma)"
-using a
-apply(induct)
-apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
-apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
-done
-
-lemma
- shows "valid Gamma \<longrightarrow> valid (p \<bullet> Gamma)"
-ML_prf {*
-val ({names, ...}, {raw_induct, intrs, elims, ...}) =
- Inductive.the_inductive @{context} (Sign.intern_const @{theory} "valid")
-*}
-apply(tactic {* rtac raw_induct 1 *})
-apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
-apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
-done
-
-
-thm eqvts
-thm eqvts_raw
-
inductive
typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60)
where
t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
- | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
+ | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<or> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
| t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"
-
-ML {* Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing") *}
-
-lemma
- shows "Gamma \<turnstile> t : T \<longrightarrow> (p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"
-ML_prf {*
-val ({names, ...}, {raw_induct, intrs, elims, ...}) =
- Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing")
-*}
-apply(tactic {* rtac raw_induct 1 *})
-apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
-apply(perm_strict_simp)
-apply(rule typing.intros)
-oops
+inductive
+ typing' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<Turnstile> _ : _" [60,60,60] 60)
+where
+ t'_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> Var x : T"
+ | t'_App[intro]: "\<lbrakk>\<Gamma> \<Turnstile> t1 : T1\<rightarrow>T2 \<and> \<Gamma> \<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> App t1 t2 : T2"
+ | t'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> \<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> Lam x t : T1\<rightarrow>T2"
-lemma uu[eqvt]:
- assumes a: "Gamma \<turnstile> t : T"
- shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"
-using a
-apply(induct)
-apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
-apply(perm_strict_simp)
-apply(rule typing.intros)
-apply(rule conj_mono[THEN mp])
-prefer 3
-apply(assumption)
-apply(rule impI)
-prefer 2
-apply(rule impI)
-apply(simp)
-apply(auto)[1]
-apply(simp)
-apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
-done
-
-(*
inductive
- typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60)
+ typing2' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ 2\<Turnstile> _ : _" [60,60,60] 60)
where
- t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
- | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<and> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
- | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"
-
-lemma uu[eqvt]:
- assumes a: "Gamma \<turnstile> t : T"
- shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"
-using a
-apply(induct)
-apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
-apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
-apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
-done
-*)
-
-ML {*
-val inductive_atomize = @{thms induct_atomize};
+ t2'_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> Var x : T"
+ | t2'_App[intro]: "\<lbrakk>\<Gamma> 2\<Turnstile> t1 : T1\<rightarrow>T2 \<or> \<Gamma> 2\<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> App t1 t2 : T2"
+ | t2'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> 2\<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> Lam x t : T1\<rightarrow>T2"
-val atomize_conv =
- MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE))
- (HOL_basic_ss addsimps inductive_atomize);
-val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
-fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
- (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
-*}
-
-ML {*
-val ({names, ...}, {raw_induct, intrs, elims, ...}) =
- Inductive.the_inductive @{context} (Sign.intern_const @{theory} "typing")
-*}
+inductive
+ typing'' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ |\<Turnstile> _ : _" [60,60,60] 60)
+and valid' :: "(name\<times>ty) list \<Rightarrow> bool"
+where
+ v1[intro]: "valid' []"
+ | v2[intro]: "\<lbrakk>valid' \<Gamma>;atom x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid' ((x,T)#\<Gamma>)"
+ | t'_Var[intro]: "\<lbrakk>valid' \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Var x : T"
+ | t'_App[intro]: "\<lbrakk>\<Gamma> |\<Turnstile> t1 : T1\<rightarrow>T2; \<Gamma> |\<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> App t1 t2 : T2"
+ | t'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> |\<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Lam x t : T1\<rightarrow>T2"
-ML {* val ind_params = Inductive.params_of raw_induct *}
-ML {* val raw_induct = atomize_induct @{context} raw_induct; *}
-ML {* val elims = map (atomize_induct @{context}) elims; *}
-ML {* val monos = Inductive.get_monos @{context}; *}
+equivariance valid
+equivariance typing
+equivariance typing'
+equivariance typing2'
+equivariance typing''
-lemma
- shows "Gamma \<turnstile> t : T \<longrightarrow> (p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"
-apply(tactic {* rtac raw_induct 1 *})
-apply(tactic {* my_tac @{context} intrs 1 *})
-apply(perm_strict_simp)
-apply(rule typing.intros)
-oops
-
-
+thm valid.eqvt
+thm typing.eqvt
thm eqvts
thm eqvts_raw
-declare permute_lam_raw.simps[eqvt]
-thm alpha_gen_real_eqvt
-(*declare alpha_gen_real_eqvt[eqvt]*)
-lemma
- assumes a: "alpha_lam_raw t1 t2"
- shows "alpha_lam_raw (p \<bullet> t1) (p \<bullet> t2)"
-using a
-apply(induct)
-apply(tactic {* my_tac @{context} @{thms alpha_lam_raw.intros} 1 *})
-oops
+inductive
+ tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
+ for r :: "('a \<Rightarrow> 'a \<Rightarrow> bool)"
+where
+ aa: "tt r a a"
+ | bb: "tt r a b ==> tt r a c"
-thm alpha_lam_raw.intros[no_vars]
+(* PROBLEM: derived eqvt-theorem does not conform with [eqvt]
+equivariance tt
+*)
+
inductive
alpha_lam_raw'
where
- "name = namea \<Longrightarrow> alpha_lam_raw' (Var_raw name) (Var_raw namea)"
-| "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow>
+ a1: "name = namea \<Longrightarrow> alpha_lam_raw' (Var_raw name) (Var_raw namea)"
+| a2: "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow>
alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)"
-| "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>
+| a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw' fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>
alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"
+declare permute_lam_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+equivariance alpha_lam_raw'
+thm eqvts_raw
+
+
+
+(* HERE *)
+
lemma
assumes a: "alpha_lam_raw' t1 t2"
shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)"
using a
apply(induct)
-apply(tactic {* my_tac @{context} @{thms alpha_lam_raw'.intros} 1 *})
-apply(tactic {* my_tac @{context} @{thms alpha_lam_raw'.intros} 1 *})
-apply(perm_strict_simp)
-apply(rule alpha_lam_raw'.intros)
-apply(simp add: alphas)
-apply(rule_tac p="- p" in permute_boolE)
-apply(perm_simp permute_minus_cancel(2))
+apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac
+ @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a1} 1*})
+apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac
+ @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a2} 1*})
+(*
+apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac
+ @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a3} 1*})
+*)
oops
-
section {* size function *}
lemma size_eqvt_raw:
--- a/Nominal/FSet.thy Mon Apr 19 09:59:32 2010 +0200
+++ b/Nominal/FSet.thy Mon Apr 19 10:00:52 2010 +0200
@@ -23,7 +23,7 @@
'a fset = "'a list" / "list_eq"
by (rule list_eq_equivp)
-section {* empty fset, finsert and membership *}
+section {* Empty fset, Finsert and Membership *}
quotient_definition
fempty ("{||}")
@@ -55,7 +55,7 @@
abbreviation
fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
where
- "x |\<notin>| S \<equiv> \<not>(x |\<in>| S)"
+ "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
lemma memb_rsp[quot_respect]:
shows "(op = ===> op \<approx> ===> op =) memb memb"
@@ -72,13 +72,12 @@
section {* Augmenting an fset -- @{const finsert} *}
lemma nil_not_cons:
- shows
- "\<not> ([] \<approx> x # xs)"
- "\<not> (x # xs \<approx> [])"
+ shows "\<not> ([] \<approx> x # xs)"
+ and "\<not> (x # xs \<approx> [])"
by auto
lemma not_memb_nil:
- "\<not> memb x []"
+ shows "\<not> memb x []"
by (simp add: memb_def)
lemma memb_cons_iff:
@@ -103,7 +102,7 @@
shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
by (simp add: id_simps) auto
-section {* Union *}
+section {* Unions *}
quotient_definition
funion (infixl "|\<union>|" 65)
@@ -126,77 +125,41 @@
"fcard_raw"
lemma fcard_raw_0:
- fixes xs :: "'a list"
- shows "(fcard_raw xs = 0) = (xs \<approx> [])"
+ shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
by (induct xs) (auto simp add: memb_def)
lemma fcard_raw_gt_0:
assumes a: "x \<in> set xs"
shows "0 < fcard_raw xs"
- using a
- by (induct xs) (auto simp add: memb_def)
+ using a by (induct xs) (auto simp add: memb_def)
lemma fcard_raw_not_memb:
- fixes x :: "'a"
- shows "\<not>(memb x xs) \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)"
+ shows "\<not> memb x xs \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)"
by auto
lemma fcard_raw_suc:
- fixes xs :: "'a list"
- assumes c: "fcard_raw xs = Suc n"
- shows "\<exists>x ys. \<not>(memb x ys) \<and> xs \<approx> (x # ys) \<and> fcard_raw ys = n"
- unfolding memb_def
- using c
- proof (induct xs)
- case Nil
- then show ?case by simp
- next
- case (Cons a xs)
- have f1: "fcard_raw xs = Suc n \<Longrightarrow> \<exists>a ys. a \<notin> set ys \<and> xs \<approx> a # ys \<and> fcard_raw ys = n" by fact
- have f2: "fcard_raw (a # xs) = Suc n" by fact
- then show ?case proof (cases "a \<in> set xs")
- case True
- then show ?thesis using f1 f2 apply -
- apply (simp add: memb_def)
- apply clarify
- by metis
- next
- case False
- then show ?thesis using f1 f2 apply -
- apply (rule_tac x="a" in exI)
- apply (rule_tac x="xs" in exI)
- apply (simp add: memb_def)
- done
- qed
- qed
+ assumes a: "fcard_raw xs = Suc n"
+ shows "\<exists>x ys. \<not> (memb x ys) \<and> xs \<approx> (x # ys) \<and> fcard_raw ys = n"
+ using a
+ by (induct xs) (auto simp add: memb_def split: if_splits)
lemma singleton_fcard_1:
- shows "set xs = {x} \<Longrightarrow> fcard_raw xs = Suc 0"
- apply (induct xs)
- apply simp_all
- apply auto
- apply (subgoal_tac "set xs = {x}")
- apply simp
- apply (simp add: memb_def)
- apply auto
- apply (subgoal_tac "set xs = {}")
- apply simp
- by (metis memb_def subset_empty subset_insert)
+ shows "set xs = {x} \<Longrightarrow> fcard_raw xs = 1"
+ by (induct xs) (auto simp add: memb_def subset_insert)
lemma fcard_raw_1:
- fixes a :: "'a list"
shows "fcard_raw xs = 1 \<longleftrightarrow> (\<exists>x. xs \<approx> [x])"
apply (auto dest!: fcard_raw_suc)
apply (simp add: fcard_raw_0)
apply (rule_tac x="x" in exI)
apply simp
apply (subgoal_tac "set xs = {x}")
- apply (erule singleton_fcard_1)
+ apply (drule singleton_fcard_1)
apply auto
done
lemma fcard_raw_delete_one:
- "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
+ shows "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)
lemma fcard_raw_rsp_aux:
@@ -212,7 +175,7 @@
done
lemma fcard_raw_rsp[quot_respect]:
- "(op \<approx> ===> op =) fcard_raw fcard_raw"
+ shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
by (simp add: fcard_raw_rsp_aux)
@@ -268,6 +231,8 @@
apply (auto simp add: memb_def)
done
+section {* deletion *}
+
fun
delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
where
@@ -279,7 +244,7 @@
by (induct xs arbitrary: x y) (auto simp add: memb_def)
lemma delete_raw_rsp:
- "l \<approx> r \<Longrightarrow> delete_raw l x \<approx> delete_raw r x"
+ "xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x"
by (simp add: memb_def[symmetric] memb_delete_raw)
lemma [quot_respect]:
@@ -287,11 +252,11 @@
by (simp add: memb_def[symmetric] memb_delete_raw)
lemma memb_delete_raw_ident:
- "\<not> memb x (delete_raw xs x)"
+ shows "\<not> memb x (delete_raw xs x)"
by (induct xs) (auto simp add: memb_def)
lemma not_memb_delete_raw_ident:
- "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
+ shows "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
by (induct xs) (auto simp add: memb_def)
lemma fset_raw_delete_raw_cases:
@@ -509,14 +474,15 @@
by (lifting fcard_raw_0)
lemma fcard_1:
- fixes S::"'b fset"
shows "(fcard S = 1) = (\<exists>x. S = {|x|})"
by (lifting fcard_raw_1)
-lemma fcard_gt_0: "x \<in> fset_to_set S \<Longrightarrow> 0 < fcard S"
+lemma fcard_gt_0:
+ shows "x \<in> fset_to_set S \<Longrightarrow> 0 < fcard S"
by (lifting fcard_raw_gt_0)
-lemma fcard_not_fin: "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
+lemma fcard_not_fin:
+ shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
by (lifting fcard_raw_not_memb)
lemma fcard_suc: "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"
@@ -529,16 +495,16 @@
text {* funion *}
lemma funion_simps[simp]:
- "{||} |\<union>| S = S"
- "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
+ shows "{||} |\<union>| S = S"
+ and "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
by (lifting append.simps)
lemma funion_sym:
- "S |\<union>| T = T |\<union>| S"
+ shows "S |\<union>| T = T |\<union>| S"
by (lifting funion_sym_pre)
lemma funion_assoc:
- "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)"
+ shows "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)"
by (lifting append_assoc)
section {* Induction and Cases rules for finite sets *}
--- a/Nominal/Fv.thy Mon Apr 19 09:59:32 2010 +0200
+++ b/Nominal/Fv.thy Mon Apr 19 10:00:52 2010 +0200
@@ -287,7 +287,6 @@
*}
(* We assume no bindings in the type on which bn is defined *)
-(* TODO: currently works only with current fv_bn function *)
ML {*
fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn (fvbn, (bn, ith_dtyp, args_in_bns)) =
let
@@ -416,9 +415,8 @@
Const (@{const_name set}, @{typ "atom list \<Rightarrow> atom set"}) $ x else x
*}
-(* TODO: Notice datatypes without bindings and replace alpha with equality *)
ML {*
-fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy =
+fun define_fv (dt_info : Datatype_Aux.info) bindsall bns lthy =
let
val thy = ProofContext.theory_of lthy;
val {descr, sorts, ...} = dt_info;
@@ -436,18 +434,8 @@
val (bn_fv_bns, fv_bn_names_eqs) = fv_bns thy dt_info fv_frees rel_bns;
val fvbns = map snd bn_fv_bns;
val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs;
- val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
- "alpha_" ^ name_of_typ (nth_dtyp i)) descr);
- val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;
- val alpha_frees = map Free (alpha_names ~~ alpha_types);
- (* We assume that a bn is either recursive or not *)
- val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns;
- val (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) =
- alpha_bns dt_info alpha_frees bns bns_rec
- val alpha_bn_frees = map snd bn_alpha_bns;
- val alpha_bn_types = map fastype_of alpha_bn_frees;
- fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =
+ fun fv_constr ith_dtyp (cname, dts) bindcs =
let
val Ts = map (typ_of_dtyp descr sorts) dts;
val bindslen = length bindcs
@@ -459,21 +447,17 @@
val bindcs = map fst bind_pis;
val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts);
val args = map Free (names ~~ Ts);
- val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts);
- val args2 = map Free (names2 ~~ Ts);
val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
val fv_c = nth fv_frees ith_dtyp;
- val alpha = nth alpha_frees ith_dtyp;
val arg_nos = 0 upto (length dts - 1)
fun fv_bind args (NONE, i, _, _) =
if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else
if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else
if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atom_set (nth args i) else
if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (nth args i) else
- (* TODO we do not know what to do with non-atomizable things *)
+ (* TODO goes the code for preiously defined nominal datatypes *)
@{term "{} :: atom set"}
| fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i)
- fun fv_binds args relevant = mk_union (map (fv_bind args) relevant)
fun fv_binds_as_set args relevant = mk_union (map (setify o fv_bind args) relevant)
fun find_nonrec_binder j (SOME (f, false), i, _, _) = if i = j then SOME f else NONE
| find_nonrec_binder _ _ = NONE
@@ -490,7 +474,7 @@
if ((is_atom thy) o fastype_of) x then mk_single_atom x else
if ((is_atom_set thy) o fastype_of) x then mk_atom_set x else
if ((is_atom_fset thy) o fastype_of) x then mk_atom_fset x else
- (* TODO we do not know what to do with non-atomizable things *)
+ (* TODO goes the code for preiously defined nominal datatypes *)
@{term "{} :: atom set"};
(* If i = j then we generate it only once *)
val relevant = filter (fn (_, i, j, _) => ((i = arg_no) orelse (j = arg_no))) bindcs;
@@ -500,6 +484,81 @@
end;
val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq
(fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos))))
+ in
+ fv_eq
+ end;
+ fun fv_eq (i, (_, _, constrs)) binds = map2i (fv_constr i) constrs binds;
+ val fveqs = map2i fv_eq descr (gather_binds bindsall)
+ val fv_eqs_perfv = fveqs
+ val rel_bns_nos = map (fn (_, i, _) => i) rel_bns;
+ fun filter_fun (_, b) = b mem rel_bns_nos;
+ val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1))
+ val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs)))
+ val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs)))
+ val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs);
+ val fv_names_all = fv_names_fst @ fv_bn_names;
+ val add_binds = map (fn x => (Attrib.empty_binding, x))
+(* Function_Fun.add_fun Function_Common.default_config ... true *)
+ val (fvs, lthy') = (Primrec.add_primrec
+ (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy)
+ val (fvs2, lthy'') =
+ if fv_eqs_snd = [] then (([], []), lthy') else
+ (Primrec.add_primrec
+ (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_snd) (add_binds fv_eqs_snd) lthy')
+ val ordered_fvs = fv_frees @ fvbns;
+ val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2)
+in
+ ((all_fvs, ordered_fvs), lthy'')
+end
+*}
+
+ML {*
+fun define_alpha (dt_info : Datatype_Aux.info) bindsall bns fv_frees lthy =
+let
+ val thy = ProofContext.theory_of lthy;
+ val {descr, sorts, ...} = dt_info;
+ fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+(* TODO: We need a transitive closure, but instead we do this hack considering
+ all binding functions as recursive or not *)
+ val nr_bns =
+ if (non_rec_binds bindsall) = [] then []
+ else map (fn (bn, _, _) => bn) bns;
+ val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
+ "alpha_" ^ name_of_typ (nth_dtyp i)) descr);
+ val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;
+ val alpha_frees = map Free (alpha_names ~~ alpha_types);
+ (* We assume that a bn is either recursive or not *)
+ val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns;
+ val (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) =
+ alpha_bns dt_info alpha_frees bns bns_rec
+ val alpha_bn_frees = map snd bn_alpha_bns;
+ val alpha_bn_types = map fastype_of alpha_bn_frees;
+
+ fun alpha_constr ith_dtyp (cname, dts) bindcs =
+ let
+ val Ts = map (typ_of_dtyp descr sorts) dts;
+ val bindslen = length bindcs
+ val pi_strs_same = replicate bindslen "pi"
+ val pi_strs = Name.variant_list [] pi_strs_same;
+ val pis = map (fn ps => Free (ps, @{typ perm})) pi_strs;
+ val bind_pis_gath = bindcs ~~ pis;
+ val bind_pis = un_gather_binds_cons bind_pis_gath;
+ val names = Name.variant_list pi_strs (Datatype_Prop.make_tnames Ts);
+ val args = map Free (names ~~ Ts);
+ val names2 = Name.variant_list (pi_strs @ names) (Datatype_Prop.make_tnames Ts);
+ val args2 = map Free (names2 ~~ Ts);
+ val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
+ val alpha = nth alpha_frees ith_dtyp;
+ val arg_nos = 0 upto (length dts - 1)
+ fun fv_bind args (NONE, i, _, _) =
+ if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else
+ if ((is_atom thy) o fastype_of) (nth args i) then mk_single_atom (nth args i) else
+ if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atom_set (nth args i) else
+ if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (nth args i) else
+ (* TODO goes the code for preiously defined nominal datatypes *)
+ @{term "{} :: atom set"}
+ | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i)
+ fun fv_binds args relevant = mk_union (map (fv_bind args) relevant)
val alpha_rhs =
HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)));
fun alpha_arg ((dt, arg_no), (arg, arg2)) =
@@ -574,400 +633,20 @@
fold (fn pi_str => fn t => HOLogic.mk_exists (pi_str, @{typ perm}, t)) pi_strs alpha_lhss
val alpha_eq = Logic.mk_implies (HOLogic.mk_Trueprop alpha_lhss_ex, alpha_rhs)
in
- (fv_eq, alpha_eq)
+ alpha_eq
end;
- fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds;
- val fveqs_alphaeqs = map2i fv_alpha_eq descr (gather_binds bindsall)
- val (fv_eqs_perfv, alpha_eqs) = apsnd flat (split_list (map split_list fveqs_alphaeqs))
- val rel_bns_nos = map (fn (_, i, _) => i) rel_bns;
- fun filter_fun (_, b) = b mem rel_bns_nos;
- val all_fvs = (fv_names ~~ fv_eqs_perfv) ~~ (0 upto (length fv_names - 1))
- val (fv_names_fst, fv_eqs_fst) = apsnd flat (split_list (map fst (filter_out filter_fun all_fvs)))
- val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs)))
- val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs);
- val fv_names_all = fv_names_fst @ fv_bn_names;
+ fun alpha_eq (i, (_, _, constrs)) binds = map2i (alpha_constr i) constrs binds;
+ val alphaeqs = map2i alpha_eq descr (gather_binds bindsall)
+ val alpha_eqs = flat alphaeqs
val add_binds = map (fn x => (Attrib.empty_binding, x))
-(* Function_Fun.add_fun Function_Common.default_config ... true *)
- val (fvs, lthy') = (Primrec.add_primrec
- (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy)
- val (fvs2, lthy'') =
- if fv_eqs_snd = [] then (([], []), lthy') else
- (Primrec.add_primrec
- (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_snd) (add_binds fv_eqs_snd) lthy')
- val (alphas, lthy''') = (Inductive.add_inductive_i
+ val (alphas, lthy') = (Inductive.add_inductive_i
{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_bn_names)
(alpha_types @ alpha_bn_types)) []
- (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'')
- val ordered_fvs = fv_frees @ fvbns;
- val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2)
-in
- (((all_fvs, ordered_fvs), alphas), lthy''')
-end
-*}
-
-
-
-ML {*
-fun build_alpha_sym_trans_gl alphas (x, y, z) =
-let
- fun build_alpha alpha =
- let
- val ty = domain_type (fastype_of alpha);
- val var = Free(x, ty);
- val var2 = Free(y, ty);
- val var3 = Free(z, ty);
- val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var);
- val transp = HOLogic.mk_imp (alpha $ var $ var2,
- HOLogic.mk_all (z, ty,
- HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3)))
- in
- (symp, transp)
- end;
- val eqs = map build_alpha alphas
- val (sym_eqs, trans_eqs) = split_list eqs
- fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l
-in
- (conj sym_eqs, conj trans_eqs)
-end
-*}
-
-ML {*
-fun build_alpha_refl_gl fv_alphas_lst alphas =
-let
- val (fvs_alphas, _) = split_list fv_alphas_lst;
- val (_, alpha_ts) = split_list fvs_alphas;
- val tys = map (domain_type o fastype_of) alpha_ts;
- val names = Datatype_Prop.make_tnames tys;
- val args = map Free (names ~~ tys);
- fun find_alphas ty x =
- domain_type (fastype_of x) = ty;
- fun refl_eq_arg (ty, arg) =
- let
- val rel_alphas = filter (find_alphas ty) alphas;
- in
- map (fn x => x $ arg $ arg) rel_alphas
- end;
- (* Flattening loses the induction structure *)
- val eqs = map (foldr1 HOLogic.mk_conj) (map refl_eq_arg (tys ~~ args))
-in
- (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs))
-end
-*}
-
-ML {*
-fun reflp_tac induct eq_iff =
- rtac induct THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
- split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
- THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
- @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv
- add_0_left supp_zero_perm Int_empty_left split_conv})
-*}
-
-ML {*
-fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt =
-let
- val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas;
- val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff 1);
-in
- HOLogic.conj_elims refl_conj
-end
-*}
-
-lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
-apply (erule exE)
-apply (rule_tac x="-pi" in exI)
-by auto
-
-ML {*
-fun symp_tac induct inj eqvt ctxt =
- rel_indtac induct THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac
- THEN_ALL_NEW
- REPEAT o etac @{thm exi_neg}
- THEN_ALL_NEW
- split_conj_tac THEN_ALL_NEW
- asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
- TRY o (resolve_tac @{thms alphas_compose_sym2} ORELSE' resolve_tac @{thms alphas_compose_sym}) THEN_ALL_NEW
- (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
-*}
-
-
-lemma exi_sum: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>pi. R pi"
-apply (erule exE)+
-apply (rule_tac x="pia + pi" in exI)
-by auto
-
-
-ML {*
-fun eetac rule =
- Subgoal.FOCUS_PARAMS (fn focus =>
- let
- val concl = #concl focus
- val prems = Logic.strip_imp_prems (term_of concl)
- val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems
- val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs
- val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs
- in
- (etac rule THEN' RANGE[atac, eresolve_tac thins]) 1
- end
- )
-*}
-
-ML {*
-fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
- rel_indtac induct THEN_ALL_NEW
- (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
- asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW
- split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac
- THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct)))
- THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
- TRY o (eresolve_tac @{thms alphas_compose_trans2} ORELSE' eresolve_tac @{thms alphas_compose_trans}) THEN_ALL_NEW
- (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct)))
-*}
-
-lemma transpI:
- "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R"
- unfolding transp_def
- by blast
-
-ML {*
-fun equivp_tac reflps symps transps =
- (*let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in *)
- simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
- THEN' rtac conjI THEN' rtac allI THEN'
- resolve_tac reflps THEN'
- rtac conjI THEN' rtac allI THEN' rtac allI THEN'
- resolve_tac symps THEN'
- rtac @{thm transpI} THEN' resolve_tac transps
-*}
-
-ML {*
-fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =
-let
- val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt;
- val (symg, transg) = build_alpha_sym_trans_gl alphas (x, y, z)
- fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1;
- fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1;
- val symp_loc = Goal.prove ctxt' [] [] symg symp_tac';
- val transp_loc = Goal.prove ctxt' [] [] transg transp_tac';
- val [symp, transp] = Variable.export ctxt' ctxt [symp_loc, transp_loc]
- val symps = HOLogic.conj_elims symp
- val transps = HOLogic.conj_elims transp
- fun equivp alpha =
- let
- val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool})
- val goal = @{term Trueprop} $ (equivp $ alpha)
- fun tac _ = equivp_tac reflps symps transps 1
- in
- Goal.prove ctxt [] [] goal tac
- end
+ (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy)
in
- map equivp alphas
-end
-*}
-
-lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)"
-by auto
-
-ML {*
-fun supports_tac perm =
- simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW (
- REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conj_tac THEN'
- asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric]
- swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh
- supp_fset_to_set supp_fmap_atom}))
-*}
-
-ML {*
-fun mk_supp ty x =
- Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x
-*}
-
-ML {*
-fun mk_supports_eq thy cnstr =
-let
- val (tys, ty) = (strip_type o fastype_of) cnstr
- val names = Datatype_Prop.make_tnames tys
- val frees = map Free (names ~~ tys)
- val rhs = list_comb (cnstr, frees)
-
- fun mk_supp_arg (x, ty) =
- if is_atom thy ty then mk_supp @{typ atom} (mk_atom ty $ x) else
- if is_atom_set thy ty then mk_supp @{typ "atom set"} (mk_atom_set x) else
- if is_atom_fset thy ty then mk_supp @{typ "atom set"} (mk_atom_fset x)
- else mk_supp ty x
- val lhss = map mk_supp_arg (frees ~~ tys)
- val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool})
- val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs)
-in
- (names, eq)
-end
-*}
-
-ML {*
-fun prove_supports ctxt perms cnst =
-let
- val (names, eq) = mk_supports_eq (ProofContext.theory_of ctxt) cnst
-in
- Goal.prove ctxt names [] eq (fn _ => supports_tac perms 1)
-end
-*}
-
-ML {*
-fun mk_fs tys =
-let
- val names = Datatype_Prop.make_tnames tys
- val frees = map Free (names ~~ tys)
- val supps = map2 mk_supp tys frees
- val fin_supps = map (fn x => @{term "finite :: atom set \<Rightarrow> bool"} $ x) supps
-in
- (names, HOLogic.mk_Trueprop (mk_conjl fin_supps))
-end
-*}
-
-ML {*
-fun fs_tac induct supports = rel_indtac induct THEN_ALL_NEW (
- rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW
- asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set
- supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp})
-*}
-
-ML {*
-fun prove_fs ctxt induct supports tys =
-let
- val (names, eq) = mk_fs tys
-in
- Goal.prove ctxt names [] eq (fn _ => fs_tac induct supports 1)
-end
-*}
-
-ML {*
-fun mk_supp x = Const (@{const_name supp}, fastype_of x --> @{typ "atom set"}) $ x;
-
-fun mk_supp_neq arg (fv, alpha) =
-let
- val collect = Const ("Collect", @{typ "(atom \<Rightarrow> bool) \<Rightarrow> atom \<Rightarrow> bool"});
- val ty = fastype_of arg;
- val perm = Const ("Nominal2_Base.pt_class.permute", @{typ perm} --> ty --> ty);
- val finite = @{term "finite :: atom set \<Rightarrow> bool"}
- val rhs = collect $ Abs ("a", @{typ atom},
- HOLogic.mk_not (finite $
- (collect $ Abs ("b", @{typ atom},
- HOLogic.mk_not (alpha $ (perm $ (@{term swap} $ Bound 1 $ Bound 0) $ arg) $ arg)))))
-in
- HOLogic.mk_eq (fv $ arg, rhs)
-end;
-
-fun supp_eq fv_alphas_lst =
-let
- val (fvs_alphas, ls) = split_list fv_alphas_lst;
- val (fv_ts, _) = split_list fvs_alphas;
- val tys = map (domain_type o fastype_of) fv_ts;
- val names = Datatype_Prop.make_tnames tys;
- val args = map Free (names ~~ tys);
- fun supp_eq_arg ((fv, arg), l) =
- mk_conjl
- ((HOLogic.mk_eq (fv $ arg, mk_supp arg)) ::
- (map (mk_supp_neq arg) l))
- val eqs = mk_conjl (map supp_eq_arg ((fv_ts ~~ args) ~~ ls))
-in
- (names, HOLogic.mk_Trueprop eqs)
-end
-*}
-
-ML {*
-fun combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos =
-if length fv_ts_bn < length alpha_ts_bn then
- (fv_ts_nobn ~~ alpha_ts_nobn) ~~ (replicate (length fv_ts_nobn) [])
-else let
- val fv_alpha_nos = 0 upto (length fv_ts_nobn - 1);
- fun filter_fn i (x, j) = if j = i then SOME x else NONE;
- val fv_alpha_bn_nos = (fv_ts_bn ~~ alpha_ts_bn) ~~ bn_nos;
- val fv_alpha_bn_all = map (fn i => map_filter (filter_fn i) fv_alpha_bn_nos) fv_alpha_nos;
-in
- (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all
-end
-*}
-
-(* TODO: this is a hack, it assumes that only one type of Abs's is present
- in the type and chooses this supp_abs. Additionally single atoms are
- treated properly. *)
-ML {*
-fun choose_alpha_abs eqiff =
-let
- fun exists_subterms f ts = true mem (map (exists_subterm f) ts);
- val terms = map prop_of eqiff;
- fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms
- val no =
- if check @{const_name alpha_lst} then 2 else
- if check @{const_name alpha_res} then 1 else
- if check @{const_name alpha_gen} then 0 else
- error "Failure choosing supp_abs"
-in
- nth @{thms supp_abs[symmetric]} no
-end
-*}
-lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}"
-by (rule supp_abs(1))
-
-lemma supp_abs_sum:
- "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))"
- "supp (Abs_res x (a :: 'a :: fs)) \<union> supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))"
- "supp (Abs_lst y (a :: 'a :: fs)) \<union> supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))"
- apply (simp_all add: supp_abs supp_Pair)
- apply blast+
- done
-
-
-ML {*
-fun supp_eq_tac ind fv perm eqiff ctxt =
- rel_indtac ind THEN_ALL_NEW
- asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
- asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW
- asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps @{thms alphas3 alphas2}) THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW
- asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
- asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps @{thms infinite_Un[symmetric]}) THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps @{thms Collect_disj_eq[symmetric]}) THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW
- simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW
- simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI})
-*}
-
-
-
-ML {*
-fun build_eqvt_gl pi frees fnctn ctxt =
-let
- val typ = domain_type (fastype_of fnctn);
- val arg = the (AList.lookup (op=) frees typ);
-in
- ([HOLogic.mk_eq ((perm_arg (fnctn $ arg) $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt)
-end
-*}
-
-ML {*
-fun prove_eqvt tys ind simps funs ctxt =
-let
- val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt;
- val pi = Free (pi, @{typ perm});
- val tac = asm_full_simp_tac (HOL_ss addsimps (@{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt'))
- val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt'
- val ths = Variable.export ctxt' ctxt ths_loc
- val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)
-in
- (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt))
+ (alphas, lthy')
end
*}
--- a/Nominal/Lift.thy Mon Apr 19 09:59:32 2010 +0200
+++ b/Nominal/Lift.thy Mon Apr 19 10:00:52 2010 +0200
@@ -2,7 +2,7 @@
imports "../Nominal-General/Nominal2_Atoms"
"../Nominal-General/Nominal2_Eqvt"
"../Nominal-General/Nominal2_Supp"
- "Abs" "Perm" "Fv" "Rsp"
+ "Abs" "Perm" "Equivp" "Rsp"
begin
@@ -69,13 +69,15 @@
ML {*
fun define_fv_alpha_export dt binds bns ctxt =
let
- val ((((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), alpha), ctxt') =
- define_fv_alpha dt binds bns ctxt;
+ val (((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), ctxt') =
+ define_fv dt binds bns ctxt;
+ val (alpha, ctxt'') =
+ define_alpha dt binds bns fv_ts_loc ctxt';
val alpha_ts_loc = #preds alpha
val alpha_induct_loc = #induct alpha
val alpha_intros_loc = #intrs alpha;
val alpha_cases_loc = #elims alpha
- val morphism = ProofContext.export_morphism ctxt' ctxt;
+ val morphism = ProofContext.export_morphism ctxt'' ctxt;
val fv_ts = map (Morphism.term morphism) fv_ts_loc;
val ord_fv_ts = map (Morphism.term morphism) ord_fv_ts_loc;
val fv_def = Morphism.fact morphism fv_def_loc;
@@ -84,7 +86,7 @@
val alpha_intros = Morphism.fact morphism alpha_intros_loc
val alpha_cases = Morphism.fact morphism alpha_cases_loc
in
- ((((fv_ts, ord_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt')
+ ((((fv_ts, ord_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt'')
end;
*}
--- a/Nominal/Manual/Term4.thy Mon Apr 19 09:59:32 2010 +0200
+++ b/Nominal/Manual/Term4.thy Mon Apr 19 10:00:52 2010 +0200
@@ -1,5 +1,5 @@
theory Term4
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" "Quotient_List"
+imports "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "Quotient_List"
begin
atom_decl name
@@ -17,6 +17,7 @@
(* there cannot be a clause for lists, as *)
(* permutations are already defined in Nominal (also functions, options, and so on) *)
setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term4.rtrm4") 1 *}
+print_theorems
(* "repairing" of the permute function *)
lemma repaired:
@@ -27,10 +28,11 @@
done
thm permute_rtrm4_permute_rtrm4_list.simps
-thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
+lemmas rawperm=permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
+
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4")
- [[[], [], [(NONE, 0,1)]], [[], []] ] *}
+local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term4.rtrm4")
+ [[[], [], [(NONE, 0, 1, AlphaGen)]], [[], []] ] [] *}
print_theorems
lemma fix2: "alpha_rtrm4_list = list_rel alpha_rtrm4"
@@ -54,34 +56,29 @@
alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *}
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *}
thm alpha4_inj
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
thm alpha4_inj_no
-local_setup {*
-snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct}
-*}
-print_theorems
+local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] fv_rtrm4_fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *}
+thm eqvts(1-2)
local_setup {*
(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt_no}, []),
- build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj_no} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt))
+ build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj_no} ctxt 1) ctxt) ctxt))
*}
lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2]
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []),
- (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *}
-lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2]
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []),
+ build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj_no} ctxt) ctxt)) *}
+thm alpha4_reflp
+ML build_equivps
-(*lemma fv_rtrm4_rsp:
- "xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya"
- "x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y"
- apply (induct rule: alpha_rtrm4_alpha_rtrm4_list.inducts)
- apply (simp_all add: alpha_gen)
-done*)
-
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []),
+ (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *}
+lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2]
quotient_type
trm4 = rtrm4 / alpha_rtrm4
@@ -91,31 +88,58 @@
local_setup {*
(fn ctxt => ctxt
- |> snd o (Quotient_Def.quotient_lift_const ("Vr4", @{term rVr4}))
- |> snd o (Quotient_Def.quotient_lift_const ("Ap4", @{term rAp4}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lm4", @{term rLm4})))
+ |> snd o (Quotient_Def.quotient_lift_const [] ("Vr4", @{term rVr4}))
+ |> snd o (Quotient_Def.quotient_lift_const [@{typ "trm4"}] ("Ap4", @{term rAp4}))
+ |> snd o (Quotient_Def.quotient_lift_const [] ("Lm4", @{term rLm4}))
+ |> snd o (Quotient_Def.quotient_lift_const [] ("fv_trm4", @{term fv_rtrm4})))
*}
print_theorems
-local_setup {* snd o prove_const_rsp @{binding fv_rtrm4_rsp} [@{term fv_rtrm4}]
- (fn _ => fvbv_rsp_tac @{thm alpha_rtrm4_alpha_rtrm4_list.inducts(1)} @{thms fv_rtrm4_fv_rtrm4_list.simps} 1) *}
+
+
+lemma fv_rtrm4_rsp:
+ "xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya"
+ "x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y"
+ apply (induct rule: alpha_rtrm4_alpha_rtrm4_list.inducts)
+ apply (simp_all add: alpha_gen)
+done
+
+local_setup {* snd o prove_const_rsp [] @{binding fv_rtrm4_rsp'} [@{term fv_rtrm4}]
+ (fn _ => asm_full_simp_tac (@{simpset} addsimps @{thms fv_rtrm4_rsp}) 1) *}
print_theorems
-local_setup {* snd o prove_const_rsp @{binding rVr4_rsp} [@{term rVr4}]
- (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *}
-lemma "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
-apply simp
-apply clarify
-apply (simp add: alpha4_inj)
+local_setup {* snd o prove_const_rsp [] @{binding rVr4_rsp} [@{term rVr4}]
+ (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *}
+local_setup {* snd o prove_const_rsp [] @{binding rLm4_rsp} [@{term rLm4}]
+ (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *}
+
+lemma [quot_respect]:
+ "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
+ by (simp add: alpha4_inj)
+
+(* Maybe also need: @{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"} *)
+local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp}
+ [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}]
+ (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *}
+print_theorems
+
+setup {* define_lifted_perms [@{typ trm4}] ["Term4.trm4"] [("permute_trm4", @{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"})] @{thms permute_rtrm4_permute_rtrm4_list_zero permute_rtrm4_permute_rtrm4_list_append} *}
+print_theorems
-local_setup {* snd o prove_const_rsp @{binding rLm4_rsp} [@{term rLm4}]
- (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *}
-local_setup {* snd o prove_const_rsp @{binding permute_rtrm4_rsp}
- [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}, @{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}]
- (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *}
+
+lemma bla: "(Ap4 trm4 list = Ap4 trm4a lista) =
+ (trm4 = trm4a \<and> list_rel (op =) list lista)"
+ by (lifting alpha4_inj(2))
+
+thm bla[simplified list_rel_eq]
-thm rtrm4.induct
-lemmas trm1_bp_induct = rtrm4.induct[quot_lifted]
+ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(1)} *}
+ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(2)} *}
+ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(3)[unfolded alpha_gen]} *}
+ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *}
+.
+
+(*lemmas trm1_bp_induct = rtrm4.induct[quot_lifted]*)
end
--- a/Nominal/Parser.thy Mon Apr 19 09:59:32 2010 +0200
+++ b/Nominal/Parser.thy Mon Apr 19 10:00:52 2010 +0200
@@ -2,7 +2,7 @@
imports "../Nominal-General/Nominal2_Atoms"
"../Nominal-General/Nominal2_Eqvt"
"../Nominal-General/Nominal2_Supp"
- "Perm" "Fv" "Rsp" "Lift"
+ "Perm" "Equivp" "Rsp" "Lift"
begin
section{* Interface for nominal_datatype *}
--- a/Nominal/Perm.thy Mon Apr 19 09:59:32 2010 +0200
+++ b/Nominal/Perm.thy Mon Apr 19 10:00:52 2010 +0200
@@ -4,8 +4,7 @@
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});
+ open Nominal_Library;
*}
ML {*
@@ -94,10 +93,10 @@
in list_abs (map (pair "x") Us,
Free (nth perm_names_types' (body_index dt)) $ pi $
list_comb (x, map (fn (i, U) =>
- (permute U) $ (minus_perm $ pi) $ Bound i)
+ (mk_perm_ty U (mk_minus pi) (Bound i)))
((length Us - 1 downto 0) ~~ Us)))
end
- else (permute T) $ pi $ x
+ else (mk_perm_ty T pi x)
end;
in
(Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -125,7 +124,8 @@
lthy'
|> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms))
|> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms))
- |> Class_Target.prove_instantiation_exit_result morphism tac (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees)
+ |> Class_Target.prove_instantiation_exit_result morphism tac
+ (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees)
end
*}
--- a/Paper/Paper.thy Mon Apr 19 09:59:32 2010 +0200
+++ b/Paper/Paper.thy Mon Apr 19 10:00:52 2010 +0200
@@ -424,7 +424,7 @@
permutations. The sorts of atoms can be used to represent different kinds of
variables, such as the term-, coercion- and type-variables in Core-Haskell.
It is assumed that there is an infinite supply of atoms for each
- sort. However, in the intrest of brevity, we shall restrict ourselves
+ sort. However, in the interest of brevity, we shall restrict ourselves
in what follows to only one sort of atoms.
Permutations are bijective functions from atoms to atoms that are
@@ -774,7 +774,7 @@
\end{center}
\noindent
- indicating that a set (or list) @{text as} is abstracted in @{text x}. We will
+ indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will
call the types \emph{abstraction types} and their elements
\emph{abstractions}. The important property we need to derive is the support of
abstractions, namely:
@@ -1032,7 +1032,7 @@
As will shortly become clear, we cannot return an atom in a binding function
that is also bound in the corresponding term-constructor. That means in the
- example above that the term-constructors @{text PVar} and @{text PTup} must not have a
+ example above that the term-constructors @{text PVar} and @{text PTup} may not have a
binding clause. In the version of Nominal Isabelle described here, we also adopted
the restriction from the Ott-tool that binding functions can only return:
the empty set or empty list (as in case @{text PNil}), a singleton set or singleton
@@ -2019,7 +2019,7 @@
definitions to equivariant functions (for such functions it is possible to
provide more automation).
- There are some restrictions we imposed in this paper, we like to lift in
+ There are some restrictions we imposed in this paper, that we would like to lift in
future work. One is the exclusion of nested datatype definitions. Nested
datatype definitions allow one to specify, for instance, the function kinds
in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded