--- a/IsaMakefile Mon Aug 30 15:59:50 2010 +0900
+++ b/IsaMakefile Sat Sep 04 14:26:09 2010 +0800
@@ -95,7 +95,18 @@
cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
cp Slides/generated3/root.beamer.pdf Slides/slides3.pdf
-slides: slides1
+session4: Slides/ROOT4.ML \
+ Slides/document/root* \
+ Slides/Slides4.thy
+ @$(USEDIR) -D generated4 -f ROOT4.ML HOL-Nominal Slides
+
+slides4: session4
+ rm -f Slides/generated4/*.aux # otherwise latex will fall over
+ cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+ cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+ cp Slides/generated4/root.beamer.pdf Slides/slides4.pdf
+
+slides: slides4
--- a/Nominal-General/Atoms.thy Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal-General/Atoms.thy Sat Sep 04 14:26:09 2010 +0800
@@ -4,9 +4,41 @@
Instantiations of concrete atoms
*)
theory Atoms
-imports Nominal2_Atoms
+imports Nominal2_Base
begin
+
+
+section {* @{const nat_of} is an example of a function
+ without finite support *}
+
+
+lemma not_fresh_nat_of:
+ shows "\<not> a \<sharp> nat_of"
+unfolding fresh_def supp_def
+proof (clarsimp)
+ assume "finite {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"
+ hence "finite ({a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of})"
+ by simp
+ then obtain b where
+ b1: "b \<noteq> a" and
+ b2: "sort_of b = sort_of a" and
+ b3: "(a \<rightleftharpoons> b) \<bullet> nat_of = nat_of"
+ by (rule obtain_atom) auto
+ have "nat_of a = (a \<rightleftharpoons> b) \<bullet> (nat_of a)" by (simp add: permute_nat_def)
+ also have "\<dots> = ((a \<rightleftharpoons> b) \<bullet> nat_of) ((a \<rightleftharpoons> b) \<bullet> a)" by (simp add: permute_fun_app_eq)
+ 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_components_eq_iff)
+ with b1 show "False" by simp
+qed
+
+lemma supp_nat_of:
+ shows "supp nat_of = UNIV"
+ using not_fresh_nat_of [unfolded fresh_def] by auto
+
+
section {* Manual instantiation of class @{text at}. *}
typedef (open) name = "{a. sort_of a = Sort ''name'' []}"
--- a/Nominal-General/Nominal2_Atoms.thy Mon Aug 30 15:59:50 2010 +0900
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,188 +0,0 @@
-(* Title: Nominal2_Atoms
- Authors: Brian Huffman, Christian Urban
-
- Definitions for concrete atom types.
-*)
-theory Nominal2_Atoms
-imports Nominal2_Base
- Nominal2_Eqvt
-uses ("nominal_atoms.ML")
-begin
-
-section {* Infrastructure for concrete atom types *}
-
-
-section {* A swapping operation for concrete atoms *}
-
-definition
- flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')")
-where
- "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)"
-
-lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0"
- unfolding flip_def by (rule swap_self)
-
-lemma flip_commute: "(a \<leftrightarrow> b) = (b \<leftrightarrow> a)"
- unfolding flip_def by (rule swap_commute)
-
-lemma minus_flip [simp]: "- (a \<leftrightarrow> b) = (a \<leftrightarrow> b)"
- unfolding flip_def by (rule minus_swap)
-
-lemma add_flip_cancel: "(a \<leftrightarrow> b) + (a \<leftrightarrow> b) = 0"
- unfolding flip_def by (rule swap_cancel)
-
-lemma permute_flip_cancel [simp]: "(a \<leftrightarrow> b) \<bullet> (a \<leftrightarrow> b) \<bullet> x = x"
- unfolding permute_plus [symmetric] add_flip_cancel by simp
-
-lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x"
- by (simp add: flip_commute)
-
-lemma flip_eqvt[eqvt]:
- fixes a b c::"'a::at_base"
- shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)"
- unfolding flip_def
- by (simp add: swap_eqvt atom_eqvt)
-
-lemma flip_at_base_simps [simp]:
- shows "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> a = b"
- and "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> b = a"
- and "\<lbrakk>a \<noteq> c; b \<noteq> c\<rbrakk> \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> c = c"
- and "sort_of (atom a) \<noteq> sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> x = x"
- unfolding flip_def
- unfolding atom_eq_iff [symmetric]
- unfolding atom_eqvt [symmetric]
- by simp_all
-
-text {* the following two lemmas do not hold for at_base,
- only for single sort atoms from at *}
-
-lemma permute_flip_at:
- fixes a b c::"'a::at"
- shows "(a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)"
- unfolding flip_def
- apply (rule atom_eq_iff [THEN iffD1])
- apply (subst atom_eqvt [symmetric])
- apply (simp add: swap_atom)
- done
-
-lemma flip_at_simps [simp]:
- fixes a b::"'a::at"
- shows "(a \<leftrightarrow> b) \<bullet> a = b"
- and "(a \<leftrightarrow> b) \<bullet> b = a"
- unfolding permute_flip_at by simp_all
-
-lemma flip_fresh_fresh:
- fixes a b::"'a::at_base"
- assumes "atom a \<sharp> x" "atom b \<sharp> x"
- shows "(a \<leftrightarrow> b) \<bullet> x = x"
-using assms
-by (simp add: flip_def swap_fresh_fresh)
-
-subsection {* Syntax for coercing at-elements to the atom-type *}
-
-syntax
- "_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3)
-
-translations
- "_atom_constrain a t" => "CONST atom (_constrain a t)"
-
-
-subsection {* A lemma for proving instances of class @{text at}. *}
-
-setup {* Sign.add_const_constraint (@{const_name "permute"}, NONE) *}
-setup {* Sign.add_const_constraint (@{const_name "atom"}, NONE) *}
-
-text {*
- New atom types are defined as subtypes of @{typ atom}.
-*}
-
-lemma exists_eq_simple_sort:
- shows "\<exists>a. a \<in> {a. sort_of a = s}"
- by (rule_tac x="Atom s 0" in exI, simp)
-
-lemma exists_eq_sort:
- shows "\<exists>a. a \<in> {a. sort_of a \<in> range sort_fun}"
- by (rule_tac x="Atom (sort_fun x) y" in exI, simp)
-
-lemma at_base_class:
- fixes sort_fun :: "'b \<Rightarrow>atom_sort"
- fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
- assumes type: "type_definition Rep Abs {a. sort_of a \<in> range sort_fun}"
- assumes atom_def: "\<And>a. atom a = Rep a"
- assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
- shows "OFCLASS('a, at_base_class)"
-proof
- interpret type_definition Rep Abs "{a. sort_of a \<in> range sort_fun}" by (rule type)
- have sort_of_Rep: "\<And>a. sort_of (Rep a) \<in> range sort_fun" using Rep by simp
- fix a b :: 'a and p p1 p2 :: perm
- show "0 \<bullet> a = a"
- unfolding permute_def by (simp add: Rep_inverse)
- show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
- unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
- show "atom a = atom b \<longleftrightarrow> a = b"
- unfolding atom_def by (simp add: Rep_inject)
- show "p \<bullet> atom a = atom (p \<bullet> a)"
- unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
-qed
-
-(*
-lemma at_class:
- fixes s :: atom_sort
- fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
- assumes type: "type_definition Rep Abs {a. sort_of a \<in> range (\<lambda>x::unit. s)}"
- assumes atom_def: "\<And>a. atom a = Rep a"
- assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
- shows "OFCLASS('a, at_class)"
-proof
- interpret type_definition Rep Abs "{a. sort_of a \<in> range (\<lambda>x::unit. s)}" by (rule type)
- have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)
- fix a b :: 'a and p p1 p2 :: perm
- show "0 \<bullet> a = a"
- unfolding permute_def by (simp add: Rep_inverse)
- show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
- unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
- show "sort_of (atom a) = sort_of (atom b)"
- unfolding atom_def by (simp add: sort_of_Rep)
- show "atom a = atom b \<longleftrightarrow> a = b"
- unfolding atom_def by (simp add: Rep_inject)
- show "p \<bullet> atom a = atom (p \<bullet> a)"
- unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
-qed
-*)
-
-lemma at_class:
- fixes s :: atom_sort
- fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
- assumes type: "type_definition Rep Abs {a. sort_of a = s}"
- assumes atom_def: "\<And>a. atom a = Rep a"
- assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
- shows "OFCLASS('a, at_class)"
-proof
- interpret type_definition Rep Abs "{a. sort_of a = s}" by (rule type)
- have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)
- fix a b :: 'a and p p1 p2 :: perm
- show "0 \<bullet> a = a"
- unfolding permute_def by (simp add: Rep_inverse)
- show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
- unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
- show "sort_of (atom a) = sort_of (atom b)"
- unfolding atom_def by (simp add: sort_of_Rep)
- show "atom a = atom b \<longleftrightarrow> a = b"
- unfolding atom_def by (simp add: Rep_inject)
- show "p \<bullet> atom a = atom (p \<bullet> a)"
- unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
-qed
-
-setup {* Sign.add_const_constraint
- (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *}
-setup {* Sign.add_const_constraint
- (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *}
-
-section {* Automation for creating concrete atom types *}
-
-text {* at the moment only single-sort concrete atoms are supported *}
-
-use "nominal_atoms.ML"
-
-
-end
--- a/Nominal-General/Nominal2_Base.thy Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal-General/Nominal2_Base.thy Sat Sep 04 14:26:09 2010 +0800
@@ -7,6 +7,7 @@
theory Nominal2_Base
imports Main Infinite_Set
uses ("nominal_library.ML")
+ ("nominal_atoms.ML")
begin
section {* Atoms and Sorts *}
@@ -430,6 +431,24 @@
shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"
by (simp add: permute_bool_def)
+lemma conj_eqvt:
+ shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
+ by (simp add: permute_bool_def)
+
+lemma imp_eqvt:
+ shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
+ by (simp add: permute_bool_def)
+
+lemma ex_eqvt:
+ shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
+ unfolding permute_fun_def permute_bool_def
+ by (auto, rule_tac x="p \<bullet> x" in exI, simp)
+
+lemma all_eqvt:
+ shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
+ unfolding permute_fun_def permute_bool_def
+ by (auto, drule_tac x="p \<bullet> x" in spec, simp)
+
lemma permute_boolE:
fixes P::"bool"
shows "p \<bullet> P \<Longrightarrow> P"
@@ -474,6 +493,21 @@
unfolding permute_set_eq
using a by (auto simp add: swap_atom)
+lemma mem_permute_iff:
+ shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
+ unfolding mem_def permute_fun_def permute_bool_def
+ by simp
+
+lemma mem_eqvt:
+ shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
+ unfolding mem_def
+ by (simp add: permute_fun_app_eq)
+
+lemma insert_eqvt:
+ shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
+ unfolding permute_set_eq_image image_insert ..
+
+
subsection {* Permutations for units *}
instantiation unit :: pt
@@ -851,6 +885,7 @@
section {* Support for finite sets of atoms *}
+
lemma supp_finite_atom_set:
fixes S::"atom set"
assumes "finite S"
@@ -862,12 +897,6 @@
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. *}
lemma perm_swap_eq:
@@ -987,6 +1016,16 @@
shows "a \<sharp> (x, y) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> y"
by (simp add: fresh_def supp_Pair)
+lemma supp_Unit:
+ shows "supp () = {}"
+ by (simp add: supp_def)
+
+lemma fresh_Unit:
+ shows "a \<sharp> ()"
+ by (simp add: fresh_def supp_Unit)
+
+
+
instance prod :: (fs, fs) fs
apply default
apply (induct_tac x)
@@ -1065,7 +1104,8 @@
apply (simp_all add: supp_Nil supp_Cons finite_supp)
done
-section {* Support and freshness for applications *}
+
+section {* Support and Freshness for Applications *}
lemma fresh_conv_MOST:
shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)"
@@ -1093,7 +1133,7 @@
unfolding fresh_def
by auto
-text {* support of equivariant functions *}
+text {* Support of Equivariant Functions *}
lemma supp_fun_eqvt:
assumes a: "\<And>p. p \<bullet> f = f"
@@ -1112,7 +1152,346 @@
qed
-section {* Concrete atoms types *}
+section {* Support of Finite Sets of Finitely Supported Elements *}
+
+lemma Union_fresh:
+ shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"
+ unfolding Union_image_eq[symmetric]
+ apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app)
+ apply(simp add: permute_fun_def UNION_def Collect_def Bex_def ex_eqvt mem_def conj_eqvt)
+ apply(subst permute_fun_app_eq)
+ back
+ apply(simp add: supp_eqvt)
+ apply(assumption)
+ done
+
+lemma Union_supports_set:
+ shows "(\<Union>x \<in> S. supp x) supports S"
+proof -
+ { fix a b
+ have "\<forall>x \<in> S. (a \<rightleftharpoons> b) \<bullet> x = x \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> S = S"
+ unfolding permute_set_eq by force
+ }
+ then show "(\<Union>x \<in> S. supp x) supports S"
+ unfolding supports_def
+ by (simp add: fresh_def[symmetric] swap_fresh_fresh)
+qed
+
+lemma Union_of_fin_supp_sets:
+ fixes S::"('a::fs set)"
+ assumes fin: "finite S"
+ shows "finite (\<Union>x\<in>S. supp x)"
+ using fin by (induct) (auto simp add: finite_supp)
+
+lemma Union_included_in_supp:
+ fixes S::"('a::fs set)"
+ assumes fin: "finite S"
+ shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
+proof -
+ have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
+ by (rule supp_finite_atom_set[symmetric])
+ (rule Union_of_fin_supp_sets[OF fin])
+ also have "\<dots> \<subseteq> supp S"
+ by (rule supp_subset_fresh)
+ (simp add: Union_fresh)
+ finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .
+qed
+
+lemma supp_of_fin_sets:
+ fixes S::"('a::fs set)"
+ assumes fin: "finite S"
+ shows "(supp S) = (\<Union>x\<in>S. supp x)"
+apply(rule subset_antisym)
+apply(rule supp_is_subset)
+apply(rule Union_supports_set)
+apply(rule Union_of_fin_supp_sets[OF fin])
+apply(rule Union_included_in_supp[OF fin])
+done
+
+lemma supp_of_fin_union:
+ fixes S T::"('a::fs) set"
+ assumes fin1: "finite S"
+ and fin2: "finite T"
+ shows "supp (S \<union> T) = supp S \<union> supp T"
+ using fin1 fin2
+ by (simp add: supp_of_fin_sets)
+
+lemma supp_of_fin_insert:
+ fixes S::"('a::fs) set"
+ assumes fin: "finite S"
+ shows "supp (insert x S) = supp x \<union> supp S"
+ using fin
+ by (simp add: supp_of_fin_sets)
+
+
+section {* Fresh-Star *}
+
+
+text {* The fresh-star generalisation of fresh is used in strong
+ induction principles. *}
+
+definition
+ fresh_star :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp>* _" [80,80] 80)
+where
+ "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x"
+
+lemma fresh_star_prod:
+ fixes as::"atom set"
+ shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)"
+ by (auto simp add: fresh_star_def fresh_Pair)
+
+lemma fresh_star_union:
+ shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"
+ by (auto simp add: fresh_star_def)
+
+lemma fresh_star_insert:
+ shows "(insert a as) \<sharp>* x = (a \<sharp> x \<and> as \<sharp>* x)"
+ by (auto simp add: fresh_star_def)
+
+lemma fresh_star_Un_elim:
+ "((as \<union> bs) \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (as \<sharp>* x \<Longrightarrow> bs \<sharp>* x \<Longrightarrow> PROP C)"
+ unfolding fresh_star_def
+ apply(rule)
+ apply(erule meta_mp)
+ apply(auto)
+ done
+
+lemma fresh_star_insert_elim:
+ "(insert a as \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (a \<sharp> x \<Longrightarrow> as \<sharp>* x \<Longrightarrow> PROP C)"
+ unfolding fresh_star_def
+ by rule (simp_all add: fresh_star_def)
+
+lemma fresh_star_empty_elim:
+ "({} \<sharp>* x \<Longrightarrow> PROP C) \<equiv> PROP C"
+ by (simp add: fresh_star_def)
+
+lemma fresh_star_unit_elim:
+ shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C"
+ by (simp add: fresh_star_def fresh_Unit)
+
+lemma fresh_star_prod_elim:
+ shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)"
+ by (rule, simp_all add: fresh_star_prod)
+
+lemma fresh_star_zero:
+ shows "as \<sharp>* (0::perm)"
+ unfolding fresh_star_def
+ by (simp add: fresh_zero_perm)
+
+lemma fresh_star_plus:
+ fixes p q::perm
+ shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
+ unfolding fresh_star_def
+ by (simp add: fresh_plus_perm)
+
+lemma fresh_star_permute_iff:
+ shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
+ unfolding fresh_star_def
+ by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff)
+
+lemma fresh_star_eqvt:
+ shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)"
+unfolding fresh_star_def
+unfolding Ball_def
+apply(simp add: all_eqvt)
+apply(subst permute_fun_def)
+apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)
+done
+
+
+section {* Induction principle for permutations *}
+
+
+lemma perm_struct_induct[consumes 1, case_names zero swap]:
+ assumes S: "supp p \<subseteq> S"
+ 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 "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
+ have as: "supp p \<subseteq> S" by fact
+ { assume "supp p = {}"
+ then have "p = 0" by (simp add: supp_perm expand_perm_eq)
+ then have "P p" using zero by simp
+ }
+ moreover
+ { assume "supp p \<noteq> {}"
+ then obtain a where a0: "a \<in> supp p" by blast
+ 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 \<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 a2 by auto
+ then have "P ?q" using ih by simp
+ moreover
+ have "supp ?q \<subseteq> S" using as a2 by simp
+ ultimately have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp
+ moreover
+ 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_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"
+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"
+ 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_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
+ next
+ case (swap a b)
+ then have "a \<sharp> x" "b \<sharp> x" by simp_all
+ then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh)
+ next
+ case (plus p1 p2)
+ have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+
+ then show "(p1 + p2) \<bullet> x = x" by simp
+ qed
+qed
+
+
+section {* Avoiding of atom sets *}
+
+text {*
+ For every set of atoms, there is another set of atoms
+ avoiding a finitely supported c and there is a permutation
+ which 'translates' between both sets.
+*}
+
+lemma at_set_avoiding_aux:
+ fixes Xs::"atom set"
+ and As::"atom set"
+ assumes b: "Xs \<subseteq> As"
+ and c: "finite As"
+ shows "\<exists>p. (p \<bullet> Xs) \<inter> As = {} \<and> (supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"
+proof -
+ from b c have "finite Xs" by (rule finite_subset)
+ then show ?thesis using b
+ proof (induct rule: finite_subset_induct)
+ case empty
+ have "0 \<bullet> {} \<inter> As = {}" by simp
+ moreover
+ have "supp (0::perm) \<subseteq> {} \<union> 0 \<bullet> {}" by (simp add: supp_zero_perm)
+ ultimately show ?case by blast
+ next
+ case (insert x Xs)
+ then obtain p where
+ p1: "(p \<bullet> Xs) \<inter> As = {}" and
+ p2: "supp p \<subseteq> (Xs \<union> (p \<bullet> Xs))" by blast
+ from `x \<in> As` p1 have "x \<notin> p \<bullet> Xs" by fast
+ with `x \<notin> Xs` p2 have "x \<notin> supp p" by fast
+ hence px: "p \<bullet> x = x" unfolding supp_perm by simp
+ have "finite (As \<union> p \<bullet> Xs)"
+ using `finite As` `finite Xs`
+ by (simp add: permute_set_eq_image)
+ then obtain y where "y \<notin> (As \<union> p \<bullet> Xs)" "sort_of y = sort_of x"
+ by (rule obtain_atom)
+ hence y: "y \<notin> As" "y \<notin> p \<bullet> Xs" "sort_of y = sort_of x"
+ by simp_all
+ let ?q = "(x \<rightleftharpoons> y) + p"
+ have q: "?q \<bullet> insert x Xs = insert y (p \<bullet> Xs)"
+ unfolding insert_eqvt
+ using `p \<bullet> x = x` `sort_of y = sort_of x`
+ using `x \<notin> p \<bullet> Xs` `y \<notin> p \<bullet> Xs`
+ by (simp add: swap_atom swap_set_not_in)
+ have "?q \<bullet> insert x Xs \<inter> As = {}"
+ using `y \<notin> As` `p \<bullet> Xs \<inter> As = {}`
+ unfolding q by simp
+ moreover
+ have "supp ?q \<subseteq> insert x Xs \<union> ?q \<bullet> insert x Xs"
+ using p2 unfolding q
+ by (intro subset_trans [OF supp_plus_perm])
+ (auto simp add: supp_swap)
+ ultimately show ?case by blast
+ qed
+qed
+
+lemma at_set_avoiding:
+ assumes a: "finite Xs"
+ and b: "finite (supp c)"
+ obtains p::"perm" where "(p \<bullet> Xs)\<sharp>*c" and "(supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"
+ using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"]
+ unfolding fresh_star_def fresh_def by blast
+
+lemma at_set_avoiding2:
+ assumes "finite xs"
+ and "finite (supp c)" "finite (supp x)"
+ and "xs \<sharp>* x"
+ shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"
+using assms
+apply(erule_tac c="(c, x)" in at_set_avoiding)
+apply(simp add: supp_Pair)
+apply(rule_tac x="p" in exI)
+apply(simp add: fresh_star_prod)
+apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x")
+apply(auto simp add: fresh_star_def fresh_def supp_perm)[1]
+apply(auto simp add: fresh_star_def fresh_def)
+done
+
+lemma at_set_avoiding2_atom:
+ assumes "finite (supp c)" "finite (supp x)"
+ and b: "a \<sharp> x"
+ shows "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p"
+proof -
+ 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> a" in allE) (simp add: permute_set_eq)
+ 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 {* Concrete Atoms Types *}
text {*
Class @{text at_base} allows types containing multiple sorts of atoms.
@@ -1179,44 +1558,363 @@
thus ?thesis ..
qed
-lemma image_eqvt:
- shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
- unfolding permute_set_eq_image
- unfolding permute_fun_def [where f=f]
- by (simp add: image_image)
-
-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_image_supp:
- shows "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_set_at_base:
assumes a: "finite S"
shows "supp S = atom ` S"
-proof -
- have fin: "finite (atom ` S)" using a by simp
- have "supp S = supp (atom ` S)" by (rule atom_image_supp)
- also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set)
- finally show "supp S = atom ` S" by simp
+apply(simp add: supp_of_fin_sets[OF a])
+apply(simp add: supp_at_base)
+apply(auto)
+done
+
+section {* Infrastructure for concrete atom types *}
+
+section {* A swapping operation for concrete atoms *}
+
+definition
+ flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')")
+where
+ "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)"
+
+lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0"
+ unfolding flip_def by (rule swap_self)
+
+lemma flip_commute: "(a \<leftrightarrow> b) = (b \<leftrightarrow> a)"
+ unfolding flip_def by (rule swap_commute)
+
+lemma minus_flip [simp]: "- (a \<leftrightarrow> b) = (a \<leftrightarrow> b)"
+ unfolding flip_def by (rule minus_swap)
+
+lemma add_flip_cancel: "(a \<leftrightarrow> b) + (a \<leftrightarrow> b) = 0"
+ unfolding flip_def by (rule swap_cancel)
+
+lemma permute_flip_cancel [simp]: "(a \<leftrightarrow> b) \<bullet> (a \<leftrightarrow> b) \<bullet> x = x"
+ unfolding permute_plus [symmetric] add_flip_cancel by simp
+
+lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x"
+ by (simp add: flip_commute)
+
+lemma flip_eqvt:
+ fixes a b c::"'a::at_base"
+ shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)"
+ unfolding flip_def
+ by (simp add: swap_eqvt atom_eqvt)
+
+lemma flip_at_base_simps [simp]:
+ shows "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> a = b"
+ and "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> b = a"
+ and "\<lbrakk>a \<noteq> c; b \<noteq> c\<rbrakk> \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> c = c"
+ and "sort_of (atom a) \<noteq> sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> x = x"
+ unfolding flip_def
+ unfolding atom_eq_iff [symmetric]
+ unfolding atom_eqvt [symmetric]
+ by simp_all
+
+text {* the following two lemmas do not hold for at_base,
+ only for single sort atoms from at *}
+
+lemma permute_flip_at:
+ fixes a b c::"'a::at"
+ shows "(a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)"
+ unfolding flip_def
+ apply (rule atom_eq_iff [THEN iffD1])
+ apply (subst atom_eqvt [symmetric])
+ apply (simp add: swap_atom)
+ done
+
+lemma flip_at_simps [simp]:
+ fixes a b::"'a::at"
+ shows "(a \<leftrightarrow> b) \<bullet> a = b"
+ and "(a \<leftrightarrow> b) \<bullet> b = a"
+ unfolding permute_flip_at by simp_all
+
+lemma flip_fresh_fresh:
+ fixes a b::"'a::at_base"
+ assumes "atom a \<sharp> x" "atom b \<sharp> x"
+ shows "(a \<leftrightarrow> b) \<bullet> x = x"
+using assms
+by (simp add: flip_def swap_fresh_fresh)
+
+subsection {* Syntax for coercing at-elements to the atom-type *}
+
+syntax
+ "_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3)
+
+translations
+ "_atom_constrain a t" => "CONST atom (_constrain a t)"
+
+
+subsection {* A lemma for proving instances of class @{text at}. *}
+
+setup {* Sign.add_const_constraint (@{const_name "permute"}, NONE) *}
+setup {* Sign.add_const_constraint (@{const_name "atom"}, NONE) *}
+
+text {*
+ New atom types are defined as subtypes of @{typ atom}.
+*}
+
+lemma exists_eq_simple_sort:
+ shows "\<exists>a. a \<in> {a. sort_of a = s}"
+ by (rule_tac x="Atom s 0" in exI, simp)
+
+lemma exists_eq_sort:
+ shows "\<exists>a. a \<in> {a. sort_of a \<in> range sort_fun}"
+ by (rule_tac x="Atom (sort_fun x) y" in exI, simp)
+
+lemma at_base_class:
+ fixes sort_fun :: "'b \<Rightarrow>atom_sort"
+ fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
+ assumes type: "type_definition Rep Abs {a. sort_of a \<in> range sort_fun}"
+ assumes atom_def: "\<And>a. atom a = Rep a"
+ assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
+ shows "OFCLASS('a, at_base_class)"
+proof
+ interpret type_definition Rep Abs "{a. sort_of a \<in> range sort_fun}" by (rule type)
+ have sort_of_Rep: "\<And>a. sort_of (Rep a) \<in> range sort_fun" using Rep by simp
+ fix a b :: 'a and p p1 p2 :: perm
+ show "0 \<bullet> a = a"
+ unfolding permute_def by (simp add: Rep_inverse)
+ show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
+ unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
+ show "atom a = atom b \<longleftrightarrow> a = b"
+ unfolding atom_def by (simp add: Rep_inject)
+ show "p \<bullet> atom a = atom (p \<bullet> a)"
+ unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
+qed
+
+(*
+lemma at_class:
+ fixes s :: atom_sort
+ fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
+ assumes type: "type_definition Rep Abs {a. sort_of a \<in> range (\<lambda>x::unit. s)}"
+ assumes atom_def: "\<And>a. atom a = Rep a"
+ assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
+ shows "OFCLASS('a, at_class)"
+proof
+ interpret type_definition Rep Abs "{a. sort_of a \<in> range (\<lambda>x::unit. s)}" by (rule type)
+ have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)
+ fix a b :: 'a and p p1 p2 :: perm
+ show "0 \<bullet> a = a"
+ unfolding permute_def by (simp add: Rep_inverse)
+ show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
+ unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
+ show "sort_of (atom a) = sort_of (atom b)"
+ unfolding atom_def by (simp add: sort_of_Rep)
+ show "atom a = atom b \<longleftrightarrow> a = b"
+ unfolding atom_def by (simp add: Rep_inject)
+ show "p \<bullet> atom a = atom (p \<bullet> a)"
+ unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
+qed
+*)
+
+lemma at_class:
+ fixes s :: atom_sort
+ fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
+ assumes type: "type_definition Rep Abs {a. sort_of a = s}"
+ assumes atom_def: "\<And>a. atom a = Rep a"
+ assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
+ shows "OFCLASS('a, at_class)"
+proof
+ interpret type_definition Rep Abs "{a. sort_of a = s}" by (rule type)
+ have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)
+ fix a b :: 'a and p p1 p2 :: perm
+ show "0 \<bullet> a = a"
+ unfolding permute_def by (simp add: Rep_inverse)
+ show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
+ unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
+ show "sort_of (atom a) = sort_of (atom b)"
+ unfolding atom_def by (simp add: sort_of_Rep)
+ show "atom a = atom b \<longleftrightarrow> a = b"
+ unfolding atom_def by (simp add: Rep_inject)
+ show "p \<bullet> atom a = atom (p \<bullet> a)"
+ unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
qed
-lemma supp_at_base_insert:
- fixes a::"'a::at_base"
- assumes a: "finite S"
- shows "supp (insert a S) = supp a \<union> supp S"
- using a by (simp add: supp_finite_set_at_base supp_at_base)
+setup {* Sign.add_const_constraint
+ (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *}
+setup {* Sign.add_const_constraint
+ (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *}
+
+
+
+section {* The freshness lemma according to Andy Pitts *}
+
+lemma freshness_lemma:
+ fixes h :: "'a::at \<Rightarrow> 'b::pt"
+ assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
+ shows "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
+proof -
+ from a obtain b where a1: "atom b \<sharp> h" and a2: "atom b \<sharp> h b"
+ by (auto simp add: fresh_Pair)
+ show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
+ proof (intro exI allI impI)
+ fix a :: 'a
+ assume a3: "atom a \<sharp> h"
+ show "h a = h b"
+ proof (cases "a = b")
+ assume "a = b"
+ thus "h a = h b" by simp
+ next
+ assume "a \<noteq> b"
+ hence "atom a \<sharp> b" by (simp add: fresh_at_base)
+ with a3 have "atom a \<sharp> h b"
+ by (rule fresh_fun_app)
+ with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)"
+ by (rule swap_fresh_fresh)
+ from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h"
+ by (rule swap_fresh_fresh)
+ from d1 have "h b = (atom b \<rightleftharpoons> atom a) \<bullet> (h b)" by simp
+ also have "\<dots> = ((atom b \<rightleftharpoons> atom a) \<bullet> h) ((atom b \<rightleftharpoons> atom a) \<bullet> b)"
+ by (rule permute_fun_app_eq)
+ also have "\<dots> = h a"
+ using d2 by simp
+ finally show "h a = h b" by simp
+ qed
+ qed
+qed
+
+lemma freshness_lemma_unique:
+ fixes h :: "'a::at \<Rightarrow> 'b::pt"
+ assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
+ shows "\<exists>!x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
+proof (rule ex_ex1I)
+ from a show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
+ by (rule freshness_lemma)
+next
+ fix x y
+ assume x: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
+ assume y: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = y"
+ from a x y show "x = y"
+ by (auto simp add: fresh_Pair)
+qed
+
+text {* packaging the freshness lemma into a function *}
+
+definition
+ fresh_fun :: "('a::at \<Rightarrow> 'b::pt) \<Rightarrow> 'b"
+where
+ "fresh_fun h = (THE x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x)"
+
+lemma fresh_fun_apply:
+ fixes h :: "'a::at \<Rightarrow> 'b::pt"
+ assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
+ assumes b: "atom a \<sharp> h"
+ shows "fresh_fun h = h a"
+unfolding fresh_fun_def
+proof (rule the_equality)
+ show "\<forall>a'. atom a' \<sharp> h \<longrightarrow> h a' = h a"
+ proof (intro strip)
+ fix a':: 'a
+ assume c: "atom a' \<sharp> h"
+ from a have "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" by (rule freshness_lemma)
+ with b c show "h a' = h a" by auto
+ qed
+next
+ fix fr :: 'b
+ assume "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = fr"
+ with b show "fr = h a" by auto
+qed
-section {* library functions for the nominal infrastructure *}
+lemma fresh_fun_apply':
+ fixes h :: "'a::at \<Rightarrow> 'b::pt"
+ assumes a: "atom a \<sharp> h" "atom a \<sharp> h a"
+ shows "fresh_fun h = h a"
+ apply (rule fresh_fun_apply)
+ apply (auto simp add: fresh_Pair intro: a)
+ done
+
+lemma fresh_fun_eqvt:
+ fixes h :: "'a::at \<Rightarrow> 'b::pt"
+ assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
+ shows "p \<bullet> (fresh_fun h) = fresh_fun (p \<bullet> h)"
+ using a
+ apply (clarsimp simp add: fresh_Pair)
+ apply (subst fresh_fun_apply', assumption+)
+ apply (drule fresh_permute_iff [where p=p, THEN iffD2])
+ apply (drule fresh_permute_iff [where p=p, THEN iffD2])
+ apply (simp add: atom_eqvt permute_fun_app_eq [where f=h])
+ apply (erule (1) fresh_fun_apply' [symmetric])
+ done
+
+lemma fresh_fun_supports:
+ fixes h :: "'a::at \<Rightarrow> 'b::pt"
+ assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
+ shows "(supp h) supports (fresh_fun h)"
+ apply (simp add: supports_def fresh_def [symmetric])
+ apply (simp add: fresh_fun_eqvt [OF a] swap_fresh_fresh)
+ done
+
+notation fresh_fun (binder "FRESH " 10)
+
+lemma FRESH_f_iff:
+ fixes P :: "'a::at \<Rightarrow> 'b::pure"
+ fixes f :: "'b \<Rightarrow> 'c::pure"
+ assumes P: "finite (supp P)"
+ shows "(FRESH x. f (P x)) = f (FRESH x. P x)"
+proof -
+ obtain a::'a where "atom a \<notin> supp P"
+ using P by (rule obtain_at_base)
+ hence "atom a \<sharp> P"
+ by (simp add: fresh_def)
+ show "(FRESH x. f (P x)) = f (FRESH x. P x)"
+ apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh])
+ apply (cut_tac `atom a \<sharp> P`)
+ apply (simp add: fresh_conv_MOST)
+ apply (elim MOST_rev_mp, rule MOST_I, clarify)
+ apply (simp add: permute_fun_def permute_pure expand_fun_eq)
+ apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh])
+ apply (rule refl)
+ done
+qed
+
+lemma FRESH_binop_iff:
+ fixes P :: "'a::at \<Rightarrow> 'b::pure"
+ fixes Q :: "'a::at \<Rightarrow> 'c::pure"
+ fixes binop :: "'b \<Rightarrow> 'c \<Rightarrow> 'd::pure"
+ assumes P: "finite (supp P)"
+ and Q: "finite (supp Q)"
+ shows "(FRESH x. binop (P x) (Q x)) = binop (FRESH x. P x) (FRESH x. Q x)"
+proof -
+ from assms have "finite (supp P \<union> supp Q)" by simp
+ then obtain a::'a where "atom a \<notin> (supp P \<union> supp Q)"
+ by (rule obtain_at_base)
+ hence "atom a \<sharp> P" and "atom a \<sharp> Q"
+ by (simp_all add: fresh_def)
+ show ?thesis
+ apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh])
+ apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`)
+ apply (simp add: fresh_conv_MOST)
+ apply (elim MOST_rev_mp, rule MOST_I, clarify)
+ apply (simp add: permute_fun_def permute_pure expand_fun_eq)
+ apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh])
+ apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> Q` pure_fresh])
+ apply (rule refl)
+ done
+qed
+
+lemma FRESH_conj_iff:
+ fixes P Q :: "'a::at \<Rightarrow> bool"
+ assumes P: "finite (supp P)" and Q: "finite (supp Q)"
+ shows "(FRESH x. P x \<and> Q x) \<longleftrightarrow> (FRESH x. P x) \<and> (FRESH x. Q x)"
+using P Q by (rule FRESH_binop_iff)
+
+lemma FRESH_disj_iff:
+ fixes P Q :: "'a::at \<Rightarrow> bool"
+ assumes P: "finite (supp P)" and Q: "finite (supp Q)"
+ shows "(FRESH x. P x \<or> Q x) \<longleftrightarrow> (FRESH x. P x) \<or> (FRESH x. Q x)"
+using P Q by (rule FRESH_binop_iff)
+
+
+section {* Library functions for the nominal infrastructure *}
+
use "nominal_library.ML"
+
+section {* Automation for creating concrete atom types *}
+
+text {* at the moment only single-sort concrete atoms are supported *}
+
+use "nominal_atoms.ML"
+
+
+
end
--- a/Nominal-General/Nominal2_Eqvt.thy Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal-General/Nominal2_Eqvt.thy Sat Sep 04 14:26:09 2010 +0800
@@ -20,6 +20,24 @@
use "nominal_thmdecls.ML"
setup "Nominal_ThmDecls.setup"
+
+section {* eqvt lemmas *}
+
+lemmas [eqvt] =
+ conj_eqvt Not_eqvt ex_eqvt all_eqvt imp_eqvt
+ imp_eqvt[folded induct_implies_def]
+ uminus_eqvt
+
+ (* nominal *)
+ supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt
+ swap_eqvt flip_eqvt
+
+ (* datatypes *)
+ Pair_eqvt permute_list.simps
+
+ (* sets *)
+ mem_eqvt insert_eqvt
+
text {* helper lemmas for the perm_simp *}
definition
@@ -79,36 +97,14 @@
shows "p \<bullet> False = False"
unfolding permute_bool_def ..
-lemma imp_eqvt[eqvt]:
- shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
- by (simp add: permute_bool_def)
-
-lemma conj_eqvt[eqvt]:
- shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
- by (simp add: permute_bool_def)
-
lemma disj_eqvt[eqvt]:
shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"
by (simp add: permute_bool_def)
-lemma Not_eqvt[eqvt]:
- shows "p \<bullet> (\<not> A) \<longleftrightarrow> \<not> (p \<bullet> A)"
- by (simp add: permute_bool_def)
-
-lemma all_eqvt[eqvt]:
- shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
- unfolding permute_fun_def permute_bool_def
- by (auto, drule_tac x="p \<bullet> x" in spec, simp)
-
lemma all_eqvt2:
shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
by (perm_simp add: permute_minus_cancel) (rule refl)
-lemma ex_eqvt[eqvt]:
- shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
- unfolding permute_fun_def permute_bool_def
- by (auto, rule_tac x="p \<bullet> x" in exI, simp)
-
lemma ex_eqvt2:
shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
by (perm_simp add: permute_minus_cancel) (rule refl)
@@ -134,16 +130,6 @@
section {* Set Operations *}
-lemma mem_permute_iff:
- shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
- unfolding mem_def permute_fun_def permute_bool_def
- by simp
-
-lemma mem_eqvt[eqvt]:
- shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
- unfolding mem_def
- by (perm_simp) (rule refl)
-
lemma not_mem_eqvt:
shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
by (perm_simp) (rule refl)
@@ -207,9 +193,11 @@
unfolding Compl_eq_Diff_UNIV
by (perm_simp) (rule refl)
-lemma insert_eqvt[eqvt]:
- shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
- unfolding permute_set_eq_image image_insert ..
+lemma image_eqvt:
+ shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
+ unfolding permute_set_eq_image
+ unfolding permute_fun_def [where f=f]
+ by (simp add: image_image)
lemma vimage_eqvt[eqvt]:
shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
@@ -230,6 +218,15 @@
shows "p \<bullet> finite A = finite (p \<bullet> A)"
unfolding finite_permute_iff permute_bool_def ..
+lemma supp_set:
+ fixes xs :: "('a::fs) list"
+ shows "supp (set xs) = supp xs"
+apply(induct xs)
+apply(simp add: supp_set_empty supp_Nil)
+apply(simp add: supp_Cons supp_of_fin_insert)
+done
+
+
section {* List Operations *}
lemma append_eqvt[eqvt]:
@@ -285,30 +282,6 @@
unfolding split_def
by (perm_simp) (rule refl)
-section {* Units *}
-
-lemma supp_unit:
- shows "supp () = {}"
- by (simp add: supp_def)
-
-lemma fresh_unit:
- shows "a \<sharp> ()"
- by (simp add: fresh_def supp_unit)
-
-section {* additional eqvt lemmas *}
-
-lemmas [eqvt] =
- imp_eqvt [folded induct_implies_def]
-
- (* nominal *)
- supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt uminus_eqvt
-
- (* datatypes *)
- Pair_eqvt permute_list.simps
-
- (* sets *)
- image_eqvt
-
section {* Test cases *}
--- a/Nominal-General/Nominal2_Supp.thy Mon Aug 30 15:59:50 2010 +0900
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,547 +0,0 @@
-(* Title: Nominal2_Supp
- Authors: Brian Huffman, Christian Urban
-
- Supplementary Lemmas and Definitions for
- Nominal Isabelle.
-*)
-theory Nominal2_Supp
-imports Nominal2_Base Nominal2_Eqvt Nominal2_Atoms
-begin
-
-
-section {* Fresh-Star *}
-
-
-text {* The fresh-star generalisation of fresh is used in strong
- induction principles. *}
-
-definition
- fresh_star :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp>* _" [80,80] 80)
-where
- "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x"
-
-lemma fresh_star_prod:
- fixes as::"atom set"
- shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)"
- by (auto simp add: fresh_star_def fresh_Pair)
-
-lemma fresh_star_union:
- shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"
- by (auto simp add: fresh_star_def)
-
-lemma fresh_star_insert:
- shows "(insert a as) \<sharp>* x = (a \<sharp> x \<and> as \<sharp>* x)"
- by (auto simp add: fresh_star_def)
-
-lemma fresh_star_Un_elim:
- "((as \<union> bs) \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (as \<sharp>* x \<Longrightarrow> bs \<sharp>* x \<Longrightarrow> PROP C)"
- unfolding fresh_star_def
- apply(rule)
- apply(erule meta_mp)
- apply(auto)
- done
-
-lemma fresh_star_insert_elim:
- "(insert a as \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (a \<sharp> x \<Longrightarrow> as \<sharp>* x \<Longrightarrow> PROP C)"
- unfolding fresh_star_def
- by rule (simp_all add: fresh_star_def)
-
-lemma fresh_star_empty_elim:
- "({} \<sharp>* x \<Longrightarrow> PROP C) \<equiv> PROP C"
- by (simp add: fresh_star_def)
-
-lemma fresh_star_unit_elim:
- shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C"
- by (simp add: fresh_star_def fresh_unit)
-
-lemma fresh_star_prod_elim:
- shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)"
- by (rule, simp_all add: fresh_star_prod)
-
-lemma fresh_star_zero:
- shows "as \<sharp>* (0::perm)"
- unfolding fresh_star_def
- by (simp add: fresh_zero_perm)
-
-lemma fresh_star_plus:
- fixes p q::perm
- shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
- unfolding fresh_star_def
- by (simp add: fresh_plus_perm)
-
-
-lemma fresh_star_permute_iff:
- shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
- unfolding fresh_star_def
- by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff)
-
-lemma fresh_star_eqvt[eqvt]:
- shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)"
-unfolding fresh_star_def
-unfolding Ball_def
-apply(simp add: all_eqvt)
-apply(subst permute_fun_def)
-apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)
-done
-
-section {* Avoiding of atom sets *}
-
-text {*
- For every set of atoms, there is another set of atoms
- avoiding a finitely supported c and there is a permutation
- which 'translates' between both sets.
-*}
-
-lemma at_set_avoiding_aux:
- fixes Xs::"atom set"
- and As::"atom set"
- assumes b: "Xs \<subseteq> As"
- and c: "finite As"
- shows "\<exists>p. (p \<bullet> Xs) \<inter> As = {} \<and> (supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"
-proof -
- from b c have "finite Xs" by (rule finite_subset)
- then show ?thesis using b
- proof (induct rule: finite_subset_induct)
- case empty
- have "0 \<bullet> {} \<inter> As = {}" by simp
- moreover
- have "supp (0::perm) \<subseteq> {} \<union> 0 \<bullet> {}" by (simp add: supp_zero_perm)
- ultimately show ?case by blast
- next
- case (insert x Xs)
- then obtain p where
- p1: "(p \<bullet> Xs) \<inter> As = {}" and
- p2: "supp p \<subseteq> (Xs \<union> (p \<bullet> Xs))" by blast
- from `x \<in> As` p1 have "x \<notin> p \<bullet> Xs" by fast
- with `x \<notin> Xs` p2 have "x \<notin> supp p" by fast
- hence px: "p \<bullet> x = x" unfolding supp_perm by simp
- have "finite (As \<union> p \<bullet> Xs)"
- using `finite As` `finite Xs`
- by (simp add: permute_set_eq_image)
- then obtain y where "y \<notin> (As \<union> p \<bullet> Xs)" "sort_of y = sort_of x"
- by (rule obtain_atom)
- hence y: "y \<notin> As" "y \<notin> p \<bullet> Xs" "sort_of y = sort_of x"
- by simp_all
- let ?q = "(x \<rightleftharpoons> y) + p"
- have q: "?q \<bullet> insert x Xs = insert y (p \<bullet> Xs)"
- unfolding insert_eqvt
- using `p \<bullet> x = x` `sort_of y = sort_of x`
- using `x \<notin> p \<bullet> Xs` `y \<notin> p \<bullet> Xs`
- by (simp add: swap_atom swap_set_not_in)
- have "?q \<bullet> insert x Xs \<inter> As = {}"
- using `y \<notin> As` `p \<bullet> Xs \<inter> As = {}`
- unfolding q by simp
- moreover
- have "supp ?q \<subseteq> insert x Xs \<union> ?q \<bullet> insert x Xs"
- using p2 unfolding q
- by (intro subset_trans [OF supp_plus_perm])
- (auto simp add: supp_swap)
- ultimately show ?case by blast
- qed
-qed
-
-lemma at_set_avoiding:
- assumes a: "finite Xs"
- and b: "finite (supp c)"
- obtains p::"perm" where "(p \<bullet> Xs)\<sharp>*c" and "(supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"
- using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"]
- unfolding fresh_star_def fresh_def by blast
-
-lemma at_set_avoiding2:
- assumes "finite xs"
- and "finite (supp c)" "finite (supp x)"
- and "xs \<sharp>* x"
- shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"
-using assms
-apply(erule_tac c="(c, x)" in at_set_avoiding)
-apply(simp add: supp_Pair)
-apply(rule_tac x="p" in exI)
-apply(simp add: fresh_star_prod)
-apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x")
-apply(auto simp add: fresh_star_def fresh_def supp_perm)[1]
-apply(auto simp add: fresh_star_def fresh_def)
-done
-
-lemma at_set_avoiding2_atom:
- assumes "finite (supp c)" "finite (supp x)"
- and b: "a \<sharp> x"
- shows "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p"
-proof -
- 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> a" in allE) (simp add: permute_set_eq)
- 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 Andy Pitts *}
-
-lemma freshness_lemma:
- fixes h :: "'a::at \<Rightarrow> 'b::pt"
- assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
- shows "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
-proof -
- from a obtain b where a1: "atom b \<sharp> h" and a2: "atom b \<sharp> h b"
- by (auto simp add: fresh_Pair)
- show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
- proof (intro exI allI impI)
- fix a :: 'a
- assume a3: "atom a \<sharp> h"
- show "h a = h b"
- proof (cases "a = b")
- assume "a = b"
- thus "h a = h b" by simp
- next
- assume "a \<noteq> b"
- hence "atom a \<sharp> b" by (simp add: fresh_at_base)
- with a3 have "atom a \<sharp> h b"
- by (rule fresh_fun_app)
- with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)"
- by (rule swap_fresh_fresh)
- from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h"
- by (rule swap_fresh_fresh)
- from d1 have "h b = (atom b \<rightleftharpoons> atom a) \<bullet> (h b)" by simp
- also have "\<dots> = ((atom b \<rightleftharpoons> atom a) \<bullet> h) ((atom b \<rightleftharpoons> atom a) \<bullet> b)"
- by (rule permute_fun_app_eq)
- also have "\<dots> = h a"
- using d2 by simp
- finally show "h a = h b" by simp
- qed
- qed
-qed
-
-lemma freshness_lemma_unique:
- fixes h :: "'a::at \<Rightarrow> 'b::pt"
- assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
- shows "\<exists>!x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
-proof (rule ex_ex1I)
- from a show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
- by (rule freshness_lemma)
-next
- fix x y
- assume x: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
- assume y: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = y"
- from a x y show "x = y"
- by (auto simp add: fresh_Pair)
-qed
-
-text {* packaging the freshness lemma into a function *}
-
-definition
- fresh_fun :: "('a::at \<Rightarrow> 'b::pt) \<Rightarrow> 'b"
-where
- "fresh_fun h = (THE x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x)"
-
-lemma fresh_fun_app:
- fixes h :: "'a::at \<Rightarrow> 'b::pt"
- assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
- assumes b: "atom a \<sharp> h"
- shows "fresh_fun h = h a"
-unfolding fresh_fun_def
-proof (rule the_equality)
- show "\<forall>a'. atom a' \<sharp> h \<longrightarrow> h a' = h a"
- proof (intro strip)
- fix a':: 'a
- assume c: "atom a' \<sharp> h"
- from a have "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" by (rule freshness_lemma)
- with b c show "h a' = h a" by auto
- qed
-next
- fix fr :: 'b
- assume "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = fr"
- with b show "fr = h a" by auto
-qed
-
-lemma fresh_fun_app':
- fixes h :: "'a::at \<Rightarrow> 'b::pt"
- assumes a: "atom a \<sharp> h" "atom a \<sharp> h a"
- shows "fresh_fun h = h a"
- apply (rule fresh_fun_app)
- apply (auto simp add: fresh_Pair intro: a)
- done
-
-lemma fresh_fun_eqvt:
- fixes h :: "'a::at \<Rightarrow> 'b::pt"
- assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
- shows "p \<bullet> (fresh_fun h) = fresh_fun (p \<bullet> h)"
- using a
- apply (clarsimp simp add: fresh_Pair)
- apply (subst fresh_fun_app', assumption+)
- apply (drule fresh_permute_iff [where p=p, THEN iffD2])
- apply (drule fresh_permute_iff [where p=p, THEN iffD2])
- apply (simp add: atom_eqvt permute_fun_app_eq [where f=h])
- apply (erule (1) fresh_fun_app' [symmetric])
- done
-
-lemma fresh_fun_supports:
- fixes h :: "'a::at \<Rightarrow> 'b::pt"
- assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
- shows "(supp h) supports (fresh_fun h)"
- apply (simp add: supports_def fresh_def [symmetric])
- apply (simp add: fresh_fun_eqvt [OF a] swap_fresh_fresh)
- done
-
-notation fresh_fun (binder "FRESH " 10)
-
-lemma FRESH_f_iff:
- fixes P :: "'a::at \<Rightarrow> 'b::pure"
- fixes f :: "'b \<Rightarrow> 'c::pure"
- assumes P: "finite (supp P)"
- shows "(FRESH x. f (P x)) = f (FRESH x. P x)"
-proof -
- obtain a::'a where "atom a \<notin> supp P"
- using P by (rule obtain_at_base)
- hence "atom a \<sharp> P"
- by (simp add: fresh_def)
- show "(FRESH x. f (P x)) = f (FRESH x. P x)"
- apply (subst fresh_fun_app' [where a=a, OF _ pure_fresh])
- apply (cut_tac `atom a \<sharp> P`)
- apply (simp add: fresh_conv_MOST)
- apply (elim MOST_rev_mp, rule MOST_I, clarify)
- apply (simp add: permute_fun_def permute_pure expand_fun_eq)
- apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> P` pure_fresh])
- apply (rule refl)
- done
-qed
-
-lemma FRESH_binop_iff:
- fixes P :: "'a::at \<Rightarrow> 'b::pure"
- fixes Q :: "'a::at \<Rightarrow> 'c::pure"
- fixes binop :: "'b \<Rightarrow> 'c \<Rightarrow> 'd::pure"
- assumes P: "finite (supp P)"
- and Q: "finite (supp Q)"
- shows "(FRESH x. binop (P x) (Q x)) = binop (FRESH x. P x) (FRESH x. Q x)"
-proof -
- from assms have "finite (supp P \<union> supp Q)" by simp
- then obtain a::'a where "atom a \<notin> (supp P \<union> supp Q)"
- by (rule obtain_at_base)
- hence "atom a \<sharp> P" and "atom a \<sharp> Q"
- by (simp_all add: fresh_def)
- show ?thesis
- apply (subst fresh_fun_app' [where a=a, OF _ pure_fresh])
- apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`)
- apply (simp add: fresh_conv_MOST)
- apply (elim MOST_rev_mp, rule MOST_I, clarify)
- apply (simp add: permute_fun_def permute_pure expand_fun_eq)
- apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> P` pure_fresh])
- apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> Q` pure_fresh])
- apply (rule refl)
- done
-qed
-
-lemma FRESH_conj_iff:
- fixes P Q :: "'a::at \<Rightarrow> bool"
- assumes P: "finite (supp P)" and Q: "finite (supp Q)"
- shows "(FRESH x. P x \<and> Q x) \<longleftrightarrow> (FRESH x. P x) \<and> (FRESH x. Q x)"
-using P Q by (rule FRESH_binop_iff)
-
-lemma FRESH_disj_iff:
- fixes P Q :: "'a::at \<Rightarrow> bool"
- assumes P: "finite (supp P)" and Q: "finite (supp Q)"
- shows "(FRESH x. P x \<or> Q x) \<longleftrightarrow> (FRESH x. P x) \<or> (FRESH x. Q x)"
-using P Q by (rule FRESH_binop_iff)
-
-
-section {* @{const nat_of} is an example of a function
- without finite support *}
-
-
-lemma not_fresh_nat_of:
- shows "\<not> a \<sharp> nat_of"
-unfolding fresh_def supp_def
-proof (clarsimp)
- assume "finite {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"
- hence "finite ({a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of})"
- by simp
- then obtain b where
- b1: "b \<noteq> a" and
- b2: "sort_of b = sort_of a" and
- b3: "(a \<rightleftharpoons> b) \<bullet> nat_of = nat_of"
- by (rule obtain_atom) auto
- have "nat_of a = (a \<rightleftharpoons> b) \<bullet> (nat_of a)" by (simp add: permute_nat_def)
- also have "\<dots> = ((a \<rightleftharpoons> b) \<bullet> nat_of) ((a \<rightleftharpoons> b) \<bullet> a)" by (simp add: permute_fun_app_eq)
- 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_components_eq_iff)
- with b1 show "False" by simp
-qed
-
-lemma supp_nat_of:
- shows "supp nat_of = UNIV"
- using not_fresh_nat_of [unfolded fresh_def] by auto
-
-
-section {* Induction principle for permutations *}
-
-
-lemma perm_struct_induct[consumes 1, case_names zero swap]:
- assumes S: "supp p \<subseteq> S"
- 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 "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
- have as: "supp p \<subseteq> S" by fact
- { assume "supp p = {}"
- then have "p = 0" by (simp add: supp_perm expand_perm_eq)
- then have "P p" using zero by simp
- }
- moreover
- { assume "supp p \<noteq> {}"
- then obtain a where a0: "a \<in> supp p" by blast
- 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 \<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 a2 by auto
- then have "P ?q" using ih by simp
- moreover
- have "supp ?q \<subseteq> S" using as a2 by simp
- ultimately have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp
- moreover
- 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_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"
-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"
- 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_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
- next
- case (swap a b)
- then have "a \<sharp> x" "b \<sharp> x" by simp_all
- then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh)
- next
- case (plus p1 p2)
- have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+
- then show "(p1 + p2) \<bullet> x = x" by simp
- qed
-qed
-
-
-section {* Support of Finite Sets of Finitely Supported Elements *}
-
-lemma Union_fresh:
- shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"
- unfolding Union_image_eq[symmetric]
- apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app)
- apply(perm_simp)
- apply(rule refl)
- apply(assumption)
- done
-
-lemma Union_supports_set:
- shows "(\<Union>x \<in> S. supp x) supports S"
-proof -
- { fix a b
- have "\<forall>x \<in> S. (a \<rightleftharpoons> b) \<bullet> x = x \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> S = S"
- unfolding permute_set_eq by force
- }
- then show "(\<Union>x \<in> S. supp x) supports S"
- unfolding supports_def
- by (simp add: fresh_def[symmetric] swap_fresh_fresh)
-qed
-
-lemma Union_of_fin_supp_sets:
- fixes S::"('a::fs set)"
- assumes fin: "finite S"
- shows "finite (\<Union>x\<in>S. supp x)"
- using fin by (induct) (auto simp add: finite_supp)
-
-lemma Union_included_in_supp:
- fixes S::"('a::fs set)"
- assumes fin: "finite S"
- shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
-proof -
- have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
- by (rule supp_finite_atom_set[symmetric])
- (rule Union_of_fin_supp_sets[OF fin])
- also have "\<dots> \<subseteq> supp S"
- by (rule supp_subset_fresh)
- (simp add: Union_fresh)
- finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .
-qed
-
-lemma supp_of_fin_sets:
- fixes S::"('a::fs set)"
- assumes fin: "finite S"
- shows "(supp S) = (\<Union>x\<in>S. supp x)"
-apply(rule subset_antisym)
-apply(rule supp_is_subset)
-apply(rule Union_supports_set)
-apply(rule Union_of_fin_supp_sets[OF fin])
-apply(rule Union_included_in_supp[OF fin])
-done
-
-lemma supp_of_fin_union:
- fixes S T::"('a::fs) set"
- assumes fin1: "finite S"
- and fin2: "finite T"
- shows "supp (S \<union> T) = supp S \<union> supp T"
- using fin1 fin2
- by (simp add: supp_of_fin_sets)
-
-lemma supp_of_fin_insert:
- fixes S::"('a::fs) set"
- assumes fin: "finite S"
- shows "supp (insert x S) = supp x \<union> supp S"
- using fin
- by (simp add: supp_of_fin_sets)
-
-
-end
--- a/Nominal-General/nominal_atoms.ML Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal-General/nominal_atoms.ML Sat Sep 04 14:26:09 2010 +0800
@@ -26,7 +26,7 @@
fun add_atom_decl (name : binding, arg : binding option) (thy : theory) =
let
- val _ = Theory.requires thy "Nominal2_Atoms" "nominal logic";
+ val _ = Theory.requires thy "Nominal2_Base" "nominal logic";
val str = Sign.full_name thy name;
(* typedef *)
--- a/Nominal-General/nominal_library.ML Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal-General/nominal_library.ML Sat Sep 04 14:26:09 2010 +0800
@@ -49,6 +49,7 @@
val mk_append: term * term -> term
val mk_union: term * term -> term
val fold_union: term list -> term
+ val fold_append: term list -> term
val mk_conj: term * term -> term
val fold_conj: term list -> term
@@ -144,6 +145,8 @@
fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}
| mk_diff (t1, @{term "{}::atom set"}) = t1
+ | mk_diff (@{term "set ([]::atom list)"}, _) = @{term "set ([]::atom list)"}
+ | mk_diff (t1, @{term "set ([]::atom list)"}) = t1
| mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)
fun mk_append (t1, @{term "[]::atom list"}) = t1
@@ -152,9 +155,12 @@
fun mk_union (t1, @{term "{}::atom set"}) = t1
| mk_union (@{term "{}::atom set"}, t2) = t2
+ | mk_union (t1, @{term "set ([]::atom list)"}) = t1
+ | mk_union (@{term "set ([]::atom list)"}, t2) = t2
| mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2)
fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"}
+fun fold_append trms = fold_rev (curry mk_append) trms @{term "[]::atom list"}
fun mk_conj (t1, @{term "True"}) = t1
| mk_conj (@{term "True"}, t2) = t2
--- a/Nominal/Abs.thy Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal/Abs.thy Sat Sep 04 14:26:09 2010 +0800
@@ -1,17 +1,16 @@
theory Abs
-imports "../Nominal-General/Nominal2_Atoms"
+imports "../Nominal-General/Nominal2_Base"
"../Nominal-General/Nominal2_Eqvt"
- "../Nominal-General/Nominal2_Supp"
"Quotient"
"Quotient_List"
"Quotient_Product"
begin
fun
- alpha_gen
+ alpha_set
where
- alpha_gen[simp del]:
- "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow>
+ alpha_set[simp del]:
+ "alpha_set (bs, x) R f pi (cs, y) \<longleftrightarrow>
f x - bs = f y - cs \<and>
(f x - bs) \<sharp>* pi \<and>
R (pi \<bullet> x) y \<and>
@@ -36,17 +35,17 @@
R (pi \<bullet> x) y \<and>
pi \<bullet> bs = cs"
-lemmas alphas = alpha_gen.simps alpha_res.simps alpha_lst.simps
+lemmas alphas = alpha_set.simps alpha_res.simps alpha_lst.simps
notation
- alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100) and
+ alpha_set ("_ \<approx>set _ _ _ _" [100, 100, 100, 100, 100] 100) and
alpha_res ("_ \<approx>res _ _ _ _" [100, 100, 100, 100, 100] 100) and
alpha_lst ("_ \<approx>lst _ _ _ _" [100, 100, 100, 100, 100] 100)
section {* Mono *}
lemma [mono]:
- shows "R1 \<le> R2 \<Longrightarrow> alpha_gen bs R1 \<le> alpha_gen bs R2"
+ shows "R1 \<le> R2 \<Longrightarrow> alpha_set bs R1 \<le> alpha_set bs R2"
and "R1 \<le> R2 \<Longrightarrow> alpha_res bs R1 \<le> alpha_res bs R2"
and "R1 \<le> R2 \<Longrightarrow> alpha_lst cs R1 \<le> alpha_lst cs R2"
by (case_tac [!] bs, case_tac [!] cs)
@@ -55,7 +54,7 @@
section {* Equivariance *}
lemma alpha_eqvt[eqvt]:
- shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+ shows "(bs, x) \<approx>set R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>set (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
and "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
and "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)"
unfolding alphas
@@ -70,7 +69,7 @@
lemma alpha_refl:
assumes a: "R x x"
- shows "(bs, x) \<approx>gen R f 0 (bs, x)"
+ shows "(bs, x) \<approx>set R f 0 (bs, x)"
and "(bs, x) \<approx>res R f 0 (bs, x)"
and "(cs, x) \<approx>lst R f 0 (cs, x)"
using a
@@ -80,7 +79,7 @@
lemma alpha_sym:
assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
- shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
+ shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set R f (- p) (bs, x)"
and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
unfolding alphas fresh_star_def
@@ -89,7 +88,7 @@
lemma alpha_trans:
assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
- shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
+ shows "\<lbrakk>(bs, x) \<approx>set R f p (cs, y); (cs, y) \<approx>set R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>set R f (q + p) (ds, z)"
and "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
and "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
using a
@@ -99,7 +98,7 @@
lemma alpha_sym_eqvt:
assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)"
and b: "p \<bullet> R = R"
- shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
+ shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set R f (- p) (bs, x)"
and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
apply(auto intro!: alpha_sym)
@@ -113,12 +112,12 @@
apply(assumption)
done
-lemma alpha_gen_trans_eqvt:
- assumes b: "(cs, y) \<approx>gen R f q (ds, z)"
- and a: "(bs, x) \<approx>gen R f p (cs, y)"
+lemma alpha_set_trans_eqvt:
+ assumes b: "(cs, y) \<approx>set R f q (ds, z)"
+ and a: "(bs, x) \<approx>set R f p (cs, y)"
and d: "q \<bullet> R = R"
and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
- shows "(bs, x) \<approx>gen R f (q + p) (ds, z)"
+ shows "(bs, x) \<approx>set R f (q + p) (ds, z)"
apply(rule alpha_trans)
defer
apply(rule a)
@@ -173,16 +172,16 @@
apply(simp add: permute_eqvt[symmetric])
done
-lemmas alpha_trans_eqvt = alpha_gen_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
+lemmas alpha_trans_eqvt = alpha_set_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
section {* General Abstractions *}
fun
- alpha_abs
+ alpha_abs_set
where
[simp del]:
- "alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
+ "alpha_abs_set (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op=) supp p (cs, y))"
fun
alpha_abs_lst
@@ -197,15 +196,15 @@
"alpha_abs_res (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (cs, y))"
notation
- alpha_abs (infix "\<approx>abs" 50) and
+ alpha_abs_set (infix "\<approx>abs'_set" 50) and
alpha_abs_lst (infix "\<approx>abs'_lst" 50) and
alpha_abs_res (infix "\<approx>abs'_res" 50)
-lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps
+lemmas alphas_abs = alpha_abs_set.simps alpha_abs_res.simps alpha_abs_lst.simps
lemma alphas_abs_refl:
- shows "(bs, x) \<approx>abs (bs, x)"
+ shows "(bs, x) \<approx>abs_set (bs, x)"
and "(bs, x) \<approx>abs_res (bs, x)"
and "(cs, x) \<approx>abs_lst (cs, x)"
unfolding alphas_abs
@@ -215,7 +214,7 @@
(simp_all add: fresh_zero_perm)
lemma alphas_abs_sym:
- shows "(bs, x) \<approx>abs (cs, y) \<Longrightarrow> (cs, y) \<approx>abs (bs, x)"
+ shows "(bs, x) \<approx>abs_set (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_set (bs, x)"
and "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_res (bs, x)"
and "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (es, y) \<approx>abs_lst (ds, x)"
unfolding alphas_abs
@@ -225,7 +224,7 @@
(auto simp add: fresh_minus_perm)
lemma alphas_abs_trans:
- shows "\<lbrakk>(bs, x) \<approx>abs (cs, y); (cs, y) \<approx>abs (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs (ds, z)"
+ shows "\<lbrakk>(bs, x) \<approx>abs_set (cs, y); (cs, y) \<approx>abs_set (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs_set (ds, z)"
and "\<lbrakk>(bs, x) \<approx>abs_res (cs, y); (cs, y) \<approx>abs_res (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs_res (ds, z)"
and "\<lbrakk>(es, x) \<approx>abs_lst (gs, y); (gs, y) \<approx>abs_lst (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>abs_lst (hs, z)"
unfolding alphas_abs
@@ -236,7 +235,7 @@
by (simp_all add: fresh_plus_perm)
lemma alphas_abs_eqvt:
- shows "(bs, x) \<approx>abs (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs (p \<bullet> cs, p \<bullet> y)"
+ shows "(bs, x) \<approx>abs_set (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs_set (p \<bullet> cs, p \<bullet> y)"
and "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs_res (p \<bullet> cs, p \<bullet> y)"
and "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>abs_lst (p \<bullet> es, p \<bullet> y)"
unfolding alphas_abs
@@ -249,7 +248,7 @@
by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
quotient_type
- 'a abs_gen = "(atom set \<times> 'a::pt)" / "alpha_abs"
+ 'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set"
and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst"
apply(rule_tac [!] equivpI)
@@ -257,9 +256,9 @@
by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
quotient_definition
- Abs ("[_]set. _" [60, 60] 60)
+ Abs_set ("[_]set. _" [60, 60] 60)
where
- "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen"
+ "Abs_set::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_set"
is
"Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
@@ -278,21 +277,21 @@
"Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)"
lemma [quot_respect]:
- shows "(op= ===> op= ===> alpha_abs) Pair Pair"
+ shows "(op= ===> op= ===> alpha_abs_set) Pair Pair"
and "(op= ===> op= ===> alpha_abs_res) Pair Pair"
and "(op= ===> op= ===> alpha_abs_lst) Pair Pair"
unfolding fun_rel_def
by (auto intro: alphas_abs_refl)
lemma [quot_respect]:
- shows "(op= ===> alpha_abs ===> alpha_abs) permute permute"
+ shows "(op= ===> alpha_abs_set ===> alpha_abs_set) permute permute"
and "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute"
and "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute"
unfolding fun_rel_def
by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
lemma abs_exhausts:
- shows "(\<And>as (x::'a::pt). y1 = Abs as x \<Longrightarrow> P1) \<Longrightarrow> P1"
+ shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1"
and "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2"
and "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3"
by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"]
@@ -300,22 +299,22 @@
prod.exhaust[where 'a="atom list" and 'b="'a"])
lemma abs_eq_iff:
- shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
+ shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (bs, x) \<approx>abs_set (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)"
unfolding alphas_abs by (lifting alphas_abs)
-instantiation abs_gen :: (pt) pt
+instantiation abs_set :: (pt) pt
begin
quotient_definition
- "permute_abs_gen::perm \<Rightarrow> ('a::pt abs_gen) \<Rightarrow> 'a abs_gen"
+ "permute_abs_set::perm \<Rightarrow> ('a::pt abs_set) \<Rightarrow> 'a abs_set"
is
"permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
lemma permute_Abs[simp]:
fixes x::"'a::pt"
- shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"
+ shows "(p \<bullet> (Abs_set as x)) = Abs_set (p \<bullet> as) (p \<bullet> x)"
by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
instance
@@ -368,13 +367,13 @@
end
-lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst
+lemmas permute_abs[eqvt] = permute_Abs permute_Abs_res permute_Abs_lst
lemma abs_swap1:
assumes a1: "a \<notin> (supp x) - bs"
and a2: "b \<notin> (supp x) - bs"
- shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+ shows "Abs_set bs x = Abs_set ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
unfolding abs_eq_iff
unfolding alphas_abs
@@ -401,7 +400,7 @@
(auto simp add: supp_perm swap_atom)
lemma abs_supports:
- shows "((supp x) - as) supports (Abs as x)"
+ shows "((supp x) - as) supports (Abs_set as x)"
and "((supp x) - as) supports (Abs_res as x)"
and "((supp x) - set bs) supports (Abs_lst bs x)"
unfolding supports_def
@@ -409,15 +408,15 @@
by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
function
- supp_gen :: "('a::pt) abs_gen \<Rightarrow> atom set"
+ supp_set :: "('a::pt) abs_set \<Rightarrow> atom set"
where
- "supp_gen (Abs as x) = supp x - as"
+ "supp_set (Abs_set as x) = supp x - as"
apply(case_tac x rule: abs_exhausts(1))
apply(simp)
apply(simp add: abs_eq_iff alphas_abs alphas)
done
-termination supp_gen
+termination supp_set
by (auto intro!: local.termination)
function
@@ -445,7 +444,7 @@
by (auto intro!: local.termination)
lemma [eqvt]:
- shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)"
+ shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)"
and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"
and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"
apply(case_tac x rule: abs_exhausts(1))
@@ -457,15 +456,15 @@
done
lemma aux_fresh:
- shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (Abs bs x)"
+ shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_set (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)"
by (rule_tac [!] fresh_fun_eqvt_app)
- (simp_all add: eqvts_raw)
+ (simp_all only: eqvts_raw)
lemma supp_abs_subset1:
assumes a: "finite (supp x)"
- shows "(supp x) - as \<subseteq> supp (Abs as x)"
+ shows "(supp x) - as \<subseteq> supp (Abs_set as x)"
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
@@ -474,7 +473,7 @@
lemma supp_abs_subset2:
assumes a: "finite (supp x)"
- shows "supp (Abs as x) \<subseteq> (supp x) - as"
+ shows "supp (Abs_set 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)"
by (rule_tac [!] supp_is_subset)
@@ -482,7 +481,7 @@
lemma abs_finite_supp:
assumes a: "finite (supp x)"
- shows "supp (Abs as x) = (supp x) - as"
+ shows "supp (Abs_set as x) = (supp x) - as"
and "supp (Abs_res as x) = (supp x) - as"
and "supp (Abs_lst bs x) = (supp x) - (set bs)"
by (rule_tac [!] subset_antisym)
@@ -490,13 +489,13 @@
lemma supp_abs:
fixes x::"'a::fs"
- shows "supp (Abs as x) = (supp x) - as"
+ shows "supp (Abs_set as x) = (supp x) - as"
and "supp (Abs_res as x) = (supp x) - as"
and "supp (Abs_lst bs x) = (supp x) - (set bs)"
by (rule_tac [!] abs_finite_supp)
(simp_all add: finite_supp)
-instance abs_gen :: (fs) fs
+instance abs_set :: (fs) fs
apply(default)
apply(case_tac x rule: abs_exhausts(1))
apply(simp add: supp_abs finite_supp)
@@ -516,13 +515,22 @@
lemma abs_fresh_iff:
fixes x::"'a::fs"
- shows "a \<sharp> Abs bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
+ shows "a \<sharp> Abs_set bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
and "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
and "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)"
unfolding fresh_def
unfolding supp_abs
by auto
+lemma Abs_eq_iff:
+ shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y))"
+ and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
+ and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
+ by (lifting alphas_abs)
+
+
+section {* Infrastructure for building tuples of relations and functions *}
+
fun
prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
where
@@ -560,16 +568,5 @@
by (perm_simp) (rule refl)
-(* Below seems to be not needed *)
-
-(*
-lemma Abs_eq_iff:
- shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
- and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
- and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
- by (lifting alphas_abs)
-*)
-
-
end
--- a/Nominal/Ex/SingleLet.thy Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal/Ex/SingleLet.thy Sat Sep 04 14:26:09 2010 +0800
@@ -10,18 +10,17 @@
Var "name"
| App "trm" "trm"
| Lam x::"name" t::"trm" bind x in t
-| Let a::"assg" t::"trm" bind (set) "bn a" in t
+| Let a::"assg" t::"trm" bind "bn a" in t
| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
| Bar x::"name" y::"name" t::"trm" bind y x in t x y
| Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2
and assg =
As "name" x::"name" t::"trm" bind x in t
binder
- bn::"assg \<Rightarrow> atom set"
+ bn::"assg \<Rightarrow> atom list"
where
- "bn (As x y t) = {atom x}"
+ "bn (As x y t) = [atom x]"
-thm Ball_def Bex_def mem_def
thm single_let.distinct
thm single_let.induct
@@ -35,47 +34,106 @@
thm single_let.supports
thm single_let.fsupp
+lemma test2:
+ assumes "fv_trm t = supp t"
+ shows "\<forall>p. fv_trm (p \<bullet> t) = supp (p \<bullet> t)"
+apply(rule allI)
+apply(rule_tac p="-p" in permute_boolE)
+apply(perm_simp add: single_let.fv_bn_eqvt permute_minus_cancel)
+apply(rule assms)
+done
+
+
+lemma supp_fv:
+ "fv_trm t = supp t \<and> fv_assg as = supp as \<and> fv_bn as = {a. infinite {b. \<not>alpha_bn ((a \<rightleftharpoons> b) \<bullet> as) as}}"
+apply(rule single_let.induct)
+apply(simp_all (no_asm_use) only: single_let.fv_defs)[2]
+apply(simp_all (no_asm_use) only: supp_def)[2]
+apply(simp_all (no_asm_use) only: single_let.perm_simps)[2]
+apply(simp_all (no_asm_use) only: single_let.eq_iff)[2]
+apply(simp_all (no_asm_use) only: de_Morgan_conj)[2]
+apply(simp_all (no_asm_use) only: Collect_disj_eq)[2]
+apply(simp_all (no_asm_use) only: finite_Un)[2]
+apply(simp_all (no_asm_use) only: de_Morgan_conj)[2]
+apply(simp_all (no_asm_use) only: Collect_disj_eq)[2]
+apply(simp)
+--" 1 "
+apply(simp only: single_let.fv_defs supp_Pair[symmetric])
+apply(simp only: supp_abs(3)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
+apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
+apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
+apply(drule test2)
+apply(simp only:)
+-- " 2 "
+apply(erule conjE)+
+apply(simp only: single_let.fv_defs supp_Pair[symmetric])
+apply(simp only: supp_abs(3)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
+apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
+apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un)
+apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
+apply(drule test2)
+apply(simp only:)
+-- " 3 "
+apply(simp only: single_let.fv_defs supp_Pair[symmetric])
+apply(simp only: supp_abs(1)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
+apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
+apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
+apply(drule test2)+
+apply(simp only: supp_Pair Un_assoc conj_assoc)
+-- " Bar "
+apply(simp only: single_let.fv_defs supp_Pair[symmetric])
+apply(simp only: supp_abs(3)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
+apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
+apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
+apply(drule test2)+
+apply(simp only: supp_Pair Un_assoc conj_assoc)
+-- " Baz "
+apply(simp only: single_let.fv_defs supp_Pair[symmetric])
+apply(simp only: supp_abs(3)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
+apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
+apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
+apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un)
+apply(drule test2)+
+apply(simp only: supp_Pair Un_assoc conj_assoc)
+-- "last"
+apply(rule conjI)
+apply(simp only: single_let.fv_defs supp_Pair[symmetric])
+apply(simp only: supp_abs(3)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
+apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
+apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
+apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un)
+apply(drule test2)+
+apply(simp only: supp_Pair Un_assoc conj_assoc)
+-- "other case"
+apply(simp only: single_let.fv_defs supp_Pair[symmetric])
+apply(simp only: supp_abs(3)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
+apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
+apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
+apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un)?
+apply(drule test2)+
+apply(simp only: supp_Pair Un_assoc conj_assoc)
+done
-(*
-lemma test:
- "(\<exists>p. (bs, x) \<approx>lst (op=) f p (cs, y)) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"
-oops
-lemma Abs_eq_iff:
- shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
- and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
- and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
- by (lifting alphas_abs)
-*)
-(*
-lemma supp_fv:
- "supp t = fv_trm t \<and> supp b = fv_bn b"
-apply(rule single_let.induct)
-apply(simp_all only: single_let.fv_defs)[2]
-apply(simp_all only: supp_def)[2]
-apply(simp_all only: single_let.perm_simps)[2]
-apply(simp_all only: single_let.eq_iff)[2]
-apply(simp_all only: de_Morgan_conj)[2]
-apply(simp_all only: Collect_disj_eq)[2]
-apply(simp_all only: finite_Un)[2]
-apply(simp_all only: de_Morgan_conj)[2]
-apply(simp_all only: Collect_disj_eq)[2]
-apply(subgoal_tac "supp (Lam name trm) = supp (Abs_lst [atom name] trm)")
-apply(simp only: single_let.fv_defs)
-apply(simp only: supp_abs)
-apply(simp)
-apply(simp (no_asm) only: supp_def)
-apply(simp only: single_let.perm_simps)
-apply(simp only: single_let.eq_iff)
-apply(simp only: permute_abs atom_eqvt permute_list.simps)
-apply(simp only: Abs_eq_iff)
-apply(subst test)
-apply(rule refl)
-sorry
-*)
+text {* *}
+
(*
consts perm_bn_trm :: "perm \<Rightarrow> trm \<Rightarrow> trm"
consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg"
--- a/Nominal/Ex/TypeSchemes.thy Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal/Ex/TypeSchemes.thy Sat Sep 04 14:26:09 2010 +0800
@@ -14,15 +14,39 @@
and tys =
All xs::"name fset" ty::"ty" bind (res) xs in ty
+thm ty_tys.distinct
+thm ty_tys.induct
+thm ty_tys.exhaust
+thm ty_tys.fv_defs
+thm ty_tys.bn_defs
+thm ty_tys.perm_simps
+thm ty_tys.eq_iff
+thm ty_tys.fv_bn_eqvt
+thm ty_tys.size_eqvt
+thm ty_tys.supports
+thm ty_tys.fsupp
nominal_datatype ty2 =
Var2 "name"
| Fun2 "ty2" "ty2"
-
nominal_datatype tys2 =
All2 xs::"name fset" ty::"ty2" bind (res) xs in ty
+thm tys2.distinct
+thm tys2.induct
+thm tys2.exhaust
+thm tys2.fv_defs
+thm tys2.bn_defs
+thm tys2.perm_simps
+thm tys2.eq_iff
+thm tys2.fv_bn_eqvt
+thm tys2.size_eqvt
+thm tys2.supports
+thm tys2.fsupp
+
+
+text {* *}
(*
ML {* Sign.of_sort @{theory} (@{typ ty}, @{sort fs}) *}
--- a/Nominal/Nominal2.thy Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal/Nominal2.thy Sat Sep 04 14:26:09 2010 +0800
@@ -2,7 +2,6 @@
imports
"../Nominal-General/Nominal2_Base"
"../Nominal-General/Nominal2_Eqvt"
- "../Nominal-General/Nominal2_Supp"
"Nominal2_FSet"
"Abs"
uses ("nominal_dt_rawperm.ML")
--- a/Nominal/Nominal2_FSet.thy Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal/Nominal2_FSet.thy Sat Sep 04 14:26:09 2010 +0800
@@ -1,6 +1,5 @@
theory Nominal2_FSet
-imports "../Nominal-General/Nominal2_Supp"
- "../Nominal-General/Nominal2_Atoms"
+imports "../Nominal-General/Nominal2_Base"
"../Nominal-General/Nominal2_Eqvt"
FSet
begin
@@ -9,11 +8,8 @@
shows "(op = ===> list_eq ===> list_eq) permute permute"
apply(simp)
apply(clarify)
- apply(simp add: eqvts[symmetric])
- apply(subst permute_minus_cancel(1)[symmetric, of "xb"])
- apply(subst mem_eqvt[symmetric])
- apply(subst (2) permute_minus_cancel(1)[symmetric, of "xb"])
- apply(subst mem_eqvt[symmetric])
+ apply(rule_tac p="-x" in permute_boolE)
+ apply(perm_simp add: permute_minus_cancel)
apply(simp)
done
@@ -36,14 +32,12 @@
end
-lemma permute_fset[simp]:
+lemma permute_fset[simp, eqvt]:
fixes S::"('a::pt) fset"
shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)"
by (lifting permute_list.simps)
-declare permute_fset[eqvt]
-
lemma fmap_eqvt[eqvt]:
shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)"
by (lifting map_eqvt)
@@ -113,7 +107,7 @@
apply (simp add: fresh_set_empty)
apply simp
apply (unfold fresh_def)
- apply (simp add: supp_atom_insert)
+ apply (simp add: supp_of_fin_insert)
apply (rule conjI)
apply (unfold fresh_star_def)
apply simp
--- a/Nominal/nominal_dt_alpha.ML Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal/nominal_dt_alpha.ML Sat Sep 04 14:26:09 2010 +0800
@@ -64,7 +64,7 @@
end
(* generates the compound binder terms *)
-fun mk_binders lthy bmode args bodies =
+fun mk_binders lthy bmode args binders =
let
fun bind_set lthy args (NONE, i) = setify lthy (nth args i)
| bind_set _ args (SOME bn, i) = bn $ (nth args i)
@@ -77,7 +77,7 @@
| Set => (mk_union, bind_set)
| Res => (mk_union, bind_set)
in
- bodies
+ binders
|> map (bind_fn lthy args)
|> foldl1 combine_fn
end
@@ -88,7 +88,7 @@
val (alpha_name, binder_ty) =
case bmode of
Lst => (@{const_name "alpha_lst"}, @{typ "atom list"})
- | Set => (@{const_name "alpha_gen"}, @{typ "atom set"})
+ | Set => (@{const_name "alpha_set"}, @{typ "atom set"})
| Res => (@{const_name "alpha_res"}, @{typ "atom set"})
val ty = fastype_of args
val pair_ty = HOLogic.mk_prodT (binder_ty, ty)
--- a/Nominal/nominal_dt_rawfuns.ML Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal/nominal_dt_rawfuns.ML Sat Sep 04 14:26:09 2010 +0800
@@ -151,7 +151,7 @@
(** functions that construct the equations for fv and fv_bn **)
-fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
+fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) =
let
fun mk_fv_body fv_map args i =
let
@@ -163,21 +163,33 @@
| SOME fv => fv $ arg
end
- fun mk_fv_binder lthy fv_bn_map args (bn_option, i) =
+ fun mk_fv_binder lthy fv_bn_map args binders =
let
- val arg = nth args i
+ fun bind_set lthy args (NONE, i) = (setify lthy (nth args i), @{term "{}::atom set"})
+ | bind_set _ args (SOME bn, i) = (bn $ (nth args i),
+ if member (op=) bodies i then @{term "{}::atom set"}
+ else lookup fv_bn_map bn $ (nth args i))
+ fun bind_lst lthy args (NONE, i) = (listify lthy (nth args i), @{term "[]::atom list"})
+ | bind_lst _ args (SOME bn, i) = (bn $ (nth args i),
+ if member (op=) bodies i then @{term "[]::atom list"}
+ else lookup fv_bn_map bn $ (nth args i))
+
+ val (combine_fn, bind_fn) =
+ case bmode of
+ Lst => (fold_append, bind_lst)
+ | Set => (fold_union, bind_set)
+ | Res => (fold_union, bind_set)
in
- case bn_option of
- NONE => (setify lthy arg, @{term "{}::atom set"})
- | SOME bn => (to_set (bn $ arg),
- if member (op=) bodies i then @{term "{}::atom set"}
- else lookup fv_bn_map bn $ arg)
+ binders
+ |> map (bind_fn lthy args)
+ |> split_list
+ |> pairself combine_fn
end
val t1 = map (mk_fv_body fv_map args) bodies
- val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders)
+ val (t2, t3) = mk_fv_binder lthy fv_bn_map args binders
in
- fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
+ mk_union (mk_diff (fold_union t1, to_set t2), to_set t3)
end
(* in case of fv_bn we have to treat the case special, where an
--- a/Paper/Paper.thy Mon Aug 30 15:59:50 2010 +0900
+++ b/Paper/Paper.thy Sat Sep 04 14:26:09 2010 +0800
@@ -1,6 +1,6 @@
(*<*)
theory Paper
-imports "../Nominal/NewParser" "LaTeXsugar"
+imports "../Nominal/Nominal2" "LaTeXsugar"
begin
consts
@@ -21,21 +21,21 @@
supp ("supp _" [78] 73) and
uminus ("-_" [78] 73) and
If ("if _ then _ else _" 10) and
- alpha_gen ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
+ alpha_set ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup> _") and
fv ("fa'(_')" [100] 100) and
equal ("=") and
- alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
- Abs ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
+ alpha_abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
+ Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
Abs_lst ("[_]\<^bsub>list\<^esub>._") and
Abs_dist ("[_]\<^bsub>#list\<^esub>._") and
Abs_res ("[_]\<^bsub>res\<^esub>._") and
Abs_print ("_\<^bsub>set\<^esub>._") and
Cons ("_::_" [78,77] 73) and
- supp_gen ("aux _" [1000] 10) and
+ supp_set ("aux _" [1000] 10) and
alpha_bn ("_ \<approx>bn _")
consts alpha_trm ::'a
@@ -647,7 +647,7 @@
%
\begin{equation}\label{alphaset}
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
- \multicolumn{3}{l}{@{term "(as, x) \<approx>gen R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+ \multicolumn{3}{l}{@{term "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
& @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
@{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
@{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
@@ -730,7 +730,7 @@
types. For this we define
%
\begin{equation}
- @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}
+ @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}
\end{equation}
\noindent
@@ -762,7 +762,7 @@
The elements in these types will be, respectively, written as:
\begin{center}
- @{term "Abs as x"} \hspace{5mm}
+ @{term "Abs_set as x"} \hspace{5mm}
@{term "Abs_res as x"} \hspace{5mm}
@{term "Abs_lst as x"}
\end{center}
@@ -832,7 +832,7 @@
function @{text aux}, taking an abstraction as argument:
%
\begin{center}
- @{thm supp_gen.simps[THEN eq_reflection, no_vars]}
+ @{thm supp_set.simps[THEN eq_reflection, no_vars]}
\end{center}
\noindent
@@ -842,7 +842,7 @@
This in turn means
%
\begin{center}
- @{term "supp (supp_gen (Abs as x)) \<subseteq> supp (Abs as x)"}
+ @{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
\end{center}
\noindent
@@ -860,7 +860,7 @@
Theorem~\ref{suppabs}.
The method of first considering abstractions of the
- form @{term "Abs as x"} etc is motivated by the fact that
+ form @{term "Abs_set as x"} etc is motivated by the fact that
we can conveniently establish at the Isabelle/HOL level
properties about them. It would be
laborious to write custom ML-code that derives automatically such properties
@@ -1489,7 +1489,7 @@
lets us formally define the premise @{text P} for a non-empty binding clause as:
%
\begin{center}
- \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>gen R fa p (B', D')"}}\;.
+ \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>set R fa p (B', D')"}}\;.
\end{center}
\noindent
--- a/Paper/ROOT.ML Mon Aug 30 15:59:50 2010 +0900
+++ b/Paper/ROOT.ML Sat Sep 04 14:26:09 2010 +0800
@@ -1,3 +1,3 @@
quick_and_dirty := true;
-no_document use_thys ["LaTeXsugar", "../Nominal/NewParser"];
+no_document use_thys ["LaTeXsugar", "../Nominal/Nominal2"];
use_thys ["Paper"];
\ No newline at end of file
--- a/Pearl-jv/Paper.thy Mon Aug 30 15:59:50 2010 +0900
+++ b/Pearl-jv/Paper.thy Sat Sep 04 14:26:09 2010 +0800
@@ -1,9 +1,7 @@
(*<*)
theory Paper
imports "../Nominal-General/Nominal2_Base"
- "../Nominal-General/Nominal2_Atoms"
"../Nominal-General/Nominal2_Eqvt"
- "../Nominal-General/Nominal2_Supp"
"../Nominal-General/Atoms"
"LaTeXsugar"
begin
@@ -44,6 +42,8 @@
section {* Introduction *}
text {*
+ TODO: write about supp of finite sets
+
Nominal Isabelle provides a proving infratructure for
convenient reasoning about programming languages. At its core Nominal
Isabelle is based on the nominal logic work by Pitts at al
--- a/Pearl-jv/ROOT.ML Mon Aug 30 15:59:50 2010 +0900
+++ b/Pearl-jv/ROOT.ML Sat Sep 04 14:26:09 2010 +0800
@@ -1,7 +1,5 @@
no_document use_thys ["../Nominal-General/Nominal2_Base",
- "../Nominal-General/Nominal2_Atoms",
"../Nominal-General/Nominal2_Eqvt",
- "../Nominal-General/Nominal2_Supp",
"../Nominal-General/Atoms",
"LaTeXsugar"];
--- a/Pearl/Paper.thy Mon Aug 30 15:59:50 2010 +0900
+++ b/Pearl/Paper.thy Sat Sep 04 14:26:09 2010 +0800
@@ -1,7 +1,6 @@
(*<*)
theory Paper
imports "../Nominal-General/Nominal2_Base"
- "../Nominal-General/Nominal2_Atoms"
"../Nominal-General/Nominal2_Eqvt"
"../Nominal-General/Atoms"
"LaTeXsugar"
--- a/Pearl/ROOT.ML Mon Aug 30 15:59:50 2010 +0900
+++ b/Pearl/ROOT.ML Sat Sep 04 14:26:09 2010 +0800
@@ -1,5 +1,4 @@
no_document use_thys ["../Nominal-General/Nominal2_Base",
- "../Nominal-General/Nominal2_Atoms",
"../Nominal-General/Nominal2_Eqvt",
"../Nominal-General/Atoms",
"LaTeXsugar"];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/ROOT4.ML Sat Sep 04 14:26:09 2010 +0800
@@ -0,0 +1,6 @@
+show_question_marks := false;
+quick_and_dirty := true;
+
+no_document use_thy "LaTeXsugar";
+
+use_thy "Slides4"
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/Slides4.thy Sat Sep 04 14:26:09 2010 +0800
@@ -0,0 +1,1133 @@
+(*<*)
+theory Slides4
+imports "LaTeXsugar" "Nominal"
+begin
+
+notation (latex output)
+ set ("_") and
+ Cons ("_::/_" [66,65] 65)
+
+(*>*)
+
+text_raw {*
+ \renewcommand{\slidecaption}{Nanjing, 31.~August 2010}
+
+ \newcommand{\abst}[2]{#1.#2}% atom-abstraction
+ \newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing
+ \newcommand{\susp}{{\boldsymbol{\cdot}}}% for suspensions
+ \newcommand{\unit}{\langle\rangle}% unit
+ \newcommand{\app}[2]{#1\,#2}% application
+ \newcommand{\eqprob}{\mathrel{{\approx}?}}
+ \newcommand{\freshprob}{\mathrel{\#?}}
+ \newcommand{\redu}[1]{\stackrel{#1}{\Longrightarrow}}% reduction
+ \newcommand{\id}{\varepsilon}% identity substitution
+
+ \newcommand{\bl}[1]{\textcolor{blue}{#1}}
+ \newcommand{\gr}[1]{\textcolor{gray}{#1}}
+ \newcommand{\rd}[1]{\textcolor{red}{#1}}
+
+ \newcommand{\ok}{\includegraphics[scale=0.07]{ok.png}}
+ \newcommand{\notok}{\includegraphics[scale=0.07]{notok.png}}
+ \newcommand{\largenotok}{\includegraphics[scale=1]{notok.png}}
+
+ \renewcommand{\Huge}{\fontsize{61.92}{77}\selectfont}
+ \newcommand{\veryHuge}{\fontsize{74.3}{93}\selectfont}
+ \newcommand{\VeryHuge}{\fontsize{89.16}{112}\selectfont}
+ \newcommand{\VERYHuge}{\fontsize{107}{134}\selectfont}
+
+ \newcommand{\LL}{$\mathbb{L}\,$}
+
+
+ \pgfdeclareradialshading{smallbluesphere}{\pgfpoint{0.5mm}{0.5mm}}%
+ {rgb(0mm)=(0,0,0.9);
+ rgb(0.9mm)=(0,0,0.7);
+ rgb(1.3mm)=(0,0,0.5);
+ rgb(1.4mm)=(1,1,1)}
+
+ \def\myitemi{\begin{pgfpicture}{-1ex}{-0.55ex}{1ex}{1ex}
+ \usebeamercolor[fg]{subitem projected}
+ {\pgftransformscale{0.8}\pgftext{\normalsize\pgfuseshading{bigsphere}}}
+ \pgftext{%
+ \usebeamerfont*{subitem projected}}
+ \end{pgfpicture}}
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>[t]
+ \frametitle{%
+ \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
+ \\
+ \huge Error-Free Programming\\[-1mm]
+ \huge with Theorem Provers\\[5mm]
+ \end{tabular}}
+ \begin{center}
+ Christian Urban
+ \end{center}
+ \begin{center}
+ \small Technical University of Munich, Germany\\[7mm]
+
+ \small in Nanjing on the kind invitation of\\ Professor Xingyuan Zhang
+ and his group
+ \end{center}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[c]
+ \frametitle{My Background}
+
+ \begin{itemize}
+ \item researcher in Theoretical Computer Science\medskip
+
+ \item programmer on a \alert<2->{software system} with 800 kloc (though I am
+ responsible only for 35 kloc)
+ \end{itemize}
+
+ \only<2->{
+ \begin{textblock}{6}(2,11)
+ \begin{tikzpicture}
+ \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ {\color{darkgray}
+ \begin{minipage}{4cm}\raggedright
+ A theorem prover called {\bf Isabelle}.
+ \end{minipage}};
+ \end{tikzpicture}
+ \end{textblock}}
+
+
+ \only<3>{
+ \begin{textblock}{6}(9,11)
+ \begin{tikzpicture}
+ \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ {\color{darkgray}
+ \begin{minipage}{4cm}\raggedright
+ Like every other code, this code is very hard to
+ get correct.
+ \end{minipage}};
+ \end{tikzpicture}
+ \end{textblock}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[t]
+ \frametitle{Regular Expressions}
+
+ An example many (should) know about:\\
+ \rd{\bf Regular Expressions:}
+
+ \only<2>{
+ \begin{center}
+ \bl{[] $\;\;\;|\;\;\;$ c $\;\;\;|\;\;\;$ r$_1$$|$r$_2$ $\;\;\;|\;\;\;$
+ r$_1$$\cdot$r$_2$ $\;\;\;|\;\;\;$ r$^*$}
+ \end{center}}
+ \only<3->{
+ \begin{center}
+ \begin{tabular}{@ {}rrll@ {}}
+ \bl{r} & \bl{$::=$} & \bl{NULL} & \gr{(matches no string)}\\
+ & \bl{$\mid$} & \bl{EMPTY} & \gr{(matches the empty string, [])}\\
+ & \bl{$\mid$} & \bl{CHR c} & \gr{(matches the character c)}\\
+ & \bl{$\mid$} & \bl{ALT r$_1$ r$_2$} & \gr{(alternative, r$_1 |\,$r$_2$)}\\
+ & \bl{$\mid$} & \bl{SEQ r$_1$ r$_2$} & \gr{(sequential, r$_1\cdot\,$r$_2$)}\\
+ & \bl{$\mid$} & \bl{STAR r} & \gr{(repeat, r$^*$)}\\
+ \end{tabular}
+ \end{center}\medskip}
+
+ \small
+ \begin{textblock}{14.5}(1,12.5)
+ \only<2->{\gr{(a$\cdot$b)$^*$ \hspace{3mm}$\mapsto$\hspace{3mm} \{[], ab, abab, ababab, \ldots\}}\\}
+ \only<2->{\gr{x$\cdot$(0 $|$ 1 $|$ 2 \ldots 8 $|$ 9)$^*$ \hspace{3mm}$\mapsto$\hspace{3mm}
+ \{x, x0, x1, \ldots, x00, \ldots, x123, \ldots\}}}
+ \end{textblock}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>[c]
+ \frametitle{RegExp Matcher}
+
+ Let's implement a regular expression matcher:\bigskip
+
+ \begin{center}
+ \begin{tikzpicture}
+ %%\draw[help lines, black] (-3,0) grid (6,3);
+
+ \draw[line width=1mm, red] (0.0,0.0) rectangle (4,2.3);
+ \node[anchor=base] at (2,1)
+ {\small\begin{tabular}{@ {}c@ {}}\Large\bf Regular\\
+ \Large\bf Expression \\
+ \Large\bf Matcher\end{tabular}};
+
+ \coordinate (m1) at (0,1.5);
+ \draw (-2,2) node (m2) {\small\begin{tabular}{c}\bl{regular}\\[-1mm] \bl{expression}\end{tabular}};
+ \path[overlay, ->, line width = 1mm, shorten <=-3mm] (m2) edge (m1);
+
+ \coordinate (s1) at (0,0.5);
+ \draw (-1.8,-0) node (s2) {\small\begin{tabular}{c}\bl{string}\end{tabular}};
+ \path[overlay, ->, line width = 1mm, shorten <=-3mm] (s2) edge (s1);
+
+ \coordinate (r1) at (4,1.2);
+ \draw (6,1.2) node (r2) {\small\begin{tabular}{c}\bl{true}, \bl{false}\end{tabular}};
+ \path[overlay, ->, line width = 1mm, shorten >=-3mm] (r1) edge (r2);
+
+ \end{tikzpicture}
+ \end{center}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[t]
+ \frametitle{RegExp Matcher}
+ \small
+
+ {\bf input:} a \underline{list} of RegExps and a string \hspace{6mm}{\bf output:} true or false
+
+ \only<2->{
+ \begin{center}
+ \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
+ \bl{match [] []} & \bl{$=$} & \bl{true}\\
+ \bl{match [] \_} & \bl{$=$} & \bl{false}\\
+ \bl{match (NULL::rs) s} & \bl{$=$} & \bl{false}\\
+ \bl{match (EMPTY::rs) s} & \bl{$=$} & \bl{match rs s}\\
+ \bl{match (CHR c::rs) (c::s)} & \bl{$=$} & \bl{match rs s}\\
+ \bl{match (CHR c::rs) \_} & \bl{$=$} & \bl{false}\\
+ \bl{match (ALT r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s}\\
+ & & \bl{\;\;\;\;orelse match (r$_2$::rs) s}\\
+ \bl{match (SEQ r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s}\\
+ \bl{match (STAR r::rs) s} & \bl{$=$} & \bl{match rs s}\\
+ & & \bl{\;\;\;\;orelse match (r::STAR r::rs) s}\\
+ \end{tabular}
+ \end{center}}
+
+ \onslide<3->{we start the program with\\
+ \hspace{6mm}\bl{matches r s $=$ match [r] s}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>[c]
+ \frametitle{Program in Scala}
+
+ \bl{\footnotesize
+ \begin{tabular}{l}
+ sealed abstract class Rexp\\
+ sealed case class Null extends Rexp\\
+ sealed case class Empty extends Rexp\\
+ sealed case class Chr(c: Char) extends Rexp\\
+ sealed case class Alt(r1 : Rexp, r2 : Rexp) extends Rexp\\
+ sealed case class Seq(r1 : Rexp, r2 : Rexp) extends Rexp\\
+ sealed case class Star(r : Rexp) extends Rexp\medskip\\
+ def match1 (rs : List[Rexp], s : List[Char]) : Boolean = rs match \{\\
+ \hspace{3mm}case Nil @{text "\<Rightarrow>"} if (s == Nil) true else false\\
+ \hspace{3mm}case (Null()::rs) @{text "\<Rightarrow>"} false\\
+ \hspace{3mm}case (Empty()::rs) @{text "\<Rightarrow>"} match1 (rs, s)\\
+ \hspace{3mm}case (Chr(c)::rs) @{text "\<Rightarrow>"} s match \\
+ \hspace{6mm}\{ case Nil @{text "\<Rightarrow>"} false\\
+ \hspace{8mm}case (d::s) @{text "\<Rightarrow>"} if (c==d) match1 (rs,s) else false \}\\
+ \hspace{3mm}case (Alt (r1, r2)::rs) @{text "\<Rightarrow>"} match1 (r1::rs, s) || match1 (r2::rs, s)\\
+ \hspace{3mm}case (Seq (r1, r2)::rs) @{text "\<Rightarrow>"} match1 (r1::r2::rs, s) \\
+ \hspace{3mm}case (Star (r)::rs) @{text "\<Rightarrow>"} match1 (r::rs, s) || match1 (r::Star (r)::rs, s)\\
+ \}
+ \end{tabular}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[c]
+ \frametitle{Testing}
+
+ \small
+ Every good programmer should do thourough tests:
+
+
+ \begin{center}
+ \begin{tabular}{@ {\hspace{-20mm}}lcl}
+ \bl{matches (a$\cdot$b)$^*\;$ []} & \bl{$\mapsto$} & \bl{true}\\
+ \bl{matches (a$\cdot$b)$^*\;$ ab} & \bl{$\mapsto$} & \bl{true}\\
+ \bl{matches (a$\cdot$b)$^*\;$ aba} & \bl{$\mapsto$} & \bl{false}\\
+ \bl{matches (a$\cdot$b)$^*\;$ abab} & \bl{$\mapsto$} & \bl{true}\\
+ \bl{matches (a$\cdot$b)$^*\;$ abaa} & \bl{$\mapsto$} & \bl{false}\medskip\\
+ \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x} & \bl{$\mapsto$} & \bl{true}}\\
+ \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x0} & \bl{$\mapsto$} & \bl{true}}\\
+ \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x3} & \bl{$\mapsto$} & \bl{false}}
+ \end{tabular}
+ \end{center}
+
+ \onslide<3->
+ {looks OK \ldots let's ship it to customers\hspace{5mm}
+ \raisebox{-5mm}{\includegraphics[scale=0.05]{sun.png}}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[t]
+ \frametitle{Testing}
+
+ \begin{itemize}
+ \item While testing is an important part in the process of programming development\pause
+
+ \item we can only test a {\bf finite} amount of examples\bigskip\pause
+
+ \begin{center}
+ \colorbox{cream}
+ {\gr{\begin{minipage}{10cm}
+ ``Testing can only show the presence of errors, never their
+ absence'' (Edsger W.~Dijkstra)
+ \end{minipage}}}
+ \end{center}\bigskip\pause
+
+ \item In a theorem prover we can establish properties that apply to
+ {\bf all} input and {\bf all} output.\pause
+
+ \item For example we can establish that the matcher terminates
+ on all input.
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[t]
+ \frametitle{RegExp Matcher}
+
+ \small
+ We need to find a measure that gets smaller in each recursive call.\bigskip
+
+ \onslide<1->{
+ \begin{center}
+ \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-9mm}}l@ {}}
+ \bl{match [] []} & \bl{$=$} & \bl{true} & \onslide<2->{\ok}\\
+ \bl{match [] \_} & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\
+ \bl{match (NULL::rs) s} & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\
+ \bl{match (EMPTY::rs) s} & \bl{$=$} & \bl{match rs s} & \onslide<3->{\ok}\\
+ \bl{match (CHR c::rs) (c::s)} & \bl{$=$} & \bl{match rs s} & \onslide<4->{\ok}\\
+ \bl{match (CHR c::rs) \_} & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\
+ \bl{match (ALT r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s} & \onslide<5->{\ok}\\
+ & & \bl{\;\;\;\;orelse match (r$_2$::rs) s}\\
+ \bl{match (SEQ r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s} & \onslide<6->{\ok}\\
+ \bl{match (STAR r::rs) s} & \bl{$=$} & \bl{match rs s} & \onslide<7->{\notok}\\
+ & & \bl{\;\;\;\;orelse match (r::STAR r::rs) s}\\
+ \end{tabular}
+ \end{center}}
+
+
+ \begin{textblock}{5}(4,4)
+ \begin{tikzpicture}
+ %%\draw[help lines, black] (-3,0) grid (6,3);
+
+ \coordinate (m1) at (-2,0);
+ \coordinate (m2) at ( 2,0);
+ \path[overlay, ->, line width = 0.6mm, color = red] (m1) edge (m2);
+ \draw (0,0) node[above=-1mm] {\footnotesize\rd{needs to get smaller}};
+ \end{tikzpicture}
+ \end{textblock}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[c]
+ \frametitle{Bug Hunting}
+
+ \only<1>{Several hours later\ldots}\pause
+
+
+ \begin{center}
+ \begin{tabular}{@ {\hspace{-20mm}}lcl}
+ \bl{matches (STAR (EMPTY)) s} & \bl{$\mapsto$} & loops\\
+ \onslide<4->{\bl{matches (STAR (EMPTY $|$ \ldots)) s} & \bl{$\mapsto$} & loops\\}
+ \end{tabular}
+ \end{center}
+
+ \small
+ \onslide<3->{
+ \begin{center}
+ \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
+ \ldots\\
+ \bl{match (EMPTY::rs) s} & \bl{$=$} & \bl{match rs s}\\
+ \ldots\\
+ \bl{match (STAR r::rs) s} & \bl{$=$} & \bl{match rs s}\\
+ & & \bl{\;\;\;\;orelse match (r::STAR r::rs) s}\\
+ \end{tabular}
+ \end{center}}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[c]
+ \frametitle{RegExp Matcher}
+ \small
+
+ \begin{center}
+ \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
+ \bl{match [] []} & \bl{$=$} & \bl{true}\\
+ \bl{match [] \_} & \bl{$=$} & \bl{false}\\
+ \bl{match (NULL::rs) s} & \bl{$=$} & \bl{false}\\
+ \bl{match (EMPTY::rs) s} & \bl{$=$} & \bl{match rs s}\\
+ \bl{match (CHR c::rs) (c::s)} & \bl{$=$} & \bl{match rs s}\\
+ \bl{match (CHR c::rs) \_} & \bl{$=$} & \bl{false}\\
+ \bl{match (ALT r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s}\\
+ & & \bl{\;\;\;\;orelse match (r$_2$::rs) s}\\
+ \bl{match (SEQ r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s}\\
+ \bl{match (STAR r::rs) s} & \bl{$=$} & \bl{match rs s}\\
+ & & \bl{\;\;\;\;orelse match (r::STAR r::rs) s}\\
+ \end{tabular}
+ \end{center}
+
+ \only<1>{
+ \begin{textblock}{5}(4,4)
+ \largenotok
+ \end{textblock}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[t]
+ \frametitle{Second Attempt}
+
+ Can a regular expression match the empty string?
+
+ \small
+ \begin{center}
+ \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}
+ \bl{nullable (NULL)} & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\
+ \bl{nullable (EMPTY)} & \bl{$=$} & \bl{true} & \onslide<2->{\ok}\\
+ \bl{nullable (CHR c)} & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\
+ \bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) orelse (nullable r$_2$)}
+ & \onslide<2->{\ok}\\
+ \bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) andalso (nullable r$_2$)}
+ & \onslide<2->{\ok}\\
+ \bl{nullable (STAR r)} & \bl{$=$} & \bl{true} & \onslide<2->{\ok}\\
+ \end{tabular}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[t]
+ \frametitle{RegExp Matcher 2}
+
+ If \bl{r} matches \bl{c::s}, which regular expression can match the string \bl{s}?
+
+ \small
+ \begin{center}
+ \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
+ \bl{der c (NULL)} & \bl{$=$} & \bl{NULL} & \onslide<3->{\ok}\\
+ \bl{der c (EMPTY)} & \bl{$=$} & \bl{NULL} & \onslide<3->{\ok}\\
+ \bl{der c (CHR d)} & \bl{$=$} & \bl{if c=d then EMPTY else NULL} & \onslide<3->{\ok}\\
+ \bl{der c (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (der c r$_1$) (der c r$_2$)} & \onslide<3->{\ok}\\
+ \bl{der c (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (SEQ (der c r$_1$) r$_2$)} & \onslide<3->{\ok}\\
+ & & \bl{\phantom{ALT} (if nullable r$_1$ then der c r$_2$ else NULL)}\\
+ \bl{der c (STAR r)} & \bl{$=$} & \bl{SEQ (der c r) (STAR r)} & \onslide<3->{\ok}\medskip\\
+ \pause
+
+ \bl{derivative r []} & \bl{$=$} & \bl{r} & \onslide<3->{\ok}\\
+ \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \onslide<3->{\ok}\\
+ \end{tabular}
+ \end{center}
+
+ we call the program with\\
+ \bl{matches r s $=$ nullable (derivative r s)}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[c]
+ \frametitle{But Now What?}
+
+ \begin{center}
+ {\usefont{T1}{ptm}{b}{N}\VERYHuge{\rd{?}}}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[c]
+ \frametitle{Testing}
+
+ \small
+
+ \begin{center}
+ \begin{tabular}{@ {\hspace{-20mm}}lcl}
+ \bl{matches []$^*$ []} & \bl{$\mapsto$} & \bl{true}\\
+ \bl{matches ([]$|$a)$^*$ a} & \bl{$\mapsto$} & \bl{true}\medskip\\
+
+ \bl{matches (a$\cdot$b)$^*\;$ []} & \bl{$\mapsto$} & \bl{true}\\
+ \bl{matches (a$\cdot$b)$^*\;$ ab} & \bl{$\mapsto$} & \bl{true}\\
+ \bl{matches (a$\cdot$b)$^*\;$ aba} & \bl{$\mapsto$} & \bl{false}\\
+ \bl{matches (a$\cdot$b)$^*\;$ abab} & \bl{$\mapsto$} & \bl{true}\\
+ \bl{matches (a$\cdot$b)$^*\;$ abaa} & \bl{$\mapsto$} & \bl{false}\medskip\\
+
+ \bl{matches x$\cdot$(0$|$1)$^*\;$ x} & \bl{$\mapsto$} & \bl{true}\\
+ \bl{matches x$\cdot$(0$|$1)$^*\;$ x0} & \bl{$\mapsto$} & \bl{true}\\
+ \bl{matches x$\cdot$(0$|$1)$^*\;$ x3} & \bl{$\mapsto$} & \bl{false}
+ \end{tabular}
+ \end{center}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[t]
+ \frametitle{Specification}
+
+ We have to specify what it means for a regular expression to match
+ a string.
+ %
+ \only<2>{
+ \mbox{}\\[8mm]
+ \bl{(a$\cdot$b)$^*$}\\
+ \hspace{7mm}\bl{$\mapsto$\hspace{3mm}\{[], ab, abab, ababab, \ldots\}}\bigskip\\
+ \bl{x$\cdot$(0 $|$ 1 $|$ 2 \ldots 8 $|$ 9 )$^*$}\\
+ \hspace{7mm}\bl{$\mapsto$\hspace{3mm}
+ \{x, x0, x1, \ldots, x00, \ldots, x123, \ldots\}}}
+ %
+ \only<3->{
+ \begin{center}
+ \begin{tabular}{rcl}
+ \bl{\LL (NULL)} & \bl{$\dn$} & \bl{\{\}}\\
+ \bl{\LL (EMPTY)} & \bl{$\dn$} & \bl{\{[]\}}\\
+ \bl{\LL (CHR c)} & \bl{$\dn$} & \bl{\{c\}}\\
+ \bl{\LL (ALT r$_1$ r$_2$)} & \bl{$\dn$} & \onslide<4->{\bl{\LL (r$_1$) $\cup$ \LL (r$_2$)}}\\
+ \bl{\LL (SEQ r$_1$ r$_2$)} & \bl{$\dn$} & \onslide<6->{\bl{\LL (r$_1$) ; \LL (r$_2$)}}\\
+ \bl{\LL (STAR r)} & \bl{$\dn$} & \onslide<8->{\bl{(\LL (r))$^\star$}}\\
+ \end{tabular}
+ \end{center}}
+
+ \only<5-6>{
+ \begin{textblock}{6}(2.9,13.3)
+ \colorbox{cream}{\bl{S$_1$ ; S$_2$ $\;\dn\;$ \{ s$_1$@s$_2$ $|$ s$_1$$\in$S$_1$ $\wedge$
+ s$_2$$\in$S$_2$ \}}}
+ \end{textblock}}
+
+ \only<7->{
+ \begin{textblock}{9}(4,13)
+ \colorbox{cream}{\bl{$\infer{\mbox{[]} \in \mbox{S}^\star}{}$}}\hspace{3mm}
+ \colorbox{cream}{\bl{$\infer{\mbox{s}_1\mbox{@}\mbox{s}_2 \in \mbox{S}^\star}
+ {\mbox{s}_1 \in \mbox{S} & \mbox{s}_2 \in \mbox{S}^\star}$}}
+ \end{textblock}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[t]
+ \frametitle{Is the Matcher Error-Free?}
+
+ We expect that
+
+ \begin{center}
+ \begin{tabular}{lcl}
+ \bl{matches r s = true} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}%
+ \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\in$ \LL(r)}\\
+ \bl{matches r s = false} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}%
+ \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\notin$ \LL(r)}\\
+ \end{tabular}
+ \end{center}
+ \pause\pause\bigskip
+ By \alert<4->{induction}, we can {\bf prove} these properties.\bigskip
+
+ \begin{tabular}{lrcl}
+ Lemmas: & \bl{nullable (r)} & \bl{$\Longleftrightarrow$} & \bl{[] $\in$ \LL (r)}\\
+ & \bl{s $\in$ \LL (der c r)} & \bl{$\Longleftrightarrow$} & \bl{(c::s) $\in$ \LL (r)}\\
+ \end{tabular}
+
+ \only<4->{
+ \begin{textblock}{3}(0.9,4.5)
+ \rd{\huge$\forall$\large{}r s.}
+ \end{textblock}}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[t]
+
+ \mbox{}\\[-2mm]
+
+ \small
+ \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}
+ \bl{nullable (NULL)} & \bl{$=$} & \bl{false} &\\
+ \bl{nullable (EMPTY)} & \bl{$=$} & \bl{true} &\\
+ \bl{nullable (CHR c)} & \bl{$=$} & \bl{false} &\\
+ \bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) orelse (nullable r$_2$)} & \\
+ \bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) andalso (nullable r$_2$)} & \\
+ \bl{nullable (STAR r)} & \bl{$=$} & \bl{true} & \\
+ \end{tabular}\medskip
+
+ \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
+ \bl{der c (NULL)} & \bl{$=$} & \bl{NULL} & \\
+ \bl{der c (EMPTY)} & \bl{$=$} & \bl{NULL} & \\
+ \bl{der c (CHR d)} & \bl{$=$} & \bl{if c=d then EMPTY else NULL} & \\
+ \bl{der c (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (der c r$_1$) (der c r$_2$)} & \\
+ \bl{der c (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (SEQ (der c r$_1$) r$_2$)} & \\
+ & & \bl{\phantom{ALT} (if nullable r$_1$ then der c r$_2$ else NULL)}\\
+ \bl{der c (STAR r)} & \bl{$=$} & \bl{SEQ (der c r) (STAR r)} &\smallskip\\
+
+ \bl{derivative r []} & \bl{$=$} & \bl{r} & \\
+ \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\
+ \end{tabular}\medskip
+
+ \bl{matches r s $=$ nullable (derivative r s)}
+
+ \only<2>{
+ \begin{textblock}{8}(1.5,4)
+ \includegraphics[scale=0.3]{approved.png}
+ \end{textblock}}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[c]
+ \frametitle{Interlude: TCB}
+
+ \begin{itemize}
+ \item The \alert{\bf Trusted Code Base} (TCB) is the code that can make your
+ program behave in unintended ways (i.e.~cause bugs).\medskip
+
+ \item Typically the TCB includes: CPUs, operating systems, C-libraries,
+ device drivers, (J)VMs\ldots\bigskip
+ \pause
+
+ \item It also includes the compiler.
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1-3>
+ \frametitle{\LARGE\begin{tabular}{c}Hacking Compilers
+ \end{tabular}}
+
+ %Why is it so paramount to have a small trusted code base (TCB)?
+ \bigskip\bigskip
+
+ \begin{columns}
+ \begin{column}{2.7cm}
+ \begin{minipage}{2.5cm}%
+ \begin{tabular}{c@ {}}
+ \includegraphics[scale=0.2]{ken-thompson.jpg}\\[-1.8mm]
+ \footnotesize Ken Thompson\\[-1.8mm]
+ \footnotesize Turing Award, 1983\\
+ \end{tabular}
+ \end{minipage}
+ \end{column}
+ \begin{column}{9cm}
+ \begin{tabular}{l@ {\hspace{1mm}}p{8cm}}
+ \myitemi
+ & Ken Thompson showed how to hide a Trojan Horse in a
+ compiler \textcolor{red}{without} leaving any traces in the source code.\\[2mm]
+ \myitemi
+ & No amount of source level verification will protect
+ you from such Thompson-hacks.\\[2mm]
+
+ \myitemi
+ & Therefore in safety-critical systems it is important to rely
+ on only a very small TCB.
+ \end{tabular}
+ \end{column}
+ \end{columns}
+
+ \only<2>{
+ \begin{textblock}{6}(4,2)
+ \begin{tikzpicture}
+ \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ {\normalsize
+ \begin{minipage}{8cm}
+ \begin{quote}
+ \includegraphics[scale=0.05]{evil.png}
+ \begin{enumerate}
+ \item[1)] Assume you ship the compiler as binary and also with sources.
+ \item[2)] Make the compiler aware when it compiles itself.
+ \item[3)] Add the Trojan horse.
+ \item[4)] Compile.
+ \item[5)] Delete Trojan horse from the sources of the compiler.
+ \item[6)] Go on holiday for the rest of your life. ;o)\\[-7mm]\mbox{}
+ \end{enumerate}
+ \end{quote}
+ \end{minipage}};
+ \end{tikzpicture}
+ \end{textblock}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}
+ \frametitle{\LARGE\begin{tabular}{c}An Example: Small TCB for\\[-2mm]
+ A Critical Infrastructure\end{tabular}}
+ \mbox{}\\[-14mm]\mbox{}
+
+ \begin{columns}
+ \begin{column}{0.2\textwidth}
+ \begin{tabular}{@ {} c@ {}}
+ \includegraphics[scale=0.3]{appel.jpg}\\[-2mm]
+ {\footnotesize Andrew Appel}\\[-2.5mm]
+ {\footnotesize (Princeton)}
+ \end{tabular}
+ \end{column}
+
+ \begin{column}{0.8\textwidth}
+ \begin{textblock}{10}(4.5,3.95)
+ \begin{block}{Proof-Carrying Code}
+ \begin{center}
+ \begin{tikzpicture}
+ \draw[help lines,cream] (0,0.2) grid (8,4);
+
+ \draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4);
+ \node[anchor=base] at (6.5,2.8)
+ {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering user needs to run untrusted code\end{tabular}};
+
+ \draw[line width=1mm, red] (0.5,0.6) rectangle (2.5,4);
+ \node[anchor=base] at (1.5,2.3)
+ {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering code developer/ web server/ Apple
+ Store\end{tabular}};
+
+ \onslide<4->{
+ \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8);
+ \node[anchor=base,white] at (6.5,1.1)
+ {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};}
+
+ \node at (3.8,3.0) [single arrow, fill=red,text=white, minimum height=3cm]{\bf code};
+ \onslide<3->{
+ \node at (3.8,1.3) [single arrow, fill=red,text=white, minimum height=3cm]{\bf LF proof};
+ \node at (3.8,1.9) {\small certificate};
+ }
+
+ \onslide<2>{\node at (4.0,1.3) [text=red]{\begin{tabular}{c}\bf Highly\\\bf Dangerous!\end{tabular}};}
+ % Code Developer
+ % User (runs untrusted code)
+ % transmits a proof that the code is safe
+ %
+ \end{tikzpicture}
+ \end{center}
+ \end{block}
+ \end{textblock}
+ \end{column}
+ \end{columns}
+
+ \small\mbox{}\\[2.5cm]
+ \begin{itemize}
+ \item<4-> TCB of the checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions;
+ 803 loc in C including 2 library functions)\\[-3mm]
+ \item<5-> 167 loc in C implement a type-checker
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+
+
+text {*
+ \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
+ \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick,
+ draw=black!50, top color=white, bottom color=black!20]
+ \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick,
+ draw=red!70, top color=white, bottom color=red!50!black!20]
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[squeeze]
+ \frametitle{Type-Checking in LF}
+
+ \begin{columns}
+ \begin{column}{0.2\textwidth}
+ \begin{tabular}{@ {\hspace{-4mm}}c@ {}}
+ \\[-4mm]
+ \includegraphics[scale=0.1]{harper.jpg}\\[-2mm]
+ {\footnotesize Bob Harper}\\[-2.5mm]
+ {\footnotesize (CMU)}\\[2mm]
+
+ \includegraphics[scale=0.3]{pfenning.jpg}\\[-2mm]
+ {\footnotesize Frank Pfenning}\\[-2.5mm]
+ {\footnotesize (CMU)}\\[2mm]
+
+ \onslide<-6>{
+ {\footnotesize 31 pages in }\\[-2.5mm]
+ {\footnotesize ACM Transact.~on}\\[-2.5mm]
+ {\footnotesize Comp.~Logic.,~2005}\\}
+ \end{tabular}
+ \end{column}
+
+ \begin{column}{0.8\textwidth}
+ \begin{textblock}{0}(3.1,2)
+
+ \begin{tikzpicture}
+ \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]
+ { \&[-10mm]
+ \node (def1) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&
+ \node (proof1) [node1] {\large Proof}; \&
+ \node (alg1) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\
+
+ \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+ \onslide<4->{\node (def2) [node2] {\large Spec$^\text{+ex}$};} \&
+ \onslide<4->{\node (proof2) [node1] {\large Proof};} \&
+ \onslide<4->{\node (alg2) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+
+ \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+ \onslide<5->{\node (def3) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
+ \onslide<5->{\node (proof3) [node1] {\large Proof};} \&
+ \onslide<5->{\node (alg3) [node2] {\large Alg$^\text{-ex}$};} \\
+
+ \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+ \onslide<6->{\node (def4) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
+ \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&
+ \onslide<6->{\node (alg4) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+ };
+
+ \draw[->,black!50,line width=2mm] (proof1) -- (def1);
+ \draw[->,black!50,line width=2mm] (proof1) -- (alg1);
+
+ \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}
+ \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}
+
+ \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}
+ \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}
+
+ \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}
+ \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}
+
+ \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);}
+ \end{tikzpicture}
+
+ \end{textblock}
+ \end{column}
+ \end{columns}
+
+ \only<2>{%
+ \begin{textblock}{2}(.1,12.85)
+ \begin{tikzpicture}
+ \draw[line width=1mm, red] (0,0) ellipse (1.5cm and 0.88cm);
+ \end{tikzpicture}
+ \end{textblock}
+ }
+
+ \begin{textblock}{3}(14,3.6)
+ \onslide<4->{
+ \begin{tikzpicture}
+ \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
+ \end{tikzpicture}}
+ \end{textblock}
+
+ \only<7->{
+ \begin{textblock}{14}(0.6,12.8)
+ \begin{block}{}
+ \small Each time one needs to check $\sim$31pp~of informal paper proofs.
+ You have to be able to keep definitions and proofs consistent.
+ \end{block}
+ \end{textblock}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>[c]
+ \frametitle{Theorem Provers}
+
+ \begin{itemize}
+ \item Theorem provers help with keeping large proofs consistent;
+ make them modifiable.\medskip
+
+ \item They can ensure that all cases are covered.\medskip
+
+ \item Sometimes, tedious reasoning can be automated.
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>[c]
+ \frametitle{Theorem Provers}
+
+ \begin{itemize}
+ \item You also pay a (sometimes heavy) price: reasoning can be much, much harder.\medskip
+
+ \item Depending on your domain, suitable reasoning infrastructure
+ might not yet be available.
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>[c]
+ \frametitle{Theorem Provers}
+
+ Recently impressive work has been accomplished proving the correctness
+
+ \begin{itemize}
+ \item of a compiler for C-light (compiled code has the same observable
+ behaviour as the original source code),\medskip
+
+ \item a mirco-kernel operating system (absence of certain
+ bugs\ldots no nil pointers, no buffer overflows).
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>[c]
+ \frametitle{Trust in Theorem Provers}
+
+ \begin{center}
+ Why should we trust theorem provers?
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}
+ \frametitle{Theorem Provers}
+
+ \begin{itemize}
+ \item Theorem provers are a \textcolor{red}{special kind} of software.
+
+ \item We do \textcolor{red}{\bf not} need to trust them; we only need to trust:
+ \end{itemize}
+
+ \begin{quote}
+ \begin{itemize}
+ \item The logic they are based on \textcolor{gray}{(e.g.~HOL)}, and\smallskip
+ \item a proof checker that checks the proofs
+ \textcolor{gray}{(this can be a very small program)}.\smallskip\pause
+ \item To a little extend, we also need to trust our definitions
+ \textcolor{gray}{(this can be mitigated)}.
+ \end{itemize}
+ \end{quote}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}
+ \frametitle{Isabelle}
+
+ \begin{itemize}
+ \item I am using the Isabelle theorem prover (development since 1990).\bigskip\bigskip\bigskip
+
+ \item It follows the LCF-approach:
+
+ \begin{itemize}
+ \item Have a special abstract type \alert{\bf thm}.
+ \item Make the constructors of this abstract type the inference rules
+ of your logic.
+ \item Implement the theorem prover in a strongly-typed language (e.g.~ML).
+ \end{itemize}
+
+ $\Rightarrow$ everything of type {\bf thm} has been proved (even if we do not
+ have to explicitly generate proofs).
+ \end{itemize}
+
+ \only<1>{
+ \begin{textblock}{5}(11,2.3)
+ \begin{center}
+ \includegraphics[scale=0.18]{robin-milner.jpg}\\[-0.8mm]
+ \footnotesize Robin Milner\\[-0.8mm]
+ \footnotesize Turing Award, 1991\\
+ \end{center}
+ \end{textblock}}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>[c]
+ \frametitle{
+ \begin{tabular}{c}
+ \mbox{}\\[23mm]
+ \LARGE Demo
+ \end{tabular}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[c]
+ \frametitle{Future Research}
+
+ \begin{itemize}
+ \item Make theorem provers more like a programming environment.\medskip\pause
+
+ \item Use all the computational power we get from the hardware to
+ automate reasoning (GPUs).\medskip\pause
+
+ \item Provide a comprehensive reasoning infrastructure for many domains and
+ design automated decision procedures.
+ \end{itemize}\pause
+
+
+ \begin{center}
+ \colorbox{cream}{
+ \begin{minipage}{10cm}
+ \color{gray}
+ \small
+ ``Formal methods will never have a significant impact until
+ they can be used by people that don't understand them.''\smallskip\\
+ \mbox{}\footnotesize\hfill attributed to Tom Melham
+ \end{minipage}}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1->[c]
+ \frametitle{Conclusion}
+
+ \begin{itemize}
+ \item The plan is to make this kind of programming the ``future''.\medskip\pause
+
+ \item Though the technology is already there\\ (compiler + micro-kernel os).\medskip\pause
+
+ \item Logic and reasoning (especially induction) are important skills for
+ Computer Scientists.
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1>[c]
+ \frametitle{
+ \begin{tabular}{c}
+ \mbox{}\\[23mm]
+ \alert{\LARGE Thank you very much!}\\
+ \alert{\Large Questions?}
+ \end{tabular}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+
+(*<*)
+end
+(*>*)
\ No newline at end of file