--- a/Attic/FIXME-TODO Wed Apr 21 12:25:52 2010 +0200
+++ b/Attic/FIXME-TODO Mon Apr 26 10:01:13 2010 +0200
@@ -67,6 +67,3 @@
That means "qconst :: qty" is not read as a term, but
as two entities.
-
-- Restrict automatic translation to particular quotient types
-
--- a/Attic/Prove.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Attic/Prove.thy Mon Apr 26 10:01:13 2010 +0200
@@ -15,7 +15,7 @@
let
val trm = ML_Context.evaluate lthy true ("r", r) txt
in
- Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy
+ Proof.theorem NONE (after_qed name_spec) [[(trm,[])]] lthy
end
val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source
--- a/Attic/Quot/Examples/FSet3.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Attic/Quot/Examples/FSet3.thy Mon Apr 26 10:01:13 2010 +0200
@@ -2,154 +2,6 @@
imports "../../../Nominal/FSet"
begin
-notation
- list_eq (infix "\<approx>" 50)
-
-lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
- shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by (lifting list.exhaust)
-
-(* 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 *)
-(* 'a_1 *)
-
-lemma concat1:
- shows "concat [] \<approx> []"
-by (simp)
-
-lemma concat2:
- shows "concat (x # xs) \<approx> x @ concat xs"
-by (simp)
-
-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"
- 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>) [] []"
- by (metis nil_rsp list_rel.simps(1) pred_compI)
-
-lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
- apply (rule eq_reflection)
- apply auto
- done
-
-lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
- unfolding list_eq.simps
- apply(simp only: set_map set_in_eq)
- done
-
-lemma quotient_compose_list_pre:
- "(list_rel op \<approx> OOO op \<approx>) r s =
- ((list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s \<and>
- abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
- apply rule
- apply rule
- apply rule
- apply (rule list_rel_refl)
- apply (metis equivp_def fset_equivp)
- apply rule
- apply (rule equivp_reflp[OF fset_equivp])
- apply (rule list_rel_refl)
- apply (metis equivp_def fset_equivp)
- apply(rule)
- apply rule
- apply (rule list_rel_refl)
- apply (metis equivp_def fset_equivp)
- apply rule
- apply (rule equivp_reflp[OF fset_equivp])
- apply (rule list_rel_refl)
- apply (metis equivp_def fset_equivp)
- apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s")
- apply (metis Quotient_rel[OF Quotient_fset])
- apply (auto simp only:)[1]
- apply (subgoal_tac "map abs_fset r = map abs_fset b")
- prefer 2
- apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
- apply (subgoal_tac "map abs_fset s = map abs_fset ba")
- prefer 2
- apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
- apply (simp only: map_rel_cong)
- apply rule
- apply (rule rep_abs_rsp[of "list_rel op \<approx>" "map abs_fset"])
- apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
- apply (rule list_rel_refl)
- apply (metis equivp_def fset_equivp)
- apply rule
- prefer 2
- apply (rule rep_abs_rsp_left[of "list_rel op \<approx>" "map abs_fset"])
- apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
- apply (rule list_rel_refl)
- apply (metis equivp_def fset_equivp)
- apply (erule conjE)+
- apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s")
- prefer 2
- apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp)
- apply (rule map_rel_cong)
- apply (assumption)
- done
-
-lemma quotient_compose_list[quot_thm]:
- shows "Quotient ((list_rel op \<approx>) OOO (op \<approx>))
- (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
- unfolding Quotient_def comp_def
- apply (rule)+
- apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset])
- apply (rule)
- apply (rule)
- apply (rule)
- apply (rule list_rel_refl)
- apply (metis equivp_def fset_equivp)
- apply (rule)
- apply (rule equivp_reflp[OF fset_equivp])
- apply (rule list_rel_refl)
- apply (metis equivp_def fset_equivp)
- apply rule
- apply rule
- apply (rule quotient_compose_list_pre)
- done
-
-lemma fconcat_empty:
- shows "fconcat {||} = {||}"
- apply(lifting concat1)
- apply(cleaning)
- apply(simp add: comp_def bot_fset_def)
- 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)
- apply (rule_tac b="x # b" in pred_compI)
- apply auto
- apply (rule_tac b="x # ba" in pred_compI)
- apply auto
- done
-
-lemma append_rsp[quot_respect]:
- "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
- by (auto)
-
-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
-
(* TBD *)
text {* syntax for fset comprehensions (adapted from lists) *}
--- a/Attic/Quot/Examples/IntEx.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Attic/Quot/Examples/IntEx.thy Mon Apr 26 10:01:13 2010 +0200
@@ -165,27 +165,6 @@
apply(lifting plus_assoc_pre)
done
-lemma int_induct_raw:
- assumes a: "P (0::nat, 0)"
- and b: "\<And>i. P i \<Longrightarrow> P (my_plus i (1,0))"
- and c: "\<And>i. P i \<Longrightarrow> P (my_plus i (my_neg (1,0)))"
- shows "P x"
- apply(case_tac x) apply(simp)
- apply(rule_tac x="b" in spec)
- apply(rule_tac Nat.induct)
- apply(rule allI)
- apply(rule_tac Nat.induct)
- using a b c apply(auto)
- done
-
-lemma int_induct:
- assumes a: "P ZERO"
- and b: "\<And>i. P i \<Longrightarrow> P (PLUS i ONE)"
- and c: "\<And>i. P i \<Longrightarrow> P (PLUS i (NEG ONE))"
- shows "P x"
- using a b c
- by (lifting int_induct_raw)
-
lemma ex1tst: "Bex1_rel (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)"
sorry
--- a/Attic/Quot/Examples/IntEx2.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Attic/Quot/Examples/IntEx2.thy Mon Apr 26 10:01:13 2010 +0200
@@ -76,7 +76,7 @@
lemma plus_raw_rsp[quot_respect]:
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
-by auto
+ by auto
lemma uminus_raw_rsp[quot_respect]:
shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw"
@@ -85,70 +85,70 @@
lemma mult_raw_fst:
assumes a: "x \<approx> z"
shows "mult_raw x y \<approx> mult_raw z y"
-using a
-apply(cases x, cases y, cases z)
-apply(auto simp add: mult_raw.simps intrel.simps)
-apply(rename_tac u v w x y z)
-apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
-apply(simp add: mult_ac)
-apply(simp add: add_mult_distrib [symmetric])
-done
+ using a
+ apply(cases x, cases y, cases z)
+ apply(auto simp add: mult_raw.simps intrel.simps)
+ apply(rename_tac u v w x y z)
+ apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
+ apply(simp add: mult_ac)
+ apply(simp add: add_mult_distrib [symmetric])
+ done
lemma mult_raw_snd:
assumes a: "x \<approx> z"
shows "mult_raw y x \<approx> mult_raw y z"
-using a
-apply(cases x, cases y, cases z)
-apply(auto simp add: mult_raw.simps intrel.simps)
-apply(rename_tac u v w x y z)
-apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
-apply(simp add: mult_ac)
-apply(simp add: add_mult_distrib [symmetric])
-done
+ using a
+ apply(cases x, cases y, cases z)
+ apply(auto simp add: mult_raw.simps intrel.simps)
+ apply(rename_tac u v w x y z)
+ apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
+ apply(simp add: mult_ac)
+ apply(simp add: add_mult_distrib [symmetric])
+ done
lemma mult_raw_rsp[quot_respect]:
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
-apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule equivp_transp[OF int_equivp])
-apply(rule mult_raw_fst)
-apply(assumption)
-apply(rule mult_raw_snd)
-apply(assumption)
-done
+ apply(simp only: fun_rel_def)
+ apply(rule allI | rule impI)+
+ apply(rule equivp_transp[OF int_equivp])
+ apply(rule mult_raw_fst)
+ apply(assumption)
+ apply(rule mult_raw_snd)
+ apply(assumption)
+ done
lemma le_raw_rsp[quot_respect]:
shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"
-by auto
+ by auto
lemma plus_assoc_raw:
shows "plus_raw (plus_raw i j) k \<approx> plus_raw i (plus_raw j k)"
-by (cases i, cases j, cases k) (simp)
+ by (cases i, cases j, cases k) (simp)
lemma plus_sym_raw:
shows "plus_raw i j \<approx> plus_raw j i"
-by (cases i, cases j) (simp)
+ by (cases i, cases j) (simp)
lemma plus_zero_raw:
shows "plus_raw (0, 0) i \<approx> i"
-by (cases i) (simp)
+ by (cases i) (simp)
lemma plus_minus_zero_raw:
shows "plus_raw (uminus_raw i) i \<approx> (0, 0)"
-by (cases i) (simp)
+ by (cases i) (simp)
lemma times_assoc_raw:
shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"
-by (cases i, cases j, cases k)
- (simp add: algebra_simps)
+ by (cases i, cases j, cases k)
+ (simp add: algebra_simps)
lemma times_sym_raw:
shows "mult_raw i j \<approx> mult_raw j i"
-by (cases i, cases j) (simp add: algebra_simps)
+ by (cases i, cases j) (simp add: algebra_simps)
lemma times_one_raw:
shows "mult_raw (1, 0) i \<approx> i"
-by (cases i) (simp)
+ by (cases i) (simp)
lemma times_plus_comm_raw:
shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
@@ -189,19 +189,19 @@
lemma plus_raw_rsp_aux:
assumes a: "a \<approx> b" "c \<approx> d"
shows "plus_raw a c \<approx> plus_raw b d"
-using a
-by (cases a, cases b, cases c, cases d)
- (simp)
+ using a
+ by (cases a, cases b, cases c, cases d)
+ (simp)
lemma add:
- "(abs_int (x,y)) + (abs_int (u,v)) =
- (abs_int (x + u, y + v))"
-apply(simp add: plus_int_def id_simps)
-apply(fold plus_raw.simps)
-apply(rule Quotient_rel_abs[OF Quotient_int])
-apply(rule plus_raw_rsp_aux)
-apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
-done
+ "(abs_int (x,y)) + (abs_int (u,v)) =
+ (abs_int (x + u, y + v))"
+ apply(simp add: plus_int_def id_simps)
+ apply(fold plus_raw.simps)
+ apply(rule Quotient_rel_abs[OF Quotient_int])
+ apply(rule plus_raw_rsp_aux)
+ apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
+ done
definition int_of_nat_raw:
"int_of_nat_raw m = (m :: nat, 0 :: nat)"
@@ -211,30 +211,29 @@
lemma[quot_respect]:
shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
-by (simp add: equivp_reflp[OF int_equivp])
+ by (simp add: equivp_reflp[OF int_equivp])
lemma int_of_nat:
shows "of_nat m = int_of_nat m"
-apply (induct m)
-apply (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add)
-done
+ by (induct m)
+ (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add)
lemma le_antisym_raw:
shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j"
-by (cases i, cases j) (simp)
+ by (cases i, cases j) (simp)
lemma le_refl_raw:
shows "le_raw i i"
-by (cases i) (simp)
+ by (cases i) (simp)
lemma le_trans_raw:
shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k"
-by (cases i, cases j, cases k) (simp)
+ by (cases i, cases j, cases k) (simp)
lemma le_cases_raw:
shows "le_raw i j \<or> le_raw j i"
-by (cases i, cases j)
- (simp add: linorder_linear)
+ by (cases i, cases j)
+ (simp add: linorder_linear)
instance int :: linorder
proof
@@ -268,8 +267,7 @@
lemma le_plus_raw:
shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)"
-by (cases i, cases j, cases k) (simp)
-
+ by (cases i, cases j, cases k) (simp)
instance int :: ordered_cancel_ab_semigroup_add
proof
@@ -285,21 +283,21 @@
fixes i j::int
and k::nat
shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
-apply(induct "k")
-apply(simp)
-apply(case_tac "k = 0")
-apply(simp_all add: left_distrib add_strict_mono)
-done
+ apply(induct "k")
+ apply(simp)
+ apply(case_tac "k = 0")
+ apply(simp_all add: left_distrib add_strict_mono)
+ done
lemma zero_le_imp_eq_int_raw:
fixes k::"(nat \<times> nat)"
shows "less_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
-apply(cases k)
-apply(simp add:int_of_nat_raw)
-apply(auto)
-apply(rule_tac i="b" and j="a" in less_Suc_induct)
-apply(auto)
-done
+ apply(cases k)
+ apply(simp add:int_of_nat_raw)
+ apply(auto)
+ apply(rule_tac i="b" and j="a" in less_Suc_induct)
+ apply(auto)
+ done
lemma zero_le_imp_eq_int:
fixes k::int
@@ -311,11 +309,8 @@
fixes i j k::int
assumes a: "i < j" "0 < k"
shows "k * i < k * j"
-using a
-using a
-apply(drule_tac zero_le_imp_eq_int)
-apply(auto simp add: zmult_zless_mono2_lemma)
-done
+ using a
+ by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
text{*The integers form an ordered integral domain*}
instance int :: linordered_idom
@@ -335,6 +330,31 @@
left_diff_distrib [of "z1::int" "z2" "w", standard]
right_diff_distrib [of "w::int" "z1" "z2", standard]
+lemma int_induct_raw:
+ assumes a: "P (0::nat, 0)"
+ and b: "\<And>i. P i \<Longrightarrow> P (plus_raw i (1, 0))"
+ and c: "\<And>i. P i \<Longrightarrow> P (plus_raw i (uminus_raw (1, 0)))"
+ shows "P x"
+proof (cases x, clarify)
+ fix a b
+ show "P (a, b)"
+ proof (induct a arbitrary: b rule: Nat.induct)
+ case zero
+ show "P (0, b)" using assms by (induct b) auto
+ next
+ case (Suc n)
+ then show ?case using assms by auto
+ qed
+qed
+
+lemma int_induct:
+ fixes x :: int
+ assumes a: "P 0"
+ and b: "\<And>i. P i \<Longrightarrow> P (i + 1)"
+ and c: "\<And>i. P i \<Longrightarrow> P (i - 1)"
+ shows "P x"
+ using a b c unfolding minus_int_def
+ by (lifting int_induct_raw)
subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
--- a/Nominal-General/Nominal2_Atoms.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal-General/Nominal2_Atoms.thy Mon Apr 26 10:01:13 2010 +0200
@@ -5,6 +5,7 @@
*)
theory Nominal2_Atoms
imports Nominal2_Base
+ Nominal2_Eqvt
uses ("nominal_atoms.ML")
begin
@@ -20,6 +21,8 @@
assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b"
assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)"
+declare atom_eqvt[eqvt]
+
class at = at_base +
assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"
@@ -75,6 +78,107 @@
thus ?thesis ..
qed
+lemma atom_image_cong:
+ fixes X Y::"('a::at_base) set"
+ shows "(atom ` X = atom ` Y) = (X = Y)"
+ apply(rule inj_image_eq_iff)
+ apply(simp add: inj_on_def)
+ done
+
+lemma atom_image_supp:
+ "supp S = supp (atom ` S)"
+ apply(simp add: supp_def)
+ apply(simp add: image_eqvt)
+ apply(subst (2) permute_fun_def)
+ apply(simp add: atom_eqvt)
+ apply(simp add: atom_image_cong)
+ done
+
+lemma supp_finite_at_set:
+ fixes S::"('a::at) set"
+ assumes a: "finite S"
+ shows "supp S = atom ` S"
+ apply(rule finite_supp_unique)
+ apply(simp add: supports_def)
+ apply(rule allI)+
+ apply(rule impI)
+ apply(rule swap_fresh_fresh)
+ apply(simp add: fresh_def)
+ apply(simp add: atom_image_supp)
+ apply(subst supp_finite_atom_set)
+ apply(rule finite_imageI)
+ apply(simp add: a)
+ apply(simp)
+ apply(simp add: fresh_def)
+ apply(simp add: atom_image_supp)
+ apply(subst supp_finite_atom_set)
+ apply(rule finite_imageI)
+ apply(simp add: a)
+ apply(simp)
+ apply(rule finite_imageI)
+ apply(simp add: a)
+ apply(drule swap_set_in)
+ apply(assumption)
+ apply(simp)
+ apply(simp add: image_eqvt)
+ apply(simp add: permute_fun_def)
+ apply(simp add: atom_eqvt)
+ apply(simp add: atom_image_cong)
+ done
+
+lemma supp_finite_at_set_aux:
+ fixes S::"('a::at) set"
+ assumes a: "finite S"
+ shows "supp S = atom ` S"
+proof
+ show "supp S \<subseteq> ((atom::'a::at \<Rightarrow> atom) ` S)"
+ apply(rule supp_is_subset)
+ apply(simp add: supports_def)
+ apply(rule allI)+
+ apply(rule impI)
+ apply(rule swap_fresh_fresh)
+ apply(simp add: fresh_def)
+ apply(simp add: atom_image_supp)
+ apply(subst supp_finite_atom_set)
+ apply(rule finite_imageI)
+ apply(simp add: a)
+ apply(simp)
+ apply(simp add: fresh_def)
+ apply(simp add: atom_image_supp)
+ apply(subst supp_finite_atom_set)
+ apply(rule finite_imageI)
+ apply(simp add: a)
+ apply(simp)
+ apply(rule finite_imageI)
+ apply(simp add: a)
+ done
+next
+ have "supp ((atom::'a::at \<Rightarrow> atom) ` S) \<subseteq> supp ((op `) (atom::'a::at \<Rightarrow> atom)) \<union> supp S"
+ by (simp add: supp_fun_app)
+ moreover
+ have "supp ((op `) (atom::'a::at \<Rightarrow> atom)) = {}"
+ apply(rule supp_fun_eqvt)
+ apply(perm_simp)
+ apply(simp)
+ done
+ moreover
+ have "supp ((atom::'a::at \<Rightarrow> atom) ` S) = ((atom::'a::at \<Rightarrow> atom) ` S)"
+ apply(subst supp_finite_atom_set)
+ apply(rule finite_imageI)
+ apply(simp add: a)
+ apply(simp)
+ done
+ ultimately
+ show "((atom::'a::at \<Rightarrow> atom) ` S) \<subseteq> supp S" by simp
+qed
+
+
+lemma supp_at_insert:
+ fixes S::"('a::at) set"
+ assumes a: "finite S"
+ shows "supp (insert a S) = supp a \<union> supp S"
+ using a by (simp add: supp_finite_at_set supp_at_base)
+
section {* A swapping operation for concrete atoms *}
--- a/Nominal-General/Nominal2_Base.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal-General/Nominal2_Base.thy Mon Apr 26 10:01:13 2010 +0200
@@ -29,6 +29,11 @@
where
"sort_of (Atom s i) = s"
+primrec
+ nat_of :: "atom \<Rightarrow> nat"
+where
+ "nat_of (Atom s n) = n"
+
text {* There are infinitely many atoms of each sort. *}
lemma INFM_sort_of_eq:
@@ -63,6 +68,11 @@
then show ?thesis ..
qed
+lemma atom_components_eq_iff:
+ fixes a b :: atom
+ shows "a = b \<longleftrightarrow> sort_of a = sort_of b \<and> nat_of a = nat_of b"
+ by (induct a, induct b, simp)
+
section {* Sort-Respecting Permutations *}
typedef perm =
@@ -459,7 +469,6 @@
unfolding permute_set_eq
using a by (auto simp add: swap_atom)
-
subsection {* Permutations for units *}
instantiation unit :: pt
@@ -835,6 +844,24 @@
instance atom :: fs
by default (simp add: supp_atom)
+section {* Support for finite sets of atoms *}
+
+lemma supp_finite_atom_set:
+ fixes S::"atom set"
+ assumes "finite S"
+ shows "supp S = S"
+ apply(rule finite_supp_unique)
+ apply(simp add: supports_def)
+ apply(simp add: swap_set_not_in)
+ apply(rule assms)
+ apply(simp add: swap_set_in)
+done
+
+lemma supp_atom_insert:
+ fixes S::"atom set"
+ assumes a: "finite S"
+ shows "supp (insert a S) = supp a \<union> supp S"
+ using a by (simp add: supp_finite_atom_set supp_atom)
section {* Type @{typ perm} is finitely-supported. *}
@@ -1054,32 +1081,18 @@
unfolding fresh_def
by auto
-(* alternative proof *)
-lemma
- shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)"
-proof (rule subsetCI)
- fix a::"atom"
- assume a: "a \<in> supp (f x)"
- assume b: "a \<notin> supp f \<union> supp x"
- then have "finite {b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f}" "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"
- unfolding supp_def by auto
- then have "finite ({b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f} \<union> {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x})" by simp
- moreover
- have "{b. ((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x) \<noteq> f x} \<subseteq> ({b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f} \<union> {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x})"
- by auto
- ultimately have "finite {b. ((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x) \<noteq> f x}"
- using finite_subset by auto
- then have "a \<notin> supp (f x)" unfolding supp_def
- by (simp add: permute_fun_app_eq)
- with a show "False" by simp
-qed
-
+lemma supp_fun_eqvt:
+ assumes a: "\<forall>p. p \<bullet> f = f"
+ shows "supp f = {}"
+ unfolding supp_def
+ using a by simp
+
+
lemma fresh_fun_eqvt_app:
assumes a: "\<forall>p. p \<bullet> f = f"
shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
proof -
- from a have "supp f = {}"
- unfolding supp_def by simp
+ from a have "supp f = {}" by (simp add: supp_fun_eqvt)
then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
unfolding fresh_def
using supp_fun_app
--- a/Nominal-General/Nominal2_Eqvt.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy Mon Apr 26 10:01:13 2010 +0200
@@ -6,7 +6,7 @@
(contains many, but not all such lemmas).
*)
theory Nominal2_Eqvt
-imports Nominal2_Base Nominal2_Atoms
+imports Nominal2_Base
uses ("nominal_thmdecls.ML")
("nominal_permeq.ML")
("nominal_eqvt.ML")
@@ -249,7 +249,7 @@
imp_eqvt [folded induct_implies_def]
(* nominal *)
- supp_eqvt fresh_eqvt
+ supp_eqvt fresh_eqvt add_perm_eqvt
(* datatypes *)
permute_prod.simps append_eqvt rev_eqvt set_eqvt
@@ -259,8 +259,7 @@
empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt
Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt
- atom_eqvt add_perm_eqvt
-
+
lemmas [eqvt_raw] =
permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *)
@@ -288,22 +287,13 @@
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 =
- {* test1 -- test2 >>
- (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt [] consts))) *}
- {* pushes permutations inside *}
+ {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *}
+ {* pushes permutations inside. *}
method_setup perm_strict_simp =
- {* 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 *}
+ {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}
+ {* pushes permutations inside, raises an error if it cannot solve all permutations. *}
declare [[trace_eqvt = true]]
--- a/Nominal-General/Nominal2_Supp.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy Mon Apr 26 10:01:13 2010 +0200
@@ -11,6 +11,7 @@
section {* Fresh-Star *}
+
text {* The fresh-star generalisation of fresh is used in strong
induction principles. *}
@@ -127,9 +128,8 @@
moreover
have "supp ?q \<subseteq> insert x Xs \<union> ?q \<bullet> insert x Xs"
using p2 unfolding q
- apply (intro subset_trans [OF supp_plus_perm])
- apply (auto simp add: supp_swap)
- done
+ by (intro subset_trans [OF supp_plus_perm])
+ (auto simp add: supp_swap)
ultimately show ?case by blast
qed
qed
@@ -158,20 +158,21 @@
lemma at_set_avoiding2_atom:
assumes "finite (supp c)" "finite (supp x)"
- and b: "xa \<sharp> x"
- shows "\<exists>p. (p \<bullet> xa) \<sharp> c \<and> supp x \<sharp>* p"
+ and b: "a \<sharp> x"
+ shows "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p"
proof -
- have a: "{xa} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
- obtain p where p1: "(p \<bullet> {xa}) \<sharp>* c" and p2: "supp x \<sharp>* p"
- using at_set_avoiding2[of "{xa}" "c" "x"] assms a by blast
- have c: "(p \<bullet> xa) \<sharp> c" using p1
+ have a: "{a} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
+ obtain p where p1: "(p \<bullet> {a}) \<sharp>* c" and p2: "supp x \<sharp>* p"
+ using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast
+ have c: "(p \<bullet> a) \<sharp> c" using p1
unfolding fresh_star_def Ball_def
- by (erule_tac x="p \<bullet> xa" in allE) (simp add: eqvts)
- hence "p \<bullet> xa \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
- then show ?thesis by blast
+ by (erule_tac x="p \<bullet> a" in allE) (simp add: eqvts)
+ hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
+ then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast
qed
-section {* The freshness lemma according to Andrew Pitts *}
+
+section {* The freshness lemma according to Andy Pitts *}
lemma freshness_lemma:
fixes h :: "'a::at \<Rightarrow> 'b::pt"
@@ -339,17 +340,9 @@
using P Q by (rule FRESH_binop_iff)
-section {* An example of a function without finite support *}
+section {* @{const nat_of} is an example of a function
+ without finite support *}
-primrec
- nat_of :: "atom \<Rightarrow> nat"
-where
- "nat_of (Atom s n) = n"
-
-lemma atom_eq_iff:
- fixes a b :: atom
- shows "a = b \<longleftrightarrow> sort_of a = sort_of b \<and> nat_of a = nat_of b"
- by (induct a, induct b, simp)
lemma not_fresh_nat_of:
shows "\<not> a \<sharp> nat_of"
@@ -368,7 +361,7 @@
also have "\<dots> = nat_of ((a \<rightleftharpoons> b) \<bullet> a)" using b3 by simp
also have "\<dots> = nat_of b" using b2 by simp
finally have "nat_of a = nat_of b" by simp
- with b2 have "a = b" by (simp add: atom_eq_iff)
+ with b2 have "a = b" by (simp add: atom_components_eq_iff)
with b1 show "False" by simp
qed
@@ -377,30 +370,17 @@
using not_fresh_nat_of [unfolded fresh_def] by auto
-section {* Support for finite sets of atoms *}
+section {* Induction principle for permutations *}
+
-lemma supp_finite_atom_set:
- fixes S::"atom set"
- assumes "finite S"
- shows "supp S = S"
- apply(rule finite_supp_unique)
- apply(simp add: supports_def)
- apply(simp add: swap_set_not_in)
- apply(rule assms)
- apply(simp add: swap_set_in)
-done
-
-text {* Induction principle for permutations *}
-
-lemma perm_subset_induct_aux [consumes 1, case_names zero swap plus]:
+lemma perm_struct_induct[consumes 1, case_names zero swap]:
assumes S: "supp p \<subseteq> S"
- assumes zero: "P 0"
- assumes swap: "\<And>a b. supp (a \<rightleftharpoons> b) \<subseteq> S \<Longrightarrow> P (a \<rightleftharpoons> b)"
- assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)"
+ and zero: "P 0"
+ and swap: "\<And>p a b. \<lbrakk>P p; supp p \<subseteq> S; a \<in> S; b \<in> S; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
shows "P p"
proof -
have "finite (supp p)" by (simp add: finite_supp)
- then show ?thesis using S
+ then show "P p" using S
proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct)
case (psubset p)
then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto
@@ -412,38 +392,42 @@
moreover
{ assume "supp p \<noteq> {}"
then obtain a where a0: "a \<in> supp p" by blast
- then have a1: "supp (- p \<bullet> a \<rightleftharpoons> a) \<subseteq> S" using as
+ then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a" using as
by (auto simp add: supp_atom supp_perm swap_atom)
- let ?q = "p + (- p \<bullet> a \<rightleftharpoons> a)"
+ let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p"
have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom)
moreover
have "a \<notin> supp ?q" by (simp add: supp_perm)
then have "supp ?q \<noteq> supp p" using a0 by auto
- ultimately have "supp ?q \<subset> supp p" using as by auto
+ ultimately have "supp ?q \<subset> supp p" using a2 by auto
then have "P ?q" using ih by simp
moreover
have "supp ?q \<subseteq> S" using as a2 by simp
- moreover
- have "P (- p \<bullet> a \<rightleftharpoons> a)" using a1 swap by simp
- ultimately
- have "P (?q + (- p \<bullet> a \<rightleftharpoons> a))" using a1 plus by simp
+ ultimately have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp
moreover
- have "p = ?q + (- p \<bullet> a \<rightleftharpoons> a)" by (simp add: expand_perm_eq)
+ have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: expand_perm_eq)
ultimately have "P p" by simp
}
ultimately show "P p" by blast
qed
qed
-lemma perm_subset_induct [consumes 1, case_names zero swap plus]:
+lemma perm_simple_struct_induct[case_names zero swap]:
+ assumes zero: "P 0"
+ and swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
+ shows "P p"
+by (rule_tac S="supp p" in perm_struct_induct)
+ (auto intro: zero swap)
+
+lemma perm_subset_induct[consumes 1, case_names zero swap plus]:
assumes S: "supp p \<subseteq> S"
assumes zero: "P 0"
assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)"
shows "P p"
-apply(rule perm_subset_induct_aux[OF S])
-apply(auto simp add: zero swap plus supp_swap split: if_splits)
-done
+using S
+by (induct p rule: perm_struct_induct)
+ (auto intro: zero plus swap simp add: supp_swap)
lemma supp_perm_eq:
assumes "(supp x) \<sharp>* p"
@@ -452,6 +436,23 @@
from assms have "supp p \<subseteq> {a. a \<sharp> x}"
unfolding supp_perm fresh_star_def fresh_def by auto
then show "p \<bullet> x = x"
+ proof (induct p rule: perm_struct_induct)
+ case zero
+ show "0 \<bullet> x = x" by simp
+ next
+ case (swap p a b)
+ then have "a \<sharp> x" "b \<sharp> x" "p \<bullet> x = x" by simp_all
+ then show "((a \<rightleftharpoons> b) + p) \<bullet> x = x" by (simp add: swap_fresh_fresh)
+ qed
+qed
+
+lemma supp_perm_eq_test:
+ assumes "(supp x) \<sharp>* p"
+ shows "p \<bullet> x = x"
+proof -
+ from assms have "supp p \<subseteq> {a. a \<sharp> x}"
+ unfolding supp_perm fresh_star_def fresh_def by auto
+ then show "p \<bullet> x = x"
proof (induct p rule: perm_subset_induct)
case zero
show "0 \<bullet> x = x" by simp
--- a/Nominal-General/nominal_eqvt.ML Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML Mon Apr 26 10:01:13 2010 +0200
@@ -9,7 +9,7 @@
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
+ val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic
end
structure Nominal_Eqvt : NOMINAL_EQVT =
@@ -27,9 +27,10 @@
(**
- proves F[f t] from F[t] which is the given theorem
+ given the theorem F[t]; proves the theorem F[f t]
+
- F needs to be monotone
- - f returns either SOME for a term it fires
+ - f returns either SOME for a term it fires on
and NONE elsewhere
**)
fun map_term f t =
@@ -90,7 +91,7 @@
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 =
+fun eqvt_rel_single_case_tac ctxt pred_names pi intro =
let
val thy = ProofContext.theory_of ctxt
val cpi = Thm.cterm_of thy (mk_minus pi)
@@ -113,7 +114,7 @@
fun eqvt_rel_tac ctxt pred_names pi induct intros =
let
- val cases = map (eqvt_rel_case_tac ctxt pred_names pi) intros
+ val cases = map (eqvt_rel_single_case_tac ctxt pred_names pi) intros
in
EVERY' (rtac induct :: cases)
end
@@ -150,9 +151,10 @@
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 (([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));
@@ -171,7 +173,7 @@
val _ =
OuterSyntax.local_theory "equivariance"
- "prove equivariance for inductive predicate involving nominal datatypes"
+ "Proves equivariance for inductive predicate involving nominal datatypes."
K.thy_decl (P.xname >> equivariance);
end;
--- a/Nominal-General/nominal_permeq.ML Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML Mon Apr 26 10:01:13 2010 +0200
@@ -7,6 +7,11 @@
sig
val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic
val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic
+
+ val perm_simp_meth: thm list * string list -> Proof.context -> Method.method
+ val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method
+ val args_parser: (thm list * string list) context_parser
+
val trace_eqvt: bool Config.T
val setup: theory -> theory
end;
@@ -157,4 +162,21 @@
val setup =
trace_eqvt_setup
+
+(** methods **)
+
+val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [];
+val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |--
+ (Scan.repeat (Args.const true))) []
+
+val args_parser =
+ add_thms_parser -- exclude_consts_parser ||
+ exclude_consts_parser -- add_thms_parser >> swap
+
+fun perm_simp_meth (thms, consts) ctxt =
+ SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts))
+
+fun perm_strict_simp_meth (thms, consts) ctxt =
+ SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts))
+
end; (* structure *)
\ No newline at end of file
--- a/Nominal-General/nominal_thmdecls.ML Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal-General/nominal_thmdecls.ML Mon Apr 26 10:01:13 2010 +0200
@@ -45,7 +45,8 @@
fun get_ps trm =
case trm of
- Const (@{const_name permute}, _) $ p $ (Bound _) => raise TERM ("get_ps", [trm])
+ Const (@{const_name permute}, _) $ p $ (Bound _) =>
+ raise TERM ("get_ps called on bound", [trm])
| Const (@{const_name permute}, _) $ p $ _ => [p]
| t $ u => get_ps t @ get_ps u
| Abs (_, _, t) => get_ps t
@@ -59,7 +60,8 @@
| 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 *)
+(* tests whether there is a disagreement between the permutations,
+ and that there is at least one permutation *)
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
@@ -88,8 +90,7 @@
fun add_raw_thm thm =
case prop_of thm of
- Const ("==", _) $ _ $ _ =>
- EqvtRawData.map (Item_Net.update (zero_var_indexes thm))
+ Const ("==", _) $ _ $ _ => (EqvtRawData.map o Item_Net.update) thm
| _ => raise THM ("Theorem must be a meta-equality", 0, [thm])
val del_raw_thm = EqvtRawData.map o Item_Net.remove;
@@ -98,7 +99,7 @@
(** transformation of eqvt lemmas **)
-(* transforms equations into the "p o c = c"-form
+(* transforms equations into the "p o c == c"-form
from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *)
fun eqvt_transform_eq_tac thm =
@@ -113,18 +114,21 @@
fun eqvt_transform_eq ctxt thm =
let
- 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 (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))
+ handle TERM _ => error "Equivariance lemma must be an equality."
+ val (p, t) = dest_perm lhs
+ handle TERM _ => error "Equivariance 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)
+ val msg = "Equivariance lemma is not of the right form "
in
if c <> c'
- then error "Eqvt lemma is not of the right form (constants do not agree)"
+ then error (msg ^ "(constants do not agree).")
else if is_bad_list (p::ps)
- then error "Eqvt lemma is not of the right form (permutations do not agree)"
+ then error (msg ^ "(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)"
+ then error (msg ^ "(arguments do not agree).")
else if is_Const t
then safe_mk_equiv thm
else
@@ -135,14 +139,16 @@
Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1)
|> singleton (ProofContext.export ctxt' ctxt)
|> safe_mk_equiv
+ |> zero_var_indexes
end
end
-(* transforms equations into the "p o c = c"-form
+(* transforms equations into the "p o c == c"-form
from R x1 ...xn ==> R (p o x1) ... (p o xn) *)
-fun eqvt_transform_imp_tac thy p p' thm =
+fun eqvt_transform_imp_tac ctxt p p' thm =
let
+ val thy = ProofContext.theory_of ctxt
val cp = Thm.cterm_of thy p
val cp' = Thm.cterm_of thy (mk_minus p')
val thm' = Drule.cterm_instantiate [(cp, cp')] thm
@@ -154,18 +160,18 @@
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, c') = (head_of prem, head_of concl)
val ps = get_ps concl handle TERM _ => []
val p = try hd ps
+ val msg = "Equivariance lemma is not of the right form "
in
if c <> c'
- then error "Eqvt lemma is not of the right form (constants do not agree)"
+ then error (msg ^ "(constants do not agree).")
else if is_bad_list ps
- then error "Eqvt lemma is not of the right form (permutations do not agree)"
+ then error (msg ^ "(permutations do not agree).")
else if not (concl aconv (put_p (the p) prem))
- then error "Eqvt lemma is not of the right form (arguments do not agree)"
+ then error (msg ^ "(arguments do not agree).")
else
let
val prem' = mk_perm (the p) prem
@@ -173,7 +179,7 @@
val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt
in
Goal.prove ctxt' [] [] goal'
- (fn _ => eqvt_transform_imp_tac thy (the p) p' thm 1)
+ (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1)
|> singleton (ProofContext.export ctxt' ctxt)
|> eqvt_transform_eq ctxt
end
--- a/Nominal/Abs.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal/Abs.thy Mon Apr 26 10:01:13 2010 +0200
@@ -2,8 +2,8 @@
imports "../Nominal-General/Nominal2_Atoms"
"../Nominal-General/Nominal2_Eqvt"
"../Nominal-General/Nominal2_Supp"
- "Nominal2_FSet"
"Quotient"
+ "Quotient_List"
"Quotient_Product"
begin
@@ -129,16 +129,22 @@
by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
quotient_definition
+ Abs ("[_]set. _" [60, 60] 60)
+where
"Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen"
is
"Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
quotient_definition
+ Abs_res ("[_]res. _" [60, 60] 60)
+where
"Abs_res::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_res"
is
"Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
quotient_definition
+ Abs_lst ("[_]lst. _" [60, 60] 60)
+where
"Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst"
is
"Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)"
@@ -169,9 +175,8 @@
shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
- apply(simp_all add: alphas_abs)
- apply(lifting alphas_abs)
- done
+ unfolding alphas_abs
+ by (lifting alphas_abs)
instantiation abs_gen :: (pt) pt
begin
@@ -327,9 +332,8 @@
shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (Abs bs x)"
and "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"
- apply(rule_tac [!] fresh_fun_eqvt_app)
- apply(simp_all add: eqvts_raw)
- done
+ by (rule_tac [!] fresh_fun_eqvt_app)
+ (simp_all add: eqvts_raw)
lemma supp_abs_subset1:
assumes a: "finite (supp x)"
@@ -337,36 +341,32 @@
and "(supp x) - as \<subseteq> supp (Abs_res as x)"
and "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"
unfolding supp_conv_fresh
- apply(auto dest!: aux_fresh)
- apply(simp_all add: fresh_def supp_finite_atom_set a)
- done
+ by (auto dest!: aux_fresh)
+ (simp_all add: fresh_def supp_finite_atom_set a)
lemma supp_abs_subset2:
assumes a: "finite (supp x)"
shows "supp (Abs as x) \<subseteq> (supp x) - as"
and "supp (Abs_res as x) \<subseteq> (supp x) - as"
and "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)"
- apply(rule_tac [!] supp_is_subset)
- apply(simp_all add: abs_supports a)
- done
+ by (rule_tac [!] supp_is_subset)
+ (simp_all add: abs_supports a)
lemma abs_finite_supp:
assumes a: "finite (supp x)"
shows "supp (Abs as x) = (supp x) - as"
and "supp (Abs_res as x) = (supp x) - as"
and "supp (Abs_lst bs x) = (supp x) - (set bs)"
- apply(rule_tac [!] subset_antisym)
- apply(simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
- done
+ by (rule_tac [!] subset_antisym)
+ (simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
lemma supp_abs:
fixes x::"'a::fs"
shows "supp (Abs as x) = (supp x) - as"
and "supp (Abs_res as x) = (supp x) - as"
and "supp (Abs_lst bs x) = (supp x) - (set bs)"
- apply(rule_tac [!] abs_finite_supp)
- apply(simp_all add: finite_supp)
- done
+ by (rule_tac [!] abs_finite_supp)
+ (simp_all add: finite_supp)
instance abs_gen :: (fs) fs
apply(default)
@@ -397,101 +397,12 @@
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
-
-lemma
- fixes t1 s1::"'a::fs"
- and t2 s2::"'b::fs"
- shows "Abs as (t1, t2) = Abs bs (s1, s2) \<longrightarrow> (Abs as t1 = Abs bs s1 \<and> Abs as t2 = Abs bs 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
-
-lemma fresh_star_eq:
- assumes a: "as \<sharp>* p"
- shows "\<forall>a \<in> as. p \<bullet> a = a"
-using a by (simp add: fresh_star_def fresh_def supp_perm)
-
-lemma fresh_star_set_eq:
- assumes a: "as \<sharp>* p"
- shows "p \<bullet> as = as"
-using a
-apply(simp add: fresh_star_def fresh_def supp_perm permute_set_eq)
-apply(auto)
-by (metis permute_atom_def)
-
-lemma
- fixes t1 s1::"'a::fs"
- and t2 s2::"'b::fs"
- assumes asm: "finite as"
- shows "(Abs as t1 = Abs bs s1 \<and> Abs as t2 = Abs bs s2) \<longrightarrow> Abs as (t1, t2) = Abs bs (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:
fixes as::"'a::at_base set"
shows "supp (atom ` as) = supp as"
apply(simp add: supp_def)
apply(simp add: image_eqvt)
-apply(simp add: atom_eqvt_raw)
+apply(simp add: eqvts_raw)
apply(simp add: atom_image_cong)
done
--- a/Nominal/Ex/Ex1rec.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal/Ex/Ex1rec.thy Mon Apr 26 10:01:13 2010 +0200
@@ -6,27 +6,27 @@
ML {* val _ = recursive := true *}
ML {* val _ = alpha_type := AlphaGen *}
-nominal_datatype lam' =
- VAR' "name"
-| APP' "lam'" "lam'"
-| LAM' x::"name" t::"lam'" bind x in t
-| LET' bp::"bp'" t::"lam'" bind "bi' bp" in t
-and bp' =
- BP' "name" "lam'"
+nominal_datatype lam =
+ VAR "name"
+| APP "lam" "lam"
+| LAM x::"name" t::"lam" bind x in t
+| LET bp::"bp" t::"lam" bind "bi bp" in t
+and bp =
+ BP "name" "lam"
binder
- bi'::"bp' \<Rightarrow> atom set"
+ bi::"bp \<Rightarrow> atom set"
where
- "bi' (BP' x t) = {atom x}"
+ "bi (BP x t) = {atom x}"
-thm lam'_bp'.fv
-thm lam'_bp'.eq_iff[no_vars]
-thm lam'_bp'.bn
-thm lam'_bp'.perm
-thm lam'_bp'.induct
-thm lam'_bp'.inducts
-thm lam'_bp'.distinct
-ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
-thm lam'_bp'.fv[simplified lam'_bp'.supp]
+thm lam_bp.fv
+thm lam_bp.eq_iff[no_vars]
+thm lam_bp.bn
+thm lam_bp.perm
+thm lam_bp.induct
+thm lam_bp.inducts
+thm lam_bp.distinct
+ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
+thm lam_bp.fv[simplified lam_bp.supp]
end
--- a/Nominal/Ex/ExPS8.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal/Ex/ExPS8.thy Mon Apr 26 10:01:13 2010 +0200
@@ -11,41 +11,41 @@
the reference. *)
ML {* val _ = recursive := false *}
-nominal_datatype exp8 =
+nominal_datatype exp =
EVar name
| EUnit
-| EPair exp8 exp8
-| ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e (* rec *)
+| EPair exp exp
+| ELetRec l::lrbs e::exp bind "b_lrbs l" in e (* rec *)
and fnclause =
- K x::name p::pat8 f::exp8 bind "b_pat p" in f (* non-rec *)
+ K x::name p::pat f::exp bind "b_pat p" in f (* non-rec *)
and fnclauses =
S fnclause
| ORs fnclause fnclauses
-and lrb8 =
+and lrb =
Clause fnclauses
-and lrbs8 =
- Single lrb8
-| More lrb8 lrbs8
-and pat8 =
+and lrbs =
+ Single lrb
+| More lrb lrbs
+and pat =
PVar name
| PUnit
-| PPair pat8 pat8
+| PPair pat pat
binder
- b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and
- b_pat :: "pat8 \<Rightarrow> atom set" and
+ b_lrbs :: "lrbs \<Rightarrow> atom set" and
+ b_pat :: "pat \<Rightarrow> atom set" and
b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
b_fnclause :: "fnclause \<Rightarrow> atom set" and
- b_lrb8 :: "lrb8 \<Rightarrow> atom set"
+ b_lrb :: "lrb \<Rightarrow> atom set"
where
- "b_lrbs8 (Single l) = b_lrb8 l"
-| "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 ls"
+ "b_lrbs (Single l) = b_lrb l"
+| "b_lrbs (More l ls) = b_lrb l \<union> b_lrbs ls"
| "b_pat (PVar x) = {atom x}"
| "b_pat (PUnit) = {}"
| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
| "b_fnclauses (S fc) = (b_fnclause fc)"
| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
-| "b_lrb8 (Clause fcs) = (b_fnclauses fcs)"
-| "b_fnclause (K x pat exp8) = {atom x}"
+| "b_lrb (Clause fcs) = (b_fnclauses fcs)"
+| "b_fnclause (K x pat exp) = {atom x}"
thm exp7_lrb_lrbs.eq_iff
thm exp7_lrb_lrbs.supp
--- a/Nominal/Ex/Lambda.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal/Ex/Lambda.thy Mon Apr 26 10:01:13 2010 +0200
@@ -126,44 +126,109 @@
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 \<or> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
+ | 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"
-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"
-
-inductive
- typing2' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ 2\<Turnstile> _ : _" [60,60,60] 60)
-where
- 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"
-
-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"
-
equivariance valid
equivariance typing
-equivariance typing'
-equivariance typing2'
-equivariance typing''
thm valid.eqvt
thm typing.eqvt
thm eqvts
thm eqvts_raw
+thm typing.induct[of "\<Gamma>" "t" "T", no_vars]
+
+lemma
+ fixes c::"'a::fs"
+ assumes a: "\<Gamma> \<turnstile> t : T"
+ and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T"
+ and a2: "\<And>\<Gamma> t1 T1 T2 t2 c. \<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<And>d. P d \<Gamma> t1 T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1; \<And>d. P d \<Gamma> t2 T1\<rbrakk>
+ \<Longrightarrow> P c \<Gamma> (App t1 t2) T2"
+ and a3: "\<And>x \<Gamma> T1 t T2 c. \<lbrakk>atom x \<sharp> c; atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2; \<And>d. P d ((x, T1) # \<Gamma>) t T2\<rbrakk>
+ \<Longrightarrow> P c \<Gamma> (Lam x t) T1 \<rightarrow> T2"
+ shows "P c \<Gamma> t T"
+proof -
+ from a have "\<And>p c. P c (p \<bullet> \<Gamma>) (p \<bullet> t) (p \<bullet> T)"
+ proof (induct)
+ case (t_Var \<Gamma> x T p c)
+ then show ?case
+ apply -
+ apply(perm_strict_simp)
+ apply(rule a1)
+ apply(rule_tac p="-p" in permute_boolE)
+ apply(perm_strict_simp add: permute_minus_cancel)
+ apply(assumption)
+ apply(rule_tac p="-p" in permute_boolE)
+ apply(perm_strict_simp add: permute_minus_cancel)
+ apply(assumption)
+ done
+ next
+ case (t_App \<Gamma> t1 T1 T2 t2 p c)
+ then show ?case
+ apply -
+ apply(perm_strict_simp)
+ apply(rule_tac ?T1.0="p \<bullet> T1" in a2)
+ apply(rule_tac p="-p" in permute_boolE)
+ apply(perm_strict_simp add: permute_minus_cancel)
+ apply(assumption)
+ apply(assumption)
+ apply(rule_tac p="-p" in permute_boolE)
+ apply(perm_strict_simp add: permute_minus_cancel)
+ apply(assumption)
+ apply(assumption)
+ done
+ next
+ case (t_Lam x \<Gamma> T1 t T2 p c)
+ then show ?case
+ apply -
+ apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom x}) \<sharp>* c \<and>
+ supp (p \<bullet> \<Gamma>, p \<bullet> Lam x t, p \<bullet> (T1 \<rightarrow> T2)) \<sharp>* q")
+ apply(erule exE)
+ apply(rule_tac t="p \<bullet> \<Gamma>" and s="q \<bullet> p \<bullet> \<Gamma>" in subst)
+ apply(rule supp_perm_eq)
+ apply(simp add: supp_Pair fresh_star_union)
+ apply(rule_tac t="p \<bullet> Lam x t" and s="q \<bullet> p \<bullet> Lam x t" in subst)
+ apply(rule supp_perm_eq)
+ apply(simp add: supp_Pair fresh_star_union)
+ apply(rule_tac t="p \<bullet> (T1 \<rightarrow> T2)" and s="q \<bullet> p \<bullet> (T1 \<rightarrow> T2)" in subst)
+ apply(rule supp_perm_eq)
+ apply(simp add: supp_Pair fresh_star_union)
+ apply(simp add: eqvts)
+ apply(rule a3)
+ apply(simp add: fresh_star_def)
+ apply(rule_tac p="-q" in permute_boolE)
+ apply(perm_strict_simp add: permute_minus_cancel)
+ apply(rule_tac p="-p" in permute_boolE)
+ apply(perm_strict_simp add: permute_minus_cancel)
+ apply(assumption)
+ apply(rule_tac p="-q" in permute_boolE)
+ apply(perm_strict_simp add: permute_minus_cancel)
+ apply(rule_tac p="-p" in permute_boolE)
+ apply(perm_strict_simp add: permute_minus_cancel)
+ apply(assumption)
+ apply(drule_tac x="d" in meta_spec)
+ apply(drule_tac x="q + p" in meta_spec)
+ apply(simp)
+ apply(rule at_set_avoiding2)
+ apply(simp add: finite_supp)
+ apply(simp add: finite_supp)
+ apply(simp add: finite_supp)
+ apply(rule_tac p="-p" in permute_boolE)
+ apply(perm_strict_simp add: permute_minus_cancel)
+ (* supplied by the user *)
+ apply(simp add: fresh_star_prod)
+ apply(simp add: fresh_star_def)
+
+
+ done
+(* HERE *)
+
+
+
+
+
+
inductive
tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
@@ -189,27 +254,9 @@
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 {* 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:
@@ -367,6 +414,29 @@
done
*)
+
+ML {*
+
+fun prove_strong_ind (pred_name, avoids) ctxt =
+ Proof.theorem NONE (K I) [] ctxt
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val _ =
+ OuterSyntax.local_theory_to_proof "nominal_inductive"
+ "proves strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
+ (P.xname -- (Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name --
+ (P.$$$ ":" |-- P.and_list1 P.term))) []) >> prove_strong_ind)
+
+end;
+
+*}
+
+(*
+nominal_inductive typing
+*)
+
+
end
--- a/Nominal/Ex/TypeSchemes.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal/Ex/TypeSchemes.thy Mon Apr 26 10:01:13 2010 +0200
@@ -108,10 +108,9 @@
apply (simp add: fin_fset_to_set)
apply (simp add: finite_supp)
apply (simp add: eqvts finite_supp)
- apply (subst atom_eqvt_raw[symmetric])
- apply (subst fmap_eqvt[symmetric])
- apply (subst fset_to_set_eqvt[symmetric])
- apply (simp only: fresh_star_permute_iff)
+ apply (rule_tac p=" -p" in permute_boolE)
+ apply(simp add: eqvts)
+ apply(simp add: permute_fun_def atom_eqvt)
apply (simp add: fresh_star_def)
apply clarify
apply (simp add: fresh_def)
--- a/Nominal/FSet.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal/FSet.thy Mon Apr 26 10:01:13 2010 +0200
@@ -71,6 +71,85 @@
else f a (ffold_raw f z A)
else z)"
+text {* Composition Quotient *}
+
+lemma list_rel_refl:
+ shows "(list_rel op \<approx>) r r"
+ by (rule list_rel_refl) (metis equivp_def fset_equivp)
+
+lemma compose_list_refl:
+ shows "(list_rel op \<approx> OOO op \<approx>) r r"
+proof
+ show c: "list_rel op \<approx> r r" by (rule list_rel_refl)
+ have d: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
+ show b: "(op \<approx> OO list_rel op \<approx>) r r" by (rule pred_compI) (rule d, rule c)
+qed
+
+lemma Quotient_fset_list:
+ shows "Quotient (list_rel op \<approx>) (map abs_fset) (map rep_fset)"
+ by (fact list_quotient[OF Quotient_fset])
+
+lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
+ by (rule eq_reflection) auto
+
+lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
+ unfolding list_eq.simps
+ by (simp only: set_map set_in_eq)
+
+lemma quotient_compose_list[quot_thm]:
+ shows "Quotient ((list_rel op \<approx>) OOO (op \<approx>))
+ (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
+ unfolding Quotient_def comp_def
+proof (intro conjI allI)
+ fix a r s
+ show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a"
+ by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
+ have b: "list_rel op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
+ by (rule list_rel_refl)
+ have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
+ by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
+ show "(list_rel op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
+ by (rule, rule list_rel_refl) (rule c)
+ show "(list_rel op \<approx> OOO op \<approx>) r s = ((list_rel op \<approx> OOO op \<approx>) r r \<and>
+ (list_rel op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
+ proof (intro iffI conjI)
+ show "(list_rel op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl)
+ show "(list_rel op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
+ next
+ assume a: "(list_rel op \<approx> OOO op \<approx>) r s"
+ then have b: "map abs_fset r \<approx> map abs_fset s" proof (elim pred_compE)
+ fix b ba
+ assume c: "list_rel op \<approx> r b"
+ assume d: "b \<approx> ba"
+ assume e: "list_rel op \<approx> ba s"
+ have f: "map abs_fset r = map abs_fset b"
+ using Quotient_rel[OF Quotient_fset_list] c by blast
+ have "map abs_fset ba = map abs_fset s"
+ using Quotient_rel[OF Quotient_fset_list] e by blast
+ then have g: "map abs_fset s = map abs_fset ba" by simp
+ then show "map abs_fset r \<approx> map abs_fset s" using d f map_rel_cong by simp
+ qed
+ then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
+ using Quotient_rel[OF Quotient_fset] by blast
+ next
+ assume a: "(list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s
+ \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
+ then have s: "(list_rel op \<approx> OOO op \<approx>) s s" by simp
+ have d: "map abs_fset r \<approx> map abs_fset s"
+ by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
+ have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)"
+ by (rule map_rel_cong[OF d])
+ have y: "list_rel op \<approx> (map rep_fset (map abs_fset s)) s"
+ by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_rel_refl[of s]])
+ have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (map abs_fset r)) s"
+ by (rule pred_compI) (rule b, rule y)
+ have z: "list_rel op \<approx> r (map rep_fset (map abs_fset r))"
+ by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_rel_refl[of r]])
+ then show "(list_rel op \<approx> OOO op \<approx>) r s"
+ using a c pred_compI by simp
+ qed
+qed
+
text {* Respectfullness *}
lemma [quot_respect]:
@@ -178,7 +257,7 @@
apply (induct b)
apply (simp_all add: not_memb_nil)
apply (auto)
- apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident rsp_fold_def memb_cons_iff)
+ apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident rsp_fold_def memb_cons_iff)
done
lemma ffold_raw_rsp_pre:
@@ -217,6 +296,44 @@
"(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
by (simp add: memb_def[symmetric] ffold_raw_rsp_pre)
+lemma concat_rsp_pre:
+ assumes a: "list_rel op \<approx> x x'"
+ and b: "x' \<approx> y'"
+ and c: "list_rel op \<approx> y' y"
+ and d: "\<exists>x\<in>set x. xa \<in> set x"
+ shows "\<exists>x\<in>set y. xa \<in> set x"
+proof -
+ obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
+ have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_rel_find_element[OF e a])
+ then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
+ have j: "ya \<in> set y'" using b h by simp
+ have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" by (rule list_rel_find_element[OF j c])
+ then show ?thesis using f i by auto
+qed
+
+lemma [quot_respect]:
+ shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
+proof (rule fun_relI, elim pred_compE)
+ fix a b ba bb
+ assume a: "list_rel op \<approx> a ba"
+ assume b: "ba \<approx> bb"
+ assume c: "list_rel op \<approx> bb b"
+ have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+ fix x
+ show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
+ assume d: "\<exists>xa\<in>set a. x \<in> set xa"
+ show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
+ next
+ assume e: "\<exists>xa\<in>set b. x \<in> set xa"
+ have a': "list_rel op \<approx> ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a])
+ have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
+ have c': "list_rel op \<approx> b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c])
+ show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
+ qed
+ qed
+ then show "concat a \<approx> concat b" by simp
+qed
+
text {* Distributive lattice with bot *}
lemma sub_list_not_eq:
@@ -375,11 +492,124 @@
"fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb"
abbreviation
- fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
+ fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50)
where
"x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
-section {* Augmenting an fset -- @{const finsert} *}
+section {* Other constants on the Quotient Type *}
+
+quotient_definition
+ "fcard :: 'a fset \<Rightarrow> nat"
+is
+ "fcard_raw"
+
+quotient_definition
+ "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
+is
+ "map"
+
+quotient_definition
+ "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset"
+ is "delete_raw"
+
+quotient_definition
+ "fset_to_set :: 'a fset \<Rightarrow> 'a set"
+ is "set"
+
+quotient_definition
+ "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
+ is "ffold_raw"
+
+quotient_definition
+ "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
+is
+ "concat"
+
+text {* Compositional Respectfullness and Preservation *}
+
+lemma [quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"
+ by (fact compose_list_refl)
+
+lemma [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
+ by simp
+
+lemma [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)
+ apply (rule_tac b="x # b" in pred_compI)
+ apply auto
+ apply (rule_tac b="x # ba" in pred_compI)
+ apply auto
+ done
+
+lemma [quot_preserve]:
+ "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
+ by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
+ abs_o_rep[OF Quotient_fset] map_id finsert_def)
+
+lemma [quot_preserve]:
+ "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion"
+ by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
+ abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
+
+lemma list_rel_app_l:
+ assumes a: "reflp R"
+ and b: "list_rel R l r"
+ shows "list_rel R (z @ l) (z @ r)"
+ by (induct z) (simp_all add: b rev_iffD1[OF a meta_eq_to_obj_eq[OF reflp_def]])
+
+lemma append_rsp2_pre0:
+ assumes a:"list_rel op \<approx> x x'"
+ shows "list_rel op \<approx> (x @ z) (x' @ z)"
+ using a apply (induct x x' rule: list_induct2')
+ by simp_all (rule list_rel_refl)
+
+lemma append_rsp2_pre1:
+ assumes a:"list_rel op \<approx> x x'"
+ shows "list_rel op \<approx> (z @ x) (z @ x')"
+ using a apply (induct x x' arbitrary: z rule: list_induct2')
+ apply (rule list_rel_refl)
+ apply (simp_all del: list_eq.simps)
+ apply (rule list_rel_app_l)
+ apply (simp_all add: reflp_def)
+ done
+
+lemma append_rsp2_pre:
+ assumes a:"list_rel op \<approx> x x'"
+ and b: "list_rel op \<approx> z z'"
+ shows "list_rel op \<approx> (x @ z) (x' @ z')"
+ apply (rule list_rel_transp[OF fset_equivp])
+ apply (rule append_rsp2_pre0)
+ apply (rule a)
+ using b apply (induct z z' rule: list_induct2')
+ apply (simp_all only: append_Nil2)
+ apply (rule list_rel_refl)
+ apply simp_all
+ apply (rule append_rsp2_pre1)
+ apply simp
+ done
+
+lemma [quot_respect]:
+ "(list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op @ op @"
+proof (intro fun_relI, elim pred_compE)
+ fix x y z w x' z' y' w' :: "'a list list"
+ assume a:"list_rel op \<approx> x x'"
+ and b: "x' \<approx> y'"
+ and c: "list_rel op \<approx> y' y"
+ assume aa: "list_rel op \<approx> z z'"
+ and bb: "z' \<approx> w'"
+ and cc: "list_rel op \<approx> w' w"
+ have a': "list_rel op \<approx> (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto
+ have b': "x' @ z' \<approx> y' @ w'" using b bb by simp
+ have c': "list_rel op \<approx> (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto
+ have d': "(op \<approx> OO list_rel op \<approx>) (x' @ z') (y @ w)"
+ by (rule pred_compI) (rule b', rule c')
+ show "(list_rel op \<approx> OOO op \<approx>) (x @ z) (y @ w)"
+ by (rule pred_compI) (rule a', rule d')
+qed
+
+text {* Raw theorems. Finsert, memb, singleron, sub_list *}
lemma nil_not_cons:
shows "\<not> ([] \<approx> x # xs)"
@@ -398,30 +628,20 @@
shows "memb x xs \<Longrightarrow> memb x (y # xs)"
by (simp add: memb_def)
-section {* Singletons *}
-
lemma singleton_list_eq:
shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
by (simp add: id_simps) auto
-section {* sub_list *}
-
lemma sub_list_cons:
"sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
by (auto simp add: memb_def sub_list_def)
-section {* Cardinality of finite sets *}
-
-quotient_definition
- "fcard :: 'a fset \<Rightarrow> nat"
-is
- "fcard_raw"
+text {* Cardinality of finite sets *}
lemma fcard_raw_0:
shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
by (induct xs) (auto simp add: memb_def)
-
lemma fcard_raw_not_memb:
shows "\<not> memb x xs \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)"
by auto
@@ -432,7 +652,7 @@
using a
by (induct xs) (auto simp add: memb_def split: if_splits)
-lemma singleton_fcard_1:
+lemma singleton_fcard_1:
shows "set xs = {x} \<Longrightarrow> fcard_raw xs = 1"
by (induct xs) (auto simp add: memb_def subset_insert)
@@ -451,11 +671,7 @@
assumes a: "fcard_raw A = Suc n"
shows "\<exists>a. memb a A"
using a
- apply (induct A)
- apply simp
- apply (rule_tac x="a" in exI)
- apply (simp add: memb_def)
- done
+ by (induct A) (auto simp add: memb_def)
lemma memb_card_not_0:
assumes a: "memb a A"
@@ -466,12 +682,7 @@
then show ?thesis using fcard_raw_0[of A] by simp
qed
-section {* fmap *}
-
-quotient_definition
- "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
-is
- "map"
+text {* fmap *}
lemma map_append:
"map f (xs @ ys) \<approx> (map f xs) @ (map f ys)"
@@ -526,28 +737,10 @@
"fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
by (simp add: fdelete_raw_filter fcard_raw_delete_one)
-
-
-
-
lemma finter_raw_empty:
"finter_raw l [] = []"
by (induct l) (simp_all add: not_memb_nil)
-section {* Constants on the Quotient Type *}
-
-quotient_definition
- "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset"
- is "delete_raw"
-
-quotient_definition
- "fset_to_set :: 'a fset \<Rightarrow> 'a set"
- is "set"
-
-quotient_definition
- "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
- is "ffold_raw"
-
lemma set_cong:
shows "(set x = set y) = (x \<approx> y)"
by auto
@@ -556,12 +749,6 @@
"inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
by (simp add: expand_set_eq[symmetric] inj_image_eq_iff)
-quotient_definition
- "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
-is
- "concat"
-
-
text {* alternate formulation with a different decomposition principle
and a proof of equivalence *}
@@ -604,42 +791,44 @@
"xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x"
by (simp add: memb_def[symmetric] memb_delete_raw)
-lemma list_eq2_equiv_aux:
- assumes a: "fcard_raw l = n"
- and b: "l \<approx> r"
- shows "list_eq2 l r"
-using a b
-proof (induct n arbitrary: l r)
- case 0
- have "fcard_raw l = 0" by fact
- then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
- then have z: "l = []" using no_memb_nil by auto
- then have "r = []" using `l \<approx> r` by simp
- then show ?case using z list_eq2_refl by simp
-next
- case (Suc m)
- have b: "l \<approx> r" by fact
- have d: "fcard_raw l = Suc m" by fact
- have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb[OF d])
- then obtain a where e: "memb a l" by auto
- then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto
- have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp
- have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp
- have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
- have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g'])
- have i: "list_eq2 l (a # delete_raw l a)" by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
- have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h])
- then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp
-qed
-
lemma list_eq2_equiv:
"(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)"
proof
show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto
- show "l \<approx> r \<Longrightarrow> list_eq2 l r" using list_eq2_equiv_aux by blast
+next
+ {
+ fix n
+ assume a: "fcard_raw l = n" and b: "l \<approx> r"
+ have "list_eq2 l r"
+ using a b
+ proof (induct n arbitrary: l r)
+ case 0
+ have "fcard_raw l = 0" by fact
+ then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
+ then have z: "l = []" using no_memb_nil by auto
+ then have "r = []" using `l \<approx> r` by simp
+ then show ?case using z list_eq2_refl by simp
+ next
+ case (Suc m)
+ have b: "l \<approx> r" by fact
+ have d: "fcard_raw l = Suc m" by fact
+ have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb[OF d])
+ then obtain a where e: "memb a l" by auto
+ then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto
+ have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp
+ have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp
+ have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
+ have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g'])
+ have i: "list_eq2 l (a # delete_raw l a)"
+ by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
+ have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h])
+ then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp
+ qed
+ }
+ then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
qed
-section {* lifted part *}
+text {* Lifted theorems *}
lemma not_fin_fnil: "x |\<notin>| {||}"
by (lifting not_memb_nil)
@@ -742,10 +931,6 @@
shows "S |\<union>| {||} = S"
by (lifting append_Nil2)
-thm sup.commute[where 'a="'a fset"]
-
-thm sup.assoc[where 'a="'a fset"]
-
lemma singleton_union_left:
"{|a|} |\<union>| S = finsert a S"
by simp
@@ -779,15 +964,7 @@
case (finsert x S)
have asm: "P S" by fact
show "P (finsert x S)"
- proof(cases "x |\<in>| S")
- case True
- have "x |\<in>| S" by fact
- then show "P (finsert x S)" using asm by simp
- next
- case False
- have "x |\<notin>| S" by fact
- then show "P (finsert x S)" using prem2 asm by simp
- qed
+ by (cases "x |\<in>| S") (simp_all add: asm prem2)
qed
lemma fset_induct2:
@@ -876,7 +1053,8 @@
"(finsert x xs |\<subseteq>| ys) = (x |\<in>| ys \<and> xs |\<subseteq>| ys)"
by (lifting sub_list_cons)
-thm sub_list_def[simplified memb_def[symmetric], quot_lifted, no_vars]
+lemma "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys"
+ by (lifting sub_list_def[simplified memb_def[symmetric]])
lemma fsubset_fin: "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
by (rule meta_eq_to_obj_eq)
@@ -911,6 +1089,19 @@
using assms
by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
+text {* concat *}
+
+lemma fconcat_empty:
+ shows "fconcat {||} = {||}"
+ by (lifting concat.simps(1))
+
+lemma fconcat_insert:
+ shows "fconcat (finsert x S) = x |\<union>| fconcat S"
+ by (lifting concat.simps(2))
+
+lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
+ by (lifting concat_append)
+
ML {*
fun dest_fsetT (Type ("FSet.fset", [T])) = T
| dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
--- a/Nominal/Manual/Term8.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal/Manual/Term8.thy Mon Apr 26 10:01:13 2010 +0200
@@ -1,5 +1,5 @@
theory Term8
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
+imports "../../Nominal-General/Nominal2_Atoms" "../../Nominal-General/Nominal2_Eqvt" "../../Nominal-General/Nominal2_Supp" "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "../../Attic/Prove"
begin
atom_decl name
@@ -20,42 +20,55 @@
setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term8.rfoo8") 2 *}
print_theorems
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term8.rfoo8") [
- [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
+ML define_fv_alpha_export
+local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term8.rfoo8") [
+ [[], [(SOME (@{term rbv8}, false), 0, 1, AlphaGen)]], [[], [(NONE, 1, 2, AlphaGen)]]]
+ [(@{term "rbv8"}, 1, [[], [(0, NONE), (2, SOME @{term rbv8})]])] *}
notation
alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and
alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100)
-thm alpha_rfoo8_alpha_rbar8.intros
-
+thm alpha_rfoo8_alpha_rbar8_alpha_rbv8.intros[no_vars]
+thm fv_rbar8.simps fv_rfoo8_fv_rbv8.simps
inductive
alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100)
and
alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100)
+and
+ alpha8bv:: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>bv _" [100, 100] 100)
where
- a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)"
-| a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)"
-| a3: "b1 \<approx>b b2 \<Longrightarrow> (\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f fv_rfoo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2"
-| a4: "v1 = v2 \<Longrightarrow> (\<exists>pi. (({atom x1}, t1) \<approx>gen alpha8b fv_rbar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 t2"
+ "name = namea \<Longrightarrow> Foo0 name \<approx>f Foo0 namea"
+| "\<exists>pi. rbar8 \<approx>bv rbar8a \<and>
+ (rbv8 rbar8, rfoo8) \<approx>gen alpha8f fv_rfoo8 pi (rbv8 rbar8a, rfoo8a) \<Longrightarrow>
+ Foo1 rbar8 rfoo8 \<approx>f Foo1 rbar8a rfoo8a"
+| "name = namea \<Longrightarrow> Bar0 name \<approx>b Bar0 namea"
+| "\<exists>pi. name1 = name1a \<and> ({atom name2}, rbar8) \<approx>gen alpha8b fv_rbv8 pi ({atom name2a}, rbar8a) \<Longrightarrow>
+ Bar1 name1 name2 rbar8 \<approx>b Bar1 name1a name2a rbar8a"
+| "name = namea \<Longrightarrow> alpha8bv (Bar0 name) (Bar0 namea)"
+| "({atom name2}, rbar8) \<approx>gen alpha8b fv_rbv8 pi ({atom name2a}, rbar8a) \<Longrightarrow>
+ alpha8bv (Bar1 name1 name2 rbar8) (Bar1 name1a name2a rbar8a)"
lemma "(alpha8b ===> op =) rbv8 rbv8"
- apply simp apply clarify
- apply (erule alpha8f_alpha8b.inducts(2))
+ apply rule
+ apply (induct_tac a b rule: alpha8f_alpha8b_alpha8bv.inducts(2))
apply (simp_all)
-done
+ done
lemma fv_rbar8_rsp_hlp: "x \<approx>b y \<Longrightarrow> fv_rbar8 x = fv_rbar8 y"
- apply (erule alpha8f_alpha8b.inducts(2))
+ apply (erule alpha8f_alpha8b_alpha8bv.inducts(2))
apply (simp_all add: alpha_gen)
-done
+ apply clarify
+ sorry
+
lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8"
apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp)
-done
+ done
lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8"
apply simp apply clarify
- apply (erule alpha8f_alpha8b.inducts(1))
+ apply (erule alpha8f_alpha8b_alpha8bv.inducts(1))
apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)
+
done
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/NewParser.thy Mon Apr 26 10:01:13 2010 +0200
@@ -0,0 +1,510 @@
+theory NewParser
+imports "../Nominal-General/Nominal2_Atoms"
+ "../Nominal-General/Nominal2_Eqvt"
+ "../Nominal-General/Nominal2_Supp"
+ "Perm" "Equivp" "Rsp" "Lift"
+begin
+
+section{* Interface for nominal_datatype *}
+
+
+ML {*
+(* nominal datatype parser *)
+local
+ structure P = OuterParse;
+ structure S = Scan
+
+ fun triple1 ((x, y), z) = (x, y, z)
+ fun triple2 (x, (y, z)) = (x, y, z)
+ fun tuple ((x, y, z), u) = (x, y, z, u)
+ fun tswap (((x, y), z), u) = (x, y, u, z)
+in
+
+val _ = OuterKeyword.keyword "bind"
+val _ = OuterKeyword.keyword "bind_set"
+val _ = OuterKeyword.keyword "bind_res"
+
+val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
+
+val bind_mode = P.$$$ "bind" || P.$$$ "bind_set" || P.$$$ "bind_res"
+
+val bind_clauses =
+ P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1)
+
+val cnstr_parser =
+ P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tswap
+
+(* datatype parser *)
+val dt_parser =
+ (P.type_args -- P.binding -- P.opt_mixfix >> triple1) --
+ (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple
+
+(* binding function parser *)
+val bnfun_parser =
+ S.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([], [])
+
+(* main parser *)
+val main_parser =
+ P.and_list1 dt_parser -- bnfun_parser >> triple2
+
+end
+*}
+
+ML {*
+datatype bmodes =
+ BEmy of int
+| BLst of ((term option * int) list) * (int list)
+| BSet of ((term option * int) list) * (int list)
+| BRes of ((term option * int) list) * (int list)
+*}
+
+ML {*
+fun get_cnstrs dts =
+ map (fn (_, _, _, constrs) => constrs) dts
+
+fun get_typed_cnstrs dts =
+ flat (map (fn (_, bn, _, constrs) =>
+ (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts)
+
+fun get_cnstr_strs dts =
+ map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts))
+
+fun get_bn_fun_strs bn_funs =
+ map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs
+*}
+
+ML {*
+fun add_primrec_wrapper funs eqs lthy =
+ if null funs then (([], []), lthy)
+ else
+ let
+ val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs
+ val funs' = map (fn (bn, ty, mx) => (bn, SOME ty, mx)) funs
+ in
+ Primrec.add_primrec funs' eqs' lthy
+ end
+*}
+
+ML {*
+fun add_datatype_wrapper dt_names dts =
+let
+ val conf = Datatype.default_config
+in
+ Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts)
+end
+*}
+
+
+text {* Infrastructure for adding "_raw" to types and terms *}
+
+ML {*
+fun add_raw s = s ^ "_raw"
+fun add_raws ss = map add_raw ss
+fun raw_bind bn = Binding.suffix_name "_raw" bn
+
+fun replace_str ss s =
+ case (AList.lookup (op=) ss s) of
+ SOME s' => s'
+ | NONE => s
+
+fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts)
+ | replace_typ ty_ss T = T
+
+fun raw_dts ty_ss dts =
+let
+ fun raw_dts_aux1 (bind, tys, mx) =
+ (raw_bind bind, map (replace_typ ty_ss) tys, mx)
+
+ fun raw_dts_aux2 (ty_args, bind, mx, constrs) =
+ (ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs)
+in
+ map raw_dts_aux2 dts
+end
+
+fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T)
+ | replace_aterm trm_ss (Free (a, T)) = Free (replace_str trm_ss a, T)
+ | replace_aterm trm_ss trm = trm
+
+fun replace_term trm_ss ty_ss trm =
+ trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss)
+*}
+
+ML {*
+fun rawify_dts dt_names dts dts_env =
+let
+ val raw_dts = raw_dts dts_env dts
+ val raw_dt_names = add_raws dt_names
+in
+ (raw_dt_names, raw_dts)
+end
+*}
+
+ML {*
+fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs =
+let
+ val bn_funs' = map (fn (bn, ty, mx) =>
+ (raw_bind bn, replace_typ dts_env ty, mx)) bn_funs
+
+ val bn_eqs' = map (fn (attr, trm) =>
+ (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs
+in
+ (bn_funs', bn_eqs')
+end
+*}
+
+ML {*
+fun rawify_bclauses dts_env cnstrs_env bn_fun_env bclauses =
+let
+ fun rawify_bnds bnds =
+ map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds
+
+ fun rawify_bclause (BEmy n) = BEmy n
+ | rawify_bclause (BLst (bnds, bdys)) = BLst (rawify_bnds bnds, bdys)
+ | rawify_bclause (BSet (bnds, bdys)) = BSet (rawify_bnds bnds, bdys)
+ | rawify_bclause (BRes (bnds, bdys)) = BRes (rawify_bnds bnds, bdys)
+in
+ map (map (map rawify_bclause)) bclauses
+end
+*}
+
+text {* What does the prep_bn code do? Cezary's Function? *}
+
+ML {*
+fun strip_bn_fun t =
+ case t of
+ Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
+ | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
+ | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y =>
+ (i, NONE) :: strip_bn_fun y
+ | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y =>
+ (i, NONE) :: strip_bn_fun y
+ | Const (@{const_name bot}, _) => []
+ | Const (@{const_name Nil}, _) => []
+ | (f as Free _) $ Bound i => [(i, SOME f)]
+ | _ => error ("Unsupported binding function: " ^ (PolyML.makestring t))
+*}
+
+ML {*
+fun find [] _ = error ("cannot find element")
+ | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y
+*}
+
+ML {*
+fun prep_bn dt_names dts eqs =
+let
+ fun aux eq =
+ let
+ val (lhs, rhs) = eq
+ |> strip_qnt_body "all"
+ |> HOLogic.dest_Trueprop
+ |> HOLogic.dest_eq
+ val (bn_fun, [cnstr]) = strip_comb lhs
+ val (_, ty) = dest_Free bn_fun
+ val (ty_name, _) = dest_Type (domain_type ty)
+ val dt_index = find_index (fn x => x = ty_name) dt_names
+ val (cnstr_head, cnstr_args) = strip_comb cnstr
+ val rhs_elements = strip_bn_fun rhs
+ val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements
+ in
+ (dt_index, (bn_fun, (cnstr_head, included)))
+ end
+ fun order dts i ts =
+ let
+ val dt = nth dts i
+ val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt)
+ val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts
+ in
+ map (find ts') cts
+ end
+
+ val unordered = AList.group (op=) (map aux eqs)
+ val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered
+ val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered'
+in
+ ordered
+end
+*}
+
+
+ML {*
+fun raw_nominal_decls dts bn_funs bn_eqs binds lthy =
+let
+ val thy = ProofContext.theory_of lthy
+ val thy_name = Context.theory_name thy
+
+ val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts
+ val dt_full_names = map (Long_Name.qualify thy_name) dt_names
+ val dt_full_names' = add_raws dt_full_names
+ val dts_env = dt_full_names ~~ dt_full_names'
+
+ val cnstrs = get_cnstr_strs dts
+ val cnstrs_ty = get_typed_cnstrs dts
+ val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs
+ val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name
+ (Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty
+ val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names'
+
+ val bn_fun_strs = get_bn_fun_strs bn_funs
+ val bn_fun_strs' = add_raws bn_fun_strs
+ val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
+ val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name))
+ (bn_fun_strs ~~ bn_fun_strs')
+
+ val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env
+
+ val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs
+
+ val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds
+
+ val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs)
+in
+ lthy
+ |> add_datatype_wrapper raw_dt_names raw_dts
+ ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs
+ ||>> pair raw_bclauses
+ ||>> pair raw_bns
+end
+*}
+
+ML {*
+fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
+let
+ val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) =
+ raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
+
+ val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
+ val {descr, sorts, ...} = dtinfo;
+
+ val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
+ Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1;
+in
+ ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy2)
+end
+*}
+
+section {* Preparing and parsing of the specification *}
+
+ML {*
+(* parsing the datatypes and declaring *)
+(* constructors in the local theory *)
+fun prepare_dts dt_strs lthy =
+let
+ val thy = ProofContext.theory_of lthy
+
+ fun mk_type full_tname tvrs =
+ Type (full_tname, map (fn a => TVar ((a, 0), [])) tvrs)
+
+ fun prep_cnstr full_tname tvs (cname, anno_tys, mx, _) =
+ let
+ val tys = map (Syntax.read_typ lthy o snd) anno_tys
+ val ty = mk_type full_tname tvs
+ in
+ ((cname, tys ---> ty, mx), (cname, tys, mx))
+ end
+
+ fun prep_dt (tvs, tname, mx, cnstrs) =
+ let
+ val full_tname = Sign.full_name thy tname
+ val (cnstrs', cnstrs'') =
+ split_list (map (prep_cnstr full_tname tvs) cnstrs)
+ in
+ (cnstrs', (tvs, tname, mx, cnstrs''))
+ end
+
+ val (cnstrs, dts) = split_list (map prep_dt dt_strs)
+in
+ lthy
+ |> Local_Theory.theory (Sign.add_consts_i (flat cnstrs))
+ |> pair dts
+end
+*}
+
+ML {*
+(* parsing the binding function specification and *)
+(* declaring the functions in the local theory *)
+fun prepare_bn_funs bn_fun_strs bn_eq_strs lthy =
+let
+ val ((bn_funs, bn_eqs), _) =
+ Specification.read_spec bn_fun_strs bn_eq_strs lthy
+
+ fun prep_bn_fun ((bn, T), mx) = (bn, T, mx)
+
+ val bn_funs' = map prep_bn_fun bn_funs
+in
+ lthy
+ |> Local_Theory.theory (Sign.add_consts_i bn_funs')
+ |> pair (bn_funs', bn_eqs)
+end
+*}
+
+text {* associates every SOME with the index in the list; drops NONEs *}
+ML {*
+fun indexify xs =
+let
+ fun mapp _ [] = []
+ | mapp i (NONE :: xs) = mapp (i + 1) xs
+ | mapp i (SOME x :: xs) = (x, i) :: mapp (i + 1) xs
+in
+ mapp 0 xs
+end
+
+fun index_lookup xs x =
+ case AList.lookup (op=) xs x of
+ SOME x => x
+ | NONE => error ("Cannot find " ^ x ^ " as argument annotation.");
+*}
+
+ML {*
+fun prepare_bclauses dt_strs lthy =
+let
+ val annos_bclauses =
+ get_cnstrs dt_strs
+ |> map (map (fn (_, antys, _, bns) => (map fst antys, bns)))
+
+ fun prep_binder env bn_str =
+ case (Syntax.read_term lthy bn_str) of
+ Free (x, _) => (NONE, index_lookup env x)
+ | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x)
+ | _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.")
+
+ fun prep_body env bn_str = index_lookup env bn_str
+
+ fun prep_mode "bind" = BLst
+ | prep_mode "bind_set" = BSet
+ | prep_mode "bind_res" = BRes
+
+ fun prep_bclause env (mode, binders, bodies) =
+ let
+ val binders' = map (prep_binder env) binders
+ val bodies' = map (prep_body env) bodies
+ in
+ prep_mode mode (binders', bodies')
+ end
+
+ fun prep_bclauses (annos, bclause_strs) =
+ let
+ val env = indexify annos (* for every label, associate the index *)
+ in
+ map (prep_bclause env) bclause_strs
+ end
+in
+ map (map prep_bclauses) annos_bclauses
+end
+*}
+
+text {*
+ adds an empty binding clause for every argument
+ that is not already part of a binding clause
+*}
+
+ML {*
+fun included i bcs =
+let
+ fun incl (BEmy j) = i = j
+ | incl (BLst (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds)
+ | incl (BSet (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds)
+ | incl (BRes (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds)
+in
+ exists incl bcs
+end
+*}
+
+ML {*
+fun complete dt_strs bclauses =
+let
+ val args =
+ get_cnstrs dt_strs
+ |> map (map (fn (_, antys, _, _) => length antys))
+
+ fun complt n bcs =
+ let
+ fun add bcs i = (if included i bcs then [] else [BEmy i])
+ in
+ bcs @ (flat (map_range (add bcs) n))
+ end
+in
+ map2 (map2 complt) args bclauses
+end
+*}
+
+ML {*
+fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy =
+let
+ fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx)
+ val lthy0 =
+ Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) lthy
+ val (dts, lthy1) = prepare_dts dt_strs lthy0
+ val ((bn_funs, bn_eqs), lthy2) = prepare_bn_funs bn_fun_strs bn_eq_strs lthy1
+ val bclauses = prepare_bclauses dt_strs lthy2
+ val bclauses' = complete dt_strs bclauses
+in
+ nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd
+end
+
+
+(* Command Keyword *)
+
+val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl
+ (main_parser >> nominal_datatype2_cmd)
+*}
+
+
+
+atom_decl name
+
+nominal_datatype exp =
+ EVar name
+| EUnit
+| EPair q1::exp q2::exp bind_set q1 q2 in q1 q2
+| ELetRec l::lrbs e::exp bind "b_lrbs l" in e l
+
+and fnclause =
+ K x::name p::pat f::exp bind_res "b_pat p" in f
+
+and fnclauses =
+ S fnclause
+| ORs fnclause fnclauses
+
+and lrb =
+ Clause fnclauses
+
+and lrbs =
+ Single lrb
+| More lrb lrbs
+
+and pat =
+ PVar name
+| PUnit
+| PPair pat pat
+
+binder
+ b_lrbs :: "lrbs \<Rightarrow> atom set" and
+ b_pat :: "pat \<Rightarrow> atom set" and
+ b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
+ b_fnclause :: "fnclause \<Rightarrow> atom set" and
+ b_lrb :: "lrb \<Rightarrow> atom set"
+
+where
+ "b_lrbs (Single l) = b_lrb l"
+| "b_lrbs (More l ls) = b_lrb l \<union> b_lrbs ls"
+| "b_pat (PVar x) = {atom x}"
+| "b_pat (PUnit) = {}"
+| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
+| "b_fnclauses (S fc) = (b_fnclause fc)"
+| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
+| "b_lrb (Clause fcs) = (b_fnclauses fcs)"
+| "b_fnclause (K x pat exp) = {atom x}"
+
+
+typ exp_raw
+thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars]
+thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars]
+thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars]
+
+
+
+
+end
+
+
+
--- a/Nominal/Nominal2_FSet.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal/Nominal2_FSet.thy Mon Apr 26 10:01:13 2010 +0200
@@ -71,55 +71,6 @@
apply (simp add: atom_fmap_cong)
done
-lemma supp_atom_insert:
- "finite (xs :: atom set) \<Longrightarrow> supp (insert x xs) = supp x \<union> supp xs"
- apply (simp add: supp_finite_atom_set)
- apply (simp add: supp_atom)
- done
-
-lemma atom_image_cong:
- shows "(atom ` X = atom ` Y) = (X = Y)"
- apply(rule inj_image_eq_iff)
- apply(simp add: inj_on_def)
- done
-
-lemma atom_eqvt_raw:
- fixes p::"perm"
- shows "(p \<bullet> atom) = atom"
- apply(perm_simp)
- apply(simp)
- done
-
-lemma supp_finite_at_set:
- fixes S::"('a :: at) set"
- assumes a: "finite S"
- shows "supp S = atom ` S"
- apply(rule finite_supp_unique)
- apply(simp add: supports_def)
- apply (rule finite_induct[OF a])
- apply (simp add: eqvts)
- apply (simp)
- apply clarify
- apply (subst atom_image_cong[symmetric])
- apply (subst atom_eqvt_raw[symmetric])
- apply (subst eqvts[symmetric])
- apply (rule swap_set_not_in)
- apply simp_all
- apply(rule finite_imageI)
- apply(rule a)
- apply (subst atom_image_cong[symmetric])
- apply (subst atom_eqvt_raw[symmetric])
- apply (subst eqvts[symmetric])
- apply (rule swap_set_in)
- apply simp_all
- done
-
-lemma supp_at_insert:
- "finite (xs :: ('a :: at) set) \<Longrightarrow> supp (insert x xs) = supp x \<union> supp xs"
- apply (simp add: supp_finite_at_set)
- apply (simp add: supp_at_base)
- done
-
lemma supp_atom_finsert:
"supp (finsert (x :: atom) S) = supp x \<union> supp S"
apply (subst supp_fset_to_set[symmetric])
@@ -129,7 +80,8 @@
done
lemma supp_at_finsert:
- "supp (finsert (x :: 'a :: at) S) = supp x \<union> supp S"
+ fixes S::"('a::at) fset"
+ shows "supp (finsert x S) = supp x \<union> supp S"
apply (subst supp_fset_to_set[symmetric])
apply (simp add: supp_finite_atom_set)
apply (simp add: supp_at_insert[OF fin_fset_to_set])
--- a/Nominal/Parser.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal/Parser.thy Mon Apr 26 10:01:13 2010 +0200
@@ -625,9 +625,14 @@
map_index (prep_typ binds) annos
end
+ val result = map (map (map (map (fn (a, b, c) =>
+ (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type)))))
+ (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs)))
+
+ val _ = warning (@{make_string} result)
+
in
- map (map (map (map (fn (a, b, c) => (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type)))))
- (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs)))
+ result
end
*}
--- a/PAPER-TODO Wed Apr 21 12:25:52 2010 +0200
+++ b/PAPER-TODO Mon Apr 26 10:01:13 2010 +0200
@@ -12,9 +12,6 @@
I didn't quite get top of second column, p. 6
-"the problem Pottier and Cheney pointed out": I had forgotten it in the
-meantime
-
the equation in the first actuall bullet on p. 8 lacks it =?
missing v. spaces, top of 2nd col p. 8
\ No newline at end of file
--- a/Paper/Paper.thy Wed Apr 21 12:25:52 2010 +0200
+++ b/Paper/Paper.thy Mon Apr 26 10:01:13 2010 +0200
@@ -338,7 +338,7 @@
(Note that this means also the term-constructors for variables, applications
and lambda are lifted to the quotient level.) This construction, of course,
only works if alpha-equivalence is indeed an equivalence relation, and the
- lifted definitions and theorems are respectful w.r.t.~alpha-equivalence.
+ ``raw'' definitions and theorems are respectful w.r.t.~alpha-equivalence.
For example, we will not be able to lift a bound-variable function. Although
this function can be defined for raw terms, it does not respect
alpha-equivalence and therefore cannot be lifted. To sum up, every lifting
@@ -352,7 +352,7 @@
known as Core-Haskell (see Figure~\ref{corehas}). This term language
involves patterns that have lists of type-, coercion- and term-variables,
all of which are bound in @{text "\<CASE>"}-expressions. One
- difficulty is that we do not know in advance how many variables need to
+ feature is that we do not know in advance how many variables need to
be bound. Another is that each bound variable comes with a kind or type
annotation. Representing such binders with single binders and reasoning
about them in a theorem prover would be a major pain. \medskip
@@ -932,9 +932,9 @@
\begin{center}
\begin{tabular}{l}
- \isacommand{bind}\; {\it binder}\; \isacommand{in}\; {\it label}\\
- \isacommand{bind\_set}\; {\it binder}\; \isacommand{in}\; {\it label}\\
- \isacommand{bind\_res}\; {\it binder}\; \isacommand{in}\; {\it label}\\
+ \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
+ \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
+ \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
\end{tabular}
\end{center}
@@ -943,15 +943,15 @@
the second is for sets of binders (the order does not matter, but the
cardinality does) and the last is for sets of binders (with vacuous binders
preserving alpha-equivalence). The ``\isacommand{in}-part'' of a binding
- clause will be called the \emph{body}; the ``\isacommand{bind}-part'' will
- be called the \emph{binder}.
+ clause will be called \emph{body}; the ``\isacommand{bind}-part'' will
+ be called \emph{binder}.
In addition we distinguish between \emph{shallow} and \emph{deep}
- binders. Shallow binders are of the form \isacommand{bind}\; {\it label}\;
- \isacommand{in}\; {\it label'} (similar for the other two modes). The
- restriction we impose on shallow binders is that the {\it label} must either
- refer to a type that is an atom type or to a type that is a finite set or
- list of an atom type. Two examples for the use of shallow binders are the
+ binders. Shallow binders are of the form \isacommand{bind}\; {\it labels}\;
+ \isacommand{in}\; {\it labels'} (similar for the other two modes). The
+ restriction we impose on shallow binders is that the {\it labels} must either
+ refer to atom types or to finite sets or
+ lists of atom types. Two examples for the use of shallow binders are the
specification of lambda-terms, where a single name is bound, and
type-schemes, where a finite set of names is bound:
@@ -1111,8 +1111,9 @@
Having dealt with all syntax matters, the problem now is how we can turn
specifications into actual type definitions in Isabelle/HOL and then
- establish a reasoning infrastructure for them. Because of the problem
- Pottier and Cheney pointed out, we cannot in general re-arrange arguments of
+ establish a reasoning infrastructure for them. As
+ Pottier and Cheney pointed out \cite{Pottier06,Cheney5}, we cannot in general
+ re-arrange arguments of
term-constructors so that binders and their bodies are next to each other, and
then use the type constructors @{text "abs_set"}, @{text "abs_res"} and
@{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first