--- a/src/HOL/AxClasses/Lattice/OrdDefs.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/AxClasses/Lattice/OrdDefs.thy Mon Feb 05 21:29:06 1996 +0100
@@ -23,7 +23,7 @@
(* duals *)
-subtype
+typedef
'a dual = "{x::'a. True}"
instance
--- a/src/HOL/Hoare/Arith2.ML Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Hoare/Arith2.ML Mon Feb 05 21:29:06 1996 +0100
@@ -30,16 +30,16 @@
\ !!x y z. [| P x y z |] ==> P (Suc x) (Suc y) (Suc z) \
\ |] ==> P m n k";
by (res_inst_tac [("x","m")] spec 1);
-by (rtac diff_induct 1);
-by (rtac allI 1);
-by (rtac allI 2);
+br diff_induct 1;
+br allI 1;
+br allI 2;
by (res_inst_tac [("m","xa"),("n","x")] diff_induct 1);
by (res_inst_tac [("m","x"),("n","Suc y")] diff_induct 4);
-by (rtac allI 7);
+br allI 7;
by (nat_ind_tac "xa" 7);
by (ALLGOALS (resolve_tac prems));
-by (assume_tac 1);
-by (assume_tac 1);
+ba 1;
+ba 1;
by (fast_tac HOL_cs 1);
by (fast_tac HOL_cs 1);
qed "diff_induct3";
@@ -48,33 +48,33 @@
val prems=goal Arith.thy "~m<n+k ==> (m - n) - k = m - ((n + k)::nat)";
by (cut_facts_tac prems 1);
-by (rtac mp 1);
-by (assume_tac 2);
+br mp 1;
+ba 2;
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (ALLGOALS Asm_simp_tac);
qed "diff_not_assoc";
val prems=goal Arith.thy "[|~m<n; ~n<k|] ==> (m - n) + k = m - ((n - k)::nat)";
by (cut_facts_tac prems 1);
-by (dtac conjI 1);
-by (assume_tac 1);
+bd conjI 1;
+ba 1;
by (res_inst_tac [("P","~m<n & ~n<k")] mp 1);
-by (assume_tac 2);
+ba 2;
by (res_inst_tac [("m","m"),("n","n"),("k","k")] diff_induct3 1);
by (ALLGOALS Asm_simp_tac);
-by (rtac impI 1);
+br impI 1;
by (dres_inst_tac [("P","~x<y")] conjE 1);
-by (assume_tac 2);
-by (rtac (Suc_diff_n RS sym) 1);
-by (rtac le_less_trans 1);
-by (etac (not_less_eq RS subst) 2);
-by (rtac (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1);
+ba 2;
+br (Suc_diff_n RS sym) 1;
+br le_less_trans 1;
+be (not_less_eq RS subst) 2;
+br (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1;
qed "diff_add_not_assoc";
val prems=goal Arith.thy "~n<k ==> (m + n) - k = m + ((n - k)::nat)";
by (cut_facts_tac prems 1);
-by (rtac mp 1);
-by (assume_tac 2);
+br mp 1;
+ba 2;
by (res_inst_tac [("m","n"),("n","k")] diff_induct 1);
by (ALLGOALS Asm_simp_tac);
qed "add_diff_assoc";
@@ -82,12 +82,12 @@
(*** more ***)
val prems = goal Arith.thy "m~=(n::nat) = (m<n | n<m)";
-by (rtac iffI 1);
+br iffI 1;
by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
by (Asm_full_simp_tac 1);
-by (etac disjE 1);
-by (etac (less_not_refl2 RS not_sym) 1);
-by (etac less_not_refl2 1);
+be disjE 1;
+be (less_not_refl2 RS not_sym) 1;
+be less_not_refl2 1;
qed "not_eq_eq_less_or_gr";
val [prem] = goal Arith.thy "m<n ==> n-m~=0";
@@ -115,7 +115,7 @@
by (res_inst_tac [("n","k")] natE 1);
by (ALLGOALS Asm_full_simp_tac);
by (nat_ind_tac "x" 1);
-by (etac add_less_mono 2);
+be add_less_mono 2;
by (ALLGOALS Asm_full_simp_tac);
qed "mult_less_mono_r";
@@ -124,8 +124,8 @@
by (nat_ind_tac "k" 1);
by (ALLGOALS Simp_tac);
by (fold_goals_tac [le_def]);
-by (etac add_le_mono 1);
-by (assume_tac 1);
+be add_le_mono 1;
+ba 1;
qed "mult_not_less_mono_r";
val prems = goal Arith.thy "m=(n::nat) ==> m*k=n*k";
@@ -137,10 +137,10 @@
val prems = goal Arith.thy "[|0<k; m~=(n::nat)|] ==> m*k~=n*k";
by (cut_facts_tac prems 1);
by (res_inst_tac [("P","m<n"),("Q","n<m")] disjE 1);
-by (rtac (less_not_refl2 RS not_sym) 2);
-by (etac mult_less_mono_r 2);
-by (rtac less_not_refl2 3);
-by (etac mult_less_mono_r 3);
+br (less_not_refl2 RS not_sym) 2;
+be mult_less_mono_r 2;
+br less_not_refl2 3;
+be mult_less_mono_r 3;
by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [not_eq_eq_less_or_gr])));
qed "mult_not_eq_mono_r";
@@ -149,24 +149,29 @@
val prems = goal Arith.thy "(m - n)*k = (m*k) - ((n*k)::nat)";
by (res_inst_tac [("P","m*k<n*k")] case_split_thm 1);
by (forward_tac [mult_not_less_mono_r COMP not_imp_swap] 1);
-by (dtac (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1);
-by (dtac (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1);
-by (rtac mp 2);
-by (assume_tac 3);
+bd (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1;
+bd (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1;
+br mp 2;
+ba 3;
by (res_inst_tac [("m","m"),("n","n")] diff_induct 2);
by (ALLGOALS Asm_simp_tac);
-by (rtac impI 1);
-by (dtac (refl RS iffD1) 1);
+br impI 1;
+bd (refl RS iffD1) 1;
by (dres_inst_tac [("k","k")] add_not_less_mono_l 1);
-by (dtac (refl RS iffD1) 1);
-by (dtac (refl RS iffD1) 1);
-by (dtac diff_not_assoc 1);
+bd (refl RS iffD1) 1;
+bd (refl RS iffD1) 1;
+bd diff_not_assoc 1;
by (asm_full_simp_tac ((simpset_of "Arith") addsimps [diff_add_inverse]) 1);
qed "diff_mult_distrib_r";
(*** mod ***)
+goal Arith.thy "(%m. m mod n) = wfrec (trancl pred_nat) \
+ \ (%f j. if j<n then j else f (j-n))";
+by (simp_tac (HOL_ss addsimps [mod_def]) 1);
+val mod_def = result() RS eq_reflection;
+
(* Alternativ-Beweis zu mod_nn_is_0: Spezialfall zu mod_prod_nn_is_0 *)
(*
val prems = goal thy "0<n ==> n mod n = 0";
@@ -178,29 +183,29 @@
val prems=goal thy "0<n ==> n mod n = 0";
by (cut_facts_tac prems 1);
-by (rtac (mod_def RS wf_less_trans) 1);
+br (mod_def RS wf_less_trans) 1;
by (asm_full_simp_tac ((simpset_of "Arith") addsimps [diff_self_eq_0,cut_def,less_eq]) 1);
-by (etac mod_less 1);
+be mod_less 1;
qed "mod_nn_is_0";
val prems=goal thy "0<n ==> m mod n = (m+n) mod n";
by (cut_facts_tac prems 1);
by (res_inst_tac [("s","n+m"),("t","m+n")] subst 1);
-by (rtac add_commute 1);
+br add_commute 1;
by (res_inst_tac [("s","n+m-n"),("P","%x.x mod n = (n + m) mod n")] subst 1);
-by (rtac diff_add_inverse 1);
-by (rtac sym 1);
-by (etac mod_geq 1);
+br diff_add_inverse 1;
+br sym 1;
+be mod_geq 1;
by (res_inst_tac [("s","n<=n+m"),("t","~n+m<n")] subst 1);
by (simp_tac ((simpset_of "Arith") addsimps [le_def]) 1);
-by (rtac le_add1 1);
+br le_add1 1;
qed "mod_eq_add";
val prems=goal thy "0<n ==> m*n mod n = 0";
by (cut_facts_tac prems 1);
by (nat_ind_tac "m" 1);
by (Simp_tac 1);
-by (etac mod_less 1);
+be mod_less 1;
by (dres_inst_tac [("n","n"),("m","m1*n")] mod_eq_add 1);
by (asm_full_simp_tac ((simpset_of "Arith") addsimps [add_commute]) 1);
qed "mod_prod_nn_is_0";
@@ -208,37 +213,38 @@
val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0|] ==> (m+n) mod x = 0";
by (cut_facts_tac prems 1);
by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1);
-by (etac mod_div_equality 1);
+be mod_div_equality 1;
by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
-by (etac mod_div_equality 1);
+be mod_div_equality 1;
by (Asm_simp_tac 1);
by (res_inst_tac [("s","(m div x + n div x) * x"),("t","m div x * x + n div x * x")] subst 1);
-by (rtac add_mult_distrib 1);
-by (etac mod_prod_nn_is_0 1);
+br add_mult_distrib 1;
+be mod_prod_nn_is_0 1;
qed "mod0_sum";
val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0; n<=m|] ==> (m-n) mod x = 0";
by (cut_facts_tac prems 1);
by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1);
-by (etac mod_div_equality 1);
+be mod_div_equality 1;
by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
-by (etac mod_div_equality 1);
+be mod_div_equality 1;
by (Asm_simp_tac 1);
by (res_inst_tac [("s","(m div x - n div x) * x"),("t","m div x * x - n div x * x")] subst 1);
-by (rtac diff_mult_distrib_r 1);
-by (etac mod_prod_nn_is_0 1);
+br diff_mult_distrib_r 1;
+be mod_prod_nn_is_0 1;
qed "mod0_diff";
(*** div ***)
+
val prems = goal thy "0<n ==> m*n div n = m";
by (cut_facts_tac prems 1);
-by (rtac (mult_not_eq_mono_r RS not_imp_swap) 1);
-by (assume_tac 1);
-by (assume_tac 1);
+br (mult_not_eq_mono_r RS not_imp_swap) 1;
+ba 1;
+ba 1;
by (res_inst_tac [("P","%x.m*n div n * n = x")] (mod_div_equality RS subst) 1);
-by (assume_tac 1);
+ba 1;
by (dres_inst_tac [("m","m")] mod_prod_nn_is_0 1);
by (Asm_simp_tac 1);
qed "div_prod_nn_is_m";
@@ -254,32 +260,32 @@
val prems=goalw thy [divides_def] "x divides n ==> x<=n";
by (cut_facts_tac prems 1);
-by (rtac ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1);
+br ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1;
by (Asm_simp_tac 1);
-by (rtac (less_not_refl2 RS not_sym) 1);
+br (less_not_refl2 RS not_sym) 1;
by (Asm_simp_tac 1);
qed "divides_le";
val prems=goalw thy [divides_def] "[|x divides m; x divides n|] ==> x divides (m+n)";
by (cut_facts_tac prems 1);
by (REPEAT ((dtac conjE 1) THEN (atac 2)));
-by (rtac conjI 1);
+br conjI 1;
by (dres_inst_tac [("m","0"),("n","m")] less_imp_add_less 1);
-by (assume_tac 1);
-by (etac conjI 1);
-by (rtac mod0_sum 1);
+ba 1;
+be conjI 1;
+br mod0_sum 1;
by (ALLGOALS atac);
qed "divides_sum";
val prems=goalw thy [divides_def] "[|x divides m; x divides n; n<m|] ==> x divides (m-n)";
by (cut_facts_tac prems 1);
by (REPEAT ((dtac conjE 1) THEN (atac 2)));
-by (rtac conjI 1);
-by (etac less_imp_diff_positive 1);
-by (etac conjI 1);
-by (rtac mod0_diff 1);
+br conjI 1;
+be less_imp_diff_positive 1;
+be conjI 1;
+br mod0_diff 1;
by (ALLGOALS (asm_simp_tac ((simpset_of "Arith") addsimps [le_def])));
-by (etac less_not_sym 1);
+be less_not_sym 1;
qed "divides_diff";
@@ -288,16 +294,16 @@
val prems=goalw thy [cd_def] "0<n ==> cd n n n";
by (cut_facts_tac prems 1);
-by (dtac divides_nn 1);
+bd divides_nn 1;
by (Asm_simp_tac 1);
qed "cd_nnn";
val prems=goalw thy [cd_def] "cd x m n ==> x<=m & x<=n";
by (cut_facts_tac prems 1);
-by (dtac conjE 1);
-by (assume_tac 2);
-by (dtac divides_le 1);
-by (dtac divides_le 1);
+bd conjE 1;
+ba 2;
+bd divides_le 1;
+bd divides_le 1;
by (Asm_simp_tac 1);
qed "cd_le";
@@ -307,32 +313,32 @@
val prems=goalw thy [cd_def] "n<m ==> cd x m n = cd x (m-n) n";
by (cut_facts_tac prems 1);
-by (rtac iffI 1);
-by (dtac conjE 1);
-by (assume_tac 2);
-by (rtac conjI 1);
-by (rtac divides_diff 1);
-by (dtac conjE 5);
-by (assume_tac 6);
-by (rtac conjI 5);
-by (dtac less_not_sym 5);
-by (dtac add_diff_inverse 5);
+br iffI 1;
+bd conjE 1;
+ba 2;
+br conjI 1;
+br divides_diff 1;
+bd conjE 5;
+ba 6;
+br conjI 5;
+bd less_not_sym 5;
+bd add_diff_inverse 5;
by (dres_inst_tac [("m","n"),("n","m-n")] divides_sum 5);
by (ALLGOALS Asm_full_simp_tac);
qed "cd_diff_l";
val prems=goalw thy [cd_def] "m<n ==> cd x m n = cd x m (n-m)";
by (cut_facts_tac prems 1);
-by (rtac iffI 1);
-by (dtac conjE 1);
-by (assume_tac 2);
-by (rtac conjI 1);
-by (rtac divides_diff 2);
-by (dtac conjE 5);
-by (assume_tac 6);
-by (rtac conjI 5);
-by (dtac less_not_sym 6);
-by (dtac add_diff_inverse 6);
+br iffI 1;
+bd conjE 1;
+ba 2;
+br conjI 1;
+br divides_diff 2;
+bd conjE 5;
+ba 6;
+br conjI 5;
+bd less_not_sym 6;
+bd add_diff_inverse 6;
by (dres_inst_tac [("n","n-m")] divides_sum 6);
by (ALLGOALS Asm_full_simp_tac);
qed "cd_diff_r";
@@ -342,15 +348,15 @@
val prems = goalw thy [gcd_def] "0<n ==> n = gcd n n";
by (cut_facts_tac prems 1);
-by (dtac cd_nnn 1);
-by (rtac (select_equality RS sym) 1);
-by (etac conjI 1);
-by (rtac allI 1);
-by (rtac impI 1);
-by (dtac cd_le 1);
-by (dtac conjE 2);
-by (assume_tac 3);
-by (rtac le_anti_sym 2);
+bd cd_nnn 1;
+br (select_equality RS sym) 1;
+be conjI 1;
+br allI 1;
+br impI 1;
+bd cd_le 1;
+bd conjE 2;
+ba 3;
+br le_anti_sym 2;
by (dres_inst_tac [("x","x")] cd_le 2);
by (dres_inst_tac [("x","n")] spec 3);
by (ALLGOALS Asm_full_simp_tac);
@@ -364,16 +370,16 @@
by (cut_facts_tac prems 1);
by (subgoal_tac "n<m ==> !x.cd x m n = cd x (m-n) n" 1);
by (Asm_simp_tac 1);
-by (rtac allI 1);
-by (etac cd_diff_l 1);
+br allI 1;
+be cd_diff_l 1;
qed "gcd_diff_l";
val prems=goalw thy [gcd_def] "m<n ==> gcd m n = gcd m (n-m)";
by (cut_facts_tac prems 1);
by (subgoal_tac "m<n ==> !x.cd x m n = cd x m (n-m)" 1);
by (Asm_simp_tac 1);
-by (rtac allI 1);
-by (etac cd_diff_r 1);
+br allI 1;
+be cd_diff_r 1;
qed "gcd_diff_r";
@@ -392,7 +398,7 @@
by (nat_ind_tac "k" 1);
by (ALLGOALS Asm_simp_tac);
by (fold_goals_tac [pow_def]);
-by (rtac (pow_add_reduce RS sym) 1);
+br (pow_add_reduce RS sym) 1;
qed "pow_pow_reduce";
(*** fac ***)
--- a/src/HOL/Hoare/Arith2.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Hoare/Arith2.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/Hoare/Arith2.thy
+(* Title: HOL/Hoare/Arith2.thy
ID: $Id$
- Author: Norbert Galm
+ Author: Norbert Galm
Copyright 1995 TUM
More arithmetic.
@@ -9,19 +9,19 @@
Arith2 = Arith +
consts
- divides :: [nat, nat] => bool (infixl 70)
- cd :: [nat, nat, nat] => bool
- gcd :: [nat, nat] => nat
+ divides :: [nat, nat] => bool (infixl 70)
+ cd :: [nat, nat, nat] => bool
+ gcd :: [nat, nat] => nat
- pow :: [nat, nat] => nat (infixl 75)
- fac :: nat => nat
+ pow :: [nat, nat] => nat (infixl 75)
+ fac :: nat => nat
defs
- divides_def "x divides n == 0<n & 0<x & (n mod x) = 0"
- cd_def "cd x m n == x divides m & x divides n"
- gcd_def "gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
+ divides_def "x divides n == 0<n & 0<x & (n mod x) = 0"
+ cd_def "cd x m n == x divides m & x divides n"
+ gcd_def "gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
- pow_def "m pow n == nat_rec n (Suc 0) (%u v.m*v)"
- fac_def "fac m == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
+ pow_def "m pow n == nat_rec n (Suc 0) (%u v.m*v)"
+ fac_def "fac m == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
end
--- a/src/HOL/Hoare/Examples.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Hoare/Examples.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/Hoare/Examples.thy
+(* Title: HOL/Hoare/Examples.thy
ID: $Id$
- Author: Norbert Galm
+ Author: Norbert Galm
Copyright 1995 TUM
Various arithmetic examples.
@@ -9,8 +9,8 @@
Examples = Hoare + Arith2 +
syntax
- "@1" :: nat ("1")
- "@2" :: nat ("2")
+ "@1" :: nat ("1")
+ "@2" :: nat ("2")
translations
"1" == "Suc(0)"
--- a/src/HOL/Hoare/Hoare.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Hoare/Hoare.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/Hoare/Hoare.thy
+(* Title: HOL/Hoare/Hoare.thy
ID: $Id$
- Author: Norbert Galm & Tobias Nipkow
+ Author: Norbert Galm & Tobias Nipkow
Copyright 1995 TUM
Sugared semantic embedding of Hoare logic.
@@ -9,49 +9,49 @@
Hoare = Arith +
types
- 'a prog (* program syntax *)
- pvar = nat (* encoding of program variables ( < 26! ) *)
- 'a state = pvar => 'a (* program state *)
- 'a exp = 'a state => 'a (* denotation of expressions *)
- 'a bexp = 'a state => bool (* denotation of boolean expressions *)
+ 'a prog (* program syntax *)
+ pvar = nat (* encoding of program variables ( < 26! ) *)
+ 'a state = pvar => 'a (* program state *)
+ 'a exp = 'a state => 'a (* denotation of expressions *)
+ 'a bexp = 'a state => bool (* denotation of boolean expressions *)
'a com = 'a state => 'a state => bool (* denotation of programs *)
syntax
- "@Skip" :: 'a prog ("SKIP")
- "@Assign" :: [id, 'a] => 'a prog ("_ := _")
- "@Seq" :: ['a prog, 'a prog] => 'a prog ("_;//_" [0,1000] 999)
- "@If" :: [bool, 'a prog, 'a prog] => 'a prog
+ "@Skip" :: 'a prog ("SKIP")
+ "@Assign" :: [id, 'a] => 'a prog ("_ := _")
+ "@Seq" :: ['a prog, 'a prog] => 'a prog ("_;//_" [0,1000] 999)
+ "@If" :: [bool, 'a prog, 'a prog] => 'a prog
("IF _//THEN// (_)//ELSE// (_)//END")
- "@While" :: [bool, bool, 'a prog] => 'a prog
+ "@While" :: [bool, bool, 'a prog] => 'a prog
("WHILE _//DO {_}// (_)//END")
- "@Spec" :: [bool, 'a prog, bool] => bool ("{_}//_//{_}")
+ "@Spec" :: [bool, 'a prog, bool] => bool ("{_}//_//{_}")
consts
(* semantics *)
- Skip :: 'a com
- Assign :: [pvar, 'a exp] => 'a com
- Seq :: ['a com, 'a com] => 'a com
- Cond :: ['a bexp, 'a com, 'a com] => 'a com
- While :: ['a bexp, 'a bexp, 'a com] => 'a com
- Iter :: [nat, 'a bexp, 'a com] => 'a com
+ Skip :: 'a com
+ Assign :: [pvar, 'a exp] => 'a com
+ Seq :: ['a com, 'a com] => 'a com
+ Cond :: ['a bexp, 'a com, 'a com] => 'a com
+ While :: ['a bexp, 'a bexp, 'a com] => 'a com
+ Iter :: [nat, 'a bexp, 'a com] => 'a com
- Spec :: ['a bexp, 'a com, 'a bexp] => bool
+ Spec :: ['a bexp, 'a com, 'a bexp] => bool
defs
(* denotational semantics *)
- SkipDef "Skip s s' == (s=s')"
- AssignDef "Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
- SeqDef "Seq c c' s s' == ? s''. c s s'' & c' s'' s'"
- CondDef "Cond b c c' s s' == (b(s) --> c s s') & (~b s --> c' s s')"
- WhileDef "While b inv c s s' == ? n. Iter n b c s s'"
+ SkipDef "Skip s s' == (s=s')"
+ AssignDef "Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
+ SeqDef "Seq c c' s s' == ? s''. c s s'' & c' s'' s'"
+ CondDef "Cond b c c' s s' == (b(s) --> c s s') & (~b s --> c' s s')"
+ WhileDef "While b inv c s s' == ? n. Iter n b c s s'"
- IterDef "Iter n b c == nat_rec n (%s s'.~b(s) & (s=s'))
- (%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s')"
+ IterDef "Iter n b c == nat_rec n (%s s'.~b(s) & (s=s'))
+ (%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s')"
- SpecDef "Spec p c q == !s s'. c s s' --> p s --> q s'"
+ SpecDef "Spec p c q == !s s'. c s s' --> p s --> q s'"
end
@@ -63,53 +63,53 @@
(* name_in_term:bool (name:string,trm:term) bestimmt, ob in trm der Name name als Konstante,
freie Var., scheme-Variable oder als Name fuer eine Lambda-Abstraktion vorkommt *)
-fun name_in_term (name,Const (s,t)) =(name=s)
- | name_in_term (name,Free (s,t)) =(name=s)
- | name_in_term (name,Var ((s,i),t)) =(name=s ^ makestring i)
- | name_in_term (name,Abs (s,t,trm)) =(name=s) orelse (name_in_term (name,trm))
- | name_in_term (name,trm1 $ trm2) =(name_in_term (name,trm1)) orelse (name_in_term (name,trm2))
- | name_in_term (_,_) =false;
+fun name_in_term (name,Const (s,t)) =(name=s)
+ | name_in_term (name,Free (s,t)) =(name=s)
+ | name_in_term (name,Var ((s,i),t)) =(name=s ^ makestring i)
+ | name_in_term (name,Abs (s,t,trm)) =(name=s) orelse (name_in_term (name,trm))
+ | name_in_term (name,trm1 $ trm2) =(name_in_term (name,trm1)) orelse (name_in_term (name,trm2))
+ | name_in_term (_,_) =false;
(* variant_name:string (name:string,trm:term) liefert einen von name abgewandelten Namen (durch Anhaengen
von genuegend vielen "_"), der nicht in trm vorkommt. Im Gegensatz zu variant_abs beruecktsichtigt es
auch Namen von scheme-Variablen und von Lambda-Abstraktionen in trm *)
-fun variant_name (name,trm) =if name_in_term (name,trm)
- then variant_name (name ^ "_",trm)
- else name;
+fun variant_name (name,trm) =if name_in_term (name,trm)
+ then variant_name (name ^ "_",trm)
+ else name;
(* subst_term:term (von:term,nach:term,trm:term) liefert den Term, der aus
trm entsteht, wenn alle Teilterme, die gleich von sind, durch nach ersetzt
wurden *)
-fun subst_term (von,nach,Abs (s,t,trm)) =if von=Abs (s,t,trm)
- then nach
- else Abs (s,t,subst_term (von,nach,trm))
- | subst_term (von,nach,trm1 $ trm2) =if von=trm1 $ trm2
- then nach
- else subst_term (von,nach,trm1) $ subst_term (von,nach,trm2)
- | subst_term (von,nach,trm) =if von=trm
- then nach
- else trm;
+fun subst_term (von,nach,Abs (s,t,trm)) =if von=Abs (s,t,trm)
+ then nach
+ else Abs (s,t,subst_term (von,nach,trm))
+ | subst_term (von,nach,trm1 $ trm2) =if von=trm1 $ trm2
+ then nach
+ else subst_term (von,nach,trm1) $ subst_term (von,nach,trm2)
+ | subst_term (von,nach,trm) =if von=trm
+ then nach
+ else trm;
(* Translation between program vars ("a" - "z") and their encoding as
natural numbers: "a" <==> 0, "b" <==> Suc(0), ..., "z" <==> 25 *)
-fun is_pvarID s = size s=1 andalso "a"<=s andalso s<="z";
+fun is_pvarID s = size s=1 andalso "a"<=s andalso s<="z";
fun pvarID2pvar s =
let fun rest2pvar (i,arg) =
if i=0 then arg else rest2pvar(i-1, Syntax.const "Suc" $ arg)
in rest2pvar(ord s - ord "a", Syntax.const "0") end;
-fun pvar2pvarID trm =
- let
- fun rest2pvarID (Const("0",_),i) =chr (i + ord "a")
- | rest2pvarID (Const("Suc",_) $ trm,i) =rest2pvarID (trm,i+1)
- in
- rest2pvarID (trm,0)
- end;
+fun pvar2pvarID trm =
+ let
+ fun rest2pvarID (Const("0",_),i) =chr (i + ord "a")
+ | rest2pvarID (Const("Suc",_) $ trm,i) =rest2pvarID (trm,i+1)
+ in
+ rest2pvarID (trm,0)
+ end;
(*** parse translations: syntax -> semantics ***)
@@ -119,10 +119,10 @@
bei name="s" und dem Term "a=b & a=X" wird der Term "s(0)=s(Suc(0)) & s(0)=X" geliefert *)
fun term_tr (name,Free (s,t)) = if is_pvarID s
- then Syntax.free name $ pvarID2pvar s
- else Free (s,t)
+ then Syntax.free name $ pvarID2pvar s
+ else Free (s,t)
| term_tr (name,Abs (s,t,trm)) = Abs (s,t,term_tr (name,trm))
- | term_tr (name,trm1 $ trm2) = term_tr (name,trm1) $ term_tr (name,trm2)
+ | term_tr (name,trm1 $ trm2) = term_tr (name,trm1) $ term_tr (name,trm2)
| term_tr (name,trm) = trm;
fun bool_tr B =
@@ -133,12 +133,12 @@
let val name = variant_name("s",E)
in Abs (name,dummyT,abstract_over (Syntax.free name,term_tr (name,E))) end;
-fun prog_tr (Const ("@Skip",_)) = Syntax.const "Skip"
+fun prog_tr (Const ("@Skip",_)) = Syntax.const "Skip"
| prog_tr (Const ("@Assign",_) $ Free (V,_) $ E) =
if is_pvarID V
then Syntax.const "Assign" $ pvarID2pvar V $ exp_tr E
else error("Not a valid program variable: " ^ quote V)
- | prog_tr (Const ("@Seq",_) $ C $ C') =
+ | prog_tr (Const ("@Seq",_) $ C $ C') =
Syntax.const "Seq" $ prog_tr C $ prog_tr C'
| prog_tr (Const ("@If",_) $ B $ C $ C') =
Syntax.const "Cond" $ bool_tr B $ prog_tr C $ prog_tr C'
@@ -154,25 +154,25 @@
(* term_tr':term (name:string,trm:term) ersetzt in trm alle Vorkommen von name $ pvar durch
entsprechende freie Variablen, welche die pvarID zu pvar darstellen. Beispiel:
- bei name="s" und dem Term "s(0)=s(Suc(0)) & s(0)=X" wird der Term "a=b & a=X" geliefert *)
+ bei name="s" und dem Term "s(0)=s(Suc(0)) & s(0)=X" wird der Term "a=b & a=X" geliefert *)
-fun term_tr' (name,Free (s,t) $ trm) =if name=s
- then Syntax.free (pvar2pvarID trm)
- else Free (s,t) $ term_tr' (name,trm)
- | term_tr' (name,Abs (s,t,trm)) =Abs (s,t,term_tr' (name,trm))
- | term_tr' (name,trm1 $ trm2) =term_tr' (name,trm1) $ term_tr' (name,trm2)
- | term_tr' (name,trm) =trm;
+fun term_tr' (name,Free (s,t) $ trm) =if name=s
+ then Syntax.free (pvar2pvarID trm)
+ else Free (s,t) $ term_tr' (name,trm)
+ | term_tr' (name,Abs (s,t,trm)) =Abs (s,t,term_tr' (name,trm))
+ | term_tr' (name,trm1 $ trm2) =term_tr' (name,trm1) $ term_tr' (name,trm2)
+ | term_tr' (name,trm) =trm;
-fun bexp_tr' (Abs(_,_,b)) =term_tr' (variant_abs ("s",dummyT,b));
+fun bexp_tr' (Abs(_,_,b)) =term_tr' (variant_abs ("s",dummyT,b));
-fun exp_tr' (Abs(_,_,e)) =term_tr' (variant_abs ("s",dummyT,e));
+fun exp_tr' (Abs(_,_,e)) =term_tr' (variant_abs ("s",dummyT,e));
-fun com_tr' (Const ("Skip",_)) =Syntax.const "@Skip"
- | com_tr' (Const ("Assign",_) $ v $ e) =Syntax.const "@Assign" $ Syntax.free (pvar2pvarID v) $ exp_tr' e
- | com_tr' (Const ("Seq",_) $ c $ c') =Syntax.const "@Seq" $ com_tr' c $ com_tr' c'
- | com_tr' (Const ("Cond",_) $ b $ c $ c') =Syntax.const "@If" $ bexp_tr' b $ com_tr' c $ com_tr' c'
- | com_tr' (Const ("While",_) $ b $ inv $ c) =Syntax.const "@While" $ bexp_tr' b $ bexp_tr' inv $ com_tr' c;
+fun com_tr' (Const ("Skip",_)) =Syntax.const "@Skip"
+ | com_tr' (Const ("Assign",_) $ v $ e) =Syntax.const "@Assign" $ Syntax.free (pvar2pvarID v) $ exp_tr' e
+ | com_tr' (Const ("Seq",_) $ c $ c') =Syntax.const "@Seq" $ com_tr' c $ com_tr' c'
+ | com_tr' (Const ("Cond",_) $ b $ c $ c') =Syntax.const "@If" $ bexp_tr' b $ com_tr' c $ com_tr' c'
+ | com_tr' (Const ("While",_) $ b $ inv $ c) =Syntax.const "@While" $ bexp_tr' b $ bexp_tr' inv $ com_tr' c;
-fun spec_tr' [p,c,q] =Syntax.const "@Spec" $ bexp_tr' p $ com_tr' c $ bexp_tr' q;
+fun spec_tr' [p,c,q] =Syntax.const "@Spec" $ bexp_tr' p $ com_tr' c $ bexp_tr' q;
-val print_translation =[("Spec",spec_tr')];
+val print_translation =[("Spec",spec_tr')];
--- a/src/HOL/IMP/Com.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IMP/Com.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/IMP/Com.thy
+(* Title: HOL/IMP/Com.thy
ID: $Id$
- Author: Heiko Loetzbeyer & Robert Sandner, TUM
+ Author: Heiko Loetzbeyer & Robert Sandner, TUM
Copyright 1994 TUM
Arithmetic expressions, Boolean expressions, Commands
@@ -32,7 +32,7 @@
inductive "evala"
intrs
N "<N(n),s> -a-> n"
- X "<X(x),s> -a-> s(x)"
+ X "<X(x),s> -a-> s(x)"
Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)"
Op2 "[| <e0,s> -a-> n0; <e1,s> -a-> n1 |]
==> <Op2 f e0 e1,s> -a-> f n0 n1"
@@ -46,11 +46,11 @@
| false
| ROp n2n2b aexp aexp
| noti bexp
- | andi bexp bexp (infixl 60)
- | ori bexp bexp (infixl 60)
+ | andi bexp bexp (infixl 60)
+ | ori bexp bexp (infixl 60)
(** Evaluation of boolean expressions **)
-consts evalb :: "(bexp*state*bool)set"
+consts evalb :: "(bexp*state*bool)set"
"@evalb" :: [bexp,state,bool] => bool ("<_,_>/ -b-> _" [0,0,50] 50)
translations
@@ -61,32 +61,32 @@
tru "<true,s> -b-> True"
fls "<false,s> -b-> False"
ROp "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |]
- ==> <ROp f a0 a1,s> -b-> f n0 n1"
+ ==> <ROp f a0 a1,s> -b-> f n0 n1"
noti "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)"
andi "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |]
==> <b0 andi b1,s> -b-> (w0 & w1)"
ori "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |]
- ==> <b0 ori b1,s> -b-> (w0 | w1)"
+ ==> <b0 ori b1,s> -b-> (w0 | w1)"
(** Commands **)
datatype
com = skip
- | ":=" loc aexp (infixl 60)
- | semic com com ("_; _" [60, 60] 10)
- | whileC bexp com ("while _ do _" 60)
- | ifC bexp com com ("ifc _ then _ else _" 60)
+ | ":=" loc aexp (infixl 60)
+ | semic com com ("_; _" [60, 60] 10)
+ | whileC bexp com ("while _ do _" 60)
+ | ifC bexp com com ("ifc _ then _ else _" 60)
(** Execution of commands **)
consts evalc :: "(com*state*state)set"
"@evalc" :: [com,state,state] => bool ("<_,_>/ -c-> _" [0,0,50] 50)
- "assign" :: [state,nat,loc] => state ("_[_'/_]" [95,0,0] 95)
+ "assign" :: [state,nat,loc] => state ("_[_'/_]" [95,0,0] 95)
translations
"<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
rules
- assign_def "s[m/x] == (%y. if y=x then m else s y)"
+ assign_def "s[m/x] == (%y. if y=x then m else s y)"
inductive "evalc"
intrs
--- a/src/HOL/IMP/Denotation.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IMP/Denotation.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/IMP/Denotation.thy
+(* Title: HOL/IMP/Denotation.thy
ID: $Id$
- Author: Heiko Loetzbeyer & Robert Sandner, TUM
+ Author: Heiko Loetzbeyer & Robert Sandner, TUM
Copyright 1994 TUM
Denotational semantics of expressions & commands
@@ -16,31 +16,31 @@
Gamma :: [bexp,com_den] => (com_den => com_den)
primrec A aexp
- A_nat "A(N(n)) = (%s. n)"
- A_loc "A(X(x)) = (%s. s(x))"
- A_op1 "A(Op1 f a) = (%s. f(A a s))"
- A_op2 "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
+ A_nat "A(N(n)) = (%s. n)"
+ A_loc "A(X(x)) = (%s. s(x))"
+ A_op1 "A(Op1 f a) = (%s. f(A a s))"
+ A_op2 "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
primrec B bexp
B_true "B(true) = (%s. True)"
B_false "B(false) = (%s. False)"
- B_op "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
- B_not "B(noti(b)) = (%s. ~(B b s))"
- B_and "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
- B_or "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
+ B_op "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))"
+ B_not "B(noti(b)) = (%s. ~(B b s))"
+ B_and "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
+ B_or "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
defs
- Gamma_def "Gamma b cd ==
- (%phi.{st. st : (phi O cd) & B b (fst st)} Un
- {st. st : id & ~B b (fst st)})"
+ Gamma_def "Gamma b cd ==
+ (%phi.{st. st : (phi O cd) & B b (fst st)} Un
+ {st. st : id & ~B b (fst st)})"
primrec C com
C_skip "C(skip) = id"
C_assign "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
C_comp "C(c0 ; c1) = C(c1) O C(c0)"
- C_if "C(ifc b then c0 else c1) =
- {st. st:C(c0) & (B b (fst st))} Un
- {st. st:C(c1) & ~(B b (fst st))}"
+ C_if "C(ifc b then c0 else c1) =
+ {st. st:C(c0) & (B b (fst st))} Un
+ {st. st:C(c1) & ~(B b (fst st))}"
C_while "C(while b do c) = lfp (Gamma b (C c))"
end
--- a/src/HOL/IMP/Equiv.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IMP/Equiv.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/IMP/Equiv.thy
+(* Title: HOL/IMP/Equiv.thy
ID: $Id$
- Author: Heiko Loetzbeyer & Robert Sandner, TUM
+ Author: Heiko Loetzbeyer & Robert Sandner, TUM
Copyright 1994 TUM
*)
--- a/src/HOL/IMP/Hoare.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IMP/Hoare.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/IMP/Hoare.thy
+(* Title: HOL/IMP/Hoare.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1995 TUM
Inductive definition of Hoare logic
@@ -27,8 +27,8 @@
hoare_if "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==>
{{P}} ifc b then c else d {{Q}}"
hoare_while "[| {{%s. P s & B b s}} c {{P}} |] ==>
- {{P}} while b do c {{%s. P s & ~B b s}}"
+ {{P}} while b do c {{%s. P s & ~B b s}}"
hoare_conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==>
- {{P'}}c{{Q'}}"
+ {{P'}}c{{Q'}}"
end
--- a/src/HOL/IMP/VC.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IMP/VC.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/IMP/VC.thy
+(* Title: HOL/IMP/VC.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1996 TUM
acom: annotated commands
--- a/src/HOL/IOA/ABP/Abschannel.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IOA/ABP/Abschannel.thy Mon Feb 05 21:29:06 1996 +0100
@@ -56,8 +56,8 @@
case fst(snd(tr))
of S(b) => ((t = s) | (t = s @ [b])) |
R(b) => s ~= [] &
- b = hd(s) &
- ((t = s) | (t = tl(s))) }"
+ b = hd(s) &
+ ((t = s) | (t = tl(s))) }"
ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)"
@@ -66,24 +66,24 @@
*********************************************************)
rsch_actions_def "rsch_actions (akt) ==
- case akt of
+ case akt of
Next => None |
S_msg(m) => None |
- R_msg(m) => None |
+ R_msg(m) => None |
S_pkt(packet) => None |
- R_pkt(packet) => None |
- S_ack(b) => Some(S(b)) |
- R_ack(b) => Some(R(b))"
+ R_pkt(packet) => None |
+ S_ack(b) => Some(S(b)) |
+ R_ack(b) => Some(R(b))"
srch_actions_def "srch_actions (akt) ==
- case akt of
- Next => None |
+ case akt of
+ Next => None |
S_msg(m) => None |
- R_msg(m) => None |
+ R_msg(m) => None |
S_pkt(p) => Some(S(p)) |
- R_pkt(p) => Some(R(p)) |
- S_ack(b) => None |
- R_ack(b) => None"
+ R_pkt(p) => Some(R(p)) |
+ S_ack(b) => None |
+ R_ack(b) => None"
end
--- a/src/HOL/IOA/ABP/Abschannel_finite.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IOA/ABP/Abschannel_finite.thy Mon Feb 05 21:29:06 1996 +0100
@@ -54,8 +54,8 @@
of S(b) => ((t = s) |
(if (b=hd(reverse(s)) & s~=[]) then t=s else t=s@[b])) |
R(b) => s ~= [] &
- b = hd(s) &
- ((t = s) | (t = tl(s))) }"
+ b = hd(s) &
+ ((t = s) | (t = tl(s))) }"
ch_fin_ioa_def "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans)"
--- a/src/HOL/IOA/ABP/Correctness.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IOA/ABP/Correctness.thy Mon Feb 05 21:29:06 1996 +0100
@@ -20,11 +20,11 @@
reduce List.list
reduce_Nil "reduce [] = []"
reduce_Cons "reduce(x#xs) =
- (case xs of
- [] => [x]
- | y#ys => (if (x=y)
- then reduce xs
- else (x#(reduce xs))))"
+ (case xs of
+ [] => [x]
+ | y#ys => (if (x=y)
+ then reduce xs
+ else (x#(reduce xs))))"
defs
@@ -36,8 +36,8 @@
"system_fin_ioa == (env_ioa || impl_fin_ioa)"
abs_def "abs ==
- (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),
- (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
+ (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),
+ (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
rules
--- a/src/HOL/IOA/ABP/Receiver.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IOA/ABP/Receiver.thy Mon Feb 05 21:29:06 1996 +0100
@@ -41,13 +41,13 @@
Next => False |
S_msg(m) => False |
R_msg(m) => (rq(s) ~= []) &
- m = hd(rq(s)) &
- rq(t) = tl(rq(s)) &
+ m = hd(rq(s)) &
+ rq(t) = tl(rq(s)) &
rbit(t)=rbit(s) |
S_pkt(pkt) => False |
R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then
- rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else
- rq(t) =rq(s) & rbit(t)=rbit(s) |
+ rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else
+ rq(t) =rq(s) & rbit(t)=rbit(s) |
S_ack(b) => b = rbit(s) &
rq(t) = rq(s) &
rbit(t)=rbit(s) |
--- a/src/HOL/IOA/ABP/Sender.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IOA/ABP/Sender.thy Mon Feb 05 21:29:06 1996 +0100
@@ -41,15 +41,15 @@
sbit(t)=sbit(s) |
R_msg(m) => False |
S_pkt(pkt) => sq(s) ~= [] &
- hdr(pkt) = sbit(s) &
+ hdr(pkt) = sbit(s) &
msg(pkt) = hd(sq(s)) &
sq(t) = sq(s) &
sbit(t) = sbit(s) |
R_pkt(pkt) => False |
S_ack(b) => False |
R_ack(b) => if b = sbit(s) then
- sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else
- sq(t)=sq(s) & sbit(t)=sbit(s)}"
+ sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else
+ sq(t)=sq(s) & sbit(t)=sbit(s)}"
sender_ioa_def "sender_ioa ==
(sender_asig, {([],True)}, sender_trans)"
--- a/src/HOL/IOA/NTP/Abschannel.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IOA/NTP/Abschannel.thy Mon Feb 05 21:29:06 1996 +0100
@@ -57,26 +57,26 @@
rsch_actions_def "rsch_actions (act) ==
- case act of
+ case act of
S_msg(m) => None |
- R_msg(m) => None |
+ R_msg(m) => None |
S_pkt(packet) => None |
- R_pkt(packet) => None |
- S_ack(b) => Some(S(b)) |
- R_ack(b) => Some(R(b)) |
+ R_pkt(packet) => None |
+ S_ack(b) => Some(S(b)) |
+ R_ack(b) => Some(R(b)) |
C_m_s => None |
C_m_r => None |
C_r_s => None |
C_r_r(m) => None"
srch_actions_def "srch_actions (act) ==
- case act of
+ case act of
S_msg(m) => None |
- R_msg(m) => None |
+ R_msg(m) => None |
S_pkt(p) => Some(S(p)) |
- R_pkt(p) => Some(R(p)) |
- S_ack(b) => None |
- R_ack(b) => None |
+ R_pkt(p) => Some(R(p)) |
+ S_ack(b) => None |
+ R_ack(b) => None |
C_m_s => None |
C_m_r => None |
C_r_s => None |
--- a/src/HOL/IOA/meta_theory/IOA.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IOA/meta_theory/IOA.thy Mon Feb 05 21:29:06 1996 +0100
@@ -22,7 +22,7 @@
asig_of ::"('action,'state)ioa => 'action signature"
starts_of ::"('action,'state)ioa => 'state set"
trans_of ::"('action,'state)ioa => ('action,'state)transition set"
- IOA ::"('action,'state)ioa => bool"
+ IOA ::"('action,'state)ioa => bool"
(* Executions, schedules, and traces *)
--- a/src/HOL/Integ/Equiv.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Integ/Equiv.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,7 +1,7 @@
-(* Title: Equiv.thy
+(* Title: Equiv.thy
ID: $Id$
- Authors: Riccardo Mattolini, Dip. Sistemi e Informatica
- Lawrence C Paulson, Cambridge University Computer Laboratory
+ Authors: Riccardo Mattolini, Dip. Sistemi e Informatica
+ Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 Universita' di Firenze
Copyright 1993 University of Cambridge
@@ -10,11 +10,11 @@
Equiv = Relation +
consts
- refl,equiv :: "['a set,('a*'a) set]=>bool"
+ refl,equiv :: "['a set,('a*'a) set]=>bool"
sym :: "('a*'a) set=>bool"
"'/" :: "['a set,('a*'a) set]=>'a set set" (infixl 90)
(*set of equiv classes*)
- congruent :: "[('a*'a) set,'a=>'b]=>bool"
+ congruent :: "[('a*'a) set,'a=>'b]=>bool"
congruent2 :: "[('a*'a) set,['a,'a]=>'b]=>bool"
defs
--- a/src/HOL/Integ/Integ.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Integ/Integ.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,7 +1,7 @@
-(* Title: Integ.thy
+(* Title: Integ.thy
ID: $Id$
- Authors: Riccardo Mattolini, Dip. Sistemi e Informatica
- Lawrence C Paulson, Cambridge University Computer Laboratory
+ Authors: Riccardo Mattolini, Dip. Sistemi e Informatica
+ Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 Universita' di Firenze
Copyright 1993 University of Cambridge
@@ -16,16 +16,16 @@
intrel_def
"intrel == {p. ? x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
-subtype (Integ)
- int = "{x::(nat*nat).True}/intrel" (Equiv.quotient_def)
+typedef (Integ)
+ int = "{x::(nat*nat).True}/intrel" (Equiv.quotient_def)
instance
int :: {ord, plus, times, minus}
consts
zNat :: nat set
- znat :: nat => int ("$# _" [80] 80)
- zminus :: int => int ("$~ _" [80] 80)
+ znat :: nat => int ("$# _" [80] 80)
+ zminus :: int => int ("$~ _" [80] 80)
znegative :: int => bool
zmagnitude :: int => int
zdiv,zmod :: [int,int]=>int (infixl 70)
@@ -37,7 +37,7 @@
znat_def "$# m == Abs_Integ(intrel ^^ {(m,0)})"
zminus_def
- "$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)"
+ "$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)"
znegative_def
"znegative(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
--- a/src/HOL/Lambda/Commutation.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Lambda/Commutation.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/Lambda/Commutation.thy
+(* Title: HOL/Lambda/Commutation.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1995 TU Muenchen
Abstract commutation and confluence notions.
--- a/src/HOL/Lex/Auto.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Lex/Auto.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/Lex/Auto.thy
+(* Title: HOL/Lex/Auto.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1995 TUM
Automata expressed as triples of
--- a/src/HOL/Lex/AutoChopper.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Lex/AutoChopper.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/Lex/AutoChopper.thy
+(* Title: HOL/Lex/AutoChopper.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1995 TUM
auto_chopper turns an automaton into a chopper. Tricky, because primrec.
@@ -20,19 +20,19 @@
is_auto_chopper :: (('a,'b)auto => 'a chopper) => bool
auto_chopper :: ('a,'b)auto => 'a chopper
acc :: "['a list, 'b, 'a list, 'a list, 'a list list*'a list, ('a,'b)auto]
- => 'a list list * 'a list"
+ => 'a list list * 'a list"
defs
is_auto_chopper_def "is_auto_chopper(chopperf) ==
- !A. is_longest_prefix_chopper(accepts A)(chopperf A)"
+ !A. is_longest_prefix_chopper(accepts A)(chopperf A)"
auto_chopper_def "auto_chopper A xs == acc xs (start A) [] [] ([],xs) A"
primrec acc List.list
acc_Nil "acc [] st ys zs chopsr A =
- (if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))"
+ (if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))"
acc_Cons "acc(x#xs) st ys zs chopsr A =
- (let s0 = start(A); nxt = next(A); fin = fin(A)
+ (let s0 = start(A); nxt = next(A); fin = fin(A)
in if fin(nxt st x)
then acc xs (nxt st x) (zs@[x]) (zs@[x])
(acc xs s0 [] [] ([],xs) A) A
--- a/src/HOL/Lex/Chopper.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Lex/Chopper.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/Lex/Chopper.thy
+(* Title: HOL/Lex/Chopper.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1995 TUM
A 'chopper' is a function which returns
@@ -25,10 +25,10 @@
defs
is_longest_prefix_chopper_def
"is_longest_prefix_chopper L chopper == !xs. \
-\ (!zs. chopper(xs) = ([],zs) --> \
-\ zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) & \
-\ (!ys yss zs. chopper(xs) = (ys#yss,zs) --> \
-\ ys ~= [] & L(ys) & xs=ys@flat(yss)@zs & \
+\ (!zs. chopper(xs) = ([],zs) --> \
+\ zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) & \
+\ (!ys yss zs. chopper(xs) = (ys#yss,zs) --> \
+\ ys ~= [] & L(ys) & xs=ys@flat(yss)@zs & \
\ chopper(flat(yss)@zs) = (yss,zs) & \
\ (!as. as <= xs & ys <= as & ys ~= as --> ~L(as)))"
end
--- a/src/HOL/Lex/Prefix.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Lex/Prefix.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/Lex/Prefix.thy
+(* Title: HOL/Lex/Prefix.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1995 TUM
*)
@@ -9,5 +9,5 @@
arities list :: (term)ord
defs
- prefix_def "xs <= zs == ? ys. zs = xs@ys"
+ prefix_def "xs <= zs == ? ys. zs = xs@ys"
end
--- a/src/HOL/MiniML/I.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/MiniML/I.thy Mon Feb 05 21:29:06 1996 +0100
@@ -8,16 +8,16 @@
I = W +
consts
- I :: [expr, typ list, nat, subst] => result_W
+ I :: [expr, typ list, nat, subst] => result_W
primrec I expr
- I_Var "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
+ I_Var "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
else Fail)"
- I_Abs "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
+ I_Abs "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
Ok(s, TVar n -> t, m) )"
- I_App "I (App e1 e2) a n s =
- ( (s1,t1,m1) := I e1 a n s;
- (s2,t2,m2) := I e2 a m1 s1;
- u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
- Ok($u o s2, TVar m2, Suc m2) )"
+ I_App "I (App e1 e2) a n s =
+ ( (s1,t1,m1) := I e1 a n s;
+ (s2,t2,m2) := I e2 a m1 s1;
+ u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
+ Ok($u o s2, TVar m2, Suc m2) )"
end
--- a/src/HOL/MiniML/MiniML.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/MiniML/MiniML.thy Mon Feb 05 21:29:06 1996 +0100
@@ -10,11 +10,11 @@
(* expressions *)
datatype
- expr = Var nat | Abs expr | App expr expr
+ expr = Var nat | Abs expr | App expr expr
(* type inference rules *)
consts
- has_type :: "(typ list * expr * typ)set"
+ has_type :: "(typ list * expr * typ)set"
syntax
"@has_type" :: [typ list, expr, typ] => bool
("((_) |-/ (_) :: (_))" 60)
@@ -23,10 +23,10 @@
inductive "has_type"
intrs
- VarI "[| n < length a |] ==> a |- Var n :: nth n a"
- AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
- AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |]
- ==> a |- App e1 e2 :: t1"
+ VarI "[| n < length a |] ==> a |- Var n :: nth n a"
+ AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
+ AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |]
+ ==> a |- App e1 e2 :: t1"
end
--- a/src/HOL/MiniML/Type.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/MiniML/Type.thy Mon Feb 05 21:29:06 1996 +0100
@@ -10,81 +10,81 @@
(* new class for structures containing type variables *)
classes
- type_struct < term
+ type_struct < term
(* type expressions *)
datatype
- typ = TVar nat | "->" typ typ (infixr 70)
+ typ = TVar nat | "->" typ typ (infixr 70)
(* type variable substitution *)
types
- subst = nat => typ
+ subst = nat => typ
arities
- typ::type_struct
- list::(type_struct)type_struct
- fun::(term,type_struct)type_struct
+ typ::type_struct
+ list::(type_struct)type_struct
+ fun::(term,type_struct)type_struct
(* substitutions *)
(* identity *)
consts
- id_subst :: subst
+ id_subst :: subst
defs
- id_subst_def "id_subst == (%n.TVar n)"
+ id_subst_def "id_subst == (%n.TVar n)"
(* extension of substitution to type structures *)
consts
- app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
+ app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
rules
- app_subst_TVar "$ s (TVar n) = s n"
- app_subst_Fun "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)"
+ app_subst_TVar "$ s (TVar n) = s n"
+ app_subst_Fun "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)"
defs
- app_subst_list "$ s == map ($ s)"
+ app_subst_list "$ s == map ($ s)"
(* free_tv s: the type variables occuring freely in the type structure s *)
consts
- free_tv :: ['a::type_struct] => nat set
+ free_tv :: ['a::type_struct] => nat set
rules
- free_tv_TVar "free_tv (TVar m) = {m}"
- free_tv_Fun "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
- free_tv_Nil "free_tv [] = {}"
- free_tv_Cons "free_tv (x#l) = (free_tv x) Un (free_tv l)"
+ free_tv_TVar "free_tv (TVar m) = {m}"
+ free_tv_Fun "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
+ free_tv_Nil "free_tv [] = {}"
+ free_tv_Cons "free_tv (x#l) = (free_tv x) Un (free_tv l)"
(* domain of a substitution *)
consts
- dom :: subst => nat set
+ dom :: subst => nat set
defs
- dom_def "dom s == {n. s n ~= TVar n}"
+ dom_def "dom s == {n. s n ~= TVar n}"
(* codomain of a substitutions: the introduced variables *)
consts
cod :: subst => nat set
defs
- cod_def "cod s == (UN m:dom s. free_tv (s m))"
+ cod_def "cod s == (UN m:dom s. free_tv (s m))"
defs
- free_tv_subst "free_tv s == (dom s) Un (cod s)"
+ free_tv_subst "free_tv s == (dom s) Un (cod s)"
(* new_tv s n computes whether n is a new type variable w.r.t. a type
structure s, i.e. whether n is greater than any type variable
occuring in the type structure *)
consts
- new_tv :: [nat,'a::type_struct] => bool
+ new_tv :: [nat,'a::type_struct] => bool
defs
new_tv_def "new_tv n ts == ! m. m:free_tv ts --> m<n"
(* unification algorithm mgu *)
consts
- mgu :: [typ,typ] => subst maybe
+ mgu :: [typ,typ] => subst maybe
rules
- mgu_eq "mgu t1 t2 = Ok u ==> $u t1 = $u t2"
- mgu_mg "[| (mgu t1 t2) = Ok u; $s t1 = $s t2 |] ==>
- ? r. s = $r o u"
- mgu_Ok "$s t1 = $s t2 ==> ? u. mgu t1 t2 = Ok u"
- mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2"
+ mgu_eq "mgu t1 t2 = Ok u ==> $u t1 = $u t2"
+ mgu_mg "[| (mgu t1 t2) = Ok u; $s t1 = $s t2 |] ==>
+ ? r. s = $r o u"
+ mgu_Ok "$s t1 = $s t2 ==> ? u. mgu t1 t2 = Ok u"
+ mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2"
end
--- a/src/HOL/MiniML/W.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/MiniML/W.thy Mon Feb 05 21:29:06 1996 +0100
@@ -13,16 +13,16 @@
(* type inference algorithm W *)
consts
- W :: [expr, typ list, nat] => result_W
+ W :: [expr, typ list, nat] => result_W
primrec W expr
- W_Var "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
- else Fail)"
- W_Abs "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
- Ok(s, (s n) -> t, m) )"
- W_App "W (App e1 e2) a n =
- ( (s1,t1,m1) := W e1 a n;
- (s2,t2,m2) := W e2 ($s1 a) m1;
- u := mgu ($s2 t1) (t2 -> (TVar m2));
- Ok( $u o $s2 o s1, $u (TVar m2), Suc m2) )"
+ W_Var "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
+ else Fail)"
+ W_Abs "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
+ Ok(s, (s n) -> t, m) )"
+ W_App "W (App e1 e2) a n =
+ ( (s1,t1,m1) := W e1 a n;
+ (s2,t2,m2) := W e2 ($s1 a) m1;
+ u := mgu ($s2 t1) (t2 -> (TVar m2));
+ Ok( $u o $s2 o s1, $u (TVar m2), Suc m2) )"
end
--- a/src/HOL/Subst/AList.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Subst/AList.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,5 +1,5 @@
-(* Title: Substitutions/alist.thy
- Author: Martin Coen, Cambridge University Computer Laboratory
+(* Title: Substitutions/alist.thy
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Association lists.
--- a/src/HOL/Subst/Setplus.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Subst/Setplus.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,5 +1,5 @@
-(* Title: Substitutions/setplus.thy
- Author: Martin Coen, Cambridge University Computer Laboratory
+(* Title: Substitutions/setplus.thy
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Minor additions to HOL's set theory
--- a/src/HOL/Subst/Subst.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Subst/Subst.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,5 +1,5 @@
-(* Title: Substitutions/subst.thy
- Author: Martin Coen, Cambridge University Computer Laboratory
+(* Title: Substitutions/subst.thy
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Substitutions on uterms
@@ -22,8 +22,8 @@
subst_eq_def "r =s= s == ALL t.t <| r = t <| s"
subst_def
- "t <| al == uterm_rec t (%x.assoc x (Var x) al)
- (%x.Const(x))
+ "t <| al == uterm_rec t (%x.assoc x (Var x) al)
+ (%x.Const(x))
(%u v q r.Comb q r)"
comp_def "al <> bl == alist_rec al bl (%x y xs g.(x,y <| bl)#g)"
--- a/src/HOL/Subst/UTLemmas.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Subst/UTLemmas.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,5 +1,5 @@
-(* Title: Substitutions/utermlemmas.thy
- Author: Martin Coen, Cambridge University Computer Laboratory
+(* Title: Substitutions/utermlemmas.thy
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Additional definitions for uterms that are not part of the basic inductive definition.
--- a/src/HOL/Subst/UTerm.ML Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Subst/UTerm.ML Mon Feb 05 21:29:06 1996 +0100
@@ -206,8 +206,18 @@
(*** UTerm_rec -- by wf recursion on pred_sexp ***)
-val UTerm_rec_unfold =
- [UTerm_rec_def, wf_pred_sexp RS wf_trancl] MRS def_wfrec;
+goal UTerm.thy
+ "(%M. UTerm_rec M b c d) = wfrec (trancl pred_sexp) \
+ \ (%g. Case (%x.b(x)) (Case (%y. c(y)) (Split (%x y. d x y (g x) (g y)))))";
+by (simp_tac (HOL_ss addsimps [UTerm_rec_def]) 1);
+bind_thm("UTerm_rec_unfold", (wf_pred_sexp RS wf_trancl) RS
+ ((result() RS eq_reflection) RS def_wfrec));
+
+(*---------------------------------------------------------------------------
+ * Old:
+ * val UTerm_rec_unfold =
+ * [UTerm_rec_def, wf_pred_sexp RS wf_trancl] MRS def_wfrec;
+ *---------------------------------------------------------------------------*)
(** conversion rules **)
--- a/src/HOL/Subst/UTerm.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Subst/UTerm.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,8 +1,8 @@
-(* Title: Substitutions/UTerm.thy
- Author: Martin Coen, Cambridge University Computer Laboratory
+(* Title: Substitutions/UTerm.thy
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-Simple term structure for unifiation.
+Simple term structure for unification.
Binary trees with leaves that are constants or variables.
*)
@@ -30,32 +30,32 @@
defs
(*defining the concrete constructors*)
- VAR_def "VAR(v) == In0(v)"
- CONST_def "CONST(v) == In1(In0(v))"
- COMB_def "COMB t u == In1(In1(t $ u))"
+ VAR_def "VAR(v) == In0(v)"
+ CONST_def "CONST(v) == In1(In0(v))"
+ COMB_def "COMB t u == In1(In1(t $ u))"
inductive "uterm(A)"
intrs
- VAR_I "v:A ==> VAR(v) : uterm(A)"
+ VAR_I "v:A ==> VAR(v) : uterm(A)"
CONST_I "c:A ==> CONST(c) : uterm(A)"
COMB_I "[| M:uterm(A); N:uterm(A) |] ==> COMB M N : uterm(A)"
rules
(*faking a type definition...*)
- Rep_uterm "Rep_uterm(xs): uterm(range(Leaf))"
- Rep_uterm_inverse "Abs_uterm(Rep_uterm(xs)) = xs"
- Abs_uterm_inverse "M: uterm(range(Leaf)) ==> Rep_uterm(Abs_uterm(M)) = M"
+ Rep_uterm "Rep_uterm(xs): uterm(range(Leaf))"
+ Rep_uterm_inverse "Abs_uterm(Rep_uterm(xs)) = xs"
+ Abs_uterm_inverse "M: uterm(range(Leaf)) ==> Rep_uterm(Abs_uterm(M)) = M"
defs
(*defining the abstract constructors*)
- Var_def "Var(v) == Abs_uterm(VAR(Leaf(v)))"
- Const_def "Const(c) == Abs_uterm(CONST(Leaf(c)))"
- Comb_def "Comb t u == Abs_uterm (COMB (Rep_uterm t) (Rep_uterm u))"
+ Var_def "Var(v) == Abs_uterm(VAR(Leaf(v)))"
+ Const_def "Const(c) == Abs_uterm(CONST(Leaf(c)))"
+ Comb_def "Comb t u == Abs_uterm (COMB (Rep_uterm t) (Rep_uterm u))"
(*uterm recursion*)
- UTerm_rec_def
- "UTerm_rec M b c d == wfrec (trancl pred_sexp) M
- (Case (%x g.b(x)) (Case (%y g. c(y)) (Split (%x y g. d x y (g x) (g y)))))"
+ UTerm_rec_def
+ "UTerm_rec M b c d == wfrec (trancl pred_sexp)
+ (%g. Case (%x.b(x)) (Case (%y. c(y)) (Split (%x y. d x y (g x) (g y))))) M"
uterm_rec_def
"uterm_rec t b c d ==
--- a/src/HOL/Subst/Unifier.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Subst/Unifier.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,5 +1,5 @@
-(* Title: Subst/unifier.thy
- Author: Martin Coen, Cambridge University Computer Laboratory
+(* Title: Subst/unifier.thy
+ Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Definition of most general idempotent unifier
@@ -22,7 +22,7 @@
Unifier_def "Unifier s t u == t <| s = u <| s"
MoreGeneral_def "r >> s == ? q.s =s= r <> q"
MGUnifier_def "MGUnifier s t u == Unifier s t u &
- (! r.Unifier r t u --> s >> r)"
+ (! r.Unifier r t u --> s >> r)"
MGIUnifier_def "MGIUnifier s t u == MGUnifier s t u & Idem(s)"
UWFD_def
--- a/src/HOL/ex/Acc.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Acc.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/ex/Acc.thy
+(* Title: HOL/ex/Acc.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Inductive definition of acc(r)
@@ -12,8 +12,8 @@
Acc = WF +
consts
- pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*)
- acc :: "('a * 'a)set => 'a set" (*Accessible part*)
+ pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*)
+ acc :: "('a * 'a)set => 'a set" (*Accessible part*)
defs
pred_def "pred x r == {y. (y,x):r}"
--- a/src/HOL/ex/BT.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/BT.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/ex/BT.thy
+(* Title: HOL/ex/BT.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
Binary trees (based on the ZF version)
@@ -11,9 +11,9 @@
datatype 'a bt = Lf | Br 'a ('a bt) ('a bt)
consts
- n_nodes :: 'a bt => nat
- n_leaves :: 'a bt => nat
- reflect :: 'a bt => 'a bt
+ n_nodes :: 'a bt => nat
+ n_leaves :: 'a bt => nat
+ reflect :: 'a bt => 'a bt
bt_map :: ('a=>'b) => ('a bt => 'b bt)
preorder :: 'a bt => 'a list
inorder :: 'a bt => 'a list
--- a/src/HOL/ex/InSort.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/InSort.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/ex/insort.thy
+(* Title: HOL/ex/insort.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1994 TU Muenchen
Insertion sort
--- a/src/HOL/ex/LList.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/LList.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/LList.thy
+(* Title: HOL/LList.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Definition of type 'a llist by a greatest fixed point
@@ -18,8 +18,8 @@
Previous definition of llistD_Fun was explicit:
llistD_Fun_def
- "llistD_Fun(r) ==
- {(LNil,LNil)} Un
+ "llistD_Fun(r) ==
+ {(LNil,LNil)} Un
(UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
*)
@@ -52,8 +52,8 @@
LList_corec :: "['a, 'a => unit + ('b item * 'a)] => 'b item"
llist_corec :: "['a, 'a => unit + ('b * 'a)] => 'b llist"
- Lmap :: ('a item => 'b item) => ('a item => 'b item)
- lmap :: ('a=>'b) => ('a llist => 'b llist)
+ Lmap :: ('a item => 'b item) => ('a item => 'b item)
+ lmap :: ('a=>'b) => ('a llist => 'b llist)
iterates :: ['a => 'a, 'a] => 'a llist
@@ -71,21 +71,21 @@
intrs
NIL_I "(NIL, NIL) : LListD(r)"
CONS_I "[| (a,b): r; (M,N) : LListD(r)
- |] ==> (CONS a M, CONS b N) : LListD(r)"
+ |] ==> (CONS a M, CONS b N) : LListD(r)"
defs
(*Now used exclusively for abbreviating the coinduction rule*)
list_Fun_def "list_Fun A X ==
- {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
+ {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
LListD_Fun_def "LListD_Fun r X ==
- {z. z = (NIL, NIL) |
- (? M N a b. z = (CONS a M, CONS b N) &
- (a, b) : r & (M, N) : X)}"
+ {z. z = (NIL, NIL) |
+ (? M N a b. z = (CONS a M, CONS b N) &
+ (a, b) : r & (M, N) : X)}"
(*defining the abstract constructors*)
- LNil_def "LNil == Abs_llist(NIL)"
- LCons_def "LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))"
+ LNil_def "LNil == Abs_llist(NIL)"
+ LCons_def "LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))"
llist_case_def
"llist_case c d l ==
@@ -93,8 +93,8 @@
LList_corec_fun_def
"LList_corec_fun k f ==
- nat_rec k (%x. {})
- (%j r x. sum_case (%u.NIL) (split(%z w. CONS z (r w))) (f x))"
+ nat_rec k (%x. {})
+ (%j r x. sum_case (%u.NIL) (split(%z w. CONS z (r w))) (f x))"
LList_corec_def
"LList_corec a f == UN k. LList_corec_fun k f a"
@@ -105,12 +105,12 @@
(split(%v w. Inr((Leaf(v), w)))) (f z)))"
llistD_Fun_def
- "llistD_Fun(r) ==
- prod_fun Abs_llist Abs_llist ``
- LListD_Fun (diag(range Leaf))
- (prod_fun Rep_llist Rep_llist `` r)"
+ "llistD_Fun(r) ==
+ prod_fun Abs_llist Abs_llist ``
+ LListD_Fun (diag(range Leaf))
+ (prod_fun Rep_llist Rep_llist `` r)"
- Lconst_def "Lconst(M) == lfp(%N. CONS M N)"
+ Lconst_def "Lconst(M) == lfp(%N. CONS M N)"
Lmap_def
"Lmap f M == LList_corec M (List_case (Inl ()) (%x M'. Inr((f(x), M'))))"
@@ -118,7 +118,7 @@
lmap_def
"lmap f l == llist_corec l (llist_case (Inl ()) (%y z. Inr((f(y), z))))"
- iterates_def "iterates f a == llist_corec a (%x. Inr((x, f(x))))"
+ iterates_def "iterates f a == llist_corec a (%x. Inr((x, f(x))))"
(*Append generates its result by applying f, where
f((NIL,NIL)) = Inl(())
@@ -127,18 +127,18 @@
*)
Lappend_def
- "Lappend M N == LList_corec (M,N)
+ "Lappend M N == LList_corec (M,N)
(split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2)))))
(%M1 M2 N. Inr((M1, (M2,N))))))"
lappend_def
- "lappend l n == llist_corec (l,n)
+ "lappend l n == llist_corec (l,n)
(split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2)))))
(%l1 l2 n. Inr((l1, (l2,n))))))"
rules
(*faking a type definition...*)
- Rep_llist "Rep_llist(xs): llist(range(Leaf))"
+ Rep_llist "Rep_llist(xs): llist(range(Leaf))"
Rep_llist_inverse "Abs_llist(Rep_llist(xs)) = xs"
Abs_llist_inverse "M: llist(range(Leaf)) ==> Rep_llist(Abs_llist(M)) = M"
--- a/src/HOL/ex/LexProd.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/LexProd.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/ex/lex-prod.thy
+(* Title: HOL/ex/lex-prod.thy
ID: $Id$
- Author: Tobias Nipkow, TU Munich
+ Author: Tobias Nipkow, TU Munich
Copyright 1993 TU Munich
The lexicographic product of two relations.
@@ -10,6 +10,6 @@
consts "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
rules
lex_prod_def "ra**rb == {p. ? a a' b b'.
- p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}"
+ p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}"
end
--- a/src/HOL/ex/MT.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/MT.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/ex/mt.thy
+(* Title: HOL/ex/mt.thy
ID: $Id$
- Author: Jacob Frost, Cambridge University Computer Laboratory
+ Author: Jacob Frost, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Based upon the article
--- a/src/HOL/ex/NatSum.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/NatSum.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/ex/natsum.thy
+(* Title: HOL/ex/natsum.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1994 TU Muenchen
A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
--- a/src/HOL/ex/Perm.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Perm.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/ex/Perm.thy
+(* Title: HOL/ex/Perm.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
Permutations: example of an inductive definition
--- a/src/HOL/ex/PropLog.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/PropLog.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/ex/PropLog.thy
+(* Title: HOL/ex/PropLog.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1994 TU Muenchen
Inductive definition of propositional logic.
@@ -11,11 +11,11 @@
'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
consts
thms :: 'a pl set => 'a pl set
- "|-" :: ['a pl set, 'a pl] => bool (infixl 50)
- "|=" :: ['a pl set, 'a pl] => bool (infixl 50)
- eval2 :: ['a pl, 'a set] => bool
- eval :: ['a set, 'a pl] => bool ("_[_]" [100,0] 100)
- hyps :: ['a pl, 'a set] => 'a pl set
+ "|-" :: ['a pl set, 'a pl] => bool (infixl 50)
+ "|=" :: ['a pl set, 'a pl] => bool (infixl 50)
+ eval2 :: ['a pl, 'a set] => bool
+ eval :: ['a set, 'a pl] => bool ("_[_]" [100,0] 100)
+ hyps :: ['a pl, 'a set] => 'a pl set
translations
"H |- p" == "p : thms(H)"
--- a/src/HOL/ex/Puzzle.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Puzzle.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/ex/puzzle.thy
+(* Title: HOL/ex/puzzle.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1993 TU Muenchen
An question from "Bundeswettbewerb Mathematik"
--- a/src/HOL/ex/Qsort.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Qsort.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/ex/qsort.thy
+(* Title: HOL/ex/qsort.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1994 TU Muenchen
Quicksort
--- a/src/HOL/ex/Rec.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Rec.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,8 +1,8 @@
Rec = Fixedpt +
consts
-fix :: ('a=>'a) => 'a
-Dom :: (('a=>'b) => ('a=>'b)) => 'a set
-Domf :: (('a=>'b) => ('a=>'b)) => 'a set => 'a set
+fix :: ('a=>'a) => 'a
+Dom :: (('a=>'b) => ('a=>'b)) => 'a set
+Domf :: (('a=>'b) => ('a=>'b)) => 'a set => 'a set
rules
Domf_def "Domf(F,D) == {y . !f g. (!x:D. f(x)=g(x)) --> F(f,y)=F(g,y)}"
Dom_def "Dom(F) == lfp(Domf(F))"
--- a/src/HOL/ex/SList.ML Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/SList.ML Mon Feb 05 21:29:06 1996 +0100
@@ -148,8 +148,18 @@
(* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
hold if pred_sexp^+ were changed to pred_sexp. *)
-val List_rec_unfold = [List_rec_def, wf_pred_sexp RS wf_trancl] MRS def_wfrec
- |> standard;
+goal SList.thy
+ "(%M. List_rec M c d) = wfrec (trancl pred_sexp) \
+ \ (%g. List_case c (%x y. d x y (g y)))";
+by (simp_tac (HOL_ss addsimps [List_rec_def]) 1);
+val List_rec_unfold = standard
+ ((wf_pred_sexp RS wf_trancl) RS ((result() RS eq_reflection) RS def_wfrec));
+
+(*---------------------------------------------------------------------------
+ * Old:
+ * val List_rec_unfold = [List_rec_def,wf_pred_sexp RS wf_trancl] MRS def_wfrec
+ * |> standard;
+ *---------------------------------------------------------------------------*)
(** pred_sexp lemmas **)
--- a/src/HOL/ex/SList.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/SList.thy Mon Feb 05 21:29:06 1996 +0100
@@ -27,7 +27,7 @@
NIL :: 'a item
CONS :: ['a item, 'a item] => 'a item
Nil :: 'a list
- "#" :: ['a, 'a list] => 'a list (infixr 65)
+ "#" :: ['a, 'a list] => 'a list (infixr 65)
List_case :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
List_rec :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
list_case :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
@@ -37,10 +37,10 @@
null :: 'a list => bool
hd :: 'a list => 'a
tl,ttl :: 'a list => 'a list
- mem :: ['a, 'a list] => bool (infixl 55)
+ mem :: ['a, 'a list] => bool (infixl 55)
list_all :: ('a => bool) => ('a list => bool)
map :: ('a=>'b) => ('a list => 'b list)
- "@" :: ['a list, 'a list] => 'a list (infixr 65)
+ "@" :: ['a list, 'a list] => 'a list (infixr 65)
filter :: ['a => bool, 'a list] => 'a list
(* list Enumeration *)
@@ -49,8 +49,8 @@
"@list" :: args => 'a list ("[(_)]")
(* Special syntax for list_all and filter *)
- "@Alls" :: [idt, 'a list, bool] => bool ("(2Alls _:_./ _)" 10)
- "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
+ "@Alls" :: [idt, 'a list, bool] => bool ("(2Alls _:_./ _)" 10)
+ "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
translations
"[x, xs]" == "x#[xs]"
@@ -59,8 +59,8 @@
"case xs of Nil => a | y#ys => b" == "list_case a (%y ys.b) xs"
- "[x:xs . P]" == "filter (%x.P) xs"
- "Alls x:xs.P" == "list_all (%x.P) xs"
+ "[x:xs . P]" == "filter (%x.P) xs"
+ "Alls x:xs.P" == "list_all (%x.P) xs"
defs
(* Defining the Concrete Constructors *)
@@ -89,8 +89,8 @@
(* list Recursion -- the trancl is Essential; see list.ML *)
List_rec_def
- "List_rec M c d == wfrec (trancl pred_sexp) M
- (List_case (%g.c) (%x y g. d x y (g y)))"
+ "List_rec M c d == wfrec (trancl pred_sexp)
+ (%g. List_case c (%x y. d x y (g y))) M"
list_rec_def
"list_rec l c d ==
@@ -105,14 +105,14 @@
hd_def "hd(xs) == list_rec xs (@x.True) (%x xs r.x)"
tl_def "tl(xs) == list_rec xs (@xs.True) (%x xs r.xs)"
(* a total version of tl: *)
- ttl_def "ttl(xs) == list_rec xs [] (%x xs r.xs)"
+ ttl_def "ttl(xs) == list_rec xs [] (%x xs r.xs)"
- mem_def "x mem xs ==
- list_rec xs False (%y ys r. if y=x then True else r)"
+ mem_def "x mem xs ==
+ list_rec xs False (%y ys r. if y=x then True else r)"
list_all_def "list_all P xs == list_rec xs True (%x l r. P(x) & r)"
map_def "map f xs == list_rec xs [] (%x l r. f(x)#r)"
- append_def "xs@ys == list_rec xs ys (%x l r. x#r)"
- filter_def "filter P xs ==
+ append_def "xs@ys == list_rec xs ys (%x l r. x#r)"
+ filter_def "filter P xs ==
list_rec xs [] (%x xs r. if P(x) then x#r else r)"
list_case_def "list_case a f xs == list_rec xs a (%x xs r.f x xs)"
--- a/src/HOL/ex/Simult.ML Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Simult.ML Mon Feb 05 21:29:06 1996 +0100
@@ -227,8 +227,19 @@
(*** TF_rec -- by wf recursion on pred_sexp ***)
-val TF_rec_unfold =
- wf_pred_sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
+goal Simult.thy
+ "(%M. TF_rec M b c d) = wfrec (trancl pred_sexp) \
+ \ (%g. Case (Split(%x y. b x y (g y))) \
+ \ (List_case c (%x y. d x y (g x) (g y))))";
+by (simp_tac (HOL_ss addsimps [TF_rec_def]) 1);
+val TF_rec_unfold = (wf_pred_sexp RS wf_trancl) RS
+ ((result() RS eq_reflection) RS def_wfrec);
+
+(*---------------------------------------------------------------------------
+ * Old:
+ * val TF_rec_unfold =
+ * wf_pred_sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
+ *---------------------------------------------------------------------------*)
(** conversion rules for TF_rec **)
--- a/src/HOL/ex/Simult.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Simult.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/ex/Simult
+(* Title: HOL/ex/Simult
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
A simultaneous recursive type definition: trees & forests
@@ -40,35 +40,35 @@
defs
(*the concrete constants*)
- TCONS_def "TCONS M N == In0(M $ N)"
- FNIL_def "FNIL == In1(NIL)"
- FCONS_def "FCONS M N == In1(CONS M N)"
+ TCONS_def "TCONS M N == In0(M $ N)"
+ FNIL_def "FNIL == In1(NIL)"
+ FCONS_def "FCONS M N == In1(CONS M N)"
(*the abstract constants*)
- Tcons_def "Tcons a ts == Abs_Tree(TCONS (Leaf a) (Rep_Forest ts))"
- Fnil_def "Fnil == Abs_Forest(FNIL)"
- Fcons_def "Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))"
+ Tcons_def "Tcons a ts == Abs_Tree(TCONS (Leaf a) (Rep_Forest ts))"
+ Fnil_def "Fnil == Abs_Forest(FNIL)"
+ Fcons_def "Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))"
- TF_def "TF(A) == lfp(%Z. A <*> Part Z In1
+ TF_def "TF(A) == lfp(%Z. A <*> Part Z In1
<+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"
rules
(*faking a type definition for tree...*)
- Rep_Tree "Rep_Tree(n): Part (TF(range Leaf)) In0"
+ Rep_Tree "Rep_Tree(n): Part (TF(range Leaf)) In0"
Rep_Tree_inverse "Abs_Tree(Rep_Tree(t)) = t"
Abs_Tree_inverse "z: Part (TF(range Leaf)) In0 ==> Rep_Tree(Abs_Tree(z)) = z"
(*faking a type definition for forest...*)
- Rep_Forest "Rep_Forest(n): Part (TF(range Leaf)) In1"
+ Rep_Forest "Rep_Forest(n): Part (TF(range Leaf)) In1"
Rep_Forest_inverse "Abs_Forest(Rep_Forest(ts)) = ts"
Abs_Forest_inverse
- "z: Part (TF(range Leaf)) In1 ==> Rep_Forest(Abs_Forest(z)) = z"
+ "z: Part (TF(range Leaf)) In1 ==> Rep_Forest(Abs_Forest(z)) = z"
defs
(*recursion*)
- TF_rec_def
- "TF_rec M b c d == wfrec (trancl pred_sexp) M
- (Case (Split(%x y g. b x y (g y)))
- (List_case (%g.c) (%x y g. d x y (g x) (g y))))"
+ TF_rec_def
+ "TF_rec M b c d == wfrec (trancl pred_sexp)
+ (%g. Case (Split(%x y. b x y (g y)))
+ (List_case c (%x y. d x y (g x) (g y)))) M"
tree_rec_def
"tree_rec t b c d ==
--- a/src/HOL/ex/Sorting.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Sorting.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/ex/sorting.thy
+(* Title: HOL/ex/sorting.thy
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1994 TU Muenchen
Specification of sorting
--- a/src/HOL/ex/Term.ML Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Term.ML Mon Feb 05 21:29:06 1996 +0100
@@ -110,8 +110,18 @@
(*** Term_rec -- by wf recursion on pred_sexp ***)
-val Term_rec_unfold =
- wf_pred_sexp RS wf_trancl RS (Term_rec_def RS def_wfrec);
+goal Term.thy
+ "(%M. Term_rec M d) = wfrec (trancl pred_sexp) \
+ \ (%g. Split(%x y. d x y (Abs_map g y)))";
+by (simp_tac (HOL_ss addsimps [Term_rec_def]) 1);
+bind_thm("Term_rec_unfold", (wf_pred_sexp RS wf_trancl) RS
+ ((result() RS eq_reflection) RS def_wfrec));
+
+(*---------------------------------------------------------------------------
+ * Old:
+ * val Term_rec_unfold =
+ * wf_pred_sexp RS wf_trancl RS (Term_rec_def RS def_wfrec);
+ *---------------------------------------------------------------------------*)
(** conversion rules **)
--- a/src/HOL/ex/Term.thy Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Term.thy Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/ex/Term
+(* Title: HOL/ex/Term
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Terms over a given alphabet -- function applications; illustrates list functor
@@ -16,14 +16,14 @@
arities term :: (term)term
consts
- term :: 'a item set => 'a item set
- Rep_term :: 'a term => 'a item
- Abs_term :: 'a item => 'a term
- Rep_Tlist :: 'a term list => 'a item
- Abs_Tlist :: 'a item => 'a term list
- App :: ['a, ('a term)list] => 'a term
- Term_rec :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
- term_rec :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
+ term :: 'a item set => 'a item set
+ Rep_term :: 'a term => 'a item
+ Abs_term :: 'a item => 'a term
+ Rep_Tlist :: 'a term list => 'a item
+ Abs_Tlist :: 'a item => 'a term list
+ App :: ['a, ('a term)list] => 'a term
+ Term_rec :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
+ term_rec :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
inductive "term(A)"
intrs
@@ -32,16 +32,16 @@
defs
(*defining abstraction/representation functions for term list...*)
- Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)"
- Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"
+ Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)"
+ Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"
(*defining the abstract constants*)
- App_def "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
+ App_def "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
(*list recursion*)
- Term_rec_def
- "Term_rec M d == wfrec (trancl pred_sexp) M
- (Split(%x y g. d x y (Abs_map g y)))"
+ Term_rec_def
+ "Term_rec M d == wfrec (trancl pred_sexp)
+ (%g. Split(%x y. d x y (Abs_map g y))) M"
term_rec_def
"term_rec t d ==
@@ -49,7 +49,7 @@
rules
(*faking a type definition for term...*)
- Rep_term "Rep_term(n): term(range(Leaf))"
- Rep_term_inverse "Abs_term(Rep_term(t)) = t"
- Abs_term_inverse "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
+ Rep_term "Rep_term(n): term(range(Leaf))"
+ Rep_term_inverse "Abs_term(Rep_term(t)) = t"
+ Abs_term_inverse "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
end