# HG changeset patch # User oheimb # Date 830271501 -7200 # Node ID 2c109cd2fdd065ef53ed6a4135bc41ed2c455a73 # Parent 608196238072f07d183c92c68c4ec8298b2f56ce repaired critical proofs depending on the order inside non-confluent SimpSets, (temporarily) removed problematic rule less_Suc_eq form simpset_of "Nat" diff -r 608196238072 -r 2c109cd2fdd0 src/HOL/Fun.ML --- 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)" ]; diff -r 608196238072 -r 2c109cd2fdd0 src/HOL/HOL.ML --- 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 **) diff -r 608196238072 -r 2c109cd2fdd0 src/HOL/HOL.thy --- 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 *) diff -r 608196238072 -r 2c109cd2fdd0 src/HOL/Nat.ML --- 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 ~P(j))" (* start 8bit 1 *) +syntax + "Gmu" :: (nat => bool) => nat (binder "´" 10) + +translations + "´x.P" == "LEAST x. P" (* end 8bit 1 *) end diff -r 608196238072 -r 2c109cd2fdd0 src/HOL/Prod.thy --- 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 diff -r 608196238072 -r 2c109cd2fdd0 src/HOL/Set.thy --- 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