repaired critical proofs depending on the order inside non-confluent SimpSets,
authoroheimb
Tue Apr 23 16:58:21 1996 +0200 (1996-04-23)
changeset 16722c109cd2fdd0
parent 1671 608196238072
child 1673 d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets,
(temporarily) removed problematic rule less_Suc_eq form simpset_of "Nat"
src/HOL/Fun.ML
src/HOL/HOL.ML
src/HOL/HOL.thy
src/HOL/Nat.ML
src/HOL/Nat.thy
src/HOL/Prod.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Fun.ML	Tue Apr 23 16:44:22 1996 +0200
     1.2 +++ b/src/HOL/Fun.ML	Tue Apr 23 16:58:21 1996 +0200
     1.3 @@ -186,10 +186,10 @@
     1.4  fun prover s = prove_goal Fun.thy s (fn _=>[fast_tac set_cs 1]);
     1.5  
     1.6  val mem_simps = map prover
     1.7 - [ "(a : A Un B)   =  (a:A | a:B)",
     1.8 -   "(a : A Int B)  =  (a:A & a:B)",
     1.9 -   "(a : Compl(B)) =  (~a:B)",
    1.10 -   "(a : A-B)      =  (a:A & ~a:B)",
    1.11 + [ "(a : A Un B)   =  (a:A | a:B)",	(* Un_iff *)
    1.12 +   "(a : A Int B)  =  (a:A & a:B)",	(* Int_iff *)
    1.13 +   "(a : Compl(B)) =  (~a:B)",		(* Compl_iff *)
    1.14 +   "(a : A-B)      =  (a:A & ~a:B)",	(* Diff_iff *)
    1.15     "(a : {b})      =  (a=b)",
    1.16     "(a : {x.P(x)}) =  P(a)" ];
    1.17  
     2.1 --- a/src/HOL/HOL.ML	Tue Apr 23 16:44:22 1996 +0200
     2.2 +++ b/src/HOL/HOL.ML	Tue Apr 23 16:58:21 1996 +0200
     2.3 @@ -305,7 +305,7 @@
     2.4  
     2.5  (** Standard abbreviations **)
     2.6  
     2.7 -fun stac th = rtac(th RS ssubst);
     2.8 +fun stac th = CHANGED o rtac (th RS ssubst);
     2.9  fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
    2.10  
    2.11  (** strip proved goal while preserving !-bound var names **)
     3.1 --- a/src/HOL/HOL.thy	Tue Apr 23 16:44:22 1996 +0200
     3.2 +++ b/src/HOL/HOL.thy	Tue Apr 23 16:58:21 1996 +0200
     3.3 @@ -143,6 +143,40 @@
     3.4    if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
     3.5  
     3.6  (* start 8bit 1 *)
     3.7 +types
     3.8 +('a, 'b) ""          (infixr 5)
     3.9 +
    3.10 +syntax
    3.11 +  ""		:: "['a::{}, 'a] => prop"       ("(_ / _)"         [3, 2] 2)
    3.12 +  ""		:: "[prop, prop] => prop"	("(_ / _)"        [2, 1] 1)
    3.13 +  "Gbigimpl"	:: "[asms, prop] => prop"	("((3 _ ) / _)" [0, 1] 1)
    3.14 +  "Gall"	:: "('a => prop) => prop"	(binder ""                0)
    3.15 +
    3.16 +  "Glam"         :: "[idts, 'a::logic] => 'b::logic"  ("(3_./ _)" 10)
    3.17 +  ""           :: "['a, 'a] => bool"                 (infixl 50)
    3.18 +  "Gnot"        :: "bool => bool"                     (" _" [40] 40)
    3.19 +  "GEps"        :: "[pttrn, bool] => 'a"               ("(3_./ _)" 10)
    3.20 +  "GAll"        :: "[idts, bool] => bool"             ("(3_./ _)" 10)
    3.21 +  "GEx"         :: "[idts, bool] => bool"             ("(3_./ _)" 10)
    3.22 +  "GEx1"        :: "[idts, bool] => bool"             ("(3!_./ _)" 10)
    3.23 +  ""           :: "[bool, bool] => bool"             (infixr 35)
    3.24 +  ""           :: "[bool, bool] => bool"             (infixr 30)
    3.25 +  ""          :: "[bool, bool] => bool"             (infixr 25)
    3.26 +
    3.27 +translations
    3.28 +(type)  "x  y"	== (type) "x => y" 
    3.29 +
    3.30 +(*  "x.t"	=> "%x.t" *)
    3.31 +
    3.32 +  "x  y"	== "x ~= y"
    3.33 +  " y"		== "~y"
    3.34 +  "x.P"	== "@x.P"
    3.35 +  "x.P"	== "! x. P"
    3.36 +  "x.P"	== "? x. P"
    3.37 +  "!x.P"	== "?! x. P"
    3.38 +  "x  y"	== "x & y"
    3.39 +  "x  y"	== "x | y"
    3.40 +  "x  y"	== "x --> y"
    3.41  (* end 8bit 1 *)
    3.42  
    3.43  end
    3.44 @@ -167,6 +201,36 @@
    3.45    map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
    3.46  
    3.47  (* start 8bit 2 *)
    3.48 +local open Ast;
    3.49 +fun bigimpl_ast_tr (*"Gbigimpl"*) [asms, concl] =
    3.50 +      fold_ast_p "" (unfold_ast "_asms" asms, concl)
    3.51 +  | bigimpl_ast_tr (*"Gbigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
    3.52 +fun impl_ast_tr' (*""*) asts =
    3.53 +  (case unfold_ast_p "" (Appl (Constant "" :: asts)) of
    3.54 +    (asms as _ :: _ :: _, concl)
    3.55 +      => Appl [Constant "Gbigimpl", fold_ast "_asms" asms, concl]
    3.56 +  | _ => raise Match);
    3.57 +
    3.58 +in
    3.59 +val parse_ast_translation = ("Gbigimpl", bigimpl_ast_tr)::
    3.60 +				("Glam",    fn asts => Appl (Constant "_abs" :: asts))::
    3.61 +				parse_ast_translation;
    3.62 +
    3.63 +val print_ast_translation = ("", impl_ast_tr')::
    3.64 +				("_lambda", fn asts => Appl (Constant "Glam" :: asts)) ::	
    3.65 +				print_ast_translation;
    3.66 +
    3.67 +end;
    3.68 +
    3.69 +local open Syntax in
    3.70 +val thy = thy 
    3.71 +|> add_trrules_i 
    3.72 +[mk_appl (Constant "" ) [Variable "P", Variable "Q"] <-> 
    3.73 + mk_appl (Constant "==") [Variable "P", Variable "Q"],
    3.74 + mk_appl (Constant "" ) [Variable "P", Variable "Q"] <-> 
    3.75 + mk_appl (Constant "==>") [Variable "P", Variable "Q"],
    3.76 + (Constant "" ) <->  (Constant "!!")]
    3.77 +end;
    3.78  (* end 8bit 2 *)
    3.79  
    3.80  
     4.1 --- a/src/HOL/Nat.ML	Tue Apr 23 16:44:22 1996 +0200
     4.2 +++ b/src/HOL/Nat.ML	Tue Apr 23 16:58:21 1996 +0200
     4.3 @@ -337,10 +337,21 @@
     4.4                       addEs  [less_trans, lessE]) 1);
     4.5  qed "Suc_mono";
     4.6  
     4.7 +
     4.8 +goal Nat.thy "(Suc m < n | Suc m = n) = (m < n)";
     4.9 +
    4.10 +
    4.11 +goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
    4.12 +by(stac less_Suc_eq 1);
    4.13 +by(rtac 
    4.14 +
    4.15 +
    4.16 +(*
    4.17  goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
    4.18  by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]);
    4.19  qed "Suc_less_eq";
    4.20  Addsimps [Suc_less_eq];
    4.21 +*)
    4.22  
    4.23  goal Nat.thy "~(Suc(n) < n)";
    4.24  by (fast_tac (HOL_cs addEs [Suc_lessD RS less_irrefl]) 1);
     5.1 --- a/src/HOL/Nat.thy	Tue Apr 23 16:44:22 1996 +0200
     5.2 +++ b/src/HOL/Nat.thy	Tue Apr 23 16:58:21 1996 +0200
     5.3 @@ -77,6 +77,11 @@
     5.4    Least_def     "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
     5.5  
     5.6  (* start 8bit 1 *)
     5.7 +syntax
     5.8 +  "Gmu"	:: (nat => bool) => nat				(binder "" 10)
     5.9 +
    5.10 +translations
    5.11 +  "x.P"	== "LEAST x. P"
    5.12  (* end 8bit 1 *)
    5.13  
    5.14  end
     6.1 --- a/src/HOL/Prod.thy	Tue Apr 23 16:44:22 1996 +0200
     6.2 +++ b/src/HOL/Prod.thy	Tue Apr 23 16:58:21 1996 +0200
     6.3 @@ -83,6 +83,17 @@
     6.4    Unity_def     "() == Abs_Unit(True)"
     6.5  
     6.6  (* start 8bit 1 *)
     6.7 +types
     6.8 +
     6.9 +('a, 'b) ""          (infixr 20)
    6.10 +
    6.11 +translations
    6.12 +
    6.13 +(type)  "x  y"	== (type) "x * y" 
    6.14 +
    6.15 +  "(x,y,zs).b"   == "split(x.(y,zs).b)"
    6.16 +  "(x,y).b"      == "split(x y.b)"
    6.17 +
    6.18  (* end 8bit 1 *)
    6.19  
    6.20  end
     7.1 --- a/src/HOL/Set.thy	Tue Apr 23 16:44:22 1996 +0200
     7.2 +++ b/src/HOL/Set.thy	Tue Apr 23 16:58:21 1996 +0200
     7.3 @@ -104,6 +104,33 @@
     7.4    surj_def      "surj(f)        == ! y. ? x. y=f(x)"
     7.5  
     7.6  (* start 8bit 1 *)
     7.7 +syntax
     7.8 +  ""		:: "['a set, 'a set] => 'a set"       (infixl 70)
     7.9 +  ""		:: "['a set, 'a set] => 'a set"       (infixl 65)
    7.10 +  ""		:: "['a, 'a set] => bool"             (infixl 50)
    7.11 +  ""		:: "['a, 'a set] => bool"             (infixl 50)
    7.12 +  GUnion	:: "(('a set)set) => 'a set"          ("_" [90] 90)
    7.13 +  GInter	:: "(('a set)set) => 'a set"          ("_" [90] 90)
    7.14 +  GUNION1       :: "['a => 'b set] => 'b set"         (binder " " 10)
    7.15 +  GINTER1       :: "['a => 'b set] => 'b set"         (binder " " 10)
    7.16 +  GINTER	:: "[pttrn, 'a set, 'b set] => 'b set"  ("(3 __./ _)" 10)
    7.17 +  GUNION	:: "[pttrn, 'a set, 'b set] => 'b set"  ("(3 __./ _)" 10)
    7.18 +  GBall		:: "[pttrn, 'a set, bool] => bool"      ("(3 __./ _)" 10)
    7.19 +  GBex		:: "[pttrn, 'a set, bool] => bool"      ("(3 __./ _)" 10)
    7.20 +
    7.21 +translations
    7.22 +  "x  y"      == "(x : y)"
    7.23 +  "x  y"      == "(x : y)"
    7.24 +  "x  y"      == "x Int y"
    7.25 +  "x  y"      == "x Un  y"
    7.26 +  "X"        == "Inter X" 
    7.27 +  "X"        == "Union X"
    7.28 +  "x.A"      == "INT x.A"
    7.29 +  "x.A"      == "UN x.A"
    7.30 +  "xA. B"   == "INT x:A. B"
    7.31 +  "xA. B"   == "UN x:A. B"
    7.32 +  "xA. P"    == "! x:A. P"
    7.33 +  "xA. P"    == "? x:A. P"
    7.34  (* end 8bit 1 *)
    7.35  
    7.36  end