src/HOL/Lambda/ListBeta.thy

--- a/src/HOL/Lambda/ListBeta.thy	Wed Oct 31 22:04:29 2001 +0100
+++ b/src/HOL/Lambda/ListBeta.thy	Wed Oct 31 22:05:37 2001 +0100
@@ -18,7 +18,7 @@
   "rs => ss" == "(rs, ss) : step1 beta"
 
 lemma head_Var_reduction_aux:
-  "v -> v' ==> \<forall>rs. v = Var n $$ rs --> (\<exists>ss. rs => ss \<and> v' = Var n $$ ss)"
+  "v -> v' ==> \<forall>rs. v = Var n \<degree>\<degree> rs --> (\<exists>ss. rs => ss \<and> v' = Var n \<degree>\<degree> ss)"
   apply (erule beta.induct)
      apply simp
     apply (rule allI)
@@ -32,16 +32,16 @@
   done
 
 lemma head_Var_reduction:
-  "Var n $$ rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n $$ ss)"
+  "Var n \<degree>\<degree> rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss)"
   apply (drule head_Var_reduction_aux)
   apply blast
   done
 
 lemma apps_betasE_aux:
-  "u -> u' ==> \<forall>r rs. u = r $$ rs -->
-    ((\<exists>r'. r -> r' \<and> u' = r' $$ rs) \<or>
-     (\<exists>rs'. rs => rs' \<and> u' = r $$ rs') \<or>
-     (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] $$ ts))"
+  "u -> u' ==> \<forall>r rs. u = r \<degree>\<degree> rs -->
+    ((\<exists>r'. r -> r' \<and> u' = r' \<degree>\<degree> rs) \<or>
+     (\<exists>rs'. rs => rs' \<and> u' = r \<degree>\<degree> rs') \<or>
+     (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] \<degree>\<degree> ts))"
   apply (erule beta.induct)
      apply (clarify del: disjCI)
      apply (case_tac r)
@@ -70,12 +70,12 @@
   done
 
 lemma apps_betasE [elim!]:
-  "[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R;
-    !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R;
-    !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] $$ us |] ==> R |]
+  "[| r \<degree>\<degree> rs -> s; !!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R;
+    !!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R;
+    !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R |]
   ==> R"
 proof -
-  assume major: "r $$ rs -> s"
+  assume major: "r \<degree>\<degree> rs -> s"
   case rule_context
   show ?thesis
     apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
@@ -84,20 +84,20 @@
 qed
 
 lemma apps_preserves_beta [simp]:
-    "r -> s ==> r $$ ss -> s $$ ss"
+    "r -> s ==> r \<degree>\<degree> ss -> s \<degree>\<degree> ss"
   apply (induct_tac ss rule: rev_induct)
   apply auto
   done
 
 lemma apps_preserves_beta2 [simp]:
-    "r ->> s ==> r $$ ss ->> s $$ ss"
+    "r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss"
   apply (erule rtrancl_induct)
    apply blast
   apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
   done
 
 lemma apps_preserves_betas [rule_format, simp]:
-    "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
+    "\<forall>ss. rs => ss --> r \<degree>\<degree> rs -> r \<degree>\<degree> ss"
   apply (induct_tac rs rule: rev_induct)
    apply simp
   apply simp