merged

--- a/Admin/components/bundled-windows	Mon Oct 04 16:11:18 2021 +0100
+++ b/Admin/components/bundled-windows	Mon Oct 04 20:51:59 2021 +0200
@@ -1,3 +1,3 @@
 #additional components to be bundled for release
-cygwin-20201130
+cygwin-20211002
 windows_app-20181006

--- a/src/CCL/CCL.thy	Mon Oct 04 16:11:18 2021 +0100
+++ b/src/CCL/CCL.thy	Mon Oct 04 20:51:59 2021 +0200
@@ -232,15 +232,15 @@
 
 ML \<open>
 local
-  fun pairs_of f x [] = []
+  fun pairs_of _ _ [] = []
     | pairs_of f x (y::ys) = (f x y) :: (f y x) :: (pairs_of f x ys)
 
-  fun mk_combs ff [] = []
+  fun mk_combs _ [] = []
     | mk_combs ff (x::xs) = (pairs_of ff x xs) @ mk_combs ff xs
 
   (* Doesn't handle binder types correctly *)
   fun saturate thy sy name =
-       let fun arg_str 0 a s = s
+       let fun arg_str 0 _ s = s
          | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")"
          | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s)
            val T = Sign.the_const_type thy (Sign.intern_const thy sy);

--- a/src/CCL/Term.thy	Mon Oct 04 16:11:18 2021 +0100
+++ b/src/CCL/Term.thy	Mon Oct 04 20:51:59 2021 +0200
@@ -45,15 +45,11 @@
 definition ncase :: "[i,i,i\<Rightarrow>i]\<Rightarrow>i"
   where "ncase(n,b,c) == when(n, \<lambda>x. b, \<lambda>y. c(y))"
 
-
-no_syntax
-  "_Let" :: "[letbinds, 'a] => 'a"  ("(let (_)/ in (_))" 10)
+definition "let1" :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
+  where let_def: "let1(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
 
-definition "let" :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
-  where "let(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
-
-syntax
-  "_Let" :: "[letbinds, 'a] => 'a"  ("(let (_)/ in (_))" 10)
+syntax "_let1" :: "[idt,i,i]\<Rightarrow>i"  ("(3let _ be _/ in _)" [0,0,60] 60)
+translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)"
 
 definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
   where "letrec(h, b) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)"
@@ -68,67 +64,65 @@
       \<lambda>g'. f(\<lambda>x y z. g'(<x,<y,z>>)))"
 
 syntax
-  "_let" :: "[id,i,i]\<Rightarrow>i"  ("(3let _ be _/ in _)" [0,0,60] 60)
-  "_letrec" :: "[id,id,i,i]\<Rightarrow>i"  ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60)
-  "_letrec2" :: "[id,id,id,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60)
-  "_letrec3" :: "[id,id,id,id,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60)
-
-ML \<open>
-(** Quantifier translations: variable binding **)
-
-(* FIXME does not handle "_idtdummy" *)
-(* FIXME should use Syntax_Trans.mark_bound, Syntax_Trans.variant_abs' *)
-
-fun let_tr [Free x, a, b] = Const(\<^const_syntax>\<open>let\<close>,dummyT) $ a $ absfree x b;
-fun let_tr' [a,Abs(id,T,b)] =
-     let val (id',b') = Syntax_Trans.variant_abs(id,T,b)
-     in Const(\<^syntax_const>\<open>_let\<close>,dummyT) $ Free(id',T) $ a $ b' end;
-
-fun letrec_tr [Free f, Free x, a, b] =
-      Const(\<^const_syntax>\<open>letrec\<close>, dummyT) $ absfree x (absfree f a) $ absfree f b;
-fun letrec2_tr [Free f, Free x, Free y, a, b] =
-      Const(\<^const_syntax>\<open>letrec2\<close>, dummyT) $ absfree x (absfree y (absfree f a)) $ absfree f b;
-fun letrec3_tr [Free f, Free x, Free y, Free z, a, b] =
-      Const(\<^const_syntax>\<open>letrec3\<close>, dummyT) $
-        absfree x (absfree y (absfree z (absfree f a))) $ absfree f b;
+  "_letrec" :: "[idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60)
+  "_letrec2" :: "[idt,idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60)
+  "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60)
+parse_translation \<open>
+  let
+    fun abs_tr t u = Syntax_Trans.abs_tr [t, u];
+    fun letrec_tr [f, x, a, b] =
+      Syntax.const \<^const_syntax>\<open>letrec\<close> $ abs_tr x (abs_tr f a) $ abs_tr f b;
+    fun letrec2_tr [f, x, y, a, b] =
+      Syntax.const \<^const_syntax>\<open>letrec2\<close> $ abs_tr x (abs_tr y (abs_tr f a)) $ abs_tr f b;
+    fun letrec3_tr [f, x, y, z, a, b] =
+      Syntax.const \<^const_syntax>\<open>letrec3\<close> $ abs_tr x (abs_tr y (abs_tr z (abs_tr f a))) $ abs_tr f b;
+  in
+    [(\<^syntax_const>\<open>_letrec\<close>, K letrec_tr),
+     (\<^syntax_const>\<open>_letrec2\<close>, K letrec2_tr),
+     (\<^syntax_const>\<open>_letrec3\<close>, K letrec3_tr)]
+  end
+\<close>
+print_translation \<open>
+  let
+    val bound = Syntax_Trans.mark_bound_abs;
 
-fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
-     let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
-         val (_,a'') = Syntax_Trans.variant_abs(f,S,a)
-         val (x',a') = Syntax_Trans.variant_abs(x,T,a'')
-     in Const(\<^syntax_const>\<open>_letrec\<close>,dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
-fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
-     let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
-         val ( _,a1) = Syntax_Trans.variant_abs(f,S,a)
-         val (y',a2) = Syntax_Trans.variant_abs(y,U,a1)
-         val (x',a') = Syntax_Trans.variant_abs(x,T,a2)
-     in Const(\<^syntax_const>\<open>_letrec2\<close>,dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
+    fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
+      let
+        val (f',b') = Syntax_Trans.print_abs(ff,SS,b)
+        val (_,a'') = Syntax_Trans.print_abs(f,S,a)
+        val (x',a') = Syntax_Trans.print_abs(x,T,a'')
+      in
+        Syntax.const \<^syntax_const>\<open>_letrec\<close> $ bound(f',SS) $ bound(x',T) $ a' $ b'
+      end;
+
+    fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
+      let
+        val (f',b') = Syntax_Trans.print_abs(ff,SS,b)
+        val ( _,a1) = Syntax_Trans.print_abs(f,S,a)
+        val (y',a2) = Syntax_Trans.print_abs(y,U,a1)
+        val (x',a') = Syntax_Trans.print_abs(x,T,a2)
+      in
+        Syntax.const \<^syntax_const>\<open>_letrec2\<close> $ bound(f',SS) $ bound(x',T) $ bound(y',U) $ a' $ b'
       end;
-fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
-     let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
-         val ( _,a1) = Syntax_Trans.variant_abs(f,S,a)
-         val (z',a2) = Syntax_Trans.variant_abs(z,V,a1)
-         val (y',a3) = Syntax_Trans.variant_abs(y,U,a2)
-         val (x',a') = Syntax_Trans.variant_abs(x,T,a3)
-     in Const(\<^syntax_const>\<open>_letrec3\<close>,dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
+
+    fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
+      let
+        val (f',b') = Syntax_Trans.print_abs(ff,SS,b)
+        val ( _,a1) = Syntax_Trans.print_abs(f,S,a)
+        val (z',a2) = Syntax_Trans.print_abs(z,V,a1)
+        val (y',a3) = Syntax_Trans.print_abs(y,U,a2)
+        val (x',a') = Syntax_Trans.print_abs(x,T,a3)
+      in
+        Syntax.const \<^syntax_const>\<open>_letrec3\<close> $
+          bound(f',SS) $ bound(x',T) $ bound(y',U) $ bound(z',V) $ a' $ b'
       end;
+  in
+    [(\<^const_syntax>\<open>letrec\<close>, K letrec_tr'),
+     (\<^const_syntax>\<open>letrec2\<close>, K letrec2_tr'),
+     (\<^const_syntax>\<open>letrec3\<close>, K letrec3_tr')]
+  end
 \<close>
 
-parse_translation \<open>
- [(\<^syntax_const>\<open>_let\<close>, K let_tr),
-  (\<^syntax_const>\<open>_letrec\<close>, K letrec_tr),
-  (\<^syntax_const>\<open>_letrec2\<close>, K letrec2_tr),
-  (\<^syntax_const>\<open>_letrec3\<close>, K letrec3_tr)]
-\<close>
-
-print_translation \<open>
- [(\<^const_syntax>\<open>let\<close>, K let_tr'),
-  (\<^const_syntax>\<open>letrec\<close>, K letrec_tr'),
-  (\<^const_syntax>\<open>letrec2\<close>, K letrec2_tr'),
-  (\<^const_syntax>\<open>letrec3\<close>, K letrec3_tr')]
-\<close>
-
-
 definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
   where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
 
@@ -165,38 +159,31 @@
   apply (unfold let_def)
   apply (erule rev_mp)
   apply (rule_tac t = "t" in term_case)
-      apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam)
+      apply simp_all
   done
 
 lemma letBabot: "let x be bot in f(x) = bot"
-  apply (unfold let_def)
-  apply (rule caseBbot)
-  done
+  unfolding let_def by (rule caseBbot)
 
 lemma letBbbot: "let x be t in bot = bot"
   apply (unfold let_def)
   apply (rule_tac t = t in term_case)
       apply (rule caseBbot)
-     apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam)
+     apply simp_all
   done
 
 lemma applyB: "(lam x. b(x)) ` a = b(a)"
-  apply (unfold apply_def)
-  apply (simp add: caseBtrue caseBfalse caseBpair caseBlam)
-  done
+  by (simp add: apply_def)
 
 lemma applyBbot: "bot ` a = bot"
-  apply (unfold apply_def)
-  apply (rule caseBbot)
-  done
+  unfolding apply_def by (rule caseBbot)
 
 lemma fixB: "fix(f) = f(fix(f))"
   apply (unfold fix_def)
   apply (rule applyB [THEN ssubst], rule refl)
   done
 
-lemma letrecB:
-    "letrec g x be h(x,g) in g(a) = h(a,\<lambda>y. letrec g x be h(x,g) in g(y))"
+lemma letrecB: "letrec g x be h(x,g) in g(a) = h(a,\<lambda>y. letrec g x be h(x,g) in g(y))"
   apply (unfold letrec_def)
   apply (rule fixB [THEN ssubst], rule applyB [THEN ssubst], rule refl)
   done
@@ -205,8 +192,10 @@
 
 method_setup beta_rl = \<open>
   Scan.succeed (fn ctxt =>
-    SIMPLE_METHOD' (CHANGED o
-      simp_tac (ctxt addsimps @{thms rawBs} setloop (fn _ => stac ctxt @{thm letrecB}))))
+    let val ctxt' = Context_Position.set_visible false ctxt in
+      SIMPLE_METHOD' (CHANGED o
+        simp_tac (ctxt' addsimps @{thms rawBs} setloop (fn _ => stac ctxt @{thm letrecB})))
+    end)
 \<close>
 
 lemma ifBtrue: "if true then t else u = t"

--- a/src/CCL/Trancl.thy	Mon Oct 04 16:11:18 2021 +0100
+++ b/src/CCL/Trancl.thy	Mon Oct 04 20:51:59 2021 +0200
@@ -66,7 +66,6 @@
 
 lemmas [intro] = compI idI
   and [elim] = compE idE
-  and [elim!] = pair_inject
 
 lemma comp_mono: "\<lbrakk>r'<=r; s'<=s\<rbrakk> \<Longrightarrow> (r' O s') <= (r O s)"
   by blast
@@ -202,8 +201,6 @@
   done
 
 lemma trancl_into_trancl2: "\<lbrakk><a,b> : r; <b,c> : r^+\<rbrakk> \<Longrightarrow> <a,c> : r^+"
-  apply (rule r_into_trancl [THEN trans_trancl [THEN transD]])
-   apply assumption+
-  done
+  by (rule r_into_trancl [THEN trans_trancl [THEN transD]])
 
 end

--- a/src/Pure/Syntax/syntax_trans.ML	Mon Oct 04 16:11:18 2021 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML	Mon Oct 04 20:51:59 2021 +0200
@@ -38,8 +38,7 @@
   val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term)
   val preserve_binder_abs_tr': string -> string -> string * (Proof.context -> term list -> term)
   val preserve_binder_abs2_tr': string -> string -> string * (Proof.context -> term list -> term)
-  val variant_abs: string * typ * term -> string * term
-  val variant_abs': string * typ * term -> string * term
+  val print_abs: string * typ * term -> string * term
   val dependent_tr': string * string -> term list -> term
   val antiquote_tr': string -> term -> term
   val quote_tr': string -> term -> term
@@ -129,8 +128,7 @@
 
 fun abs_tr [Free x, t] = absfree_proper x t
   | abs_tr [Const ("_idtdummy", T), t] = absdummy T t
-  | abs_tr [Const ("_constrain", _) $ x $ tT, t] =
-      Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT
+  | abs_tr [Const ("_constrain", _) $ x $ tT, t] = Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT
   | abs_tr ts = raise TERM ("abs_tr", ts);
 
 
@@ -140,9 +138,7 @@
   let
     fun err ts = raise TERM ("binder_tr: " ^ syn, ts)
     fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
-      | binder_tr [x, t] =
-          let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
-          in Syntax.const name $ abs end
+      | binder_tr [x, t] = Syntax.const name $ (abs_tr [x, t] handle TERM _ => err [x, t])
       | binder_tr ts = err ts;
   in (syn, fn _ => binder_tr) end;
 
@@ -392,16 +388,13 @@
 
 (* dependent / nondependent quantifiers *)
 
-fun var_abs mark (x, T, b) =
+fun print_abs (x, T, b) =
   let val (x', _) = Name.variant x (Term.declare_term_names b Name.context)
-  in (x', subst_bound (mark (x', T), b)) end;
-
-val variant_abs = var_abs Free;
-val variant_abs' = var_abs mark_bound_abs;
+  in (x', subst_bound (mark_bound_abs (x', T), b)) end;
 
 fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
       if Term.is_dependent B then
-        let val (x', B') = variant_abs' (x, dummyT, B);
+        let val (x', B') = print_abs (x, dummyT, B);
         in Term.list_comb (Syntax.const q $ mark_bound_abs (x', T) $ A $ B', ts) end
       else Term.list_comb (Syntax.const r $ A $ incr_boundvars ~1 B, ts)
   | dependent_tr' _ _ = raise Match;

--- a/src/Pure/Tools/build_docker.scala	Mon Oct 04 16:11:18 2021 +0100
+++ b/src/Pure/Tools/build_docker.scala	Mon Oct 04 20:51:59 2021 +0200
@@ -15,7 +15,7 @@
   private val Isabelle_Name = """^.*?(Isabelle[^/\\:]+)_linux\.tar\.gz$""".r
 
   val packages: List[String] =
-    List("curl", "less", "libfontconfig1", "libgomp1", "perl", "pwgen", "rlwrap", "unzip")
+    List("curl", "less", "libfontconfig1", "libgomp1", "pwgen", "rlwrap", "unzip")
 
   val package_collections: Map[String, List[String]] =
     Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"),

--- a/src/Pure/term.ML	Mon Oct 04 16:11:18 2021 +0100
+++ b/src/Pure/term.ML	Mon Oct 04 20:51:59 2021 +0200
@@ -165,6 +165,7 @@
   val could_beta_contract: term -> bool
   val could_eta_contract: term -> bool
   val could_beta_eta_contract: term -> bool
+  val used_free: string -> term -> bool
   val dest_abs: string * typ * term -> string * term
   val dummy_pattern: typ -> term
   val dummy: term

--- a/src/Tools/Code/code_thingol.ML	Mon Oct 04 16:11:18 2021 +0100
+++ b/src/Tools/Code/code_thingol.ML	Mon Oct 04 20:51:59 2021 +0200
@@ -622,9 +622,8 @@
       pair (IVar (SOME v))
   | translate_term ctxt algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
       let
-        val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize (SOME false) v, ty, t);
-        val v'' = if member (op =) (Term.add_free_names t' []) v'
-          then SOME v' else NONE
+        val (v', t') = Term.dest_abs (Name.desymbolize (SOME false) v, ty, t);
+        val v'' = if Term.used_free v' t' then SOME v' else NONE
       in
         translate_typ ctxt algbr eqngr permissive ty
         ##>> translate_term ctxt algbr eqngr permissive some_thm (t', some_abs)