Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merge
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Sun, 06 Dec 2009 22:58:03 +0100
changeset 581 2da4fb1894d2
parent 580 fc48fe9667f2 (diff)
parent 578 070161f1996a (current diff)
child 584 97f6e5c61f03
Merge
IntEx2.thy file | annotate | diff | comparison | revisions 
--- a/IntEx2.thy	Sun Dec 06 11:39:34 2009 +0100
+++ b/IntEx2.thy	Sun Dec 06 22:58:03 2009 +0100
@@ -54,7 +54,7 @@
 where
   "minus_raw (x, y) = (y, x)"
 
-quotient_def 
+quotient_def
   minus_qnt::"int \<Rightarrow> int"
 where
   "minus_qnt \<equiv> minus_raw"
@@ -111,6 +111,10 @@
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
 by auto
 
+lemma minus_raw_rsp[quotient_rsp]:
+  shows "(op \<approx> ===> op \<approx>) minus_raw minus_raw"
+  by auto
+
 lemma mult_raw_rsp[quotient_rsp]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
 apply(auto)
@@ -156,9 +160,9 @@
    (simp add: mult algebra_simps)
 
 lemma one_zero_distinct:
-  shows "(0, 0) \<noteq> ((1::nat), (0::nat))"
+  shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
   by simp
-  
+
 text{*The integers form a @{text comm_ring_1}*}
 
 
@@ -179,61 +183,34 @@
     done
   show "0 + i = (i::int)"
     unfolding add_int_def Zero_int_def 
-    apply(tactic {* procedure_tac @{context} @{thm plus_zero_raw} 1 *})
-    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
-    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-    defer
-    apply(tactic {* clean_tac @{context} 1*})
-    sorry
+    apply(tactic {* lift_tac @{context} @{thm plus_zero_raw} [@{thm int_equivp}] 1 *})
+    done
   show "- i + i = 0"
     unfolding add_int_def minus_int_def Zero_int_def 
-    apply(tactic {* procedure_tac @{context} @{thm plus_minus_zero_raw} 1 *})
-    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
-    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-    defer
-    apply(tactic {* clean_tac @{context} 1*})
-    sorry
+    apply(tactic {* lift_tac @{context} @{thm plus_minus_zero_raw} [@{thm int_equivp}] 1 *})
+    done
   show "i - j = i + - j"
     by (simp add: diff_int_def)
   show "(i * j) * k = i * (j * k)"
     unfolding mult_int_def 
-    apply(tactic {* procedure_tac @{context} @{thm mult_assoc_raw} 1 *})
-    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
-    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-    defer
-    apply(tactic {* clean_tac @{context} 1*})
-    sorry
+    apply(tactic {* lift_tac @{context} @{thm mult_assoc_raw} [@{thm int_equivp}] 1 *})
+    done
   show "i * j = j * i"
     unfolding mult_int_def 
-    apply(tactic {* procedure_tac @{context} @{thm mult_sym_raw} 1 *})
-    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
-    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-    defer
-    apply(tactic {* clean_tac @{context} 1*})
-    sorry
+    apply(tactic {* lift_tac @{context} @{thm mult_sym_raw} [@{thm int_equivp}] 1 *})
+    done
   show "1 * i = i"
     unfolding mult_int_def One_int_def
-    apply(tactic {* procedure_tac @{context} @{thm mult_one_raw} 1 *})
-    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
-    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-    defer
-    apply(tactic {* clean_tac @{context} 1*})
-    sorry
+    apply(tactic {* lift_tac @{context} @{thm mult_one_raw} [@{thm int_equivp}] 1 *})
+    done
   show "(i + j) * k = i * k + j * k"
     unfolding mult_int_def add_int_def
-    apply(tactic {* procedure_tac @{context} @{thm mult_plus_comm_raw} 1 *})
-    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
-    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-    defer
-    apply(tactic {* clean_tac @{context} 1*})
-    sorry
+    apply(tactic {* lift_tac @{context} @{thm mult_plus_comm_raw} [@{thm int_equivp}] 1 *})
+    done
   show "0 \<noteq> (1::int)"
     unfolding Zero_int_def One_int_def
-    apply(tactic {* procedure_tac @{context} @{thm one_zero_distinct} 1 *})
-    defer
-    defer
-    apply(tactic {* clean_tac @{context} 1*})
-    sorry
+    apply(tactic {* lift_tac @{context} @{thm one_zero_distinct} [@{thm int_equivp}] 1 *})
+    done
 qed
 
 term of_nat
@@ -317,8 +294,8 @@
 qed
 
 lemma test:
-  "\<lbrakk>le_raw i j \<and> i \<noteq> j; le_raw (0, 0) k \<and> (0, 0) \<noteq> k\<rbrakk>
-    \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> mult_raw k i \<noteq> mult_raw k j"
+  "\<lbrakk>le_raw i j \<and> \<not>i \<approx> j; le_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk>
+    \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> \<not>mult_raw k i \<approx> mult_raw k j"
 apply(cases i, cases j, cases k)
 apply(auto simp add: mult algebra_simps)
 sorry
@@ -330,12 +307,8 @@
   fix i j k :: int
   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
     unfolding mult_int_def le_int_def less_int_def Zero_int_def
-    apply(tactic {* procedure_tac @{context} @{thm test} 1 *})
-    defer
-    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-    defer
-    apply(tactic {* clean_tac @{context} 1*})
-    sorry
+    apply(tactic {* lift_tac @{context} @{thm test} [@{thm int_equivp}] 1 *})
+    done
   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
     by (simp only: zabs_def)
   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
--- a/LFex.thy	Sun Dec 06 11:39:34 2009 +0100
+++ b/LFex.thy	Sun Dec 06 22:58:03 2009 +0100
@@ -287,15 +287,15 @@
 using a0 a1 a2 a3 a4 a5 a6 a7 a8
 *)
 
-lemma "\<lbrakk>P1 TYP;
-  \<And>ty name kind. \<lbrakk>P2 ty; P1 kind\<rbrakk> \<Longrightarrow> P1 (KPI ty name kind);
-  \<And>id. P2 (TCONST id);
-  \<And>ty trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P2 (TAPP ty trm);
-  \<And>ty1 name ty2. \<lbrakk>P2 ty1; P2 ty2\<rbrakk> \<Longrightarrow> P2 (TPI ty1 name ty2);
-  \<And>id. P3 (CONS id); \<And>name. P3 (VAR name);
-  \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2);
-  \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk>
-  \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm"
+lemma "\<lbrakk>P TYP;
+  \<And>ty name kind. \<lbrakk>Q ty; P kind\<rbrakk> \<Longrightarrow> P (KPI ty name kind);
+  \<And>id. Q (TCONST id);
+  \<And>ty trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> Q (TAPP ty trm);
+  \<And>ty1 name ty2. \<lbrakk>Q ty1; Q ty2\<rbrakk> \<Longrightarrow> Q (TPI ty1 name ty2);
+  \<And>id. R (CONS id); \<And>name. R (VAR name);
+  \<And>trm1 trm2. \<lbrakk>R trm1; R trm2\<rbrakk> \<Longrightarrow> R (APP trm1 trm2);
+  \<And>ty name trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> R (LAM ty name trm)\<rbrakk>
+  \<Longrightarrow> P mkind \<and> Q mty \<and> R mtrm"
 apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_equivps} 1 *})
 done
nominal2