src/HOL/Induct/LList.ML
changeset 5148 74919e8f221c
parent 5143 b94cd208f073
child 5184 9b8547a9496a
     1.1 --- a/src/HOL/Induct/LList.ML	Wed Jul 15 14:13:18 1998 +0200
     1.2 +++ b/src/HOL/Induct/LList.ML	Wed Jul 15 14:19:02 1998 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  ***)
     1.5  
     1.6  Goalw [list_Fun_def]
     1.7 -    "!!M. [| M : X;  X <= list_Fun A (X Un llist(A)) |] ==>  M : llist(A)";
     1.8 +    "[| M : X;  X <= list_Fun A (X Un llist(A)) |] ==>  M : llist(A)";
     1.9  by (etac llist.coinduct 1);
    1.10  by (etac (subsetD RS CollectD) 1);
    1.11  by (assume_tac 1);
    1.12 @@ -44,7 +44,7 @@
    1.13  AddIffs [list_Fun_NIL_I];
    1.14  
    1.15  Goalw [list_Fun_def,CONS_def]
    1.16 -    "!!M N. [| M: A;  N: X |] ==> CONS M N : list_Fun A X";
    1.17 +    "[| M: A;  N: X |] ==> CONS M N : list_Fun A X";
    1.18  by (Fast_tac 1);
    1.19  qed "list_Fun_CONS_I";
    1.20  Addsimps [list_Fun_CONS_I];
    1.21 @@ -52,7 +52,7 @@
    1.22  
    1.23  (*Utilise the "strong" part, i.e. gfp(f)*)
    1.24  Goalw (llist.defs @ [list_Fun_def])
    1.25 -    "!!M N. M: llist(A) ==> M : list_Fun A (X Un llist(A))";
    1.26 +    "M: llist(A) ==> M : list_Fun A (X Un llist(A))";
    1.27  by (etac (llist.mono RS gfp_fun_UnI2) 1);
    1.28  qed "list_Fun_llist_I";
    1.29  
    1.30 @@ -195,7 +195,7 @@
    1.31  qed "LListD_Fun_mono";
    1.32  
    1.33  Goalw [LListD_Fun_def]
    1.34 -    "!!M. [| M : X;  X <= LListD_Fun r (X Un LListD(r)) |] ==>  M : LListD(r)";
    1.35 +    "[| M : X;  X <= LListD_Fun r (X Un LListD(r)) |] ==>  M : LListD(r)";
    1.36  by (etac LListD.coinduct 1);
    1.37  by (etac (subsetD RS CollectD) 1);
    1.38  by (assume_tac 1);
    1.39 @@ -206,13 +206,13 @@
    1.40  qed "LListD_Fun_NIL_I";
    1.41  
    1.42  Goalw [LListD_Fun_def,CONS_def]
    1.43 - "!!x. [| x:A;  (M,N):s |] ==> (CONS x M, CONS x N) : LListD_Fun (diag A) s";
    1.44 + "[| x:A;  (M,N):s |] ==> (CONS x M, CONS x N) : LListD_Fun (diag A) s";
    1.45  by (Fast_tac 1);
    1.46  qed "LListD_Fun_CONS_I";
    1.47  
    1.48  (*Utilise the "strong" part, i.e. gfp(f)*)
    1.49  Goalw (LListD.defs @ [LListD_Fun_def])
    1.50 -    "!!M N. M: LListD(r) ==> M : LListD_Fun r (X Un LListD(r))";
    1.51 +    "M: LListD(r) ==> M : LListD_Fun r (X Un LListD(r))";
    1.52  by (etac (LListD.mono RS gfp_fun_UnI2) 1);
    1.53  qed "LListD_Fun_LListD_I";
    1.54  
    1.55 @@ -236,7 +236,7 @@
    1.56  qed "LListD_eq_diag";
    1.57  
    1.58  Goal 
    1.59 -    "!!M N. M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
    1.60 +    "M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
    1.61  by (rtac (LListD_eq_diag RS subst) 1);
    1.62  by (rtac LListD_Fun_LListD_I 1);
    1.63  by (asm_simp_tac (simpset() addsimps [LListD_eq_diag, diagI]) 1);
    1.64 @@ -247,7 +247,7 @@
    1.65        [also admits true equality]
    1.66     Replace "A" by some particular set, like {x.True}??? *)
    1.67  Goal 
    1.68 -    "!!r. [| (M,N) : r;  r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
    1.69 +    "[| (M,N) : r;  r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
    1.70  \         |] ==>  M=N";
    1.71  by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
    1.72  by (etac LListD_coinduct 1);
    1.73 @@ -539,7 +539,7 @@
    1.74  
    1.75  (*weak co-induction: bisimulation and case analysis on both variables*)
    1.76  Goal
    1.77 -    "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
    1.78 +    "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
    1.79  by (res_inst_tac
    1.80      [("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
    1.81  by (Fast_tac 1);
    1.82 @@ -552,7 +552,7 @@
    1.83  
    1.84  (*strong co-induction: bisimulation and case analysis on one variable*)
    1.85  Goal
    1.86 -    "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
    1.87 +    "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
    1.88  by (res_inst_tac [("X", "(%u. Lappend u N)``llist(A)")] llist_coinduct 1);
    1.89  by (etac imageI 1);
    1.90  by (rtac image_subsetI 1);
    1.91 @@ -620,7 +620,7 @@
    1.92  (*** Deriving llist_equalityI -- llist equality is a bisimulation ***)
    1.93  
    1.94  Goalw [LListD_Fun_def]
    1.95 -    "!!r A. r <= (llist A) Times (llist A) ==> \
    1.96 +    "r <= (llist A) Times (llist A) ==> \
    1.97  \           LListD_Fun (diag A) r <= (llist A) Times (llist A)";
    1.98  by (stac llist_unfold 1);
    1.99  by (simp_tac (simpset() addsimps [NIL_def, CONS_def]) 1);
   1.100 @@ -654,7 +654,7 @@
   1.101  
   1.102  (*Surprisingly hard to prove.  Used with lfilter*)
   1.103  Goalw [llistD_Fun_def, prod_fun_def]
   1.104 -    "!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
   1.105 +    "A<=B ==> llistD_Fun A <= llistD_Fun B";
   1.106  by Auto_tac;
   1.107  by (rtac image_eqI 1);
   1.108  by (fast_tac (claset() addss (simpset())) 1);
   1.109 @@ -693,7 +693,7 @@
   1.110  
   1.111  (*Utilise the "strong" part, i.e. gfp(f)*)
   1.112  Goalw [llistD_Fun_def]
   1.113 -     "!!l. (l,l) : llistD_Fun(r Un range(%x.(x,x)))";
   1.114 +     "(l,l) : llistD_Fun(r Un range(%x.(x,x)))";
   1.115  by (rtac (Rep_llist_inverse RS subst) 1);
   1.116  by (rtac prod_fun_imageI 1);
   1.117  by (stac image_Un 1);