Prod is now a parent of Lfp.
authornipkow
Tue May 09 22:10:08 1995 +0200 (1995-05-09)
changeset 1114c8dfb56a7e95
parent 1113 dd7284573601
child 1115 c2d51f10b9ee
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.
src/HOL/HOL.thy
src/HOL/Lfp.ML
src/HOL/Lfp.thy
src/HOL/Prod.thy
     1.1 --- a/src/HOL/HOL.thy	Tue May 09 10:43:19 1995 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue May 09 22:10:08 1995 +0200
     1.3 @@ -101,8 +101,7 @@
     1.4    "EX xs. P"    => "? xs. P"
     1.5    "EX! xs. P"   => "?! xs. P"
     1.6    "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
     1.7 -  "let x = a in e"          == "Let a (%x. e)"
     1.8 -
     1.9 +  "let x = a in e"        == "Let a (%x. e)"
    1.10  
    1.11  rules
    1.12  
     2.1 --- a/src/HOL/Lfp.ML	Tue May 09 10:43:19 1995 +0200
     2.2 +++ b/src/HOL/Lfp.ML	Tue May 09 22:10:08 1995 +0200
     2.3 @@ -52,6 +52,17 @@
     2.4  	    rtac (CollectI RS subsetI), rtac indhyp, atac]);
     2.5  qed "induct";
     2.6  
     2.7 +val major::prems = goal Lfp.thy
     2.8 +  "[| (a,b) : lfp f; mono f; \
     2.9 +\     !!a b. (a,b) : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b";
    2.10 +by(res_inst_tac [("c1","P")] (split RS subst) 1);
    2.11 +br (major RS induct) 1;
    2.12 +brs prems 1;
    2.13 +by(res_inst_tac[("p","x")]PairE 1);
    2.14 +by(hyp_subst_tac 1);
    2.15 +by(asm_simp_tac (prod_ss addsimps prems) 1);
    2.16 +qed"induct2";
    2.17 +
    2.18  (** Definition forms of lfp_Tarski and induct, to control unfolding **)
    2.19  
    2.20  val [rew,mono] = goal Lfp.thy "[| h==lfp(f);  mono(f) |] ==> h = f(h)";
     3.1 --- a/src/HOL/Lfp.thy	Tue May 09 10:43:19 1995 +0200
     3.2 +++ b/src/HOL/Lfp.thy	Tue May 09 22:10:08 1995 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  The Knaster-Tarski Theorem
     3.5  *)
     3.6  
     3.7 -Lfp = mono + 
     3.8 +Lfp = mono + Prod +
     3.9  consts lfp :: "['a set=>'a set] => 'a set"
    3.10  defs
    3.11   (*least fixed point*)
     4.1 --- a/src/HOL/Prod.thy	Tue May 09 10:43:19 1995 +0200
     4.2 +++ b/src/HOL/Prod.thy	Tue May 09 22:10:08 1995 +0200
     4.3 @@ -40,16 +40,16 @@
     4.4  syntax
     4.5    "@Tuple"      :: "['a, args] => 'a * 'b"            ("(1'(_,/ _'))")
     4.6  
     4.7 -  "@pttrn"  :: "pttrns => pttrn"            ("'(_')")
     4.8 -  ""        :: " pttrn           => pttrns" ("_")
     4.9 -  "@pttrns" :: "[pttrn,pttrns]   => pttrns" ("_,/_")
    4.10 +  "@pttrn"  :: "[pttrn,pttrns] => pttrn"              ("'(_,/_')")
    4.11 +  ""        :: " pttrn         => pttrns"             ("_")
    4.12 +  "@pttrns" :: "[pttrn,pttrns] => pttrns"             ("_,/_")
    4.13  
    4.14  translations
    4.15    "(x, y, z)"   == "(x, (y, z))"
    4.16    "(x, y)"      == "Pair x y"
    4.17  
    4.18 -  "%(x,y,zs).b"   => "split(%x (y,zs).b)"
    4.19 -  "%(x,y).b"      => "split(%x y.b)"
    4.20 +  "%(x,y,zs).b"   == "split(%x (y,zs).b)"
    4.21 +  "%(x,y).b"      == "split(%x y.b)"
    4.22  (* The <= direction fails if split has more than one argument because
    4.23     ast-matching fails. Otherwise it would work fine *)
    4.24  
    4.25 @@ -75,12 +75,12 @@
    4.26    Unity_def     "() == Abs_Unit(True)"
    4.27  
    4.28  end
    4.29 -
    4.30 +(*
    4.31  ML
    4.32  
    4.33  local open Syntax
    4.34  
    4.35 -fun pttrn s = const"@pttrn" $ s;
    4.36 +fun pttrn(_ $ s $ t) = const"@pttrn" $ s $ t;
    4.37  fun pttrns s t = const"@pttrns" $ s $ t;
    4.38  
    4.39  fun split2(Abs(x,T,t)) =
    4.40 @@ -102,3 +102,4 @@
    4.41  val print_translation = [("split", split_tr')];
    4.42  
    4.43  end;
    4.44 +*)