--- a/Quot/Examples/LamEx.thy Fri Jan 01 11:30:00 2010 +0100
+++ b/Quot/Examples/LamEx.thy Fri Jan 01 23:59:32 2010 +0100
@@ -4,33 +4,44 @@
atom_decl name
-thm abs_fresh(1)
-
-nominal_datatype rlam =
+datatype rlam =
rVar "name"
| rApp "rlam" "rlam"
| rLam "name" "rlam"
-print_theorems
-
-function
+fun
rfv :: "rlam \<Rightarrow> name set"
where
rfv_var: "rfv (rVar a) = {a}"
| rfv_app: "rfv (rApp t1 t2) = (rfv t1) \<union> (rfv t2)"
| rfv_lam: "rfv (rLam a t) = (rfv t) - {a}"
-sorry
+
+overloading
+ perm_rlam \<equiv> "perm :: 'x prm \<Rightarrow> rlam \<Rightarrow> rlam" (unchecked)
+begin
-termination rfv sorry
+fun
+ perm_rlam
+where
+ "perm_rlam pi (rVar a) = rVar (pi \<bullet> a)"
+| "perm_rlam pi (rApp t1 t2) = rApp (perm_rlam pi t1) (perm_rlam pi t2)"
+| "perm_rlam pi (rLam a t) = rLam (pi \<bullet> a) (perm_rlam pi t)"
+
+end
inductive
alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
where
a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
| a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
-| a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a \<notin> rfv (rLam b t)\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
+| a3: "\<lbrakk>t \<approx> ([(a,b)] \<bullet> s); a \<notin> rfv (rLam b t)\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
-print_theorems
+lemma helper:
+ fixes t::"rlam"
+ and a::"name"
+ shows "[(a, a)] \<bullet> t = t"
+by (induct t)
+ (auto simp add: calc_atm)
lemma alpha_refl:
fixes t::"rlam"
@@ -39,10 +50,7 @@
apply(simp add: a1)
apply(simp add: a2)
apply(rule a3)
- apply(subst pt_swap_bij'')
- apply(rule pt_name_inst)
- apply(rule at_name_inst)
- apply(simp)
+ apply(simp add: helper)
apply(simp)
done
@@ -51,10 +59,8 @@
sorry
quotient_type lam = rlam / alpha
- apply(rule alpha_equivp)
- done
+ by (rule alpha_equivp)
-print_quotients
quotient_definition
"Var :: name \<Rightarrow> lam"
@@ -71,15 +77,14 @@
as
"rLam"
-thm Var_def
-thm App_def
-thm Lam_def
-
quotient_definition
"fv :: lam \<Rightarrow> name set"
as
"rfv"
+thm Var_def
+thm App_def
+thm Lam_def
thm fv_def
(* definition of overloaded permutation function *)
@@ -97,22 +102,36 @@
thm perm_lam_def
-(* lemmas that need to lift *)
-lemma pi_var_com:
+(* lemmas that need to be lifted *)
+lemma pi_var_eqvt1:
fixes pi::"'x prm"
- shows "(pi\<bullet>rVar a) \<approx> rVar (pi\<bullet>a)"
- sorry
+ shows "(pi \<bullet> rVar a) \<approx> rVar (pi \<bullet> a)"
+ by (simp add: alpha_refl)
-lemma pi_app_com:
+lemma pi_var_eqvt2:
+ fixes pi::"'x prm"
+ shows "(pi \<bullet> rVar a) = rVar (pi \<bullet> a)"
+ by (simp)
+
+lemma pi_app_eqvt1:
fixes pi::"'x prm"
- shows "(pi\<bullet>rApp t1 t2) \<approx> rApp (pi\<bullet>t1) (pi\<bullet>t2)"
- sorry
+ shows "(pi \<bullet> rApp t1 t2) \<approx> rApp (pi \<bullet> t1) (pi \<bullet> t2)"
+ by (simp add: alpha_refl)
+
+lemma pi_app_eqvt2:
+ fixes pi::"'x prm"
+ shows "(pi \<bullet> rApp t1 t2) = rApp (pi \<bullet> t1) (pi \<bullet> t2)"
+ by (simp)
-lemma pi_lam_com:
+lemma pi_lam_eqvt1:
fixes pi::"'x prm"
- shows "(pi\<bullet>rLam a t) \<approx> rLam (pi\<bullet>a) (pi\<bullet>t)"
- sorry
+ shows "(pi \<bullet> rLam a t) \<approx> rLam (pi \<bullet> a) (pi \<bullet> t)"
+ by (simp add: alpha_refl)
+lemma pi_lam_eqvt2:
+ fixes pi::"'x prm"
+ shows "(pi \<bullet> rLam a t) = rLam (pi \<bullet> a) (pi \<bullet> t)"
+ by (simp add: alpha)
lemma real_alpha:
@@ -136,25 +155,20 @@
lemma rVar_rsp[quot_respect]:
"(op = ===> alpha) rVar rVar"
-by (auto intro:a1)
+by (auto intro: a1)
lemma rApp_rsp[quot_respect]: "(alpha ===> alpha ===> alpha) rApp rApp"
-by (auto intro:a2)
+by (auto intro: a2)
lemma rLam_rsp[quot_respect]: "(op = ===> alpha ===> alpha) rLam rLam"
apply(auto)
apply(rule a3)
- apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst)
- apply(rule sym)
- apply(rule trans)
- apply(rule pt_name3)
- apply(rule at_ds1[OF at_name_inst])
- apply(simp add: pt_name1)
- apply(assumption)
- apply(simp add: abs_fresh)
+ apply(simp add: helper)
+ apply(simp)
done
-lemma rfv_rsp[quot_respect]: "(alpha ===> op =) rfv rfv"
+lemma rfv_rsp[quot_respect]:
+ "(alpha ===> op =) rfv rfv"
sorry
lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"
@@ -164,76 +178,86 @@
done
-lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
-apply (lifting pi_var_com)
-done
+lemma pi_var1:
+ fixes pi::"'x prm"
+ shows "pi \<bullet> Var a = Var (pi \<bullet> a)"
+ by (lifting pi_var_eqvt1)
-lemma pi_app: "(pi\<Colon>('x \<times> 'x) list) \<bullet> App (x\<Colon>lam) (xa\<Colon>lam) = App (pi \<bullet> x) (pi \<bullet> xa)"
-apply (lifting pi_app_com)
-done
+lemma pi_var2:
+ fixes pi::"'x prm"
+ shows "pi \<bullet> Var a = Var (pi \<bullet> a)"
+ by (lifting pi_var_eqvt2)
+
-lemma pi_lam: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Lam (a\<Colon>name) (x\<Colon>lam) = Lam (pi \<bullet> a) (pi \<bullet> x)"
-apply (lifting pi_lam_com)
-done
+lemma pi_app:
+ fixes pi::"'x prm"
+ shows "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)"
+ by (lifting pi_app_eqvt2)
-lemma fv_var: "fv (Var (a\<Colon>name)) = {a}"
-apply (lifting rfv_var)
-done
+lemma pi_lam:
+ fixes pi::"'x prm"
+ shows "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)"
+ by (lifting pi_lam_eqvt2)
-lemma fv_app: "fv (App (x\<Colon>lam) (xa\<Colon>lam)) = fv x \<union> fv xa"
-apply (lifting rfv_app)
-done
+lemma fv_var:
+ shows "fv (Var a) = {a}"
+ by (lifting rfv_var)
-lemma fv_lam: "fv (Lam (a\<Colon>name) (x\<Colon>lam)) = fv x - {a}"
-apply (lifting rfv_lam)
-done
+lemma fv_app:
+ shows "fv (App t1 t2) = fv t1 \<union> fv t2"
+ by (lifting rfv_app)
+
+lemma fv_lam:
+ shows "fv (Lam a t) = fv t - {a}"
+ by (lifting rfv_lam)
-lemma a1: "(a\<Colon>name) = (b\<Colon>name) \<Longrightarrow> Var a = Var b"
-apply (lifting a1)
-done
+lemma a1:
+ "a = b \<Longrightarrow> Var a = Var b"
+ by (lifting a1)
-lemma a2: "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); (xb\<Colon>lam) = (xc\<Colon>lam)\<rbrakk> \<Longrightarrow> App x xb = App xa xc"
-apply (lifting a2)
-done
+lemma a2:
+ "\<lbrakk>x = xa; xb = xc\<rbrakk> \<Longrightarrow> App x xb = App xa xc"
+ by (lifting a2)
-lemma a3: "\<lbrakk>(x\<Colon>lam) = [(a\<Colon>name, b\<Colon>name)] \<bullet> (xa\<Colon>lam); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> Lam a x = Lam b xa"
-apply (lifting a3)
-done
+lemma a3:
+ "\<lbrakk>x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> Lam a x = Lam b xa"
+ by (lifting a3)
-lemma alpha_cases: "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;
- \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
- \<And>x a b xa. \<lbrakk>a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk>
+lemma alpha_cases:
+ "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;
+ \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
+ \<And>x a b xa. \<lbrakk>a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk>
\<Longrightarrow> P"
-apply (lifting alpha.cases)
-done
+ by (lifting alpha.cases)
-lemma alpha_induct: "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b);
- \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
- \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam.
+lemma alpha_induct:
+ "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b);
+ \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
+ \<And>x a b xa.
\<lbrakk>x = [(a, b)] \<bullet> xa; qxb x ([(a, b)] \<bullet> xa); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> qxb (Lam a x) (Lam b xa)\<rbrakk>
\<Longrightarrow> qxb qx qxa"
-apply (lifting alpha.induct)
-done
+ by (lifting alpha.induct)
+
+lemma var_inject:
+ "(Var a = Var b) = (a = b)"
+ by (lifting rvar_inject)
-lemma var_inject: "(Var a = Var b) = (a = b)"
-apply (lifting rvar_inject)
-done
-
-lemma lam_induct:" \<lbrakk>\<And>name. P (Var name); \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
- \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> \<Longrightarrow> P lam"
-apply (lifting rlam.induct)
-done
+lemma lam_induct:
+ "\<lbrakk>\<And>name. P (Var name);
+ \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
+ \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> \<Longrightarrow> P lam"
+ by (lifting rlam.induct)
lemma var_supp:
shows "supp (Var a) = ((supp a)::name set)"
apply(simp add: supp_def)
- apply(simp add: pi_var)
+ apply(simp add: pi_var2)
apply(simp add: var_inject)
done
lemma var_fresh:
fixes a::"name"
- shows "(a\<sharp>(Var b)) = (a\<sharp>b)"
+ shows "(a \<sharp> (Var b)) = (a \<sharp> b)"
apply(simp add: fresh_def)
apply(simp add: var_supp)
done
--- a/Quot/Examples/LarryDatatype.thy Fri Jan 01 11:30:00 2010 +0100
+++ b/Quot/Examples/LarryDatatype.thy Fri Jan 01 23:59:32 2010 +0100
@@ -51,7 +51,7 @@
theorem msgrel_imp_eq_freenonces:
assumes a: "U \<sim> V"
shows "freenonces U = freenonces V"
-using a by (induct) (auto)
+ using a by (induct) (auto)
subsubsection{*The Left Projection*}
@@ -70,13 +70,13 @@
(the abstract constructor) is injective*}
lemma msgrel_imp_eqv_freeleft_aux:
shows "freeleft U \<sim> freeleft U"
-by (induct rule: freeleft.induct) (auto)
+ by (induct rule: freeleft.induct) (auto)
theorem msgrel_imp_eqv_freeleft:
assumes a: "U \<sim> V"
shows "freeleft U \<sim> freeleft V"
-using a
-by (induct)(auto intro: msgrel_imp_eqv_freeleft_aux)
+ using a
+ by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux)
subsubsection{*The Right Projection*}
@@ -94,13 +94,13 @@
(the abstract constructor) is injective*}
lemma msgrel_imp_eqv_freeright_aux:
shows "freeright U \<sim> freeright U"
-by (induct rule: freeright.induct) (auto)
+ by (induct rule: freeright.induct) (auto)
theorem msgrel_imp_eqv_freeright:
assumes a: "U \<sim> V"
shows "freeright U \<sim> freeright V"
-using a
-by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)
+ using a
+ by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)
subsubsection{*The Discriminator for Constructors*}
@@ -117,7 +117,7 @@
theorem msgrel_imp_eq_freediscrim:
assumes a: "U \<sim> V"
shows "freediscrim U = freediscrim V"
-using a by (induct, auto)
+ using a by (induct) (auto)
subsection{*The Initial Algebra: A Quotiented Message Type*}
@@ -155,11 +155,13 @@
by (auto intro: DECRYPT)
text{*Establishing these two equations is the point of the whole exercise*}
-theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X"
-by (lifting CD)
+theorem CD_eq [simp]:
+ shows "Crypt K (Decrypt K X) = X"
+ by (lifting CD)
-theorem DC_eq [simp]: "Decrypt K (Crypt K X) = X"
-by (lifting DC)
+theorem DC_eq [simp]:
+ shows "Decrypt K (Crypt K X) = X"
+ by (lifting DC)
subsection{*The Abstract Function to Return the Set of Nonces*}
@@ -172,30 +174,31 @@
lemma [quot_respect]:
shows "(op \<sim> ===> op =) freenonces freenonces"
-by (simp add: msgrel_imp_eq_freenonces)
+ by (simp add: msgrel_imp_eq_freenonces)
lemma [quot_respect]:
shows "(op = ===> op \<sim>) NONCE NONCE"
-by (simp add: NONCE)
+ by (simp add: NONCE)
lemma nonces_Nonce [simp]:
shows "nonces (Nonce N) = {N}"
-by (lifting freenonces.simps(1))
+ by (lifting freenonces.simps(1))
lemma [quot_respect]:
shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
-by (simp add: MPAIR)
+ by (simp add: MPAIR)
lemma nonces_MPair [simp]:
shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
-by (lifting freenonces.simps(2))
+ by (lifting freenonces.simps(2))
lemma nonces_Crypt [simp]:
shows "nonces (Crypt K X) = nonces X"
-by (lifting freenonces.simps(3))
+ by (lifting freenonces.simps(3))
-lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X"
-by (lifting freenonces.simps(4))
+lemma nonces_Decrypt [simp]:
+ shows "nonces (Decrypt K X) = nonces X"
+ by (lifting freenonces.simps(4))
subsection{*The Abstract Function to Return the Left Part*}
@@ -206,23 +209,23 @@
lemma [quot_respect]:
shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
-by (simp add: msgrel_imp_eqv_freeleft)
+ by (simp add: msgrel_imp_eqv_freeleft)
lemma left_Nonce [simp]:
shows "left (Nonce N) = Nonce N"
-by (lifting freeleft.simps(1))
+ by (lifting freeleft.simps(1))
lemma left_MPair [simp]:
shows "left (MPair X Y) = X"
-by (lifting freeleft.simps(2))
+ by (lifting freeleft.simps(2))
lemma left_Crypt [simp]:
shows "left (Crypt K X) = left X"
-by (lifting freeleft.simps(3))
+ by (lifting freeleft.simps(3))
lemma left_Decrypt [simp]:
shows "left (Decrypt K X) = left X"
-by (lifting freeleft.simps(4))
+ by (lifting freeleft.simps(4))
subsection{*The Abstract Function to Return the Right Part*}
@@ -235,29 +238,29 @@
lemma [quot_respect]:
shows "(op \<sim> ===> op \<sim>) freeright freeright"
-by (simp add: msgrel_imp_eqv_freeright)
+ by (simp add: msgrel_imp_eqv_freeright)
lemma right_Nonce [simp]:
shows "right (Nonce N) = Nonce N"
-by (lifting freeright.simps(1))
+ by (lifting freeright.simps(1))
lemma right_MPair [simp]:
shows "right (MPair X Y) = Y"
-by (lifting freeright.simps(2))
+ by (lifting freeright.simps(2))
lemma right_Crypt [simp]:
shows "right (Crypt K X) = right X"
-by (lifting freeright.simps(3))
+ by (lifting freeright.simps(3))
lemma right_Decrypt [simp]:
shows "right (Decrypt K X) = right X"
-by (lifting freeright.simps(4))
+ by (lifting freeright.simps(4))
subsection{*Injectivity Properties of Some Constructors*}
lemma NONCE_imp_eq:
shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
-by (drule msgrel_imp_eq_freenonces, simp)
+ by (drule msgrel_imp_eq_freenonces, simp)
text{*Can also be proved using the function @{term nonces}*}
lemma Nonce_Nonce_eq [iff]:
@@ -272,51 +275,51 @@
lemma MPAIR_imp_eqv_left:
shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
-by (drule msgrel_imp_eqv_freeleft) (simp)
+ by (drule msgrel_imp_eqv_freeleft) (simp)
lemma MPair_imp_eq_left:
assumes eq: "MPair X Y = MPair X' Y'"
shows "X = X'"
-using eq by (lifting MPAIR_imp_eqv_left)
+ using eq by (lifting MPAIR_imp_eqv_left)
lemma MPAIR_imp_eqv_right:
shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
-by (drule msgrel_imp_eqv_freeright) (simp)
+ by (drule msgrel_imp_eqv_freeright) (simp)
lemma MPair_imp_eq_right:
shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
-by (lifting MPAIR_imp_eqv_right)
+ by (lifting MPAIR_imp_eqv_right)
theorem MPair_MPair_eq [iff]:
shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
-by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
+ by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
lemma NONCE_neqv_MPAIR:
shows "\<not>(NONCE m \<sim> MPAIR X Y)"
-by (auto dest: msgrel_imp_eq_freediscrim)
+ by (auto dest: msgrel_imp_eq_freediscrim)
theorem Nonce_neq_MPair [iff]:
shows "Nonce N \<noteq> MPair X Y"
-by (lifting NONCE_neqv_MPAIR)
+ by (lifting NONCE_neqv_MPAIR)
text{*Example suggested by a referee*}
lemma CRYPT_NONCE_neq_NONCE:
shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
-by (auto dest: msgrel_imp_eq_freediscrim)
+ by (auto dest: msgrel_imp_eq_freediscrim)
theorem Crypt_Nonce_neq_Nonce:
shows "Crypt K (Nonce M) \<noteq> Nonce N"
-by (lifting CRYPT_NONCE_neq_NONCE)
+ by (lifting CRYPT_NONCE_neq_NONCE)
text{*...and many similar results*}
lemma CRYPT2_NONCE_neq_NONCE:
shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
-by (auto dest: msgrel_imp_eq_freediscrim)
+ by (auto dest: msgrel_imp_eq_freediscrim)
theorem Crypt2_Nonce_neq_Nonce:
shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
-by (lifting CRYPT2_NONCE_neq_NONCE)
+ by (lifting CRYPT2_NONCE_neq_NONCE)
theorem Crypt_Crypt_eq [iff]:
shows "(Crypt K X = Crypt K X') = (X=X')"
@@ -345,7 +348,7 @@
\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
\<And>K X. P X \<Longrightarrow> P (Crypt K X);
\<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
-by (lifting freemsg.induct)
+ by (lifting freemsg.induct)
lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
assumes N: "\<And>N. P (Nonce N)"
@@ -353,7 +356,7 @@
and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
shows "P msg"
-using N M C D by (rule msg_induct_aux)
+ using N M C D by (rule msg_induct_aux)
subsection{*The Abstract Discriminator*}
@@ -369,23 +372,23 @@
lemma [quot_respect]:
shows "(op \<sim> ===> op =) freediscrim freediscrim"
-by (auto simp add: msgrel_imp_eq_freediscrim)
+ by (auto simp add: msgrel_imp_eq_freediscrim)
lemma discrim_Nonce [simp]:
shows "discrim (Nonce N) = 0"
-by (lifting freediscrim.simps(1))
+ by (lifting freediscrim.simps(1))
lemma discrim_MPair [simp]:
shows "discrim (MPair X Y) = 1"
-by (lifting freediscrim.simps(2))
+ by (lifting freediscrim.simps(2))
lemma discrim_Crypt [simp]:
shows "discrim (Crypt K X) = discrim X + 2"
-by (lifting freediscrim.simps(3))
+ by (lifting freediscrim.simps(3))
lemma discrim_Decrypt [simp]:
shows "discrim (Decrypt K X) = discrim X - 2"
-by (lifting freediscrim.simps(4))
+ by (lifting freediscrim.simps(4))
end
--- a/Quot/Examples/LarryInt.thy Fri Jan 01 11:30:00 2010 +0100
+++ b/Quot/Examples/LarryInt.thy Fri Jan 01 23:59:32 2010 +0100
@@ -76,18 +76,18 @@
shows "(intrel ===> intrel) uminus_raw uminus_raw"
by (simp add: uminus_raw_def)
-lemma zminus_zminus:
- shows "- (- z) = (z::int)"
-apply(lifting zminus_zminus_raw)
-done
+lemma zminus_zminus:
+ fixes z::"int"
+ shows "- (- z) = z"
+ by(lifting zminus_zminus_raw)
lemma zminus_0_raw:
shows "uminus_raw (0, 0) = (0, 0::nat)"
-by (simp add: uminus_raw_def)
+ by (simp add: uminus_raw_def)
-lemma zminus_0: "- 0 = (0::int)"
-apply(lifting zminus_0_raw)
-done
+lemma zminus_0:
+ shows "- 0 = (0::int)"
+ by (lifting zminus_0_raw)
subsection{*Integer Addition*}
@@ -101,9 +101,9 @@
by (simp add: add_raw_def)
lemma zminus_zadd_distrib:
- shows "- (z + w) = (- z) + (- w::int)"
-apply(lifting zminus_zadd_distrib_raw)
-done
+ fixes z w::"int"
+ shows "- (z + w) = (- z) + (- w)"
+ by(lifting zminus_zadd_distrib_raw)
lemma zadd_commute_raw:
shows "add_raw z w = add_raw w z"
@@ -111,43 +111,45 @@
(simp add: add_raw_def)
lemma zadd_commute:
+ fixes z w::"int"
shows "(z::int) + w = w + z"
-apply(lifting zadd_commute_raw)
-done
+ by (lifting zadd_commute_raw)
lemma zadd_assoc_raw:
shows "add_raw (add_raw z1 z2) z3 = add_raw z1 (add_raw z2 z3)"
-by (cases z1, cases z2, cases z3) (simp add: add_raw_def)
+ by (cases z1, cases z2, cases z3) (simp add: add_raw_def)
-lemma zadd_assoc: "((z1::int) + z2) + z3 = z1 + (z2 + z3)"
-apply(lifting zadd_assoc_raw)
-done
+lemma zadd_assoc:
+ fixes z1 z2 z3::"int"
+ shows "(z1 + z2) + z3 = z1 + (z2 + z3)"
+ by (lifting zadd_assoc_raw)
lemma zadd_0_raw:
- fixes z::"nat \<times> nat"
shows "add_raw (0, 0) z = z"
-by (simp add: add_raw_def)
+ by (simp add: add_raw_def)
-(*also for the instance declaration int :: plus_ac0*)
-lemma zadd_0: "(0::int) + z = z"
-apply(lifting zadd_0_raw)
-done
+text {*also for the instance declaration int :: plus_ac0*}
+lemma zadd_0:
+ fixes z::"int"
+ shows "0 + z = z"
+ by (lifting zadd_0_raw)
lemma zadd_zminus_inverse_raw:
shows "intrel (add_raw (uminus_raw z) z) (0, 0)"
-by (cases z) (simp add: add_raw_def uminus_raw_def)
+ by (cases z) (simp add: add_raw_def uminus_raw_def)
-lemma zadd_zminus_inverse2: "(- z) + z = (0::int)"
-apply(lifting zadd_zminus_inverse_raw)
-done
+lemma zadd_zminus_inverse2:
+ fixes z::"int"
+ shows "(- z) + z = 0"
+ by (lifting zadd_zminus_inverse_raw)
subsection{*Integer Multiplication*}
lemma zmult_zminus_raw:
shows "mult_raw (uminus_raw z) w = uminus_raw (mult_raw z w)"
apply(cases z, cases w)
-apply(simp add:uminus_raw_def)
+apply(simp add: uminus_raw_def)
done
lemma mult_raw_fst:
@@ -185,9 +187,10 @@
apply(assumption)
done
-lemma zmult_zminus: "(- z) * w = - (z * (w::int))"
-apply(lifting zmult_zminus_raw)
-done
+lemma zmult_zminus:
+ fixes z w::"int"
+ shows "(- z) * w = - (z * w)"
+ by (lifting zmult_zminus_raw)
lemma zmult_commute_raw:
shows "mult_raw z w = mult_raw w z"
@@ -195,8 +198,10 @@
apply(simp add: add_ac mult_ac)
done
-lemma zmult_commute: "(z::int) * w = w * z"
-by (lifting zmult_commute_raw)
+lemma zmult_commute:
+ fixes z w::"int"
+ shows "z * w = w * z"
+ by (lifting zmult_commute_raw)
lemma zmult_assoc_raw:
shows "mult_raw (mult_raw z1 z2) z3 = mult_raw z1 (mult_raw z2 z3)"
@@ -204,8 +209,10 @@
apply(simp add: add_mult_distrib2 mult_ac)
done
-lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)"
-by (lifting zmult_assoc_raw)
+lemma zmult_assoc:
+ fixes z1 z2 z3::"int"
+ shows "(z1 * z2) * z3 = z1 * (z2 * z3)"
+ by (lifting zmult_assoc_raw)
lemma zadd_mult_distrib_raw:
shows "mult_raw (add_raw z1 z2) w = add_raw (mult_raw z1 w) (mult_raw z2 w)"
@@ -213,18 +220,25 @@
apply(simp add: add_mult_distrib2 mult_ac add_raw_def)
done
-lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"
-apply(lifting zadd_mult_distrib_raw)
-done
+lemma zadd_zmult_distrib:
+ fixes z1 z2 w::"int"
+ shows "(z1 + z2) * w = (z1 * w) + (z2 * w)"
+ by(lifting zadd_mult_distrib_raw)
+
+lemma zadd_zmult_distrib2:
+ fixes w z1 z2::"int"
+ shows "w * (z1 + z2) = (w * z1) + (w * z2)"
+ by (simp add: zmult_commute [of w] zadd_zmult_distrib)
-lemma zadd_zmult_distrib2: "(w::int) * (z1 + z2) = (w * z1) + (w * z2)"
-by (simp add: zmult_commute [of w] zadd_zmult_distrib)
+lemma zdiff_zmult_distrib:
+ fixes w z1 z2::"int"
+ shows "(z1 - z2) * w = (z1 * w) - (z2 * w)"
+ by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus)
-lemma zdiff_zmult_distrib: "((z1::int) - z2) * w = (z1 * w) - (z2 * w)"
-by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus)
-
-lemma zdiff_zmult_distrib2: "(w::int) * (z1 - z2) = (w * z1) - (w * z2)"
-by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
+lemma zdiff_zmult_distrib2:
+ fixes w z1 z2::"int"
+ shows "w * (z1 - z2) = (w * z1) - (w * z2)"
+ by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
lemmas int_distrib =
zadd_zmult_distrib zadd_zmult_distrib2
@@ -232,20 +246,21 @@
lemma zmult_1_raw:
shows "mult_raw (1, 0) z = z"
-apply(cases z)
-apply(auto)
-done
+ by (cases z) (auto)
-lemma zmult_1: "(1::int) * z = z"
-apply(lifting zmult_1_raw)
-done
+lemma zmult_1:
+ fixes z::"int"
+ shows "1 * z = z"
+ by (lifting zmult_1_raw)
-lemma zmult_1_right: "z * (1::int) = z"
-by (rule trans [OF zmult_commute zmult_1])
+lemma zmult_1_right:
+ fixes z::"int"
+ shows "z * 1 = z"
+ by (rule trans [OF zmult_commute zmult_1])
lemma zero_not_one:
shows "\<not>(intrel (0, 0) (1::nat, 0::nat))"
-by auto
+ by auto
text{*The Integers Form A Ring*}
instance int :: comm_ring_1
@@ -267,29 +282,29 @@
subsection{*The @{text "\<le>"} Ordering*}
lemma zle_refl_raw:
- "le_raw w w"
-apply(cases w)
-apply(simp add: le_raw_def)
-done
+ shows "le_raw w w"
+ by (cases w) (simp add: le_raw_def)
lemma [quot_respect]:
shows "(intrel ===> intrel ===> op =) le_raw le_raw"
-by (auto) (simp_all add: le_raw_def)
+ by (auto) (simp_all add: le_raw_def)
-lemma zle_refl: "w \<le> (w::int)"
-apply(lifting zle_refl_raw)
-done
+lemma zle_refl:
+ fixes w::"int"
+ shows "w \<le> w"
+ by (lifting zle_refl_raw)
+
lemma zle_trans_raw:
shows "\<lbrakk>le_raw i j; le_raw j k\<rbrakk> \<Longrightarrow> le_raw i k"
apply(cases i, cases j, cases k)
-apply(auto)
-apply(simp add:le_raw_def)
+apply(auto simp add: le_raw_def)
done
-lemma zle_trans: "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> (k::int)"
-apply(lifting zle_trans_raw)
-done
+lemma zle_trans:
+ fixes i j k::"int"
+ shows "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> k"
+ by (lifting zle_trans_raw)
lemma zle_anti_sym_raw:
shows "\<lbrakk>le_raw z w; le_raw w z\<rbrakk> \<Longrightarrow> intrel z w"
@@ -297,34 +312,43 @@
apply(auto iff: le_raw_def)
done
-lemma zle_anti_sym: "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = (w::int)"
-apply(lifting zle_anti_sym_raw)
-done
+lemma zle_anti_sym:
+ fixes z w::"int"
+ shows "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = w"
+ by (lifting zle_anti_sym_raw)
+
(* Axiom 'order_less_le' of class 'order': *)
-lemma zless_le: "((w::int) < z) = (w \<le> z & w \<noteq> z)"
-by (simp add: less_int_def)
+lemma zless_le:
+ fixes w z::"int"
+ shows "(w < z) = (w \<le> z & w \<noteq> z)"
+ by (simp add: less_int_def)
instance int :: order
-apply(intro_classes)
-apply(auto intro: zle_refl zle_trans zle_anti_sym zless_le simp add: less_int_def)
+apply (default)
+apply(auto simp add: zless_le zle_anti_sym)[1]
+apply(rule zle_refl)
+apply(erule zle_trans, assumption)
+apply(erule zle_anti_sym, assumption)
done
(* Axiom 'linorder_linear' of class 'linorder': *)
lemma zle_linear_raw:
- "le_raw z w \<or> le_raw w z"
+ shows "le_raw z w \<or> le_raw w z"
apply(cases w, cases z)
apply(auto iff: le_raw_def)
done
-
-lemma zle_linear: "(z::int) \<le> w \<or> w \<le> z"
-apply(lifting zle_linear_raw)
-done
+lemma zle_linear:
+ fixes z w::"int"
+ shows "z \<le> w \<or> w \<le> z"
+ by (lifting zle_linear_raw)
instance int :: linorder
-proof qed (rule zle_linear)
+apply(default)
+apply(rule zle_linear)
+done
lemma zadd_left_mono_raw:
shows "le_raw i j \<Longrightarrow> le_raw (add_raw k i) (add_raw k j)"
@@ -332,10 +356,10 @@
apply(auto simp add: add_raw_def le_raw_def)
done
-lemma zadd_left_mono: "i \<le> j \<Longrightarrow> k + i \<le> k + (j::int)"
-apply(lifting zadd_left_mono_raw)
-done
-
+lemma zadd_left_mono:
+ fixes i j::"int"
+ shows "i \<le> j \<Longrightarrow> k + i \<le> k + j"
+ by (lifting zadd_left_mono_raw)
subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
@@ -344,7 +368,7 @@
"nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
quotient_definition
- "nat2::int\<Rightarrow>nat"
+ "nat2::int \<Rightarrow> nat"
as
"nat_raw"
@@ -358,12 +382,12 @@
lemma [quot_respect]:
shows "(intrel ===> op =) nat_raw nat_raw"
-apply(auto iff: nat_raw_def)
-done
+ by (auto iff: nat_raw_def)
-lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
-unfolding less_int_def
-apply(lifting nat_le_eq_zle_raw)
-done
+lemma nat_le_eq_zle:
+ fixes w z::"int"
+ shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
+ unfolding less_int_def
+ by (lifting nat_le_eq_zle_raw)
end
--- a/Quot/quotient_def.ML Fri Jan 01 11:30:00 2010 +0100
+++ b/Quot/quotient_def.ML Fri Jan 01 23:59:32 2010 +0100
@@ -26,15 +26,15 @@
(* interface and syntax setup *)
-(* the ML-interface takes a 4-tuple consisting of *)
-(* *)
-(* - the mixfix annotation *)
-(* - name and attributes *)
-(* - the new constant including its type *)
-(* - the rhs of the definition *)
-(* *)
-(* returns the defined constant and its definition *)
-(* theorem; stores the data in the qconsts slot *)
+(* the ML-interface takes a 4-tuple consisting of *)
+(* *)
+(* - the mixfix annotation *)
+(* - name and attributes *)
+(* - the new constant as term *)
+(* - the rhs of the definition as term *)
+(* *)
+(* it returns the defined constant and its definition *)
+(* theorem; stores the data in the qconsts slot *)
fun quotient_def mx attr lhs rhs lthy =
let
@@ -55,10 +55,10 @@
((trm, thm), lthy'')
end
-fun quotdef_cmd ((attr, lhsstr), (mx, rhsstr)) lthy =
+fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy =
let
- val lhs = Syntax.read_term lthy lhsstr
- val rhs = Syntax.read_term lthy rhsstr
+ val lhs = Syntax.read_term lthy lhs_str
+ val rhs = Syntax.read_term lthy rhs_str
in
quotient_def mx attr lhs rhs lthy |> snd
end
--- a/Quot/quotient_tacs.ML Fri Jan 01 11:30:00 2010 +0100
+++ b/Quot/quotient_tacs.ML Fri Jan 01 23:59:32 2010 +0100
@@ -39,7 +39,7 @@
fun atomize_thm thm =
let
- val thm' = Thm.freezeT (forall_intr_vars thm) (* TODO: is this proper Isar-technology? *)
+ val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
val thm'' = ObjectLogic.atomize (cprop_of thm')
in
@{thm equal_elim_rule1} OF [thm'', thm']
@@ -60,7 +60,7 @@
val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
(* FIXME / TODO: test whether DETERM makes any runtime-difference *)
-(* FIXME / TODO: reason: it might back-track over the two alternatives in FIRST' *)
+(* FIXME / TODO: reason: the tactic might back-track over the two alternatives in FIRST' *)
fun quotient_tac ctxt = SOLVES'
(REPEAT_ALL_NEW (FIRST'
[rtac @{thm identity_quotient},
@@ -84,15 +84,15 @@
fun get_match_inst thy pat trm =
let
val univ = Unify.matchers thy [(pat, trm)]
- val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *)
+ val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *)
val tenv = Vartab.dest (Envir.term_env env)
val tyenv = Vartab.dest (Envir.type_env env)
in
(map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
end
-(* calculates the instantiations for te lemmas *)
-(* ball_reg_eqv_range and bex_reg_eqv_range *)
+(* calculates the instantiations for the lemmas *)
+(* ball_reg_eqv_range and bex_reg_eqv_range *)
fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
let
fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
@@ -106,11 +106,11 @@
SOME thm''
end
handle _ => NONE
-(* FIXME/TODO: !!!CLEVER CODE!!! *)
-(* FIXME/TODO: What is the place where the exception is raised, *)
-(* FIXME/TODO: and which exception is it? *)
-(* FIXME/TODO: Can one not find out from the types of R1 or R2, *)
-(* FIXME/TODO: or from their form, when NONE should be returned? *)
+(* FIXME/TODO: !!!CLEVER CODE!!! *)
+(* FIXME/TODO: What are the places where the exceptions are raised, *)
+(* FIXME/TODO: and which exception is it? *)
+(* FIXME/TODO: Can one not find out from the types of R1, R2 and redex *)
+(* FIXME/TODO: when NONE should be returned? *)
fun ball_bex_range_simproc ss redex =
let
@@ -231,10 +231,9 @@
val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
-
-(* We apply apply_rsp only in case if the type needs lifting. *)
-(* This is the case if the type of the data in the Quot_True *)
-(* assumption is different from the corresponding type in the goal *)
+(* We apply apply_rsp only in case if the type needs lifting. *)
+(* This is the case if the type of the data in the Quot_True *)
+(* assumption is different from the corresponding type in the goal. *)
val apply_rsp_tac =
Subgoal.FOCUS (fn {concl, asms, context,...} =>
let
@@ -269,13 +268,13 @@
in
rtac thm THEN' quotient_tac ctxt
end
-(* TODO: Are they raised by instantiate'? *)
-(* TODO: Again, can one specify more concretely when no_tac should be returned? *)
+(* TODO: Are they raised by instantiate'? *)
+(* TODO: Again, can one specify more concretely *)
+(* TODO: in terms of R when no_tac should be returned? *)
handle THM _ => K no_tac
| TYPE _ => K no_tac
| TERM _ => K no_tac
-
fun rep_abs_rsp_tac ctxt =
SUBGOAL (fn (goal, i) =>
case (bare_concl goal) of
@@ -564,16 +563,16 @@
(* The General Shape of the Lifting Procedure *)
(**********************************************)
-(* - A is the original raw theorem *)
-(* - B is the regularized theorem *)
-(* - C is the rep/abs injected version of B *)
-(* - D is the lifted theorem *)
-(* *)
-(* - 1st prem is the regularization step *)
-(* - 2nd prem is the rep/abs injection step *)
-(* - 3rd prem is the cleaning part *)
-(* *)
-(* the Quot_True premise in 2 records the lifted theorem *)
+(* - A is the original raw theorem *)
+(* - B is the regularized theorem *)
+(* - C is the rep/abs injected version of B *)
+(* - D is the lifted theorem *)
+(* *)
+(* - 1st prem is the regularization step *)
+(* - 2nd prem is the rep/abs injection step *)
+(* - 3rd prem is the cleaning part *)
+(* *)
+(* the Quot_True premise in 2nd records the lifted theorem *)
val lifting_procedure_thm =
@{lemma "[|A;
--- a/Quot/quotient_term.ML Fri Jan 01 11:30:00 2010 +0100
+++ b/Quot/quotient_term.ML Fri Jan 01 23:59:32 2010 +0100
@@ -72,7 +72,7 @@
TVar _ => mk_Free rty
| Type (_, []) => mk_identity rty
| Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
- | _ => raise LIFT_MATCH ("mk_mapfun_aux (default)")
+ | _ => raise LIFT_MATCH ("mk_mapfun (default)")
in
fold_rev Term.lambda vs' (mk_mapfun_aux rty)
end
@@ -120,13 +120,13 @@
(* produces an aggregate absrep function *)
(* *)
-(* - In case of equal types we just return the identity *)
+(* - In case of equal types we just return the identity. *)
(* *)
(* - In case of function types and TFrees, we recurse, taking in *)
(* the first case the polarity change into account. *)
(* *)
(* - If the type constructors are equal, we recurse for the *)
-(* arguments and prefix the appropriate map function *)
+(* arguments and build the appropriate map function. *)
(* *)
(* - If the type constructors are unequal, there must be an *)
(* instance of quotient types: *)
@@ -135,12 +135,12 @@
(* must be some distinct TVars *)
(* - we then match the rty_pat with rty and qty_pat with qty; *)
(* if matching fails the types do not match *)
-(* - the matching produces two environments, we look up the *)
+(* - the matching produces two environments; we look up the *)
(* assignments for the qty_pat variables and recurse on the *)
-(* assignmetnts *)
+(* assignments *)
(* - we prefix the aggregate map function for the rty_pat, *)
(* which is an abstraction over all type variables *)
-(* - finally we compse the result with the appropriate *)
+(* - finally we compose the result with the appropriate *)
(* absrep function *)
(* *)
(* The composition is necessary for types like *)
--- a/Quot/quotient_typ.ML Fri Jan 01 11:30:00 2010 +0100
+++ b/Quot/quotient_typ.ML Fri Jan 01 23:59:32 2010 +0100
@@ -218,8 +218,8 @@
(* - the type to be quotient *)
(* - the relation according to which the type is quotient *)
(* *)
-(* opens a proof-state in which one has to show that the *)
-(* relation is an equivalence relation *)
+(* it opens a proof-state in which one has to show that the *)
+(* relations are equivalence relations *)
fun quotient_type quot_list lthy =
let