# HG changeset patch
# User nipkow
# Date 800050208 -7200
# Node ID c8dfb56a7e95b998b7cbc9a6fedd84370c92c6b8
# Parent  dd72845736014b82c9569985356832b6c47f4b65
Prod is now a parent of Lfp.
Added thm induct2 to Lfp.
Changed the way patterns in abstractions are pretty printed.
It has become simpler now but fails if split has more than one argument
because then the ast-translation does not match.

diff -r dd7284573601 -r c8dfb56a7e95 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue May 09 10:43:19 1995 +0200
+++ b/src/HOL/HOL.thy	Tue May 09 22:10:08 1995 +0200
@@ -101,8 +101,7 @@
   "EX xs. P"    => "? xs. P"
   "EX! xs. P"   => "?! xs. P"
   "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
-  "let x = a in e"          == "Let a (%x. e)"
-
+  "let x = a in e"        == "Let a (%x. e)"
 
 rules
 
diff -r dd7284573601 -r c8dfb56a7e95 src/HOL/Lfp.ML
--- a/src/HOL/Lfp.ML	Tue May 09 10:43:19 1995 +0200
+++ b/src/HOL/Lfp.ML	Tue May 09 22:10:08 1995 +0200
@@ -52,6 +52,17 @@
 	    rtac (CollectI RS subsetI), rtac indhyp, atac]);
 qed "induct";
 
+val major::prems = goal Lfp.thy
+  "[| (a,b) : lfp f; mono f; \
+\     !!a b. (a,b) : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b";
+by(res_inst_tac [("c1","P")] (split RS subst) 1);
+br (major RS induct) 1;
+brs prems 1;
+by(res_inst_tac[("p","x")]PairE 1);
+by(hyp_subst_tac 1);
+by(asm_simp_tac (prod_ss addsimps prems) 1);
+qed"induct2";
+
 (** Definition forms of lfp_Tarski and induct, to control unfolding **)
 
 val [rew,mono] = goal Lfp.thy "[| h==lfp(f);  mono(f) |] ==> h = f(h)";
diff -r dd7284573601 -r c8dfb56a7e95 src/HOL/Lfp.thy
--- a/src/HOL/Lfp.thy	Tue May 09 10:43:19 1995 +0200
+++ b/src/HOL/Lfp.thy	Tue May 09 22:10:08 1995 +0200
@@ -6,7 +6,7 @@
 The Knaster-Tarski Theorem
 *)
 
-Lfp = mono + 
+Lfp = mono + Prod +
 consts lfp :: "['a set=>'a set] => 'a set"
 defs
  (*least fixed point*)
diff -r dd7284573601 -r c8dfb56a7e95 src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Tue May 09 10:43:19 1995 +0200
+++ b/src/HOL/Prod.thy	Tue May 09 22:10:08 1995 +0200
@@ -40,16 +40,16 @@
 syntax
   "@Tuple"      :: "['a, args] => 'a * 'b"            ("(1'(_,/ _'))")
 
-  "@pttrn"  :: "pttrns => pttrn"            ("'(_')")
-  ""        :: " pttrn           => pttrns" ("_")
-  "@pttrns" :: "[pttrn,pttrns]   => pttrns" ("_,/_")
+  "@pttrn"  :: "[pttrn,pttrns] => pttrn"              ("'(_,/_')")
+  ""        :: " pttrn         => pttrns"             ("_")
+  "@pttrns" :: "[pttrn,pttrns] => pttrns"             ("_,/_")
 
 translations
   "(x, y, z)"   == "(x, (y, z))"
   "(x, y)"      == "Pair x y"
 
-  "%(x,y,zs).b"   => "split(%x (y,zs).b)"
-  "%(x,y).b"      => "split(%x y.b)"
+  "%(x,y,zs).b"   == "split(%x (y,zs).b)"
+  "%(x,y).b"      == "split(%x y.b)"
 (* The <= direction fails if split has more than one argument because
    ast-matching fails. Otherwise it would work fine *)
 
@@ -75,12 +75,12 @@
   Unity_def     "() == Abs_Unit(True)"
 
 end
-
+(*
 ML
 
 local open Syntax
 
-fun pttrn s = const"@pttrn" $ s;
+fun pttrn(_ $ s $ t) = const"@pttrn" $ s $ t;
 fun pttrns s t = const"@pttrns" $ s $ t;
 
 fun split2(Abs(x,T,t)) =
@@ -102,3 +102,4 @@
 val print_translation = [("split", split_tr')];
 
 end;
+*)