Adapted to new inductive definition package.
authorberghofe
Tue Jun 30 20:51:15 1998 +0200 (1998-06-30)
changeset 51028c782c25a11e
parent 5101 52e7c75acfe6
child 5103 866a281a8c2a
Adapted to new inductive definition package.
src/HOL/Auth/Message.ML
src/HOL/Auth/Message.thy
src/HOL/IMP/Expr.thy
src/HOL/IMP/Hoare.thy
src/HOL/IMP/Natural.thy
src/HOL/Induct/Acc.thy
src/HOL/Induct/Com.thy
src/HOL/Induct/Comb.thy
src/HOL/Induct/LList.ML
src/HOL/Inductive.thy
src/HOL/Lambda/Lambda.thy
src/HOL/ex/MT.thy
src/HOLCF/IOA/meta_theory/Automata.ML
src/HOLCF/IOA/meta_theory/Automata.thy
src/HOLCF/IOA/meta_theory/Seq.thy
     1.1 --- a/src/HOL/Auth/Message.ML	Tue Jun 30 20:50:34 1998 +0200
     1.2 +++ b/src/HOL/Auth/Message.ML	Tue Jun 30 20:51:15 1998 +0200
     1.3 @@ -443,7 +443,7 @@
     1.4  \              analz (insert (Crypt K X) H) <= \
     1.5  \              insert (Crypt K X) (analz (insert X H))";
     1.6  by (rtac subsetI 1);
     1.7 -by (eres_inst_tac [("za","x")] analz.induct 1);
     1.8 +by (eres_inst_tac [("xa","x")] analz.induct 1);
     1.9  by (ALLGOALS (Blast_tac));
    1.10  val lemma1 = result();
    1.11  
    1.12 @@ -451,7 +451,7 @@
    1.13  \              insert (Crypt K X) (analz (insert X H)) <= \
    1.14  \              analz (insert (Crypt K X) H)";
    1.15  by Auto_tac;
    1.16 -by (eres_inst_tac [("za","x")] analz.induct 1);
    1.17 +by (eres_inst_tac [("xa","x")] analz.induct 1);
    1.18  by Auto_tac;
    1.19  by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1);
    1.20  val lemma2 = result();
     2.1 --- a/src/HOL/Auth/Message.thy	Tue Jun 30 20:50:34 1998 +0200
     2.2 +++ b/src/HOL/Auth/Message.thy	Tue Jun 30 20:51:15 1998 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  Inductive relations "parts", "analz" and "synth"
     2.5  *)
     2.6  
     2.7 -Message = Arith +
     2.8 +Message = Arith + Inductive +
     2.9  
    2.10  (*Is there a difference between a nonce and arbitrary numerical data?
    2.11    Do we need a type of nonces?*)
     3.1 --- a/src/HOL/IMP/Expr.thy	Tue Jun 30 20:50:34 1998 +0200
     3.2 +++ b/src/HOL/IMP/Expr.thy	Tue Jun 30 20:51:15 1998 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  Not used in the rest of the language, but included for completeness.
     3.5  *)
     3.6  
     3.7 -Expr = Arith +
     3.8 +Expr = Arith + Inductive +
     3.9  
    3.10  (** Arithmetic expressions **)
    3.11  types loc
     4.1 --- a/src/HOL/IMP/Hoare.thy	Tue Jun 30 20:50:34 1998 +0200
     4.2 +++ b/src/HOL/IMP/Hoare.thy	Tue Jun 30 20:51:15 1998 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  Inductive definition of Hoare logic
     4.5  *)
     4.6  
     4.7 -Hoare = Denotation + Gfp +
     4.8 +Hoare = Denotation + Inductive +
     4.9  
    4.10  types assn = state => bool
    4.11  
     5.1 --- a/src/HOL/IMP/Natural.thy	Tue Jun 30 20:50:34 1998 +0200
     5.2 +++ b/src/HOL/IMP/Natural.thy	Tue Jun 30 20:51:15 1998 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4  Natural semantics of commands
     5.5  *)
     5.6  
     5.7 -Natural = Com +
     5.8 +Natural = Com + Inductive +
     5.9  
    5.10  (** Execution of commands **)
    5.11  consts  evalc    :: "(com*state*state)set"
     6.1 --- a/src/HOL/Induct/Acc.thy	Tue Jun 30 20:50:34 1998 +0200
     6.2 +++ b/src/HOL/Induct/Acc.thy	Tue Jun 30 20:51:15 1998 +0200
     6.3 @@ -9,7 +9,7 @@
     6.4  Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
     6.5  *)
     6.6  
     6.7 -Acc = WF + 
     6.8 +Acc = WF + Inductive +
     6.9  
    6.10  constdefs
    6.11    pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)
     7.1 --- a/src/HOL/Induct/Com.thy	Tue Jun 30 20:50:34 1998 +0200
     7.2 +++ b/src/HOL/Induct/Com.thy	Tue Jun 30 20:51:15 1998 +0200
     7.3 @@ -6,7 +6,7 @@
     7.4  Example of Mutual Induction via Iteratived Inductive Definitions: Commands
     7.5  *)
     7.6  
     7.7 -Com = Arith +
     7.8 +Com = Arith + Inductive +
     7.9  
    7.10  types loc
    7.11        state = "loc => nat"
     8.1 --- a/src/HOL/Induct/Comb.thy	Tue Jun 30 20:50:34 1998 +0200
     8.2 +++ b/src/HOL/Induct/Comb.thy	Tue Jun 30 20:51:15 1998 +0200
     8.3 @@ -13,7 +13,7 @@
     8.4  *)
     8.5  
     8.6  
     8.7 -Comb = Arith +
     8.8 +Comb = Arith + Inductive +
     8.9  
    8.10  (** Datatype definition of combinators S and K, with infixed application **)
    8.11  datatype comb = K
     9.1 --- a/src/HOL/Induct/LList.ML	Tue Jun 30 20:50:34 1998 +0200
     9.2 +++ b/src/HOL/Induct/LList.ML	Tue Jun 30 20:51:15 1998 +0200
     9.3 @@ -544,8 +544,8 @@
     9.4      [("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
     9.5  by (Fast_tac 1);
     9.6  by Safe_tac;
     9.7 -by (eres_inst_tac [("a", "u")] llist.elim 1);
     9.8 -by (eres_inst_tac [("a", "v")] llist.elim 1);
     9.9 +by (eres_inst_tac [("aa", "u")] llist.elim 1);
    9.10 +by (eres_inst_tac [("aa", "v")] llist.elim 1);
    9.11  by (ALLGOALS Asm_simp_tac);
    9.12  by (Blast_tac 1);
    9.13  qed "Lappend_type";
    9.14 @@ -556,7 +556,7 @@
    9.15  by (res_inst_tac [("X", "(%u. Lappend u N)``llist(A)")] llist_coinduct 1);
    9.16  by (etac imageI 1);
    9.17  by (rtac image_subsetI 1);
    9.18 -by (eres_inst_tac [("a", "x")] llist.elim 1);
    9.19 +by (eres_inst_tac [("aa", "x")] llist.elim 1);
    9.20  by (asm_simp_tac (simpset() addsimps [list_Fun_llist_I]) 1);
    9.21  by (Asm_simp_tac 1);
    9.22  qed "Lappend_type";
    10.1 --- a/src/HOL/Inductive.thy	Tue Jun 30 20:50:34 1998 +0200
    10.2 +++ b/src/HOL/Inductive.thy	Tue Jun 30 20:51:15 1998 +0200
    10.3 @@ -1,3 +1,4 @@
    10.4 -Inductive = Gfp + Prod + Sum + "indrule"
    10.5 +Inductive = Gfp + Prod + Sum +
    10.6  
    10.7 +end
    10.8  
    11.1 --- a/src/HOL/Lambda/Lambda.thy	Tue Jun 30 20:50:34 1998 +0200
    11.2 +++ b/src/HOL/Lambda/Lambda.thy	Tue Jun 30 20:51:15 1998 +0200
    11.3 @@ -7,7 +7,7 @@
    11.4  substitution and beta-reduction.
    11.5  *)
    11.6  
    11.7 -Lambda = Arith +
    11.8 +Lambda = Arith + Inductive +
    11.9  
   11.10  datatype dB = Var nat | "@" dB dB (infixl 200) | Abs dB
   11.11  
    12.1 --- a/src/HOL/ex/MT.thy	Tue Jun 30 20:50:34 1998 +0200
    12.2 +++ b/src/HOL/ex/MT.thy	Tue Jun 30 20:51:15 1998 +0200
    12.3 @@ -13,7 +13,7 @@
    12.4      Report 308, Computer Lab, University of Cambridge (1993).
    12.5  *)
    12.6  
    12.7 -MT = Gfp + Sum + 
    12.8 +MT = Inductive + 
    12.9  
   12.10  types 
   12.11    Const
    13.1 --- a/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Jun 30 20:50:34 1998 +0200
    13.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Jun 30 20:51:15 1998 +0200
    13.3 @@ -242,7 +242,7 @@
    13.4  \  ==> invariant A P";
    13.5  by (rtac allI 1);
    13.6  by (rtac impI 1);
    13.7 -by (res_inst_tac [("za","s")] reachable.induct 1);
    13.8 +by (res_inst_tac [("xa","s")] reachable.induct 1);
    13.9  by (atac 1);
   13.10  by (etac p1 1);
   13.11  by (eres_inst_tac [("s1","sa")] (p2 RS mp) 1);
    14.1 --- a/src/HOLCF/IOA/meta_theory/Automata.thy	Tue Jun 30 20:50:34 1998 +0200
    14.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Tue Jun 30 20:51:15 1998 +0200
    14.3 @@ -7,7 +7,7 @@
    14.4  *)   
    14.5  
    14.6  		       
    14.7 -Automata = Option + Asig +  
    14.8 +Automata = Option + Asig + Inductive +
    14.9  
   14.10  default term
   14.11   
    15.1 --- a/src/HOLCF/IOA/meta_theory/Seq.thy	Tue Jun 30 20:50:34 1998 +0200
    15.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Tue Jun 30 20:51:15 1998 +0200
    15.3 @@ -7,7 +7,7 @@
    15.4  *)  
    15.5  
    15.6  
    15.7 -Seq = HOLCF + 
    15.8 +Seq = HOLCF + Inductive +
    15.9  
   15.10  domain 'a seq = nil | "##" (HD::'a) (lazy TL::'a seq)  (infixr 65) 
   15.11