repaired critical proofs depending on the order inside non-confluent SimpSets,
(temporarily) removed problematic rule less_Suc_eq form simpset_of "Nat"
--- a/src/HOL/Fun.ML Tue Apr 23 16:44:22 1996 +0200
+++ b/src/HOL/Fun.ML Tue Apr 23 16:58:21 1996 +0200
@@ -186,10 +186,10 @@
fun prover s = prove_goal Fun.thy s (fn _=>[fast_tac set_cs 1]);
val mem_simps = map prover
- [ "(a : A Un B) = (a:A | a:B)",
- "(a : A Int B) = (a:A & a:B)",
- "(a : Compl(B)) = (~a:B)",
- "(a : A-B) = (a:A & ~a:B)",
+ [ "(a : A Un B) = (a:A | a:B)", (* Un_iff *)
+ "(a : A Int B) = (a:A & a:B)", (* Int_iff *)
+ "(a : Compl(B)) = (~a:B)", (* Compl_iff *)
+ "(a : A-B) = (a:A & ~a:B)", (* Diff_iff *)
"(a : {b}) = (a=b)",
"(a : {x.P(x)}) = P(a)" ];
--- a/src/HOL/HOL.ML Tue Apr 23 16:44:22 1996 +0200
+++ b/src/HOL/HOL.ML Tue Apr 23 16:58:21 1996 +0200
@@ -305,7 +305,7 @@
(** Standard abbreviations **)
-fun stac th = rtac(th RS ssubst);
+fun stac th = CHANGED o rtac (th RS ssubst);
fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);
(** strip proved goal while preserving !-bound var names **)
--- a/src/HOL/HOL.thy Tue Apr 23 16:44:22 1996 +0200
+++ b/src/HOL/HOL.thy Tue Apr 23 16:58:21 1996 +0200
@@ -143,6 +143,40 @@
if_def "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
(* start 8bit 1 *)
+types
+('a, 'b) "ë" (infixr 5)
+
+syntax
+ "Ú" :: "['a::{}, 'a] => prop" ("(_ Ú/ _)" [3, 2] 2)
+ "êë" :: "[prop, prop] => prop" ("(_ êë/ _)" [2, 1] 1)
+ "Gbigimpl" :: "[asms, prop] => prop" ("((3Ë _ Ì) êë/ _)" [0, 1] 1)
+ "Gall" :: "('a => prop) => prop" (binder "Ä" 0)
+
+ "Glam" :: "[idts, 'a::logic] => 'b::logic" ("(3³_./ _)" 10)
+ "Û" :: "['a, 'a] => bool" (infixl 50)
+ "Gnot" :: "bool => bool" ("¿ _" [40] 40)
+ "GEps" :: "[pttrn, bool] => 'a" ("(3®_./ _)" 10)
+ "GAll" :: "[idts, bool] => bool" ("(3Â_./ _)" 10)
+ "GEx" :: "[idts, bool] => bool" ("(3Ã_./ _)" 10)
+ "GEx1" :: "[idts, bool] => bool" ("(3Ã!_./ _)" 10)
+ "À" :: "[bool, bool] => bool" (infixr 35)
+ "Á" :: "[bool, bool] => bool" (infixr 30)
+ "çè" :: "[bool, bool] => bool" (infixr 25)
+
+translations
+(type) "x ë y" == (type) "x => y"
+
+(* "³x.t" => "%x.t" *)
+
+ "x Û y" == "x ~= y"
+ "¿ y" == "~y"
+ "®x.P" == "@x.P"
+ "Âx.P" == "! x. P"
+ "Ãx.P" == "? x. P"
+ "Ã!x.P" == "?! x. P"
+ "x À y" == "x & y"
+ "x Á y" == "x | y"
+ "x çè y" == "x --> y"
(* end 8bit 1 *)
end
@@ -167,6 +201,36 @@
map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
(* start 8bit 2 *)
+local open Ast;
+fun bigimpl_ast_tr (*"Gbigimpl"*) [asms, concl] =
+ fold_ast_p "êë" (unfold_ast "_asms" asms, concl)
+ | bigimpl_ast_tr (*"Gbigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
+fun impl_ast_tr' (*"êë"*) asts =
+ (case unfold_ast_p "êë" (Appl (Constant "êë" :: asts)) of
+ (asms as _ :: _ :: _, concl)
+ => Appl [Constant "Gbigimpl", fold_ast "_asms" asms, concl]
+ | _ => raise Match);
+
+in
+val parse_ast_translation = ("Gbigimpl", bigimpl_ast_tr)::
+ ("Glam", fn asts => Appl (Constant "_abs" :: asts))::
+ parse_ast_translation;
+
+val print_ast_translation = ("êë", impl_ast_tr')::
+ ("_lambda", fn asts => Appl (Constant "Glam" :: asts)) ::
+ print_ast_translation;
+
+end;
+
+local open Syntax in
+val thy = thy
+|> add_trrules_i
+[mk_appl (Constant "Ú" ) [Variable "P", Variable "Q"] <->
+ mk_appl (Constant "==") [Variable "P", Variable "Q"],
+ mk_appl (Constant "êë" ) [Variable "P", Variable "Q"] <->
+ mk_appl (Constant "==>") [Variable "P", Variable "Q"],
+ (Constant "Ä" ) <-> (Constant "!!")]
+end;
(* end 8bit 2 *)
--- a/src/HOL/Nat.ML Tue Apr 23 16:44:22 1996 +0200
+++ b/src/HOL/Nat.ML Tue Apr 23 16:58:21 1996 +0200
@@ -337,10 +337,21 @@
addEs [less_trans, lessE]) 1);
qed "Suc_mono";
+
+goal Nat.thy "(Suc m < n | Suc m = n) = (m < n)";
+
+
+goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
+by(stac less_Suc_eq 1);
+by(rtac
+
+
+(*
goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]);
qed "Suc_less_eq";
Addsimps [Suc_less_eq];
+*)
goal Nat.thy "~(Suc(n) < n)";
by (fast_tac (HOL_cs addEs [Suc_lessD RS less_irrefl]) 1);
--- a/src/HOL/Nat.thy Tue Apr 23 16:44:22 1996 +0200
+++ b/src/HOL/Nat.thy Tue Apr 23 16:58:21 1996 +0200
@@ -77,6 +77,11 @@
Least_def "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
(* start 8bit 1 *)
+syntax
+ "Gmu" :: (nat => bool) => nat (binder "´" 10)
+
+translations
+ "´x.P" == "LEAST x. P"
(* end 8bit 1 *)
end
--- a/src/HOL/Prod.thy Tue Apr 23 16:44:22 1996 +0200
+++ b/src/HOL/Prod.thy Tue Apr 23 16:58:21 1996 +0200
@@ -83,6 +83,17 @@
Unity_def "() == Abs_Unit(True)"
(* start 8bit 1 *)
+types
+
+('a, 'b) "ò" (infixr 20)
+
+translations
+
+(type) "x ò y" == (type) "x * y"
+
+ "³(x,y,zs).b" == "split(³x.³(y,zs).b)"
+ "³(x,y).b" == "split(³x y.b)"
+
(* end 8bit 1 *)
end
--- a/src/HOL/Set.thy Tue Apr 23 16:44:22 1996 +0200
+++ b/src/HOL/Set.thy Tue Apr 23 16:58:21 1996 +0200
@@ -104,6 +104,33 @@
surj_def "surj(f) == ! y. ? x. y=f(x)"
(* start 8bit 1 *)
+syntax
+ "Ð" :: "['a set, 'a set] => 'a set" (infixl 70)
+ "Ñ" :: "['a set, 'a set] => 'a set" (infixl 65)
+ "Î" :: "['a, 'a set] => bool" (infixl 50)
+ "ñ" :: "['a, 'a set] => bool" (infixl 50)
+ GUnion :: "(('a set)set) => 'a set" ("Ó_" [90] 90)
+ GInter :: "(('a set)set) => 'a set" ("Ò_" [90] 90)
+ GUNION1 :: "['a => 'b set] => 'b set" (binder "Ó " 10)
+ GINTER1 :: "['a => 'b set] => 'b set" (binder "Ò " 10)
+ GINTER :: "[pttrn, 'a set, 'b set] => 'b set" ("(3Ò _Î_./ _)" 10)
+ GUNION :: "[pttrn, 'a set, 'b set] => 'b set" ("(3Ó _Î_./ _)" 10)
+ GBall :: "[pttrn, 'a set, bool] => bool" ("(3Â _Î_./ _)" 10)
+ GBex :: "[pttrn, 'a set, bool] => bool" ("(3Ã _Î_./ _)" 10)
+
+translations
+ "x ñ y" == "¿(x : y)"
+ "x Î y" == "(x : y)"
+ "x Ð y" == "x Int y"
+ "x Ñ y" == "x Un y"
+ "ÒX" == "Inter X"
+ "ÓX" == "Union X"
+ "Òx.A" == "INT x.A"
+ "Óx.A" == "UN x.A"
+ "ÒxÎA. B" == "INT x:A. B"
+ "ÓxÎA. B" == "UN x:A. B"
+ "ÂxÎA. P" == "! x:A. P"
+ "ÃxÎA. P" == "? x:A. P"
(* end 8bit 1 *)
end