# HG changeset patch # User wenzelm # Date 1633373519 -7200 # Node ID 8ae5ec7eecaa7261b8fbfa43b66813fd231f0a1d # Parent aca96bd12b12bcb658a8027c780de2b8198fab75# Parent 78d1f73bbeaa0b1e6dfa64d5c33b5a038889c9a7 merged diff -r aca96bd12b12 -r 8ae5ec7eecaa Admin/components/bundled-windows --- 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 diff -r aca96bd12b12 -r 8ae5ec7eecaa NEWS diff -r aca96bd12b12 -r 8ae5ec7eecaa src/CCL/CCL.thy --- 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 \ 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); diff -r aca96bd12b12 -r 8ae5ec7eecaa src/CCL/Term.thy --- 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\i]\i" where "ncase(n,b,c) == when(n, \x. b, \y. c(y))" - -no_syntax - "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) +definition "let1" :: "[i,i\i]\i" + where let_def: "let1(t, f) == case(t,f(true),f(false), \x y. f(), \u. f(lam x. u(x)))" -definition "let" :: "[i,i\i]\i" - where "let(t, f) == case(t,f(true),f(false), \x y. f(), \u. f(lam x. u(x)))" - -syntax - "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) +syntax "_let1" :: "[idt,i,i]\i" ("(3let _ be _/ in _)" [0,0,60] 60) +translations "let x be a in e" == "CONST let1(a, \x. e)" definition letrec :: "[[i,i\i]\i,(i\i)\i]\i" where "letrec(h, b) == b(\x. fix(\f. lam x. h(x,\y. f`y))`x)" @@ -68,67 +64,65 @@ \g'. f(\x y z. g'(>)))" syntax - "_let" :: "[id,i,i]\i" ("(3let _ be _/ in _)" [0,0,60] 60) - "_letrec" :: "[id,id,i,i]\i" ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60) - "_letrec2" :: "[id,id,id,i,i]\i" ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60) - "_letrec3" :: "[id,id,id,id,i,i]\i" ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60) - -ML \ -(** 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>\let\,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>\_let\,dummyT) $ Free(id',T) $ a $ b' end; - -fun letrec_tr [Free f, Free x, a, b] = - Const(\<^const_syntax>\letrec\, dummyT) $ absfree x (absfree f a) $ absfree f b; -fun letrec2_tr [Free f, Free x, Free y, a, b] = - Const(\<^const_syntax>\letrec2\, 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>\letrec3\, dummyT) $ - absfree x (absfree y (absfree z (absfree f a))) $ absfree f b; + "_letrec" :: "[idt,idt,i,i]\i" ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60) + "_letrec2" :: "[idt,idt,idt,i,i]\i" ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60) + "_letrec3" :: "[idt,idt,idt,idt,i,i]\i" ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60) +parse_translation \ + let + fun abs_tr t u = Syntax_Trans.abs_tr [t, u]; + fun letrec_tr [f, x, a, b] = + Syntax.const \<^const_syntax>\letrec\ $ abs_tr x (abs_tr f a) $ abs_tr f b; + fun letrec2_tr [f, x, y, a, b] = + Syntax.const \<^const_syntax>\letrec2\ $ 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>\letrec3\ $ abs_tr x (abs_tr y (abs_tr z (abs_tr f a))) $ abs_tr f b; + in + [(\<^syntax_const>\_letrec\, K letrec_tr), + (\<^syntax_const>\_letrec2\, K letrec2_tr), + (\<^syntax_const>\_letrec3\, K letrec3_tr)] + end +\ +print_translation \ + 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>\_letrec\,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>\_letrec2\,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>\_letrec\ $ 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>\_letrec2\ $ 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>\_letrec3\,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>\_letrec3\ $ + bound(f',SS) $ bound(x',T) $ bound(y',U) $ bound(z',V) $ a' $ b' end; + in + [(\<^const_syntax>\letrec\, K letrec_tr'), + (\<^const_syntax>\letrec2\, K letrec2_tr'), + (\<^const_syntax>\letrec3\, K letrec3_tr')] + end \ -parse_translation \ - [(\<^syntax_const>\_let\, K let_tr), - (\<^syntax_const>\_letrec\, K letrec_tr), - (\<^syntax_const>\_letrec2\, K letrec2_tr), - (\<^syntax_const>\_letrec3\, K letrec3_tr)] -\ - -print_translation \ - [(\<^const_syntax>\let\, K let_tr'), - (\<^const_syntax>\letrec\, K letrec_tr'), - (\<^const_syntax>\letrec2\, K letrec2_tr'), - (\<^const_syntax>\letrec3\, K letrec3_tr')] -\ - - definition nrec :: "[i,i,[i,i]\i]\i" where "nrec(n,b,c) == letrec g x be ncase(x, b, \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,\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,\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 = \ 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) \ lemma ifBtrue: "if true then t else u = t" diff -r aca96bd12b12 -r 8ae5ec7eecaa src/CCL/Trancl.thy --- 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: "\r'<=r; s'<=s\ \ (r' O s') <= (r O s)" by blast @@ -202,8 +201,6 @@ done lemma trancl_into_trancl2: "\ : r; : r^+\ \ : 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 diff -r aca96bd12b12 -r 8ae5ec7eecaa src/Pure/Syntax/syntax_trans.ML --- 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; diff -r aca96bd12b12 -r 8ae5ec7eecaa src/Pure/Tools/build_docker.scala --- 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"), diff -r aca96bd12b12 -r 8ae5ec7eecaa src/Pure/term.ML --- 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 diff -r aca96bd12b12 -r 8ae5ec7eecaa src/Tools/Code/code_thingol.ML --- 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)